From db0064a68a8f5c13b0e187c782ebfd3563d3ff16 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@meta.com>
Date: Tue, 17 Dec 2024 04:52:33 -0800
Subject: [PATCH] [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
---
 infer/src/pulse/PulseCallOperations.ml  |  4 +++-
 infer/src/pulse/PulseExecutionDomain.ml |  2 +-
 infer/src/pulse/PulseResult.ml          | 10 ++++++++++
 infer/src/pulse/PulseResult.mli         |  8 ++++++++
 4 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml
index 8635a9a0046..4e544b340e7 100644
--- 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
index 04197ceb007..776baaa9d85 100644
--- 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
index f4b49bb92c4..e4e1893d919 100644
--- 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
index 724fdd0e867..571d1ebb6e3 100644
--- a/infer/src/pulse/PulseResult.mli
+++ b/infer/src/pulse/PulseResult.mli
@@ -6,6 +6,7 @@
  *)
 
 open! IStd
+module F = Format
 
 [@@@warning "-unused-value-declaration"]
 
@@ -13,6 +14,13 @@ open! IStd
     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 *)