[absint] don't require domains to define their initial state

Summary:
A domain should not definite its initial state, since distinct users of the domain may want to choose different initial values.
For example, one user might want to bind all of the formals to some special values, and one user might want the initial domain to be an empty map
This diff makes this distinction clear in the types by (a) requiring the initial state to be passed to the abstract interpreter and (b) lifting the requirement that abstract domains define `initial`.

Reviewed By: jberdine

Differential Revision: D4359629

fbshipit-source-id: cbcee28

infer/src/backend/preanal.ml

@@ -198,13 +198,15 @@ let add_nullify_instrs pdesc tenv liveness_inv_map =
     if Procname.is_java (Procdesc.get_proc_name pdesc)
     then AddressTaken.Domain.empty (* can't take the address of a variable in Java *)
     else
-      match AddressTaken.Analyzer.compute_post (ProcData.make_default pdesc tenv) with
+      let initial = AddressTaken.Domain.empty in
+      match AddressTaken.Analyzer.compute_post (ProcData.make_default pdesc tenv) ~initial with
       | Some post -> post
       | None -> AddressTaken.Domain.empty in
 
   let nullify_proc_cfg = ProcCfg.Exceptional.from_pdesc pdesc in
   let nullify_proc_data = ProcData.make pdesc tenv liveness_inv_map in
-  let nullify_inv_map = NullifyAnalysis.exec_cfg nullify_proc_cfg nullify_proc_data in
+  let initial = VarDomain.empty, VarDomain.empty in
+  let nullify_inv_map = NullifyAnalysis.exec_cfg nullify_proc_cfg nullify_proc_data ~initial in
 
   (* only nullify pvars that are local; don't nullify those that can escape *)
   let is_local pvar =
@@ -258,7 +260,8 @@ module CopyProp =
 
 let do_copy_propagation pdesc tenv =
   let proc_cfg = ExceptionalOneInstrPerNodeCfg.from_pdesc pdesc in
-  let copy_prop_inv_map = CopyProp.exec_cfg proc_cfg (ProcData.make_default pdesc tenv) in
+  let initial = CopyPropagation.Domain.empty in
+  let copy_prop_inv_map = CopyProp.exec_cfg proc_cfg (ProcData.make_default pdesc tenv) ~initial in
   (* [var_map] represents a chain of variable. copies v_0 -> v_1 ... -> v_n. starting from some
      ident v_j, we want to walk backward through the chain to find the lowest v_i that is also an
      ident. *)
@@ -302,8 +305,9 @@ let do_copy_propagation pdesc tenv =
 
 let do_liveness pdesc tenv =
   let liveness_proc_cfg = BackwardCfg.from_pdesc pdesc in
+  let initial = Liveness.Domain.empty in
   let liveness_inv_map =
-    LivenessAnalysis.exec_cfg liveness_proc_cfg (ProcData.make_default pdesc tenv) in
+    LivenessAnalysis.exec_cfg liveness_proc_cfg (ProcData.make_default pdesc tenv) ~initial in
   if Config.copy_propagation then do_copy_propagation pdesc tenv;
   add_nullify_instrs pdesc tenv liveness_inv_map;
   Procdesc.signal_did_preanalysis pdesc

infer/src/checkers/AbstractDomain.ml

@@ -14,19 +14,24 @@ module F = Format
 module type S = sig
   type astate
 
-  val initial : astate
   val (<=) : lhs:astate -> rhs:astate -> bool (* fst \sqsubseteq snd? *)
   val join : astate -> astate -> astate
   val widen : prev:astate -> next:astate -> num_iters:int -> astate
   val pp : F.formatter -> astate -> unit
 end
 
+module type WithBottom = sig
+  include S
+
+  val empty : astate
+end
+
 module BottomLifted (Domain : S) = struct
   type astate =
     | Bottom
     | NonBottom of Domain.astate
 
-  let initial = Bottom
+  let empty = Bottom
 
   let (<=) ~lhs ~rhs =
     if phys_equal lhs rhs
@@ -63,8 +68,6 @@ end
 module Pair (Domain1 : S) (Domain2 : S) = struct
   type astate = Domain1.astate * Domain2.astate
 
-  let initial = Domain1.initial, Domain2.initial
-
   let (<=) ~lhs ~rhs =
     if phys_equal lhs rhs
     then true
@@ -91,8 +94,6 @@ module FiniteSet (S : PrettyPrintable.PPSet) = struct
   include S
   type astate = t
 
-  let initial = empty
-
   let (<=) ~lhs ~rhs =
     if phys_equal lhs rhs
     then true
@@ -111,8 +112,6 @@ module InvertedSet (S : PrettyPrintable.PPSet) = struct
   include S
   type astate = t
 
-  let initial = empty
-
   let (<=) ~lhs ~rhs =
     if phys_equal lhs rhs
     then true
@@ -131,8 +130,6 @@ module Map (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct
   include M
   type astate = ValueDomain.astate M.t
 
-  let initial = M.empty
-
   (** true if all keys in [lhs] are in [rhs], and each lhs value <= corresponding rhs value *)
   let (<=) ~lhs ~rhs =
     if phys_equal lhs rhs
@@ -175,8 +172,6 @@ end
 module BooleanAnd = struct
   type astate = bool
 
-  let initial = false
-
   let (<=) ~lhs ~rhs = lhs || not rhs
 
   let join = (&&)

infer/src/checkers/AbstractDomain.mli

@@ -16,13 +16,24 @@ module F = Format
 module type S = sig
   type astate
 
-  val initial : astate
-  val (<=) : lhs:astate -> rhs:astate -> bool (* fst \sqsubseteq snd? *)
+  (** the partial order induced by join *)
+  val (<=) : lhs:astate -> rhs:astate -> bool
+
   val join : astate -> astate -> astate
+
   val widen : prev:astate -> next:astate -> num_iters:int -> astate
+
   val pp : F.formatter -> astate -> unit
 end
 
+(** A domain with an explicit bottom value *)
+module type WithBottom = sig
+  include S
+
+  (** The bottom value of the domain. *)
+  val empty : astate
+end
+
 (** Lift a pre-domain to a domain *)
 module BottomLifted (Domain : S) : sig
   type astate =
@@ -39,7 +50,7 @@ module Pair (Domain1 : S) (Domain2 : S) : S with type astate = Domain1.astate *
     a *finite* collection of possible values, since the widening operator here is just union. *)
 module FiniteSet (Set : PrettyPrintable.PPSet) : sig
   include PrettyPrintable.PPSet with type t = Set.t and type elt = Set.elt
-  include S with type astate = t
+  include WithBottom with type astate = t
 end
 
 (** Lift a set to a powerset domain ordered by superset, so the join operator is intersection *)
@@ -51,7 +62,7 @@ end
 (** Lift a map whose value type is an abstract domain to a domain. *)
 module Map (Map : PrettyPrintable.PPMap) (ValueDomain : S) : sig
   include PrettyPrintable.PPMap with type 'a t = 'a Map.t and type key = Map.key
-  include S with type astate = ValueDomain.astate Map.t
+  include WithBottom with type astate = ValueDomain.astate Map.t
 end
 
 (** Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's

infer/src/checkers/AbstractInterpreter.ml

@@ -20,11 +20,19 @@ module type S = sig
 
   type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t
 
-  val compute_post : TransferFunctions.extras ProcData.t -> TransferFunctions.Domain.astate option
+  val compute_post :
+    TransferFunctions.extras ProcData.t ->
+    initial:TransferFunctions.Domain.astate ->
+    TransferFunctions.Domain.astate option
 
-  val exec_cfg : TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t -> invariant_map
+  val exec_cfg :
+    TransferFunctions.CFG.t ->
+    TransferFunctions.extras ProcData.t ->
+    initial:TransferFunctions.Domain.astate ->
+    invariant_map
 
-  val exec_pdesc : TransferFunctions.extras ProcData.t -> invariant_map
+  val exec_pdesc :
+    TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map
 
   val extract_post : InvariantMap.key -> 'a state InvariantMap.t -> 'a option
 
@@ -113,10 +121,10 @@ module MakeNoCFG
         inv_map
 
   (* compute and return an invariant map for [cfg] *)
-  let exec_cfg cfg proc_data =
+  let exec_cfg cfg proc_data ~initial =
     let start_node = CFG.start_node cfg in
     let inv_map', work_queue' =
-      exec_node start_node Domain.initial (Scheduler.empty cfg) InvariantMap.empty proc_data in
+      exec_node start_node initial (Scheduler.empty cfg) InvariantMap.empty proc_data in
     exec_worklist cfg work_queue' inv_map' proc_data
 
   (* compute and return an invariant map for [pdesc] *)
@@ -124,9 +132,9 @@ module MakeNoCFG
     exec_cfg (CFG.from_pdesc pdesc) proc_data
 
   (* compute and return the postcondition of [pdesc] *)
-  let compute_post ({ ProcData.pdesc; } as proc_data) =
+  let compute_post ({ ProcData.pdesc; } as proc_data) ~initial =
     let cfg = CFG.from_pdesc pdesc in
-    let inv_map = exec_cfg cfg proc_data in
+    let inv_map = exec_cfg cfg proc_data ~initial in
     extract_post (CFG.id (CFG.exit_node cfg)) inv_map
 
 end

infer/src/checkers/AbstractInterpreter.mli

@@ -20,14 +20,22 @@ module type S = sig
   (** invariant map from node id -> state representing postcondition for node id *)
   type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t
 
-  (** compute and return the postcondition for the given procedure *)
-  val compute_post : TransferFunctions.extras ProcData.t -> TransferFunctions.Domain.astate option
+  (** compute and return the postcondition for the given procedure starting from [initial] *)
+  val compute_post :
+    TransferFunctions.extras ProcData.t ->
+    initial:TransferFunctions.Domain.astate ->
+    TransferFunctions.Domain.astate option
 
-  (** compute and return invariant map for the given CFG/procedure. *)
-  val exec_cfg : TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t -> invariant_map
+  (** compute and return invariant map for the given CFG/procedure starting from [initial] *)
+  val exec_cfg :
+    TransferFunctions.CFG.t ->
+    TransferFunctions.extras ProcData.t ->
+    initial:TransferFunctions.Domain.astate ->
+    invariant_map
 
-  (** compute and return invariant map for the given procedure. *)
-  val exec_pdesc : TransferFunctions.extras ProcData.t -> invariant_map
+  (** compute and return invariant map for the given procedure starting from [initial] *)
+  val exec_pdesc :
+    TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map
 
   (** extract the postcondition for a node id from the given invariant map *)
   val extract_post : InvariantMap.key -> 'a state InvariantMap.t -> 'a option

infer/src/checkers/BoundedCallTree.ml

@@ -186,5 +186,5 @@ let checker { Callbacks.proc_desc; tenv; get_proc_desc; } =
       SpecSummary.write_summary
         (Procdesc.get_proc_name proc_desc)
         (Some (stacktree_of_pdesc proc_desc "proc_start"));
-      ignore(Analyzer.exec_pdesc (ProcData.make proc_desc tenv extras))
+      ignore(Analyzer.exec_pdesc (ProcData.make proc_desc tenv extras) ~initial:Domain.empty)
     end

infer/src/checkers/IdAccessPathMapDomain.ml

@@ -18,8 +18,6 @@ include IdMap
 let pp fmt astate =
   IdMap.pp ~pp_value:AccessPath.pp_raw fmt astate
 
-let initial = IdMap.empty
-
 let (<=) ~lhs ~rhs =
   if phys_equal lhs rhs
   then true

infer/src/checkers/IdAccessPathMapDomain.mli

@@ -17,4 +17,4 @@ type astate = AccessPath.raw IdMap.t
 
 include (module type of IdMap)
 
-include AbstractDomain.S with type astate := astate
+include AbstractDomain.WithBottom with type astate := astate

infer/src/checkers/SimpleChecker.ml

@@ -54,8 +54,6 @@ module Make (Spec : Spec) : S = struct
           end)
         )
 
-    let initial = singleton Spec.initial
-
     let widen ~prev ~next ~num_iters =
       let iters_befor_timeout = 1000 in
       (* failsafe for accidental non-finite height domains *)
@@ -103,6 +101,7 @@ module Make (Spec : Spec) : S = struct
           (fun astate ->
              Spec.report astate (ProcCfg.Exceptional.loc node) proc_name)
           astate_set in
-    let inv_map = Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv) in
+    let inv_map =
+      Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv) ~initial:Domain.empty in
     Analyzer.InvariantMap.iter do_reporting inv_map
 end

