From f41575411cb154771ce27bc32ef70e976fc0c43a Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 6 May 2020 11:23:12 -0700 Subject: [PATCH] make pulse take an `InterproceduralAnalysis.t` Summary: Needed to make pulse into a dune library. Reviewed By: skcho Differential Revision: D21401820 fbshipit-source-id: d8c758913 --- infer/src/backend/registerCheckers.ml | 7 +-- infer/src/pulse/Pulse.ml | 82 +++++++++++++------------- infer/src/pulse/Pulse.mli | 3 +- infer/src/pulse/PulseModels.ml | 85 +++++++++++++-------------- infer/src/pulse/PulseModels.mli | 2 +- infer/src/pulse/PulseOperations.ml | 6 +- infer/src/pulse/PulseOperations.mli | 2 +- infer/src/pulse/PulsePayload.ml | 14 ----- infer/src/pulse/PulsePayload.mli | 10 ---- 9 files changed, 91 insertions(+), 120 deletions(-) delete mode 100644 infer/src/pulse/PulsePayload.ml delete mode 100644 infer/src/pulse/PulsePayload.mli diff --git a/infer/src/backend/registerCheckers.ml b/infer/src/backend/registerCheckers.ml index e63b5566f..b16432fd5 100644 --- a/infer/src/backend/registerCheckers.ml +++ b/infer/src/backend/registerCheckers.ml @@ -107,10 +107,9 @@ let all_checkers = ; { name= "pulse" ; active= Config.(is_checker_enabled Pulse || is_checker_enabled Impurity) ; callbacks= - (Procedure Pulse.checker, Language.Clang) - :: - ( if Config.is_checker_enabled Impurity then [(Procedure Pulse.checker, Language.Java)] - else [] ) } + (let pulse = interprocedural Payloads.Fields.pulse Pulse.checker in + (pulse, Language.Clang) + :: (if Config.is_checker_enabled Impurity then [(pulse, Language.Java)] else []) ) } ; { name= "impurity" ; active= Config.is_checker_enabled Impurity ; callbacks= diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 160384011..c03a7c3d4 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -12,24 +12,27 @@ open IResult.Let_syntax open PulseBasicInterface open PulseDomainInterface -let report summary diagnostic = +let report {InterproceduralAnalysis.proc_desc; err_log} diagnostic = + let attrs = Procdesc.get_attributes proc_desc in let open Diagnostic in - SummaryReporting.log_error summary ~loc:(get_location diagnostic) ~ltr:(get_trace diagnostic) + Reporting.log_error attrs err_log ~loc:(get_location diagnostic) ~ltr:(get_trace diagnostic) (get_issue_type diagnostic) (get_message diagnostic) -let check_error_transform summary ~f = function +let check_error_transform analysis_data ~f = function | Ok astate -> f astate | Error (diagnostic, astate) -> if PulseArithmetic.is_unsat_expensive astate then [] else ( - report summary diagnostic ; + report analysis_data diagnostic ; [ExecutionDomain.AbortProgram astate] ) -let check_error_continue summary result = - check_error_transform summary ~f:(fun astate -> [ExecutionDomain.ContinueProgram astate]) result +let check_error_continue analysis_data result = + check_error_transform analysis_data + ~f:(fun astate -> [ExecutionDomain.ContinueProgram astate]) + result let proc_name_of_call call_exp = @@ -40,19 +43,21 @@ let proc_name_of_call call_exp = None -type get_formals = Procname.t -> (Pvar.t * Typ.t) list option - module PulseTransferFunctions = struct module CFG = ProcCfg.Normal module Domain = ExecutionDomain - type analysis_data = get_formals ProcData.t + type analysis_data = PulseSummary.t InterproceduralAnalysis.t - let interprocedural_call caller_summary ret call_exp actuals call_loc get_formals astate = + let interprocedural_call {InterproceduralAnalysis.analyze_dependency} ret call_exp actuals + call_loc astate = match proc_name_of_call call_exp with | Some callee_pname when not Config.pulse_intraprocedural_only -> - let formals_opt = get_formals callee_pname in - PulseOperations.call ~caller_summary call_loc callee_pname ~ret ~actuals ~formals_opt astate + let formals_opt = + AnalysisCallbacks.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals + in + let callee_data = analyze_dependency callee_pname in + PulseOperations.call ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt astate | _ -> L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ; PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals @@ -87,7 +92,8 @@ module PulseTransferFunctions = struct Ok exec_state - let dispatch_call tenv summary ret call_exp actuals call_loc flags get_formals astate = + let dispatch_call ({InterproceduralAnalysis.tenv} as analysis_data) ret call_exp actuals call_loc + flags astate = (* evaluate all actuals *) let* astate, rev_func_args = List.fold_result actuals ~init:(astate, []) @@ -113,17 +119,15 @@ module PulseTransferFunctions = struct match model with | Some (model, callee_procname) -> L.d_printfln "Found model for call@\n" ; - model ~caller_summary:summary ~callee_procname call_loc ~ret astate + model analysis_data ~callee_procname call_loc ~ret astate | None -> PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ; let only_actuals_evaled = - List.map - ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} -> (arg_payload, typ)) - func_args + List.map func_args ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} -> + (arg_payload, typ) ) in let r = - interprocedural_call summary ret call_exp only_actuals_evaled call_loc get_formals - astate + interprocedural_call analysis_data ret call_exp only_actuals_evaled call_loc astate in PerfEvent.(log (fun logger -> log_end_event logger ())) ; r @@ -139,8 +143,8 @@ module PulseTransferFunctions = struct exec_state_res - let exec_instr (astate : Domain.t) {tenv; ProcData.summary; extras= get_formals} _cfg_node - (instr : Sil.instr) : Domain.t list = + let exec_instr (astate : Domain.t) ({InterproceduralAnalysis.proc_desc} as analysis_data) + _cfg_node (instr : Sil.instr) : Domain.t list = match astate with | AbortProgram _ -> (* We can also continue the analysis with the error state here @@ -157,7 +161,7 @@ module PulseTransferFunctions = struct let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in PulseOperations.write_id lhs_id rhs_addr_hist astate in - check_error_continue summary result + check_error_continue analysis_data result | Store {e1= lhs_exp; e2= rhs_exp; loc} -> (* [*lhs_exp := rhs_exp] *) let event = ValueHistory.Assignment loc in @@ -171,15 +175,14 @@ module PulseTransferFunctions = struct in match lhs_exp with | Lvar pvar when Pvar.is_return pvar -> - PulseOperations.check_address_escape loc summary.Summary.proc_desc rhs_addr - rhs_history astate + PulseOperations.check_address_escape loc proc_desc rhs_addr rhs_history astate | _ -> Ok astate in - check_error_continue summary result + check_error_continue analysis_data result | Prune (condition, loc, _is_then_branch, _if_kind) -> PulseOperations.prune loc ~condition astate - |> check_error_transform summary ~f:(fun astate -> + |> check_error_transform analysis_data ~f:(fun astate -> if PulseArithmetic.is_unsat_cheap astate then (* [condition] is known to be unsatisfiable: prune path *) [] @@ -187,11 +190,11 @@ module PulseTransferFunctions = struct (* [condition] is true or unknown value: go into the branch *) [Domain.ContinueProgram astate] ) | Call (ret, call_exp, actuals, loc, call_flags) -> - dispatch_call tenv summary ret call_exp actuals loc call_flags get_formals astate - |> check_error_transform summary ~f:(fun id -> id) + dispatch_call analysis_data ret call_exp actuals loc call_flags astate + |> check_error_transform analysis_data ~f:(fun id -> id) | Metadata (ExitScope (vars, location)) -> let astate = PulseOperations.remove_vars vars location astate in - check_error_continue summary astate + check_error_continue analysis_data astate | Metadata (VariableLifetimeBegins (pvar, _, location)) -> [PulseOperations.realloc_pvar pvar location astate |> Domain.continue] | Metadata (Abstract _ | Nullify _ | Skip) -> @@ -229,20 +232,14 @@ let sledge_test_fmt = f ) -let checker {Callbacks.exe_env; summary} = - let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in +let checker ({InterproceduralAnalysis.proc_desc} as analysis_data) = AbstractValue.State.reset () ; - let pdesc = Summary.get_proc_desc summary in - let initial = [ExecutionDomain.mk_initial pdesc] in - let get_formals callee_pname = - Ondemand.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals - in - let proc_data = {ProcData.summary; tenv; extras= get_formals} in - match DisjunctiveAnalyzer.compute_post proc_data ~initial pdesc with + let initial = [ExecutionDomain.mk_initial proc_desc] in + match DisjunctiveAnalyzer.compute_post analysis_data ~initial proc_desc with | Some posts -> - PulsePayload.update_summary (PulseSummary.of_posts pdesc posts) summary + Some (PulseSummary.of_posts proc_desc posts) | None -> - summary + None | exception exn -> (* output sledge replay tests, see comment on [sledge_test_fmt] *) IExn.reraise_if exn ~f:(fun () -> @@ -250,7 +247,8 @@ let checker {Callbacks.exe_env; summary} = | List [exn; replay] -> let exn = Error.t_of_sexp exn in L.internal_error "Analysis of %a FAILED:@\n@[%a@]@\n" Procname.pp - (Procdesc.get_proc_name pdesc) Error.pp exn ; + (Procdesc.get_proc_name proc_desc) + Error.pp exn ; F.fprintf (Lazy.force sledge_test_fmt) "@\n\ \ let%%expect_test _ =@\n\ @@ -264,7 +262,7 @@ let checker {Callbacks.exe_env; summary} = | _ | (exception _) -> (* re-raise original exception *) true ) ; - summary + None let () = Sledge.Timer.enabled := Config.sledge_timers diff --git a/infer/src/pulse/Pulse.mli b/infer/src/pulse/Pulse.mli index 949618830..8bc0a3546 100644 --- a/infer/src/pulse/Pulse.mli +++ b/infer/src/pulse/Pulse.mli @@ -4,6 +4,7 @@ * This source code is licensed under the MIT license found in the * LICENSE file in the root directory of this source tree. *) + open! IStd -val checker : Callbacks.proc_callback_args -> Summary.t +val checker : PulseSummary.t InterproceduralAnalysis.t -> PulseSummary.t option diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index a11684e96..b597c6888 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -12,7 +12,7 @@ open PulseDomainInterface type arg_payload = AbstractValue.t * ValueHistory.t type model = - caller_summary:Summary.t + PulseSummary.t InterproceduralAnalysis.t -> callee_procname:Procname.t -> Location.t -> ret:Ident.t * Typ.t @@ -21,7 +21,7 @@ type model = module Misc = struct let shallow_copy model_desc dest_pointer_hist src_pointer_hist : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in let* astate, obj = PulseOperations.eval_access location src_pointer_hist Dereference astate in let* astate, obj_copy = PulseOperations.shallow_copy location obj astate in @@ -35,12 +35,11 @@ module Misc = struct let early_exit : model = - fun ~caller_summary:_ ~callee_procname:_ _ ~ret:_ astate -> - Ok [ExecutionDomain.ExitProgram astate] + fun _ ~callee_procname:_ _ ~ret:_ astate -> Ok [ExecutionDomain.ExitProgram astate] let return_int : Int64.t -> model = - fun i64 ~caller_summary:_ ~callee_procname:_ _location ~ret:(ret_id, _) astate -> + fun i64 _ ~callee_procname:_ _location ~ret:(ret_id, _) astate -> let i = IntLit.of_int64 i64 in let ret_addr = AbstractValue.Constants.get_int i in let astate = PulseArithmetic.and_eq_int ret_addr i astate in @@ -48,30 +47,28 @@ module Misc = struct let return_unknown_size : model = - fun ~caller_summary:_ ~callee_procname:_ _location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname:_ _location ~ret:(ret_id, _) astate -> let ret_addr = AbstractValue.mk_fresh () in let astate = PulseArithmetic.and_nonnegative ret_addr astate in PulseOperations.write_id ret_id (ret_addr, []) astate |> PulseOperations.ok_continue - let skip : model = - fun ~caller_summary:_ ~callee_procname:_ _ ~ret:_ astate -> PulseOperations.ok_continue astate - + let skip : model = fun _ ~callee_procname:_ _ ~ret:_ astate -> PulseOperations.ok_continue astate let nondet ~fn_name : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model fn_name; location; in_call= []} in PulseOperations.havoc_id ret_id [event] astate |> PulseOperations.ok_continue let id_first_arg arg_access_hist : model = - fun ~caller_summary:_ ~callee_procname:_ _ ~ret astate -> + fun _ ~callee_procname:_ _ ~ret astate -> PulseOperations.write_id (fst ret) arg_access_hist astate |> PulseOperations.ok_continue end module C = struct let free deleted_access : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> + fun _ ~callee_procname:_ location ~ret:_ astate -> (* NOTE: we could introduce a case-split explicitly on =0 vs ≠0 but instead only act on what we currently know about the value. This is purely to avoid contributing to path explosion. *) (* freeing 0 is a no-op *) @@ -84,7 +81,7 @@ module C = struct let malloc _ : model = - fun ~caller_summary:_ ~callee_procname location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname location ~ret:(ret_id, _) astate -> let ret_addr = AbstractValue.mk_fresh () in let ret_value = (ret_addr, [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}]) @@ -102,7 +99,7 @@ module C = struct let malloc_not_null _ : model = - fun ~caller_summary:_ ~callee_procname location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname location ~ret:(ret_id, _) astate -> let ret_addr = AbstractValue.mk_fresh () in let ret_value = (ret_addr, [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}]) @@ -114,14 +111,14 @@ module C = struct let cf_bridging_release access : model = - fun ~caller_summary:_ ~callee_procname:_ _ ~ret:(ret_id, _) astate -> + fun _ ~callee_procname:_ _ ~ret:(ret_id, _) astate -> let astate = PulseOperations.write_id ret_id access astate in PulseOperations.remove_allocation_attr (fst access) astate |> PulseOperations.ok_continue end module Cplusplus = struct let delete deleted_access : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> + fun _ ~callee_procname:_ location ~ret:_ astate -> let+ astate = PulseOperations.invalidate location Invalidation.CppDelete deleted_access astate in @@ -129,7 +126,7 @@ module Cplusplus = struct let placement_new actuals : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "()"; location; in_call= []} in ( match List.rev actuals with | ProcnameDispatcher.Call.FuncArg.{arg_payload= address, hist} :: _ -> @@ -156,7 +153,7 @@ module StdAtomicInteger = struct let constructor this_address init_value : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> + fun _ ~callee_procname:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model "std::atomic::atomic()"; location; in_call= []} in let this = (AbstractValue.mk_fresh (), [event]) in let* astate, int_field = @@ -181,7 +178,7 @@ module StdAtomicInteger = struct let fetch_add this (increment, _) _memory_ordering : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::fetch_add()"; location; in_call= []} in let+ astate = arith_bop `Post location event ret_id (PlusA None) this (AbstractValueOperand increment) @@ -191,7 +188,7 @@ module StdAtomicInteger = struct let fetch_sub this (increment, _) _memory_ordering : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::fetch_sub()"; location; in_call= []} in let+ astate = arith_bop `Post location event ret_id (MinusA None) this (AbstractValueOperand increment) @@ -201,7 +198,7 @@ module StdAtomicInteger = struct let operator_plus_plus_pre this : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::operator++()"; location; in_call= []} in let+ astate = arith_bop `Pre location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate @@ -210,7 +207,7 @@ module StdAtomicInteger = struct let operator_plus_plus_post this _int : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::operator++(T)"; location; in_call= []} in @@ -221,7 +218,7 @@ module StdAtomicInteger = struct let operator_minus_minus_pre this : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::operator--()"; location; in_call= []} in let+ astate = arith_bop `Pre location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate @@ -230,7 +227,7 @@ module StdAtomicInteger = struct let operator_minus_minus_post this _int : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::operator--(T)"; location; in_call= []} in @@ -241,7 +238,7 @@ module StdAtomicInteger = struct let load_instr model_desc this _memory_ordering_opt : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in let+ astate, _int_addr, (int, hist) = load_backing_int location this astate in let astate = PulseOperations.write_id ret_id (int, event :: hist) astate in @@ -261,14 +258,14 @@ module StdAtomicInteger = struct let store this_address (new_value, new_hist) _memory_ordering : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> + fun _ ~callee_procname:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model "std::atomic::store()"; location; in_call= []} in let+ astate = store_backing_int location this_address (new_value, event :: new_hist) astate in [ExecutionDomain.ContinueProgram astate] let exchange this_address (new_value, new_hist) _memory_ordering : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::exchange()"; location; in_call= []} in let* astate, _int_addr, (old_int, old_hist) = load_backing_int location this_address astate in let+ astate = store_backing_int location this_address (new_value, event :: new_hist) astate in @@ -279,7 +276,7 @@ end module JavaObject = struct (* naively modeled as shallow copy. *) let clone src_pointer_hist : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "Object.clone"; location; in_call= []} in let* astate, obj = PulseOperations.eval_access location src_pointer_hist Dereference astate in let+ astate, obj_copy = PulseOperations.shallow_copy location obj astate in @@ -301,7 +298,7 @@ module StdBasicString = struct let data this_hist : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::basic_string::data()"; location; in_call= []} in let* astate, string_addr_hist = to_internal_string location this_hist astate in let+ astate, (string, hist) = @@ -312,7 +309,7 @@ module StdBasicString = struct let destructor this_hist : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> + fun _ ~callee_procname:_ location ~ret:_ astate -> let model = CallEvent.Model "std::basic_string::~basic_string()" in let call_event = ValueHistory.Call {f= model; location; in_call= []} in let* astate, (string_addr, string_hist) = to_internal_string location this_hist astate in @@ -326,7 +323,7 @@ end module StdFunction = struct let operator_call lambda_ptr_hist actuals : model = - fun ~caller_summary ~callee_procname:_ location ~ret astate -> + fun {analyze_dependency} ~callee_procname:_ location ~ret astate -> let havoc_ret (ret_id, _) astate = let event = ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} in [PulseOperations.havoc_id ret_id [event] astate] @@ -344,8 +341,9 @@ module StdFunction = struct List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} -> (arg_payload, typ) ) in - PulseOperations.call ~caller_summary location callee_proc_name ~ret ~actuals - ~formals_opt:None astate + PulseOperations.call + ~callee_data:(analyze_dependency callee_proc_name) + location callee_proc_name ~ret ~actuals ~formals_opt:None astate end module GenericArrayBackedCollection = struct @@ -384,7 +382,7 @@ module GenericArrayBackedCollectionIterator = struct let constructor ~desc this init : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> + fun _ ~callee_procname:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let* astate, (arr_addr, arr_hist) = GenericArrayBackedCollection.eval location init astate in let* astate = @@ -399,7 +397,7 @@ module GenericArrayBackedCollectionIterator = struct >>| ExecutionDomain.continue >>| List.return - let operator_star ~desc iter ~caller_summary:_ ~callee_procname:_ location ~ret astate = + let operator_star ~desc iter _ ~callee_procname:_ location ~ret astate = let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let* astate, (iter_index_addr, iter_index_hist) = to_internal_pointer location iter astate in let+ astate, (elem_val, _) = @@ -409,7 +407,7 @@ module GenericArrayBackedCollectionIterator = struct [ExecutionDomain.ContinueProgram astate] - let operator_plus_plus ~desc iter ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate = + let operator_plus_plus ~desc iter _ ~callee_procname:_ location ~ret:_ astate = let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let index_next = AbstractValue.mk_fresh () in let* astate, (current_index, current_index_hist) = to_internal_pointer location iter astate in @@ -435,8 +433,7 @@ module StdVector = struct >>= PulseOperations.havoc_field location vector GenericArrayBackedCollection.field trace - let init_list_constructor this init_list ~caller_summary:_ ~callee_procname:_ location ~ret:_ - astate = + let init_list_constructor this init_list _ ~callee_procname:_ location ~ret:_ astate = let event = ValueHistory.Call {f= Model "std::vector::vector()"; location; in_call= []} in let* astate, init_copy = PulseOperations.shallow_copy location init_list astate in let+ astate = @@ -448,7 +445,7 @@ module StdVector = struct let invalidate_references vector_f vector : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> + fun _ ~callee_procname:_ location ~ret:_ astate -> let crumb = ValueHistory.Call { f= Model (Format.asprintf "%a()" Invalidation.pp_std_vector_function vector_f) @@ -460,7 +457,7 @@ module StdVector = struct let at ~desc vector index : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret astate -> + fun _ ~callee_procname:_ location ~ret astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let+ astate, (addr, hist) = GenericArrayBackedCollection.element location vector (fst index) astate @@ -470,7 +467,7 @@ module StdVector = struct let vector_begin vector iter : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> + fun _ ~callee_procname:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model "std::vector::begin()"; location; in_call= []} in let index_zero = AbstractValue.mk_fresh () in let astate = PulseArithmetic.and_eq_int index_zero IntLit.zero astate in @@ -488,7 +485,7 @@ module StdVector = struct let reserve vector : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> + fun _ ~callee_procname:_ location ~ret:_ astate -> let crumb = ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []} in reallocate_internal_array [crumb] vector Reserve location astate >>| AddressAttributes.std_vector_reserve (fst vector) @@ -496,7 +493,7 @@ module StdVector = struct let push_back vector : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret:_ astate -> + fun _ ~callee_procname:_ location ~ret:_ astate -> let crumb = ValueHistory.Call {f= Model "std::vector::push_back()"; location; in_call= []} in if AddressAttributes.is_std_vector_reserved (fst vector) astate then (* assume that any call to [push_back] is ok after one called [reserve] on the same vector @@ -510,7 +507,7 @@ end module JavaCollection = struct let set coll index new_elem : model = - fun ~caller_summary:_ ~callee_procname:_ location ~ret astate -> + fun _ ~callee_procname:_ location ~ret astate -> let event = ValueHistory.Call {f= Model "Collection.set"; location; in_call= []} in let* astate, ((old_addr, old_hist) as old_elem) = GenericArrayBackedCollection.element location coll (fst index) astate diff --git a/infer/src/pulse/PulseModels.mli b/infer/src/pulse/PulseModels.mli index dac286a70..6ed8aebb3 100644 --- a/infer/src/pulse/PulseModels.mli +++ b/infer/src/pulse/PulseModels.mli @@ -9,7 +9,7 @@ open PulseBasicInterface open PulseDomainInterface type model = - caller_summary:Summary.t + PulseSummary.t InterproceduralAnalysis.t -> callee_procname:Procname.t -> Location.t -> ret:Ident.t * Typ.t diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 84c4aff0c..d40f342ae 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -442,9 +442,9 @@ let apply_callee callee_pname call_loc callee_exec_state ~ret ~formals ~actuals apply astate ~f:(fun astate -> ExitProgram astate) -let call ~caller_summary call_loc callee_pname ~ret ~actuals ~formals_opt - (astate : AbductiveDomain.t) : (ExecutionDomain.t list, Diagnostic.t * t) result = - match PulsePayload.read_full ~caller_summary ~callee_pname with +let call ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) + : (ExecutionDomain.t list, Diagnostic.t * t) result = + match callee_data with | Some (callee_proc_desc, exec_states) -> let formals = Procdesc.get_formals callee_proc_desc diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 0b5754075..f512ee44d 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -106,7 +106,7 @@ val check_address_escape : Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t access_result val call : - caller_summary:Summary.t + callee_data:(Procdesc.t * PulseSummary.t) option -> Location.t -> Procname.t -> ret:Ident.t * Typ.t diff --git a/infer/src/pulse/PulsePayload.ml b/infer/src/pulse/PulsePayload.ml deleted file mode 100644 index 241ec9aa0..000000000 --- a/infer/src/pulse/PulsePayload.ml +++ /dev/null @@ -1,14 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd - -include SummaryPayload.Make (struct - type nonrec t = PulseSummary.t - - let field = Payloads.Fields.pulse -end) diff --git a/infer/src/pulse/PulsePayload.mli b/infer/src/pulse/PulsePayload.mli deleted file mode 100644 index fb002744f..000000000 --- a/infer/src/pulse/PulsePayload.mli +++ /dev/null @@ -1,10 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -open! IStd - -include SummaryPayload.S with type t = PulseSummary.t