diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml index bdd0f504c..3e9e822aa 100644 --- a/infer/src/IR/HilExp.ml +++ b/infer/src/IR/HilExp.ml @@ -220,50 +220,6 @@ module AccessExpression = struct let pp = pp_access_expr - let to_accesses_fold access_expr ~init ~f_array_offset = - let rec aux accum accesses = function - | Base base -> - (accum, base, accesses) - | FieldOffset (access_expr, fld) -> - aux accum (Access.FieldAccess fld :: accesses) access_expr - | ArrayOffset (access_expr, typ, index) -> - let accum, index' = f_array_offset accum index in - aux accum (Access.ArrayAccess (typ, index') :: accesses) access_expr - | AddressOf access_expr -> - aux accum (Access.TakeAddress :: accesses) access_expr - | Dereference access_expr -> - aux accum (Access.Dereference :: accesses) access_expr - in - aux init [] access_expr - - - let to_accesses access_expr = - let (), base, accesses = - to_accesses_fold access_expr ~init:() ~f_array_offset:(fun () index -> ((), index)) - in - (base, accesses) - - - let add_access access access_expr = - match (access : _ Access.t) with - | FieldAccess fld -> - Some (field_offset access_expr fld) - | ArrayAccess (typ, _index) -> - Some (array_offset access_expr typ None) - | Dereference -> - Some (dereference access_expr) - | TakeAddress -> - address_of access_expr - - - let add_rev_accesses rev_accesses access_expr = - List.fold rev_accesses ~init:(Some access_expr) ~f:(fun access_expr_opt access -> - let open Option.Monad_infix in - access_expr_opt >>= add_access access ) - - - let add_accesses accesses access_expr = add_rev_accesses (List.rev accesses) access_expr - (** convert to an AccessPath.t, ignoring AddressOf and Dereference for now *) let rec to_access_path t = let rec to_access_path_ t = @@ -366,16 +322,6 @@ module AccessExpression = struct init | Sizeof (_, exp_opt) -> fold_vars_exp_opt exp_opt ~init ~f - - - let appears_in_source_code access_expr = - (* should probably eventually check more than just the base but yolo *) - let var, _ = get_base access_expr in - Var.appears_in_source_code var - - - let to_source_string access_expr = - if appears_in_source_code access_expr then Some (F.asprintf "%a" pp access_expr) else None end let rec get_typ tenv = function diff --git a/infer/src/IR/HilExp.mli b/infer/src/IR/HilExp.mli index 3628c185e..1f7eb5cae 100644 --- a/infer/src/IR/HilExp.mli +++ b/infer/src/IR/HilExp.mli @@ -41,7 +41,7 @@ and access_expression = private [@@deriving compare] module AccessExpression : sig - val of_id : Ident.t -> Typ.t -> access_expression + val of_id : Ident.t -> Typ.t -> access_expression [@@warning "-32"] val base : AccessPath.base -> access_expression @@ -56,15 +56,7 @@ module AccessExpression : sig [@@warning "-32"] (** address_of doesn't always make sense, eg [address_of (Dereference t)] is [None] *) - val address_of_base : AccessPath.base -> access_expression - - val to_accesses_fold : - access_expression - -> init:'accum - -> f_array_offset:('accum -> t option -> 'accum * 'array_index) - -> 'accum * AccessPath.base * 'array_index Access.t list - - val to_accesses : access_expression -> AccessPath.base * t option Access.t list + val address_of_base : AccessPath.base -> access_expression [@@warning "-32"] val to_access_path : access_expression -> AccessPath.t @@ -92,18 +84,6 @@ module AccessExpression : sig [@@deriving compare] val fold_vars : (t, Var.t, 'accum) Container.fold - - val add_access : _ Access.t -> t -> t option - - val add_accesses : _ Access.t list -> t -> t option - - val add_rev_accesses : _ Access.t list -> t -> t option - - val appears_in_source_code : t -> bool - - val to_source_string : t -> string option - (** get a string representation of the access expression in terms of symbols that appear in the - program, to show to the user *) end val pp : F.formatter -> t -> unit diff --git a/infer/src/IR/HilInstr.mli b/infer/src/IR/HilInstr.mli index 6a28b4dbb..4577d0d8b 100644 --- a/infer/src/IR/HilInstr.mli +++ b/infer/src/IR/HilInstr.mli @@ -11,7 +11,7 @@ module F = Format (** type of a procedure call; either direct or via function pointer *) type call = Direct of Typ.Procname.t | Indirect of HilExp.AccessExpression.t [@@deriving compare] -val pp_call : F.formatter -> call -> unit +val pp_call : F.formatter -> call -> unit [@@warning "-32"] type t = | Assign of HilExp.AccessExpression.t * HilExp.t * Location.t diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml index 059d85851..8c82ec3be 100644 --- a/infer/src/IR/Sil.ml +++ b/infer/src/IR/Sil.ml @@ -57,7 +57,7 @@ type instr = - [typ] is the root type of [lexp1] - - [exp2] is the expression whose value is store. *) + - [exp2] is the expression whose value is stored. *) | Prune of Exp.t * Location.t * bool * if_kind (** prune the state based on [exp=1], the boolean indicates whether true branch *) | Call of (Ident.t * Typ.t) * Exp.t * (Exp.t * Typ.t) list * Location.t * CallFlags.t diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index f03c28ec8..01a161e01 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -10,6 +10,7 @@ module L = Logging open Result.Monad_infix module AbstractAddress = PulseDomain.AbstractAddress module InterprocAction = PulseDomain.InterprocAction +module Invalidation = PulseDomain.Invalidation module ValueHistory = PulseDomain.ValueHistory include (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *) @@ -45,114 +46,87 @@ module Payload = SummaryPayload.Make (struct let field = Payloads.Fields.pulse end) +let proc_name_of_call call_exp = + match (call_exp : Exp.t) with + | Const (Cfun proc_name) | Closure {name= proc_name} -> + Some proc_name + | _ -> + None + + module PulseTransferFunctions = struct module CFG = ProcCfg.Exceptional module Domain = PulseAbductiveDomain type extras = Summary.t - let rec exec_assign summary (lhs_access : HilExp.AccessExpression.t) (rhs_exp : HilExp.t) loc - astate = - (* try to evaluate [rhs_exp] down to an abstract address or generate a fresh one *) - let crumb = - ValueHistory.Assignment - {lhs= PulseAbductiveDomain.explain_access_expr lhs_access astate; location= loc} - in - match rhs_exp with - | AccessExpression rhs_access -> ( - PulseOperations.read loc rhs_access astate - >>= fun (astate, (rhs_addr, rhs_trace)) -> - let return_addr_trace = (rhs_addr, crumb :: rhs_trace) in - PulseOperations.write loc lhs_access return_addr_trace astate - >>= fun astate -> - match lhs_access with - | Base (var, _) when Var.is_return var -> - PulseOperations.check_address_escape loc summary.Summary.proc_desc rhs_addr rhs_trace - astate - | _ -> - Ok astate ) - | Closure (pname, captured) -> - PulseOperations.Closures.record loc lhs_access pname captured astate - | Cast (_, e) -> - exec_assign summary lhs_access e loc astate - | _ -> - PulseOperations.read_all loc (HilExp.get_access_exprs rhs_exp) astate - >>= PulseOperations.havoc [crumb] loc lhs_access - - - let exec_unknown_call _summary ret (call : HilInstr.call) (actuals : HilExp.t list) _flags - call_loc astate = - let read_all args astate = - PulseOperations.read_all call_loc (List.concat_map args ~f:HilExp.get_access_exprs) astate - in - let crumb = - ValueHistory.Call - { f= `HilCall call - ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate) - ; location= call_loc } - in - let havoc_ret (ret, _) astate = PulseOperations.havoc_var [crumb] ret astate in - let read_actuals_havoc_ret actuals ret astate = read_all actuals astate >>| havoc_ret ret in - match call with - | Direct callee_pname when Typ.Procname.is_constructor callee_pname -> ( + let exec_unknown_call reason ret call actuals _flags call_loc astate = + let event = ValueHistory.Call {f= reason; location= call_loc} in + let havoc_ret (ret, _) astate = PulseOperations.havoc_id ret [event] astate in + match proc_name_of_call call with + | Some callee_pname when Typ.Procname.is_constructor callee_pname -> ( L.d_printfln "constructor call detected@." ; match actuals with - | AccessExpression constructor_access :: rest -> - let constructed_object = HilExp.AccessExpression.dereference constructor_access in - PulseOperations.havoc [crumb] call_loc constructed_object astate - >>= read_actuals_havoc_ret rest ret + | (object_ref, _) :: _ -> + PulseOperations.havoc_deref call_loc object_ref [event] astate >>| havoc_ret ret | _ -> Ok (havoc_ret ret astate) ) - | Direct (Typ.Procname.ObjC_Cpp callee_pname) + | Some (Typ.Procname.ObjC_Cpp callee_pname) when Typ.Procname.ObjC_Cpp.is_operator_equal callee_pname -> ( L.d_printfln "operator= detected@." ; match actuals with (* copy assignment *) - | [AccessExpression lhs; HilExp.AccessExpression rhs] -> - let lhs_deref = HilExp.AccessExpression.dereference lhs in - let rhs_deref = HilExp.AccessExpression.dereference rhs in - PulseOperations.havoc [crumb] call_loc lhs_deref astate - >>= fun astate -> - PulseOperations.read call_loc rhs_deref astate >>| fst >>| havoc_ret ret + | [(lhs, _); _rhs] -> + PulseOperations.havoc_deref call_loc lhs [event] astate >>| havoc_ret ret | _ -> - read_actuals_havoc_ret actuals ret astate ) + Ok (havoc_ret ret astate) ) | _ -> L.d_printfln "skipping unknown procedure@." ; - read_actuals_havoc_ret actuals ret astate + Ok (havoc_ret ret astate) - let interprocedural_call caller_summary ret (call : HilInstr.call) (actuals : HilExp.t list) - flags call_loc astate = - let unknown_function () = - exec_unknown_call caller_summary ret call actuals flags call_loc astate >>| List.return + let interprocedural_call caller_summary ret call_exp actuals flags call_loc astate = + let unknown_function reason = + exec_unknown_call reason ret call_exp actuals flags call_loc astate >>| List.return in - match call with - | Direct callee_pname -> ( + match proc_name_of_call call_exp with + | Some callee_pname -> ( match Payload.read_full caller_summary.Summary.proc_desc callee_pname with | Some (callee_proc_desc, preposts) -> let formals = Procdesc.get_formals callee_proc_desc |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar) in - PulseOperations.Interproc.call callee_pname ~formals ~ret ~actuals flags call_loc astate - preposts + (* call {!PulseAbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *) + List.fold_result preposts ~init:[] ~f:(fun posts pre_post -> + (* apply all pre/post specs *) + PulseAbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~actuals + astate + >>| fun (post, return_val_opt) -> + let event = ValueHistory.Call {f= `Call call_exp; location= call_loc} in + let post = + match return_val_opt with + | Some return_val -> + PulseOperations.write_id (fst ret) (return_val, [event]) post + | None -> + PulseOperations.havoc_id (fst ret) [event] post + in + post :: posts ) | None -> (* no spec found for some reason (unknown function, ...) *) L.d_printfln "No spec found for %a@\n" Typ.Procname.pp callee_pname ; - unknown_function () ) - | Indirect access_expression -> - L.d_printfln "Indirect call %a@\n" HilExp.AccessExpression.pp access_expression ; - unknown_function () + unknown_function (`UnknownCall call_exp) ) + | None -> + L.d_printfln "Indirect call %a@\n" Exp.pp call_exp ; + unknown_function (`IndirectCall call_exp) (** has an object just gone out of scope? *) - let get_out_of_scope_object (call : HilInstr.call) (actuals : HilExp.t list) - (flags : CallFlags.t) = + let get_out_of_scope_object call_exp actuals (flags : CallFlags.t) = (* injected destructors are precisely inserted where an object goes out of scope *) if flags.cf_injected_destructor then - match (call, actuals) with - | ( Direct (Typ.Procname.ObjC_Cpp pname) - , [AccessExpression (AddressOf (Base (ProgramVar pvar, typ)))] ) + match (proc_name_of_call call_exp, actuals) with + | Some (Typ.Procname.ObjC_Cpp pname), [(Exp.Lvar pvar, typ)] when Pvar.is_local pvar && not (Typ.Procname.ObjC_Cpp.is_inner_destructor pname) -> (* ignore inner destructors, only trigger out of scope on the final destructor call *) Some (pvar, typ) @@ -163,36 +137,44 @@ 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) astate = - (* invalidate both [&x] and [x]: reading either is now forbidden *) - let invalidate pvar typ access astate = - PulseOperations.invalidate - (InterprocAction.Immediate {imm= GoneOutOfScope (pvar, typ); location= call_loc}) - call_loc access astate + let event = + InterprocAction.Immediate {imm= Invalidation.GoneOutOfScope (pvar, typ); location= call_loc} in - let out_of_scope_base = HilExp.AccessExpression.base (Var.of_pvar pvar, typ) in - invalidate pvar typ (HilExp.AccessExpression.dereference out_of_scope_base) astate - >>= invalidate pvar typ out_of_scope_base - - - let dispatch_call summary ret (call : HilInstr.call) (actuals : HilExp.t list) flags call_loc - astate = + (* invalidate both [&x] and [x]: reading either is now forbidden *) + PulseOperations.eval call_loc (Exp.Lvar pvar) astate + >>= fun (astate, out_of_scope_base) -> + PulseOperations.invalidate_deref call_loc event out_of_scope_base astate + >>= PulseOperations.invalidate call_loc event out_of_scope_base + + + let dispatch_call summary ret call_exp actuals call_loc flags astate = + (* evaluate all actuals *) + List.fold_result actuals ~init:(astate, []) + ~f:(fun (astate, rev_actuals_evaled) (actual_exp, actual_typ) -> + PulseOperations.eval call_loc actual_exp astate + >>| fun (astate, actual_evaled) -> + (astate, (actual_evaled, actual_typ) :: rev_actuals_evaled) ) + >>= fun (astate, rev_actuals_evaled) -> + let actuals_evaled = List.rev rev_actuals_evaled in let model = - match call with - | Indirect _ -> + match proc_name_of_call call_exp with + | Some callee_pname -> + PulseModels.dispatch callee_pname flags + | None -> (* function pointer, etc.: skip for now *) None - | Direct callee_pname -> - PulseModels.dispatch callee_pname flags in match model with | Some model -> - model call_loc ~ret ~actuals astate + model call_loc ~ret ~actuals:actuals_evaled astate | None -> ( (* do interprocedural call then destroy objects going out of scope *) PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ; - let posts = interprocedural_call summary ret call actuals flags call_loc astate in + let posts = + interprocedural_call summary ret call_exp actuals_evaled flags call_loc astate + in PerfEvent.(log (fun logger -> log_end_event logger ())) ; - match get_out_of_scope_object call actuals flags with + match get_out_of_scope_object call_exp actuals flags with | Some pvar_typ -> L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ; posts @@ -203,66 +185,46 @@ module PulseTransferFunctions = struct posts ) - let hil_of_sil ?(add_deref = false) exp typ = - HilExp.of_sil ~include_array_indexes:true ~f_resolve_id:(fun _ -> None) ~add_deref exp typ - - let exec_instr (astate : Domain.t) {ProcData.extras= summary} _cfg_node (instr : Sil.instr) = match instr with - | Load (lhs_id, rhs_exp, typ, loc) -> - let lhs_access = HilExp.AccessExpression.of_id lhs_id typ in - let rhs_hexp = hil_of_sil ~add_deref:true rhs_exp typ in - let post = exec_assign summary lhs_access rhs_hexp loc astate |> check_error summary in - [post] - | Store (lhs_exp, typ, rhs_exp, loc) -> - let lhs_access_expr = - match - HilExp.access_expr_of_exp ~include_array_indexes:true - ~f_resolve_id:(fun _ -> None) - lhs_exp typ - with - | Some access_expr -> - access_expr - | None -> - L.die InternalError "Non-assignable LHS expression %a at %a" Exp.pp lhs_exp - Location.pp_file_pos loc + | Load (lhs_id, rhs_exp, _typ, loc) -> + (* [lhs_id := *rhs_exp] *) + let result = + PulseOperations.eval_deref loc rhs_exp astate + >>| fun (astate, (rhs_addr, rhs_history)) -> + PulseOperations.write_id lhs_id (rhs_addr, rhs_history) astate in - let rhs_hexp = hil_of_sil rhs_exp typ in - let post = - exec_assign summary lhs_access_expr rhs_hexp loc astate |> check_error summary + [check_error summary result] + | Store (lhs_exp, _typ, rhs_exp, loc) -> + (* [*lhs_exp := rhs_exp] *) + let event = ValueHistory.Assignment {location= loc} in + let result = + PulseOperations.eval loc rhs_exp astate + >>= fun (astate, (rhs_addr, rhs_history)) -> + PulseOperations.eval loc lhs_exp astate + >>= fun (astate, lhs_addr_hist) -> + PulseOperations.write_deref loc ~ref:lhs_addr_hist + ~obj:(rhs_addr, event :: rhs_history) + astate + >>= fun astate -> + match lhs_exp with + | Lvar pvar when Pvar.is_return pvar -> + PulseOperations.check_address_escape loc summary.Summary.proc_desc rhs_addr + rhs_history astate + | _ -> + Ok astate in - [post] + [check_error summary result] | Prune (condition, loc, _is_then_branch, _if_kind) -> - let condition_hexp = hil_of_sil condition (Typ.mk (Tint IBool)) in - let post = - PulseOperations.read_all loc (HilExp.get_access_exprs condition_hexp) astate - |> check_error summary - in + (* ignored for now *) + let post = PulseOperations.eval loc condition astate |> check_error summary |> fst in [post] - | Call ((ret_id, ret_typ), call_exp, actuals, loc, call_flags) -> - let ret_hil = (Var.of_id ret_id, ret_typ) in - let call_hil = - match hil_of_sil call_exp (Typ.mk Tvoid) with - | Constant (Cfun procname) | Closure (procname, _) -> - HilInstr.Direct procname - | HilExp.AccessExpression access_expr -> - HilInstr.Indirect access_expr - | call_exp -> - L.(die InternalError) "Unexpected call expression %a" HilExp.pp call_exp - in - let actuals_hil = List.map ~f:(fun (exp, typ) -> hil_of_sil exp typ) actuals in - let posts = - dispatch_call summary ret_hil call_hil actuals_hil call_flags loc astate - |> check_error summary - in - posts + | Call (ret, call_exp, actuals, loc, call_flags) -> + dispatch_call summary ret call_exp actuals loc call_flags astate |> check_error summary | Metadata (ExitScope (vars, _)) -> - let post = PulseOperations.remove_vars vars astate in - [post] + [PulseOperations.remove_vars vars astate] | Metadata (VariableLifetimeBegins (pvar, _, location)) -> - let var = Var.of_pvar pvar in - let post = PulseOperations.realloc_var var location astate in - [post] + [PulseOperations.realloc_var (Var.of_pvar pvar) location astate] | Metadata (Abstract _ | Nullify _ | Skip) -> [astate] diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 0f744698e..b61f4425c 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -85,12 +85,6 @@ let ( <= ) ~lhs ~rhs = ~rhs:(rhs.post :> PulseDomain.t) -let explain_access_expr access_expr {post} = - PulseDomain.explain_access_expr access_expr (post :> base_domain) - - -let explain_hil_exp hil_exp {post} = PulseDomain.explain_hil_exp hil_exp (post :> base_domain) - module Stack = struct let is_abducible astate var = (* HACK: formals are pre-registered in the initial state *) @@ -103,25 +97,25 @@ module Stack = struct if phys_equal new_post astate.post then astate else {astate with post= new_post} - let materialize var astate = + let eval var astate = match BaseStack.find_opt var (astate.post :> base_domain).stack with - | Some addr_loc_opt -> - (astate, addr_loc_opt) + | Some addr_hist -> + (astate, addr_hist) | None -> - let addr_loc_opt' = (AbstractAddress.mk_fresh (), None) in - let post_stack = BaseStack.add var addr_loc_opt' (astate.post :> base_domain).stack in + let addr_hist = (AbstractAddress.mk_fresh (), []) in + let post_stack = BaseStack.add var addr_hist (astate.post :> base_domain).stack in let pre = (* do not overwrite values of variables already in the pre *) if (not (BaseStack.mem var (astate.pre :> base_domain).stack)) && is_abducible astate var then - let foot_stack = BaseStack.add var addr_loc_opt' (astate.pre :> base_domain).stack in + let foot_stack = BaseStack.add var addr_hist (astate.pre :> base_domain).stack in let foot_heap = - BaseMemory.register_address (fst addr_loc_opt') (astate.pre :> base_domain).heap + BaseMemory.register_address (fst addr_hist) (astate.pre :> base_domain).heap in InvertedDomain.make foot_stack foot_heap else astate.pre in - ({post= Domain.update astate.post ~stack:post_stack; pre}, addr_loc_opt') + ({post= Domain.update astate.post ~stack:post_stack; pre}, addr_hist) let add var addr_loc_opt astate = @@ -140,6 +134,8 @@ module Stack = struct let fold f astate accum = BaseStack.fold f (astate.post :> base_domain).stack accum let find_opt var astate = BaseStack.find_opt var (astate.post :> base_domain).stack + + let mem var astate = BaseStack.mem var (astate.post :> base_domain).stack end module Memory = struct @@ -174,7 +170,7 @@ module Memory = struct map_post_heap astate ~f:(fun heap -> BaseMemory.add_edge addr access new_addr_trace heap) - let materialize_edge addr access astate = + let eval_edge addr access astate = match BaseMemory.find_edge_opt addr access (astate.post :> base_domain).heap with | Some addr_trace' -> (astate, addr_trace') @@ -224,11 +220,13 @@ let mk_initial proc_desc = correspond to formals *) let formals = let proc_name = Procdesc.get_proc_name proc_desc in - let location = Some (Procdesc.get_loc proc_desc) in + let location = Procdesc.get_loc proc_desc in Procdesc.get_formals proc_desc |> List.map ~f:(fun (mangled, _) -> let var = Var.of_pvar (Pvar.mk mangled proc_name) in - (var, (AbstractAddress.mk_fresh (), location)) ) + ( var + , (AbstractAddress.mk_fresh (), [PulseDomain.ValueHistory.VariableDeclaration location]) + ) ) in let initial_stack = List.fold formals ~init:(InvertedDomain.empty :> PulseDomain.t).stack @@ -323,14 +321,16 @@ module PrePost = struct let fold_globals_of_stack stack call_state ~f = Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:BaseStack.fold) stack ~init:call_state ~f:(fun call_state (var, stack_value) -> - if Var.is_global var then - let call_state, (addr_caller, _) = - let astate, var_value = Stack.materialize var call_state.astate in - if phys_equal astate call_state.astate then (call_state, var_value) - else ({call_state with astate}, var_value) - in - f var ~stack_value ~addr_caller call_state - else Ok call_state ) + match var with + | Var.ProgramVar pvar when Pvar.is_global pvar -> + let call_state, (addr_caller, _) = + let astate, var_value = Stack.eval var call_state.astate in + if phys_equal astate call_state.astate then (call_state, var_value) + else ({call_state with astate}, var_value) + in + f pvar ~stack_value ~addr_caller call_state + | _ -> + Ok call_state ) let visit call_state ~addr_callee ~addr_caller = @@ -361,8 +361,8 @@ module PrePost = struct (** Materialize the (abstract memory) subgraph of [pre] reachable from [addr_pre] in [call_state.astate] starting from address [addr_caller]. Report an error if some invalid addresses are traversed in the process. *) - let rec materialize_pre_from_address callee_proc_name call_location access_expr ~pre ~addr_pre - ~addr_caller history call_state = + let rec materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre ~addr_caller + history call_state = let mk_action action = PulseDomain.InterprocAction.ViaCall {action; proc_name= callee_proc_name; location= call_location} @@ -381,25 +381,17 @@ module PrePost = struct | Error invalidated_by -> Error (PulseDiagnostic.AccessToInvalidAddress - { access= explain_access_expr access_expr call_state.astate - ; invalidated_by - ; accessed_by= {action; history} }) + {invalidated_by; accessed_by= {action; history}}) | Ok astate -> let call_state = {call_state with astate} in Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) ~init:call_state edges_pre ~f:(fun call_state (access, (addr_pre_dest, _)) -> let astate, (addr_caller_dest, _) = - Memory.materialize_edge addr_caller access call_state.astate + Memory.eval_edge addr_caller access call_state.astate in let call_state = {call_state with astate} in - let access_expr = - (* if the new access expression doesn't make sense then keep the old one; should - be fine since this is used only for reporting *) - HilExp.AccessExpression.add_access access access_expr - |> Option.value ~default:access_expr - in - materialize_pre_from_address callee_proc_name call_location access_expr ~pre + materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre:addr_pre_dest ~addr_caller:addr_caller_dest history call_state )) |> function Some result -> result | None -> Ok call_state ) @@ -408,22 +400,16 @@ module PrePost = struct has been instantiated with the corresponding [actual] into the current state [call_state.astate] *) let materialize_pre_from_actual callee_proc_name call_location ~pre ~formal ~actual call_state = - L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal (Pp.option AbstractAddress.pp) - (Option.map ~f:fst3 actual) ; - match actual with - | None -> - (* the expression representing the actual couldn't be evaluated down to an abstract address - *) - Ok call_state - | Some (addr_caller, access_expr, trace) -> ( - (let open Option.Monad_infix in - PulseDomain.Stack.find_opt formal pre.PulseDomain.stack - >>= fun (addr_formal_pre, _) -> - PulseDomain.Memory.find_edge_opt addr_formal_pre Dereference pre.PulseDomain.heap - >>| fun (formal_pre, _) -> - materialize_pre_from_address callee_proc_name call_location access_expr ~pre - ~addr_pre:formal_pre ~addr_caller trace call_state) - |> function Some result -> result | None -> Ok call_state ) + let addr_caller, trace = actual in + L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal AbstractAddress.pp addr_caller ; + (let open Option.Monad_infix in + PulseDomain.Stack.find_opt formal pre.PulseDomain.stack + >>= fun (addr_formal_pre, _) -> + PulseDomain.Memory.find_edge_opt addr_formal_pre Dereference pre.PulseDomain.heap + >>| fun (formal_pre, _) -> + materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre:formal_pre + ~addr_caller trace call_state) + |> function Some result -> result | None -> Ok call_state let is_cell_read_only ~cell_pre_opt ~cell_post:(edges_post, attrs_post) = @@ -448,7 +434,7 @@ module PrePost = struct call [materialize_pre_from] on them. Give up if calling the function introduces aliasing. *) match - IList.fold2_result formals actuals ~init:call_state ~f:(fun call_state formal actual -> + IList.fold2_result formals actuals ~init:call_state ~f:(fun call_state formal (actual, _) -> materialize_pre_from_actual callee_proc_name call_location ~pre:(pre_post.pre :> PulseDomain.t) ~formal ~actual call_state ) @@ -463,15 +449,10 @@ module PrePost = struct let materialize_pre_for_globals callee_proc_name call_location pre_post call_state = fold_globals_of_stack (pre_post.pre :> PulseDomain.t).stack call_state - ~f:(fun var ~stack_value:(addr_pre, loc_opt) ~addr_caller call_state -> - let trace = - Option.map loc_opt ~f:(fun loc -> PulseDomain.ValueHistory.VariableDeclaration loc) - |> Option.to_list - in - let access_expr = HilExp.AccessExpression.base (var, Typ.void) in - materialize_pre_from_address callee_proc_name call_location access_expr + ~f:(fun _var ~stack_value:(addr_pre, history) ~addr_caller call_state -> + materialize_pre_from_address callee_proc_name call_location ~pre:(pre_post.pre :> PulseDomain.t) - ~addr_pre ~addr_caller trace call_state ) + ~addr_pre ~addr_caller history call_state ) let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state = @@ -591,7 +572,7 @@ module PrePost = struct ( subst , ( addr_curr , PulseDomain.ValueHistory.Call - {f= `HilCall (Direct callee_proc_name); actuals= [ (* TODO *) ]; location= call_loc} + {f= `Call (Const (Cfun callee_proc_name)); location= call_loc} :: trace_post ) ) ) in let caller_post = @@ -608,36 +589,50 @@ module PrePost = struct let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual call_state = - L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal - (Pp.option AbstractAddress.pp) (Option.map ~f:fst3 actual) ; - match actual with + let addr_caller, _ = actual in + L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal AbstractAddress.pp + addr_caller ; + match + let open Option.Monad_infix in + PulseDomain.Stack.find_opt formal (pre_post.pre :> PulseDomain.t).PulseDomain.stack + >>= fun (addr_formal_pre, _) -> + PulseDomain.Memory.find_edge_opt addr_formal_pre Dereference + (pre_post.pre :> PulseDomain.t).PulseDomain.heap + >>| fun (formal_pre, _) -> + record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:formal_pre + ~addr_caller call_state + with + | Some call_state -> + call_state | None -> call_state - | Some (addr_caller, _access_expr, _trace) -> ( - let open Option.Monad_infix in - match - PulseDomain.Stack.find_opt formal (pre_post.pre :> PulseDomain.t).PulseDomain.stack - >>= fun (addr_formal_pre, _) -> - PulseDomain.Memory.find_edge_opt addr_formal_pre Dereference - (pre_post.pre :> PulseDomain.t).PulseDomain.heap - >>| fun (formal_pre, _) -> - record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:formal_pre - ~addr_caller call_state - with - | Some call_state -> - call_state - | None -> - call_state ) - let record_post_for_return callee_proc_name call_loc pre_post ~ret call_state = + let record_post_for_return callee_proc_name call_loc pre_post call_state = let return_var = Var.of_pvar (Pvar.get_ret_pvar callee_proc_name) in match PulseDomain.Stack.find_opt return_var (pre_post.post :> PulseDomain.t).stack with - | Some (addr_return, _) -> - record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:addr_return - ~addr_caller:(fst ret) call_state | None -> - call_state + (call_state, None) + | Some (addr_return, _) -> ( + match + PulseDomain.Memory.find_edge_opt addr_return Dereference + (pre_post.post :> PulseDomain.t).PulseDomain.heap + with + | None -> + (call_state, None) + | Some (return_callee, _) -> + let return_caller = + match AddressMap.find_opt return_callee call_state.subst with + | Some return_caller -> + return_caller + | None -> + AbstractAddress.mk_fresh () + in + let call_state = + record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:return_callee + ~addr_caller:return_caller call_state + in + (call_state, Some return_caller) ) let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals @@ -648,7 +643,7 @@ module PrePost = struct between pre and post since it's unreliable, eg replace value read in pre with same value in 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 -> + 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 ) with @@ -673,15 +668,15 @@ module PrePost = struct call_state - let apply_post callee_proc_name call_location pre_post ~formals ~ret ~actuals call_state = + let apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state = PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ; let r = apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state |> Option.map ~f:(fun call_state -> apply_post_for_globals callee_proc_name call_location pre_post call_state - |> record_post_for_return callee_proc_name call_location pre_post ~ret - |> fun {astate; _} -> astate ) + |> record_post_for_return callee_proc_name call_location pre_post + |> fun ({astate; _}, return_caller) -> (astate, return_caller) ) in PerfEvent.(log (fun logger -> log_end_event logger ())) ; r @@ -701,7 +696,7 @@ module PrePost = struct the noise that this will introduce since we don't care about values. For instance, if the pre is for a path where [formal != 0] and we pass [0] then it will be an FP. Maybe the solution is to bake in some value analysis. *) - let apply callee_proc_name call_location pre_post ~formals ~ret ~actuals astate = + let apply callee_proc_name call_location pre_post ~formals ~actuals astate = L.d_printfln "Applying pre/post for %a(%a):@\n%a" Typ.Procname.pp callee_proc_name (Pp.seq ~sep:"," Var.pp) formals pp pre_post ; let empty_call_state = @@ -714,11 +709,11 @@ module PrePost = struct | exception Aliasing -> (* can't make sense of the pre-condition in the current context: give up on that particular pre/post pair *) - Ok astate + Ok (astate, None) | None -> (* couldn't apply the pre for some technical reason (as in: not by the fault of the programmer as far as we know) *) - Ok astate + Ok (astate, None) | Some (Error _ as error) -> (* error: the function call requires to read some state known to be invalid *) error @@ -726,18 +721,13 @@ module PrePost = struct (* reset [visited] *) let call_state = {call_state with visited= AddressSet.empty} in (* apply the postcondition *) - match - apply_post callee_proc_name call_location pre_post ~formals ~ret ~actuals call_state - with + match apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state with | exception Aliasing -> - Ok astate + Ok (astate, None) | None -> (* same as when trying to apply the pre: give up for that pre/post pair and return the original state *) - Ok astate + Ok (astate, None) | Some astate_post -> Ok astate_post ) end - -let explain_access_expr access_expr {post} = - PulseDomain.explain_access_expr access_expr (post :> base_domain) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 8ea31aee3..33ee62724 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -29,7 +29,10 @@ module Stack : sig val find_opt : Var.t -> t -> PulseDomain.Stack.value option - val materialize : Var.t -> t -> t * PulseDomain.Stack.value + val eval : Var.t -> t -> t * PulseDomain.AddrTracePair.t + (** return the value of the variable in the stack or create a fresh one if needed *) + + val mem : Var.t -> t -> bool end (** stack operations like {!PulseDomain.Heap} but that also take care of propagating facts to the @@ -43,7 +46,7 @@ module Memory : sig val add_edge : AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t val check_valid : - HilExp.AccessExpression.t PulseDomain.explained PulseDomain.InterprocAction.t + unit PulseDomain.InterprocAction.t -> AbstractAddress.t -> t -> (t, PulseDomain.Invalidation.t PulseDomain.Trace.t) result @@ -62,7 +65,9 @@ module Memory : sig val std_vector_reserve : AbstractAddress.t -> t -> t - val materialize_edge : AbstractAddress.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t + val eval_edge : AbstractAddress.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t + (** [eval_edge addr access astate] follows the edge [addr --access--> .] in memory and returns + what it points to or creates a fresh value if that edge didn't exist. *) end module PrePost : sig @@ -79,18 +84,12 @@ module PrePost : sig -> Location.t -> t -> formals:Var.t list - -> ret:AbstractAddress.t * PulseDomain.ValueHistory.t - -> actuals:(AbstractAddress.t * HilExp.AccessExpression.t * PulseDomain.ValueHistory.t) option - list + -> actuals:((AbstractAddress.t * PulseDomain.ValueHistory.t) * Typ.t) list -> domain_t - -> (domain_t, PulseDiagnostic.t) result + -> (domain_t * AbstractAddress.t option, PulseDiagnostic.t) result + (** return the abstract state after the call along with an optional return value *) end val discard_unreachable : t -> t (** garbage collect unreachable addresses in the state to make it smaller, just for convenience and keep its size down *) - -val explain_access_expr : - HilExp.AccessExpression.t -> t -> HilExp.AccessExpression.t PulseDomain.explained - -val explain_hil_exp : HilExp.t -> t -> HilExp.t PulseDomain.explained diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index 9626533cc..931267545 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -10,9 +10,8 @@ module F = Format type t = | AccessToInvalidAddress of - { access: HilExp.AccessExpression.t PulseDomain.explained - ; invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t - ; accessed_by: HilExp.AccessExpression.t PulseDomain.explained PulseDomain.Trace.t } + { invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t + ; accessed_by: unit PulseDomain.Trace.t } | StackVariableAddressEscape of { variable: Var.t ; history: PulseDomain.ValueHistory.t @@ -26,7 +25,7 @@ let get_location = function let get_message = function - | AccessToInvalidAddress {access; accessed_by; invalidated_by; _} -> + | AccessToInvalidAddress {accessed_by; invalidated_by; _} -> (* The goal is to get one of the following messages depending on the scenario: 42: delete x; return x->f @@ -44,47 +43,13 @@ let get_message = function Likewise if we don't have "x" in the second part but instead some non-user-visible expression, then "`x->f` accesses `x`, which was invalidated at line 42 by `delete`" *) - let pp_access_trace invalidated f - (trace : HilExp.AccessExpression.t PulseDomain.explained PulseDomain.Trace.t) = + let pp_access_trace f (trace : _ PulseDomain.Trace.t) = match trace.action with - | Immediate {imm= access; _} -> ( - match HilExp.AccessExpression.to_source_string (access :> HilExp.AccessExpression.t) with - | Some access_s - when HilExp.AccessExpression.equal (access :> HilExp.AccessExpression.t) invalidated -> - F.fprintf f "`%s` " access_s - | Some access_s -> ( - match HilExp.AccessExpression.to_source_string invalidated with - | Some invalidated_s -> - F.fprintf f "`%s` accesses `%s`, which " access_s invalidated_s - | None -> - F.fprintf f "access to `%s`, which " access_s ) - | None -> ( - match HilExp.AccessExpression.to_source_string invalidated with - | Some invalidated_s -> - F.fprintf f "`%s` " invalidated_s - | None -> - F.fprintf f "accessing memory that " ) ) - | ViaCall {action; proc_name; _} -> ( - let access_and_invalidated_s = - match - ( HilExp.AccessExpression.to_source_string - (PulseDomain.InterprocAction.get_immediate action :> HilExp.AccessExpression.t) - , HilExp.AccessExpression.to_source_string invalidated ) - with - | Some access_s, Some invalidated_s -> - Some (access_s, invalidated_s) - | Some s, None | None, Some s -> - Some (s, s) - | None, None -> - None - in - match access_and_invalidated_s with - | Some (access_s, invalidated_s) -> - F.fprintf f "call to `%a` eventually accesses `%s` but `%s` " Typ.Procname.describe - proc_name access_s invalidated_s - | None -> - F.fprintf f "call to `%a` eventually accesses `%a`, which " Typ.Procname.describe - proc_name HilExp.AccessExpression.pp invalidated ) + | Immediate {imm= _; _} -> + F.fprintf f "accessing memory that " + | ViaCall {proc_name; _} -> + F.fprintf f "call to `%a` eventually accesses memory that " Typ.Procname.describe + proc_name in let pp_invalidation_trace line f trace = match trace.PulseDomain.Trace.action with @@ -103,9 +68,7 @@ let get_message = function line in let invalidation_line = line_of_trace invalidated_by in - F.asprintf "%a%a" - (pp_access_trace (access :> HilExp.AccessExpression.t)) - accessed_by + F.asprintf "%a%a" pp_access_trace accessed_by (pp_invalidation_trace invalidation_line) invalidated_by | StackVariableAddressEscape {variable; _} -> @@ -123,9 +86,7 @@ let get_trace = function F.fprintf f "memory %a" PulseDomain.Invalidation.describe invalidation ) invalidated_by @@ PulseDomain.Trace.add_to_errlog ~header:"use-after-lifetime part of the trace starts here" - (fun f (access : HilExp.AccessExpression.t PulseDomain.explained) -> - F.fprintf f "invalid access to `%a`" HilExp.AccessExpression.pp - (access :> HilExp.AccessExpression.t) ) + (fun f () -> F.pp_print_string f "invalid access occurs here") accessed_by @@ [] | StackVariableAddressEscape {history; location; _} -> diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index 9992478e8..090726cac 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -10,9 +10,8 @@ open! IStd (** an error to report to the user *) type t = | AccessToInvalidAddress of - { access: HilExp.AccessExpression.t PulseDomain.explained - ; invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t - ; accessed_by: HilExp.AccessExpression.t PulseDomain.explained PulseDomain.Trace.t } + { invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t + ; accessed_by: unit PulseDomain.Trace.t } | StackVariableAddressEscape of { variable: Var.t ; history: PulseDomain.ValueHistory.t diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index 3c0ffc991..cd4756666 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -10,8 +10,6 @@ module L = Logging (* {2 Abstract domain description } *) -type 'a explained = 'a [@@deriving compare] - module Invalidation = struct type std_vector_function = | Assign @@ -44,17 +42,17 @@ module Invalidation = struct type t = - | CFree of HilExp.AccessExpression.t explained - | CppDelete of HilExp.AccessExpression.t explained + | CFree + | CppDelete | GoneOutOfScope of Pvar.t * Typ.t | Nullptr - | StdVector of std_vector_function * HilExp.AccessExpression.t explained + | StdVector of std_vector_function [@@deriving compare] let issue_type_of_cause = function - | CFree _ -> + | CFree -> IssueType.use_after_free - | CppDelete _ -> + | CppDelete -> IssueType.use_after_delete | GoneOutOfScope _ -> IssueType.use_after_lifetime @@ -64,12 +62,12 @@ module Invalidation = struct IssueType.vector_invalidation - let describe f = function - | CFree access_expr -> - F.fprintf f "was invalidated by call to `free()` on `%a`" HilExp.AccessExpression.pp - access_expr - | CppDelete access_expr -> - F.fprintf f "was invalidated by `delete` on `%a`" HilExp.AccessExpression.pp access_expr + let describe f cause = + match cause with + | CFree -> + F.pp_print_string f "was invalidated by call to `free()`" + | CppDelete -> + F.pp_print_string f "was invalidated by `delete`" | GoneOutOfScope (pvar, typ) -> let pp_var f pvar = if Pvar.is_cpp_temporary pvar then @@ -78,17 +76,16 @@ module Invalidation = struct in F.fprintf f "%a whose lifetime has ended" pp_var pvar | Nullptr -> - F.fprintf f "is the null pointer" - | StdVector (std_vector_f, access_expr) -> - F.fprintf f "was potentially invalidated by `%a()` on `%a`" pp_std_vector_function - std_vector_f HilExp.AccessExpression.pp access_expr + F.pp_print_string f "is the null pointer" + | StdVector std_vector_f -> + F.fprintf f "was potentially invalidated by `%a()`" pp_std_vector_function std_vector_f let pp f invalidation = match invalidation with - | CFree _ -> + | CFree -> F.fprintf f "CFree(%a)" describe invalidation - | CppDelete _ -> + | CppDelete -> F.fprintf f "CppDelete(%a)" describe invalidation | GoneOutOfScope _ -> describe f invalidation @@ -102,14 +99,10 @@ module ValueHistory = struct type event = | VariableDeclaration of Location.t | CppTemporaryCreated of Location.t - | Assignment of {lhs: HilExp.AccessExpression.t explained; location: Location.t} - | Capture of - { captured_as: AccessPath.base - ; captured: HilExp.AccessExpression.t explained - ; location: Location.t } + | Assignment of {location: Location.t} + | Capture of {captured_as: Pvar.t; location: Location.t} | Call of - { f: [`HilCall of HilInstr.call | `Model of string] - ; actuals: HilExp.t explained list + { f: [`Call of Exp.t | `UnknownCall of Exp.t | `IndirectCall of Exp.t | `Model of string] ; location: Location.t } [@@deriving compare] @@ -118,20 +111,22 @@ module ValueHistory = struct F.pp_print_string fmt "variable declared" | CppTemporaryCreated _ -> F.pp_print_string fmt "C++ temporary created" - | Capture {captured_as; captured; location= _} -> - F.fprintf fmt "`%a` captured as `%a`" HilExp.AccessExpression.pp captured - AccessPath.pp_base captured_as - | Assignment {lhs; location= _} -> - if HilExp.AccessExpression.appears_in_source_code lhs then - F.fprintf fmt "assigned to `%a`" HilExp.AccessExpression.pp lhs - | Call {f; actuals; location= _} -> + | Capture {captured_as; location= _} -> + F.fprintf fmt "value captured as `%a`" (Pvar.pp Pp.text) captured_as + | Assignment _ -> + F.pp_print_string fmt "assigned" + | Call {f; location= _} -> let pp_f fmt = function - | `HilCall call -> - F.fprintf fmt "%a" HilInstr.pp_call call + | `Call call_exp -> + F.fprintf fmt "`%a()`" Exp.pp call_exp + | `UnknownCall call_exp -> + F.fprintf fmt "unknown function `%a`" Exp.pp call_exp + | `IndirectCall call_exp -> + F.fprintf fmt "unresolved expression `%a`" Exp.pp call_exp | `Model model -> - F.pp_print_string fmt model + F.fprintf fmt "`%s()` (pulse model)" model in - F.fprintf fmt "returned from call to `%a(%a)`" pp_f f (Pp.seq ~sep:"," HilExp.pp) actuals + F.fprintf fmt "returned from call to %a" pp_f f let location_of_event = function @@ -239,8 +234,8 @@ end module Attribute = struct type t = | Invalid of Invalidation.t Trace.t - | MustBeValid of HilExp.AccessExpression.t explained InterprocAction.t - | AddressOfCppTemporary of Var.t * Location.t option + | MustBeValid of unit InterprocAction.t + | AddressOfCppTemporary of Var.t * ValueHistory.t | Closure of Typ.Procname.t | StdVectorReserve [@@deriving compare, variants] @@ -256,13 +251,7 @@ module Attribute = struct let must_be_valid_rank = - Variants.to_rank - (MustBeValid - (Immediate - { imm= - HilExp.AccessExpression.base - (AccessPath.base_of_pvar (Pvar.mk_global Mangled.self) Typ.void) - ; location= Location.dummy })) + Variants.to_rank (MustBeValid (Immediate {imm= (); location= Location.dummy})) let std_vector_reserve_rank = Variants.to_rank StdVectorReserve @@ -272,11 +261,11 @@ module Attribute = struct (Trace.pp Invalidation.pp) f invalidation | MustBeValid action -> F.fprintf f "MustBeValid (read by %a @ %a)" - (InterprocAction.pp HilExp.AccessExpression.pp) + (InterprocAction.pp (fun _ () -> ())) action Location.pp (InterprocAction.to_outer_location action) - | AddressOfCppTemporary (var, location_opt) -> - F.fprintf f "&%a (%a)" Var.pp var (Pp.option Location.pp) location_opt + | AddressOfCppTemporary (var, history) -> + F.fprintf f "&%a (%a)" Var.pp var ValueHistory.pp history | Closure pname -> Typ.Procname.pp f pname | StdVectorReserve -> @@ -532,22 +521,16 @@ module Stack = struct F.fprintf f "%a%a" pp_ampersand var Var.pp var end - module VarValue = struct - type t = AbstractAddress.t * Location.t option [@@deriving compare] - - let pp = Pp.pair ~fst:AbstractAddress.pp ~snd:(Pp.option Location.pp) - end - - include PrettyPrintable.MakePPMonoMap (VarAddress) (VarValue) + include PrettyPrintable.MakePPMonoMap (VarAddress) (AddrTracePair) let pp fmt m = let pp_item fmt (var_address, v) = - F.fprintf fmt "%a=%a" VarAddress.pp var_address VarValue.pp v + F.fprintf fmt "%a=%a" VarAddress.pp var_address AddrTracePair.pp v in PrettyPrintable.pp_collection ~pp_item fmt (bindings m) - let compare = compare VarValue.compare + let compare = compare AddrTracePair.compare end type t = {heap: Memory.t; stack: Stack.t} @@ -787,77 +770,3 @@ let reachable_addresses astate = ~init:() ~finish:Fn.id ~f:(fun () _ _ _ -> Continue ()) |> fst - - -let rec evaluate_accesses address accesses astate = - match accesses with - | [] -> - Some address - | access :: next_accesses -> - let open Option.Monad_infix in - Memory.find_edge_opt address access astate.heap - >>= fun (addr, _) -> evaluate_accesses addr next_accesses astate - - -let evaluate_access_path var should_deref astate = - let open Option.Monad_infix in - Stack.find_opt var astate.stack - >>= fun (addr_var, _) -> - if should_deref then evaluate_accesses addr_var [HilExp.Access.Dereference] astate - else Some addr_var - - -let explain_address address astate = - GraphVisit.fold astate ~init:() ~var_filter:Var.appears_in_source_code - ~finish:(fun _ -> None) - ~f:(fun () address' var accesses -> - if AbstractAddress.equal address address' then Stop (Some (var, accesses)) else Continue () - ) - |> snd - |> Option.bind ~f:(fun (var, rev_accesses) -> - let base = HilExp.AccessExpression.address_of_base (var, Typ.void) in - HilExp.AccessExpression.add_rev_accesses rev_accesses base ) - - -let explain_access_expr access_expr astate = - if HilExp.AccessExpression.appears_in_source_code access_expr then access_expr - else - let (base_var, _), accesses = HilExp.AccessExpression.to_accesses access_expr in - let should_deref, accesses_left = - match accesses with [HilExp.Access.TakeAddress] -> (false, []) | _ -> (true, accesses) - in - match - let open Option.Monad_infix in - evaluate_access_path base_var should_deref astate - >>= fun base_address -> - explain_address base_address astate >>= HilExp.AccessExpression.add_accesses accesses_left - with - | Some explained -> - explained - | None -> - L.d_printfln "Can't explain how to reach address %a from state %a" - HilExp.AccessExpression.pp access_expr pp astate ; - access_expr - - -let rec explain_hil_exp (e : HilExp.t) astate = - match e with - | AccessExpression access_expr -> - HilExp.AccessExpression (explain_access_expr access_expr astate) - | UnaryOperator (op, e', t) -> - HilExp.UnaryOperator (op, explain_hil_exp e' astate, t) - | BinaryOperator (op, e1, e2) -> - HilExp.BinaryOperator (op, explain_hil_exp e1 astate, explain_hil_exp e2 astate) - | Exception e' -> - HilExp.Exception (explain_hil_exp e' astate) - | Closure (proc_name, captured) -> - HilExp.Closure - (proc_name, List.map captured ~f:(fun (base, e') -> (base, explain_hil_exp e' astate))) - | Constant _ -> - e - | Cast (t, e') -> - HilExp.Cast (t, explain_hil_exp e' astate) - | Sizeof (t, Some e') -> - HilExp.Sizeof (t, Some (explain_hil_exp e' astate)) - | Sizeof (_, None) -> - e diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index a1f14b4bb..89c4fc4ef 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -8,8 +8,6 @@ open! IStd module F = Format -type 'a explained = private 'a - module Invalidation : sig type std_vector_function = | Assign @@ -25,11 +23,11 @@ module Invalidation : sig val pp_std_vector_function : Format.formatter -> std_vector_function -> unit type t = - | CFree of HilExp.AccessExpression.t explained - | CppDelete of HilExp.AccessExpression.t explained + | CFree + | CppDelete | GoneOutOfScope of Pvar.t * Typ.t | Nullptr - | StdVector of std_vector_function * HilExp.AccessExpression.t explained + | StdVector of std_vector_function [@@deriving compare] val issue_type_of_cause : t -> IssueType.t @@ -41,14 +39,10 @@ module ValueHistory : sig type event = | VariableDeclaration of Location.t | CppTemporaryCreated of Location.t - | Assignment of {lhs: HilExp.AccessExpression.t explained; location: Location.t} - | Capture of - { captured_as: AccessPath.base - ; captured: HilExp.AccessExpression.t explained - ; location: Location.t } + | Assignment of {location: Location.t} + | Capture of {captured_as: Pvar.t; location: Location.t} | Call of - { f: [`HilCall of HilInstr.call | `Model of string] - ; actuals: HilExp.t explained list + { f: [`Call of Exp.t | `UnknownCall of Exp.t | `IndirectCall of Exp.t | `Model of string] ; location: Location.t } type t = event list [@@deriving compare] @@ -82,8 +76,8 @@ end module Attribute : sig type t = | Invalid of Invalidation.t Trace.t - | MustBeValid of HilExp.AccessExpression.t explained InterprocAction.t - | AddressOfCppTemporary of Var.t * Location.t option + | MustBeValid of unit InterprocAction.t + | AddressOfCppTemporary of Var.t * ValueHistory.t | Closure of Typ.Procname.t | StdVectorReserve [@@deriving compare] @@ -92,7 +86,7 @@ end module Attributes : sig include PrettyPrintable.PPUniqRankSet with type elt = Attribute.t - val get_must_be_valid : t -> HilExp.AccessExpression.t explained InterprocAction.t option + val get_must_be_valid : t -> unit InterprocAction.t option end module AbstractAddress : sig @@ -117,21 +111,18 @@ module AbstractAddressSet : PrettyPrintable.PPSet with type elt = AbstractAddres module AbstractAddressMap : PrettyPrintable.PPMap with type key = AbstractAddress.t +module AddrTracePair : sig + type t = AbstractAddress.t * ValueHistory.t [@@deriving compare] +end + module Stack : sig - include - PrettyPrintable.MonoMap - with type key = Var.t - and type value = AbstractAddress.t * Location.t option + include PrettyPrintable.MonoMap with type key = Var.t and type value = AddrTracePair.t (* need to shadow the declaration in [MonoMap] even though it is unused since [MapS.compare] has a different type *) val compare : t -> t -> int [@@warning "-32"] end -module AddrTracePair : sig - type t = AbstractAddress.t * ValueHistory.t [@@deriving compare] -end - module Memory : sig module Access : PrettyPrintable.PrintableOrderedType with type t = AbstractAddress.t HilExp.Access.t @@ -194,7 +185,3 @@ type isograph_relation = val isograph_map : lhs:t -> rhs:t -> mapping -> isograph_relation val is_isograph : lhs:t -> rhs:t -> mapping -> bool - -val explain_access_expr : HilExp.AccessExpression.t -> t -> HilExp.AccessExpression.t explained - -val explain_hil_exp : HilExp.t -> t -> HilExp.t explained diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 55ba35b46..2fd930cd2 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -9,8 +9,8 @@ open Result.Monad_infix type exec_fun = Location.t - -> ret:Var.t * Typ.t - -> actuals:HilExp.t list + -> ret:Ident.t * Typ.t + -> actuals:(PulseDomain.AddrTracePair.t * Typ.t) list -> PulseAbductiveDomain.t -> PulseAbductiveDomain.t list PulseOperations.access_result @@ -24,14 +24,10 @@ module C = struct let free : model = fun location ~ret:_ ~actuals astate -> match actuals with - | [AccessExpression deleted_access] -> - PulseOperations.invalidate - (PulseDomain.InterprocAction.Immediate - { imm= - PulseDomain.Invalidation.CFree - (PulseAbductiveDomain.explain_access_expr deleted_access astate) - ; location }) - location deleted_access astate + | [(deleted_access, _)] -> + PulseOperations.invalidate location + (PulseDomain.InterprocAction.Immediate {imm= PulseDomain.Invalidation.CFree; location}) + deleted_access astate >>| List.return | _ -> Ok [astate] @@ -40,63 +36,38 @@ end module Cplusplus = struct let delete : model = fun location ~ret:_ ~actuals astate -> - PulseOperations.read_all location (List.concat_map actuals ~f:HilExp.get_access_exprs) astate - >>= fun astate -> match actuals with - | [AccessExpression deleted_access] -> - PulseOperations.invalidate - (PulseDomain.InterprocAction.Immediate - { imm= - PulseDomain.Invalidation.CppDelete - (PulseAbductiveDomain.explain_access_expr deleted_access astate) - ; location }) - location deleted_access astate + | [(deleted_access, _)] -> + PulseOperations.invalidate location + (PulseDomain.InterprocAction.Immediate {imm= PulseDomain.Invalidation.CppDelete; location}) + deleted_access astate >>| List.return | _ -> Ok [astate] let operator_call : model = - fun location ~ret:(ret_var, _) ~actuals astate -> - PulseOperations.read_all location (List.concat_map actuals ~f:HilExp.get_access_exprs) astate - >>= fun astate -> + fun location ~ret:(ret_id, _) ~actuals astate -> ( match actuals with - | AccessExpression lambda :: _ -> - PulseOperations.read location HilExp.AccessExpression.(dereference lambda) astate - >>= fun (astate, address) -> - PulseOperations.Closures.check_captured_addresses location lambda (fst address) astate + | (lambda, _) :: _ -> + PulseOperations.Closures.check_captured_addresses + (PulseDomain.InterprocAction.Immediate {imm= (); location}) + (fst lambda) astate | _ -> Ok astate ) >>| fun astate -> - [ PulseOperations.havoc_var - [ PulseDomain.ValueHistory.Call - { f= `Model "" - ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate) - ; location } ] - ret_var astate ] + let event = PulseDomain.ValueHistory.Call {f= `Model ""; location} in + [PulseOperations.havoc_id ret_id [event] astate] let placement_new : model = - fun location ~ret:(ret_var, _) ~actuals astate -> - let read_all args astate = - PulseOperations.read_all location (List.concat_map args ~f:HilExp.get_access_exprs) astate - in - let crumb = - PulseDomain.ValueHistory.Call - { f= `Model "" - ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate) - ; location } - in + fun location ~ret:(ret_id, _) ~actuals astate -> + let event = PulseDomain.ValueHistory.Call {f= `Model ""; location} in match List.rev actuals with - | HilExp.AccessExpression expr :: other_actuals -> - PulseOperations.read location expr astate - >>= fun (astate, (address, trace)) -> - PulseOperations.write_var ret_var (address, crumb :: trace) astate - |> read_all other_actuals >>| List.return - | _ :: other_actuals -> - read_all other_actuals astate >>| PulseOperations.havoc_var [crumb] ret_var >>| List.return - | [] -> - Ok [PulseOperations.havoc_var [crumb] ret_var astate] + | ((address, _), _) :: _ -> + Ok [PulseOperations.write_id ret_id (address, [event]) astate] + | _ -> + Ok [PulseOperations.havoc_id ret_id [event] astate] end module StdVector = struct @@ -106,41 +77,39 @@ module StdVector = struct "__internal_array" - let to_internal_array vector = HilExp.AccessExpression.field_offset vector internal_array - - let deref_internal_array vector = - HilExp.AccessExpression.(dereference (to_internal_array vector)) + let to_internal_array location vector astate = + PulseOperations.eval_access location vector (FieldAccess internal_array) astate - let element_of_internal_array vector index = - HilExp.AccessExpression.array_offset (deref_internal_array vector) Typ.void index + let element_of_internal_array location vector index astate = + to_internal_array location vector astate + >>= fun (astate, vector_internal_array) -> + PulseOperations.eval_access location vector_internal_array + (ArrayAccess (Typ.void, index)) + astate let reallocate_internal_array trace vector vector_f location astate = - let array_address = to_internal_array vector in - let array = deref_internal_array vector in + to_internal_array location vector astate + >>= fun (astate, array_address) -> let invalidation = PulseDomain.InterprocAction.Immediate - { imm= - PulseDomain.Invalidation.StdVector - (vector_f, PulseAbductiveDomain.explain_access_expr vector astate) - ; location } + {imm= PulseDomain.Invalidation.StdVector vector_f; location} in - PulseOperations.invalidate_array_elements invalidation location array astate - >>= PulseOperations.invalidate invalidation location array - >>= PulseOperations.havoc trace location array_address + PulseOperations.invalidate_array_elements location invalidation array_address astate + >>= PulseOperations.invalidate_deref location invalidation array_address + >>= PulseOperations.havoc_field location vector internal_array trace let invalidate_references vector_f : model = fun location ~ret:_ ~actuals astate -> match actuals with - | AccessExpression vector :: _ -> + | (vector, _) :: _ -> let crumb = PulseDomain.ValueHistory.Call { f= `Model (Format.asprintf "%a" PulseDomain.Invalidation.pp_std_vector_function vector_f) - ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate) ; location } in reallocate_internal_array [crumb] vector vector_f location astate >>| List.return @@ -150,39 +119,22 @@ module StdVector = struct let at : model = fun location ~ret ~actuals astate -> - let crumb = - PulseDomain.ValueHistory.Call - { f= `Model "std::vector::at" - ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate) - ; location } - in + let event = PulseDomain.ValueHistory.Call {f= `Model "std::vector::at"; location} in match actuals with - | [AccessExpression vector_access_expr; index_exp] -> - PulseOperations.read location - (element_of_internal_array vector_access_expr (Some index_exp)) - astate - >>= fun (astate, (addr, trace)) -> - PulseOperations.write location - (HilExp.AccessExpression.base ret) - (addr, crumb :: trace) - astate - >>| List.return + | [(vector, _); (index, _)] -> + element_of_internal_array location vector (fst index) astate + >>| fun (astate, (addr, _)) -> [PulseOperations.write_id (fst ret) (addr, [event]) astate] | _ -> - Ok [PulseOperations.havoc_var [crumb] (fst ret) astate] + Ok [PulseOperations.havoc_id (fst ret) [event] astate] let reserve : model = fun location ~ret:_ ~actuals astate -> match actuals with - | [AccessExpression vector; _value] -> - let crumb = - PulseDomain.ValueHistory.Call - { f= `Model "std::vector::reserve" - ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate) - ; location } - in + | [(vector, _); _value] -> + let crumb = PulseDomain.ValueHistory.Call {f= `Model "std::vector::reserve"; location} in reallocate_internal_array [crumb] vector Reserve location astate - >>= PulseOperations.StdVector.mark_reserved location vector + >>| PulseAbductiveDomain.Memory.std_vector_reserve (fst vector) >>| List.return | _ -> Ok [astate] @@ -191,16 +143,9 @@ module StdVector = struct let push_back : model = fun location ~ret:_ ~actuals astate -> match actuals with - | [AccessExpression vector; _value] -> - let crumb = - PulseDomain.ValueHistory.Call - { f= `Model "std::vector::push_back" - ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate) - ; location } - in - PulseOperations.StdVector.is_reserved location vector astate - >>= fun (astate, is_reserved) -> - if is_reserved then + | [(vector, _); _value] -> + let crumb = PulseDomain.ValueHistory.Call {f= `Model "std::vector::push_back"; location} in + if PulseAbductiveDomain.Memory.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 (a perfect analysis would also make sure we don't exceed the reserved size) *) Ok [astate] diff --git a/infer/src/pulse/PulseModels.mli b/infer/src/pulse/PulseModels.mli index 22a32f556..8e9360fec 100644 --- a/infer/src/pulse/PulseModels.mli +++ b/infer/src/pulse/PulseModels.mli @@ -8,8 +8,8 @@ open! IStd type exec_fun = Location.t - -> ret:Var.t * Typ.t - -> actuals:HilExp.t list + -> ret:Ident.t * Typ.t + -> actuals:(PulseDomain.AddrTracePair.t * Typ.t) list -> PulseAbductiveDomain.t -> PulseAbductiveDomain.t list PulseOperations.access_result diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index e622f5800..afe6c464a 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -27,194 +27,179 @@ type t = PulseAbductiveDomain.t type 'a access_result = ('a, PulseDiagnostic.t) result -(** Check that the address is not known to be invalid *) -let check_addr_access access action (address, history) astate = +(** Check that the [address] is not known to be invalid *) +let check_addr_access action (address, history) astate = Memory.check_valid action address astate |> Result.map_error ~f:(fun invalidated_by -> - let access = PulseAbductiveDomain.explain_access_expr access astate in - PulseDiagnostic.AccessToInvalidAddress - {access; invalidated_by; accessed_by= {action; history}} ) - - -(** Walk the heap starting from [addr] and following [path]. Stop either at the element before last - and return [new_addr] if [overwrite_last] is [Some new_addr], or go until the end of the path if it - is [None]. Create more addresses into the heap as needed to follow the [path]. Check that each - address reached is valid. *) -let rec walk ~dereference_to_ignore access_expr action ~on_last addr_trace path astate = - let check_addr_access_optional action addr_trace astate = - match dereference_to_ignore with - | Some 0 -> - Ok astate + PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= {action; history}} ) + + +module Closures = struct + open Result.Monad_infix + module Memory = PulseAbductiveDomain.Memory + + let fake_capture_field_prefix = "__capture_" + + let mk_fake_field ~id = + Typ.Fieldname.Clang.from_class_name + (Typ.CStruct (QualifiedCppName.of_list ["std"; "function"])) + (Printf.sprintf "%s%d" fake_capture_field_prefix id) + + + let is_captured_fake_access (access : _ HilExp.Access.t) = + match access with + | FieldAccess fieldname + when String.is_prefix ~prefix:fake_capture_field_prefix (Typ.Fieldname.to_string fieldname) + -> + true | _ -> - check_addr_access access_expr action addr_trace astate - in - match (path, on_last) with - | [], `Access -> - Ok (astate, addr_trace) - | [], `Overwrite _ -> - L.die InternalError "Cannot overwrite last address in empty path" - | [a], `Overwrite new_addr_trace -> - check_addr_access_optional action addr_trace astate - >>| fun astate -> - let astate = Memory.add_edge (fst addr_trace) a new_addr_trace astate in - (astate, new_addr_trace) - | a :: path, _ -> - check_addr_access_optional action addr_trace astate - >>= fun astate -> - let dereference_to_ignore = - Option.map ~f:(fun index -> max 0 (index - 1)) dereference_to_ignore - in - let astate, addr_trace' = Memory.materialize_edge (fst addr_trace) a astate in - let access_expr = - HilExp.AccessExpression.add_access a access_expr |> Option.value ~default:access_expr - in - walk access_expr ~dereference_to_ignore action ~on_last addr_trace' path astate - - -let write_var var new_addr_trace astate = - let astate, (var_address_of, _) = Stack.materialize var astate in - (* Update heap with var_address_of -*-> new_addr *) - Memory.add_edge var_address_of HilExp.Access.Dereference new_addr_trace astate - - -let ends_with_addressof = function HilExp.AccessExpression.AddressOf _ -> true | _ -> false - -let last_dereference access_list = - let rec last_dereference_inner access_list index result = - match access_list with - | [] -> - result - | HilExp.Access.Dereference :: rest -> - last_dereference_inner rest (index + 1) (Some index) - | _ :: rest -> - last_dereference_inner rest (index + 1) result - in - last_dereference_inner access_list 0 None - - -let rec to_accesses location access_expr astate = - let exception Failed_fold of PulseDiagnostic.t in - try - HilExp.AccessExpression.to_accesses_fold access_expr ~init:astate - ~f_array_offset:(fun astate hil_exp_opt -> - match hil_exp_opt with - | None -> - (astate, AbstractAddress.mk_fresh ()) - | Some hil_exp -> ( - match eval_hil_exp location hil_exp astate with - | Ok result -> - result - | Error diag -> - raise (Failed_fold diag) ) ) - |> Result.return - with Failed_fold diag -> Error diag - - -(** add addresses to the state to give an address to the destination of the given access path *) -and walk_access_expr ~on_last astate access_expr location = - to_accesses location access_expr astate - >>= fun (astate, base, access_list) -> - let dereference_to_ignore = - if ends_with_addressof access_expr then last_dereference access_list else None + false + + + let mk_capture_edges captured = + let fake_fields = + List.rev_mapi captured ~f:(fun id captured_addr_trace -> + (HilExp.Access.FieldAccess (mk_fake_field ~id), captured_addr_trace) ) + in + Memory.Edges.of_seq (Caml.List.to_seq fake_fields) + + + let check_captured_addresses action lambda_addr astate = + match Memory.find_opt lambda_addr astate with + | None -> + Ok astate + | Some (edges, attributes) -> + IContainer.iter_result ~fold:Attributes.fold attributes ~f:(function + | Attribute.Closure _ -> + IContainer.iter_result + ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) edges + ~f:(fun (access, addr_trace) -> + if is_captured_fake_access access then + check_addr_access action addr_trace astate >>| fun _ -> () + else Ok () ) + | _ -> + Ok () ) + >>| fun () -> astate + + + let record location pname captured astate = + let captured_addresses = + List.rev_map captured ~f:(fun (captured_as, (address_captured, trace_captured)) -> + let new_trace = ValueHistory.Capture {captured_as; location} :: trace_captured in + (address_captured, new_trace) ) + in + let closure_addr = AbstractAddress.mk_fresh () in + let fake_capture_edges = mk_capture_edges captured_addresses in + let astate = + Memory.set_cell closure_addr + (fake_capture_edges, Attributes.singleton (Closure pname)) + astate + in + (astate, (closure_addr, (* TODO: trace *) [])) +end + +let eval_var var astate = Stack.eval var astate + +let eval_access location addr_trace access astate = + let addr = fst addr_trace in + let action = InterprocAction.Immediate {imm= (); location} in + check_addr_access action addr_trace astate >>| fun astate -> Memory.eval_edge addr access astate + + +let eval location exp0 astate = + let action = InterprocAction.Immediate {imm= (); location} in + let rec eval exp astate = + match (exp : Exp.t) with + | Var id -> + Ok (eval_var (Var.of_id id) astate) + | Lvar pvar -> + Ok (eval_var (Var.of_pvar pvar) astate) + | Lfield (exp', field, _) -> + eval exp' astate + >>= fun (astate, addr_trace) -> + check_addr_access action addr_trace astate + >>| fun astate -> Memory.eval_edge (fst addr_trace) (FieldAccess field) astate + | Lindex (exp', exp_index) -> + eval exp_index astate + >>= fun (astate, addr_trace_index) -> + check_addr_access action addr_trace_index astate + >>= fun astate -> + eval exp' astate + >>= fun (astate, addr_trace) -> + check_addr_access action addr_trace astate + >>| fun astate -> + Memory.eval_edge (fst addr_trace) (ArrayAccess (Typ.void, fst addr_trace_index)) astate + | Closure {name; captured_vars} -> + List.fold_result captured_vars ~init:(astate, []) + ~f:(fun (astate, rev_captured) (capt_exp, captured_as, _) -> + eval capt_exp astate + >>| fun (astate, addr_trace) -> (astate, (captured_as, addr_trace) :: rev_captured) ) + >>| fun (astate, rev_captured) -> + Closures.record location name (List.rev rev_captured) astate + | Cast (_, exp') -> + eval exp' astate + | Sizeof _ | UnOp _ | BinOp _ | Exn _ | Const _ -> + Ok (astate, (AbstractAddress.mk_fresh (), (* TODO history *) [])) in - let access_var, _ = base in - if Config.write_html then - L.d_printfln "Accessing %a -> [%a]" Var.pp access_var - (Pp.seq ~sep:"," Memory.Access.pp) - access_list ; - match (on_last, access_list) with - | `Overwrite new_addr_trace, [] -> - Ok (write_var access_var new_addr_trace astate, new_addr_trace) - | `Access, _ | `Overwrite _, _ :: _ -> ( - let astate, base_addr_trace = - let astate, (addr, init_loc_opt) = Stack.materialize access_var astate in - let trace = - Option.map init_loc_opt ~f:(fun init_loc -> - if Var.is_cpp_temporary access_var then ValueHistory.CppTemporaryCreated init_loc - else ValueHistory.VariableDeclaration init_loc ) - |> Option.to_list - in - (astate, (addr, trace)) - in - match access_list with - | [HilExp.Access.TakeAddress] -> - Ok (astate, base_addr_trace) - | _ -> - let action = - InterprocAction.Immediate - {imm= PulseAbductiveDomain.explain_access_expr access_expr astate; location} - in - walk - (HilExp.AccessExpression.base base) - ~dereference_to_ignore action ~on_last base_addr_trace - (HilExp.Access.Dereference :: access_list) - astate ) - - -(** Use the stack and heap to walk the access path represented by the given expression down to an - abstract address representing what the expression points to. - - Return an error state if it traverses some known invalid address or if the end destination is - known to be invalid. *) -and materialize_address astate access_expr = walk_access_expr ~on_last:`Access astate access_expr - -and read location access_expr astate = materialize_address astate access_expr location - -and read_all location access_exprs astate = - List.fold_result access_exprs ~init:astate ~f:(fun astate access_expr -> - read location access_expr astate >>| fst ) - - -and eval_hil_exp location (hil_exp : HilExp.t) astate = - match hil_exp with - | AccessExpression access_expr -> - read location access_expr astate >>| fun (astate, (addr, _)) -> (astate, addr) - | _ -> - read_all location (HilExp.get_access_exprs hil_exp) astate - >>| fun astate -> (astate, AbstractAddress.mk_fresh ()) - - -(** Use the stack and heap to walk the access path represented by the given expression down to an - abstract address representing what the expression points to, and replace that with the given - address. - - Return an error state if it traverses some known invalid address. *) -let overwrite_address astate access_expr new_addr_trace = - walk_access_expr ~on_last:(`Overwrite new_addr_trace) astate access_expr - - -(** Add the given address to the set of know invalid addresses. *) -let mark_invalid action address astate = Memory.invalidate address action astate + eval exp0 astate + + +let eval_deref location exp astate = + eval location exp astate + >>= fun (astate, addr_trace) -> + let action = InterprocAction.Immediate {imm= (); location} in + check_addr_access action addr_trace astate + >>| fun astate -> Memory.eval_edge (fst addr_trace) Dereference astate + let realloc_var var location astate = - Stack.add var (AbstractAddress.mk_fresh (), Some location) astate + Stack.add var (AbstractAddress.mk_fresh (), [ValueHistory.VariableDeclaration location]) astate -let havoc_var trace var astate = write_var var (AbstractAddress.mk_fresh (), trace) astate +let write_id id new_addr_loc astate = Stack.add (Var.of_id id) new_addr_loc astate -let havoc trace location (access_expr : HilExp.AccessExpression.t) astate = - overwrite_address astate access_expr (AbstractAddress.mk_fresh (), trace) location >>| fst +let havoc_id id loc_opt astate = + if Stack.mem (Var.of_id id) astate then write_id id (AbstractAddress.mk_fresh (), loc_opt) astate + else astate -let write location access_expr addr astate = - overwrite_address astate access_expr addr location >>| fun (astate, _) -> astate +let action_of_address location = InterprocAction.Immediate {imm= (); location} +let write_access location addr_trace_ref access addr_trace_obj astate = + let action = action_of_address location in + check_addr_access action addr_trace_ref astate + >>| Memory.add_edge (fst addr_trace_ref) access addr_trace_obj -let invalidate cause location access_expr astate = - materialize_address astate access_expr location - >>= fun (astate, addr_trace) -> - check_addr_access access_expr - (Immediate {imm= PulseAbductiveDomain.explain_access_expr access_expr astate; location}) - addr_trace astate - >>| mark_invalid cause addr_trace +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 invalidate_array_elements cause location access_expr astate = - materialize_address astate access_expr location - >>= fun (astate, addr_trace) -> - check_addr_access access_expr - (Immediate {imm= PulseAbductiveDomain.explain_access_expr access_expr astate; location}) - addr_trace astate + +let write_field location addr_trace_ref field addr_trace_obj astate = + write_access location addr_trace_ref (FieldAccess field) addr_trace_obj astate + + +let havoc_deref location addr_trace trace_obj astate = + write_deref location ~ref:addr_trace ~obj:(AbstractAddress.mk_fresh (), trace_obj) astate + + +let havoc_field location addr_trace field trace_obj astate = + write_field location addr_trace field (AbstractAddress.mk_fresh (), trace_obj) astate + + +let invalidate location cause addr_trace astate = + let action = action_of_address location in + check_addr_access action addr_trace astate >>| Memory.invalidate addr_trace cause + + +let invalidate_deref location cause (addr_ref, history) astate = + let astate, (addr_obj, _) = Memory.eval_edge addr_ref Dereference astate in + invalidate location cause (addr_obj, history) astate + + +let invalidate_array_elements location cause addr_trace astate = + let action = action_of_address location in + check_addr_access action addr_trace astate >>| fun astate -> match Memory.find_opt (fst addr_trace) astate with | None -> @@ -224,7 +209,7 @@ let invalidate_array_elements cause location access_expr astate = (fun access dest_addr_trace astate -> match (access : Memory.Access.t) with | ArrayAccess _ -> - mark_invalid cause dest_addr_trace astate + Memory.invalidate dest_addr_trace cause astate | _ -> astate ) edges astate @@ -263,9 +248,9 @@ let check_address_escape escape_location proc_desc address history astate = check_address_of_cpp_temporary () >>= check_address_of_stack_variable >>| fun () -> astate -let mark_address_of_cpp_temporary location variable address astate = +let mark_address_of_cpp_temporary history variable address astate = Memory.add_attributes address - (Attributes.singleton (AddressOfCppTemporary (variable, location))) + (Attributes.singleton (AddressOfCppTemporary (variable, history))) astate @@ -273,136 +258,10 @@ let remove_vars vars astate = let astate = List.fold vars ~init:astate ~f:(fun heap var -> match Stack.find_opt var astate with - | Some (address, location) when Var.is_cpp_temporary var -> - mark_address_of_cpp_temporary location var address astate + | Some (address, history) when Var.is_cpp_temporary var -> + mark_address_of_cpp_temporary history var address astate | _ -> heap ) in let astate' = Stack.remove_vars vars astate in if phys_equal astate' astate then astate else PulseAbductiveDomain.discard_unreachable astate' - - -module Closures = struct - open Result.Monad_infix - module Memory = PulseAbductiveDomain.Memory - - let fake_capture_field_prefix = "__capture_" - - let mk_fake_field ~id = - Typ.Fieldname.Clang.from_class_name - (Typ.CStruct (QualifiedCppName.of_list ["std"; "function"])) - (Printf.sprintf "%s%d" fake_capture_field_prefix id) - - - let is_captured_fake_access (access : _ HilExp.Access.t) = - match access with - | FieldAccess fieldname - when String.is_prefix ~prefix:fake_capture_field_prefix (Typ.Fieldname.to_string fieldname) - -> - true - | _ -> - false - - - let mk_capture_edges captured = - let fake_fields = - List.rev_mapi captured ~f:(fun id captured_addr_trace -> - (HilExp.Access.FieldAccess (mk_fake_field ~id), captured_addr_trace) ) - in - Memory.Edges.of_seq (Caml.List.to_seq fake_fields) - - - let check_captured_addresses location lambda addr astate = - match Memory.find_opt addr astate with - | None -> - Ok astate - | Some (edges, attributes) -> - IContainer.iter_result ~fold:Attributes.fold attributes ~f:(function - | Attribute.Closure _ -> - IContainer.iter_result - ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) edges - ~f:(fun (access, addr_trace) -> - if is_captured_fake_access access then - check_addr_access lambda - (Immediate - {imm= PulseAbductiveDomain.explain_access_expr lambda astate; location}) - addr_trace astate - >>| fun _ -> () - else Ok () ) - | _ -> - Ok () ) - >>| fun () -> astate - - - let write location access_expr pname captured astate = - let closure_addr = AbstractAddress.mk_fresh () in - write location access_expr - ( closure_addr - , [ ValueHistory.Assignment - {lhs= PulseAbductiveDomain.explain_access_expr access_expr astate; location} ] ) - astate - >>| fun astate -> - let fake_capture_edges = mk_capture_edges captured in - Memory.set_cell closure_addr (fake_capture_edges, Attributes.singleton (Closure pname)) astate - - - let record location access_expr pname captured astate = - List.fold_result captured ~init:(astate, []) - ~f:(fun ((astate, captured) as result) (captured_as, captured_exp) -> - match captured_exp with - | HilExp.AccessExpression (AddressOf access_expr as captured_access_expr) -> - read location access_expr astate - >>= fun (astate, (address, trace)) -> - let new_trace = - ValueHistory.Capture - { captured_as - ; captured= PulseAbductiveDomain.explain_access_expr captured_access_expr astate - ; location } - :: trace - in - Ok (astate, (address, new_trace) :: captured) - | _ -> - Ok result ) - >>= fun (astate, captured_addresses) -> - write location access_expr pname captured_addresses astate -end - -module StdVector = struct - open Result.Monad_infix - module Memory = PulseAbductiveDomain.Memory - - let is_reserved location vector_access_expr astate = - read location vector_access_expr astate - >>| fun (astate, (addr, _)) -> (astate, Memory.is_std_vector_reserved addr astate) - - - let mark_reserved location vector_access_expr astate = - read location vector_access_expr astate - >>| fun (astate, (addr, _)) -> Memory.std_vector_reserve addr astate -end - -module Interproc = struct - open Result.Monad_infix - - (* compute addresses for actuals and then call {!PulseAbductiveDomain.PrePost.apply} on each - pre/post pair in the summary. *) - let call callee_pname ~formals ~ret ~actuals _flags call_loc astate pre_posts = - L.d_printfln "PulseOperations.call" ; - List.fold_result actuals ~init:(astate, []) ~f:(fun (astate, rev_actual_addresses) actual -> - match actual with - | HilExp.AccessExpression access_expr -> - read call_loc access_expr astate - >>| fun (astate, (addr, trace)) -> - (astate, Some (addr, access_expr, trace) :: rev_actual_addresses) - | _ -> - Ok (astate, None :: rev_actual_addresses) ) - >>= fun (astate, rev_actual_addresses) -> - let actuals = List.rev rev_actual_addresses in - read call_loc HilExp.AccessExpression.(address_of_base ret) astate - >>= fun (astate, ret) -> - List.fold_result pre_posts ~init:[] ~f:(fun posts pre_post -> - (* apply all pre/post specs *) - PulseAbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~ret ~actuals - astate - >>| fun post -> post :: posts ) -end diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 8084416ab..a69fdfb1a 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -14,66 +14,77 @@ type 'a access_result = ('a, PulseDiagnostic.t) result module Closures : sig val check_captured_addresses : - Location.t - -> HilExp.AccessExpression.t - -> PulseDomain.AbstractAddress.t - -> t - -> t access_result + unit PulseDomain.InterprocAction.t -> AbstractAddress.t -> t -> (t, PulseDiagnostic.t) result (** assert the validity of the addresses captured by the lambda *) - - val record : - Location.t - -> HilExp.AccessExpression.t - -> Typ.Procname.t - -> (AccessPath.base * HilExp.t) list - -> t - -> t access_result - (** record that the access expression points to a lambda with its captured addresses *) end -module StdVector : sig - val is_reserved : Location.t -> HilExp.AccessExpression.t -> t -> (t * bool) access_result +val eval : Location.t -> Exp.t -> t -> (t * PulseDomain.AddrTracePair.t) access_result +(** Use the stack and heap to evaluate the given expression down to an abstract address representing + its value. - val mark_reserved : Location.t -> HilExp.AccessExpression.t -> t -> t access_result -end + Return an error state if it traverses some known invalid address or if the end destination is + known to be invalid. *) -val read : +val eval_deref : Location.t -> Exp.t -> t -> (t * PulseDomain.AddrTracePair.t) access_result +(** Like [eval] but evaluates [*exp]. *) + +val eval_access : Location.t - -> HilExp.AccessExpression.t + -> PulseDomain.AddrTracePair.t + -> PulseDomain.Memory.Access.t -> t - -> (t * (AbstractAddress.t * PulseDomain.ValueHistory.t)) access_result + -> (t * PulseDomain.AddrTracePair.t) access_result +(** Like [eval] but starts from an address instead of an expression, checks that it is valid, and if + so dereferences it according to the access. *) -val read_all : Location.t -> HilExp.AccessExpression.t list -> t -> t access_result +val havoc_id : Ident.t -> PulseDomain.ValueHistory.t -> t -> t -val havoc_var : PulseDomain.ValueHistory.t -> Var.t -> t -> t +val havoc_deref : + Location.t -> PulseDomain.AddrTracePair.t -> PulseDomain.ValueHistory.t -> t -> t access_result -val havoc : - PulseDomain.ValueHistory.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result +val havoc_field : + Location.t + -> PulseDomain.AddrTracePair.t + -> Typ.Fieldname.t + -> PulseDomain.ValueHistory.t + -> t + -> t access_result val realloc_var : Var.t -> Location.t -> t -> t -val write_var : Var.t -> AbstractAddress.t * PulseDomain.ValueHistory.t -> t -> t +val write_id : Ident.t -> PulseDomain.Stack.value -> t -> t -val write : +val write_deref : Location.t - -> HilExp.AccessExpression.t - -> AbstractAddress.t * PulseDomain.ValueHistory.t + -> ref:PulseDomain.AddrTracePair.t + -> obj:PulseDomain.AddrTracePair.t -> t -> t access_result +(** write the edge [ref --*--> obj] *) val invalidate : - PulseDomain.Invalidation.t PulseDomain.InterprocAction.t - -> Location.t - -> HilExp.AccessExpression.t + Location.t + -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t + -> PulseDomain.AddrTracePair.t -> t -> t access_result +(** record that the address is invalid *) + +val invalidate_deref : + Location.t + -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t + -> PulseDomain.AddrTracePair.t + -> t + -> t access_result +(** record that what the address points to is invalid *) val invalidate_array_elements : - PulseDomain.Invalidation.t PulseDomain.InterprocAction.t - -> Location.t - -> HilExp.AccessExpression.t + Location.t + -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t + -> PulseDomain.AddrTracePair.t -> t -> t access_result +(** record that all the array elements that address points to is invalid *) val remove_vars : Var.t list -> t -> t @@ -84,16 +95,3 @@ val check_address_escape : -> PulseDomain.ValueHistory.t -> t -> t access_result - -module Interproc : sig - val call : - Typ.Procname.t - -> formals:Var.t list - -> ret:AccessPath.base - -> actuals:HilExp.t list - -> CallFlags.t - -> Location.t - -> t - -> PulseSummary.t - -> PulseAbductiveDomain.t list access_result -end diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index e13e3aa7b..6f20c31f2 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,50 +1,51 @@ -codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` on `ptr` here,use-after-lifetime part of the trace starts here,invalid access to `*ptr` here] -codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` on `ptr` here,use-after-lifetime part of the trace starts here,invalid access to `ptr` here] -codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access to `*(a.f)` here] -codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access to `*(a.f)` here] -codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<_Bool>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(deduplication::A))`,assigned to `a`,when calling `deduplication::templated_access_function` here,invalid access to `*(a.f)` here] -codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` on `a` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(deduplication::A))`,assigned to `a`,when calling `deduplication::templated_access_function` here,invalid access to `*(a.f)` here] -codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::double_delete_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` on `this` here,use-after-lifetime part of the trace starts here,invalid access to `this` here] -codetoanalyze/cpp/pulse/interprocedural.cpp, delete_aliased_then_read_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `y`,memory was invalidated by `delete` on `y` here,use-after-lifetime part of the trace starts here,assigned to `z`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `*(x.f)` here] -codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` on `x` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `*(x.f)` here] -codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` on `x` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `*(x.f)` here] -codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete()` here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` on `x` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `*(x.f)` here] -codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Y))`,assigned to `y`,when calling `may_return_invalid_ptr_ok()` here,memory was invalidated by `delete` on `y` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Y))`,assigned to `y`,assigned to `return`,returned from call to `may_return_invalid_ptr_ok()`,assigned to `y`,when calling `call_store()` here,when calling `store()` here,invalid access to `*(y.p)` here] -codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `result`,memory was invalidated by `delete` on `result` here,use-after-lifetime part of the trace starts here,assigned to `result`,invalid access to `*result` here] -codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperHeap()` here,when calling `~WrapsB` here,when calling `__infer_inner_destructor_~WrapsB` here,memory was invalidated by `delete` on `*(*(&this.b))` here,use-after-lifetime part of the trace starts here,assigned to `*(this.b)`,returned from call to `ReferenceWrapperHeap::ReferenceWrapperHeap()`,invalid access to `*(&rw.b->f)` here] -codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperStack()` here,memory is the address of a stack variable `b` whose lifetime has ended here,use-after-lifetime part of the trace starts here,returned from call to `getwrapperStack()`,invalid access to `*(&rw.b->f)` here] -codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,returned here] +codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here here] +codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here here] +codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass::lifetime_error_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `templated_wrapper_access_ok` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<_Bool>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::double_delete_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here here] +codetoanalyze/cpp/pulse/interprocedural.cpp, delete_aliased_then_read_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete()` here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `may_return_invalid_ptr_ok()` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `_fun_may_return_invalid_ptr_ok()`,assigned,when calling `call_store()` here,when calling `store()` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperHeap()` here,when calling `~WrapsB` here,when calling `__infer_inner_destructor_~WrapsB` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `_fun_ReferenceWrapperHeap::ReferenceWrapperHeap()`,invalid access occurs here here] +codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_stack_bad, 2, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,when calling `getwrapperStack()` here,memory is the address of a stack variable `b` whose lifetime has ended here,use-after-lifetime part of the trace starts here,assigned,returned from call to `_fun_ReferenceWrapperStack::ReferenceWrapperStack()`,invalid access occurs here here] +codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,returned here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,returned here] -codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,assigned to `x`,returned here] -codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 3, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [C++ temporary created,assigned to `x`,assigned to `y`,returned here] -codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~UniquePtr` here,when calling `__infer_inner_destructor_~UniquePtr` here,memory was invalidated by `delete` on `*(*(&this.x_))` here,use-after-lifetime part of the trace starts here,assigned to `return`,returned from call to `temporaries::UniquePtr::get()`,assigned to `a`,invalid access to `*(a.s_)` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalid access to `*(s.f)` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalid access to `s` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,when calling `Simple` here,invalid access to `*(__param_0.f)` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalid access to `s` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalid access to `*(s.f)` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,when calling `Simple` here,invalid access to `*(__param_0.f)` here] -codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalid access to `*(s.f)` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `*(*(&this.f))` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,returned from call to `(sizeof(use_after_destructor::S),s)`,assigned to `alias`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,invalid access to `*(s.f)` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,memory was invalidated by `delete` on `alias` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,returned from call to `(sizeof(use_after_destructor::S),s)`,assigned to `alias`,invalid access to `*(alias.f)` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,memory was invalidated by `delete` on `s` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `alias`,invalid access to `*(alias.f)` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `*(*(&this.f))` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,assigned to `*(this.f)`,returned from call to `use_after_destructor::S::operator=()`,invalid access to `*(*(&s.f))` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(int))`,assigned to `*(this.f)`,returned from call to `use_after_destructor::S::S()`,invalid access to `*(*(&s.f))` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope1_bad, 7, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `*(*(&this.f))` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `*(*(&this.f))` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access to `*(*(&this.f))` here] -codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,memory is the address of a stack variable `c` whose lifetime has ended here,use-after-lifetime part of the trace starts here,invalid access to `*(pc.f)` here] -codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_global_pointer_ok()` here,memory was invalidated by call to `free()` on `global_pointer` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_ok()` here,invalid access to `global_pointer` here] -codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` on `x` here,use-after-lifetime part of the trace starts here,invalid access to `x` here] -codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` on `x` here,use-after-lifetime part of the trace starts here,invalid access to `*x` here] -codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::assign()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] -codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::clear()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] -codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` on `&vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(&vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] -codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,assigned to `y`,invalid access to `*y` here] -codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::emplace_back()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] -codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::emplace()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] -codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::insert()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] -codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` on `&vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(&vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] -codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::reserve()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] -codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::shrink_to_fit()` on `vec` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalid access to `*elt` here] +codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,assigned,returned here] +codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 3, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable declared,assigned,assigned,returned here] +codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~UniquePtr` here,when calling `__infer_inner_destructor_~UniquePtr` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `_fun_temporaries::UniquePtr::get()`,assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `Simple` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `Simple` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,returned from call to `()` (pulse model),assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `()` (pulse model),assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `_fun_use_after_destructor::S::operator=()`,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,returned from call to `_fun_use_after_destructor::S::S()`,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope1_bad, 7, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable declared,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable declared,memory is the address of a stack variable `c` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable declared,assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_global_pointer_ok()` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_ok()` here,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here here] +codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here here] +codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::assign()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::clear()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::emplace_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::emplace()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::insert()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::push_back()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::reserve()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here] +codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,memory was potentially invalidated by `std::vector::shrink_to_fit()` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at()` (pulse model),assigned,invalid access occurs here here]