infer/src/checkers/SinkTrace.ml

@@ -46,7 +46,7 @@ module Make (TraceElem : TraceElem.S) = struct
 
   type sink_path = Passthroughs.t * (Sink.t * Passthroughs.t) list
 
-  let initial =
+  let empty =
     let dummy_source = () in
     of_source dummy_source
 
@@ -63,7 +63,7 @@ module Make (TraceElem : TraceElem.S) = struct
       (fun t_acc sink ->
          let callee_sink = Sink.with_callsite sink call_site in
          add_sink callee_sink t_acc)
-      initial
+      empty
       (Sinks.elements (sinks t))
 
   let pp fmt t =

infer/src/checkers/Siof.ml

@@ -56,7 +56,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       astate
     else
       let trace = match astate with
-        | Domain.Bottom -> SiofTrace.initial
+        | Domain.Bottom -> SiofTrace.empty
         | Domain.NonBottom t -> t in
       let globals_trace =
         SiofTrace.add_sink (SiofTrace.make_access globals outer_loc) trace in
@@ -68,7 +68,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     |> add_globals astate (Procdesc.get_loc pdesc)
 
   let at_least_nonbottom =
-    Domain.join (Domain.NonBottom SiofTrace.initial)
+    Domain.join (Domain.NonBottom SiofTrace.empty)
 
   let exec_instr astate { ProcData.pdesc; } _ (instr : Sil.instr) =
     match instr with
