From 8d0f6e822c01adeba546c771d1bafb1b66786d8f Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 3 Jan 2017 10:03:07 -0800 Subject: [PATCH] [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 | 12 +++++++---- infer/src/checkers/AbstractDomain.ml | 19 +++++++---------- infer/src/checkers/AbstractDomain.mli | 19 +++++++++++++---- infer/src/checkers/AbstractInterpreter.ml | 22 +++++++++++++------- infer/src/checkers/AbstractInterpreter.mli | 20 ++++++++++++------ infer/src/checkers/BoundedCallTree.ml | 2 +- infer/src/checkers/IdAccessPathMapDomain.ml | 2 -- infer/src/checkers/IdAccessPathMapDomain.mli | 2 +- infer/src/checkers/SimpleChecker.ml | 5 ++--- infer/src/checkers/SinkTrace.ml | 4 ++-- infer/src/checkers/Siof.ml | 8 +++---- infer/src/checkers/ThreadSafety.ml | 8 +++---- infer/src/checkers/ThreadSafetyDomain.ml | 12 +++++------ infer/src/checkers/Trace.ml | 6 ++++-- infer/src/checkers/Trace.mli | 5 ++++- infer/src/checkers/accessPathDomains.ml | 6 +++--- infer/src/checkers/accessPathDomains.mli | 2 +- infer/src/checkers/accessTree.ml | 16 ++++++-------- infer/src/checkers/accessTree.mli | 8 +++---- infer/src/checkers/annotationReachability.ml | 19 ++++++++--------- infer/src/checkers/copyPropagation.ml | 2 -- infer/src/checkers/liveness.ml | 3 --- infer/src/quandary/TaintAnalysis.ml | 22 ++++++++++---------- infer/src/unit/BoundedCallTreeTests.ml | 16 +++++++------- infer/src/unit/TaintTests.ml | 5 ++++- infer/src/unit/abstractInterpreterTests.ml | 5 +++-- infer/src/unit/accessTreeTests.ml | 10 ++++----- infer/src/unit/addressTakenTests.ml | 2 +- infer/src/unit/analyzerTester.ml | 8 +++---- infer/src/unit/copyPropagationTests.ml | 2 +- infer/src/unit/livenessTests.ml | 2 +- 31 files changed, 147 insertions(+), 127 deletions(-) diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 635226787..9f56d1356 100644 --- a/infer/src/backend/preanal.ml +++ b/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 diff --git a/infer/src/checkers/AbstractDomain.ml b/infer/src/checkers/AbstractDomain.ml index dfff8107f..e46f429cc 100644 --- a/infer/src/checkers/AbstractDomain.ml +++ b/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 = (&&) diff --git a/infer/src/checkers/AbstractDomain.mli b/infer/src/checkers/AbstractDomain.mli index c26f5b754..281368a99 100644 --- a/infer/src/checkers/AbstractDomain.mli +++ b/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 diff --git a/infer/src/checkers/AbstractInterpreter.ml b/infer/src/checkers/AbstractInterpreter.ml index 900bceba4..0a1dc21a4 100644 --- a/infer/src/checkers/AbstractInterpreter.ml +++ b/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 diff --git a/infer/src/checkers/AbstractInterpreter.mli b/infer/src/checkers/AbstractInterpreter.mli index 2b49eb8d3..9196529ac 100644 --- a/infer/src/checkers/AbstractInterpreter.mli +++ b/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 diff --git a/infer/src/checkers/BoundedCallTree.ml b/infer/src/checkers/BoundedCallTree.ml index 0aa1250d2..ed3a1d426 100644 --- a/infer/src/checkers/BoundedCallTree.ml +++ b/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 diff --git a/infer/src/checkers/IdAccessPathMapDomain.ml b/infer/src/checkers/IdAccessPathMapDomain.ml index ed959d3eb..8eb00b008 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.ml +++ b/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 diff --git a/infer/src/checkers/IdAccessPathMapDomain.mli b/infer/src/checkers/IdAccessPathMapDomain.mli index 2dcdde878..622ba359a 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.mli +++ b/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 diff --git a/infer/src/checkers/SimpleChecker.ml b/infer/src/checkers/SimpleChecker.ml index dfc2819a9..516140402 100644 --- a/infer/src/checkers/SimpleChecker.ml +++ b/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 diff --git a/infer/src/checkers/SinkTrace.ml b/infer/src/checkers/SinkTrace.ml index 3b85d4a8c..a01b984f6 100644 --- a/infer/src/checkers/SinkTrace.ml +++ b/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 = diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml index 4ab565020..9dd34429a 100644 --- a/infer/src/checkers/Siof.ml +++ b/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 = diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index cf8510e09..22761e660 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/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 diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 259e0af94..44ad763dd 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/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 = diff --git a/infer/src/checkers/Trace.ml b/infer/src/checkers/Trace.ml index 46edd3141..ba65ed2f4 100644 --- a/infer/src/checkers/Trace.ml +++ b/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 diff --git a/infer/src/checkers/Trace.mli b/infer/src/checkers/Trace.mli index 29e388b9f..dd2e3f5ed 100644 --- a/infer/src/checkers/Trace.mli +++ b/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 diff --git a/infer/src/checkers/accessPathDomains.ml b/infer/src/checkers/accessPathDomains.ml index acd7854bb..9d9b925b9 100644 --- a/infer/src/checkers/accessPathDomains.ml +++ b/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 diff --git a/infer/src/checkers/accessPathDomains.mli b/infer/src/checkers/accessPathDomains.mli index 7a21e2a45..85f5120e0 100644 --- a/infer/src/checkers/accessPathDomains.mli +++ b/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 diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml index 352cb4af6..58f0e5d9a 100644 --- a/infer/src/checkers/accessTree.ml +++ b/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 = , then x[j].f.g = , I don't want to overwrite . 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 diff --git a/infer/src/checkers/accessTree.mli b/infer/src/checkers/accessTree.mli index ef201aa3a..b62b05b85 100644 --- a/infer/src/checkers/accessTree.mli +++ b/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 diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index ea272d5a0..7ae068f19 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/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, _) -> diff --git a/infer/src/checkers/copyPropagation.ml b/infer/src/checkers/copyPropagation.ml index fd8422341..c79ce2b3c 100644 --- a/infer/src/checkers/copyPropagation.ml +++ b/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 = diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index dc99ec904..7d37f9ac7 100644 --- a/infer/src/checkers/liveness.ml +++ b/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)) diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index be20cb3af..8d9a7ccba 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/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 -> diff --git a/infer/src/unit/BoundedCallTreeTests.ml b/infer/src/unit/BoundedCallTreeTests.ml index 4aaed0eca..0f3e5aeac 100644 --- a/infer/src/unit/BoundedCallTreeTests.ml +++ b/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 @ diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 6bc1013ce..61c37c363 100644 --- a/infer/src/unit/TaintTests.ml +++ b/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 diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml index c858e48da..a14e0c922 100644 --- a/infer/src/unit/abstractInterpreterTests.ml +++ b/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) diff --git a/infer/src/unit/accessTreeTests.ml b/infer/src/unit/accessTreeTests.ml index 8ebcfd672..09dc5db70 100644 --- a/infer/src/unit/accessTreeTests.ml +++ b/infer/src/unit/accessTreeTests.ml @@ -14,10 +14,10 @@ module F = Format (* string set domain we use to ensure we're getting the expected traces *) module MockTraceDomain = struct include AbstractDomain.FiniteSet - (PrettyPrintable.MakePPSet(struct - include String - let pp_element fmt s = Format.fprintf fmt "%s" s - end)) + (PrettyPrintable.MakePPSet(struct + include String + let pp_element fmt s = Format.fprintf fmt "%s" s + end)) let top_str = "T" @@ -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; diff --git a/infer/src/unit/addressTakenTests.ml b/infer/src/unit/addressTakenTests.ml index a3e81240a..37bbf6e83 100644 --- a/infer/src/unit/addressTakenTests.ml +++ b/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 diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index aa0816d65..942ba6840 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/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 diff --git a/infer/src/unit/copyPropagationTests.ml b/infer/src/unit/copyPropagationTests.ml index 9b4074d86..1b3b6e1ce 100644 --- a/infer/src/unit/copyPropagationTests.ml +++ b/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 diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml index 2bc23ba93..cb7b8db49 100644 --- a/infer/src/unit/livenessTests.ml +++ b/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