From ac62b64009351fa7d86e49602b79c487bfb104bb Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Thu, 11 Apr 2019 03:55:14 -0700
Subject: [PATCH] [pulse][minor] improve debug html

Summary:
Useful to know which disjunct is being executed. Reprinting them
wholesale is too spammy so compromise by outputting just enough to be
able to reconstruct the info "which disjunct was executed and which new
disjuncts were produced?".

Reviewed By: ngorogiannis

Differential Revision: D14753495

fbshipit-source-id: f5aa68160
---
 infer/src/absint/TransferFunctions.ml   | 16 ++++++++++++----
 infer/src/pulse/PulseAbductiveDomain.ml |  2 +-
 2 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml
index 8c700ded0..41be53d4e 100644
--- a/infer/src/absint/TransferFunctions.ml
+++ b/infer/src/absint/TransferFunctions.ml
@@ -7,6 +7,7 @@
 
 open! IStd
 module F = Format
+module L = Logging
 
 module type S = sig
   module CFG : ProcCfg.S
@@ -156,7 +157,7 @@ module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : Disjunct
   end
 
   let exec_instr pre_disjuncts extras node instr =
-    List.fold pre_disjuncts ~init:[] ~f:(fun post_disjuncts pre_disjunct ->
+    List.foldi pre_disjuncts ~init:[] ~f:(fun i post_disjuncts pre_disjunct ->
         if pre_disjunct.visited then
           (* SUBTLE/WORST HACK EVER: ignore pres that we know we have gone through already. This
              means that the invariant map at that program point will be junk since they are going to
@@ -165,9 +166,16 @@ module MakeHILDisjunctive (TransferFunctions : HILDisjReady) (DConfig : Disjunct
 
              This should really be implemented in {!AbstractInterpreter}. *)
           post_disjuncts
-        else
-          let disjuncts' = TransferFunctions.exec_instr pre_disjunct.astate extras node instr in
-          Domain.join post_disjuncts (List.map disjuncts' ~f:Disjuncts.mk_disjunct) )
+        else (
+          L.d_printfln "@[<v2>Executing from disjunct #%d@;" i ;
+          let disjuncts' =
+            TransferFunctions.exec_instr pre_disjunct.astate extras node instr
+            |> List.map ~f:Disjuncts.mk_disjunct
+          in
+          ( if Config.write_html then
+            let n = List.length disjuncts' in
+            L.d_printfln "@]@\n@[Got %d disjunct%s back@]" n (if Int.equal n 1 then "" else "s") ) ;
+          Domain.join post_disjuncts disjuncts' ) )
 
 
   let pp_session_name node f = TransferFunctions.pp_session_name node f
diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index cac02f451..3c526b790 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -456,7 +456,7 @@ module PrePost = struct
 
   let rec record_post_for_address callee_proc_name call_loc ({pre; post} as pre_post) ~addr_callee
       ~addr_caller call_state =
-    L.d_printfln "%a<->%a@\n" AbstractAddress.pp addr_callee AbstractAddress.pp addr_caller ;
+    L.d_printfln "%a<->%a" AbstractAddress.pp addr_callee AbstractAddress.pp addr_caller ;
     match visit call_state ~addr_callee ~addr_caller with
     | `AlreadyVisited, call_state ->
         call_state