@@ -127,7 +127,7 @@ let report_siof trace pdesc gname loc =
   let trace_of_pname pname =
     match Summary.read_summary pdesc pname with
     | Some (SiofDomain.NonBottom summary) -> summary
-    | _ -> SiofTrace.initial in
+    | _ -> SiofTrace.empty in
 
   let report_one_path (passthroughs, path) =
     let description, sink_path' = match path with
@@ -176,7 +176,7 @@ let siof_check pdesc gname = function
       ()
 
 let compute_post proc_data =
-  Analyzer.compute_post proc_data |> Option.map ~f:SiofDomain.normalize
+  Analyzer.compute_post proc_data ~initial:SiofDomain.Bottom |> Option.map ~f:SiofDomain.normalize
 
 let checker ({ Callbacks.proc_desc; } as callback) =
   let post =

infer/src/checkers/ThreadSafety.ml

@@ -268,7 +268,7 @@ let make_results_table get_proc_desc file_env =
       (* convert the abstract state to a summary by dropping the id map *)
       let compute_post ({ ProcData.pdesc; tenv; } as proc_data) =
         if not (Procdesc.did_preanalysis pdesc) then Preanal.do_liveness pdesc tenv;
-        match Analyzer.compute_post proc_data with
+        match Analyzer.compute_post proc_data ~initial:ThreadSafetyDomain.empty with
         | Some { locks; reads; writes; } -> Some (locks, reads, writes)
         | None -> None in
       let callback_arg =
