From d10e1133fa7517965541f05d9fcf5d049277b767 Mon Sep 17 00:00:00 2001
From: David Pichardie <dpichardie@meta.com>
Date: Wed, 31 Jul 2024 03:47:51 -0700
Subject: [PATCH] [stats] count the unknown calls

Summary: we increment the (new) counter each time pulse uses an unknown call

Reviewed By: thizanne

Differential Revision:
D60456696

Privacy Context Container: L1122176

fbshipit-source-id: f53ee58e4f6a16cf5d83b315bc9b2f3fc42872fa
---
 infer/src/base/Stats.ml  | 7 ++++++-
 infer/src/base/Stats.mli | 2 ++
 infer/src/pulse/Pulse.ml | 1 +
 3 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/infer/src/base/Stats.ml b/infer/src/base/Stats.ml
index 15c7d04fa96..814ed6b3c2d 100644
--- a/infer/src/base/Stats.ml
+++ b/infer/src/base/Stats.ml
@@ -172,6 +172,7 @@ type t =
   ; mutable pulse_captured_vars_length_contradictions: IntCounter.t
   ; mutable pulse_disjuncts_dropped: IntCounter.t
   ; mutable pulse_interrupted_loops: IntCounter.t
+  ; mutable pulse_unknown_calls: IntCounter.t
   ; mutable pulse_summaries_contradictions: IntCounter.t
   ; mutable pulse_summaries_unsat_for_caller: IntCounter.t
   ; mutable pulse_summaries_unsat_for_caller_percent: IntCounter.t
@@ -261,7 +262,7 @@ let pp fmt stats =
     ~pulse_args_length_contradictions:(pp_int_field fmt)
     ~pulse_captured_vars_length_contradictions:(pp_int_field fmt)
     ~pulse_disjuncts_dropped:(pp_int_field fmt) ~pulse_interrupted_loops:(pp_int_field fmt)
-    ~pulse_summaries_contradictions:(pp_int_field fmt)
+    ~pulse_unknown_calls:(pp_int_field fmt) ~pulse_summaries_contradictions:(pp_int_field fmt)
     ~pulse_summaries_count:(pp_pulse_summaries_count fmt)
     ~pulse_summaries_count_0_continue_program:(pp_int_field fmt)
     ~pulse_summaries_count_0_percent:(pp_int_field fmt)
@@ -285,6 +286,7 @@ let log_to_file
     ; pulse_captured_vars_length_contradictions
     ; pulse_disjuncts_dropped
     ; pulse_interrupted_loops
+    ; pulse_unknown_calls
     ; pulse_summaries_contradictions
     ; pulse_summaries_unsat_for_caller
     ; pulse_summaries_unsat_for_caller_percent
@@ -306,6 +308,7 @@ let log_to_file
     pulse_captured_vars_length_contradictions ;
   F.fprintf fmt "pulse_disjuncts_dropped: %d@\n" pulse_disjuncts_dropped ;
   F.fprintf fmt "pulse_interrupted_loops: %d@\n" pulse_interrupted_loops ;
+  F.fprintf fmt "pulse_unknown_calls: %d@\n" pulse_unknown_calls ;
   F.fprintf fmt "pulse_summaries_contradictions: %d@\n" pulse_summaries_contradictions ;
   F.fprintf fmt "pulse_summaries_unsat_for_caller: %d@\n" pulse_summaries_unsat_for_caller ;
   F.fprintf fmt "pulse_summaries_with_some_unreachable_nodes: %d@\n"
@@ -416,6 +419,8 @@ let add_pulse_disjuncts_dropped n = add Fields.pulse_disjuncts_dropped n
 
 let add_pulse_interrupted_loops n = add Fields.pulse_interrupted_loops n
 
+let incr_pulse_unknown_calls () = incr Fields.pulse_unknown_calls
+
 let incr_pulse_summaries_contradictions () = incr Fields.pulse_summaries_contradictions
 
 let incr_pulse_summaries_unsat_for_caller () = incr Fields.pulse_summaries_unsat_for_caller
diff --git a/infer/src/base/Stats.mli b/infer/src/base/Stats.mli
index 441bd08916b..b98f8943cbd 100644
--- a/infer/src/base/Stats.mli
+++ b/infer/src/base/Stats.mli
@@ -40,6 +40,8 @@ val add_pulse_disjuncts_dropped : int -> unit
 
 val add_pulse_interrupted_loops : int -> unit
 
+val incr_pulse_unknown_calls : unit -> unit
+
 val incr_pulse_summaries_contradictions : unit -> unit
 
 val incr_pulse_summaries_unsat_for_caller : unit -> unit
diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index 9677ed00a6c..34abfc50102 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -969,6 +969,7 @@ module PulseTransferFunctions = struct
             let call_was_unknown =
               match call_was_unknown with `UnknownCall -> true | `KnownCall -> false
             in
+            if call_was_unknown then Stats.incr_pulse_unknown_calls () ;
             let ret_opt = PulseOperations.read_id (fst ret) astate in
             let+ astate =
               let astate_after_call =