From 7f12ced394dadc01deb0446e505cccce20490162 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 26 Jun 2019 02:55:15 -0700 Subject: [PATCH] [pulse] move to SIL proper Summary: [apologies for the unreviewable diff...] Get rid of HIL expressions in pulse. This finishes the HIL -> SIL migration. The first step made pulse start from SIL instructions but would translate most accesses to HIL to re-use most of the existing pulse code. This diff gets rid of the intermediate translation of SIL expressions to HIL expressions. Big changes: 1. `PulseOperations` mostly rewritten, driven by using `Exp.t` instead of `HilExp.AccessExpression.t` for everything. 2. Stop trying to reverse-engineer what addresses mean in terms of access paths from program variables. Rely on the trace pointing at the right places in the code to be enough. This is because it wasn't that useful (and could even be misleading when wrong) but could be prohibitively expensive in degenerate cases (eg nodes with tens of thousands of successive array accesses...) 3. `PulseAbductiveDomain.apply_post` now returns the computed return value instead of recording it itself. 4. Change of vocabulary: `materialize` -> `eval`, `crumb` -> `event` 5. Function calls arguments are now evaluated prior to doing anything else, which saves everything else from having to (remember to) do that. In particular, this changes how models look quite a bit. Reviewed By: mbouaziz Differential Revision: D15986373 fbshipit-source-id: 1d79935de --- infer/src/IR/HilExp.ml | 54 -- infer/src/IR/HilExp.mli | 24 +- infer/src/IR/HilInstr.mli | 2 +- infer/src/IR/Sil.ml | 2 +- infer/src/pulse/Pulse.ml | 252 ++++------ infer/src/pulse/PulseAbductiveDomain.ml | 194 ++++---- infer/src/pulse/PulseAbductiveDomain.mli | 23 +- infer/src/pulse/PulseDiagnostic.ml | 61 +-- infer/src/pulse/PulseDiagnostic.mli | 5 +- infer/src/pulse/PulseDomain.ml | 173 ++----- infer/src/pulse/PulseDomain.mli | 41 +- infer/src/pulse/PulseModels.ml | 153 ++---- infer/src/pulse/PulseModels.mli | 4 +- infer/src/pulse/PulseOperations.ml | 467 ++++++------------ infer/src/pulse/PulseOperations.mli | 94 ++-- .../tests/codetoanalyze/cpp/pulse/issues.exp | 99 ++-- 16 files changed, 592 insertions(+), 1056 deletions(-) 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]