[pulse][minor] easier-to-understand debug output

Summary:
- number the disjuncts in the abstract state and in the specs: #0, #1, ... This makes it much easier to know which disjunct the rest of the debug output is talking about, eg in "Executing from disjunct #N" messages
- label the currently-inferred precondition with `PRE=` instead of just
  putting it in square brackets
- print value histories when the debug level is >= 3
- separate the memory printing into heap and attributes labelled more
  explicitly

For example, before:

```
2 disjuncts:
{ {visited= false;
   astate= { heap=({ v1 -> { * -> v3 }, v2 -> { * -> v5 } },
                  { v5 -> { CppDelete(was invalidated by `delete`) } });
             stack={ &n=v1, &ptr=v2 };}
           [{ heap=({ v1 -> { * -> v3 },
                      v2 -> { * -> v5 },
                      v3 -> { },
                      v5 -> { } },
                   { v1 -> { MustBeValid (read by   line 57, column 7) },
                     v2 -> { MustBeValid (read by   line 58, column 12) },
                     v5 -> { MustBeValid (read by   line 58, column 5) } });
              stack={ &n=v1, &ptr=v2 };}]},
  {visited= false;
   astate= { heap=({ v1 -> { * -> v3 }, v2 -> { * -> v7 } },
                  { v7 -> { CppDelete(was invalidated by `delete`) } });
             stack={ &n=v1, &ptr=v2 };}
           [{ heap=({ v1 -> { * -> v3 },
                      v2 -> { * -> v7 },
                      v3 -> { },
                      v7 -> { } },
                   { v1 -> { MustBeValid (read by   line 57, column 7) },
                     v2 -> { MustBeValid (read by   line 60, column 12) },
                     v7 -> { MustBeValid (read by   line 60, column 5) } });
              stack={ &n=v1, &ptr=v2 };}]} }
```

after:

```
2 disjuncts:
#0: visited=false;
    { roots={ &n=v1, &ptr=v2 };
      mem  ={ v1 -> { * -> v3 }, v2 -> { * -> v4 } };
      attrs={ v3 -> { =7 },
              v4 -> { CppDelete(was invalidated by `delete`) } };}
    PRE=[{ roots={ &n=v1, &ptr=v2 };
           mem  ={ v1 -> { * -> v3 },
                   v2 -> { * -> v4 },
                   v3 -> { },
                   v4 -> { } };
           attrs={ v1 -> { MustBeValid (read by   line 57, column 7) },
                   v2 -> { MustBeValid (read by   line 58, column 12) },
                   v4 -> { MustBeValid (read by   line 58, column 5) } };}]
#1: visited=false;
    { roots={ &n=v1, &ptr=v2 };
      mem  ={ v1 -> { * -> v3 }, v2 -> { * -> v5 } };
      attrs={ v5 -> { CppDelete(was invalidated by `delete`) } };}
    PRE=[{ roots={ &n=v1, &ptr=v2 };
           mem  ={ v1 -> { * -> v3 },
                   v2 -> { * -> v5 },
                   v3 -> { },
                   v5 -> { } };
           attrs={ v1 -> { MustBeValid (read by   line 57, column 7) },
                   v2 -> { MustBeValid (read by   line 60, column 12) },
                   v5 -> { MustBeValid (read by   line 60, column 5) } };}]

```

Reviewed By: ezgicicek

Differential Revision: D17906167

fbshipit-source-id: 2e14325c8

infer/src/absint/TransferFunctions.ml