@@ -281,9 +281,7 @@ let make_results_table get_proc_desc file_env =
           callback_arg with
       | Some post -> post
       | None ->
-          ThreadSafetyDomain.LocksDomain.initial,
-          ThreadSafetyDomain.PathDomain.initial,
-          ThreadSafetyDomain.PathDomain.initial
+          false, ThreadSafetyDomain.PathDomain.empty, ThreadSafetyDomain.PathDomain.empty
   in
   map_post_computation_over_procs compute_post_for_procedure file_env
 
@@ -314,7 +312,7 @@ let report_thread_safety_violations ( _, tenv, pname, pdesc) trace =
   let trace_of_pname callee_pname =
     match Summary.read_summary pdesc callee_pname with
     | Some (_, _, writes) -> writes
-    | _ -> PathDomain.initial in
+    | _ -> PathDomain.empty in
   let report_one_path ((_, sinks) as path) =
     let pp_accesses fmt sink =
       let _, accesses = PathDomain.Sink.kind sink in

infer/src/checkers/ThreadSafetyDomain.ml

@@ -76,12 +76,12 @@ type astate =
 (** same as astate, but without [id_map] (since it's local) *)
 type summary = LocksDomain.astate * PathDomain.astate * PathDomain.astate
 
-let initial =
-  let locks = LocksDomain.initial in
-  let reads = PathDomain.initial in
-  let writes = PathDomain.initial in
-  let id_map = IdAccessPathMapDomain.initial in
-  let owned = OwnershipDomain.initial in
+let empty =
+  let locks = false in
+  let reads = PathDomain.empty in
+  let writes = PathDomain.empty in
+  let id_map = IdAccessPathMapDomain.empty in
+  let owned = OwnershipDomain.empty in
   { locks; reads; writes; id_map; owned; }
 
 let (<=) ~lhs ~rhs =

infer/src/checkers/Trace.ml

@@ -24,7 +24,7 @@ module type S = sig
   include Spec
   type t
   type astate = t
-  include AbstractDomain.S with type astate := astate
+  include AbstractDomain.WithBottom with type astate := astate
 
   module Sources = Source.Set
   module Sinks = Sink.Set
@@ -35,6 +35,8 @@ module type S = sig
       both the source and sink stack *)
   type path = Passthroughs.t * (Source.t * Passthroughs.t) list * (Sink.t * Passthroughs.t) list
 
+  val empty : t
+
   (** get the sources of the trace. *)
   val sources : t -> Sources.t
 
@@ -377,7 +379,7 @@ module Make (Spec : Spec) = struct
 
       { sources; sinks; passthroughs; }
 
-  let initial =
+  let empty =
     let sources = Sources.empty in
     let sinks = Sinks.empty in
     let passthroughs = Passthroughs.empty in

infer/src/checkers/Trace.mli

@@ -24,7 +24,7 @@ module type S = sig
   include Spec
   type t
   type astate = t
-  include AbstractDomain.S with type astate := astate
+  include AbstractDomain.WithBottom with type astate := astate
 
   module Sources = Source.Set
   module Sinks = Sink.Set
@@ -35,6 +35,9 @@ module type S = sig
       both the source and sink stack *)
   type path = Passthroughs.t * (Source.t * Passthroughs.t) list * (Sink.t * Passthroughs.t) list
 
