[pulse] a little more logging

Summary: I've found these useful. In particular, print "ContinueProgram" in front of ContinueProgram disjuncts just to be more explicit. Reviewed By: hajduakos, dulmarod Differential Revision: D67276992 fbshipit-source-id: f144a0a03200906691cb4198dda982f9770809a1
jeremydubreil · Dec 17, 2024 · db0064a · db0064a
1 parent d79b340
commit db0064a
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 2 deletions.
diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml
@@ -527,7 +527,9 @@ let call_aux disjunct_limit ({InterproceduralAnalysis.tenv} as analysis_data) pa
           (not path.PathContext.is_non_disj)
           && ( Option.exists disjunct_limit ~f:(fun limit -> List.length posts >= limit)
              || (should_keep_at_most_one_disjunct && not (List.is_empty posts)) )
-        then (posts, contradiction)
+        then (
+          L.d_printfln "disjunct limit reached, stop applying callee pre/posts" ;
+          (posts, contradiction) )
         else (
           (* apply one pre/post spec, check for timeouts in-between each pre/post spec from the callee
               *)

diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml
@@ -74,7 +74,7 @@ let pp_header kind fmt = function
   | AbortProgram _ ->
       Pp.with_color kind Red F.pp_print_string fmt "AbortProgram"
   | ContinueProgram _ ->
-      ()
+      F.pp_print_string fmt "ContinueProgram"
   | ExceptionRaised _ ->
       Pp.with_color kind Orange F.pp_print_string fmt "ExceptionRaised"
   | ExitProgram _ ->

diff --git a/infer/src/pulse/PulseResult.ml b/infer/src/pulse/PulseResult.ml
@@ -6,10 +6,20 @@
  *)
 
 open! IStd
+module F = Format
 module L = Logging
 
 type ('ok, 'err) t = Ok of 'ok | Recoverable of 'ok * 'err list | FatalError of 'err * 'err list
 
+let pp pp_ok pp_err fmt = function
+  | Ok ok ->
+      F.fprintf fmt "Ok (%a)" pp_ok ok
+  | Recoverable (ok, errs) ->
+      F.fprintf fmt "Recoverable (%a, [%a])" pp_ok ok (Pp.comma_seq pp_err) errs
+  | FatalError (err, errs) ->
+      F.fprintf fmt "FatalError (%a, [%a])" pp_err err (Pp.comma_seq pp_err) errs
+
+
 let append_errors errors result =
   if List.is_empty errors then result
   else

diff --git a/infer/src/pulse/PulseResult.mli b/infer/src/pulse/PulseResult.mli
@@ -6,13 +6,21 @@
  *)
 
 open! IStd
+module F = Format
 
 [@@@warning "-unused-value-declaration"]
 
 (** Pulse's base error monad: some errors can be accumulated along paths, others are fatal and
     there's no point continuing the execution. *)
 type ('ok, 'err) t = Ok of 'ok | Recoverable of 'ok * 'err list | FatalError of 'err * 'err list
 
+val pp :
+     (F.formatter -> 'ok -> unit)
+  -> (F.formatter -> 'err -> unit)
+  -> F.formatter
+  -> ('ok, 'err) t
+  -> unit
+
 val append_errors : 'err list -> ('ok, 'err) t -> ('ok, 'err) t
 (** adds the given error list to the result, possibly changing an [Ok] result into a [Recoverable]
     one in the process *)