@@ -66,8 +66,7 @@ module MakeDisjunctive (TransferFunctions : DisjReady) (DConfig : DisjunctiveCon
     type disjunct = {visited: bool; astate: TransferFunctions.Domain.t}
 
     let pp_disjunct fmt ({visited; astate}[@warning "+9"]) =
-      F.fprintf fmt "{@[<hv>visited= %b;@;astate= @[%a@]@]}" visited TransferFunctions.Domain.pp
-        astate
+      F.fprintf fmt "@[<hv>visited=%b;@;@[%a@]@]" visited TransferFunctions.Domain.pp astate
 
 
     type t = disjunct list
@@ -79,9 +78,11 @@ module MakeDisjunctive (TransferFunctions : DisjReady) (DConfig : DisjunctiveCon
     let elements disjuncts = List.map disjuncts ~f:(fun {astate} -> astate)
 
     let pp f disjuncts =
-      F.fprintf f "@[<v>%d disjuncts:@;%a@]" (List.length disjuncts)
-        (PrettyPrintable.pp_collection ~pp_item:pp_disjunct)
-        disjuncts
+      let pp_disjuncts f disjuncts =
+        List.iteri disjuncts ~f:(fun i disjunct ->
+            F.fprintf f "#%d: @[%a@]@;" i pp_disjunct disjunct )
+      in
+      F.fprintf f "@[<v>%d disjuncts:@;%a@]" (List.length disjuncts) pp_disjuncts disjuncts
   end
 
   type disjunct_t = Disjuncts.disjunct = {visited: bool; astate: TransferFunctions.Domain.t}

infer/src/pulse/PulseAbductiveDomain.ml

@@ -70,7 +70,7 @@ type t =
   { post: Domain.t  (** state at the current program point*)
   ; pre: InvertedDomain.t  (** inferred pre at the current program point *) }
 
-let pp f {post; pre} = F.fprintf f "@[<v>%a@;[%a]@]" Domain.pp post InvertedDomain.pp pre
+let pp f {post; pre} = F.fprintf f "@[<v>%a@;PRE=[%a]@]" Domain.pp post InvertedDomain.pp pre
 
 let ( <= ) ~lhs ~rhs =
   match

infer/src/pulse/PulseDomain.ml

@@ -222,7 +222,12 @@ end
 module Trace = struct
   type 'a t = {action: 'a InterprocAction.t; history: ValueHistory.t} [@@deriving compare]
 
-  let pp pp_immediate f {action; _} = InterprocAction.pp pp_immediate f action
+  let pp pp_immediate f {action; history} =
+    if Config.debug_level_analysis < 3 then InterprocAction.pp pp_immediate f action
+    else
+      F.fprintf f "{@[action=@[%a@]@;history=@[%a@]@]}" (InterprocAction.pp pp_immediate) action
+        ValueHistory.pp history
+
 
   let add_errlog_header ~title location errlog =
     let depth = 0 in
@@ -464,7 +469,9 @@ module Memory : sig
 
   val mem_edges : AbstractAddress.t -> t -> bool
 
-  val pp : F.formatter -> t -> unit
+  val pp_heap : F.formatter -> t -> unit
+
+  val pp_attributes : F.formatter -> t -> unit
 
   val register_address : AbstractAddress.t -> t -> t
 
@@ -506,7 +513,9 @@ end = struct
 
   type t = edges Graph.t * Attributes.t Graph.t
 
-  let pp = Pp.pair ~fst:(Graph.pp ~pp_value:pp_edges) ~snd:(Graph.pp ~pp_value:Attributes.pp)
+  let pp_heap fmt (heap, _) = Graph.pp ~pp_value:pp_edges fmt heap
+
+  let pp_attributes fmt (_, attrs) = Graph.pp ~pp_value:Attributes.pp fmt attrs
 
   let register_address addr memory =
     if Graph.mem addr (fst memory) then memory
@@ -796,7 +805,8 @@ let ( <= ) ~lhs ~rhs =
 
 
 let pp fmt {heap; stack} =
-  F.fprintf fmt "{@[<v1> heap=@[<hv>%a@];@;stack=@[<hv>%a@];@]}" Memory.pp heap Stack.pp stack
+  F.fprintf fmt "{@[<v1> roots=@[<hv>%a@];@;mem  =@[<hv>%a@];@;attrs=@[<hv>%a@];@]}" Stack.pp stack
+    Memory.pp_heap heap Memory.pp_attributes heap
 
 
 module GraphVisit : sig

infer/src/pulse/PulseSummary.ml

@@ -5,10 +5,15 @@
  * LICENSE file in the root directory of this source tree.
  *)
 open! IStd
+module F = Format
 
 type t = PulseAbductiveDomain.PrePost.t list
 
 let of_posts pdesc posts = List.map posts ~f:(PulseAbductiveDomain.PrePost.of_post pdesc)
 
 let pp fmt summary =
-  PrettyPrintable.pp_collection ~pp_item:PulseAbductiveDomain.PrePost.pp fmt summary
+  F.open_vbox 0 ;
+  F.fprintf fmt "%d pre/post(s)@;" (List.length summary) ;
+  List.iteri summary ~f:(fun i pre_post ->
+      F.fprintf fmt "#%d: @[%a@]@;" i PulseAbductiveDomain.PrePost.pp pre_post ) ;
+  F.close_box ()