+  (** the empty trace *)
+  val empty : t
+
   (** get the sources of the trace. *)
   val sources : t -> Sources.t
 

infer/src/checkers/accessPathDomains.ml

@@ -22,10 +22,10 @@ module Set = struct
       bool recording whether an abstracted access path has been introduced *)
   type astate = APSet.t
 
-  let initial = APSet.empty
-
   let pp = APSet.pp
 
+  let empty = APSet.empty
+
   let normalize aps =
     APSet.filter
       (fun lhs ->
@@ -65,6 +65,6 @@ module Set = struct
         | AccessPath.Exact exact_ap -> APSet.add (AccessPath.Abstracted exact_ap) aps
         | AccessPath.Abstracted _ -> APSet.add ap aps in
       let diff_aps = APSet.diff next prev in
-      APSet.fold abstract_access_path diff_aps initial
+      APSet.fold abstract_access_path diff_aps APSet.empty
       |> join prev
 end

infer/src/checkers/accessPathDomains.mli

@@ -17,7 +17,7 @@ open! IStd
     call to [normalize]. however, [normalize] is quadratic in the size of the set, so it should be
     used sparingly (recommendation: only before computing a summary based on the access path set) *)
 module Set : sig
-  include AbstractDomain.S
+  include AbstractDomain.WithBottom
 
   val of_list : AccessPath.t list -> astate
 

infer/src/checkers/accessTree.ml

@@ -13,7 +13,7 @@ module F = Format
 module L = Logging
 
 module type S = sig
-  module TraceDomain : AbstractDomain.S
+  module TraceDomain : AbstractDomain.WithBottom
   module AccessMap = AccessPath.AccessMap
   module BaseMap = AccessPath.BaseMap
 
@@ -24,9 +24,7 @@ module type S = sig
 
   type t = node BaseMap.t
 
-  include AbstractDomain.S with type astate = t
-
-  val empty : t
+  include AbstractDomain.WithBottom with type astate = t
 
   val empty_node : node
 
@@ -51,7 +49,7 @@ module type S = sig
   val pp_node : F.formatter -> node -> unit
 end
 
-module Make (TraceDomain : AbstractDomain.S) = struct
+module Make (TraceDomain : AbstractDomain.WithBottom) = struct
   module TraceDomain = TraceDomain
   module AccessMap = AccessPath.AccessMap
   module BaseMap = AccessPath.BaseMap
@@ -66,13 +64,11 @@ module Make (TraceDomain : AbstractDomain.S) = struct
 
   let empty = BaseMap.empty
 
-  let initial = empty
-
   let make_node trace subtree =
     trace, Subtree subtree
 
   let empty_node =
-    make_node TraceDomain.initial AccessMap.empty
+    make_node TraceDomain.empty AccessMap.empty
 
   let make_normal_leaf trace =
     make_node trace AccessMap.empty
@@ -217,7 +213,7 @@ module Make (TraceDomain : AbstractDomain.S) = struct
       | access :: accesses, (trace, Subtree subtree) ->
           let access_node =
             try AccessMap.find access subtree
-            with Not_found -> make_normal_leaf TraceDomain.initial in
+            with Not_found -> make_normal_leaf TraceDomain.empty in
           (* once we encounter a subtree rooted in an array access, we have to do weak updates in
              the entire subtree. the reason: if I do x[i].f.g = <interesting trace>, then
              x[j].f.g = <empty trace>, I don't want to overwrite <interesting trace>. instead, I
@@ -234,7 +230,7 @@ module Make (TraceDomain : AbstractDomain.S) = struct
     let is_exact = AccessPath.is_exact ap in
     let base_node =
       try BaseMap.find base tree
-      with Not_found -> make_normal_leaf TraceDomain.initial in
+      with Not_found -> make_normal_leaf TraceDomain.empty in
     let base_node' =
       access_tree_add_trace ~node_to_add ~seen_array_access:false ~is_exact accesses base_node in
     BaseMap.add base base_node' tree

infer/src/checkers/accessTree.mli

@@ -9,7 +9,7 @@
 
 (** tree of (trace, access path) associations organized by structure of access paths *)
 module type S = sig
-  module TraceDomain : AbstractDomain.S
+  module TraceDomain : AbstractDomain.WithBottom
   module AccessMap = AccessPath.AccessMap
   module BaseMap = AccessPath.BaseMap
 
@@ -30,9 +30,7 @@ module type S = sig
   *)
   type t = node BaseMap.t
 
