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]