[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
telekom · Jul 31, 2024 · d10e113 · d10e113
1 parent d47d9b3
commit d10e113
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 1 deletion.
diff --git 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
@@ -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
@@ -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 =