From 1f6b9edacc57f1d5099f377c95a3c89ec1dc1943 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 1 Feb 2021 11:57:45 -0800 Subject: [PATCH] [pulse] do not short-circuit valid paths because of errors Summary: Change most `t list access_result` to `t access_result list` so that the Ok/Error is individual to each result in the list instead of having only a toplevel Ok/Error affecting the whole list. To make it not horrible to write this introduces new "monadic" operators `let<*>` and `let<+>`. They are not entirely satisfactory but perhaps it's just a notation issue as they are not quite bind/map operators unlike what their notation might suggest. I'd say good enough for now. The type change induced quite the churn but the new operators simplify the code overall. Reviewed By: skcho Differential Revision: D26150505 fbshipit-source-id: 33764fae3 --- infer/src/pulse/Pulse.ml | 80 +++-- infer/src/pulse/PulseExecutionDomain.ml | 55 ++-- infer/src/pulse/PulseExecutionDomain.mli | 2 +- infer/src/pulse/PulseModels.ml | 378 +++++++++++------------ infer/src/pulse/PulseModels.mli | 2 +- infer/src/pulse/PulseOperations.ml | 46 ++- infer/src/pulse/PulseOperations.mli | 49 ++- 7 files changed, 332 insertions(+), 280 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 7d32152b3..084929e3c 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -8,10 +8,10 @@ open! IStd module F = Format module L = Logging -open IResult.Let_syntax module IRAttributes = Attributes open PulseBasicInterface open PulseDomainInterface +open PulseOperations.Import let exec_list_of_list_result = function | Ok posts -> @@ -24,17 +24,27 @@ let exec_list_of_list_result = function let report_on_error {InterproceduralAnalysis.proc_desc; tenv; err_log} result = PulseReport.report_error proc_desc tenv err_log result - >>| List.map ~f:(fun post -> ExecutionDomain.ContinueProgram post) + >>| List.map ~f:(fun post -> ContinueProgram post) |> exec_list_of_list_result -let report_on_error_list {InterproceduralAnalysis.proc_desc; tenv; err_log} result = - PulseReport.report_error proc_desc tenv err_log result |> exec_list_of_list_result +let post_of_report_result = function + | Ok post -> + Some post + | Error Unsat -> + None + | Error (Sat post) -> + Some post + + +let report_on_error_list {InterproceduralAnalysis.proc_desc; tenv; err_log} results = + List.filter_map results ~f:(fun exec_result -> + PulseReport.report_error proc_desc tenv err_log exec_result |> post_of_report_result ) let report_topl_errors proc_desc err_log summary = let f = function - | ExecutionDomain.ContinueProgram astate -> + | ContinueProgram astate -> PulseTopl.report_errors proc_desc err_log (AbductiveDomain.Topl.get astate) | _ -> () @@ -60,24 +70,24 @@ module PulseTransferFunctions = struct AnalysisCallbacks.proc_resolve_attributes pname |> Option.map ~f:ProcAttributes.get_pvar_formals - let interprocedural_call {InterproceduralAnalysis.analyze_dependency; proc_desc; tenv; err_log} - ret callee_pname call_exp actuals call_loc astate = + let interprocedural_call {InterproceduralAnalysis.analyze_dependency; proc_desc} ret callee_pname + call_exp actuals call_loc astate = match callee_pname with | Some callee_pname when not Config.pulse_intraprocedural_only -> let formals_opt = get_pvar_formals callee_pname in let callee_data = analyze_dependency callee_pname in - PulseOperations.call ~caller_proc_desc:proc_desc tenv err_log ~callee_data call_loc - callee_pname ~ret ~actuals ~formals_opt astate + PulseOperations.call ~caller_proc_desc:proc_desc ~callee_data call_loc callee_pname ~ret + ~actuals ~formals_opt astate | _ -> L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ; let astate = let arg_values = List.map actuals ~f:(fun ((value, _), _) -> value) in PulseOperations.conservatively_initialize_args arg_values astate in - Ok - [ Domain.ContinueProgram - (PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals - ~formals_opt:None astate) ] + [ Ok + (ContinueProgram + (PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals + ~formals_opt:None astate)) ] (** has an object just gone out of scope? *) @@ -126,7 +136,7 @@ module PulseTransferFunctions = struct | ISLLatentMemoryError _ | AbortProgram _ | LatentAbortProgram _ | ExitProgram _ -> exec_state in - Result.map ~f:(List.map ~f:do_one_exec_state) exec_state_res + List.map ~f:(Result.map ~f:do_one_exec_state) exec_state_res let topl_store_step loc ~lhs ~rhs:_ astate = @@ -145,7 +155,7 @@ module PulseTransferFunctions = struct let dispatch_call ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data) ret call_exp actuals call_loc flags astate = (* evaluate all actuals *) - let* astate, rev_func_args = + let<*> astate, rev_func_args = List.fold_result actuals ~init:(astate, []) ~f:(fun (astate, rev_func_args) (actual_exp, actual_typ) -> let+ astate, actual_evaled = PulseOperations.eval Read call_loc actual_exp astate in @@ -166,7 +176,7 @@ module PulseTransferFunctions = struct None in (* do interprocedural call then destroy objects going out of scope *) - let exec_state_res = + let exec_states_res = match model with | Some (model, callee_procname) -> L.d_printfln "Found model for call@\n" ; @@ -191,29 +201,33 @@ module PulseTransferFunctions = struct PerfEvent.(log (fun logger -> log_end_event logger ())) ; r in - let exec_state_res = + let exec_states_res = if Topl.is_deep_active () then match callee_pname with | Some callee_pname -> - topl_small_step call_loc callee_pname func_args ret exec_state_res + topl_small_step call_loc callee_pname func_args ret exec_states_res | None -> - (* skip, as above for non-topl *) exec_state_res - else exec_state_res + (* skip, as above for non-topl *) exec_states_res + else exec_states_res in - let+ exec_state = + let exec_states_res = match get_out_of_scope_object callee_pname actuals flags with | Some pvar_typ -> L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ; - let* exec_states = exec_state_res in - List.map exec_states ~f:(fun exec_state -> - exec_object_out_of_scope call_loc pvar_typ exec_state ) - |> Result.all + List.map exec_states_res ~f:(fun exec_state -> + exec_state >>= exec_object_out_of_scope call_loc pvar_typ ) | None -> - exec_state_res + exec_states_res in if Option.exists callee_pname ~f:IRAttributes.is_no_return then - ExecutionDomain.force_exit_program proc_desc exec_state - else exec_state + List.filter_map exec_states_res ~f:(fun exec_state_res -> + match exec_state_res with + | Error _ as err -> + Some err + | Ok exec_state -> + ExecutionDomain.force_exit_program proc_desc exec_state + |> Option.map ~f:(fun exec_state -> Ok exec_state) ) + else exec_states_res (* [get_dealloc_from_dynamic_types vars_types loc] returns a dealloc procname and vars and @@ -271,7 +285,7 @@ module PulseTransferFunctions = struct L.d_printfln ~color:Pp.Orange "Executing injected call to dealloc for vars (%a) that are exiting the scope@." (Pp.seq ~sep:"," Var.pp) vars ; - let astates = List.fold ~f:call_dealloc dealloc_data ~init:[Domain.ContinueProgram astate] in + let astates = List.fold ~f:call_dealloc dealloc_data ~init:[ContinueProgram astate] in (astates, ret_vars) @@ -362,13 +376,13 @@ module PulseTransferFunctions = struct in report_on_error analysis_data result | Prune (condition, loc, _is_then_branch, _if_kind) -> - (let+ astate = PulseOperations.prune loc ~condition astate in + (let<*> astate = PulseOperations.prune loc ~condition astate in if PulseArithmetic.is_unsat_cheap astate then (* [condition] is known to be unsatisfiable: prune path *) [] else (* [condition] is true or unknown value: go into the branch *) - [Domain.ContinueProgram astate]) + [Ok (ContinueProgram astate)]) |> report_on_error_list analysis_data | Call (ret, call_exp, actuals, loc, call_flags) -> dispatch_call analysis_data ret call_exp actuals loc call_flags astate @@ -393,7 +407,7 @@ module PulseTransferFunctions = struct ~init:[] astates in if Procname.is_java (Procdesc.get_proc_name proc_desc) then - remove_vars vars [Domain.ContinueProgram astate] + remove_vars vars [ContinueProgram astate] else (* Here we add and execute calls to dealloc for Objective-C objects before removing the variables *) @@ -411,7 +425,7 @@ module PulseTransferFunctions = struct | Metadata (VariableLifetimeBegins (pvar, typ, location)) when not (Pvar.is_global pvar) -> [PulseOperations.realloc_pvar pvar typ location astate |> Domain.continue] | Metadata (Abstract _ | VariableLifetimeBegins _ | Nullify _ | Skip) -> - [Domain.ContinueProgram astate] ) + [ContinueProgram astate] ) let exec_instr astate analysis_data cfg_node instr = diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index 48cdb076c..7dbba75dd 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -78,33 +78,32 @@ let is_unsat_cheap exec_state = PathCondition.is_unsat_cheap (get_astate exec_st type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson_of] -let summary_of_posts_common ~continue_program pdesc posts = +let summary_of_post_common ~continue_program proc_desc = function + | ContinueProgram astate | ISLLatentMemoryError astate -> ( + match AbductiveDomain.summary_of_post proc_desc astate with + | Unsat -> + None + | Sat astate -> + Some (continue_program astate) ) + (* already a summary but need to reconstruct the variants to make the type system happy *) + | AbortProgram astate -> + Some (AbortProgram astate) + | ExitProgram astate -> + Some (ExitProgram astate) + | LatentAbortProgram {astate; latent_issue} -> + Some (LatentAbortProgram {astate; latent_issue}) + + +let summary_of_posts proc_desc posts = List.filter_mapi posts ~f:(fun i exec_state -> L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ; - match exec_state with - | ContinueProgram astate | ISLLatentMemoryError astate -> ( - match AbductiveDomain.summary_of_post pdesc astate with - | Unsat -> - None - | Sat astate -> - Some (continue_program astate) ) - (* already a summary but need to reconstruct the variants to make the type system happy *) - | AbortProgram astate -> - Some (AbortProgram astate) - | ExitProgram astate -> - Some (ExitProgram astate) - | LatentAbortProgram {astate; latent_issue} -> - Some (LatentAbortProgram {astate; latent_issue}) ) - - -let summary_of_posts = - summary_of_posts_common ~continue_program:(fun astate -> - match (astate :> AbductiveDomain.t).isl_status with - | ISLOk -> - ContinueProgram astate - | ISLError -> - ISLLatentMemoryError astate ) - - -let force_exit_program = - summary_of_posts_common ~continue_program:(fun astate -> ExitProgram astate) + summary_of_post_common proc_desc exec_state ~continue_program:(fun astate -> + match (astate :> AbductiveDomain.t).isl_status with + | ISLOk -> + ContinueProgram astate + | ISLError -> + ISLLatentMemoryError astate ) ) + + +let force_exit_program proc_desc post = + summary_of_post_common proc_desc post ~continue_program:(fun astate -> ExitProgram astate) diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index a1080e536..972b113a5 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -36,4 +36,4 @@ type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson val summary_of_posts : Procdesc.t -> t list -> summary list -val force_exit_program : Procdesc.t -> t list -> t list +val force_exit_program : Procdesc.t -> t -> t option diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 64da377bc..747840027 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -6,9 +6,9 @@ *) open! IStd -open IResult.Let_syntax open PulseBasicInterface open PulseDomainInterface +open PulseOperations.Import type arg_payload = AbstractValue.t * ValueHistory.t @@ -18,16 +18,16 @@ type model = -> Location.t -> ret:Ident.t * Typ.t -> AbductiveDomain.t - -> ExecutionDomain.t list PulseOperations.access_result + -> ExecutionDomain.t PulseOperations.access_result list -let ok_continue post = Ok [ExecutionDomain.ContinueProgram post] +let ok_continue post = [Ok (ContinueProgram post)] let cpp_model_namespace = QualifiedCppName.of_list ["__infer_pulse_model"] module Misc = struct let shallow_copy_value location event ret_id dest_pointer_hist src_value_hist astate = - let* astate, obj_copy = PulseOperations.shallow_copy location src_value_hist astate in - let+ astate = + let<*> astate, obj_copy = PulseOperations.shallow_copy location src_value_hist astate in + let<+> astate = PulseOperations.write_deref location ~ref:dest_pointer_hist ~obj:(fst obj_copy, event :: snd obj_copy) astate @@ -36,7 +36,7 @@ module Misc = struct let shallow_copy location event ret_id dest_pointer_hist src_pointer_hist astate = - let* astate, obj = + let<*> astate, obj = PulseOperations.eval_access Read location src_pointer_hist Dereference astate in shallow_copy_value location event ret_id dest_pointer_hist obj astate @@ -45,17 +45,16 @@ module Misc = struct let shallow_copy_model model_desc dest_pointer_hist src_pointer_hist : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in - let+ astate = shallow_copy location event ret_id dest_pointer_hist src_pointer_hist astate in - [ExecutionDomain.ContinueProgram astate] + shallow_copy location event ret_id dest_pointer_hist src_pointer_hist astate let early_exit : model = fun {proc_desc} ~callee_procname:_ _ ~ret:_ astate -> match AbductiveDomain.summary_of_post proc_desc astate with | Unsat -> - Ok [] + [] | Sat astate -> - Ok [ExecutionDomain.ExitProgram astate] + [Ok (ExitProgram astate)] let return_int : Int64.t -> model = @@ -96,10 +95,8 @@ module Misc = struct AnalysisCallbacks.proc_resolve_attributes callee_procname |> Option.map ~f:ProcAttributes.get_pvar_formals in - Ok - [ ExecutionDomain.ContinueProgram - (PulseOperations.unknown_call location (Model skip_reason) ~ret ~actuals ~formals_opt - astate) ] + PulseOperations.unknown_call location (Model skip_reason) ~ret ~actuals ~formals_opt astate + |> ok_continue (** don't actually do nothing, apply the heuristics for unknown calls (this may or may not be a @@ -129,13 +126,14 @@ module Misc = struct match operation with `Free -> Invalidation.CFree | `Delete -> Invalidation.CppDelete in if Config.pulse_isl then - let+ astates = - PulseOperations.invalidate_biad_isl location invalidation deleted_access astate - in - List.map astates ~f:(fun astate -> ExecutionDomain.ContinueProgram astate) + match PulseOperations.invalidate_biad_isl location invalidation deleted_access astate with + | Error _ as err -> + [err] + | Ok astates -> + List.map astates ~f:(fun astate -> Ok (ContinueProgram astate)) else - let+ astate = PulseOperations.invalidate location invalidation deleted_access astate in - [ExecutionDomain.ContinueProgram astate] + let<+> astate = PulseOperations.invalidate location invalidation deleted_access astate in + astate end module C = struct @@ -160,11 +158,14 @@ module C = struct |> PulseOperations.allocate callee_procname location ret_value |> set_uninitialized size_exp_opt location ret_addr in - let+ astate_null = - PulseArithmetic.and_eq_int ret_addr IntLit.zero astate - |> PulseOperations.invalidate location (ConstantDereference IntLit.zero) ret_value + let result_null = + let+ astate_null = + PulseArithmetic.and_eq_int ret_addr IntLit.zero astate + |> PulseOperations.invalidate location (ConstantDereference IntLit.zero) ret_value + in + ContinueProgram astate_null in - [ExecutionDomain.ContinueProgram astate_alloc; ExecutionDomain.ContinueProgram astate_null] + [Ok (ContinueProgram astate_alloc); result_null] let malloc_not_null_common ~size_exp_opt : model = @@ -217,19 +218,19 @@ module ObjC = struct let dispatch_sync args : model = - fun {analyze_dependency; proc_desc; tenv; err_log} ~callee_procname:_ location ~ret astate -> + fun {analyze_dependency; proc_desc} ~callee_procname:_ location ~ret astate -> match List.last args with | None -> - Ok [ExecutionDomain.ContinueProgram astate] + ok_continue astate | Some {ProcnameDispatcher.Call.FuncArg.arg_payload= lambda_ptr_hist} -> ( - let* astate, (lambda, _) = + let<*> astate, (lambda, _) = PulseOperations.eval_access Read location lambda_ptr_hist Dereference astate in match AddressAttributes.get_closure_proc_name lambda astate with | None -> - Ok [ExecutionDomain.ContinueProgram astate] + ok_continue astate | Some callee_proc_name -> - PulseOperations.call ~caller_proc_desc:proc_desc tenv err_log + PulseOperations.call ~caller_proc_desc:proc_desc ~callee_data:(analyze_dependency callee_proc_name) location callee_proc_name ~ret ~actuals:[] ~formals_opt:None astate ) end @@ -262,41 +263,40 @@ module Optional = struct let assign_none this ~desc : model = fun _ ~callee_procname:_ location ~ret:_ astate -> - let* astate, value = assign_value_fresh location this ~desc astate in + 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 - [ExecutionDomain.ContinueProgram astate] + let<+> astate = PulseOperations.invalidate location Invalidation.OptionalEmpty value astate in + astate let assign_value this _value ~desc : model = fun _ ~callee_procname:_ location ~ret:_ 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 - [ExecutionDomain.ContinueProgram astate] + let<+> astate, value = assign_value_fresh location this ~desc astate in + PulseArithmetic.and_positive (fst value) astate let assign_optional_value this init ~desc : model = fun _ ~callee_procname:_ location ~ret:_ astate -> - let* astate, value = to_internal_value_deref Read location init astate in - let+ astate, _ = write_value location this ~value ~desc astate in - [ExecutionDomain.ContinueProgram 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 -> - let+ astate, _ = assign_value_fresh location optional ~desc astate in - [ExecutionDomain.ContinueProgram 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 -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in - let* astate, ((value_addr, value_hist) as value) = + let<*> astate, ((value_addr, value_hist) as value) = to_internal_value_deref Write location optional astate in (* Check dereference to show an error at the callsite of `value()` *) - let* astate, _ = PulseOperations.eval_access Write location value Dereference astate in + let<*> astate, _ = PulseOperations.eval_access Write location value Dereference astate in PulseOperations.write_id ret_id (value_addr, event :: value_hist) astate |> ok_continue @@ -304,51 +304,51 @@ module Optional = struct fun _ ~callee_procname:_ 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 + let<*> astate, (value_addr, _) = to_internal_value_deref Read location optional astate in let astate = PulseOperations.write_id ret_id ret_value astate in let astate_non_empty = PulseArithmetic.and_positive value_addr astate in let astate_true = PulseArithmetic.and_positive ret_addr astate_non_empty in let astate_empty = PulseArithmetic.and_eq_int value_addr IntLit.zero astate in let astate_false = PulseArithmetic.and_eq_int ret_addr IntLit.zero astate_empty in - [ExecutionDomain.ContinueProgram astate_false; ExecutionDomain.ContinueProgram astate_true] + [Ok (ContinueProgram astate_false); Ok (ContinueProgram astate_true)] let get_pointer optional ~desc : model = fun _ ~callee_procname:_ 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, value_addr = to_internal_value_deref Read location optional astate in let value_update_hist = (fst value_addr, event :: snd value_addr) in let astate_value_addr = PulseOperations.write_id ret_id value_update_hist astate |> PulseArithmetic.and_positive (fst value_addr) in let nullptr = (AbstractValue.mk_fresh (), [event]) in - let+ astate_null = + let<*> astate_null = PulseOperations.write_id ret_id nullptr astate |> PulseArithmetic.and_eq_int (fst value_addr) IntLit.zero |> PulseArithmetic.and_eq_int (fst nullptr) IntLit.zero |> PulseOperations.invalidate location (ConstantDereference IntLit.zero) nullptr in - [ExecutionDomain.ContinueProgram astate_value_addr; ExecutionDomain.ContinueProgram astate_null] + [Ok (ContinueProgram astate_value_addr); Ok (ContinueProgram astate_null)] let value_or optional default ~desc : model = fun _ ~callee_procname:_ 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, value_addr = to_internal_value_deref Read location optional astate in let astate_non_empty = PulseArithmetic.and_positive (fst value_addr) astate in - let* astate_non_empty, value = + let<*> astate_non_empty, value = PulseOperations.eval_access Read location value_addr Dereference astate_non_empty in let value_update_hist = (fst value, event :: snd value) in let astate_value = PulseOperations.write_id ret_id value_update_hist astate_non_empty in - let+ astate, (default_val, default_hist) = + let<*> astate, (default_val, default_hist) = PulseOperations.eval_access Read location default Dereference astate in let default_value_hist = (default_val, event :: default_hist) in let astate_empty = PulseArithmetic.and_eq_int (fst value_addr) IntLit.zero astate in let astate_default = PulseOperations.write_id ret_id default_value_hist astate_empty in - [ExecutionDomain.ContinueProgram astate_value; ExecutionDomain.ContinueProgram astate_default] + [Ok (ContinueProgram astate_value); Ok (ContinueProgram astate_default)] end module Cplusplus = struct @@ -385,12 +385,12 @@ module StdAtomicInteger = struct 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 = + let<*> astate, int_field = PulseOperations.eval_access Write location this (FieldAccess internal_int) astate in - let* astate = PulseOperations.write_deref location ~ref:int_field ~obj:init_value astate in - let+ astate = PulseOperations.write_deref location ~ref:this_address ~obj:this astate in - [ExecutionDomain.ContinueProgram astate] + let<*> astate = PulseOperations.write_deref location ~ref:int_field ~obj:init_value astate in + let<+> astate = PulseOperations.write_deref location ~ref:this_address ~obj:this astate in + astate let arith_bop prepost location event ret_id bop this operand astate = @@ -409,30 +409,30 @@ module StdAtomicInteger = struct let fetch_add this (increment, _) _memory_ordering : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::fetch_add()"; location; in_call= []} in - let+ astate = + let<+> astate = arith_bop `Post location event ret_id (PlusA None) this (AbstractValueOperand increment) astate in - [ExecutionDomain.ContinueProgram astate] + astate let fetch_sub this (increment, _) _memory_ordering : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::fetch_sub()"; location; in_call= []} in - let+ astate = + let<+> astate = arith_bop `Post location event ret_id (MinusA None) this (AbstractValueOperand increment) astate in - [ExecutionDomain.ContinueProgram astate] + astate let operator_plus_plus_pre this : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::operator++()"; location; in_call= []} in - let+ astate = + let<+> astate = arith_bop `Pre location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate in - [ExecutionDomain.ContinueProgram astate] + astate let operator_plus_plus_post this _int : model = @@ -440,19 +440,19 @@ module StdAtomicInteger = struct let event = ValueHistory.Call {f= Model "std::atomic::operator++(T)"; location; in_call= []} in - let+ astate = + let<+> astate = arith_bop `Post location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate in - [ExecutionDomain.ContinueProgram astate] + astate let operator_minus_minus_pre this : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "std::atomic::operator--()"; location; in_call= []} in - let+ astate = + let<+> astate = arith_bop `Pre location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate in - [ExecutionDomain.ContinueProgram astate] + astate let operator_minus_minus_post this _int : model = @@ -460,18 +460,17 @@ module StdAtomicInteger = struct let event = ValueHistory.Call {f= Model "std::atomic::operator--(T)"; location; in_call= []} in - let+ astate = + let<+> astate = arith_bop `Post location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate in - [ExecutionDomain.ContinueProgram astate] + astate let load_instr model_desc this _memory_ordering_opt : model = 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 - [ExecutionDomain.ContinueProgram astate] + let<+> astate, _int_addr, (int, hist) = load_backing_int location this astate in + PulseOperations.write_id ret_id (int, event :: hist) astate let load = load_instr "std::atomic::load()" @@ -489,17 +488,16 @@ module StdAtomicInteger = struct let store this_address (new_value, new_hist) _memory_ordering : model = 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<+> 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 -> 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 - let astate = PulseOperations.write_id ret_id (old_int, event :: old_hist) astate in - [ExecutionDomain.ContinueProgram astate] + 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 + PulseOperations.write_id ret_id (old_int, event :: old_hist) astate end module JavaObject = struct @@ -507,12 +505,11 @@ module JavaObject = struct let clone src_pointer_hist : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let event = ValueHistory.Call {f= Model "Object.clone"; location; in_call= []} in - let* astate, obj = + let<*> astate, obj = PulseOperations.eval_access Read location src_pointer_hist Dereference astate in - let+ astate, obj_copy = PulseOperations.shallow_copy location obj astate in - let astate = PulseOperations.write_id ret_id (fst obj_copy, event :: snd obj_copy) astate in - [ExecutionDomain.ContinueProgram astate] + let<+> astate, obj_copy = PulseOperations.shallow_copy location obj astate in + PulseOperations.write_id ret_id (fst obj_copy, event :: snd obj_copy) astate end module StdBasicString = struct @@ -531,52 +528,49 @@ module StdBasicString = struct let data this_hist : model = 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) = + let<*> astate, string_addr_hist = to_internal_string location this_hist astate in + let<+> astate, (string, hist) = PulseOperations.eval_access Read location string_addr_hist Dereference astate in - let astate = PulseOperations.write_id ret_id (string, event :: hist) astate in - [ExecutionDomain.ContinueProgram astate] + PulseOperations.write_id ret_id (string, event :: hist) astate let destructor this_hist : model = 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 + let<*> astate, (string_addr, string_hist) = to_internal_string location this_hist astate in let string_addr_hist = (string_addr, call_event :: string_hist) in - let* astate = + let<*> astate = PulseOperations.invalidate_access location CppDelete string_addr_hist Dereference astate in - let+ astate = PulseOperations.invalidate location CppDelete string_addr_hist astate in - [ExecutionDomain.ContinueProgram astate] + let<+> astate = PulseOperations.invalidate location CppDelete string_addr_hist astate in + astate end module StdFunction = struct let operator_call ProcnameDispatcher.Call.FuncArg.{arg_payload= lambda_ptr_hist; typ} actuals : model = - fun {analyze_dependency; proc_desc; tenv; err_log} ~callee_procname:_ location ~ret astate -> + fun {analyze_dependency; proc_desc} ~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] in - let* astate, (lambda, _) = + let<*> astate, (lambda, _) = PulseOperations.eval_access Read location lambda_ptr_hist Dereference astate in - let* astate = PulseOperations.Closures.check_captured_addresses location lambda astate in + let<*> astate = PulseOperations.Closures.check_captured_addresses location lambda astate in match AddressAttributes.get_closure_proc_name lambda astate with | None -> (* we don't know what proc name this lambda resolves to *) - Ok - ( havoc_ret ret astate - |> List.map ~f:(fun astate -> ExecutionDomain.ContinueProgram astate) ) + havoc_ret ret astate |> List.map ~f:(fun astate -> Ok (ContinueProgram astate)) | Some callee_proc_name -> let actuals = (lambda_ptr_hist, typ) :: List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} -> (arg_payload, typ) ) in - PulseOperations.call ~caller_proc_desc:proc_desc tenv err_log + PulseOperations.call ~caller_proc_desc:proc_desc ~callee_data:(analyze_dependency callee_proc_name) location callee_proc_name ~ret ~actuals ~formals_opt:None astate @@ -584,21 +578,18 @@ 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 -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in - let+ astate = - if PulseArithmetic.is_known_zero astate (fst src) then - let empty_target = AbstractValue.mk_fresh () in - let+ astate = - PulseOperations.write_deref location ~ref:dest ~obj:(empty_target, [event]) astate - in - PulseOperations.havoc_id ret_id [event] astate - else - match src_typ.Typ.desc with - | Tptr (_, Pk_reference) -> - Misc.shallow_copy location event ret_id dest src astate - | _ -> - Misc.shallow_copy_value location event ret_id dest src astate - in - [ExecutionDomain.ContinueProgram astate] + if PulseArithmetic.is_known_zero astate (fst src) then + let empty_target = AbstractValue.mk_fresh () in + let<+> astate = + PulseOperations.write_deref location ~ref:dest ~obj:(empty_target, [event]) astate + in + PulseOperations.havoc_id ret_id [event] astate + else + match src_typ.Typ.desc with + | Tptr (_, Pk_reference) -> + Misc.shallow_copy location event ret_id dest src astate + | _ -> + Misc.shallow_copy_value location event ret_id dest src astate end module GenericArrayBackedCollection = struct @@ -689,14 +680,15 @@ module GenericArrayBackedCollectionIterator = struct let constructor ~desc this init : model = fun _ ~callee_procname:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in - construct location event ~init ~ref:this astate >>| ExecutionDomain.continue >>| List.return + let<+> astate = construct location event ~init ~ref:this astate in + astate - let operator_compare comparison ~desc iter_lhs iter_rhs _ ~callee_procname:_ location - ~ret:(ret_id, _) astate = + let operator_compare comparison ~desc iter_lhs iter_rhs : model = + fun _ ~callee_procname:_ 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 + 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 let ret_val = AbstractValue.mk_fresh () in let astate = PulseOperations.write_id ret_id (ret_val, [event]) astate in let ret_val_equal, ret_val_notequal = @@ -716,24 +708,29 @@ module GenericArrayBackedCollectionIterator = struct |> PulseArithmetic.prune_binop ~negated:false Ne (AbstractValueOperand index_lhs) (AbstractValueOperand index_rhs) in - [ExecutionDomain.ContinueProgram astate_equal; ExecutionDomain.ContinueProgram astate_notequal] + [Ok (ContinueProgram astate_equal); Ok (ContinueProgram astate_notequal)] - let operator_star ~desc iter _ ~callee_procname:_ location ~ret astate = + let operator_star ~desc iter : model = + fun _ ~callee_procname:_ 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 - let astate = PulseOperations.write_id (fst ret) (elem, event :: snd pointer) astate in - [ExecutionDomain.ContinueProgram astate] + 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 _ ~callee_procname:_ location ~ret:_ astate = + let operator_step step ~desc iter : model = + fun _ ~callee_procname:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let index_new = AbstractValue.mk_fresh () in - let* astate, pointer, _ = + let<*> astate, pointer, _ = to_elem_pointed_by_iterator Read ~step:(Some step) location iter astate in - PulseOperations.write_deref location ~ref:pointer ~obj:(index_new, event :: snd pointer) astate - >>| ExecutionDomain.continue >>| List.return + let<+> astate = + PulseOperations.write_deref location ~ref:pointer + ~obj:(index_new, event :: snd pointer) + astate + in + astate end module JavaIterator = struct @@ -741,54 +738,54 @@ module JavaIterator = struct fun _ ~callee_procname:_ location ~ret astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let ref = (AbstractValue.mk_fresh (), [event]) in - let+ astate = GenericArrayBackedCollectionIterator.construct location event ~init ~ref astate in - let astate = PulseOperations.write_id (fst ret) ref astate in - [ExecutionDomain.ContinueProgram astate] + let<+> astate = + GenericArrayBackedCollectionIterator.construct location event ~init ~ref astate + in + PulseOperations.write_id (fst ret) ref astate (* {curr -> v_c} is modified to {curr -> v_fresh} and returns array[v_c] *) - let next ~desc iter _ ~callee_procname:_ location ~ret astate = + let next ~desc iter : model = + fun _ ~callee_procname:_ 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) = + let<*> astate, (curr_index, curr_index_hist) = GenericArrayBackedCollectionIterator.to_internal_pointer Read location iter astate in - let* astate, (curr_elem_val, curr_elem_hist) = + let<*> astate, (curr_elem_val, curr_elem_hist) = GenericArrayBackedCollection.element location iter curr_index astate in - let+ astate = + let<+> astate = PulseOperations.write_field location ~ref:iter GenericArrayBackedCollectionIterator.internal_pointer ~obj:(new_index, event :: curr_index_hist) astate in - let astate = - PulseOperations.write_id (fst ret) (curr_elem_val, event :: curr_elem_hist) astate - in - [ExecutionDomain.ContinueProgram astate] + PulseOperations.write_id (fst ret) (curr_elem_val, event :: curr_elem_hist) astate (* {curr -> v_c } is modified to {curr -> v_fresh} and writes to array[v_c] *) - let remove ~desc iter _ ~callee_procname:_ location ~ret:_ astate = + let remove ~desc iter : model = + fun _ ~callee_procname:_ 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) = + let<*> astate, (curr_index, curr_index_hist) = GenericArrayBackedCollectionIterator.to_internal_pointer Read location iter astate in - let* astate = + let<*> astate = PulseOperations.write_field location ~ref:iter GenericArrayBackedCollectionIterator.internal_pointer ~obj:(new_index, event :: curr_index_hist) astate in let new_elem = AbstractValue.mk_fresh () in - let* astate, arr = GenericArrayBackedCollection.eval Read location iter astate in - let+ astate = + let<*> astate, arr = GenericArrayBackedCollection.eval Read location iter astate in + let<+> astate = PulseOperations.write_arr_index location ~ref:arr ~index:curr_index ~obj:(new_elem, event :: curr_index_hist) astate in - [ExecutionDomain.ContinueProgram astate] + astate end module StdVector = struct @@ -802,15 +799,16 @@ module StdVector = struct >>= PulseOperations.havoc_field location vector GenericArrayBackedCollection.field trace - let init_list_constructor this init_list _ ~callee_procname:_ location ~ret:_ astate = + let init_list_constructor this init_list : model = + fun _ ~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 = + let<*> astate, init_copy = PulseOperations.shallow_copy location init_list astate in + let<+> astate = PulseOperations.write_field location ~ref:this GenericArrayBackedCollection.field ~obj:(fst init_copy, event :: snd init_copy) astate in - [ExecutionDomain.ContinueProgram astate] + astate let invalidate_references vector_f vector : model = @@ -821,18 +819,17 @@ module StdVector = struct ; location ; in_call= [] } in - reallocate_internal_array [crumb] vector vector_f location astate - >>| ExecutionDomain.continue >>| List.return + let<+> astate = reallocate_internal_array [crumb] vector vector_f location astate in + astate let at ~desc vector index : model = fun _ ~callee_procname:_ location ~ret astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in - let+ astate, (addr, hist) = + let<+> astate, (addr, hist) = GenericArrayBackedCollection.element location vector (fst index) astate in - let astate = PulseOperations.write_id (fst ret) (addr, event :: hist) astate in - [ExecutionDomain.ContinueProgram astate] + PulseOperations.write_id (fst ret) (addr, event :: hist) astate let vector_begin vector iter : model = @@ -842,44 +839,48 @@ module StdVector = struct let pointer_val = (AbstractValue.mk_fresh (), pointer_hist) in let index_zero = AbstractValue.mk_fresh () in let astate = PulseArithmetic.and_eq_int index_zero IntLit.zero astate in - let* astate, ((arr_addr, _) as arr) = + let<*> astate, ((arr_addr, _) as arr) = GenericArrayBackedCollection.eval Read location vector astate in - let* astate, _ = GenericArrayBackedCollection.eval_element location arr index_zero astate in - PulseOperations.write_field location ~ref:iter GenericArrayBackedCollection.field - ~obj:(arr_addr, pointer_hist) astate - >>= PulseOperations.write_field location ~ref:iter - GenericArrayBackedCollectionIterator.internal_pointer ~obj:pointer_val - >>= PulseOperations.write_deref location ~ref:pointer_val ~obj:(index_zero, pointer_hist) - >>| ExecutionDomain.continue >>| List.return + let<*> astate, _ = GenericArrayBackedCollection.eval_element location arr index_zero astate in + let<+> astate = + PulseOperations.write_field location ~ref:iter GenericArrayBackedCollection.field + ~obj:(arr_addr, pointer_hist) astate + >>= PulseOperations.write_field location ~ref:iter + GenericArrayBackedCollectionIterator.internal_pointer ~obj:pointer_val + >>= PulseOperations.write_deref location ~ref:pointer_val ~obj:(index_zero, pointer_hist) + in + astate let vector_end vector iter : model = fun _ ~callee_procname:_ location ~ret:_ 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, _) = + let<*> astate, (arr_addr, _) = GenericArrayBackedCollection.eval Read location vector astate in + let<*> astate, (pointer_addr, _) = GenericArrayBackedCollection.eval_pointer_to_last_element location vector astate in let pointer_hist = event :: snd iter in let pointer_val = (pointer_addr, pointer_hist) in - let* astate = + let<*> astate = PulseOperations.write_field location ~ref:iter GenericArrayBackedCollection.field ~obj:(arr_addr, pointer_hist) astate in - let+ astate = + let<+> astate = PulseOperations.write_field location ~ref:iter GenericArrayBackedCollectionIterator.internal_pointer ~obj:pointer_val astate in - [ExecutionDomain.ContinueProgram astate] + astate let reserve vector : model = 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) - >>| ExecutionDomain.continue >>| List.return + let<+> astate = + reallocate_internal_array [crumb] vector Reserve location astate + >>| AddressAttributes.std_vector_reserve (fst vector) + in + astate let push_back vector : model = @@ -891,18 +892,17 @@ module StdVector = struct ok_continue astate else (* simulate a re-allocation of the underlying array every time an element is added *) - reallocate_internal_array [crumb] vector PushBack location astate - >>| ExecutionDomain.continue >>| List.return + let<+> astate = reallocate_internal_array [crumb] vector PushBack location astate in + astate let empty vector : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> let crumb = ValueHistory.Call {f= Model "std::vector::empty()"; location; in_call= []} in - let+ astate, (value_addr, value_hist) = + let<+> astate, (value_addr, value_hist) = GenericArrayBackedCollection.eval_is_empty location vector astate in - let astate = PulseOperations.write_id ret_id (value_addr, crumb :: value_hist) astate in - [ExecutionDomain.ContinueProgram astate] + PulseOperations.write_id ret_id (value_addr, crumb :: value_hist) astate end module JavaCollection = struct @@ -910,30 +910,29 @@ module JavaCollection = struct let set coll (index, _) (new_elem, new_elem_hist) : model = fun _ ~callee_procname:_ location ~ret astate -> let event = ValueHistory.Call {f= Model "Collection.set"; location; in_call= []} in - let* astate, arr = GenericArrayBackedCollection.eval Read location coll astate in - let* astate, (old_addr, old_hist) = + let<*> astate, arr = GenericArrayBackedCollection.eval Read location coll astate in + let<*> astate, (old_addr, old_hist) = GenericArrayBackedCollection.element location coll index astate in - let+ astate = + let<+> astate = PulseOperations.write_arr_index location ~ref:arr ~index ~obj:(new_elem, event :: new_elem_hist) astate in - let astate = PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate in - [ExecutionDomain.ContinueProgram astate] + PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate (* writes to arr[index]-> new_elem *) let add_at coll (index, _) (new_elem, new_elem_hist) : model = fun _ ~callee_procname:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model "Collection.add"; location; in_call= []} in - let* astate, arr = GenericArrayBackedCollection.eval Read location coll astate in - let+ astate = + let<*> astate, arr = GenericArrayBackedCollection.eval Read location coll astate in + let<+> astate = PulseOperations.write_arr_index location ~ref:arr ~index ~obj:(new_elem, event :: new_elem_hist) astate in - [ExecutionDomain.ContinueProgram astate] + astate (* writes to arr[index]-> new_elem where index is a fresh address *) @@ -946,14 +945,14 @@ module JavaCollection = struct let remove_at coll (index, _) : model = fun _ ~callee_procname:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model "Collection.add"; location; in_call= []} in - let* astate, arr = GenericArrayBackedCollection.eval Read location coll astate in + let<*> astate, arr = GenericArrayBackedCollection.eval Read location coll astate in let fresh_elem = AbstractValue.mk_fresh () in - let+ astate = + let<+> astate = PulseOperations.write_arr_index location ~ref:arr ~index ~obj:(fresh_elem, event :: snd arr) astate in - [ExecutionDomain.ContinueProgram astate] + astate (* writes to arr[index]-> fresh_elem where index is fresh *) @@ -990,14 +989,14 @@ module JavaInteger = struct let constructor this_address init_value : model = fun _ ~callee_procname:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model "Integer.init"; location; in_call= []} in - let+ state = construct this_address init_value event location astate in - [ExecutionDomain.continue state] + 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 -> - 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<*> 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 let astate = PulseArithmetic.eval_binop binop_addr Binop.Eq (AbstractValueOperand int1) @@ -1008,7 +1007,7 @@ module JavaInteger = struct let int_val this : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> - let* astate, _int_addr1, int_value_hist = load_backing_int location this astate in + 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 @@ -1016,9 +1015,8 @@ module JavaInteger = struct fun _ ~callee_procname:_ 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 - let astate = PulseOperations.write_id ret_id new_alloc astate in - [ExecutionDomain.continue astate] + let<+> astate = construct new_alloc init_value event location astate in + PulseOperations.write_id ret_id new_alloc astate end module JavaPreconditions = struct diff --git a/infer/src/pulse/PulseModels.mli b/infer/src/pulse/PulseModels.mli index 6ed8aebb3..3c2cc11dd 100644 --- a/infer/src/pulse/PulseModels.mli +++ b/infer/src/pulse/PulseModels.mli @@ -14,7 +14,7 @@ type model = -> Location.t -> ret:Ident.t * Typ.t -> AbductiveDomain.t - -> ExecutionDomain.t list PulseOperations.access_result + -> ExecutionDomain.t PulseOperations.access_result list val dispatch : Tenv.t diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index f6805e59c..ea5c07dab 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -4,17 +4,35 @@ * This source code is licensed under the MIT license found in the * LICENSE file in the root directory of this source tree. *) + open! IStd module L = Logging -open IResult.Let_syntax open PulseBasicInterface open PulseDomainInterface type t = AbductiveDomain.t -type 'a access_result = 'a PulseReport.access_result +module Import = struct + type access_mode = Read | Write | NoAccess + + type 'abductive_domain_t base_t = 'abductive_domain_t ExecutionDomain.base_t = + | ContinueProgram of 'abductive_domain_t + | ExitProgram of AbductiveDomain.summary + | AbortProgram of AbductiveDomain.summary + | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} + | ISLLatentMemoryError of 'abductive_domain_t + + type 'a access_result = 'a PulseReport.access_result -type access_mode = Read | Write | NoAccess + include IResult.Let_syntax + + let ( let<*> ) x f = match x with Error _ as err -> [err] | Ok y -> f y + + let ( let<+> ) x f = + match x with Error _ as err -> [err] | Ok y -> [Ok (ExecutionDomain.ContinueProgram (f y))] +end + +include Import let check_addr_access access_mode location (address, history) astate = let access_trace = Trace.Immediate {location; history} in @@ -665,8 +683,8 @@ let conservatively_initialize_args arg_values ({AbductiveDomain.post} as astate) AbstractValue.Set.fold AbductiveDomain.initialize reachable_values astate -let call ~caller_proc_desc tenv err_log ~(callee_data : (Procdesc.t * PulseSummary.t) option) - call_loc callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) = +let call ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc + callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) = let get_arg_values () = List.map actuals ~f:(fun ((value, _), _) -> value) in match callee_data with | Some (callee_proc_desc, exec_states) -> @@ -688,7 +706,7 @@ let call ~caller_proc_desc tenv err_log ~(callee_data : (Procdesc.t * PulseSumma let pvar = Pvar.mk name callee_pname in (Var.of_pvar pvar, capture_mode) ) in - let+ astate, captured_vars_with_actuals = + let<*> astate, captured_vars_with_actuals = match actuals with | (actual_closure, _) :: _ when not (Procname.is_objc_block callee_pname || List.is_empty captured_vars) -> @@ -718,15 +736,13 @@ let call ~caller_proc_desc tenv err_log ~(callee_data : (Procdesc.t * PulseSumma | Unsat -> (* couldn't apply pre/post pair *) posts - | Sat post -> ( - match PulseReport.report_error caller_proc_desc tenv err_log post with - | Error Unsat -> - posts - | Error (Sat post) | Ok post -> - post :: posts ) ) + | Sat post -> + post :: posts ) | None -> (* no spec found for some reason (unknown function, ...) *) L.d_printfln "No spec found for %a@\n" Procname.pp callee_pname ; - let astate = conservatively_initialize_args (get_arg_values ()) astate in - unknown_call call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt astate - |> fun astate -> Ok [ExecutionDomain.ContinueProgram astate] + let astate = + conservatively_initialize_args (get_arg_values ()) astate + |> unknown_call call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt + in + [Ok (ContinueProgram astate)] diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 605dcbf14..fa3e7216f 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -9,17 +9,44 @@ open! IStd open PulseBasicInterface open PulseDomainInterface -type t = AbductiveDomain.t +(** For [open]ing in other modules. *) +module Import : sig + type access_mode = + | Read + | Write + | NoAccess + (** The initialized-ness of the address is not checked when it evaluates a heap address + without actual memory access, for example, when evaluating [&x.f] we need to check + initialized-ness of [x], not that of [x.f]. *) + + (** {2 Imported types for ease of use and so we can write variants without the corresponding + module prefix} *) + + type 'abductive_domain_t base_t = 'abductive_domain_t ExecutionDomain.base_t = + | ContinueProgram of 'abductive_domain_t + | ExitProgram of AbductiveDomain.summary + | AbortProgram of AbductiveDomain.summary + | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} + | ISLLatentMemoryError of 'abductive_domain_t + + type 'a access_result = 'a PulseReport.access_result + + (** {2 Monadic syntax} *) + + include module type of IResult.Let_syntax + + val ( let<*> ) : 'a access_result -> ('a -> 'b access_result list) -> 'b access_result list + (** monadic "bind" but not really that turns an [access_result] into a list of [access_result]s + (not really because the first type is not an [access_result list] but just an [access_result]) *) + + val ( let<+> ) : + 'a access_result -> ('a -> 'abductive_domain_t) -> 'abductive_domain_t base_t access_result list + (** monadic "map" but even less really that turns an [access_result] into an analysis result *) +end -type 'a access_result = 'a PulseReport.access_result +include module type of Import -type access_mode = - | Read - | Write - | NoAccess - (** The initialized-ness of the address is not checked when it evaluates a heap address - without actual memory access, for example, when evaluating [&x.f] we need to check - initialized-ness of [x], not that of [x.f]. *) +type t = AbductiveDomain.t val check_addr_access : access_mode -> Location.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result @@ -159,8 +186,6 @@ val check_address_escape : val call : caller_proc_desc:Procdesc.t - -> Tenv.t - -> Errlog.t -> callee_data:(Procdesc.t * PulseSummary.t) option -> Location.t -> Procname.t @@ -168,7 +193,7 @@ val call : -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list -> formals_opt:(Pvar.t * Typ.t) list option -> t - -> ExecutionDomain.t list access_result + -> ExecutionDomain.t access_result list (** perform an interprocedural call: apply the summary for the call proc name passed as argument if it exists *)