From f5fef60a42f53e667dfeb3b9a87908f2e5310e14 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 28 Apr 2021 04:47:17 -0700 Subject: [PATCH] [pulse] refactor arguments of models into a record Summary: This looks a bit better as it makes it easier to ignore parts of the arguments in models, which happens all the time. Also easier to add more to the record in the future, which is the real reason. Reviewed By: skcho Differential Revision: D27997695 fbshipit-source-id: a7c680025 --- infer/src/pulse/Pulse.ml | 2 +- infer/src/pulse/PulseModels.ml | 150 ++++++++++++++++---------------- infer/src/pulse/PulseModels.mli | 14 +-- 3 files changed, 83 insertions(+), 83 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index b008e27e4..f029d8a88 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -166,7 +166,7 @@ module PulseTransferFunctions = struct in PulseCallOperations.conservatively_initialize_args arg_values astate in - model analysis_data ~callee_procname call_loc ~ret astate + model {analysis_data; callee_procname; location= call_loc; ret} astate | None -> PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ; let only_actuals_evaled = diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 60c00a5f0..b7f569c05 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -12,13 +12,13 @@ open PulseOperations.Import type arg_payload = AbstractValue.t * ValueHistory.t -type model = - PulseSummary.t InterproceduralAnalysis.t - -> callee_procname:Procname.t - -> Location.t - -> ret:Ident.t * Typ.t - -> AbductiveDomain.t - -> ExecutionDomain.t AccessResult.t list +type model_data = + { analysis_data: PulseSummary.t InterproceduralAnalysis.t + ; callee_procname: Procname.t + ; location: Location.t + ; ret: Ident.t * Typ.t } + +type model = model_data -> AbductiveDomain.t -> ExecutionDomain.t AccessResult.t list let ok_continue post = [Ok (ContinueProgram post)] @@ -43,13 +43,13 @@ module Misc = struct let shallow_copy_model model_desc dest_pointer_hist src_pointer_hist : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in shallow_copy location event ret_id dest_pointer_hist src_pointer_hist astate let early_exit : model = - fun {tenv; proc_desc} ~callee_procname:_ _ ~ret:_ astate -> + fun {analysis_data= {tenv; proc_desc}} astate -> let open SatUnsat.Import in match AbductiveDomain.summary_of_post tenv proc_desc astate >>| AccessResult.of_abductive_result @@ -63,7 +63,7 @@ module Misc = struct let return_int : Int64.t -> model = - fun i64 _ ~callee_procname:_ _location ~ret:(ret_id, _) astate -> + fun i64 {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 @@ -71,7 +71,7 @@ module Misc = struct let return_positive ~desc : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let ret_addr = AbstractValue.mk_fresh () in let ret_value = (ret_addr, [event]) in @@ -80,7 +80,7 @@ module Misc = struct let return_unknown_size : model = - fun _ ~callee_procname:_ _location ~ret:(ret_id, _) astate -> + fun {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 @@ -90,7 +90,7 @@ module Misc = struct don't have the implementation. This triggers a bunch of heuristics, e.g. to havoc arguments we suspect are passed by reference. *) let unknown_call skip_reason args : model = - fun {tenv} ~callee_procname location ~ret astate -> + fun {analysis_data= {tenv}; callee_procname; location; ret} astate -> let actuals = List.map args ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload= actual; typ} -> (actual, typ) ) @@ -109,20 +109,20 @@ module Misc = struct let skip = unknown_call let nondet ~fn_name : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model fn_name; location; in_call= []} in PulseOperations.havoc_id ret_id [event] astate |> ok_continue let id_first_arg ~desc (arg_value, arg_history) : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let ret_value = (arg_value, event :: arg_history) in PulseOperations.write_id ret_id ret_value astate |> ok_continue let free_or_delete operation deleted_access : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} astate -> (* NOTE: freeing 0 is a no-op so we introduce a case split *) let invalidation = match operation with `Free -> Invalidation.CFree | `Delete -> Invalidation.CppDelete @@ -143,7 +143,7 @@ module Misc = struct let alloc_not_null ~event arg : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let ret_addr = AbstractValue.mk_fresh () in let event = event location in let ret_value = (ret_addr, [event]) in @@ -177,7 +177,7 @@ module C = struct let malloc_common ~size_exp_opt : model = - fun {tenv} ~callee_procname location ~ret:(ret_id, _) astate -> + fun {analysis_data= {tenv}; 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}]) @@ -199,7 +199,7 @@ module C = struct let malloc_not_null_common ~size_exp_opt : model = - fun {tenv} ~callee_procname location ~ret:(ret_id, _) astate -> + fun {analysis_data= {tenv}; 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}]) @@ -224,7 +224,7 @@ end module ObjCCoreFoundation = struct let cf_bridging_release access : model = - fun _ ~callee_procname:_ _ ~ret:(ret_id, _) astate -> + fun {ret= ret_id, _} astate -> let astate = PulseOperations.write_id ret_id access astate in PulseOperations.remove_allocation_attr (fst access) astate |> ok_continue end @@ -237,7 +237,7 @@ module ObjC = struct let dispatch_sync args : model = - fun {analyze_dependency; tenv; proc_desc} ~callee_procname:_ location ~ret astate -> + fun {analysis_data= {analyze_dependency; tenv; proc_desc}; location; ret} astate -> match List.last args with | None -> ok_continue astate @@ -281,7 +281,7 @@ module Optional = struct let assign_none this ~desc : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} astate -> let<*> astate, value = assign_value_fresh location this ~desc astate in let<*> astate = PulseArithmetic.and_eq_int (fst value) IntLit.zero astate in let<+> astate = PulseOperations.invalidate location Invalidation.OptionalEmpty value astate in @@ -289,7 +289,7 @@ module Optional = struct let assign_value this _value ~desc : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} astate -> (* TODO: call the copy constructor of a value *) let<*> astate, value = assign_value_fresh location this ~desc astate in let<+> astate = PulseArithmetic.and_positive (fst value) astate in @@ -297,20 +297,20 @@ module Optional = struct let assign_optional_value this init ~desc : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} astate -> let<*> astate, value = to_internal_value_deref Read location init astate in let<+> astate, _ = write_value location this ~value ~desc astate in astate let emplace optional ~desc : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} astate -> let<+> astate, _ = assign_value_fresh location optional ~desc astate in astate let value optional ~desc : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let<*> astate, ((value_addr, value_hist) as value) = to_internal_value_deref Write location optional astate @@ -321,7 +321,7 @@ module Optional = struct let has_value optional ~desc : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let ret_addr = AbstractValue.mk_fresh () in let ret_value = (ret_addr, [ValueHistory.Call {f= Model desc; location; in_call= []}]) in let<*> astate, (value_addr, _) = to_internal_value_deref Read location optional astate in @@ -334,7 +334,7 @@ module Optional = struct let get_pointer optional ~desc : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let<*> astate, value_addr = to_internal_value_deref Read location optional astate in let value_update_hist = (fst value_addr, event :: snd value_addr) in @@ -353,7 +353,7 @@ module Optional = struct let value_or optional default ~desc : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let<*> astate, value_addr = to_internal_value_deref Read location optional astate in let<*> astate_non_empty = PulseArithmetic.prune_positive (fst value_addr) astate in @@ -375,7 +375,7 @@ module Cplusplus = struct let delete deleted_access : model = Misc.free_or_delete `Delete deleted_access let placement_new actuals : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {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} :: _ -> @@ -402,7 +402,7 @@ module StdAtomicInteger = struct let constructor this_address init_value : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} 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 = @@ -427,7 +427,7 @@ module StdAtomicInteger = struct let fetch_add this (increment, _) _memory_ordering : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {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) @@ -437,7 +437,7 @@ module StdAtomicInteger = struct let fetch_sub this (increment, _) _memory_ordering : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {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) @@ -447,7 +447,7 @@ module StdAtomicInteger = struct let operator_plus_plus_pre this : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {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 @@ -456,7 +456,7 @@ module StdAtomicInteger = struct let operator_plus_plus_post this _int : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model "std::atomic::operator++(T)"; location; in_call= []} in @@ -467,7 +467,7 @@ module StdAtomicInteger = struct let operator_minus_minus_pre this : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {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 @@ -476,7 +476,7 @@ module StdAtomicInteger = struct let operator_minus_minus_post this _int : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model "std::atomic::operator--(T)"; location; in_call= []} in @@ -487,7 +487,7 @@ module StdAtomicInteger = struct let load_instr model_desc this _memory_ordering_opt : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {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 PulseOperations.write_id ret_id (int, event :: hist) astate @@ -511,14 +511,14 @@ module StdAtomicInteger = struct let store this_address (new_value, new_hist) _memory_ordering : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} 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 astate let exchange this_address (new_value, new_hist) _memory_ordering : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {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 @@ -528,7 +528,7 @@ end module JavaObject = struct (* naively modeled as shallow copy. *) let clone src_pointer_hist : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model "Object.clone"; location; in_call= []} in let<*> astate, obj = PulseOperations.eval_access Read location src_pointer_hist Dereference astate @@ -551,7 +551,7 @@ module StdBasicString = struct let data this_hist : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {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) = @@ -561,7 +561,7 @@ module StdBasicString = struct let destructor this_hist : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} 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 @@ -576,7 +576,7 @@ end module StdFunction = struct let operator_call ProcnameDispatcher.Call.FuncArg.{arg_payload= lambda_ptr_hist; typ} actuals : model = - fun {analyze_dependency; tenv; proc_desc} ~callee_procname:_ location ~ret astate -> + fun {analysis_data= {analyze_dependency; tenv; proc_desc}; 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] @@ -601,7 +601,7 @@ module StdFunction = struct let assign dest ProcnameDispatcher.Call.FuncArg.{arg_payload= src; typ= src_typ} ~desc : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in if PulseArithmetic.is_known_zero astate (fst src) then let empty_target = AbstractValue.mk_fresh () in @@ -709,14 +709,14 @@ module GenericArrayBackedCollectionIterator = struct let constructor ~desc this init : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let<+> astate = construct location event ~init ~ref:this astate in astate let operator_compare comparison ~desc iter_lhs iter_rhs : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let<*> astate, _, (index_lhs, _) = to_internal_pointer_deref Read location iter_lhs astate in let<*> astate, _, (index_rhs, _) = to_internal_pointer_deref Read location iter_rhs astate in @@ -743,14 +743,14 @@ module GenericArrayBackedCollectionIterator = struct let operator_star ~desc iter : model = - fun _ ~callee_procname:_ location ~ret astate -> + fun {location; ret} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let<+> astate, pointer, (elem, _) = to_elem_pointed_by_iterator Read location iter astate in PulseOperations.write_id (fst ret) (elem, event :: snd pointer) astate let operator_step step ~desc iter : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let index_new = AbstractValue.mk_fresh () in let<*> astate, pointer, _ = @@ -766,7 +766,7 @@ end module JavaIterator = struct let constructor ~desc init : model = - fun _ ~callee_procname:_ location ~ret astate -> + fun {location; ret} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let ref = (AbstractValue.mk_fresh (), [event]) in let<+> astate = @@ -777,7 +777,7 @@ module JavaIterator = struct (* {curr -> v_c} is modified to {curr -> v_fresh} and returns array[v_c] *) let next ~desc iter : model = - fun _ ~callee_procname:_ location ~ret astate -> + fun {location; ret} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let new_index = AbstractValue.mk_fresh () in let<*> astate, (curr_index, curr_index_hist) = @@ -797,7 +797,7 @@ module JavaIterator = struct (* {curr -> v_c } is modified to {curr -> v_fresh} and writes to array[v_c] *) let remove ~desc iter : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let new_index = AbstractValue.mk_fresh () in let<*> astate, (curr_index, curr_index_hist) = @@ -831,7 +831,7 @@ module StdVector = struct let init_list_constructor this init_list : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} 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 = @@ -843,7 +843,7 @@ module StdVector = struct let invalidate_references vector_f vector : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} astate -> let crumb = ValueHistory.Call { f= Model (Format.asprintf "%a()" Invalidation.pp_std_vector_function vector_f) @@ -855,7 +855,7 @@ module StdVector = struct let at ~desc vector index : model = - fun _ ~callee_procname:_ location ~ret astate -> + fun {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 @@ -864,7 +864,7 @@ module StdVector = struct let vector_begin vector iter : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} astate -> let event = ValueHistory.Call {f= Model "std::vector::begin()"; location; in_call= []} in let pointer_hist = event :: snd iter in let pointer_val = (AbstractValue.mk_fresh (), pointer_hist) in @@ -885,7 +885,7 @@ module StdVector = struct let vector_end vector iter : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} astate -> let event = ValueHistory.Call {f= Model "std::vector::end()"; location; in_call= []} in let<*> astate, (arr_addr, _) = GenericArrayBackedCollection.eval Read location vector astate in let<*> astate, (pointer_addr, _) = @@ -905,7 +905,7 @@ module StdVector = struct let reserve vector : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} astate -> let crumb = ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []} in let<+> astate = reallocate_internal_array [crumb] vector Reserve location astate @@ -915,7 +915,7 @@ module StdVector = struct let push_back vector : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} 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 @@ -928,7 +928,7 @@ module StdVector = struct let empty vector : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let crumb = ValueHistory.Call {f= Model "std::vector::empty()"; location; in_call= []} in let<+> astate, (value_addr, value_hist) = GenericArrayBackedCollection.eval_is_empty location vector astate @@ -959,7 +959,7 @@ module Java = struct let instance_of (argv, hist) typeexpr : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model "Java.instanceof"; location; in_call= []} in let res_addr = AbstractValue.mk_fresh () in match typeexpr with @@ -986,7 +986,7 @@ module JavaCollection = struct let init ~desc this : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let fresh_val = (AbstractValue.mk_fresh (), [event]) in let is_empty_value = AbstractValue.mk_fresh () in @@ -1007,7 +1007,7 @@ module JavaCollection = struct let add ~desc coll new_elem : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let ret_value = AbstractValue.mk_fresh () in let<*> astate, coll_val = PulseOperations.eval_access Read location coll Dereference astate in @@ -1061,7 +1061,7 @@ module JavaCollection = struct let set coll _ (new_val, new_val_hist) : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model "Collection.set()"; location; in_call= []} in let<*> astates = update coll new_val new_val_hist event location ret_id astate in List.map ~f:(fun astate -> Ok (ContinueProgram astate)) astates @@ -1120,7 +1120,7 @@ module JavaCollection = struct let remove ~desc args : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> match args with | [ {ProcnameDispatcher.Call.FuncArg.arg_payload= coll_arg} ; {ProcnameDispatcher.Call.FuncArg.arg_payload= elem_arg; typ} ] -> @@ -1139,7 +1139,7 @@ module JavaCollection = struct let is_empty ~desc coll : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let<*> astate, coll_val = PulseOperations.eval_access Read location coll Dereference astate in let<*> astate, _, (is_empty_val, hist) = @@ -1149,7 +1149,7 @@ module JavaCollection = struct let clear ~desc coll : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let null_val = AbstractValue.mk_fresh () in let is_empty_val = AbstractValue.mk_fresh () in @@ -1208,7 +1208,7 @@ module JavaCollection = struct let get ~desc coll (elem, _) : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let<*> astate, coll_val = PulseOperations.eval_access Read location coll Dereference astate in let<*> astate, _, (is_empty_val, _) = Java.load_field is_empty_field location coll_val astate in @@ -1247,14 +1247,14 @@ module JavaInteger = struct let init this_address init_value : model = - fun _ ~callee_procname:_ location ~ret:_ astate -> + fun {location} astate -> let event = ValueHistory.Call {f= Model "Integer.init"; location; in_call= []} in let<+> astate = construct this_address init_value event location astate in astate let equals this arg : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let<*> astate, _int_addr1, (int1, hist) = load_backing_int location this astate in let<*> astate, _int_addr2, (int2, _) = load_backing_int location arg astate in let binop_addr = AbstractValue.mk_fresh () in @@ -1266,13 +1266,13 @@ module JavaInteger = struct let int_val this : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let<*> astate, _int_addr1, int_value_hist = load_backing_int location this astate in PulseOperations.write_id ret_id int_value_hist astate |> ok_continue let value_of init_value : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model "Integer.valueOf"; location; in_call= []} in let new_alloc = (AbstractValue.mk_fresh (), [event]) in let<+> astate = construct new_alloc init_value event location astate in @@ -1281,21 +1281,21 @@ end module JavaPreconditions = struct let check_not_null (address, hist) : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model "Preconditions.checkNotNull"; location; in_call= []} in let<+> astate = PulseArithmetic.prune_positive address astate in PulseOperations.write_id ret_id (address, event :: hist) astate let check_state_argument (address, _) : model = - fun _ ~callee_procname:_ _ ~ret:_ astate -> + fun _ astate -> let<+> astate = PulseArithmetic.prune_positive address astate in astate end module Android = struct let text_utils_is_empty ~desc (address, hist) : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + fun {location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let ret_val = AbstractValue.mk_fresh () in let astate = PulseOperations.write_id ret_id (ret_val, event :: hist) astate in diff --git a/infer/src/pulse/PulseModels.mli b/infer/src/pulse/PulseModels.mli index 3844cd92a..6f60702d7 100644 --- a/infer/src/pulse/PulseModels.mli +++ b/infer/src/pulse/PulseModels.mli @@ -8,13 +8,13 @@ open! IStd open PulseBasicInterface open PulseDomainInterface -type model = - PulseSummary.t InterproceduralAnalysis.t - -> callee_procname:Procname.t - -> Location.t - -> ret:Ident.t * Typ.t - -> AbductiveDomain.t - -> ExecutionDomain.t AccessResult.t list +type model_data = + { analysis_data: PulseSummary.t InterproceduralAnalysis.t + ; callee_procname: Procname.t + ; location: Location.t + ; ret: Ident.t * Typ.t } + +type model = model_data -> AbductiveDomain.t -> ExecutionDomain.t AccessResult.t list val dispatch : Tenv.t