[quandary] better printing for access trees

Summary:
Add `is_empty` to `AbstractDomain.WithBottom` sig and use the empty checks for nicer printing of access trees: don't print empty nodes/traces.
This should make it easier to debug Quandary; it's pretty hard to stare at an access tree and see what's going on right now.

Reviewed By: jberdine

Differential Revision: D5682248

fbshipit-source-id: 56d2a9d

infer/src/absint/AbstractDomain.ml

@@ -28,6 +28,8 @@ module type WithBottom = sig
   include S
 
   val empty : astate
+
+  val is_empty : astate -> bool
 end
 
 module type WithTop = sig
@@ -41,6 +43,8 @@ module BottomLifted (Domain : S) = struct
 
   let empty = Bottom
 
+  let is_empty = function Bottom -> true | NonBottom _ -> false
+
   let ( <= ) ~lhs ~rhs =
     if phys_equal lhs rhs then true
     else
@@ -264,6 +268,8 @@ module BooleanOr = struct
 
   let empty = false
 
+  let is_empty astate = not astate
+
   let ( <= ) ~lhs ~rhs = not lhs || rhs
 
   let join = ( || )

infer/src/absint/AbstractDomain.mli

@@ -33,6 +33,9 @@ module type WithBottom = sig
   (** The bottom value of the domain.
       Naming it empty instead of bottom helps to bind the empty
       value for sets and maps to the natural definition for bottom *)
+
+  val is_empty : astate -> bool
+  (** Return true if this is the bottom value *)
 end
 
 (** A domain with an explicit top value *)

infer/src/checkers/ThreadSafetyDomain.ml

@@ -328,6 +328,11 @@ let empty =
   let escapees = EscapeeDomain.empty in
   {thumbs_up; threads; locks; accesses; ownership; attribute_map; escapees}
 
+let is_empty {thumbs_up; threads; locks; accesses; ownership; attribute_map; escapees} =
+  thumbs_up && not threads && not locks && AccessDomain.is_empty accesses
+  && OwnershipDomain.is_empty ownership && AttributeMapDomain.is_empty attribute_map
+  && EscapeeDomain.is_empty escapees
+
 let ( <= ) ~lhs ~rhs =
   if phys_equal lhs rhs then true
   else ThreadsDomain.( <= ) ~lhs:lhs.threads ~rhs:rhs.threads

infer/src/checkers/Trace.ml

@@ -237,9 +237,14 @@ module Make (Spec : Spec) = struct
   type path =
     Passthroughs.t * (path_source * Passthroughs.t) list * (path_sink * Passthroughs.t) list
 
-  let pp fmt t =
+  let pp fmt {sources; sinks; passthroughs} =
-    F.fprintf fmt "%a -> %a via %a" Sources.pp t.sources Sinks.pp t.sinks Passthroughs.pp
+    (* empty sources implies empty sinks and passthroughs *)
-      t.passthroughs
+    if not (Passthroughs.is_empty passthroughs) then
+      if not (Sinks.is_empty sinks) then
+        F.fprintf fmt "%a ~> %a via %a" Sources.pp sources Sinks.pp sinks Passthroughs.pp
+          passthroughs
+      else F.fprintf fmt "%a ~> ? via %a" Sources.pp sources Passthroughs.pp passthroughs
+    else F.fprintf fmt "%a ~> ?" Sources.pp sources
 
   let get_path_source_call_site = function
     | Known source

infer/src/checkers/accessPathDomains.ml

@@ -21,6 +21,8 @@ module Set = struct
 
   let empty = APSet.empty
 
+  let is_empty = APSet.is_empty
+
   let normalize aps =
     APSet.filter
       (fun lhs ->

infer/src/checkers/accessTree.ml

@@ -80,10 +80,14 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct
 
   let empty = BaseMap.empty
 
+  let is_empty = BaseMap.is_empty
+
   let make_node trace subtree = (trace, Subtree subtree)
 
   let empty_node = make_node TraceDomain.empty AccessMap.empty
 
+  let is_empty_tree = function Star -> false | Subtree node_map -> AccessMap.is_empty node_map
+
   let make_normal_leaf trace = make_node trace AccessMap.empty
 
   let make_starred_leaf trace = (trace, Star)
@@ -309,13 +313,18 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct
       BaseMap.merge (fun _ prev_node next_node -> node_widen prev_node next_node) prev next
 
   let rec pp_node fmt (trace, subtree) =
-    let pp_subtree fmt = function
+    let pp_subtree fmt tree =
+      match tree with
       | Subtree access_map
        -> AccessMap.pp ~pp_value:pp_node fmt access_map
       | Star
        -> F.fprintf fmt "*"
     in
-    F.fprintf fmt "(%a, %a)" TraceDomain.pp trace pp_subtree subtree
+    if not (TraceDomain.is_empty trace) then
+      if not (is_empty_tree subtree) then
+        F.fprintf fmt "(%a, %a)" TraceDomain.pp trace pp_subtree subtree
+      else F.fprintf fmt "%a" TraceDomain.pp trace
+    else F.fprintf fmt "%a" pp_subtree subtree
 
   let pp fmt base_tree = BaseMap.pp ~pp_value:pp_node fmt base_tree
 end