From df9a7bbc810dedde0fd669052ef1dd22c96e0c8b Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 25 May 2021 09:09:36 -0700 Subject: [PATCH] [pulse][4/5] add a path context to record timestamps Summary: Add a new `PathContext.t` component to the abstract state. For now it tracks only the current "timestamp" of symbolic execution inside the procedure, i.e. which step of symbolic execution we are in (bumped by 1 each time we've executed one instruction). In the future this will also hold, eg, which conditionals we've been through on the path (for reporting traces with that information). Most of the diff is about propagating the path context through many of the APIs. We use timestamps only in `MustBeValid` attributes to report the first incorrect access in a function call for now. Reviewed By: skcho Differential Revision: D28674726 fbshipit-source-id: 2cd825e73 --- infer/src/absint/AbstractDomain.ml | 11 +- infer/src/absint/AbstractDomain.mli | 2 + infer/src/pulse/Pulse.ml | 94 +-- infer/src/pulse/PulseAbductiveDomain.ml | 30 +- infer/src/pulse/PulseAbductiveDomain.mli | 17 +- infer/src/pulse/PulseAttribute.ml | 25 +- infer/src/pulse/PulseAttribute.mli | 8 +- infer/src/pulse/PulseBaseAddressAttributes.ml | 4 +- .../src/pulse/PulseBaseAddressAttributes.mli | 4 +- infer/src/pulse/PulseBasicInterface.ml | 2 + infer/src/pulse/PulseCallOperations.ml | 18 +- infer/src/pulse/PulseCallOperations.mli | 1 + infer/src/pulse/PulseInterproc.ml | 205 ++++--- infer/src/pulse/PulseInterproc.mli | 3 +- infer/src/pulse/PulseModels.ml | 578 ++++++++++-------- infer/src/pulse/PulseModels.mli | 1 + infer/src/pulse/PulseObjectiveCSummary.ml | 31 +- infer/src/pulse/PulseOperations.ml | 184 +++--- infer/src/pulse/PulseOperations.mli | 83 ++- infer/src/pulse/PulsePathContext.ml | 24 + infer/src/pulse/PulsePathContext.mli | 24 + infer/tests/codetoanalyze/c/pulse/issues.exp | 2 +- infer/tests/codetoanalyze/c/pulse/nullptr.c | 3 + .../tests/codetoanalyze/objc/pulse/issues.exp | 2 +- 24 files changed, 792 insertions(+), 564 deletions(-) create mode 100644 infer/src/pulse/PulsePathContext.ml create mode 100644 infer/src/pulse/PulsePathContext.mli diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index 3756da823..ad0e4806a 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -175,7 +175,7 @@ module TopLifted (Domain : S) = struct let pp = TopLiftedUtils.pp ~pp:Domain.pp end -module Pair (Domain1 : S) (Domain2 : S) = struct +module PairNoJoin (Domain1 : NoJoin) (Domain2 : NoJoin) = struct type t = Domain1.t * Domain2.t let leq ~lhs ~rhs = @@ -183,6 +183,12 @@ module Pair (Domain1 : S) (Domain2 : S) = struct else Domain1.leq ~lhs:(fst lhs) ~rhs:(fst rhs) && Domain2.leq ~lhs:(snd lhs) ~rhs:(snd rhs) + let pp fmt astate = Pp.pair ~fst:Domain1.pp ~snd:Domain2.pp fmt astate +end + +module Pair (Domain1 : S) (Domain2 : S) = struct + include PairNoJoin (Domain1) (Domain2) + let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 else @@ -199,9 +205,6 @@ module Pair (Domain1 : S) (Domain2 : S) = struct ( Domain1.widen ~prev:(fst prev) ~next:(fst next) ~num_iters , Domain2.widen ~prev:(snd prev) ~next:(snd next) ~num_iters ) prev next - - - let pp fmt astate = Pp.pair ~fst:Domain1.pp ~snd:Domain2.pp fmt astate end module Flat (V : PrettyPrintable.PrintableEquatableType) = struct diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index 29a0f0fcb..e31a512fd 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -83,6 +83,8 @@ end (** Cartesian product of two domains. *) module Pair (Domain1 : S) (Domain2 : S) : S with type t = Domain1.t * Domain2.t +module PairNoJoin (Domain1 : NoJoin) (Domain2 : NoJoin) : NoJoin with type t = Domain1.t * Domain2.t + (** Flat abstract domain: Bottom, Top, and non-comparable elements in between *) module Flat (V : PrettyPrintable.PrintableEquatableType) : sig include WithBottom diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 2fd669ccb..1449f04fc 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -25,7 +25,7 @@ let report_topl_errors proc_desc err_log summary = module PulseTransferFunctions = struct module CFG = ProcCfg.Normal - module Domain = ExecutionDomain + module Domain = AbstractDomain.PairNoJoin (PathContext) (ExecutionDomain) type analysis_data = PulseSummary.t InterproceduralAnalysis.t @@ -33,18 +33,18 @@ module PulseTransferFunctions = struct AnalysisCallbacks.proc_resolve_attributes pname |> Option.map ~f:Pvar.get_pvar_formals - let interprocedural_call {InterproceduralAnalysis.analyze_dependency; tenv; proc_desc} ret + let interprocedural_call {InterproceduralAnalysis.analyze_dependency; tenv; proc_desc} path 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 - PulseCallOperations.call tenv ~caller_proc_desc:proc_desc ~callee_data call_loc callee_pname - ~ret ~actuals ~formals_opt astate + PulseCallOperations.call tenv path ~caller_proc_desc:proc_desc ~callee_data call_loc + callee_pname ~ret ~actuals ~formals_opt astate | _ -> (* dereference call expression to catch nil issues *) let<*> astate, _ = - PulseOperations.eval_deref ~must_be_valid_reason:BlockCall call_loc call_exp astate + PulseOperations.eval_deref path ~must_be_valid_reason:BlockCall call_loc call_exp astate in L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ; let astate = @@ -72,15 +72,15 @@ module PulseTransferFunctions = struct (** [out_of_scope_access_expr] has just gone out of scope and in now invalid *) - let exec_object_out_of_scope call_loc (pvar, typ) exec_state = + let exec_object_out_of_scope path call_loc (pvar, typ) exec_state = match (exec_state : ExecutionDomain.t) with | ContinueProgram astate -> let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in let* astate, out_of_scope_base = - PulseOperations.eval NoAccess call_loc (Exp.Lvar pvar) astate + PulseOperations.eval path NoAccess call_loc (Exp.Lvar pvar) astate in (* invalidate [&x] *) - PulseOperations.invalidate + PulseOperations.invalidate path (StackAddress (Var.of_pvar pvar, [])) call_loc gone_out_of_scope out_of_scope_base astate >>| ExecutionDomain.continue @@ -102,7 +102,7 @@ module PulseTransferFunctions = struct let topl_event = PulseTopl.Call {return; arguments; procname} in AbductiveDomain.Topl.small_step loc topl_event astate in - let do_one_exec_state (exec_state : Domain.t) : Domain.t = + let do_one_exec_state (exec_state : ExecutionDomain.t) : ExecutionDomain.t = match exec_state with | ContinueProgram astate -> ContinueProgram (do_astate astate) @@ -116,12 +116,12 @@ module PulseTransferFunctions = struct List.map ~f:(Result.map ~f:do_one_exec_state) exec_state_res - let topl_store_step loc ~lhs ~rhs:_ astate = + let topl_store_step path loc ~lhs ~rhs:_ astate = match (lhs : Exp.t) with | Lindex (arr, index) -> (let open IResult.Let_syntax in - let* _astate, (aw_array, _history) = PulseOperations.eval Read loc arr astate in - let+ _astate, (aw_index, _history) = PulseOperations.eval Read loc index astate in + let* _astate, (aw_array, _history) = PulseOperations.eval path Read loc arr astate in + let+ _astate, (aw_index, _history) = PulseOperations.eval path Read loc index astate in let topl_event = PulseTopl.ArrayWrite {aw_array; aw_index} in AbductiveDomain.Topl.small_step loc topl_event astate) |> Result.ok (* don't emit Topl event if evals fail *) |> Option.value ~default:astate @@ -129,9 +129,9 @@ module PulseTransferFunctions = struct astate - let dispatch_call ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) ret + let dispatch_call ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) path ret call_exp actuals call_loc flags astate = - let<*> astate, callee_pname = PulseOperations.eval_proc_name call_loc call_exp astate in + let<*> astate, callee_pname = PulseOperations.eval_proc_name path call_loc call_exp astate in (* special case for objc dispatch models *) let callee_pname, actuals = match callee_pname with @@ -148,7 +148,7 @@ module PulseTransferFunctions = struct 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 + let+ astate, actual_evaled = PulseOperations.eval path Read call_loc actual_exp astate in ( astate , ProcnameDispatcher.Call.FuncArg. {exp= actual_exp; arg_payload= actual_evaled; typ= actual_typ} @@ -176,7 +176,7 @@ module PulseTransferFunctions = struct in PulseCallOperations.conservatively_initialize_args arg_values astate in - model {analysis_data; callee_procname; location= call_loc; ret} astate + model {analysis_data; path; callee_procname; location= call_loc; ret} astate | None -> PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ; let only_actuals_evaled = @@ -184,7 +184,7 @@ module PulseTransferFunctions = struct (arg_payload, typ) ) in let r = - interprocedural_call analysis_data ret callee_pname call_exp only_actuals_evaled + interprocedural_call analysis_data path ret callee_pname call_exp only_actuals_evaled call_loc astate in PerfEvent.(log (fun logger -> log_end_event logger ())) ; @@ -204,7 +204,7 @@ module PulseTransferFunctions = struct | Some pvar_typ -> L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ; List.map exec_states_res ~f:(fun exec_state -> - exec_state >>= exec_object_out_of_scope call_loc pvar_typ ) + exec_state >>= exec_object_out_of_scope path call_loc pvar_typ ) | None -> exec_states_res in @@ -244,10 +244,11 @@ module PulseTransferFunctions = struct is that some memory could be freed in dealloc, and we would be reporting a leak on it if we didn't call it. *) let execute_injected_dealloc_calls - ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) vars astate location = + ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) path vars astate + location = let used_ids = Stack.keys astate |> List.filter_map ~f:(fun var -> Var.get_ident var) in Ident.update_name_generator used_ids ; - let call_dealloc (astate_list : Domain.t list) (ret_id, id, typ, dealloc) = + let call_dealloc (astate_list : ExecutionDomain.t list) (ret_id, id, typ, dealloc) = let ret = (ret_id, StdTyp.void) in let call_flags = CallFlags.default in let call_exp = Exp.Const (Cfun dealloc) in @@ -256,7 +257,7 @@ module PulseTransferFunctions = struct L.d_printfln ~color:Pp.Orange "@\nExecuting injected instr:%a@\n@." (Sil.pp_instr Pp.text ~print_types:true) call_instr ; - List.concat_map astate_list ~f:(fun (astate : Domain.t) -> + List.concat_map astate_list ~f:(fun (astate : ExecutionDomain.t) -> match astate with | ISLLatentMemoryError _ | AbortProgram _ @@ -265,7 +266,7 @@ module PulseTransferFunctions = struct | LatentInvalidAccess _ -> [astate] | ContinueProgram astate -> - dispatch_call analysis_data ret call_exp actuals location call_flags astate + dispatch_call analysis_data path ret call_exp actuals location call_flags astate |> PulseReport.report_exec_results tenv proc_desc err_log location ) in let dynamic_types_unreachable = @@ -280,9 +281,9 @@ module PulseTransferFunctions = struct (astates, ret_vars) - let exec_instr_aux (astate : Domain.t) + let exec_instr_aux path (astate : ExecutionDomain.t) ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) _cfg_node - (instr : Sil.instr) : Domain.t list = + (instr : Sil.instr) : ExecutionDomain.t list = match astate with | AbortProgram _ | ISLLatentMemoryError _ | LatentAbortProgram _ | LatentInvalidAccess _ -> [astate] @@ -294,17 +295,17 @@ module PulseTransferFunctions = struct | Load {id= lhs_id; e= rhs_exp; loc} -> (* [lhs_id := *rhs_exp] *) let deref_rhs astate = - let result = + let results = if Config.pulse_isl then - PulseOperations.eval_deref_isl loc rhs_exp astate + PulseOperations.eval_deref_isl path loc rhs_exp astate |> List.map ~f:(fun result -> let+ astate, rhs_addr_hist = result in PulseOperations.write_id lhs_id rhs_addr_hist astate ) else - [ (let+ astate, rhs_addr_hist = PulseOperations.eval_deref loc rhs_exp astate in + [ (let+ astate, rhs_addr_hist = PulseOperations.eval_deref path loc rhs_exp astate in PulseOperations.write_id lhs_id rhs_addr_hist astate) ] in - PulseReport.report_results tenv proc_desc err_log loc result + PulseReport.report_results tenv proc_desc err_log loc results in let set_global_astates = match rhs_exp with @@ -320,7 +321,7 @@ module PulseTransferFunctions = struct let call_flags = CallFlags.default in let ret_id_void = (Ident.create_fresh Ident.knormal, StdTyp.void) in let no_error_states = - dispatch_call analysis_data ret_id_void (Const (Cfun proc_name)) [] loc + dispatch_call analysis_data path ret_id_void (Const (Cfun proc_name)) [] loc call_flags astate |> List.filter_map ~f:(function | Ok (ContinueProgram astate) -> @@ -347,21 +348,22 @@ module PulseTransferFunctions = struct in let result = let<*> astate, (rhs_addr, rhs_history) = - PulseOperations.eval NoAccess loc rhs_exp astate + PulseOperations.eval path NoAccess loc rhs_exp astate in let<*> is_structured, ls_astate_lhs_addr_hist = - if Config.pulse_isl then PulseOperations.eval_structure_isl Write loc lhs_exp astate + if Config.pulse_isl then + PulseOperations.eval_structure_isl path Write loc lhs_exp astate else - let+ astate, lhs_addr_hist = PulseOperations.eval Write loc lhs_exp astate in + let+ astate, lhs_addr_hist = PulseOperations.eval path Write loc lhs_exp astate in (false, [Ok (astate, lhs_addr_hist)]) in let write_function lhs_addr_hist astate = if is_structured then - PulseOperations.write_deref_biad_isl loc ~ref:lhs_addr_hist Dereference + PulseOperations.write_deref_biad_isl path loc ~ref:lhs_addr_hist Dereference ~obj:(rhs_addr, event :: rhs_history) astate else - [ PulseOperations.write_deref loc ~ref:lhs_addr_hist + [ PulseOperations.write_deref path loc ~ref:lhs_addr_hist ~obj:(rhs_addr, event :: rhs_history) astate ] in @@ -374,7 +376,7 @@ module PulseTransferFunctions = struct if Topl.is_active () then List.map astates ~f:(fun result -> let+ astate = result in - topl_store_step loc ~lhs:lhs_exp ~rhs:rhs_exp astate ) + topl_store_step path loc ~lhs:lhs_exp ~rhs:rhs_exp astate ) else astates in match lhs_exp with @@ -387,7 +389,7 @@ module PulseTransferFunctions = struct in PulseReport.report_results tenv proc_desc err_log loc result | Prune (condition, loc, _is_then_branch, _if_kind) -> - (let<*> astate = PulseOperations.prune loc ~condition astate in + (let<*> astate = PulseOperations.prune path loc ~condition astate in if PulseArithmetic.is_unsat_cheap astate then (* [condition] is known to be unsatisfiable: prune path *) [] @@ -396,11 +398,11 @@ module PulseTransferFunctions = struct [Ok (ContinueProgram astate)]) |> PulseReport.report_exec_results tenv proc_desc err_log loc | Call (ret, call_exp, actuals, loc, call_flags) -> - dispatch_call analysis_data ret call_exp actuals loc call_flags astate + dispatch_call analysis_data path ret call_exp actuals loc call_flags astate |> PulseReport.report_exec_results tenv proc_desc err_log loc | Metadata (ExitScope (vars, location)) -> let remove_vars vars astates = - List.map astates ~f:(fun (exec_state : Domain.t) -> + List.map astates ~f:(fun (exec_state : ExecutionDomain.t) -> match exec_state with | ISLLatentMemoryError _ | AbortProgram _ @@ -417,7 +419,7 @@ module PulseTransferFunctions = struct (* Here we add and execute calls to dealloc for Objective-C objects before removing the variables *) let astates, ret_vars = - execute_injected_dealloc_calls analysis_data vars astate location + execute_injected_dealloc_calls analysis_data path vars astate location in (* OPTIM: avoid re-allocating [vars] when [ret_vars] is empty (in particular if no ObjC objects are involved), but otherwise @@ -428,7 +430,7 @@ module PulseTransferFunctions = struct in remove_vars vars_to_remove astates | Metadata (VariableLifetimeBegins (pvar, typ, location)) when not (Pvar.is_global pvar) -> - [PulseOperations.realloc_pvar tenv pvar typ location astate |> Domain.continue] + [PulseOperations.realloc_pvar tenv pvar typ location astate |> ExecutionDomain.continue] | Metadata ( Abstract _ | CatchEntry _ @@ -440,11 +442,13 @@ module PulseTransferFunctions = struct [ContinueProgram astate] ) - let exec_instr astate analysis_data cfg_node instr = + let exec_instr (path, astate) analysis_data cfg_node instr : Domain.t list = (* Sometimes instead of stopping on contradictions a false path condition is recorded instead. Prune these early here so they don't spuriously count towards the disjunct limit. *) - exec_instr_aux astate analysis_data cfg_node instr - |> List.filter ~f:(fun exec_state -> not (Domain.is_unsat_cheap exec_state)) + exec_instr_aux path astate analysis_data cfg_node instr + |> List.filter_map ~f:(fun exec_state -> + if ExecutionDomain.is_unsat_cheap exec_state then None + else Some (PathContext.post_exec_instr path, exec_state) ) let pp_session_name _node fmt = F.pp_print_string fmt "Pulse" @@ -469,9 +473,11 @@ let with_debug_exit_node proc_desc ~f = let checker ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) = AbstractValue.State.reset () ; let initial_astate = ExecutionDomain.mk_initial tenv proc_desc in - let initial = [initial_astate] in + let initial = [(PathContext.initial, initial_astate)] in match DisjunctiveAnalyzer.compute_post analysis_data ~initial proc_desc with | Some posts -> + (* forget path contexts, we don't propagate them across functions *) + let posts = List.map ~f:snd posts in with_debug_exit_node proc_desc ~f:(fun () -> let updated_posts = PulseObjectiveCSummary.update_objc_method_posts analysis_data ~initial_astate ~posts diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index fe6887c6e..ef7fbfff9 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -143,7 +143,7 @@ module Stack = struct if phys_equal new_post astate.post then astate else {astate with post= new_post} - let eval location origin var astate = + let eval path location origin var astate = match BaseStack.find_opt var (astate.post :> base_domain).stack with | Some addr_hist -> (astate, addr_hist) @@ -160,7 +160,7 @@ module Stack = struct if Config.pulse_isl then let access_trace = Trace.Immediate {location; history= []} in BaseAddressAttributes.add_one addr - (MustBeValid (access_trace, None)) + (MustBeValid (path.PathContext.timestamp, access_trace, None)) (astate.post :> base_domain).attrs else (astate.post :> base_domain).attrs in @@ -236,10 +236,12 @@ module AddressAttributes = struct if phys_equal new_pre astate.pre then astate else {astate with pre= new_pre} - let check_valid ?must_be_valid_reason access_trace addr astate = + let check_valid path ?must_be_valid_reason access_trace addr astate = let+ () = BaseAddressAttributes.check_valid addr (astate.post :> base_domain).attrs in (* if [address] is in [pre] and it should be valid then that fact goes in the precondition *) - abduce_attribute addr (MustBeValid (access_trace, must_be_valid_reason)) astate + abduce_attribute addr + (MustBeValid (path.PathContext.timestamp, access_trace, must_be_valid_reason)) + astate let check_initialized access_trace addr astate = @@ -323,11 +325,11 @@ module AddressAttributes = struct map_post_attrs astate ~f:(BaseAddressAttributes.add_unreachable_at addr location) - let replace_must_be_valid_reason reason addr astate = + let replace_must_be_valid_reason path reason addr astate = match BaseAddressAttributes.get_must_be_valid addr (astate.pre :> base_domain).attrs with - | Some (trace, _reason) -> + | Some (_timestamp, trace, _reason) -> remove_must_be_valid_attr addr astate - |> abduce_attribute addr (MustBeValid (trace, Some reason)) + |> abduce_attribute addr (MustBeValid (path.PathContext.timestamp, trace, Some reason)) | None -> astate @@ -365,7 +367,7 @@ module AddressAttributes = struct BaseAddressAttributes.find_opt address (astate.post :> base_domain).attrs - let check_valid_isl access_trace addr ?(null_noop = false) astate = + let check_valid_isl path access_trace addr ?(null_noop = false) astate = L.d_printfln "*****check_valid_isl: addr*** %a@\n" AbstractValue.pp addr ; match BaseAddressAttributes.get_invalid addr (astate.post :> BaseDomain.t).attrs with | None -> @@ -389,7 +391,9 @@ module AddressAttributes = struct else let valid_astate = let abdalloc = Attribute.ISLAbduced access_trace in - let valid_attr = Attribute.MustBeValid (access_trace, None) in + let valid_attr = + Attribute.MustBeValid (path.PathContext.timestamp, access_trace, None) + in add_one addr abdalloc astate |> abduce_attribute addr valid_attr |> abduce_attribute addr abdalloc in @@ -476,7 +480,7 @@ let rec set_uninitialized_post tenv src typ location ?(fields_prefix = RevList.e let attrs = if Config.pulse_isl then BaseAddressAttributes.add_one addr - (MustBeValid (Immediate {location; history= []}, None)) + (MustBeValid (PathContext.t0, Immediate {location; history= []}, None)) attrs else attrs in @@ -562,7 +566,7 @@ let mk_initial tenv proc_desc = List.fold formals_and_captured ~init:(PreDomain.empty :> base_domain).attrs ~f:(fun attrs (_, _, (addr, _)) -> BaseAddressAttributes.add_one addr - (MustBeValid (Immediate {location; history= []}, None)) + (MustBeValid (PathContext.t0, Immediate {location; history= []}, None)) attrs ) else BaseDomain.empty.attrs in @@ -941,8 +945,8 @@ let incorporate_new_eqs astate new_eqs = L.d_printfln "Not clear why %a should be allocated in the first place, giving up" AbstractValue.pp v ; Stop Unsat - | Some must_be_valid -> - Stop (Sat (astate, Some (v, must_be_valid))) ) + | Some (_, trace, reason_opt) -> + Stop (Sat (astate, Some (v, (trace, reason_opt)))) ) | EqZero _ (* [v] not allocated *) -> Continue (astate, error) ) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 729a97c71..e75bfb369 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -68,7 +68,13 @@ module Stack : sig val find_opt : Var.t -> t -> BaseStack.value option - val eval : Location.t -> ValueHistory.t -> Var.t -> t -> t * (AbstractValue.t * ValueHistory.t) + val eval : + PathContext.t + -> Location.t + -> ValueHistory.t + -> Var.t + -> t + -> t * (AbstractValue.t * ValueHistory.t) (** return the value of the variable in the stack or create a fresh one if needed *) val mem : Var.t -> t -> bool @@ -114,7 +120,8 @@ module AddressAttributes : sig val add_attrs : AbstractValue.t -> Attributes.t -> t -> t val check_valid : - ?must_be_valid_reason:Invalidation.must_be_valid_reason + PathContext.t + -> ?must_be_valid_reason:Invalidation.must_be_valid_reason -> Trace.t -> AbstractValue.t -> t @@ -124,7 +131,8 @@ module AddressAttributes : sig val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t - val replace_must_be_valid_reason : Invalidation.must_be_valid_reason -> AbstractValue.t -> t -> t + val replace_must_be_valid_reason : + PathContext.t -> Invalidation.must_be_valid_reason -> AbstractValue.t -> t -> t val allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t @@ -149,7 +157,8 @@ module AddressAttributes : sig val find_opt : AbstractValue.t -> t -> Attributes.t option val check_valid_isl : - Trace.t + PathContext.t + -> Trace.t -> AbstractValue.t -> ?null_noop:bool -> t diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 54103557c..6f14a1385 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -7,6 +7,7 @@ open! IStd module F = Format module Invalidation = PulseInvalidation +module PathContext = PulsePathContext module Trace = PulseTrace module ValueHistory = PulseValueHistory @@ -34,7 +35,7 @@ module Attribute = struct | Invalid of Invalidation.t * Trace.t | ISLAbduced of Trace.t | MustBeInitialized of Trace.t - | MustBeValid of Trace.t * Invalidation.must_be_valid_reason option + | MustBeValid of PathContext.timestamp * Trace.t * Invalidation.must_be_valid_reason option | StdVectorReserve | Uninitialized | UnreachableAt of Location.t @@ -64,7 +65,7 @@ module Attribute = struct Variants.to_rank (Invalid (Invalidation.ConstantDereference IntLit.zero, dummy_trace)) - let must_be_valid_rank = Variants.to_rank (MustBeValid (dummy_trace, None)) + let must_be_valid_rank = Variants.to_rank (MustBeValid (PathContext.t0, dummy_trace, None)) let std_vector_reserve_rank = Variants.to_rank StdVectorReserve @@ -128,10 +129,11 @@ module Attribute = struct F.fprintf f "MustBeInitialized %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "read")) trace - | MustBeValid (trace, reason) -> - F.fprintf f "MustBeValid %a (%a)" + | MustBeValid (timestamp, trace, reason) -> + F.fprintf f "MustBeValid(%a, %a, t=%d)" (Trace.pp ~pp_immediate:(pp_string_if_debug "access")) trace Invalidation.pp_must_be_valid_reason reason + (timestamp :> int) | StdVectorReserve -> F.pp_print_string f "std::vector::reserve()" | Uninitialized -> @@ -176,7 +178,7 @@ module Attribute = struct true - let add_call proc_name call_location caller_history attr = + let add_call path proc_name call_location caller_history attr = let add_call_to_trace in_call = Trace.ViaCall {f= Call proc_name; location= call_location; history= caller_history; in_call} in @@ -197,8 +199,8 @@ module Attribute = struct Invalid (invalidation, add_call_to_trace trace) | ISLAbduced trace -> ISLAbduced (add_call_to_trace trace) - | MustBeValid (trace, reason) -> - MustBeValid (add_call_to_trace trace, reason) + | MustBeValid (_timestamp, trace, reason) -> + MustBeValid (path.PathContext.timestamp, add_call_to_trace trace, reason) | MustBeInitialized trace -> MustBeInitialized (add_call_to_trace trace) | WrittenTo trace -> @@ -227,8 +229,8 @@ module Attributes = struct let get_must_be_valid attrs = Set.find_rank attrs Attribute.must_be_valid_rank |> Option.map ~f:(fun attr -> - let[@warning "-8"] (Attribute.MustBeValid (trace, reason)) = attr in - (trace, reason) ) + let[@warning "-8"] (Attribute.MustBeValid (timestamp, trace, reason)) = attr in + (timestamp, trace, reason) ) let get_written_to attrs = @@ -335,8 +337,9 @@ module Attributes = struct Set.add acc attr1 ) - let add_call proc_name call_location caller_history attrs = - Set.map attrs ~f:(fun attr -> Attribute.add_call proc_name call_location caller_history attr) + let add_call path proc_name call_location caller_history attrs = + Set.map attrs ~f:(fun attr -> + Attribute.add_call path proc_name call_location caller_history attr ) include Set diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 3f702fa92..686942c20 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -7,6 +7,7 @@ open! IStd module F = Format module Invalidation = PulseInvalidation +module PathContext = PulsePathContext module Trace = PulseTrace module ValueHistory = PulseValueHistory @@ -21,7 +22,7 @@ type t = | Invalid of Invalidation.t * Trace.t | ISLAbduced of Trace.t (** The allocation is abduced so as the analysis could run normally *) | MustBeInitialized of Trace.t - | MustBeValid of Trace.t * Invalidation.must_be_valid_reason option + | MustBeValid of PathContext.timestamp * Trace.t * Invalidation.must_be_valid_reason option | StdVectorReserve | Uninitialized | UnreachableAt of Location.t @@ -53,7 +54,8 @@ module Attributes : sig val get_isl_abduced : t -> Trace.t option - val get_must_be_valid : t -> (Trace.t * Invalidation.must_be_valid_reason option) option + val get_must_be_valid : + t -> (PathContext.timestamp * Trace.t * Invalidation.must_be_valid_reason option) option val get_written_to : t -> Trace.t option @@ -75,5 +77,5 @@ module Attributes : sig (** While applying a spec, replacing ISLAbduced by Allocated and Invalidation.Cfree by Invalidation.delete, if applicable *) - val add_call : Procname.t -> Location.t -> ValueHistory.t -> t -> t + val add_call : PathContext.t -> Procname.t -> Location.t -> ValueHistory.t -> t -> t end diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index 36d6712de..2356dd147 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -118,8 +118,8 @@ let remove_isl_abduced_attr address memory = let remove_must_be_valid_attr address memory = match get_attribute Attributes.get_must_be_valid address memory with - | Some (trace, reason) -> - remove_one address (Attribute.MustBeValid (trace, reason)) memory + | Some (timestamp, trace, reason) -> + remove_one address (Attribute.MustBeValid (timestamp, trace, reason)) memory | None -> memory diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index 78845a342..d7783e677 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -42,7 +42,9 @@ val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option val get_invalid : AbstractValue.t -> t -> (Invalidation.t * Trace.t) option val get_must_be_valid : - AbstractValue.t -> t -> (Trace.t * Invalidation.must_be_valid_reason option) option + AbstractValue.t + -> t + -> (PathContext.timestamp * Trace.t * Invalidation.must_be_valid_reason option) option val is_must_be_valid_or_allocated_isl : AbstractValue.t -> t -> bool diff --git a/infer/src/pulse/PulseBasicInterface.ml b/infer/src/pulse/PulseBasicInterface.ml index 4a860a6ed..45c3fa1ca 100644 --- a/infer/src/pulse/PulseBasicInterface.ml +++ b/infer/src/pulse/PulseBasicInterface.ml @@ -16,6 +16,7 @@ module CallEvent = PulseCallEvent module Diagnostic = PulseDiagnostic module Invalidation = PulseInvalidation module PathCondition = PulsePathCondition +module PathContext = PulsePathContext module SatUnsat = PulseSatUnsat module SkippedCalls = PulseSkippedCalls module Trace = PulseTrace @@ -36,6 +37,7 @@ include struct [@@deprecated "use the short form Invalidation instead"] module PulsePathCondition = PulsePathCondition [@@deprecated "use the short form PathCondition instead"] + module PulsePathContext = PulsePathContext [@@deprecated "use the short form PathContext instead"] module PulseSkippedCalls = PulseSkippedCalls [@@deprecated "use the short form SkippedCalls instead"] module PulseTrace = PulseTrace [@@deprecated "use the short form Trace instead"] diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml index 1f7de9ef2..8b4d6ea47 100644 --- a/infer/src/pulse/PulseCallOperations.ml +++ b/infer/src/pulse/PulseCallOperations.ml @@ -83,11 +83,11 @@ let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate = |> havoc_ret ret |> add_skipped_proc -let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret +let apply_callee tenv path ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret ~captured_vars_with_actuals ~formals ~actuals astate = let map_call_result ~is_isl_error_prepost callee_prepost ~f = match - PulseInterproc.apply_prepost ~is_isl_error_prepost callee_pname call_loc ~callee_prepost + PulseInterproc.apply_prepost path ~is_isl_error_prepost callee_pname call_loc ~callee_prepost ~captured_vars_with_actuals ~formals ~actuals astate with | (Sat (Error _) | Unsat) as path_result -> @@ -194,8 +194,8 @@ let conservatively_initialize_args arg_values ({AbductiveDomain.post} as astate) AbstractValue.Set.fold AbductiveDomain.initialize reachable_values astate -let call_aux tenv caller_proc_desc call_loc callee_pname ret actuals callee_proc_desc exec_states - (astate : AbductiveDomain.t) = +let call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals callee_proc_desc + exec_states (astate : AbductiveDomain.t) = let formals = Procdesc.get_formals callee_proc_desc |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar) @@ -211,7 +211,7 @@ let call_aux tenv caller_proc_desc call_loc callee_pname ret actuals callee_proc | (actual_closure, _) :: _ when not (Procname.is_objc_block callee_pname || List.is_empty captured_vars) -> (* Assumption: the first parameter will be a closure *) - PulseOperations.get_captured_actuals call_loc ~captured_vars ~actual_closure astate + PulseOperations.get_captured_actuals path call_loc ~captured_vars ~actual_closure astate | _ -> Ok (astate, []) in @@ -228,7 +228,7 @@ let call_aux tenv caller_proc_desc call_loc callee_pname ret actuals callee_proc else (* apply all pre/post specs *) match - apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state + apply_callee tenv path ~caller_proc_desc callee_pname call_loc callee_exec_state ~captured_vars_with_actuals ~formals ~actuals ~ret astate with | Unsat -> @@ -238,7 +238,7 @@ let call_aux tenv caller_proc_desc call_loc callee_pname ret actuals callee_proc post :: posts ) -let call tenv ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc +let call tenv path ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) = (* a special case for objc nil messaging *) let unknown_objc_nil_messaging astate_unknown procdesc = @@ -254,7 +254,7 @@ let call tenv ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) op (ExecutionDomain.mk_initial tenv procdesc) |> Option.value_map ~default:[] ~f:(fun nil_summary -> let<*> nil_astate = nil_summary in - call_aux tenv caller_proc_desc call_loc callee_pname ret actuals procdesc + call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals procdesc ([ContinueProgram nil_astate] :> ExecutionDomain.t list) astate ) in @@ -262,7 +262,7 @@ let call tenv ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) op in match callee_data with | Some (callee_proc_desc, exec_states) -> - call_aux tenv caller_proc_desc call_loc callee_pname ret actuals callee_proc_desc + call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals callee_proc_desc (exec_states :> ExecutionDomain.t list) astate | None -> diff --git a/infer/src/pulse/PulseCallOperations.mli b/infer/src/pulse/PulseCallOperations.mli index af4da9ca4..c8ed96304 100644 --- a/infer/src/pulse/PulseCallOperations.mli +++ b/infer/src/pulse/PulseCallOperations.mli @@ -13,6 +13,7 @@ type t = AbductiveDomain.t val call : Tenv.t + -> PathContext.t -> caller_proc_desc:Procdesc.t -> callee_data:(Procdesc.t * PulseSummary.t) option -> Location.t diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 98938f159..9b7a6bb44 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -84,14 +84,14 @@ let pp_contradiction fmt = function exception Contradiction of contradiction -let fold_globals_of_stack call_loc stack call_state ~f = +let fold_globals_of_stack path call_loc stack call_state ~f = Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold BaseStack.fold) stack ~init:call_state ~f:(fun call_state (var, stack_value) -> match var with | Var.ProgramVar pvar when Pvar.is_global pvar -> let call_state, addr_hist_caller = let astate, var_value = - Stack.eval call_loc + Stack.eval path call_loc [ValueHistory.VariableAccessed (pvar, call_loc)] var call_state.astate in @@ -252,8 +252,8 @@ let materialize_pre_for_parameters callee_proc_name call_location pre_post ~form result -let materialize_pre_for_globals callee_proc_name call_location pre_post call_state = - fold_globals_of_stack call_location (pre_post.AbductiveDomain.pre :> BaseDomain.t).stack +let materialize_pre_for_globals path callee_proc_name call_location pre_post call_state = + fold_globals_of_stack path call_location (pre_post.AbductiveDomain.pre :> BaseDomain.t).stack call_state ~f:(fun _var ~stack_value:(addr_pre, _) ~addr_hist_caller call_state -> materialize_pre_from_address callee_proc_name call_location ~pre:(pre_post.AbductiveDomain.pre :> BaseDomain.t) @@ -281,11 +281,11 @@ let conjoin_callee_arith pre_post call_state = else {call_state with astate; subst} -let apply_arithmetic_constraints callee_proc_name call_location pre_post call_state = +let apply_arithmetic_constraints path callee_proc_name call_location pre_post call_state = let open IResult.Let_syntax in let one_address_sat callee_attrs (addr_caller, caller_history) call_state = let attrs_caller = - Attributes.add_call callee_proc_name call_location caller_history callee_attrs + Attributes.add_call path callee_proc_name call_location caller_history callee_attrs in let astate = AddressAttributes.abduce_and_add addr_caller attrs_caller call_state.astate in if phys_equal astate call_state.astate then call_state else {call_state with astate} @@ -332,8 +332,8 @@ let apply_arithmetic_constraints callee_proc_name call_location pre_post call_st call_state.subst call_state -let materialize_pre callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals - ~actuals call_state = +let materialize_pre path callee_proc_name call_location pre_post ~captured_vars_with_actuals + ~formals ~actuals call_state = PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call pre" ())) ; let r = let open IResult.Let_syntax in @@ -342,10 +342,10 @@ let materialize_pre callee_proc_name call_location pre_post ~captured_vars_with_ call_state >>= materialize_pre_for_captured_vars callee_proc_name call_location pre_post ~captured_vars_with_actuals - >>= materialize_pre_for_globals callee_proc_name call_location pre_post + >>= materialize_pre_for_globals path callee_proc_name call_location pre_post >>= (* ...then relational arithmetic constraints in the callee's attributes will make sense in terms of the caller's values *) - apply_arithmetic_constraints callee_proc_name call_location pre_post + apply_arithmetic_constraints path callee_proc_name call_location pre_post in PerfEvent.(log (fun logger -> log_end_event logger ())) ; r @@ -386,11 +386,11 @@ let delete_edges_in_callee_pre_from_caller ~edges_pre_opt addr_caller call_state (subst, post_edges) ) -let record_post_cell callee_proc_name call_loc ~edges_pre_opt +let record_post_cell path callee_proc_name call_loc ~edges_pre_opt ~cell_callee_post:(edges_callee_post, attrs_callee_post) (addr_caller, hist_caller) call_state = let call_state = let attrs_post_caller = - Attributes.add_call callee_proc_name call_loc hist_caller attrs_callee_post + Attributes.add_call path callee_proc_name call_loc hist_caller attrs_callee_post in let astate = if Config.pulse_isl then @@ -427,8 +427,8 @@ let record_post_cell callee_proc_name call_loc ~edges_pre_opt ; astate= AbductiveDomain.set_post_edges addr_caller edges_post_caller call_state.astate } -let rec record_post_for_address callee_proc_name call_loc ({AbductiveDomain.pre; _} as pre_post) - ~addr_callee ~addr_hist_caller call_state = +let rec record_post_for_address path callee_proc_name call_loc + ({AbductiveDomain.pre; _} as pre_post) ~addr_callee ~addr_hist_caller call_state = L.d_printfln "%a<->%a" AbstractValue.pp addr_callee AbstractValue.pp (fst addr_hist_caller) ; match visit call_state ~pre:(pre :> BaseDomain.t) ~addr_callee ~addr_hist_caller with | `AlreadyVisited, call_state -> @@ -454,7 +454,7 @@ let rec record_post_for_address callee_proc_name call_loc ({AbductiveDomain.pre; Attributes.replace_isl_abduced attrs_post attrs_caller else attrs_post in - record_post_cell callee_proc_name call_loc ~edges_pre_opt addr_hist_caller + record_post_cell path callee_proc_name call_loc ~edges_pre_opt addr_hist_caller ~cell_callee_post:(edges_post, attrs_post) call_state in Memory.Edges.fold ~init:call_state_after_post edges_post @@ -463,11 +463,11 @@ let rec record_post_for_address callee_proc_name call_loc ({AbductiveDomain.pre; call_state_subst_find_or_new call_state addr_callee_dest ~default_hist_caller:(snd addr_hist_caller) in - record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:addr_callee_dest - ~addr_hist_caller:addr_hist_curr_dest call_state ) ) + record_post_for_address path callee_proc_name call_loc pre_post + ~addr_callee:addr_callee_dest ~addr_hist_caller:addr_hist_curr_dest call_state ) ) -let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual:(actual, typ) +let record_post_for_actual path callee_proc_name call_loc pre_post ~formal ~actual:(actual, typ) call_state = L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal AbstractValue.pp (fst actual) ; match @@ -479,7 +479,7 @@ let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual:(a deref_non_c_struct addr_formal_pre typ (pre_post.AbductiveDomain.pre :> BaseDomain.t).BaseDomain.heap in - record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:formal_pre + record_post_for_address path callee_proc_name call_loc pre_post ~addr_callee:formal_pre ~addr_hist_caller:actual call_state with | Some call_state -> @@ -488,7 +488,7 @@ let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual:(a call_state -let record_post_for_return callee_proc_name call_loc pre_post call_state = +let record_post_for_return path callee_proc_name call_loc pre_post call_state = let return_var = Var.of_pvar (Pvar.get_ret_pvar callee_proc_name) in match BaseStack.find_opt return_var (pre_post.AbductiveDomain.post :> BaseDomain.t).stack with | None -> @@ -517,13 +517,14 @@ let record_post_for_return callee_proc_name call_loc pre_post call_state = L.d_printfln_escaped "Recording POST from [return] <-> %a" AbstractValue.pp (fst return_caller_addr_hist) ; let call_state = - record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:return_callee + record_post_for_address path callee_proc_name call_loc pre_post ~addr_callee:return_callee ~addr_hist_caller:return_caller_addr_hist call_state in (call_state, Some return_caller_addr_hist) ) -let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state = +let apply_post_for_parameters path callee_proc_name call_location pre_post ~formals ~actuals + call_state = (* for each [(formal_i, actual_i)] pair, do [post_i = post union subst(graph reachable from formal_i in post)], deleting previous info when comparing pre and post shows a difference (TODO: record in the pre when a location is written to instead of just comparing values @@ -531,7 +532,8 @@ let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~ post but nuke other fields in the meantime? is that possible?). *) match List.fold2 formals actuals ~init:call_state ~f:(fun call_state formal actual -> - record_post_for_actual callee_proc_name call_location pre_post ~formal ~actual call_state ) + record_post_for_actual path callee_proc_name call_location pre_post ~formal ~actual + call_state ) with | Unequal_lengths -> (* should have been checked before by [materialize_pre] *) @@ -540,18 +542,18 @@ let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~ call_state -let apply_post_for_captured_vars callee_proc_name call_location pre_post ~captured_vars_with_actuals - call_state = +let apply_post_for_captured_vars path callee_proc_name call_location pre_post + ~captured_vars_with_actuals call_state = List.fold captured_vars_with_actuals ~init:call_state ~f:(fun call_state (formal, actual) -> - record_post_for_actual callee_proc_name call_location pre_post ~formal ~actual call_state ) + record_post_for_actual path callee_proc_name call_location pre_post ~formal ~actual call_state ) -let apply_post_for_globals callee_proc_name call_location pre_post call_state = +let apply_post_for_globals path callee_proc_name call_location pre_post call_state = match - fold_globals_of_stack call_location (pre_post.AbductiveDomain.pre :> BaseDomain.t).stack + fold_globals_of_stack path call_location (pre_post.AbductiveDomain.pre :> BaseDomain.t).stack call_state ~f:(fun _var ~stack_value:(addr_callee, _) ~addr_hist_caller call_state -> Ok - (record_post_for_address callee_proc_name call_location pre_post ~addr_callee + (record_post_for_address path callee_proc_name call_location pre_post ~addr_callee ~addr_hist_caller call_state) ) with | Error _ -> @@ -560,7 +562,7 @@ let apply_post_for_globals callee_proc_name call_location pre_post call_state = call_state -let record_post_remaining_attributes callee_proc_name call_loc pre_post call_state = +let record_post_remaining_attributes path callee_proc_name call_loc pre_post call_state = BaseAddressAttributes.fold (fun addr_callee attrs call_state -> if AddressSet.mem addr_callee call_state.visited then @@ -571,7 +573,7 @@ let record_post_remaining_attributes callee_proc_name call_loc pre_post call_sta | None -> (* callee address has no meaning for the caller *) call_state | Some (addr_caller, history) -> - let attrs' = Attributes.add_call callee_proc_name call_loc history attrs in + let attrs' = Attributes.add_call path callee_proc_name call_loc history attrs in let astate = AddressAttributes.abduce_and_add addr_caller attrs' call_state.astate in {call_state with astate} ) (pre_post.AbductiveDomain.post :> BaseDomain.t).attrs call_state @@ -587,20 +589,21 @@ let record_skipped_calls callee_proc_name call_loc pre_post call_state = {call_state with astate} -let apply_post callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals ~actuals - call_state = +let apply_post path callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals + ~actuals call_state = let open IResult.Let_syntax in PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ; let r = let call_state, return_caller = - apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state - |> apply_post_for_captured_vars callee_proc_name call_location pre_post + apply_post_for_parameters path callee_proc_name call_location pre_post ~formals ~actuals + call_state + |> apply_post_for_captured_vars path callee_proc_name call_location pre_post ~captured_vars_with_actuals - |> apply_post_for_globals callee_proc_name call_location pre_post - |> record_post_for_return callee_proc_name call_location pre_post + |> apply_post_for_globals path callee_proc_name call_location pre_post + |> record_post_for_return path callee_proc_name call_location pre_post in let+ call_state = - record_post_remaining_attributes callee_proc_name call_location pre_post call_state + record_post_remaining_attributes path callee_proc_name call_location pre_post call_state |> record_skipped_calls callee_proc_name call_location pre_post |> conjoin_callee_arith pre_post in @@ -610,50 +613,78 @@ let apply_post callee_proc_name call_location pre_post ~captured_vars_with_actua r -let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call_state = - AddressMap.fold - (fun addr_pre (addr_caller, hist_caller) astate_result -> - let mk_access_trace callee_access_trace = - Trace.ViaCall - { in_call= callee_access_trace - ; f= Call callee_proc_name - ; location= call_location - ; history= hist_caller } - in - let open IResult.Let_syntax in - let* astate = astate_result in - let* astate = - match BaseAddressAttributes.get_must_be_valid addr_pre (pre :> BaseDomain.t).attrs with +let check_all_valid path callee_proc_name call_location {AbductiveDomain.pre; _} call_state = + (* collect all the checks to perform then do each check in timestamp order to make sure we report + the first issue if any *) + let addresses_to_check = + AddressMap.fold + (fun addr_pre addr_hist_caller to_check -> + let to_check = + match BaseAddressAttributes.get_must_be_valid addr_pre (pre :> BaseDomain.t).attrs with + | None -> + to_check + | Some must_be_valid_data -> + (addr_hist_caller, `MustBeValid must_be_valid_data) :: to_check + in + match + BaseAddressAttributes.get_must_be_initialized addr_pre (pre :> BaseDomain.t).attrs + with | None -> - astate_result - | Some (callee_access_trace, must_be_valid_reason) -> - let access_trace = mk_access_trace callee_access_trace in - AddressAttributes.check_valid access_trace addr_caller astate - |> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> - L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ; - AccessResult.ReportableError - { diagnostic= - Diagnostic.AccessToInvalidAddress - { calling_context= [] - ; invalidation - ; invalidation_trace - ; access_trace - ; must_be_valid_reason } - ; astate } ) - in - match BaseAddressAttributes.get_must_be_initialized addr_pre (pre :> BaseDomain.t).attrs with - | None -> - astate_result - | Some callee_access_trace -> - let access_trace = mk_access_trace callee_access_trace in - AddressAttributes.check_initialized access_trace addr_caller astate - |> Result.map_error ~f:(fun () -> - L.d_printfln "ERROR: caller's %a is uninitialized!" AbstractValue.pp addr_caller ; - AccessResult.ReportableError - { diagnostic= - Diagnostic.ReadUninitializedValue {calling_context= []; trace= access_trace} - ; astate } ) ) - call_state.subst (Ok call_state.astate) + to_check + | Some must_be_init_data -> + (addr_hist_caller, `MustBeInitialized must_be_init_data) :: to_check ) + call_state.subst [] + in + let timestamp_of_check = function + | `MustBeValid (timestamp, _, _) -> + Some timestamp + | `MustBeInitialized _ -> + None + in + List.sort addresses_to_check ~compare:(fun (_, check1) (_, check2) -> + match (timestamp_of_check check1, timestamp_of_check check2) with + | Some t1, Some t2 -> + (* smaller timestamp first *) PathContext.compare_timestamp t1 t2 + (* with a timestamp first (gone soon when MustBeInitialized will get a timestamp too), otherwise dummy comparison *) + | None, None -> + 0 + | Some _, None -> + -1 + | None, Some _ -> + 1 ) + |> List.fold_result ~init:call_state.astate ~f:(fun astate ((addr_caller, hist_caller), check) -> + let mk_access_trace callee_access_trace = + Trace.ViaCall + { in_call= callee_access_trace + ; f= Call callee_proc_name + ; location= call_location + ; history= hist_caller } + in + match check with + | `MustBeValid (_timestamp, callee_access_trace, must_be_valid_reason) -> + let access_trace = mk_access_trace callee_access_trace in + AddressAttributes.check_valid path access_trace addr_caller astate + |> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> + L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ; + AccessResult.ReportableError + { diagnostic= + Diagnostic.AccessToInvalidAddress + { calling_context= [] + ; invalidation + ; invalidation_trace + ; access_trace + ; must_be_valid_reason } + ; astate } ) + | `MustBeInitialized callee_access_trace -> + let access_trace = mk_access_trace callee_access_trace in + AddressAttributes.check_initialized access_trace addr_caller astate + |> Result.map_error ~f:(fun () -> + L.d_printfln "ERROR: caller's %a is uninitialized!" AbstractValue.pp addr_caller ; + AccessResult.ReportableError + { diagnostic= + Diagnostic.ReadUninitializedValue + {calling_context= []; trace= access_trace} + ; astate } ) ) let isl_check_all_invalid invalid_addr_callers callee_proc_name call_location @@ -704,7 +735,7 @@ let isl_check_all_invalid invalid_addr_callers callee_proc_name call_location - for each actual, write the post for that actual - if aliasing is introduced at any time then give up *) -let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_prepost:pre_post +let apply_prepost path ~is_isl_error_prepost callee_proc_name call_location ~callee_prepost:pre_post ~captured_vars_with_actuals ~formals ~actuals astate = L.d_printfln "Applying pre/post for %a(%a):@\n%a" Procname.pp callee_proc_name (Pp.seq ~sep:"," Var.pp) formals AbductiveDomain.pp pre_post ; @@ -717,8 +748,8 @@ let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_p in (* read the precondition *) match - materialize_pre callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals - ~actuals empty_call_state + materialize_pre path callee_proc_name call_location pre_post ~captured_vars_with_actuals + ~formals ~actuals empty_call_state with | exception Contradiction reason -> (* can't make sense of the pre-condition in the current context: give up on that particular @@ -738,7 +769,7 @@ let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_p ContinueProgram ok specs *) let* astate = if Config.pulse_isl then Ok astate - else check_all_valid callee_proc_name call_location pre_post call_state + else check_all_valid path callee_proc_name call_location pre_post call_state in (* reset [visited] *) let invalid_subst = call_state.invalid_subst in @@ -746,8 +777,8 @@ let apply_prepost ~is_isl_error_prepost callee_proc_name call_location ~callee_p let call_state = {call_state with astate; visited= AddressSet.empty} in (* apply the postcondition *) let* call_state, return_caller = - apply_post callee_proc_name call_location pre_post ~captured_vars_with_actuals ~formals - ~actuals call_state + apply_post path callee_proc_name call_location pre_post ~captured_vars_with_actuals + ~formals ~actuals call_state in let astate = if Topl.is_active () then diff --git a/infer/src/pulse/PulseInterproc.mli b/infer/src/pulse/PulseInterproc.mli index 8af5e7076..5cd8ff23c 100644 --- a/infer/src/pulse/PulseInterproc.mli +++ b/infer/src/pulse/PulseInterproc.mli @@ -10,7 +10,8 @@ open PulseBasicInterface open PulseDomainInterface val apply_prepost : - is_isl_error_prepost:bool + PathContext.t + -> is_isl_error_prepost:bool -> Procname.t -> Location.t -> callee_prepost:AbductiveDomain.t diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 0c4ce3556..f08cbd6a2 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -14,6 +14,7 @@ type arg_payload = AbstractValue.t * ValueHistory.t type model_data = { analysis_data: PulseSummary.t InterproceduralAnalysis.t + ; path: PathContext.t ; callee_procname: Procname.t ; location: Location.t ; ret: Ident.t * Typ.t } @@ -25,27 +26,27 @@ 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 shallow_copy_value path location event ret_id dest_pointer_hist src_value_hist astate = + let<*> astate, obj_copy = PulseOperations.shallow_copy path location src_value_hist astate in let<+> astate = - PulseOperations.write_deref location ~ref:dest_pointer_hist + PulseOperations.write_deref path location ~ref:dest_pointer_hist ~obj:(fst obj_copy, event :: snd obj_copy) astate in PulseOperations.havoc_id ret_id [event] astate - let shallow_copy location event ret_id dest_pointer_hist src_pointer_hist astate = + let shallow_copy path location event ret_id dest_pointer_hist src_pointer_hist astate = let<*> astate, obj = - PulseOperations.eval_access Read location src_pointer_hist Dereference astate + PulseOperations.eval_access path Read location src_pointer_hist Dereference astate in - shallow_copy_value location event ret_id dest_pointer_hist obj astate + shallow_copy_value path location event ret_id dest_pointer_hist obj astate let shallow_copy_model model_desc dest_pointer_hist src_pointer_hist : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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 + shallow_copy path location event ret_id dest_pointer_hist src_pointer_hist astate let early_exit : model = @@ -124,7 +125,7 @@ module Misc = struct let free_or_delete operation deleted_access : model = - fun {location} astate -> + fun {path; 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 @@ -132,13 +133,14 @@ module Misc = struct let astates_alloc = let<*> astate = PulseArithmetic.and_positive (fst deleted_access) astate in if Config.pulse_isl then - PulseOperations.invalidate_biad_isl location invalidation deleted_access astate + PulseOperations.invalidate_biad_isl path location invalidation deleted_access astate |> List.map ~f:(fun result -> let+ astate = result in ContinueProgram astate ) else let<+> astate = - PulseOperations.invalidate UntraceableAccess location invalidation deleted_access astate + PulseOperations.invalidate path UntraceableAccess location invalidation deleted_access + astate in astate in @@ -177,7 +179,7 @@ module C = struct let malloc_common ~size_exp_opt : model = - fun {analysis_data= {tenv}; callee_procname; location; ret= ret_id, _} astate -> + fun {path; analysis_data= {tenv}; callee_procname; location; ret= ret_id, _} astate -> let ret_addr = AbstractValue.mk_fresh () in let<*> astate_alloc = let ret_alloc_hist = @@ -196,7 +198,7 @@ module C = struct let+ astate_null = PulseOperations.write_id ret_id ret_null_value astate |> PulseArithmetic.and_eq_int ret_addr IntLit.zero - >>= PulseOperations.invalidate + >>= PulseOperations.invalidate path (StackAddress (Var.of_id ret_id, ret_null_hist)) location (ConstantDereference IntLit.zero) ret_null_value in @@ -253,33 +255,33 @@ end module ObjC = struct let dispatch_sync args : model = - fun {analysis_data= {analyze_dependency; tenv; proc_desc}; location; ret} astate -> + fun {path; analysis_data= {analyze_dependency; tenv; proc_desc}; location; ret} astate -> match List.last args with | None -> ok_continue astate | Some {ProcnameDispatcher.Call.FuncArg.arg_payload= lambda_ptr_hist} -> ( let<*> astate, (lambda, _) = - PulseOperations.eval_access Read location lambda_ptr_hist Dereference astate + PulseOperations.eval_access path Read location lambda_ptr_hist Dereference astate in match AddressAttributes.get_closure_proc_name lambda astate with | None -> ok_continue astate | Some callee_proc_name -> - PulseCallOperations.call tenv ~caller_proc_desc:proc_desc + PulseCallOperations.call tenv path ~caller_proc_desc:proc_desc ~callee_data:(analyze_dependency callee_proc_name) location callee_proc_name ~ret ~actuals:[] ~formals_opt:None astate ) let insertion_into_collection_key_and_value (value, value_hist) (key, key_hist) ~desc : model = - fun {location} astate -> + fun {path; location} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let<*> astate, _ = - PulseOperations.eval_access ~must_be_valid_reason:InsertionIntoCollection Read location + PulseOperations.eval_access path ~must_be_valid_reason:InsertionIntoCollection Read location (value, event :: value_hist) Dereference astate in let<+> astate, _ = - PulseOperations.eval_access ~must_be_valid_reason:InsertionIntoCollection Read location + PulseOperations.eval_access path ~must_be_valid_reason:InsertionIntoCollection Read location (key, event :: key_hist) Dereference astate in @@ -287,10 +289,10 @@ module ObjC = struct let insertion_into_collection_key_or_value (value, value_hist) ~desc : model = - fun {location} astate -> + fun {path; location} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let<+> astate, _ = - PulseOperations.eval_access ~must_be_valid_reason:InsertionIntoCollection Read location + PulseOperations.eval_access path ~must_be_valid_reason:InsertionIntoCollection Read location (value, event :: value_hist) Dereference astate in @@ -302,33 +304,35 @@ module Optional = struct let internal_value_access = HilExp.Access.FieldAccess internal_value - let to_internal_value mode location optional astate = - PulseOperations.eval_access mode location optional internal_value_access astate + let to_internal_value path mode location optional astate = + PulseOperations.eval_access path mode location optional internal_value_access astate - let to_internal_value_deref mode location optional astate = - let* astate, pointer = to_internal_value Read location optional astate in - PulseOperations.eval_access mode location pointer Dereference astate + let to_internal_value_deref path mode location optional astate = + let* astate, pointer = to_internal_value path Read location optional astate in + PulseOperations.eval_access path mode location pointer Dereference astate - let write_value location this ~value ~desc astate = + let write_value path location this ~value ~desc astate = let event = ValueHistory.Call {f= Model desc; location; in_call= []} in - let* astate, value_field = to_internal_value Read location this astate in + let* astate, value_field = to_internal_value path Read location this astate in let value_hist = (fst value, event :: snd value) in - let+ astate = PulseOperations.write_deref location ~ref:value_field ~obj:value_hist astate in + let+ astate = + PulseOperations.write_deref path location ~ref:value_field ~obj:value_hist astate + in (astate, value_field, value_hist) - let assign_value_fresh location this ~desc astate = - write_value location this ~value:(AbstractValue.mk_fresh (), []) ~desc astate + let assign_value_fresh path location this ~desc astate = + write_value path location this ~value:(AbstractValue.mk_fresh (), []) ~desc astate let assign_none this ~desc : model = - fun {location} astate -> - let<*> astate, pointer, value = assign_value_fresh location this ~desc astate in + fun {path; location} astate -> + let<*> astate, pointer, value = assign_value_fresh path location this ~desc astate in let<*> astate = PulseArithmetic.and_eq_int (fst value) IntLit.zero astate in let<+> astate = - PulseOperations.invalidate + PulseOperations.invalidate path (MemoryAccess {pointer; access= Dereference; hist_obj_default= snd value}) location OptionalEmpty value astate in @@ -336,42 +340,42 @@ module Optional = struct let assign_value this _value ~desc : model = - fun {location} astate -> + fun {path; location} astate -> (* TODO: call the copy constructor of a value *) - let<*> astate, _, value = assign_value_fresh location this ~desc astate in + let<*> astate, _, value = assign_value_fresh path location this ~desc astate in let<+> astate = PulseArithmetic.and_positive (fst value) astate in astate let assign_optional_value this init ~desc : model = - 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 + fun {path; location} astate -> + let<*> astate, value = to_internal_value_deref path Read location init astate in + let<+> astate, _, _ = write_value path location this ~value ~desc astate in astate let emplace optional ~desc : model = - fun {location} astate -> - let<+> astate, _, _ = assign_value_fresh location optional ~desc astate in + fun {path; location} astate -> + let<+> astate, _, _ = assign_value_fresh path location optional ~desc astate in astate let value optional ~desc : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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 + to_internal_value_deref path 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 path Write location value Dereference astate in PulseOperations.write_id ret_id (value_addr, event :: value_hist) astate |> ok_continue let has_value optional ~desc : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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 path Read location optional astate in let astate = PulseOperations.write_id ret_id ret_value astate in let<*> astate_non_empty = PulseArithmetic.prune_positive value_addr astate in let<*> astate_true = PulseArithmetic.prune_positive ret_addr astate_non_empty in @@ -381,9 +385,9 @@ module Optional = struct let get_pointer optional ~desc : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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 path 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 @@ -394,7 +398,7 @@ module Optional = struct PulseOperations.write_id ret_id nullptr astate |> PulseArithmetic.prune_eq_zero (fst value_addr) >>= PulseArithmetic.and_eq_int (fst nullptr) IntLit.zero - >>= PulseOperations.invalidate + >>= PulseOperations.invalidate path (StackAddress (Var.of_id ret_id, snd nullptr)) location (ConstantDereference IntLit.zero) nullptr in @@ -402,17 +406,17 @@ module Optional = struct let value_or optional default ~desc : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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 path Read location optional astate in let<*> astate_non_empty = PulseArithmetic.prune_positive (fst value_addr) astate in let<*> astate_non_empty, value = - PulseOperations.eval_access Read location value_addr Dereference astate_non_empty + PulseOperations.eval_access path 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) = - PulseOperations.eval_access Read location default Dereference astate + PulseOperations.eval_access path Read location default Dereference astate in let default_value_hist = (default_val, event :: default_hist) in let<*> astate_empty = PulseArithmetic.prune_eq_zero (fst value_addr) astate in @@ -441,104 +445,111 @@ module StdAtomicInteger = struct "__infer_model_backing_int" - let load_backing_int location this astate = - let* astate, obj = PulseOperations.eval_access Read location this Dereference astate in + let load_backing_int path location this astate = + let* astate, obj = PulseOperations.eval_access path Read location this Dereference astate in let* astate, int_addr = - PulseOperations.eval_access Read location obj (FieldAccess internal_int) astate + PulseOperations.eval_access path Read location obj (FieldAccess internal_int) astate + in + let+ astate, int_val = + PulseOperations.eval_access path Read location int_addr Dereference astate in - let+ astate, int_val = PulseOperations.eval_access Read location int_addr Dereference astate in (astate, int_addr, int_val) let constructor this_address init_value : model = - fun {location} astate -> + fun {path; 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 = - PulseOperations.eval_access Write location this (FieldAccess internal_int) astate + PulseOperations.eval_access path 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 + let<*> astate = + PulseOperations.write_deref path location ~ref:int_field ~obj:init_value astate + in + let<+> astate = PulseOperations.write_deref path location ~ref:this_address ~obj:this astate in astate - let arith_bop prepost location event ret_id bop this operand astate = - let* astate, int_addr, (old_int, hist) = load_backing_int location this astate in + let arith_bop path prepost location event ret_id bop this operand astate = + let* astate, int_addr, (old_int, hist) = load_backing_int path location this astate in let bop_addr = AbstractValue.mk_fresh () in let* astate = PulseArithmetic.eval_binop bop_addr bop (AbstractValueOperand old_int) operand astate in let+ astate = - PulseOperations.write_deref location ~ref:int_addr ~obj:(bop_addr, event :: hist) astate + PulseOperations.write_deref path location ~ref:int_addr ~obj:(bop_addr, event :: hist) astate in let ret_int = match prepost with `Pre -> bop_addr | `Post -> old_int in PulseOperations.write_id ret_id (ret_int, event :: hist) astate let fetch_add this (increment, _) _memory_ordering : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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) + arith_bop path `Post location event ret_id (PlusA None) this (AbstractValueOperand increment) astate in astate let fetch_sub this (increment, _) _memory_ordering : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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) + arith_bop path `Post location event ret_id (MinusA None) this (AbstractValueOperand increment) astate in astate let operator_plus_plus_pre this : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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 + arith_bop path `Pre location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate in astate let operator_plus_plus_post this _int : model = - fun {location; ret= ret_id, _} astate -> + fun {path; location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model "std::atomic::operator++(T)"; location; in_call= []} in let<+> astate = - arith_bop `Post location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate + arith_bop path `Post location event ret_id (PlusA None) this (LiteralOperand IntLit.one) + astate in astate let operator_minus_minus_pre this : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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 + arith_bop path `Pre location event ret_id (MinusA None) this (LiteralOperand IntLit.one) + astate in astate let operator_minus_minus_post this _int : model = - fun {location; ret= ret_id, _} astate -> + fun {path; location; ret= ret_id, _} astate -> let event = ValueHistory.Call {f= Model "std::atomic::operator--(T)"; location; in_call= []} in let<+> astate = - arith_bop `Post location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate + arith_bop path `Post location event ret_id (MinusA None) this (LiteralOperand IntLit.one) + astate in astate let load_instr model_desc this _memory_ordering_opt : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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, _int_addr, (int, hist) = load_backing_int path location this astate in PulseOperations.write_id ret_id (int, event :: hist) astate @@ -546,43 +557,51 @@ module StdAtomicInteger = struct let operator_t = load_instr "std::atomic::operator_T()" - let store_backing_int location this_address new_value astate = - let* astate, this = PulseOperations.eval_access Read location this_address Dereference astate in + let store_backing_int path location this_address new_value astate = + let* astate, this = + PulseOperations.eval_access path Read location this_address Dereference astate + in let astate = AddressAttributes.add_one (fst this_address) (WrittenTo (Trace.Immediate {location; history= []})) astate in let* astate, int_field = - PulseOperations.eval_access Write location this (FieldAccess internal_int) astate + PulseOperations.eval_access path Write location this (FieldAccess internal_int) astate in - PulseOperations.write_deref location ~ref:int_field ~obj:new_value astate + PulseOperations.write_deref path location ~ref:int_field ~obj:new_value astate let store this_address (new_value, new_hist) _memory_ordering : model = - fun {location} astate -> + fun {path; 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 + let<+> astate = + store_backing_int path location this_address (new_value, event :: new_hist) astate + in astate let exchange this_address (new_value, new_hist) _memory_ordering : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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, _int_addr, (old_int, old_hist) = + load_backing_int path location this_address astate + in + let<+> astate = + store_backing_int path 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 (* naively modeled as shallow copy. *) let clone src_pointer_hist : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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 + PulseOperations.eval_access path Read location src_pointer_hist Dereference astate in - let<+> astate, obj_copy = PulseOperations.shallow_copy location obj astate in + let<+> astate, obj_copy = PulseOperations.shallow_copy path location obj astate in PulseOperations.write_id ret_id (fst obj_copy, event :: snd obj_copy) astate end @@ -595,31 +614,31 @@ module StdBasicString = struct let internal_string_access = HilExp.Access.FieldAccess internal_string - let to_internal_string location bstring astate = - PulseOperations.eval_access Read location bstring internal_string_access astate + let to_internal_string path location bstring astate = + PulseOperations.eval_access path Read location bstring internal_string_access astate let data this_hist : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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_addr_hist = to_internal_string path location this_hist astate in let<+> astate, (string, hist) = - PulseOperations.eval_access Read location string_addr_hist Dereference astate + PulseOperations.eval_access path Read location string_addr_hist Dereference astate in PulseOperations.write_id ret_id (string, event :: hist) astate let destructor this_hist : model = - fun {location} astate -> + fun {path; 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 + let<*> astate, (string_addr, string_hist) = to_internal_string path location this_hist astate in let string_addr_hist = (string_addr, call_event :: string_hist) in let<*> astate = - PulseOperations.invalidate_access location CppDelete string_addr_hist Dereference astate + PulseOperations.invalidate_access path location CppDelete string_addr_hist Dereference astate in let<+> astate = - PulseOperations.invalidate + PulseOperations.invalidate path (MemoryAccess { pointer= this_hist ; access= internal_string_access @@ -632,15 +651,15 @@ end module StdFunction = struct let operator_call ProcnameDispatcher.Call.FuncArg.{arg_payload= lambda_ptr_hist; typ} actuals : model = - fun {analysis_data= {analyze_dependency; tenv; proc_desc}; location; ret} astate -> + fun {path; 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] in let<*> astate, (lambda, _) = - PulseOperations.eval_access Read location lambda_ptr_hist Dereference astate + PulseOperations.eval_access path 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 path 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 *) @@ -651,26 +670,26 @@ module StdFunction = struct :: List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} -> (arg_payload, typ) ) in - PulseCallOperations.call tenv ~caller_proc_desc:proc_desc + PulseCallOperations.call tenv path ~caller_proc_desc:proc_desc ~callee_data:(analyze_dependency callee_proc_name) location callee_proc_name ~ret ~actuals ~formals_opt:None astate let assign dest ProcnameDispatcher.Call.FuncArg.{arg_payload= src; typ= src_typ} ~desc : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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 let<+> astate = - PulseOperations.write_deref location ~ref:dest ~obj:(empty_target, [event]) astate + PulseOperations.write_deref path 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 path location event ret_id dest src astate | _ -> - Misc.shallow_copy_value location event ret_id dest src astate + Misc.shallow_copy_value path location event ret_id dest src astate end module GenericArrayBackedCollection = struct @@ -682,31 +701,32 @@ module GenericArrayBackedCollection = struct let access = HilExp.Access.FieldAccess field - let eval mode location collection astate = - PulseOperations.eval_deref_access mode location collection access astate + let eval path mode location collection astate = + PulseOperations.eval_deref_access path mode location collection access astate - let eval_element location internal_array index astate = - PulseOperations.eval_access Read location internal_array + let eval_element path location internal_array index astate = + PulseOperations.eval_access path Read location internal_array (ArrayAccess (StdTyp.void, index)) astate - let element location collection index astate = - let* astate, internal_array = eval Read location collection astate in - eval_element location internal_array index astate + let element path location collection index astate = + let* astate, internal_array = eval path Read location collection astate in + eval_element path location internal_array index astate - let eval_pointer_to_last_element location collection astate = + let eval_pointer_to_last_element path location collection astate = let+ astate, pointer = - PulseOperations.eval_deref_access Write location collection (FieldAccess last_field) astate + PulseOperations.eval_deref_access path Write location collection (FieldAccess last_field) + astate in let astate = AddressAttributes.mark_as_end_of_collection (fst pointer) astate in (astate, pointer) - let eval_is_empty location collection astate = - PulseOperations.eval_deref_access Write location collection (FieldAccess is_empty) astate + let eval_is_empty path location collection astate = + PulseOperations.eval_deref_access path Write location collection (FieldAccess is_empty) astate end module GenericArrayBackedCollectionIterator = struct @@ -714,19 +734,23 @@ module GenericArrayBackedCollectionIterator = struct let internal_pointer_access = HilExp.Access.FieldAccess internal_pointer - let to_internal_pointer mode location iterator astate = - PulseOperations.eval_access mode location iterator internal_pointer_access astate + let to_internal_pointer path mode location iterator astate = + PulseOperations.eval_access path mode location iterator internal_pointer_access astate - let to_internal_pointer_deref mode location iterator astate = - let* astate, pointer = to_internal_pointer Read location iterator astate in - let+ astate, index = PulseOperations.eval_access mode location pointer Dereference astate in + let to_internal_pointer_deref path mode location iterator astate = + let* astate, pointer = to_internal_pointer path Read location iterator astate in + let+ astate, index = + PulseOperations.eval_access path mode location pointer Dereference astate + in (astate, pointer, index) - let to_elem_pointed_by_iterator mode ?(step = None) location iterator astate = - let* astate, pointer = to_internal_pointer Read location iterator astate in - let* astate, index = PulseOperations.eval_access mode location pointer Dereference astate in + let to_elem_pointed_by_iterator path mode ?(step = None) location iterator astate = + let* astate, pointer = to_internal_pointer path Read location iterator astate in + let* astate, index = + PulseOperations.eval_access path mode location pointer Dereference astate + in (* Check if not end iterator *) let is_minus_minus = match step with Some `MinusMinus -> true | _ -> false in let* astate = @@ -746,36 +770,44 @@ module GenericArrayBackedCollectionIterator = struct else Ok astate in (* We do not want to create internal array if iterator pointer has an invalid value *) - let* astate = PulseOperations.check_addr_access Read location index astate in - let+ astate, elem = GenericArrayBackedCollection.element location iterator (fst index) astate in + let* astate = PulseOperations.check_addr_access path Read location index astate in + let+ astate, elem = + GenericArrayBackedCollection.element path location iterator (fst index) astate + in (astate, pointer, elem) - let construct location event ~init ~ref astate = + let construct path location event ~init ~ref astate = let* astate, (arr_addr, arr_hist) = - GenericArrayBackedCollection.eval Read location init astate + GenericArrayBackedCollection.eval path Read location init astate in let* astate = - PulseOperations.write_deref_field location ~ref GenericArrayBackedCollection.field + PulseOperations.write_deref_field path location ~ref GenericArrayBackedCollection.field ~obj:(arr_addr, event :: arr_hist) astate in - let* astate, (p_addr, p_hist) = to_internal_pointer Read location init astate in - PulseOperations.write_field location ~ref internal_pointer ~obj:(p_addr, event :: p_hist) astate + let* astate, (p_addr, p_hist) = to_internal_pointer path Read location init astate in + PulseOperations.write_field path location ~ref internal_pointer + ~obj:(p_addr, event :: p_hist) + astate let constructor ~desc this init : model = - fun {location} astate -> + fun {path; location} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in - let<+> astate = construct location event ~init ~ref:this astate in + let<+> astate = construct path location event ~init ~ref:this astate in astate let operator_compare comparison ~desc iter_lhs iter_rhs : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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 path Read location iter_lhs astate + in + let<*> astate, _, (index_rhs, _) = + to_internal_pointer_deref path 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 = @@ -799,21 +831,23 @@ module GenericArrayBackedCollectionIterator = struct let operator_star ~desc iter : model = - fun {location; ret} astate -> + fun {path; 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, pointer, (elem, _) = + to_elem_pointed_by_iterator path Read location iter astate + in PulseOperations.write_id (fst ret) (elem, event :: snd pointer) astate let operator_step step ~desc iter : model = - fun {location} astate -> + fun {path; location} astate -> let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let index_new = AbstractValue.mk_fresh () in let<*> astate, pointer, _ = - to_elem_pointed_by_iterator Read ~step:(Some step) location iter astate + to_elem_pointed_by_iterator path Read ~step:(Some step) location iter astate in let<+> astate = - PulseOperations.write_deref location ~ref:pointer + PulseOperations.write_deref path location ~ref:pointer ~obj:(index_new, event :: snd pointer) astate in @@ -822,28 +856,28 @@ end module JavaIterator = struct let constructor ~desc init : model = - fun {location; ret} astate -> + fun {path; 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 + GenericArrayBackedCollectionIterator.construct path 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 : model = - fun {location; ret} astate -> + fun {path; 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) = - GenericArrayBackedCollectionIterator.to_internal_pointer Read location iter astate + GenericArrayBackedCollectionIterator.to_internal_pointer path Read location iter astate in let<*> astate, (curr_elem_val, curr_elem_hist) = - GenericArrayBackedCollection.element location iter curr_index astate + GenericArrayBackedCollection.element path location iter curr_index astate in let<+> astate = - PulseOperations.write_field location ~ref:iter + PulseOperations.write_field path location ~ref:iter GenericArrayBackedCollectionIterator.internal_pointer ~obj:(new_index, event :: curr_index_hist) astate @@ -853,22 +887,22 @@ module JavaIterator = struct (* {curr -> v_c } is modified to {curr -> v_fresh} and writes to array[v_c] *) let remove ~desc iter : model = - fun {location} astate -> + fun {path; 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) = - GenericArrayBackedCollectionIterator.to_internal_pointer Read location iter astate + GenericArrayBackedCollectionIterator.to_internal_pointer path Read location iter astate in let<*> astate = - PulseOperations.write_field location ~ref:iter + PulseOperations.write_field path 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, arr = GenericArrayBackedCollection.eval path Read location iter astate in let<+> astate = - PulseOperations.write_arr_index location ~ref:arr ~index:curr_index + PulseOperations.write_arr_index path location ~ref:arr ~index:curr_index ~obj:(new_elem, event :: curr_index_hist) astate in @@ -876,22 +910,24 @@ module JavaIterator = struct end module StdVector = struct - let reallocate_internal_array trace vector vector_f location astate = + let reallocate_internal_array path trace vector vector_f location astate = let* astate, array_address = - GenericArrayBackedCollection.eval NoAccess location vector astate + GenericArrayBackedCollection.eval path NoAccess location vector astate in - PulseOperations.invalidate_array_elements location (StdVector vector_f) array_address astate - >>= PulseOperations.invalidate_deref_access location (StdVector vector_f) vector + PulseOperations.invalidate_array_elements path location (StdVector vector_f) array_address + astate + >>= PulseOperations.invalidate_deref_access path location (StdVector vector_f) vector GenericArrayBackedCollection.access - >>= PulseOperations.havoc_deref_field location vector GenericArrayBackedCollection.field trace + >>= PulseOperations.havoc_deref_field path location vector GenericArrayBackedCollection.field + trace let init_list_constructor this init_list : model = - fun {location} astate -> + fun {path; 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, init_copy = PulseOperations.shallow_copy path location init_list astate in let<+> astate = - PulseOperations.write_deref_field location ~ref:this GenericArrayBackedCollection.field + PulseOperations.write_deref_field path location ~ref:this GenericArrayBackedCollection.field ~obj:(fst init_copy, event :: snd init_copy) astate in @@ -899,79 +935,83 @@ module StdVector = struct let invalidate_references vector_f vector : model = - fun {location} astate -> + fun {path; location} astate -> let crumb = ValueHistory.Call { f= Model (Format.asprintf "%a()" Invalidation.pp_std_vector_function vector_f) ; location ; in_call= [] } in - let<+> astate = reallocate_internal_array [crumb] vector vector_f location astate in + let<+> astate = reallocate_internal_array path [crumb] vector vector_f location astate in astate let at ~desc vector index : model = - fun {location; ret} astate -> + fun {path; 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 + GenericArrayBackedCollection.element path location vector (fst index) astate in PulseOperations.write_id (fst ret) (addr, event :: hist) astate let vector_begin vector iter : model = - fun {location} astate -> + fun {path; 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 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) = - GenericArrayBackedCollection.eval Read location vector astate + GenericArrayBackedCollection.eval path Read location vector astate + in + let<*> astate, _ = + GenericArrayBackedCollection.eval_element path location arr index_zero astate in - let<*> astate, _ = GenericArrayBackedCollection.eval_element location arr index_zero astate in let<+> astate = - PulseOperations.write_deref_field location ~ref:iter GenericArrayBackedCollection.field + PulseOperations.write_deref_field path location ~ref:iter GenericArrayBackedCollection.field ~obj:(arr_addr, pointer_hist) astate - >>= PulseOperations.write_field location ~ref:iter + >>= PulseOperations.write_field path location ~ref:iter GenericArrayBackedCollectionIterator.internal_pointer ~obj:pointer_val - >>= PulseOperations.write_deref location ~ref:pointer_val ~obj:(index_zero, pointer_hist) + >>= PulseOperations.write_deref path location ~ref:pointer_val ~obj:(index_zero, pointer_hist) in astate let vector_end vector iter : model = - fun {location} astate -> + fun {path; 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, (arr_addr, _) = + GenericArrayBackedCollection.eval path Read location vector astate + in let<*> astate, (pointer_addr, _) = - GenericArrayBackedCollection.eval_pointer_to_last_element location vector astate + GenericArrayBackedCollection.eval_pointer_to_last_element path location vector astate in let pointer_hist = event :: snd iter in let pointer_val = (pointer_addr, pointer_hist) in let<*> astate = - PulseOperations.write_deref_field location ~ref:iter GenericArrayBackedCollection.field + PulseOperations.write_deref_field path location ~ref:iter GenericArrayBackedCollection.field ~obj:(arr_addr, pointer_hist) astate in let<+> astate = - PulseOperations.write_field location ~ref:iter + PulseOperations.write_field path location ~ref:iter GenericArrayBackedCollectionIterator.internal_pointer ~obj:pointer_val astate in astate let reserve vector : model = - fun {location} astate -> + fun {path; 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 + reallocate_internal_array path [crumb] vector Reserve location astate >>| AddressAttributes.std_vector_reserve (fst vector) in astate let push_back vector : model = - fun {location} astate -> + fun {path; 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 @@ -979,15 +1019,15 @@ module StdVector = struct ok_continue astate else (* simulate a re-allocation of the underlying array every time an element is added *) - let<+> astate = reallocate_internal_array [crumb] vector PushBack location astate in + let<+> astate = reallocate_internal_array path [crumb] vector PushBack location astate in astate let empty vector : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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 + GenericArrayBackedCollection.eval_is_empty path location vector astate in PulseOperations.write_id ret_id (value_addr, crumb :: value_hist) astate end @@ -997,21 +1037,21 @@ module Java = struct Fieldname.make (Typ.JavaClass (JavaClassName.make ~package:(Some pkg) ~classname:clazz)) field - let load_field field location obj astate = + let load_field path field location obj astate = let* astate, field_addr = - PulseOperations.eval_access Read location obj (FieldAccess field) astate + PulseOperations.eval_access path Read location obj (FieldAccess field) astate in let+ astate, field_val = - PulseOperations.eval_access Read location field_addr Dereference astate + PulseOperations.eval_access path Read location field_addr Dereference astate in (astate, field_addr, field_val) - let write_field field new_val location addr astate = + let write_field path field new_val location addr astate = let* astate, field_addr = - PulseOperations.eval_access Write location addr (FieldAccess field) astate + PulseOperations.eval_access path Write location addr (FieldAccess field) astate in - PulseOperations.write_deref location ~ref:field_addr ~obj:new_val astate + PulseOperations.write_deref path location ~ref:field_addr ~obj:new_val astate let instance_of (argv, hist) typeexpr : model = @@ -1042,20 +1082,24 @@ module JavaCollection = struct let init ~desc this : model = - fun {location} astate -> + fun {path; 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 let init_value = AbstractValue.mk_fresh () in (* The two internal fields are initially set to null *) - let<*> astate = Java.write_field fst_field (init_value, [event]) location fresh_val astate in - let<*> astate = Java.write_field snd_field (init_value, [event]) location fresh_val astate in + let<*> astate = + Java.write_field path fst_field (init_value, [event]) location fresh_val astate + in + let<*> astate = + Java.write_field path snd_field (init_value, [event]) location fresh_val astate + in (* The empty field is initially set to true *) let<*> astate = - Java.write_field is_empty_field (is_empty_value, [event]) location fresh_val astate + Java.write_field path is_empty_field (is_empty_value, [event]) location fresh_val astate in let<*> astate = - PulseOperations.write_deref location ~ref:this ~obj:fresh_val astate + PulseOperations.write_deref path location ~ref:this ~obj:fresh_val astate >>= PulseArithmetic.and_eq_int init_value IntLit.zero >>= PulseArithmetic.and_eq_int is_empty_value IntLit.one in @@ -1063,16 +1107,18 @@ module JavaCollection = struct let add ~desc coll new_elem : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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 + let<*> astate, coll_val = + PulseOperations.eval_access path Read location coll Dereference astate + in (* reads snd_field from collection *) - let<*> astate, snd_addr, snd_val = Java.load_field snd_field location coll_val astate in + let<*> astate, snd_addr, snd_val = Java.load_field path snd_field location coll_val astate in (* fst_field takes value stored in snd_field *) - let<*> astate = Java.write_field fst_field snd_val location coll_val astate in + let<*> astate = Java.write_field path fst_field snd_val location coll_val astate in (* snd_field takes new value given *) - let<*> astate = PulseOperations.write_deref location ~ref:snd_addr ~obj:new_elem astate in + let<*> astate = PulseOperations.write_deref path location ~ref:snd_addr ~obj:new_elem astate in (* Collection.add returns a boolean, in this case the return always has value one *) let<*> astate = PulseArithmetic.and_eq_int ret_value IntLit.one astate @@ -1080,64 +1126,68 @@ module JavaCollection = struct in (* empty field set to false if the collection was empty *) let<*> astate, _, (is_empty_val, hist) = - Java.load_field is_empty_field location coll_val astate + Java.load_field path is_empty_field location coll_val astate in if PulseArithmetic.is_known_zero astate is_empty_val then astate |> ok_continue else let is_empty_new_val = AbstractValue.mk_fresh () in let<*> astate = - Java.write_field is_empty_field (is_empty_new_val, event :: hist) location coll_val astate + Java.write_field path is_empty_field + (is_empty_new_val, event :: hist) + location coll_val astate >>= PulseArithmetic.and_eq_int is_empty_new_val IntLit.zero in astate |> ok_continue - let update coll new_val new_val_hist event location ret_id astate = + let update path coll new_val new_val_hist event location ret_id astate = (* case0: element not present in collection *) - let* astate, coll_val = PulseOperations.eval_access Read location coll Dereference astate in - let* astate, _, fst_val = Java.load_field fst_field location coll_val astate in - let* astate, _, snd_val = Java.load_field snd_field location coll_val astate in + let* astate, coll_val = + PulseOperations.eval_access path Read location coll Dereference astate + in + let* astate, _, fst_val = Java.load_field path fst_field location coll_val astate in + let* astate, _, snd_val = Java.load_field path snd_field location coll_val astate in let is_empty_val = AbstractValue.mk_fresh () in let* astate' = - Java.write_field is_empty_field (is_empty_val, [event]) location coll_val astate + Java.write_field path is_empty_field (is_empty_val, [event]) location coll_val astate in (* case1: fst_field is updated *) let* astate1 = - Java.write_field fst_field (new_val, event :: new_val_hist) location coll astate' + Java.write_field path fst_field (new_val, event :: new_val_hist) location coll astate' in let astate1 = PulseOperations.write_id ret_id fst_val astate1 in (* case2: snd_field is updated *) let+ astate2 = - Java.write_field snd_field (new_val, event :: new_val_hist) location coll astate' + Java.write_field path snd_field (new_val, event :: new_val_hist) location coll astate' in let astate2 = PulseOperations.write_id ret_id snd_val astate2 in [astate; astate1; astate2] let set coll (new_val, new_val_hist) : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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 + let<*> astates = update path coll new_val new_val_hist event location ret_id astate in List.map ~f:(fun astate -> Ok (ContinueProgram astate)) astates - let remove_at ~desc coll location ret_id astate = + let remove_at path ~desc coll location ret_id astate = let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let new_val = AbstractValue.mk_fresh () in PulseArithmetic.and_eq_int new_val IntLit.zero astate - >>= update coll new_val [] event location ret_id + >>= update path coll new_val [] event location ret_id (* Auxiliary function that updates the state by: (1) assuming that value to be removed is equal to field value (2) assigning field to null value Collection.remove should return a boolean. In this case, the return val is one *) - let remove_elem_found coll_val elem field_addr field_val ret_id location event astate = + let remove_elem_found path coll_val elem field_addr field_val ret_id location event astate = let null_val = AbstractValue.mk_fresh () in let ret_val = AbstractValue.mk_fresh () in let is_empty_val = AbstractValue.mk_fresh () in let* astate = - Java.write_field is_empty_field (is_empty_val, [event]) location coll_val astate + Java.write_field path is_empty_field (is_empty_val, [event]) location coll_val astate in let* astate = PulseArithmetic.and_eq_int null_val IntLit.zero astate @@ -1148,21 +1198,27 @@ module JavaCollection = struct (AbstractValueOperand field_val) astate in let* astate = - PulseOperations.write_deref location ~ref:field_addr ~obj:(null_val, [event]) astate + PulseOperations.write_deref path location ~ref:field_addr ~obj:(null_val, [event]) astate in let astate = PulseOperations.write_id ret_id (ret_val, [event]) astate in Ok astate - let remove_obj ~desc coll (elem, _) location ret_id astate = + let remove_obj path ~desc coll (elem, _) location 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, coll_val = + PulseOperations.eval_access path Read location coll Dereference astate + in (* case1: given element is equal to fst_field *) - let* astate, fst_addr, (fst_val, _) = Java.load_field fst_field location coll_val astate in - let* astate1 = remove_elem_found coll_val elem fst_addr fst_val ret_id location event astate in + let* astate, fst_addr, (fst_val, _) = Java.load_field path fst_field location coll_val astate in + let* astate1 = + remove_elem_found path coll_val elem fst_addr fst_val ret_id location event astate + in (* case2: given element is equal to snd_field *) - let* astate, snd_addr, (snd_val, _) = Java.load_field snd_field location coll_val astate in - let* astate2 = remove_elem_found coll_val elem snd_addr snd_val ret_id location event astate in + let* astate, snd_addr, (snd_val, _) = Java.load_field path snd_field location coll_val astate in + let* astate2 = + remove_elem_found path coll_val elem snd_addr snd_val ret_id location event astate + in (* case 3: given element is not equal to the fst AND not equal to the snd *) let+ astate = PulseArithmetic.prune_binop ~negated:true Binop.Eq (AbstractValueOperand elem) @@ -1174,7 +1230,7 @@ module JavaCollection = struct let remove ~desc args : model = - fun {location; ret= ret_id, _} astate -> + fun {path; location; ret= ret_id, _} astate -> match args with | [ {ProcnameDispatcher.Call.FuncArg.arg_payload= coll_arg} ; {ProcnameDispatcher.Call.FuncArg.arg_payload= elem_arg; typ} ] -> @@ -1182,10 +1238,10 @@ module JavaCollection = struct match typ.desc with | Tint _ -> (* Case of remove(int index) *) - remove_at ~desc coll_arg location ret_id astate + remove_at path ~desc coll_arg location ret_id astate | _ -> (* Case of remove(Object o) *) - remove_obj ~desc coll_arg elem_arg location ret_id astate + remove_obj path ~desc coll_arg elem_arg location ret_id astate in List.map ~f:(fun astate -> Ok (ContinueProgram astate)) astates | _ -> @@ -1193,25 +1249,29 @@ module JavaCollection = struct let is_empty ~desc coll : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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, coll_val = + PulseOperations.eval_access path Read location coll Dereference astate + in let<*> astate, _, (is_empty_val, hist) = - Java.load_field is_empty_field location coll_val astate + Java.load_field path is_empty_field location coll_val astate in PulseOperations.write_id ret_id (is_empty_val, event :: hist) astate |> ok_continue let clear ~desc coll : model = - fun {location} astate -> + fun {path; 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 - let<*> astate, coll_val = PulseOperations.eval_access Read location coll Dereference astate in - let<*> astate = Java.write_field fst_field (null_val, [event]) location coll_val astate in - let<*> astate = Java.write_field snd_field (null_val, [event]) location coll_val astate in + let<*> astate, coll_val = + PulseOperations.eval_access path Read location coll Dereference astate + in + let<*> astate = Java.write_field path fst_field (null_val, [event]) location coll_val astate in + let<*> astate = Java.write_field path snd_field (null_val, [event]) location coll_val astate in let<*> astate = - Java.write_field is_empty_field (is_empty_val, [event]) location coll_val astate + Java.write_field path is_empty_field (is_empty_val, [event]) location coll_val astate in let<+> astate = PulseArithmetic.and_eq_int null_val IntLit.zero astate @@ -1223,7 +1283,7 @@ module JavaCollection = struct (* Auxiliary function that changes the state by (1) assuming that internal is_empty field has value one (2) in such case we can return 0 *) - let get_elem_coll_is_empty is_empty_val is_empty_expected_val event location ret_id astate = + let get_elem_coll_is_empty path is_empty_val is_empty_expected_val event location ret_id astate = let not_found_val = AbstractValue.mk_fresh () in let* astate = PulseArithmetic.prune_binop ~negated:false Binop.Eq (AbstractValueOperand is_empty_val) @@ -1233,7 +1293,7 @@ module JavaCollection = struct in let hist = [event] in let astate = PulseOperations.write_id ret_id (not_found_val, hist) astate in - PulseOperations.invalidate + PulseOperations.invalidate path (StackAddress (Var.of_id ret_id, hist)) location (ConstantDereference IntLit.zero) (not_found_val, [event]) @@ -1265,17 +1325,23 @@ module JavaCollection = struct let get ~desc coll (elem, _) : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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 + let<*> astate, coll_val = + PulseOperations.eval_access path Read location coll Dereference astate + in + let<*> astate, _, (is_empty_val, _) = + Java.load_field path is_empty_field location coll_val astate + in (* case 1: collection is empty *) let true_val = AbstractValue.mk_fresh () in - let<*> astate1 = get_elem_coll_is_empty is_empty_val true_val event location ret_id astate in + let<*> astate1 = + get_elem_coll_is_empty path is_empty_val true_val event location ret_id astate + in (* case 2: collection is not known to be empty *) let found_val = AbstractValue.mk_fresh () in - let<*> astate2, _, (fst_val, _) = Java.load_field fst_field location coll_val astate in - let<*> astate2, _, (snd_val, _) = Java.load_field snd_field location coll_val astate2 in + let<*> astate2, _, (fst_val, _) = Java.load_field path fst_field location coll_val astate in + let<*> astate2, _, (snd_val, _) = Java.load_field path snd_field location coll_val astate2 in let<*> astate2 = PulseArithmetic.prune_binop ~negated:true Binop.Eq (AbstractValueOperand is_empty_val) (AbstractValueOperand true_val) astate2 @@ -1289,31 +1355,31 @@ end module JavaInteger = struct let internal_int = Java.mk_java_field "java.lang" "Integer" "__infer_model_backing_int" - let load_backing_int location this astate = - let* astate, obj = PulseOperations.eval_access Read location this Dereference astate in - Java.load_field internal_int location obj astate + let load_backing_int path location this astate = + let* astate, obj = PulseOperations.eval_access path Read location this Dereference astate in + Java.load_field path internal_int location obj astate - let construct this_address init_value event location astate = + let construct path this_address init_value event location astate = let this = (AbstractValue.mk_fresh (), [event]) in let* astate, int_field = - PulseOperations.eval_access Write location this (FieldAccess internal_int) astate + PulseOperations.eval_access path Write location this (FieldAccess internal_int) astate in - let* astate = PulseOperations.write_deref location ~ref:int_field ~obj:init_value astate in - PulseOperations.write_deref location ~ref:this_address ~obj:this astate + let* astate = PulseOperations.write_deref path location ~ref:int_field ~obj:init_value astate in + PulseOperations.write_deref path location ~ref:this_address ~obj:this astate let init this_address init_value : model = - fun {location} astate -> + fun {path; 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 + let<+> astate = construct path this_address init_value event location astate in astate let equals this arg : model = - 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 + fun {path; location; ret= ret_id, _} astate -> + let<*> astate, _int_addr1, (int1, hist) = load_backing_int path location this astate in + let<*> astate, _int_addr2, (int2, _) = load_backing_int path location arg astate in let binop_addr = AbstractValue.mk_fresh () in let<+> astate = PulseArithmetic.eval_binop binop_addr Binop.Eq (AbstractValueOperand int1) @@ -1323,16 +1389,16 @@ module JavaInteger = struct let int_val this : model = - fun {location; ret= ret_id, _} astate -> - let<*> astate, _int_addr1, int_value_hist = load_backing_int location this astate in + fun {path; location; ret= ret_id, _} astate -> + let<*> astate, _int_addr1, int_value_hist = load_backing_int path location this astate in PulseOperations.write_id ret_id int_value_hist astate |> ok_continue let value_of init_value : model = - fun {location; ret= ret_id, _} astate -> + fun {path; 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 = construct path new_alloc init_value event location astate in PulseOperations.write_id ret_id new_alloc astate end diff --git a/infer/src/pulse/PulseModels.mli b/infer/src/pulse/PulseModels.mli index 6f60702d7..ab38fcf91 100644 --- a/infer/src/pulse/PulseModels.mli +++ b/infer/src/pulse/PulseModels.mli @@ -10,6 +10,7 @@ open PulseDomainInterface type model_data = { analysis_data: PulseSummary.t InterproceduralAnalysis.t + ; path: PathContext.t ; callee_procname: Procname.t ; location: Location.t ; ret: Ident.t * Typ.t } diff --git a/infer/src/pulse/PulseObjectiveCSummary.ml b/infer/src/pulse/PulseObjectiveCSummary.ml index 87e87f3ec..9c157d803 100644 --- a/infer/src/pulse/PulseObjectiveCSummary.ml +++ b/infer/src/pulse/PulseObjectiveCSummary.ml @@ -15,7 +15,7 @@ let mk_objc_self_pvar proc_desc = Pvar.mk Mangled.self proc_name -let init_fields_zero tenv location ~zero addr typ astate = +let init_fields_zero tenv path location ~zero addr typ astate = let get_fields typ = match typ.Typ.desc with | Tstruct struct_name -> @@ -31,7 +31,7 @@ let init_fields_zero tenv location ~zero addr typ astate = let acc, field_addr = Memory.eval_edge addr (FieldAccess field) acc in init_fields_zero_helper field_addr field_typ acc ) | None -> - PulseOperations.write_deref location ~ref:addr ~obj:zero astate + PulseOperations.write_deref path location ~ref:addr ~obj:zero astate in init_fields_zero_helper addr typ astate @@ -39,10 +39,11 @@ let init_fields_zero tenv location ~zero addr typ astate = let mk_objc_method_nil_summary_aux tenv proc_desc astate = (* Constructs summary {self = 0} {return = self}. This allows us to connect invalidation with invalid access in the trace *) + let path = PathContext.initial in let location = Procdesc.get_loc proc_desc in let self = mk_objc_self_pvar proc_desc in let* astate, (self_value, self_history) = - PulseOperations.eval_deref location (Lvar self) astate + PulseOperations.eval_deref path location (Lvar self) astate in let* astate = PulseArithmetic.prune_eq_zero self_value astate in let event = ValueHistory.NilMessaging location in @@ -51,14 +52,16 @@ let mk_objc_method_nil_summary_aux tenv proc_desc astate = | Some (last_formal, {desc= Tptr (typ, _)}) when Mangled.is_return_param last_formal -> let ret_param_var = Procdesc.get_ret_param_var proc_desc in let* astate, ret_param_var_addr_hist = - PulseOperations.eval_deref location (Lvar ret_param_var) astate + PulseOperations.eval_deref path location (Lvar ret_param_var) astate in - init_fields_zero tenv location ~zero:updated_self_value_hist ret_param_var_addr_hist typ + init_fields_zero tenv path location ~zero:updated_self_value_hist ret_param_var_addr_hist typ astate | _ -> let ret_var = Procdesc.get_ret_var proc_desc in - let* astate, ret_var_addr_hist = PulseOperations.eval Write location (Lvar ret_var) astate in - PulseOperations.write_deref location ~ref:ret_var_addr_hist ~obj:updated_self_value_hist + let* astate, ret_var_addr_hist = + PulseOperations.eval path Write location (Lvar ret_var) astate + in + PulseOperations.write_deref path location ~ref:ret_var_addr_hist ~obj:updated_self_value_hist astate @@ -88,7 +91,9 @@ let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log} match astate with | ContinueProgram astate -> let result = - let* astate, value = PulseOperations.eval_deref location (Lvar self) astate in + let* astate, value = + PulseOperations.eval_deref PathContext.initial location (Lvar self) astate + in PulseArithmetic.prune_positive (fst value) astate in PulseReport.report_result tenv proc_desc err_log location result @@ -111,6 +116,7 @@ let append_objc_actual_self_positive procdesc self_actual astate = let update_must_be_valid_reason {InterproceduralAnalysis.tenv; proc_desc; err_log} astate = + let path = PathContext.initial in let location = Procdesc.get_loc proc_desc in let self = mk_objc_self_pvar proc_desc in let proc_name = Procdesc.get_proc_name proc_desc in @@ -119,12 +125,9 @@ let update_must_be_valid_reason {InterproceduralAnalysis.tenv; proc_desc; err_lo when not (Procdesc.is_ret_type_pod proc_desc) -> let result = (* add reason for must be valid to be because the return type is non pod *) - let+ astate, value = PulseOperations.eval_deref location (Lvar self) astate in - let astate = - AddressAttributes.replace_must_be_valid_reason Invalidation.SelfOfNonPODReturnMethod - (fst value) astate - in - astate + let+ astate, value = PulseOperations.eval_deref path location (Lvar self) astate in + AddressAttributes.replace_must_be_valid_reason path SelfOfNonPODReturnMethod (fst value) + astate in PulseReport.report_result tenv proc_desc err_log location result | ContinueProgram _, _ diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 432d04c1a..005c4f684 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -50,10 +50,10 @@ end include Import -let check_addr_access ?must_be_valid_reason access_mode location (address, history) astate = +let check_addr_access path ?must_be_valid_reason access_mode location (address, history) astate = let access_trace = Trace.Immediate {location; history} in let* astate = - AddressAttributes.check_valid ?must_be_valid_reason access_trace address astate + AddressAttributes.check_valid path ?must_be_valid_reason access_trace address astate |> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> ReportableError { diagnostic= @@ -79,10 +79,10 @@ let check_addr_access ?must_be_valid_reason access_mode location (address, histo Ok astate -let check_and_abduce_addr_access_isl access_mode location (address, history) ?(null_noop = false) - astate = +let check_and_abduce_addr_access_isl path access_mode location (address, history) + ?(null_noop = false) astate = let access_trace = Trace.Immediate {location; history} in - AddressAttributes.check_valid_isl access_trace address ~null_noop astate + AddressAttributes.check_valid_isl path access_trace address ~null_noop astate |> List.map ~f:(fun access_result -> let* astate = AccessResult.of_abductive_access_result access_trace access_result in match access_mode with @@ -137,7 +137,7 @@ module Closures = struct Memory.Edges.add (HilExp.Access.FieldAccess (mk_fake_field ~id mode)) (addr, trace) edges ) - let check_captured_addresses action lambda_addr (astate : t) = + let check_captured_addresses path action lambda_addr (astate : t) = match AbductiveDomain.find_post_cell_opt lambda_addr astate with | None -> Ok astate @@ -147,7 +147,7 @@ module Closures = struct | Attribute.Closure _ -> IContainer.iter_result ~fold:Memory.Edges.fold edges ~f:(fun (access, addr_trace) -> if is_captured_by_ref_fake_access access then - let+ _ = check_addr_access Read action addr_trace astate in + let+ _ = check_addr_access path Read action addr_trace astate in () else Ok () ) | _ -> @@ -172,50 +172,52 @@ module Closures = struct (astate, closure_addr_hist) end -let eval_var location hist var astate = Stack.eval location hist var astate - -let eval_access ?must_be_valid_reason mode location addr_hist access astate = - let+ astate = check_addr_access ?must_be_valid_reason mode location addr_hist astate in +let eval_access path ?must_be_valid_reason mode location addr_hist access astate = + let+ astate = check_addr_access path ?must_be_valid_reason mode location addr_hist astate in Memory.eval_edge addr_hist access astate -let eval_deref_access ?must_be_valid_reason mode location addr_hist access astate = - let* astate, addr_hist = eval_access Read location addr_hist access astate in - eval_access ?must_be_valid_reason mode location addr_hist Dereference astate +let eval_deref_access path ?must_be_valid_reason mode location addr_hist access astate = + let* astate, addr_hist = eval_access path Read location addr_hist access astate in + eval_access path ?must_be_valid_reason mode location addr_hist Dereference astate -let eval_access_biad_isl mode location addr_hist access astate = +let eval_access_biad_isl path mode location addr_hist access astate = let map_ok addr_hist access results = List.map results ~f:(fun result -> let+ astate = result in Memory.eval_edge addr_hist access astate ) in - let results = check_and_abduce_addr_access_isl mode location addr_hist astate in + let results = check_and_abduce_addr_access_isl path mode location addr_hist astate in map_ok addr_hist access results -let eval mode location exp0 astate = - let rec eval mode exp astate = +let eval path mode location exp0 astate = + let rec eval path mode exp astate = match (exp : Exp.t) with | Var id -> - Ok (eval_var location (* error in case of missing history? *) [] (Var.of_id id) astate) + Ok + (Stack.eval path location (* error in case of missing history? *) [] (Var.of_id id) + astate) | Lvar pvar -> Ok - (eval_var location + (Stack.eval path location [ValueHistory.VariableAccessed (pvar, location)] (Var.of_pvar pvar) astate) | Lfield (exp', field, _) -> - let* astate, addr_hist = eval Read exp' astate in - eval_access mode location addr_hist (FieldAccess field) astate + let* astate, addr_hist = eval path Read exp' astate in + eval_access path mode location addr_hist (FieldAccess field) astate | Lindex (exp', exp_index) -> - let* astate, addr_hist_index = eval Read exp_index astate in - let* astate, addr_hist = eval Read exp' astate in - eval_access mode location addr_hist (ArrayAccess (StdTyp.void, fst addr_hist_index)) astate + let* astate, addr_hist_index = eval path Read exp_index astate in + let* astate, addr_hist = eval path Read exp' astate in + eval_access path mode location addr_hist + (ArrayAccess (StdTyp.void, fst addr_hist_index)) + astate | Closure {name; captured_vars} -> let+ astate, rev_captured = List.fold_result captured_vars ~init:(astate, []) ~f:(fun (astate, rev_captured) (capt_exp, captured_as, _, mode) -> - let+ astate, addr_trace = eval Read capt_exp astate in + let+ astate, addr_trace = eval path Read capt_exp astate in (astate, (captured_as, addr_trace, mode) :: rev_captured) ) in Closures.record location name (List.rev rev_captured) astate @@ -223,7 +225,7 @@ let eval mode location exp0 astate = (* function pointers are represented as closures with no captured variables *) Ok (Closures.record location proc_name [] astate) | Cast (_, exp') -> - eval mode exp' astate + eval path mode exp' astate | Const (Cint i) -> let v = AbstractValue.Constants.get_int i in let invalidation = Invalidation.ConstantDereference i in @@ -235,14 +237,14 @@ let eval mode location exp0 astate = in (astate, (v, [ValueHistory.Invalidated (invalidation, location)])) | UnOp (unop, exp, _typ) -> - let* astate, (addr, hist) = eval Read exp astate in + let* astate, (addr, hist) = eval path Read exp astate in let unop_addr = AbstractValue.mk_fresh () in let+ astate = PulseArithmetic.eval_unop unop_addr unop addr astate in (astate, (unop_addr, hist)) | BinOp (bop, e_lhs, e_rhs) -> - let* astate, (addr_lhs, hist_lhs) = eval Read e_lhs astate in + let* astate, (addr_lhs, hist_lhs) = eval path Read e_lhs astate in (* NOTE: keeping track of only [hist_lhs] into the binop is not the best *) - let* astate, (addr_rhs, _hist_rhs) = eval Read e_rhs astate in + let* astate, (addr_rhs, _hist_rhs) = eval path Read e_rhs astate in let binop_addr = AbstractValue.mk_fresh () in let+ astate = PulseArithmetic.eval_binop binop_addr bop (AbstractValueOperand addr_lhs) @@ -252,24 +254,24 @@ let eval mode location exp0 astate = | Const _ | Sizeof _ | Exn _ -> Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) [])) in - eval mode exp0 astate + eval path mode exp0 astate -let eval_to_operand mode location exp astate = +let eval_to_operand path mode location exp astate = match (exp : Exp.t) with | Const (Cint i) -> Ok (astate, PulseArithmetic.LiteralOperand i) | exp -> - let+ astate, (value, _) = eval mode location exp astate in + let+ astate, (value, _) = eval path mode location exp astate in (astate, PulseArithmetic.AbstractValueOperand value) -let prune location ~condition astate = +let prune path location ~condition astate = let rec prune_aux ~negated exp astate = match (exp : Exp.t) with | BinOp (bop, exp_lhs, exp_rhs) -> - let* astate, lhs_op = eval_to_operand Read location exp_lhs astate in - let* astate, rhs_op = eval_to_operand Read location exp_rhs astate in + let* astate, lhs_op = eval_to_operand path Read location exp_lhs astate in + let* astate, rhs_op = eval_to_operand path Read location exp_rhs astate in PulseArithmetic.prune_binop ~negated bop lhs_op rhs_op astate | UnOp (LNot, exp', _) -> prune_aux ~negated:(not negated) exp' astate @@ -279,53 +281,53 @@ let prune location ~condition astate = prune_aux ~negated:false condition astate -let eval_deref ?must_be_valid_reason location exp astate = - let* astate, addr_hist = eval Read location exp astate in - let+ astate = check_addr_access ?must_be_valid_reason Read location addr_hist astate in +let eval_deref path ?must_be_valid_reason location exp astate = + let* astate, addr_hist = eval path Read location exp astate in + let+ astate = check_addr_access path ?must_be_valid_reason Read location addr_hist astate in Memory.eval_edge addr_hist Dereference astate -let eval_proc_name location call_exp astate = +let eval_proc_name path location call_exp astate = match (call_exp : Exp.t) with | Const (Cfun proc_name) | Closure {name= proc_name} -> Ok (astate, Some proc_name) | _ -> - let+ astate, (f, _) = eval Read location call_exp astate in + let+ astate, (f, _) = eval path Read location call_exp astate in (astate, AddressAttributes.get_closure_proc_name f astate) -let eval_structure_isl mode loc exp astate = +let eval_structure_isl path mode loc exp astate = match (exp : Exp.t) with | Lfield (exp', field, _) -> - let+ astate, addr_hist = eval mode loc exp' astate in - let astates = eval_access_biad_isl mode loc addr_hist (FieldAccess field) astate in + let+ astate, addr_hist = eval path mode loc exp' astate in + let astates = eval_access_biad_isl path mode loc addr_hist (FieldAccess field) astate in (false, astates) | Lindex (exp', exp_index) -> - let* astate, addr_hist_index = eval mode loc exp_index astate in - let+ astate, addr_hist = eval mode loc exp' astate in + let* astate, addr_hist_index = eval path mode loc exp_index astate in + let+ astate, addr_hist = eval path mode loc exp' astate in let astates = - eval_access_biad_isl mode loc addr_hist + eval_access_biad_isl path mode loc addr_hist (ArrayAccess (StdTyp.void, fst addr_hist_index)) astate in (false, astates) | _ -> - let+ astate, (addr, history) = eval mode loc exp astate in + let+ astate, (addr, history) = eval path mode loc exp astate in (true, [Ok (astate, (addr, history))]) -let eval_deref_biad_isl location access addr_hist astate = - check_and_abduce_addr_access_isl Read location addr_hist astate +let eval_deref_biad_isl path location access addr_hist astate = + check_and_abduce_addr_access_isl path Read location addr_hist astate |> List.map ~f:(fun result -> let+ astate = result in Memory.eval_edge addr_hist access astate ) -let eval_deref_isl location exp astate = - let<*> is_structured, ls_astate_addr_hist = eval_structure_isl Read location exp astate in +let eval_deref_isl path location exp astate = + let<*> is_structured, ls_astate_addr_hist = eval_structure_isl path Read location exp astate in let eval_deref_function (astate, addr_hist) = - if is_structured then eval_deref_biad_isl location Dereference addr_hist astate - else [eval_deref location exp astate] + if is_structured then eval_deref_biad_isl path location Dereference addr_hist astate + else [eval_deref path location exp astate] in List.concat_map ls_astate_addr_hist ~f:(fun result -> let<*> astate_addr = result in @@ -349,42 +351,44 @@ let havoc_id id loc_opt astate = else astate -let write_access location addr_trace_ref access addr_trace_obj astate = - check_addr_access Write location addr_trace_ref astate +let write_access path location addr_trace_ref access addr_trace_obj astate = + check_addr_access path Write location addr_trace_ref astate >>| Memory.add_edge addr_trace_ref access addr_trace_obj location -let write_access_biad_isl location addr_trace_ref access addr_trace_obj astate = - let astates = check_and_abduce_addr_access_isl Write location addr_trace_ref astate in +let write_access_biad_isl path location addr_trace_ref access addr_trace_obj astate = + let astates = check_and_abduce_addr_access_isl path Write location addr_trace_ref astate in List.map astates ~f:(fun result -> let+ astate = result in Memory.add_edge addr_trace_ref access addr_trace_obj location astate ) -let write_deref location ~ref:addr_trace_ref ~obj:addr_trace_obj astate = - write_access location addr_trace_ref Dereference addr_trace_obj astate +let write_deref path location ~ref:addr_trace_ref ~obj:addr_trace_obj astate = + write_access path location addr_trace_ref Dereference addr_trace_obj astate -let write_deref_biad_isl location ~ref:(addr_ref, addr_ref_history) access ~obj:addr_trace_obj +let write_deref_biad_isl path location ~ref:(addr_ref, addr_ref_history) access ~obj:addr_trace_obj astate = - write_access_biad_isl location (addr_ref, addr_ref_history) access addr_trace_obj astate + write_access_biad_isl path location (addr_ref, addr_ref_history) access addr_trace_obj astate -let write_field location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate = - write_access location addr_trace_ref (FieldAccess field) addr_trace_obj astate +let write_field path location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate = + write_access path location addr_trace_ref (FieldAccess field) addr_trace_obj astate -let write_deref_field location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate = - let* astate, addr_hist = eval_access Read location addr_trace_ref (FieldAccess field) astate in - write_deref location ~ref:addr_hist ~obj:addr_trace_obj astate +let write_deref_field path location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate = + let* astate, addr_hist = + eval_access path Read location addr_trace_ref (FieldAccess field) astate + in + write_deref path location ~ref:addr_hist ~obj:addr_trace_obj astate -let write_arr_index location ~ref:addr_trace_ref ~index ~obj:addr_trace_obj astate = - write_access location addr_trace_ref (ArrayAccess (StdTyp.void, index)) addr_trace_obj astate +let write_arr_index path location ~ref:addr_trace_ref ~index ~obj:addr_trace_obj astate = + write_access path location addr_trace_ref (ArrayAccess (StdTyp.void, index)) addr_trace_obj astate -let havoc_deref_field location addr_trace field trace_obj astate = - write_deref_field location ~ref:addr_trace field +let havoc_deref_field path location addr_trace field trace_obj astate = + write_deref_field path location ~ref:addr_trace field ~obj:(AbstractValue.mk_fresh (), trace_obj) astate @@ -405,10 +409,10 @@ type invalidation_access = | StackAddress of Var.t * ValueHistory.t | UntraceableAccess -let record_invalidation access_path location cause astate = +let record_invalidation path access_path location cause astate = match access_path with | StackAddress (x, hist0) -> - let astate, (addr, hist) = Stack.eval location hist0 x astate in + let astate, (addr, hist) = Stack.eval path location hist0 x astate in Stack.add x (addr, Invalidated (cause, location) :: hist) astate | MemoryAccess {pointer; access; hist_obj_default} -> let addr_obj, hist_obj = @@ -425,40 +429,40 @@ let record_invalidation access_path location cause astate = astate -let invalidate access_path location cause addr_trace astate = - check_addr_access NoAccess location addr_trace astate +let invalidate path access_path location cause addr_trace astate = + check_addr_access path NoAccess location addr_trace astate >>| AddressAttributes.invalidate addr_trace cause location - >>| record_invalidation access_path location cause + >>| record_invalidation path access_path location cause -let invalidate_biad_isl location cause (address, history) astate = - check_and_abduce_addr_access_isl NoAccess location (address, history) ~null_noop:true astate +let invalidate_biad_isl path location cause (address, history) astate = + check_and_abduce_addr_access_isl path NoAccess location (address, history) ~null_noop:true astate |> List.map ~f:(fun result -> let+ astate = result in AddressAttributes.invalidate (address, history) cause location astate ) -let invalidate_access location cause ref_addr_hist access astate = +let invalidate_access path location cause ref_addr_hist access astate = let astate, (addr_obj, hist_obj) = Memory.eval_edge ref_addr_hist access astate in - invalidate + invalidate path (MemoryAccess {pointer= ref_addr_hist; access; hist_obj_default= hist_obj}) location cause (addr_obj, snd ref_addr_hist) astate -let invalidate_deref_access location cause ref_addr_hist access astate = +let invalidate_deref_access path location cause ref_addr_hist access astate = let astate, addr_hist = Memory.eval_edge ref_addr_hist access astate in let astate, (addr_obj, hist_obj) = Memory.eval_edge addr_hist Dereference astate in - invalidate + invalidate path (MemoryAccess {pointer= ref_addr_hist; access; hist_obj_default= hist_obj}) location cause (addr_obj, snd ref_addr_hist) astate -let invalidate_array_elements location cause addr_trace astate = - let+ astate = check_addr_access NoAccess location addr_trace astate in +let invalidate_array_elements path location cause addr_trace astate = + let+ astate = check_addr_access path NoAccess location addr_trace astate in match Memory.find_opt (fst addr_trace) astate with | None -> astate @@ -467,15 +471,15 @@ let invalidate_array_elements location cause addr_trace astate = match (access : Memory.Access.t) with | ArrayAccess _ as access -> AddressAttributes.invalidate dest_addr_trace cause location astate - |> record_invalidation + |> record_invalidation path (MemoryAccess {pointer= addr_trace; access; hist_obj_default= snd dest_addr_trace}) location cause | _ -> astate ) -let shallow_copy location addr_hist astate = - let+ astate = check_addr_access Read location addr_hist astate in +let shallow_copy path location addr_hist astate = + let+ astate = check_addr_access path Read location addr_hist astate in let cell = match AbductiveDomain.find_post_cell_opt (fst addr_hist) astate with | None -> @@ -668,13 +672,13 @@ let remove_vars vars location astate = Stack.remove_vars vars astate -let get_captured_actuals location ~captured_vars ~actual_closure astate = - let* astate, this_value_addr = eval_access Read location actual_closure Dereference astate in +let get_captured_actuals path location ~captured_vars ~actual_closure astate = + let* astate, this_value_addr = eval_access path Read location actual_closure Dereference astate in let+ _, astate, captured_vars_with_actuals = List.fold_result captured_vars ~init:(0, astate, []) ~f:(fun (id, astate, captured) (var, mode, typ) -> let+ astate, captured_actual = - eval_access Read location this_value_addr + eval_access path Read location this_value_addr (FieldAccess (Closures.mk_fake_field ~id mode)) astate in diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 790f05652..7bb2c2abf 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -68,7 +68,8 @@ include module type of Import type t = AbductiveDomain.t val check_addr_access : - ?must_be_valid_reason:Invalidation.must_be_valid_reason + PathContext.t + -> ?must_be_valid_reason:Invalidation.must_be_valid_reason -> access_mode -> Location.t -> AbstractValue.t * ValueHistory.t @@ -77,12 +78,18 @@ val check_addr_access : (** Check that the [address] is not known to be invalid *) module Closures : sig - val check_captured_addresses : Location.t -> AbstractValue.t -> t -> t AccessResult.t + val check_captured_addresses : + PathContext.t -> Location.t -> AbstractValue.t -> t -> t AccessResult.t (** assert the validity of the addresses captured by the lambda *) end val eval : - access_mode -> Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t + PathContext.t + -> access_mode + -> Location.t + -> Exp.t + -> t + -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t (** Use the stack and heap to evaluate the given expression down to an abstract address representing its value. @@ -90,7 +97,8 @@ val eval : known to be invalid. *) val eval_structure_isl : - access_mode + PathContext.t + -> access_mode -> Location.t -> Exp.t -> t @@ -98,10 +106,11 @@ val eval_structure_isl : (** Similar to eval but apply to data structures and ISL abduction. Return a list of abduced states (ISLOk and ISLErs); The boolean indicates whether it is data structures or not. *) -val prune : Location.t -> condition:Exp.t -> t -> t AccessResult.t +val prune : PathContext.t -> Location.t -> condition:Exp.t -> t -> t AccessResult.t val eval_deref : - ?must_be_valid_reason:Invalidation.must_be_valid_reason + PathContext.t + -> ?must_be_valid_reason:Invalidation.must_be_valid_reason -> Location.t -> Exp.t -> t @@ -109,10 +118,15 @@ val eval_deref : (** Like [eval] but evaluates [*exp]. *) val eval_deref_isl : - Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t list + PathContext.t + -> Location.t + -> Exp.t + -> t + -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t list val eval_access : - ?must_be_valid_reason:Invalidation.must_be_valid_reason + PathContext.t + -> ?must_be_valid_reason:Invalidation.must_be_valid_reason -> access_mode -> Location.t -> AbstractValue.t * ValueHistory.t @@ -123,7 +137,8 @@ val eval_access : so dereferences it according to the access. *) val eval_deref_access : - ?must_be_valid_reason:Invalidation.must_be_valid_reason + PathContext.t + -> ?must_be_valid_reason:Invalidation.must_be_valid_reason -> access_mode -> Location.t -> AbstractValue.t * ValueHistory.t @@ -132,12 +147,14 @@ val eval_deref_access : -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t (** Like [eval_access] but does additional dereference. *) -val eval_proc_name : Location.t -> Exp.t -> t -> (t * Procname.t option) AccessResult.t +val eval_proc_name : + PathContext.t -> Location.t -> Exp.t -> t -> (t * Procname.t option) AccessResult.t val havoc_id : Ident.t -> ValueHistory.t -> t -> t val havoc_deref_field : - Location.t + PathContext.t + -> Location.t -> AbstractValue.t * ValueHistory.t -> Fieldname.t -> ValueHistory.t @@ -150,7 +167,8 @@ val realloc_pvar : Tenv.t -> Pvar.t -> Typ.t -> Location.t -> t -> t val write_id : Ident.t -> AbstractValue.t * ValueHistory.t -> t -> t val write_field : - Location.t + PathContext.t + -> Location.t -> ref:AbstractValue.t * ValueHistory.t -> Fieldname.t -> obj:AbstractValue.t * ValueHistory.t @@ -159,7 +177,8 @@ val write_field : (** write the edge [ref --.field--> obj] *) val write_deref_field : - Location.t + PathContext.t + -> Location.t -> ref:AbstractValue.t * ValueHistory.t -> Fieldname.t -> obj:AbstractValue.t * ValueHistory.t @@ -168,7 +187,8 @@ val write_deref_field : (** write the edge [ref --.field--> _ --*--> obj] *) val write_arr_index : - Location.t + PathContext.t + -> Location.t -> ref:AbstractValue.t * ValueHistory.t -> index:AbstractValue.t -> obj:AbstractValue.t * ValueHistory.t @@ -177,7 +197,8 @@ val write_arr_index : (** write the edge [ref\[index\]--> obj] *) val write_deref : - Location.t + PathContext.t + -> Location.t -> ref:AbstractValue.t * ValueHistory.t -> obj:AbstractValue.t * ValueHistory.t -> t @@ -185,7 +206,8 @@ val write_deref : (** write the edge [ref --*--> obj] *) val write_deref_biad_isl : - Location.t + PathContext.t + -> Location.t -> ref:AbstractValue.t * ValueHistory.t -> AbstractValue.t HilExp.Access.t -> obj:AbstractValue.t * ValueHistory.t @@ -204,7 +226,8 @@ type invalidation_access = | UntraceableAccess (** we don't know where the value came from; avoid using if possible *) val invalidate : - invalidation_access + PathContext.t + -> invalidation_access -> Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t @@ -213,7 +236,12 @@ val invalidate : (** record that the address is invalid *) val invalidate_biad_isl : - Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t AccessResult.t list + PathContext.t + -> Location.t + -> Invalidation.t + -> AbstractValue.t * ValueHistory.t + -> t + -> t AccessResult.t list (** record that the address is invalid. If the address has not been allocated, abduce ISL specs for both invalid (null, free, unint) and allocated heap. *) @@ -224,7 +252,8 @@ val add_dynamic_type : Typ.t -> AbstractValue.t -> t -> t val remove_allocation_attr : AbstractValue.t -> t -> t val invalidate_access : - Location.t + PathContext.t + -> Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> BaseMemory.Access.t @@ -233,7 +262,8 @@ val invalidate_access : (** record that what the address points via the access to is invalid *) val invalidate_deref_access : - Location.t + PathContext.t + -> Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> BaseMemory.Access.t @@ -242,11 +272,17 @@ val invalidate_deref_access : (** Like [invalidate_access] but invalidates dereferenced address. *) val invalidate_array_elements : - Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t AccessResult.t + PathContext.t + -> Location.t + -> Invalidation.t + -> AbstractValue.t * ValueHistory.t + -> t + -> t AccessResult.t (** record that all the array elements that address points to is invalid *) val shallow_copy : - Location.t + PathContext.t + -> Location.t -> AbstractValue.t * ValueHistory.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t @@ -262,7 +298,8 @@ val check_address_escape : Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t AccessResult.t val get_captured_actuals : - Location.t + PathContext.t + -> Location.t -> captured_vars:(Var.t * CapturedVar.capture_mode * Typ.t) list -> actual_closure:AbstractValue.t * ValueHistory.t -> t diff --git a/infer/src/pulse/PulsePathContext.ml b/infer/src/pulse/PulsePathContext.ml new file mode 100644 index 000000000..e201731a8 --- /dev/null +++ b/infer/src/pulse/PulsePathContext.ml @@ -0,0 +1,24 @@ +(* + * 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 +module F = Format + +type timestamp = int [@@deriving compare] + +let t0 = 0 + +type t = {timestamp: timestamp} + +(** path contexts is metadata that do not contribute to the semantics *) +let leq ~lhs:_ ~rhs:_ = true + +let pp fmt ({timestamp}[@warning "+9"]) = F.fprintf fmt "timestamp= %d" timestamp + +let initial = {timestamp= 0} + +let post_exec_instr {timestamp} = {timestamp= timestamp + 1} diff --git a/infer/src/pulse/PulsePathContext.mli b/infer/src/pulse/PulsePathContext.mli new file mode 100644 index 000000000..9f8f850cf --- /dev/null +++ b/infer/src/pulse/PulsePathContext.mli @@ -0,0 +1,24 @@ +(* + * 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 +module F = Format + +type timestamp = private int [@@deriving compare] + +val t0 : timestamp + +type t = {timestamp: timestamp (** step number *)} + +val leq : lhs:t -> rhs:t -> bool + +val initial : t + +val post_exec_instr : t -> t +(** call this after each step of the symbolic execution to update the path information *) + +val pp : F.formatter -> t -> unit diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index 27b66ae1a..fd7175038 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -38,7 +38,7 @@ codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_un codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here] codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] -codetoanalyze/c/pulse/nullptr.c, report_correct_error_among_multiple_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,when calling `several_dereferences_ok` here,parameter `x` of several_dereferences_ok,invalid access occurs here] +codetoanalyze/c/pulse/nullptr.c, report_correct_error_among_multiple_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,when calling `several_dereferences_ok` here,parameter `z` of several_dereferences_ok,invalid access occurs here] codetoanalyze/c/pulse/traces.c, access_null_deref_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/c/pulse/traces.c, access_use_after_free_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `l` of access_use_after_free_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `l` of access_use_after_free_bad,invalid access occurs here] codetoanalyze/c/pulse/traces.c, call_makes_null_deref_manifest_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `something_about_strings_latent`,null pointer dereference part of the trace starts here,in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/c/pulse/nullptr.c b/infer/tests/codetoanalyze/c/pulse/nullptr.c index 3b9d31855..ed7cf0920 100644 --- a/infer/tests/codetoanalyze/c/pulse/nullptr.c +++ b/infer/tests/codetoanalyze/c/pulse/nullptr.c @@ -122,9 +122,12 @@ void null_alias_bad(int* x) { *x = 42; } +void dereference(int* p) { *p; } + void several_dereferences_ok(int* x, int* y, int* z) { int* p = x; *z = 52; + dereference(y); *y = 42; *x = 32; *x = 777; diff --git a/infer/tests/codetoanalyze/objc/pulse/issues.exp b/infer/tests/codetoanalyze/objc/pulse/issues.exp index 4f44be83e..d17c1f30f 100644 --- a/infer/tests/codetoanalyze/objc/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objc/pulse/issues.exp @@ -13,6 +13,6 @@ codetoanalyze/objc/pulse/NPENilBlocks.m, BlockA.assignNilBad, 5, NIL_BLOCK_CALL, codetoanalyze/objc/pulse/NPENilBlocks.m, BlockA.paramAssignNilBad:, 3, NIL_BLOCK_CALL, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/objc/pulse/NPENilBlocks.m, BlockA.paramReassignNilBad:, 6, NIL_BLOCK_CALL, no_bucket, ERROR, [is the null pointer,assigned,assigned,invalid access occurs here] codetoanalyze/objc/pulse/NPENilBlocks.m, calldoSomethingThenCallbackWithNilBad, 2, NIL_BLOCK_CALL, no_bucket, ERROR, [is the null pointer,when calling `BlockA.doSomethingThenCallback:` here,parameter `my_block` of BlockA.doSomethingThenCallback:,invalid access occurs here] -codetoanalyze/objc/pulse/uninit.m, Uninit.call_setter_c_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `x` created,when calling `Uninit.setS:` here,parameter `s` of Uninit.setS:,read to uninitialized value occurs here] +codetoanalyze/objc/pulse/uninit.m, Uninit.call_setter_c_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `y` created,when calling `Uninit.setS:` here,parameter `s` of Uninit.setS:,read to uninitialized value occurs here] codetoanalyze/objc/pulse/use_after_free.m, PulseTest.use_after_free_simple_in_objc_method_bad:, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of PulseTest.use_after_free_simple_in_objc_method_bad:,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of PulseTest.use_after_free_simple_in_objc_method_bad:,invalid access occurs here] codetoanalyze/objc/pulse/use_after_free.m, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]