-  include AbstractDomain.S with type astate = t
-
-  val empty : t
+  include AbstractDomain.WithBottom with type astate = t
 
   val empty_node : node
 
@@ -69,4 +67,4 @@ module type S = sig
   val pp_node : Format.formatter -> node -> unit
 end
 
-module Make (TraceDomain : AbstractDomain.S) : S with module TraceDomain = TraceDomain
+module Make (TraceDomain : AbstractDomain.WithBottom) : S with module TraceDomain = TraceDomain

infer/src/checkers/annotationReachability.ml

@@ -37,15 +37,6 @@ module Domain = struct
   module TrackingDomain = AbstractDomain.Pair (CallsDomain) (TrackingVar)
   include AbstractDomain.BottomLifted (TrackingDomain)
 
-  let initial =
-    let init_map =
-      IList.fold_left
-        (fun astate_acc (_, snk_annot) -> CallsDomain.add snk_annot CallSiteSet.empty astate_acc)
-        CallsDomain.initial
-        (src_snk_pairs ()) in
-    NonBottom
-      (init_map, TrackingVar.empty)
-
   let add_call key call = function
     | Bottom -> Bottom
     | NonBottom (call_map, vars) as astate ->
@@ -403,8 +394,16 @@ module Interprocedural = struct
       if not (IList.length calls = 0)
       then IList.iter (report_src_snk_path calls) src_annot_list in
 
+    let initial =
+      let init_map =
+        IList.fold_left
+          (fun astate_acc (_, snk_annot) -> CallsDomain.add snk_annot CallSiteSet.empty astate_acc)
+          CallsDomain.empty
+          (src_snk_pairs ()) in
+      Domain.NonBottom
+        (init_map, Domain.TrackingVar.empty) in
     match compute_and_store_post
-            ~compute_post:Analyzer.compute_post
+            ~compute_post:(Analyzer.compute_post ~initial)
             ~make_extras:ProcData.make_empty_extras
             proc_data with
     | Some Domain.NonBottom (call_map, _) ->

infer/src/checkers/copyPropagation.ml

@@ -16,8 +16,6 @@ module Domain = struct
   include Var.Map
   type astate = Var.t Var.Map.t
 
-  let initial = Var.Map.empty
-
   (* return true if the key-value bindings in [rhs] are a subset of the key-value bindings in
      [lhs] *)
   let (<=) ~lhs ~rhs =

infer/src/checkers/liveness.ml

@@ -59,6 +59,3 @@ module Analyzer =
     (ProcCfg.Backward(ProcCfg.Exceptional))
     (Scheduler.ReversePostorder)
     (TransferFunctions)
-
-let checker { Callbacks.proc_desc; tenv; } =
-  ignore(Analyzer.exec_pdesc (ProcData.make_default proc_desc tenv))

infer/src/quandary/TaintAnalysis.ml

@@ -30,7 +30,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
 
       let read_from_payload payload =
         match payload.Specs.quandary with
-        | None -> Some (TaintSpecification.to_summary_access_tree TaintDomain.initial)
+        | None -> Some (TaintSpecification.to_summary_access_tree TaintDomain.empty)
         | summary_opt -> summary_opt
     end)
 
@@ -41,9 +41,9 @@ module Make (TaintSpecification : TaintSpec.S) = struct
         id_map : IdMapDomain.astate; (* mapping of id's to access paths for normalization *)
       }
 
-    let initial =
-      let access_tree = TaintDomain.initial in
-      let id_map = IdMapDomain.initial in
+    let empty =
+      let access_tree = TaintDomain.empty in
+      let id_map = IdMapDomain.empty in
       { access_tree; id_map; }
 
     let (<=) ~lhs ~rhs =
@@ -126,7 +126,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
     let access_path_get_trace access_path access_tree proc_data loc =
       match access_path_get_node access_path access_tree proc_data loc with
       | Some (trace, _) -> trace
-      | None -> TraceDomain.initial
+      | None -> TraceDomain.empty
 
     (* get the node associated with [exp] in [access_tree] *)
     let exp_get_node ?(abstracted=false) exp typ { Domain.access_tree; id_map; } proc_data loc =
@@ -172,9 +172,9 @@ module Make (TaintSpecification : TaintSpec.S) = struct
             TaintDomain.fold
               (fun acc _ trace -> TraceDomain.join trace acc)
               (TaintSpecification.of_summary_access_tree summary)
