[quandary] sanity checks for preventing oversized summaries

Summary:
Looked at some problematic summaries and am noticing some common patterns.
Adding some dynamic checks to be run in debug mode in order to make sure my fixes for these patterns are real.

Reviewed By: jeremydubreil

Differential Revision: D5779593

fbshipit-source-id: 9de6497

infer/src/checkers/accessTree.ml

@@ -49,6 +49,10 @@ module type S = sig
 
   val trace_fold : ('a -> AccessPath.Abs.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a
 
+  val exists : (AccessPath.Abs.t -> node -> bool) -> t -> bool
+
+  val iter : (AccessPath.Abs.t -> node -> unit) -> t -> unit
+
   val depth : t -> int
 
   val pp_node : F.formatter -> node -> unit
@@ -368,6 +372,18 @@ module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) = struct
     fold f_
 
 
+  exception Found
+
+  let exists (f: AccessPath.Abs.t -> node -> bool) tree =
+    try
+      fold (fun _ access_path node -> if f access_path node then raise Found else false) tree false
+    with Found -> true
+
+
+  let iter (f: AccessPath.Abs.t -> node -> unit) tree =
+    fold (fun () access_path node -> f access_path node) tree ()
+
+
   (* try for a bit to reach a fixed point before widening aggressively *)
   let joins_before_widen = 3
 
@@ -422,6 +438,10 @@ end
 module PathSet (Config : Config) = struct
   include Make (AbstractDomain.BooleanOr) (Config)
 
+  let mem access_path tree =
+    match get_node access_path tree with None -> false | Some (is_mem, _) -> is_mem
+
+
   (* 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

infer/src/checkers/accessTree.mli

@@ -75,6 +75,10 @@ module type S = sig
 
   val trace_fold : ('a -> AccessPath.Abs.t -> TraceDomain.astate -> 'a) -> t -> 'a -> 'a
 
+  val exists : (AccessPath.Abs.t -> node -> bool) -> t -> bool
+
+  val iter : (AccessPath.Abs.t -> node -> unit) -> t -> unit
+
   val depth : t -> int
   (** number of traces in the tallest branch of the tree *)
 
@@ -93,4 +97,8 @@ module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) :
   S with module TraceDomain = TraceDomain
 
 (** Concise representation of a set of access paths *)
-module PathSet : module type of Make (AbstractDomain.BooleanOr)
+module PathSet (Config : Config) : sig
+  include module type of Make (AbstractDomain.BooleanOr) (Config)
+
+  val mem : AccessPath.Abs.t -> astate -> bool
+end

infer/src/quandary/TaintAnalysis.ml

@@ -693,6 +693,44 @@ module Make (TaintSpecification : TaintSpec.S) = struct
   module Analyzer =
     AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.Make (TransferFunctions) (HilConfig))
 
+  (* sanity checks for summaries. should only be used in developer mode *)
+  let check_invariants access_tree =
+    let open TraceDomain in
+    TaintDomain.iter
+      (fun access_path (trace, _) ->
+        let sources = sources trace in
+        let footprint_sources = sources.footprint in
+        let passthroughs = passthroughs trace in
+        let sinks = sinks trace in
+        (* invariant 1: sinks with no footprint sources are dead and should be forgotten *)
+        if Sources.Footprint.is_empty footprint_sources && not (Sinks.is_empty sinks) then
+          Logging.die InternalError
+            "Trace %a associated with %a tracks sinks even though no more sources can flow into them"
+            Sinks.pp sinks AccessPath.Abs.pp access_path ;
+        (* invariant 2: we should never have sinks without sources *)
+        if Sources.is_empty sources && not (Sinks.is_empty sinks) then
+          Logging.die InternalError "We have sinks %a associated with %a, but no sources" Sinks.pp
+            sinks AccessPath.Abs.pp access_path ;
+        (* invariant 3: we should never have passthroughs without sources *)
+        if Sources.is_empty sources && not (Passthroughs.is_empty passthroughs) then
+          Logging.die InternalError "We have passthroughs %a associated with %a, but no sources"
+            Passthroughs.pp passthroughs AccessPath.Abs.pp access_path ;
+        (* invariant 4: we should never map an access path to a trace consisting only of its
+           corresponding footprint source. a trace like this is a waste of space, since we can
+           lazily create it if/when someone actually tries to read the access path instead *)
+        if AccessPath.Abs.is_exact access_path && Sinks.is_empty sinks
+           && Sources.Footprint.mem access_path footprint_sources
+           && Sources.Footprint.exists
+                (fun footprint_access_path (is_mem, _) ->
+                  is_mem && AccessPath.Abs.equal access_path footprint_access_path)
+                footprint_sources
+        then
+          Logging.die InternalError
+            "The trace associated with %a consists only of its footprint source: %a"
+            AccessPath.Abs.pp access_path pp trace)
+      access_tree
+
+
   let make_summary {ProcData.pdesc; extras= {formal_map}} access_tree =
     let is_java = Typ.Procname.is_java (Procdesc.get_proc_name pdesc) in
     (* if a trace has footprint sources, attach them to the appropriate footprint var *)
@@ -764,6 +802,9 @@ module Make (TaintSpecification : TaintSpec.S) = struct
                 acc)
         access_tree' TaintDomain.empty
     in
+    if Config.developer_mode && false
+       (* TODO: temporarily disabled to avoid crashes until we clean up all violations *)
+    then check_invariants with_footprint_vars ;
     TaintSpecification.to_summary_access_tree with_footprint_vars