From 0859f61695d0a546a493651a67efe7884ac69cb7 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 29 Apr 2020 02:59:00 -0700 Subject: [PATCH] make AbstractInterpreter agnostic in ProcData Summary: `ProcData.t` contains a `Summary.t`. Eventually we want to fix this too so that checkers don't depend on backend/, i.e. on all the other checkers via Summary.ml. But in order to migrate progressively we can first migrate absint/ and one step on the way is for it to not know what kind of analysis data it is passing around. This extra flexibility only costs us passing an extra `Procdesc.t` in a couple more functions so it's actually not a bad change in itself. Reviewed By: ngorogiannis Differential Revision: D21257466 fbshipit-source-id: a91f7b191 --- infer/src/absint/AbstractInterpreter.ml | 69 +++++++++---------- infer/src/absint/AbstractInterpreter.mli | 12 ++-- infer/src/absint/LowerHil.ml | 21 +++--- infer/src/absint/LowerHil.mli | 6 +- infer/src/absint/TransferFunctions.ml | 8 +-- infer/src/absint/TransferFunctions.mli | 8 +-- infer/src/{absint => backend}/ProcData.ml | 8 --- infer/src/{absint => backend}/ProcData.mli | 8 --- .../bufferoverrun/bufferOverrunAnalysis.ml | 6 +- infer/src/checkers/NullabilityPreanalysis.ml | 5 +- infer/src/checkers/RequiredProps.ml | 8 ++- infer/src/checkers/SelfInBlock.ml | 6 +- infer/src/checkers/SimpleChecker.ml | 6 +- infer/src/checkers/Siof.ml | 6 +- infer/src/checkers/addressTaken.ml | 2 +- infer/src/checkers/annotationReachability.ml | 6 +- infer/src/checkers/control.ml | 4 +- infer/src/checkers/functionPointers.ml | 4 +- infer/src/checkers/liveness.ml | 6 +- infer/src/checkers/liveness.mli | 2 +- infer/src/checkers/preanal.ml | 12 ++-- infer/src/checkers/purity.ml | 11 +-- infer/src/checkers/reachingDefs.ml | 4 +- infer/src/checkers/uninit.ml | 6 +- infer/src/concurrency/RacerD.ml | 6 +- infer/src/concurrency/starvation.ml | 6 +- infer/src/labs/ResourceLeaks.ml | 9 ++- infer/src/pulse/Pulse.ml | 6 +- infer/src/quandary/TaintAnalysis.ml | 6 +- infer/src/unit/TaintTests.ml | 5 +- infer/src/unit/abstractInterpreterTests.ml | 10 ++- infer/src/unit/addressTakenTests.ml | 4 +- infer/src/unit/analyzerTester.ml | 11 +-- infer/src/unit/livenessTests.ml | 4 +- 34 files changed, 158 insertions(+), 143 deletions(-) rename infer/src/{absint => backend}/ProcData.ml (61%) rename infer/src/{absint => backend}/ProcData.mli (63%) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 1ff623aa0..03f3ec73f 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -17,19 +17,19 @@ module VisitCount : sig val first_time : t - val succ : pdesc:Procdesc.t -> t -> t + val succ : t -> t end = struct type t = int let first_time = 1 - let succ ~pdesc visit_count = + let succ visit_count = let visit_count' = visit_count + 1 in if visit_count' > Config.max_widens then - L.(die InternalError) - "Exceeded max widening threshold %d while analyzing %a. Please check your widening \ - operator or increase the threshold" - Config.max_widens Procname.pp (Procdesc.get_proc_name pdesc) ; + L.die InternalError + "Exceeded max widening threshold %d. Please check your widening operator or increase the \ + threshold" + Config.max_widens ; visit_count' end @@ -56,21 +56,23 @@ module type S = sig val compute_post : ?do_narrowing:bool -> ?pp_instr:(TransferFunctions.Domain.t -> Sil.instr -> (Format.formatter -> unit) option) - -> TransferFunctions.extras ProcData.t + -> TransferFunctions.analysis_data -> initial:TransferFunctions.Domain.t + -> Procdesc.t -> TransferFunctions.Domain.t option val exec_cfg : ?do_narrowing:bool -> TransferFunctions.CFG.t - -> TransferFunctions.extras ProcData.t + -> TransferFunctions.analysis_data -> initial:TransferFunctions.Domain.t -> invariant_map val exec_pdesc : ?do_narrowing:bool - -> TransferFunctions.extras ProcData.t + -> TransferFunctions.analysis_data -> initial:TransferFunctions.Domain.t + -> Procdesc.t -> invariant_map val extract_post : InvariantMap.key -> 'a State.t InvariantMap.t -> 'a option @@ -112,7 +114,7 @@ module MakeDisjunctiveTransferFunctions struct module CFG = T.CFG - type extras = T.extras + type analysis_data = T.analysis_data module Domain = struct (** a list [\[x1; x2; ...; xN\]] represents a disjunction [x1 ∨ x2 ∨ ... ∨ xN] *) @@ -180,10 +182,10 @@ struct F.fprintf f "@[%d disjuncts:@;%a@]" (List.length disjuncts) pp_disjuncts disjuncts end - let exec_instr pre_disjuncts extras node instr = + let exec_instr pre_disjuncts analysis_data node instr = List.foldi pre_disjuncts ~init:[] ~f:(fun i post_disjuncts pre_disjunct -> L.d_printfln "@[Executing instruction from disjunct #%d@;" i ; - let disjuncts' = T.exec_instr pre_disjunct extras node instr in + let disjuncts' = T.exec_instr pre_disjunct analysis_data node instr in ( if Config.write_html then let n = List.length disjuncts' in L.d_printfln "@]@\n@[Got %d disjunct%s back@]" n (if Int.equal n 1 then "" else "s") ) ; @@ -315,17 +317,16 @@ module AbstractInterpreterCommon (TransferFunctions : NodeTransferFunctions) = s (* Note on narrowing operations: we defines the narrowing operations simply to take a smaller one. So, as of now, the termination of narrowing is not guaranteed in general. *) - let exec_node ~pp_instr ({ProcData.summary} as proc_data) node ~is_loop_head ~is_narrowing - astate_pre inv_map = + let exec_node ~pp_instr analysis_data node ~is_loop_head ~is_narrowing astate_pre inv_map = let node_id = Node.id node in let update_inv_map inv_map new_pre old_state_opt = - let new_post = exec_node_instrs old_state_opt ~pp_instr proc_data node new_pre in + let new_post = exec_node_instrs old_state_opt ~pp_instr analysis_data node new_pre in let new_visit_count = match old_state_opt with | None -> VisitCount.first_time | Some {State.visit_count; _} -> - VisitCount.succ ~pdesc:(Summary.get_proc_desc summary) visit_count + VisitCount.succ visit_count in InvariantMap.add node_id {State.pre= new_pre; post= new_post; visit_count= new_visit_count} @@ -351,9 +352,8 @@ module AbstractInterpreterCommon (TransferFunctions : NodeTransferFunctions) = s else Domain.leq ~lhs:new_pre ~rhs:old_state.State.pre then (inv_map, ReachedFixPoint) else if is_narrowing && not (Domain.leq ~lhs:new_pre ~rhs:old_state.State.pre) then ( - L.(debug Analysis Verbose) - "Terminate narrowing because old and new states are not comparable at %a:%a@." - Procname.pp (Summary.get_proc_name summary) Node.pp_id node_id ; + L.d_printfln "Terminate narrowing because old and new states are not comparable: %a@." + Node.pp_id node_id ; (inv_map, ReachedFixPoint) ) else (update_inv_map inv_map new_pre (Some old_state), DidNotReachFixPoint) else @@ -401,17 +401,16 @@ module AbstractInterpreterCommon (TransferFunctions : NodeTransferFunctions) = s (** compute and return an invariant map for [pdesc] *) - let make_exec_pdesc ~exec_cfg_internal ({ProcData.summary} as proc_data) ~do_narrowing ~initial = - exec_cfg_internal ~pp_instr:pp_sil_instr - (CFG.from_pdesc (Summary.get_proc_desc summary)) - proc_data ~do_narrowing ~initial + let make_exec_pdesc ~exec_cfg_internal analysis_data ~do_narrowing ~initial proc_desc = + exec_cfg_internal ~pp_instr:pp_sil_instr (CFG.from_pdesc proc_desc) analysis_data ~do_narrowing + ~initial (** compute and return the postcondition of [pdesc] *) - let make_compute_post ~exec_cfg_internal ?(pp_instr = pp_sil_instr) - ({ProcData.summary} as proc_data) ~do_narrowing ~initial = - let cfg = CFG.from_pdesc (Summary.get_proc_desc summary) in - let inv_map = exec_cfg_internal ~pp_instr cfg proc_data ~do_narrowing ~initial in + let make_compute_post ~exec_cfg_internal ?(pp_instr = pp_sil_instr) analysis_data ~do_narrowing + ~initial proc_desc = + let cfg = CFG.from_pdesc proc_desc in + let inv_map = exec_cfg_internal ~pp_instr cfg analysis_data ~do_narrowing ~initial in extract_post (Node.id (CFG.exit_node cfg)) inv_map end @@ -421,17 +420,17 @@ module MakeWithScheduler struct include AbstractInterpreterCommon (SimpleNodeTransferFunctions (TransferFunctions)) - let rec exec_worklist ~pp_instr cfg ({ProcData.summary} as proc_data) work_queue inv_map = + let rec exec_worklist ~pp_instr cfg analysis_data work_queue inv_map = match Scheduler.pop work_queue with | Some (_, [], work_queue') -> - exec_worklist ~pp_instr cfg proc_data work_queue' inv_map + exec_worklist ~pp_instr cfg analysis_data work_queue' inv_map | Some (node, _, work_queue') -> let inv_map_post, work_queue_post = match compute_pre cfg node inv_map with | Some astate_pre -> ( - let is_loop_head = CFG.is_loop_head (Summary.get_proc_desc summary) node in + let is_loop_head = CFG.is_loop_head (CFG.proc_desc cfg) node in match - exec_node ~pp_instr proc_data node ~is_loop_head ~is_narrowing:false astate_pre + exec_node ~pp_instr analysis_data node ~is_loop_head ~is_narrowing:false astate_pre inv_map with | inv_map, ReachedFixPoint -> @@ -441,20 +440,20 @@ struct | None -> (inv_map, work_queue') in - exec_worklist ~pp_instr cfg proc_data work_queue_post inv_map_post + exec_worklist ~pp_instr cfg analysis_data work_queue_post inv_map_post | None -> inv_map (** compute and return an invariant map for [cfg] *) - let exec_cfg_internal ~pp_instr cfg proc_data ~do_narrowing:_ ~initial = + let exec_cfg_internal ~pp_instr cfg analysis_data ~do_narrowing:_ ~initial = let start_node = CFG.start_node cfg in let inv_map, _did_not_reach_fix_point = - exec_node ~pp_instr proc_data start_node ~is_loop_head:false ~is_narrowing:false initial + exec_node ~pp_instr analysis_data start_node ~is_loop_head:false ~is_narrowing:false initial InvariantMap.empty in let work_queue = Scheduler.schedule_succs (Scheduler.empty cfg) start_node in - exec_worklist ~pp_instr cfg proc_data work_queue inv_map + exec_worklist ~pp_instr cfg analysis_data work_queue inv_map let exec_cfg ?do_narrowing:_ = exec_cfg_internal ~pp_instr:pp_sil_instr ~do_narrowing:false diff --git a/infer/src/absint/AbstractInterpreter.mli b/infer/src/absint/AbstractInterpreter.mli index cd2eabe9e..aa0d2c844 100644 --- a/infer/src/absint/AbstractInterpreter.mli +++ b/infer/src/absint/AbstractInterpreter.mli @@ -27,24 +27,26 @@ module type S = sig val compute_post : ?do_narrowing:bool -> ?pp_instr:(TransferFunctions.Domain.t -> Sil.instr -> (Format.formatter -> unit) option) - -> TransferFunctions.extras ProcData.t + -> TransferFunctions.analysis_data -> initial:TransferFunctions.Domain.t + -> Procdesc.t -> TransferFunctions.Domain.t option - (** compute and return the postcondition for the given procedure starting from [initial]. + (** compute and return the postcondition for the given {Procdesc.t} starting from [initial]. [pp_instr] is used for the debug HTML and passed as a hook to handle both SIL and HIL CFGs. *) val exec_cfg : ?do_narrowing:bool -> TransferFunctions.CFG.t - -> TransferFunctions.extras ProcData.t + -> TransferFunctions.analysis_data -> initial:TransferFunctions.Domain.t -> invariant_map (** compute and return invariant map for the given CFG/procedure starting from [initial]. *) val exec_pdesc : ?do_narrowing:bool - -> TransferFunctions.extras ProcData.t + -> TransferFunctions.analysis_data -> initial:TransferFunctions.Domain.t + -> Procdesc.t -> invariant_map (** compute and return invariant map for the given procedure starting from [initial] *) @@ -77,6 +79,6 @@ module MakeDisjunctive (T : TransferFunctions.DisjReady) (DConfig : TransferFunctions.DisjunctiveConfig) : S - with type TransferFunctions.extras = T.extras + with type TransferFunctions.analysis_data = T.analysis_data and module TransferFunctions.CFG = T.CFG and type TransferFunctions.Domain.t = T.Domain.t list diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index 8bec0e209..d6da320ee 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -30,7 +30,7 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig) module CFG = TransferFunctions.CFG module Domain = MakeHILDomain (TransferFunctions.Domain) - type extras = TransferFunctions.extras + type analysis_data = TransferFunctions.analysis_data let pp_session_name = TransferFunctions.pp_session_name @@ -40,7 +40,7 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig) && match ConcurrencyModels.get_lock_effect pname actuals with Unlock _ -> true | _ -> false - let exec_instr_actual extras bindings node hil_instr actual_state = + let exec_instr_actual analysis_data bindings node hil_instr actual_state = match (hil_instr : HilInstr.t) with | Call (_, Direct callee_pname, actuals, _, loc) as hil_instr when is_java_unlock callee_pname actuals -> @@ -53,11 +53,11 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig) let dummy_assign = HilInstr.Assign (lhs_access_path, HilExp.AccessExpression access_expr, loc) in - TransferFunctions.exec_instr astate_acc extras node dummy_assign ) + TransferFunctions.exec_instr astate_acc analysis_data node dummy_assign ) in - (TransferFunctions.exec_instr actual_state' extras node hil_instr, Bindings.empty) + (TransferFunctions.exec_instr actual_state' analysis_data node hil_instr, Bindings.empty) | hil_instr -> - (TransferFunctions.exec_instr actual_state extras node hil_instr, bindings) + (TransferFunctions.exec_instr actual_state analysis_data node hil_instr, bindings) let append_bindings = IList.append_no_duplicates ~cmp:Var.compare |> Staged.unstage @@ -84,13 +84,13 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig) (Some instr, bindings) - let exec_instr ((actual_state, bindings) as astate) extras node instr = + let exec_instr ((actual_state, bindings) as astate) analysis_data node instr = let actual_state', bindings' = match hil_instr_of_sil bindings instr with | None, bindings -> (actual_state, bindings) | Some hil_instr, bindings -> - exec_instr_actual extras bindings node hil_instr actual_state + exec_instr_actual analysis_data bindings node hil_instr actual_state in if phys_equal bindings bindings' && phys_equal actual_state actual_state' then astate else (actual_state', bindings') @@ -102,7 +102,7 @@ module type S = sig type domain val compute_post : - Interpreter.TransferFunctions.extras ProcData.t -> initial:domain -> domain option + Interpreter.TransferFunctions.analysis_data -> initial:domain -> Procdesc.t -> domain option end module MakeAbstractInterpreterWithConfig @@ -117,7 +117,7 @@ module MakeAbstractInterpreterWithConfig type domain = TransferFunctions.Domain.t - let compute_post proc_data ~initial = + let compute_post analysis_data ~initial proc_desc = let initial' = (initial, Bindings.empty) in let pp_instr (_, bindings) instr = match LowerHilInterpreter.hil_instr_of_sil bindings instr with @@ -126,7 +126,8 @@ module MakeAbstractInterpreterWithConfig | None, _ -> None in - Interpreter.compute_post ~pp_instr proc_data ~initial:initial' |> Option.map ~f:fst + Interpreter.compute_post ~pp_instr analysis_data ~initial:initial' proc_desc + |> Option.map ~f:fst end module MakeAbstractInterpreter (TransferFunctions : TransferFunctions.HIL) = diff --git a/infer/src/absint/LowerHil.mli b/infer/src/absint/LowerHil.mli index 9c6a4093d..bf1407a8e 100644 --- a/infer/src/absint/LowerHil.mli +++ b/infer/src/absint/LowerHil.mli @@ -27,9 +27,9 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig) module Domain : module type of AbstractDomain.Pair (TransferFunctions.Domain) (Bindings) - type extras = TransferFunctions.extras + type analysis_data = TransferFunctions.analysis_data - val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Domain.t + val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> Sil.instr -> Domain.t val pp_session_name : CFG.Node.t -> Format.formatter -> unit end @@ -40,7 +40,7 @@ module type S = sig type domain val compute_post : - Interpreter.TransferFunctions.extras ProcData.t -> initial:domain -> domain option + Interpreter.TransferFunctions.analysis_data -> initial:domain -> Procdesc.t -> domain option (** compute and return the postcondition for the given procedure starting from [initial]. *) end diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index b315ca025..6f79c860d 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/infer/src/absint/TransferFunctions.ml @@ -12,11 +12,11 @@ module type S = sig module Domain : AbstractDomain.S - type extras + type analysis_data type instr - val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> instr -> Domain.t + val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> instr -> Domain.t val pp_session_name : CFG.Node.t -> Format.formatter -> unit end @@ -44,9 +44,9 @@ module type DisjReady = sig module Domain : AbstractDomain.NoJoin - type extras + type analysis_data - val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Domain.t list + val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> Sil.instr -> Domain.t list val pp_session_name : CFG.Node.t -> Format.formatter -> unit end diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index 67da62eb1..3b86b3e83 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/infer/src/absint/TransferFunctions.mli @@ -17,12 +17,12 @@ module type S = sig (** abstract domain whose state we propagate *) (** read-only extra state (results of previous analyses, globals, etc.) *) - type extras + type analysis_data (** type of the instructions the transfer functions operate on *) type instr - val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> instr -> Domain.t + val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> instr -> Domain.t (** [exec_instr astate proc_data node instr] should usually return [astate'] such that [{astate} instr {astate'}] is a valid Hoare triple. In other words, [exec_instr] defines how executing an instruction from a given abstract state changes that state into a new one. This @@ -57,9 +57,9 @@ module type DisjReady = sig module Domain : AbstractDomain.NoJoin - type extras + type analysis_data - val exec_instr : Domain.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Domain.t list + val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> Sil.instr -> Domain.t list val pp_session_name : CFG.Node.t -> Format.formatter -> unit end diff --git a/infer/src/absint/ProcData.ml b/infer/src/backend/ProcData.ml similarity index 61% rename from infer/src/absint/ProcData.ml rename to infer/src/backend/ProcData.ml index 06a675afe..57aa63fdf 100644 --- a/infer/src/absint/ProcData.ml +++ b/infer/src/backend/ProcData.ml @@ -8,11 +8,3 @@ open! IStd type 'a t = {summary: Summary.t; tenv: Tenv.t; extras: 'a} - -type no_extras = unit - -let empty_extras = () - -let make summary tenv extras = {summary; tenv; extras} - -let make_default summary tenv = make summary tenv empty_extras diff --git a/infer/src/absint/ProcData.mli b/infer/src/backend/ProcData.mli similarity index 63% rename from infer/src/absint/ProcData.mli rename to infer/src/backend/ProcData.mli index 743f93f22..57aa63fdf 100644 --- a/infer/src/absint/ProcData.mli +++ b/infer/src/backend/ProcData.mli @@ -8,11 +8,3 @@ open! IStd type 'a t = {summary: Summary.t; tenv: Tenv.t; extras: 'a} - -type no_extras - -val empty_extras : no_extras - -val make : Summary.t -> Tenv.t -> 'a -> 'a t - -val make_default : Summary.t -> Tenv.t -> no_extras t diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 14382a4ac..5f20b7fa1 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -58,7 +58,7 @@ module TransferFunctions = struct module CFG = CFG module Domain = Dom.Mem - type nonrec extras = extras + type analysis_data = extras ProcData.t let instantiate_latest_prune ~ret_id ~callee_exit_mem eval_sym_trace location mem = match @@ -455,10 +455,10 @@ let compute_invariant_map : let cfg = CFG.from_pdesc pdesc in let pdata = let oenv = OndemandEnv.mk pdesc tenv integer_type_widths in - ProcData.make summary tenv {get_summary; get_formals; oenv} + {ProcData.summary; tenv; extras= {get_summary; get_formals; oenv}} in let initial = Init.initial_state pdata (CFG.start_node cfg) in - Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata + Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata pdesc let cached_compute_invariant_map = diff --git a/infer/src/checkers/NullabilityPreanalysis.ml b/infer/src/checkers/NullabilityPreanalysis.ml index f3287d8e7..ebf86b1e7 100644 --- a/infer/src/checkers/NullabilityPreanalysis.ml +++ b/infer/src/checkers/NullabilityPreanalysis.ml @@ -20,7 +20,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = FieldsAssignedInConstructors - type extras = Exp.t Ident.Hash.t + type analysis_data = Exp.t Ident.Hash.t ProcData.t let exp_is_null ids_map exp = match exp with @@ -95,7 +95,8 @@ let analysis cfg tenv = if Procdesc.is_defined pdesc && Procname.is_constructor proc_name then match FieldsAssignedInConstructorsChecker.compute_post ~initial - (ProcData.make (Summary.OnDisk.reset pdesc) tenv (Ident.Hash.create 10)) + {ProcData.summary= Summary.OnDisk.reset pdesc; tenv; extras= Ident.Hash.create 10} + pdesc with | Some new_domain -> FieldsAssignedInConstructors.union new_domain domain diff --git a/infer/src/checkers/RequiredProps.ml b/infer/src/checkers/RequiredProps.ml index 67cc57871..8c7f1018b 100644 --- a/infer/src/checkers/RequiredProps.ml +++ b/infer/src/checkers/RequiredProps.ml @@ -205,6 +205,8 @@ module TransferFunctions = struct type extras = {get_proc_summary_and_formals: get_proc_summary_and_formals} + type analysis_data = extras ProcData.t + let apply_callee_summary summary_opt callsite ~caller_pname ~callee_pname ret_id_typ formals actuals astate = Option.value_map summary_opt ~default:astate ~f:(fun callee_summary -> @@ -291,21 +293,21 @@ let init_extras summary = |> Option.map ~f:(fun (callee_pdesc, callee_summary) -> (callee_summary, Procdesc.get_pvar_formals callee_pdesc) ) in - TransferFunctions.{get_proc_summary_and_formals} + {TransferFunctions.get_proc_summary_and_formals} let checker {Callbacks.summary; exe_env} = let proc_desc = Summary.get_proc_desc summary in let proc_name = Summary.get_proc_name summary in let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in - let proc_data = ProcData.make summary tenv (init_extras summary) in + let proc_data = {ProcData.summary; tenv; extras= init_extras summary} in let ret_path = let ret_var = Procdesc.get_ret_var proc_desc in let ret_typ = Procdesc.get_ret_type proc_desc in Domain.LocalAccessPath.make_from_pvar ret_var ret_typ proc_name in let initial = Domain.init tenv proc_name (Procdesc.get_pvar_formals proc_desc) ret_path in - match Analyzer.compute_post proc_data ~initial with + match Analyzer.compute_post proc_data ~initial proc_desc with | Some post -> let is_void_func = Procdesc.get_ret_type proc_desc |> Typ.is_void in let post = Domain.get_summary ~is_void_func post in diff --git a/infer/src/checkers/SelfInBlock.ml b/infer/src/checkers/SelfInBlock.ml index 90866f6b6..9e7b936e3 100644 --- a/infer/src/checkers/SelfInBlock.ml +++ b/infer/src/checkers/SelfInBlock.ml @@ -143,7 +143,7 @@ module TransferFunctions = struct module Domain = Domain module CFG = ProcCfg.Normal - type extras = unit + type analysis_data = unit ProcData.t let pp_session_name _node fmt = F.pp_print_string fmt "SelfCapturedInBlock" @@ -555,10 +555,10 @@ let checker {Callbacks.exe_env; summary} = let initial = {Domain.vars= Vars.empty; strongVars= StrongEqualToWeakCapturedVars.empty} in let procname = Summary.get_proc_name summary in let tenv = Exe_env.get_tenv exe_env procname in - let proc_data = ProcData.make summary tenv () in + let proc_data = {ProcData.summary; tenv; extras= ()} in let attributes = Summary.get_attributes summary in ( if Procname.is_objc_block procname then - match Analyzer.compute_post proc_data ~initial with + match Analyzer.compute_post proc_data ~initial (Summary.get_proc_desc summary) with | Some domain -> report_issues summary domain.vars attributes | None -> diff --git a/infer/src/checkers/SimpleChecker.ml b/infer/src/checkers/SimpleChecker.ml index 797ad5757..295bf744e 100644 --- a/infer/src/checkers/SimpleChecker.ml +++ b/infer/src/checkers/SimpleChecker.ml @@ -60,7 +60,7 @@ module Make (Spec : Spec) : S = struct module CFG = CFG module Domain = Domain - type extras = ProcData.no_extras + type analysis_data = unit ProcData.t let exec_instr astate_set proc_data node instr = let node_kind = CFG.Node.kind node in @@ -94,7 +94,9 @@ module Make (Spec : Spec) : S = struct (fun astate -> Spec.report astate (ProcCfg.Exceptional.Node.loc node) proc_name) astate_set in - let inv_map = Analyzer.exec_pdesc (ProcData.make_default summary tenv) ~initial:Domain.empty in + let inv_map = + Analyzer.exec_pdesc {ProcData.summary; tenv; extras= ()} ~initial:Domain.empty proc_desc + in Analyzer.InvariantMap.iter do_reporting inv_map ; summary end diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml index 6772021e2..ab11d3431 100644 --- a/infer/src/checkers/Siof.ml +++ b/infer/src/checkers/Siof.ml @@ -66,7 +66,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = SiofDomain - type extras = ProcData.no_extras + type analysis_data = unit ProcData.t let is_compile_time_constructed summary pv = let init_pname = Pvar.get_initializer_pname pv in @@ -287,7 +287,7 @@ let checker {Callbacks.exe_env; summary} : Summary.t = in includes_iostream (Procdesc.get_attributes proc_desc).ProcAttributes.translation_unit in - let proc_data = ProcData.make_default summary tenv in + let proc_data = {ProcData.summary; tenv; extras= ()} in let initial = ( Bottom , if standard_streams_initialized_in_tu then SiofDomain.VarNames.of_list standard_streams @@ -302,7 +302,7 @@ let checker {Callbacks.exe_env; summary} : Summary.t = match pname with ObjC_Cpp cpp_pname -> Procname.ObjC_Cpp.is_constexpr cpp_pname | _ -> false then Payload.update_summary initial summary else - match Analyzer.compute_post proc_data ~initial with + match Analyzer.compute_post proc_data ~initial proc_desc with | Some post -> Payload.update_summary post summary | None -> diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml index f99d2c131..98955498d 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/infer/src/checkers/addressTaken.ml @@ -17,7 +17,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = Domain - type extras = ProcData.no_extras + type analysis_data = unit ProcData.t let rec add_address_taken_pvars exp astate = match exp with diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 5473cdbfa..bdfc9a3f7 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -485,7 +485,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = Domain - type extras = AnnotationSpec.t list + type analysis_data = AnnotationSpec.t list ProcData.t let is_sink tenv (spec : AnnotationSpec.t) ~caller_pname ~callee_pname = spec.sink_predicate tenv callee_pname @@ -548,8 +548,8 @@ let checker ({Callbacks.exe_env; summary} as callback) : Summary.t = let tenv = Exe_env.get_tenv exe_env proc_name in let initial = Domain.empty in let specs = get_annot_specs proc_name in - let proc_data = ProcData.make summary tenv specs in - match Analyzer.compute_post proc_data ~initial with + let proc_data = {ProcData.summary; tenv; extras= specs} in + match Analyzer.compute_post proc_data ~initial (Summary.get_proc_desc summary) with | Some annot_map -> List.iter specs ~f:(fun spec -> spec.AnnotationSpec.report callback annot_map) ; Payload.update_summary annot_map summary diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml index b99b4713b..ee86963d9 100644 --- a/infer/src/checkers/control.ml +++ b/infer/src/checkers/control.ml @@ -56,7 +56,7 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = ControlDepSet - type extras = loop_control_maps + type analysis_data = loop_control_maps ProcData.t let collect_vars_in_exp exp loop_head = Var.get_all_vars_in_exp exp @@ -160,7 +160,7 @@ module ControlDepAnalyzer = AbstractInterpreter.MakeRPO (TransferFunctionsContro type invariant_map = ControlDepAnalyzer.invariant_map let compute_invariant_map summary tenv control_maps : invariant_map = - let proc_data = ProcData.make summary tenv control_maps in + let proc_data = {ProcData.summary; tenv; extras= control_maps} in let node_cfg = CFG.from_pdesc (Summary.get_proc_desc summary) in ControlDepAnalyzer.exec_cfg node_cfg proc_data ~initial:ControlDepSet.empty diff --git a/infer/src/checkers/functionPointers.ml b/infer/src/checkers/functionPointers.ml index c6bde9bac..ce4adf993 100644 --- a/infer/src/checkers/functionPointers.ml +++ b/infer/src/checkers/functionPointers.ml @@ -21,7 +21,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = Domain - type extras = ProcData.no_extras + type analysis_data = unit ProcData.t let exec_instr astate _ _ = function | Sil.Load {id= lhs_id} when Ident.is_none lhs_id -> @@ -91,7 +91,7 @@ let substitute_function_ptrs ~function_pointers node instr = let get_function_pointers summary tenv = - let proc_data = ProcData.make_default summary tenv in + let proc_data = {ProcData.summary; tenv; extras= ()} in let cfg = CFG.from_pdesc (Summary.get_proc_desc summary) in Analyzer.exec_cfg cfg proc_data ~initial:Domain.empty diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index 7cc469c06..ea0201ebc 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -92,7 +92,7 @@ module TransferFunctions (LConfig : LivenessConfig) (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = Domain - type extras = ProcData.no_extras + type analysis_data = unit ProcData.t (** add all of the vars read in [exp] to the live set *) let exp_add_live exp astate = @@ -181,7 +181,7 @@ module CapturedByRefTransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = VarSet - type extras = ProcData.no_extras + type analysis_data = unit ProcData.t let exec_instr astate _ _ instr = List.fold (Sil.exps_of_instr instr) @@ -213,7 +213,7 @@ let get_captured_by_ref_invariant_map proc_desc proc_data = let checker {Callbacks.exe_env; summary} : Summary.t = let proc_desc = Summary.get_proc_desc summary in let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in - let proc_data = ProcData.make_default summary tenv in + let proc_data = {ProcData.summary; tenv; extras= ()} in let captured_by_ref_invariant_map = get_captured_by_ref_invariant_map proc_desc proc_data in let cfg = CFG.from_pdesc proc_desc in let invariant_map = CheckerAnalyzer.exec_cfg cfg proc_data ~initial:Domain.empty in diff --git a/infer/src/checkers/liveness.mli b/infer/src/checkers/liveness.mli index 0a4bb464e..0065d87b9 100644 --- a/infer/src/checkers/liveness.mli +++ b/infer/src/checkers/liveness.mli @@ -14,6 +14,6 @@ module PreAnalysisTransferFunctions (CFG : ProcCfg.S) : TransferFunctions.SIL with module CFG = CFG and module Domain = Domain - and type extras = ProcData.no_extras + and type analysis_data = unit ProcData.t val checker : Callbacks.proc_callback_args -> Summary.t diff --git a/infer/src/checkers/preanal.ml b/infer/src/checkers/preanal.ml index 2817113a2..e759c8895 100644 --- a/infer/src/checkers/preanal.ml +++ b/infer/src/checkers/preanal.ml @@ -161,7 +161,7 @@ module Liveness = struct module CFG = ProcCfg.Exceptional - type extras = LivenessAnalysis.invariant_map + type analysis_data = LivenessAnalysis.invariant_map ProcData.t let postprocess ((reaching_defs, _) as astate) node {ProcData.extras} = let node_id = Procdesc.Node.get_id (CFG.Node.underlying_node node) in @@ -234,14 +234,18 @@ module Liveness = struct (* can't take the address of a variable in Java *) else let initial = AddressTaken.Domain.empty in - match AddressTaken.Analyzer.compute_post (ProcData.make_default summary tenv) ~initial with + match + AddressTaken.Analyzer.compute_post + {ProcData.summary; tenv; extras= ()} + ~initial (Summary.get_proc_desc summary) + with | Some post -> post | None -> AddressTaken.Domain.empty in let nullify_proc_cfg = ProcCfg.Exceptional.from_pdesc (Summary.get_proc_desc summary) in - let nullify_proc_data = ProcData.make summary tenv liveness_inv_map in + let nullify_proc_data = {ProcData.summary; tenv; extras= liveness_inv_map} 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 *) @@ -298,7 +302,7 @@ module Liveness = struct let liveness_proc_cfg = BackwardCfg.from_pdesc (Summary.get_proc_desc summary) in let initial = Liveness.Domain.empty in let liveness_inv_map = - LivenessAnalysis.exec_cfg liveness_proc_cfg (ProcData.make_default summary tenv) ~initial + LivenessAnalysis.exec_cfg liveness_proc_cfg {ProcData.summary; tenv; extras= ()} ~initial in add_nullify_instrs summary tenv liveness_inv_map end diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml index 3a2d039ce..f51106a37 100644 --- a/infer/src/checkers/purity.ml +++ b/infer/src/checkers/purity.ml @@ -29,7 +29,7 @@ module TransferFunctions = struct module CFG = ProcCfg.Normal module Domain = PurityDomain - type extras = purity_extras + type analysis_data = purity_extras ProcData.t let get_alias_set inferbo_mem var = let default = ModifiedVarSet.empty in @@ -215,12 +215,15 @@ let report_errors astate summary = let compute_summary summary tenv get_callee_summary inferbo_invariant_map = let proc_name = Summary.get_proc_name summary in + let proc_desc = Summary.get_proc_desc summary in let formals = - Procdesc.get_formals (Summary.get_proc_desc summary) + Procdesc.get_formals proc_desc |> List.map ~f:(fun (mname, _) -> Var.of_pvar (Pvar.mk mname proc_name)) in - let proc_data = ProcData.make summary tenv {inferbo_invariant_map; formals; get_callee_summary} in - Analyzer.compute_post proc_data ~initial:PurityDomain.pure + let proc_data = + {ProcData.summary; tenv; extras= {inferbo_invariant_map; formals; get_callee_summary}} + in + Analyzer.compute_post proc_data ~initial:PurityDomain.pure proc_desc let checker {Callbacks.exe_env; summary} : Summary.t = diff --git a/infer/src/checkers/reachingDefs.ml b/infer/src/checkers/reachingDefs.ml index 59e209e1d..aae35d037 100644 --- a/infer/src/checkers/reachingDefs.ml +++ b/infer/src/checkers/reachingDefs.ml @@ -24,7 +24,7 @@ module TransferFunctionsReachingDefs (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = ReachingDefsMap - type extras = ProcData.no_extras + type analysis_data = unit ProcData.t (* for each x := e at node n, remove x's definitions and introduce x -> n *) let exec_instr astate _ (node : CFG.Node.t) instr = @@ -70,7 +70,7 @@ type invariant_map = Analyzer.invariant_map let compute_invariant_map summary tenv = let pdesc = Summary.get_proc_desc summary in - let proc_data = ProcData.make_default summary tenv in + let proc_data = {ProcData.summary; tenv; extras= ()} in let node_cfg = NodeCFG.from_pdesc pdesc in Analyzer.exec_cfg node_cfg proc_data ~initial:(init_reaching_defs_with_formals pdesc) diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index d0c7798c8..42d86ccbb 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -75,7 +75,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = RecordDomain - type nonrec extras = extras + type analysis_data = extras ProcData.t let report_intra access_expr loc summary = let message = @@ -352,9 +352,9 @@ let checker {Callbacks.exe_env; summary} : Summary.t = in let proc_data = let formals = FormalMap.make proc_desc in - ProcData.make summary tenv {formals; summary} + {ProcData.summary; tenv; extras= {formals; summary}} in - match Analyzer.compute_post proc_data ~initial with + match Analyzer.compute_post proc_data ~initial proc_desc with | Some {RecordDomain.prepost} -> Payload.update_summary prepost summary | None -> diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index f67d500bd..e11b3bab1 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -23,7 +23,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = RacerDDomain - type extras = FormalMap.t + type analysis_data = FormalMap.t ProcData.t let rec get_access_exp = function | HilExp.AccessExpression access_expr -> @@ -527,8 +527,8 @@ let analyze_procedure {Callbacks.exe_env; summary} = in let initial = set_initial_attributes tenv summary {bottom with ownership; threads; locks} in let formal_map = FormalMap.make proc_desc in - let proc_data = ProcData.make summary tenv formal_map in - Analyzer.compute_post proc_data ~initial + let proc_data = {ProcData.summary; tenv; extras= formal_map} in + Analyzer.compute_post proc_data ~initial proc_desc |> Option.map ~f:(astate_to_summary proc_desc formal_map) |> Option.value_map ~default:summary ~f:(fun post -> Payload.update_summary post summary) else Payload.update_summary empty_summary summary diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 0b45faada..35dade037 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -24,7 +24,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = Domain - type extras = FormalMap.t + type analysis_data = FormalMap.t ProcData.t let log_parse_error error pname actuals = L.debug Analysis Verbose "%s pname:%a actuals:%a@." error Procname.pp pname @@ -358,7 +358,7 @@ let analyze_procedure {Callbacks.exe_env; summary} = if StarvationModels.should_skip_analysis tenv procname [] then summary else let formals = FormalMap.make proc_desc in - let proc_data = ProcData.make summary tenv formals in + let proc_data = {ProcData.summary; tenv; extras= formals} in let loc = Procdesc.get_loc proc_desc in let set_lock_state_for_synchronized_proc astate = if Procdesc.is_java_synchronized proc_desc then @@ -388,7 +388,7 @@ let analyze_procedure {Callbacks.exe_env; summary} = |> set_initial_attributes tenv summary |> set_lock_state_for_synchronized_proc |> set_thread_status_by_annotation in - Analyzer.compute_post proc_data ~initial + Analyzer.compute_post proc_data ~initial proc_desc |> Option.map ~f:filter_blocks |> Option.map ~f:(Domain.summary_of_astate proc_desc) |> Option.fold ~init:summary ~f:(fun acc payload -> Payload.update_summary payload acc) diff --git a/infer/src/labs/ResourceLeaks.ml b/infer/src/labs/ResourceLeaks.ml index 706f0c867..2fb3ae3f3 100644 --- a/infer/src/labs/ResourceLeaks.ml +++ b/infer/src/labs/ResourceLeaks.ml @@ -20,7 +20,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = ResourceLeakDomain - type extras = unit + type analysis_data = unit ProcData.t let is_closeable_typename tenv typename = let is_closable_interface typename _ = @@ -88,8 +88,11 @@ let report_if_leak _post _summary (_proc_data : unit ProcData.t) = () let checker {Callbacks.summary; exe_env} : Summary.t = let proc_name = Summary.get_proc_name summary in let tenv = Exe_env.get_tenv exe_env proc_name in - let proc_data = ProcData.make summary tenv () in - match Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial with + let proc_data = {ProcData.summary; tenv; extras= ()} in + match + Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial + (Summary.get_proc_desc summary) + with | Some post -> report_if_leak post summary proc_data ; Payload.update_summary post summary diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index a35bf7273..dfc5fd173 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -46,7 +46,7 @@ module PulseTransferFunctions = struct module CFG = ProcCfg.Normal module Domain = ExecutionDomain - type extras = get_formals + type analysis_data = get_formals ProcData.t let interprocedural_call caller_summary ret call_exp actuals call_loc get_formals astate = match proc_name_of_call call_exp with @@ -236,8 +236,8 @@ let checker {Callbacks.exe_env; summary} = let get_formals callee_pname = Ondemand.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals in - let proc_data = ProcData.make summary tenv get_formals in - match DisjunctiveAnalyzer.compute_post proc_data ~initial with + let proc_data = {ProcData.summary; tenv; extras= get_formals} in + match DisjunctiveAnalyzer.compute_post proc_data ~initial pdesc with | Some posts -> PulsePayload.update_summary (PulseSummary.of_posts pdesc posts) summary | None -> diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 10940f795..c4cca138e 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -28,7 +28,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct module CFG = CFG module Domain = Domain - type nonrec extras = extras + type analysis_data = extras ProcData.t (* get the node associated with [access_path] in [access_tree] *) let access_path_get_node access_path access_tree (proc_data : extras ProcData.t) = @@ -863,8 +863,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct let formal_map = FormalMap.make proc_desc in {formal_map; summary} in - let proc_data = ProcData.make summary tenv extras in - match Analyzer.compute_post proc_data ~initial with + let proc_data = {ProcData.summary; tenv; extras} in + match Analyzer.compute_post proc_data ~initial proc_desc with | Some access_tree -> Payload.update_summary (make_summary proc_data access_tree) summary | None -> diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 87538aacb..bfb028042 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -153,7 +153,10 @@ let tests = ; ( "sink without source not tracked" , [assign_to_non_source "ret_id"; call_sink "ret_id"; assert_empty] ) ] |> TestInterpreter.create_tests ~pp_opt:pp_sparse - {formal_map= FormalMap.empty; summary= Summary.OnDisk.dummy} + (fun summary -> + { ProcData.summary + ; tenv= Tenv.create () + ; extras= {formal_map= FormalMap.empty; summary= Summary.OnDisk.dummy} } ) ~initial:(MockTaintAnalysis.Domain.bottom, Bindings.empty) in "taint_test_suite" >::: test_list diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml index 24132fa7b..b26216114 100644 --- a/infer/src/unit/abstractInterpreterTests.ml +++ b/infer/src/unit/abstractInterpreterTests.ml @@ -49,7 +49,7 @@ module PathCountTransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = PathCountDomain - type extras = ProcData.no_extras + type analysis_data = unit ProcData.t (* just propagate the current path count *) let exec_instr astate _ _ _ = astate @@ -102,7 +102,9 @@ let tests = , (* we expect the finally block to be visited *) [invariant "1"] ) ; invariant "1" ] ) ] - |> NormalTestInterpreter.create_tests ProcData.empty_extras ~initial + |> NormalTestInterpreter.create_tests + (fun summary -> {ProcData.summary; tenv= Tenv.create (); extras= ()}) + ~initial in let exceptional_test_list = [ ( "try1" @@ -127,6 +129,8 @@ let tests = , (* could arrive here via (1, 2, 3), (1, 4), or (2, 4) *) [invariant "3"] ) ; invariant "3" ] ) ] - |> ExceptionalTestInterpreter.create_tests ProcData.empty_extras ~initial + |> ExceptionalTestInterpreter.create_tests + (fun summary -> {ProcData.summary; tenv= Tenv.create (); extras= ()}) + ~initial in "analyzer_tests_suite" >::: normal_test_list @ exceptional_test_list diff --git a/infer/src/unit/addressTakenTests.ml b/infer/src/unit/addressTakenTests.ml index efbb05df5..79e282289 100644 --- a/infer/src/unit/addressTakenTests.ml +++ b/infer/src/unit/addressTakenTests.ml @@ -57,6 +57,8 @@ let tests = ; invariant "{ &b, &d }" ; var_assign_addrof_var ~rhs_typ:int_ptr_typ "e" "f" ; invariant "{ &b, &f, &d }" ] ) ] - |> TestInterpreter.create_tests ProcData.empty_extras ~initial:AddressTaken.Domain.empty + |> TestInterpreter.create_tests + (fun summary -> {ProcData.summary; tenv= Tenv.create (); 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 3ab84b715..110546aff 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -251,10 +251,12 @@ struct (Summary.OnDisk.reset pdesc, assert_map) - let create_test test_program extras ~initial pp_opt test_pname _ = + let create_test test_program make_analysis_data ~initial pp_opt test_pname _ = let pp_state = Option.value ~default:I.TransferFunctions.Domain.pp pp_opt in let summary, assert_map = structured_program_to_cfg test_program test_pname in - let inv_map = I.exec_pdesc (ProcData.make summary (Tenv.create ()) extras) ~initial in + let inv_map = + I.exec_pdesc (make_analysis_data summary) ~initial (Summary.get_proc_desc summary) + in let collect_invariant_mismatches node_id (inv_str, inv_label) error_msgs_acc = let post_str = try @@ -293,11 +295,12 @@ module Make (T : TransferFunctions.SIL with type CFG.Node.t = Procdesc.Node.t) = let ai_list = [("ai_rpo", AI_RPO.create_test); ("ai_wto", AI_WTO.create_test)] - let create_tests ?(test_pname = Procname.empty_block) ~initial ?pp_opt extras tests = + let create_tests ?(test_pname = Procname.empty_block) ~initial ?pp_opt make_analysis_data tests = let open OUnit2 in List.concat_map ~f:(fun (name, test_program) -> List.map ai_list ~f:(fun (ai_name, create_test) -> - name ^ "_" ^ ai_name >:: create_test test_program extras ~initial pp_opt test_pname ) ) + name ^ "_" ^ ai_name + >:: create_test test_program make_analysis_data ~initial pp_opt test_pname ) ) tests end diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml index 120bab027..5162784da 100644 --- a/infer/src/unit/livenessTests.ml +++ b/infer/src/unit/livenessTests.ml @@ -97,6 +97,8 @@ let tests = ; While (unknown_cond, [id_assign_var "b" "d"]) ; invariant "{ b }" ; id_assign_var "a" "b" ] ) ] - |> TestInterpreter.create_tests ProcData.empty_extras ~initial:Liveness.Domain.empty + |> TestInterpreter.create_tests + (fun summary -> {ProcData.summary; tenv= Tenv.create (); extras= ()}) + ~initial:Liveness.Domain.empty in "liveness_test_suite" >::: test_list