-              TraceDomain.initial
+              TraceDomain.empty
         | None ->
-            TraceDomain.initial in
+            TraceDomain.empty in
 
       let pp_path_short fmt (_, sources_passthroughs, sinks_passthroughs) =
         let original_source = fst (IList.hd sources_passthroughs) in
@@ -394,7 +394,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
               | None -> trace_acc in
             let propagate_to_access_path access_path actuals (astate : Domain.astate) =
               let trace_with_propagation =
-                IList.fold_left exp_join_traces TraceDomain.initial actuals in
+                IList.fold_left exp_join_traces TraceDomain.empty actuals in
               let access_tree =
                 TaintDomain.add_trace access_path trace_with_propagation astate.access_tree in
               { astate with access_tree; } in
@@ -473,7 +473,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
                 [called_pname]
               end in
           (* for each possible target of the call, apply the summary. join all results together *)
-          IList.fold_left analyze_call Domain.initial targets
+          IList.fold_left analyze_call Domain.empty targets
       | Sil.Call _ ->
           failwith "Unimp: non-pname call expressions"
       | Sil.Nullify (pvar, _) ->
@@ -507,7 +507,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
                base in
            AccessPath.BaseMap.add base' node acc)
         access_tree
-        TaintDomain.initial in
+        TaintDomain.empty in
 
     TaintSpecification.to_summary_access_tree access_tree'
 
@@ -522,7 +522,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
           Preanal.do_liveness proc_data.pdesc proc_data.tenv;
           Preanal.do_dynamic_dispatch proc_data.pdesc (Cg.create None) proc_data.tenv;
         end;
-      match Analyzer.compute_post proc_data with
+      match Analyzer.compute_post proc_data ~initial:Domain.empty with
       | Some { access_tree; } ->
           Some (make_summary proc_data.extras access_tree)
       | None ->

infer/src/unit/BoundedCallTreeTests.ml

@@ -21,6 +21,7 @@ let mock_get_proc_desc _ = None
 let tests =
   let open OUnit2 in
   let open AnalyzerTester.StructuredSil in
+  let initial = BoundedCallTree.Domain.empty in
   let f_proc_name = Procname.from_string_c_fun "f" in
   let g_proc_name = Procname.from_string_c_fun "g" in
   let g_args = [((Exp.Const (Const.Cint (IntLit.one))), (Typ.Tint IInt))] in
@@ -66,37 +67,38 @@ let tests =
       make_call ~procname:f_proc_name None [];
       invariant "{ f }"
     ];
-  ] |> TestInterpreter.create_tests ~test_pname:caller_foo_name extras in
+  ] |> TestInterpreter.create_tests
+      ~test_pname:caller_foo_name
+      ~initial:BoundedCallTree.Domain.empty
+      extras in
   let test_list_from_bar = [
     "on_call_anywhere_on_stack_add_proc_name",
     [
       make_call ~procname:f_proc_name None []; (* means f() *)
       invariant "{ f }"
     ];
-  ] |> TestInterpreter.create_tests ~test_pname:caller_bar_name extras in
+  ] |> TestInterpreter.create_tests ~test_pname:caller_bar_name extras ~initial in
   let test_list_from_baz = [
     "ignore_procs_unrelated_to_trace",
     [
       make_call ~procname:f_proc_name None []; (* means f() *)
       invariant "{  }"
     ];
-  ] |> TestInterpreter.create_tests ~test_pname:caller_baz_name extras in
+  ] |> TestInterpreter.create_tests ~test_pname:caller_baz_name extras ~initial in
   let test_list_multiple_traces_from_foo = [
     "on_call_add_proc_name_in_any_stack_1",
     [
       make_call ~procname:f_proc_name None []; (* means f() *)
       invariant "{ f }"
     ];
-  ] |> TestInterpreter.create_tests
-      ~test_pname:caller_foo_name multi_trace_extras in
+  ] |> TestInterpreter.create_tests ~test_pname:caller_foo_name multi_trace_extras ~initial in
   let test_list_multiple_traces_from_bar = [
     "on_call_add_proc_name_in_any_stack_2",
     [
       make_call ~procname:f_proc_name None []; (* means f() *)
       invariant "{ f }"
     ];
-  ] |> TestInterpreter.create_tests
-      ~test_pname:caller_bar_name multi_trace_extras in
+  ] |> TestInterpreter.create_tests ~test_pname:caller_bar_name multi_trace_extras ~initial in
   let test_list = test_list_from_foo @
                   test_list_from_bar @
                   test_list_from_baz @

infer/src/unit/TaintTests.ml

@@ -255,5 +255,8 @@ let tests =
       invariant "{ ret_id$0 => (SOURCE -> SINK) }";
     ];
 
