diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index 675b6ab73..04de277fc 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/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 = ( || ) diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index a1793af12..eb3f079a6 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/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 *) diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 22a27aef6..e41889947 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/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 diff --git a/infer/src/checkers/Trace.ml b/infer/src/checkers/Trace.ml index c21954329..23e03834d 100644 --- a/infer/src/checkers/Trace.ml +++ b/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 = - F.fprintf fmt "%a -> %a via %a" Sources.pp t.sources Sinks.pp t.sinks Passthroughs.pp - t.passthroughs + let pp fmt {sources; sinks; passthroughs} = + (* empty sources implies empty sinks and 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 diff --git a/infer/src/checkers/accessPathDomains.ml b/infer/src/checkers/accessPathDomains.ml index c2af61a4e..683e786c2 100644 --- a/infer/src/checkers/accessPathDomains.ml +++ b/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 -> diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml index da7e44ea8..aee840962 100644 --- a/infer/src/checkers/accessTree.ml +++ b/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