[quandary] better printing of sources

Summary:
Rather than printing the footprint using its actual representation (an access trie with bool nodes), print it as a set of access paths.
This makes it easier to read sources in Quandary specs/debug Quandary.

Reviewed By: jeremydubreil

Differential Revision: D5682630

fbshipit-source-id: ac55b7f

infer/src/checkers/Trace.ml

@@ -188,7 +188,10 @@ module Make (Spec : Spec) = struct
         {known; footprint}
 
     let pp fmt {known; footprint} =
-      F.fprintf fmt "Known: %a@\nFootprint: %a@\n" Known.pp known Footprint.pp footprint
+      if Known.is_empty known then
+        if Footprint.is_empty footprint then F.fprintf fmt "{}"
+        else F.fprintf fmt "Footprint(%a)" Footprint.pp footprint
+      else F.fprintf fmt "%a + Footprint(%a)" Known.pp known Footprint.pp footprint
 
     let empty = {known= Known.empty; footprint= Footprint.empty}
 

infer/src/checkers/accessTree.ml

@@ -329,4 +329,11 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct
   let pp fmt base_tree = BaseMap.pp ~pp_value:pp_node fmt base_tree
 end
 
-module PathSet = Make (AbstractDomain.BooleanOr)
+module PathSet = struct
+  include Make (AbstractDomain.BooleanOr)
+
+  (* print as a set of paths rather than a map of paths to bools *)
+  let pp fmt tree =
+    let collect_path acc access_path (is_mem, _) = if is_mem then access_path :: acc else acc in
+    fold collect_path tree [] |> PrettyPrintable.pp_collection ~pp_item:AccessPath.Abs.pp fmt
+end