-  ] |> TestInterpreter.create_tests ~pp_opt:pp_sparse AccessPath.BaseMap.empty in
+  ] |> TestInterpreter.create_tests
+      ~pp_opt:pp_sparse
+      AccessPath.BaseMap.empty
+      ~initial:MockTaintAnalysis.Domain.empty in
   "taint_test_suite">:::test_list

infer/src/unit/abstractInterpreterTests.ml

@@ -69,6 +69,7 @@ module ExceptionalTestInterpreter = AnalyzerTester.Make
 let tests =
   let open OUnit2 in
   let open AnalyzerTester.StructuredSil in
+  let initial = PathCountDomain.initial in
   let normal_test_list = [
     "straightline",
     [
@@ -180,7 +181,7 @@ let tests =
       );
       invariant "1"
     ];
-  ] |> NormalTestInterpreter.create_tests ProcData.empty_extras in
+  ] |> NormalTestInterpreter.create_tests ProcData.empty_extras ~initial in
   let exceptional_test_list = [
     "try1",
     [
@@ -216,5 +217,5 @@ let tests =
       );
       invariant "3"
     ];
-  ] |> ExceptionalTestInterpreter.create_tests ProcData.empty_extras in
+  ] |> ExceptionalTestInterpreter.create_tests ProcData.empty_extras ~initial in
   "analyzer_tests_suite">:::(normal_test_list @ exceptional_test_list)

infer/src/unit/accessTreeTests.ml

@@ -406,7 +406,7 @@ let tests =
       let x_y_star_base_tree =
         Domain.BaseMap.add
           y_base
-          (Domain.make_starred_leaf MockTraceDomain.initial)
+          (Domain.make_starred_leaf MockTraceDomain.empty)
           x_base_tree in
       assert_trees_equal (widen x_base_tree y_base_tree) x_y_star_base_tree;
 

infer/src/unit/addressTakenTests.ml

@@ -98,5 +98,5 @@ let tests =
       var_assign_addrof_var ~rhs_typ:int_ptr_typ "e" "f";
       invariant "{ &b, &d, &f }"
     ];
-  ] |> TestInterpreter.create_tests ProcData.empty_extras in
+  ] |> TestInterpreter.create_tests ProcData.empty_extras ~initial:AddressTaken.Domain.empty in
   "address_taken_suite">:::test_list

infer/src/unit/analyzerTester.ml

@@ -245,10 +245,10 @@ module Make
     Procdesc.set_exit_node pdesc exit_node;
     pdesc, assert_map
 
-  let create_test test_program extras pp_opt test_pname _ =
+  let create_test test_program extras pp_opt ~initial test_pname _ =
     let pp_state = Option.value ~default:I.TransferFunctions.Domain.pp pp_opt in
     let pdesc, assert_map = structured_program_to_cfg test_program test_pname in
-    let inv_map = I.exec_pdesc (ProcData.make pdesc (Tenv.create ()) extras) in
+    let inv_map = I.exec_pdesc (ProcData.make pdesc (Tenv.create ()) extras) ~initial in
 
     let collect_invariant_mismatches node_id (inv_str, inv_label) error_msgs_acc =
       let post_str =
@@ -279,9 +279,9 @@ module Make
           |> F.flush_str_formatter in
         OUnit2.assert_failure assert_fail_message
 
-  let create_tests ?(test_pname=Procname.empty_block) ?pp_opt extras tests =
+  let create_tests ?(test_pname=Procname.empty_block) ~initial ?pp_opt extras tests =
     let open OUnit2 in
     IList.map (fun (name, test_program) ->
-        name>::create_test test_program extras pp_opt test_pname) tests
+        name>::create_test test_program extras ~initial pp_opt test_pname) tests
 
 end

infer/src/unit/copyPropagationTests.ml

@@ -162,5 +162,5 @@ let tests =
       var_assign_id "c" "b";
       invariant "{ &b -> a$0, &c -> b$0 }"
     ];
-  ] |> TestInterpreter.create_tests ProcData.empty_extras in
+  ] |> TestInterpreter.create_tests ProcData.empty_extras ~initial:CopyPropagation.Domain.empty in
   "copy_propagation_test_suite">:::test_list

infer/src/unit/livenessTests.ml

@@ -191,5 +191,5 @@ let tests =
       invariant "{ &b }";
       id_assign_var "a" "b"
     ];
-  ] |> TestInterpreter.create_tests ProcData.empty_extras in
+  ] |> TestInterpreter.create_tests ProcData.empty_extras ~initial:Liveness.Domain.empty in
   "liveness_test_suite">:::test_list