From 0592bac25e74af9c4dbd5ed6fe4c7029e1481d8c Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 19 Jun 2019 05:05:22 -0700 Subject: [PATCH] [pulse] explain SIL logical variables in terms of program access paths Summary: Now that HIL doesn't help us anymore we need to reconstruct its mapping "SIL logical var -> program access path". We already have everything we need in pulse: it suffices to walk the current memory graph starting from program variables until we find the value of the temporary we are interested in. This diff also builds some type machinery to make sure all accesses are explained. Reviewed By: mbouaziz Differential Revision: D15824959 fbshipit-source-id: 722c81b39 --- infer/src/IR/HilExp.ml | 23 ++++- infer/src/IR/HilExp.mli | 8 ++ infer/src/pulse/Pulse.ml | 12 ++- infer/src/pulse/PulseAbductiveDomain.ml | 13 ++- infer/src/pulse/PulseAbductiveDomain.mli | 7 +- infer/src/pulse/PulseDiagnostic.ml | 18 ++-- infer/src/pulse/PulseDiagnostic.mli | 4 +- infer/src/pulse/PulseDomain.ml | 93 +++++++++++++++++-- infer/src/pulse/PulseDomain.mli | 22 +++-- infer/src/pulse/PulseModels.ml | 46 +++++++-- infer/src/pulse/PulseOperations.ml | 29 ++++-- .../tests/codetoanalyze/cpp/pulse/issues.exp | 90 +++++++++--------- 12 files changed, 274 insertions(+), 91 deletions(-) diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml index 0e7db7e62..bdd0f504c 100644 --- a/infer/src/IR/HilExp.ml +++ b/infer/src/IR/HilExp.ml @@ -237,6 +237,13 @@ module AccessExpression = struct 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 -> @@ -249,6 +256,14 @@ module AccessExpression = struct 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 = @@ -353,10 +368,14 @@ module AccessExpression = struct fold_vars_exp_opt exp_opt ~init ~f - let to_source_string access_expr = + 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 - if Var.appears_in_source_code var then Some (F.asprintf "%a" pp access_expr) else None + 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 1bec37c9e..3628c185e 100644 --- a/infer/src/IR/HilExp.mli +++ b/infer/src/IR/HilExp.mli @@ -64,6 +64,8 @@ module AccessExpression : sig -> 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 to_access_path : access_expression -> AccessPath.t val to_access_paths : access_expression list -> AccessPath.t list @@ -93,6 +95,12 @@ module AccessExpression : sig 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 *) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index e6df1c7aa..f03c28ec8 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -54,7 +54,10 @@ module PulseTransferFunctions = struct 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= lhs_access; location= loc} in + 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 @@ -82,7 +85,12 @@ module PulseTransferFunctions = struct 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; location= call_loc} 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 diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index aa4f03599..0f744698e 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -85,6 +85,12 @@ 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 *) @@ -375,7 +381,9 @@ module PrePost = struct | Error invalidated_by -> Error (PulseDiagnostic.AccessToInvalidAddress - {access= access_expr; invalidated_by; accessed_by= {action; history}}) + { access= explain_access_expr access_expr call_state.astate + ; invalidated_by + ; accessed_by= {action; history} }) | Ok astate -> let call_state = {call_state with astate} in Container.fold_result @@ -730,3 +738,6 @@ module PrePost = struct | 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 b19dc7e7d..8ea31aee3 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -43,7 +43,7 @@ module Memory : sig val add_edge : AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t val check_valid : - HilExp.AccessExpression.t PulseDomain.InterprocAction.t + HilExp.AccessExpression.t PulseDomain.explained PulseDomain.InterprocAction.t -> AbstractAddress.t -> t -> (t, PulseDomain.Invalidation.t PulseDomain.Trace.t) result @@ -89,3 +89,8 @@ 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 15b11d670..9626533cc 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -10,9 +10,9 @@ module F = Format type t = | AccessToInvalidAddress of - { access: HilExp.AccessExpression.t + { access: HilExp.AccessExpression.t PulseDomain.explained ; invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t - ; accessed_by: HilExp.AccessExpression.t PulseDomain.Trace.t } + ; accessed_by: HilExp.AccessExpression.t PulseDomain.explained PulseDomain.Trace.t } | StackVariableAddressEscape of { variable: Var.t ; history: PulseDomain.ValueHistory.t @@ -44,11 +44,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.Trace.t) = + let pp_access_trace invalidated f + (trace : HilExp.AccessExpression.t PulseDomain.explained PulseDomain.Trace.t) = match trace.action with | Immediate {imm= access; _} -> ( - match HilExp.AccessExpression.to_source_string access with - | Some access_s when HilExp.AccessExpression.equal access invalidated -> + 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 @@ -101,7 +103,9 @@ let get_message = function line in let invalidation_line = line_of_trace invalidated_by in - F.asprintf "%a%a" (pp_access_trace access) accessed_by + F.asprintf "%a%a" + (pp_access_trace (access :> HilExp.AccessExpression.t)) + accessed_by (pp_invalidation_trace invalidation_line) invalidated_by | StackVariableAddressEscape {variable; _} -> @@ -119,7 +123,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) -> + (fun f (access : HilExp.AccessExpression.t PulseDomain.explained) -> F.fprintf f "invalid access to `%a`" HilExp.AccessExpression.pp (access :> HilExp.AccessExpression.t) ) accessed_by diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index dc9343a4d..9992478e8 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -10,9 +10,9 @@ open! IStd (** an error to report to the user *) type t = | AccessToInvalidAddress of - { access: HilExp.AccessExpression.t + { access: HilExp.AccessExpression.t PulseDomain.explained ; invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t - ; accessed_by: HilExp.AccessExpression.t PulseDomain.Trace.t } + ; accessed_by: HilExp.AccessExpression.t PulseDomain.explained 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 c28d8e44c..3c0ffc991 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -10,6 +10,8 @@ module L = Logging (* {2 Abstract domain description } *) +type 'a explained = 'a [@@deriving compare] + module Invalidation = struct type std_vector_function = | Assign @@ -42,11 +44,11 @@ module Invalidation = struct type t = - | CFree of HilExp.AccessExpression.t - | CppDelete of HilExp.AccessExpression.t + | CFree of HilExp.AccessExpression.t explained + | CppDelete of HilExp.AccessExpression.t explained | GoneOutOfScope of Pvar.t * Typ.t | Nullptr - | StdVector of std_vector_function * HilExp.AccessExpression.t + | StdVector of std_vector_function * HilExp.AccessExpression.t explained [@@deriving compare] let issue_type_of_cause = function @@ -100,14 +102,14 @@ module ValueHistory = struct type event = | VariableDeclaration of Location.t | CppTemporaryCreated of Location.t - | Assignment of {lhs: HilExp.AccessExpression.t; location: Location.t} + | Assignment of {lhs: HilExp.AccessExpression.t explained; location: Location.t} | Capture of { captured_as: AccessPath.base - ; captured: HilExp.AccessExpression.t + ; captured: HilExp.AccessExpression.t explained ; location: Location.t } | Call of { f: [`HilCall of HilInstr.call | `Model of string] - ; actuals: HilExp.t list + ; actuals: HilExp.t explained list ; location: Location.t } [@@deriving compare] @@ -120,7 +122,8 @@ module ValueHistory = struct F.fprintf fmt "`%a` captured as `%a`" HilExp.AccessExpression.pp captured AccessPath.pp_base captured_as | Assignment {lhs; location= _} -> - F.fprintf fmt "assigned to `%a`" HilExp.AccessExpression.pp lhs + if HilExp.AccessExpression.appears_in_source_code lhs then + F.fprintf fmt "assigned to `%a`" HilExp.AccessExpression.pp lhs | Call {f; actuals; location= _} -> let pp_f fmt = function | `HilCall call -> @@ -236,7 +239,7 @@ end module Attribute = struct type t = | Invalid of Invalidation.t Trace.t - | MustBeValid of HilExp.AccessExpression.t InterprocAction.t + | MustBeValid of HilExp.AccessExpression.t explained InterprocAction.t | AddressOfCppTemporary of Var.t * Location.t option | Closure of Typ.Procname.t | StdVectorReserve @@ -784,3 +787,77 @@ 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 89bacd5a2..a1f14b4bb 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -8,6 +8,8 @@ open! IStd module F = Format +type 'a explained = private 'a + module Invalidation : sig type std_vector_function = | Assign @@ -23,11 +25,11 @@ module Invalidation : sig val pp_std_vector_function : Format.formatter -> std_vector_function -> unit type t = - | CFree of HilExp.AccessExpression.t - | CppDelete of HilExp.AccessExpression.t + | CFree of HilExp.AccessExpression.t explained + | CppDelete of HilExp.AccessExpression.t explained | GoneOutOfScope of Pvar.t * Typ.t | Nullptr - | StdVector of std_vector_function * HilExp.AccessExpression.t + | StdVector of std_vector_function * HilExp.AccessExpression.t explained [@@deriving compare] val issue_type_of_cause : t -> IssueType.t @@ -39,14 +41,14 @@ module ValueHistory : sig type event = | VariableDeclaration of Location.t | CppTemporaryCreated of Location.t - | Assignment of {lhs: HilExp.access_expression; location: Location.t} + | Assignment of {lhs: HilExp.AccessExpression.t explained; location: Location.t} | Capture of { captured_as: AccessPath.base - ; captured: HilExp.access_expression + ; captured: HilExp.AccessExpression.t explained ; location: Location.t } | Call of { f: [`HilCall of HilInstr.call | `Model of string] - ; actuals: HilExp.t list + ; actuals: HilExp.t explained list ; location: Location.t } type t = event list [@@deriving compare] @@ -80,7 +82,7 @@ end module Attribute : sig type t = | Invalid of Invalidation.t Trace.t - | MustBeValid of HilExp.AccessExpression.t InterprocAction.t + | MustBeValid of HilExp.AccessExpression.t explained InterprocAction.t | AddressOfCppTemporary of Var.t * Location.t option | Closure of Typ.Procname.t | StdVectorReserve @@ -90,7 +92,7 @@ end module Attributes : sig include PrettyPrintable.PPUniqRankSet with type elt = Attribute.t - val get_must_be_valid : t -> HilExp.AccessExpression.t InterprocAction.t option + val get_must_be_valid : t -> HilExp.AccessExpression.t explained InterprocAction.t option end module AbstractAddress : sig @@ -192,3 +194,7 @@ 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 30ce94ea2..55ba35b46 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -27,7 +27,10 @@ module C = struct | [AccessExpression deleted_access] -> PulseOperations.invalidate (PulseDomain.InterprocAction.Immediate - {imm= PulseDomain.Invalidation.CFree deleted_access; location}) + { imm= + PulseDomain.Invalidation.CFree + (PulseAbductiveDomain.explain_access_expr deleted_access astate) + ; location }) location deleted_access astate >>| List.return | _ -> @@ -43,7 +46,10 @@ module Cplusplus = struct | [AccessExpression deleted_access] -> PulseOperations.invalidate (PulseDomain.InterprocAction.Immediate - {imm= PulseDomain.Invalidation.CppDelete deleted_access; location}) + { imm= + PulseDomain.Invalidation.CppDelete + (PulseAbductiveDomain.explain_access_expr deleted_access astate) + ; location }) location deleted_access astate >>| List.return | _ -> @@ -63,7 +69,10 @@ module Cplusplus = struct Ok astate ) >>| fun astate -> [ PulseOperations.havoc_var - [PulseDomain.ValueHistory.Call {f= `Model ""; actuals; location}] + [ PulseDomain.ValueHistory.Call + { f= `Model "" + ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate) + ; location } ] ret_var astate ] @@ -72,7 +81,12 @@ module Cplusplus = struct 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; location} in + let crumb = + PulseDomain.ValueHistory.Call + { f= `Model "" + ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate) + ; location } + in match List.rev actuals with | HilExp.AccessExpression expr :: other_actuals -> PulseOperations.read location expr astate @@ -107,7 +121,10 @@ module StdVector = struct let array = deref_internal_array vector in let invalidation = PulseDomain.InterprocAction.Immediate - {imm= PulseDomain.Invalidation.StdVector (vector_f, vector); location} + { imm= + PulseDomain.Invalidation.StdVector + (vector_f, PulseAbductiveDomain.explain_access_expr vector astate) + ; location } in PulseOperations.invalidate_array_elements invalidation location array astate >>= PulseOperations.invalidate invalidation location array @@ -123,7 +140,7 @@ module StdVector = struct { f= `Model (Format.asprintf "%a" PulseDomain.Invalidation.pp_std_vector_function vector_f) - ; actuals + ; 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 @@ -133,7 +150,12 @@ module StdVector = struct let at : model = fun location ~ret ~actuals astate -> - let crumb = PulseDomain.ValueHistory.Call {f= `Model "std::vector::at"; actuals; location} in + 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 match actuals with | [AccessExpression vector_access_expr; index_exp] -> PulseOperations.read location @@ -154,7 +176,10 @@ module StdVector = struct match actuals with | [AccessExpression vector; _value] -> let crumb = - PulseDomain.ValueHistory.Call {f= `Model "std::vector::reserve"; actuals; location} + PulseDomain.ValueHistory.Call + { f= `Model "std::vector::reserve" + ; actuals= List.map actuals ~f:(fun e -> PulseAbductiveDomain.explain_hil_exp e astate) + ; location } in reallocate_internal_array [crumb] vector Reserve location astate >>= PulseOperations.StdVector.mark_reserved location vector @@ -168,7 +193,10 @@ module StdVector = struct match actuals with | [AccessExpression vector; _value] -> let crumb = - PulseDomain.ValueHistory.Call {f= `Model "std::vector::push_back"; actuals; location} + 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) -> diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index e9e668091..e622f5800 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -31,6 +31,7 @@ type 'a access_result = ('a, PulseDiagnostic.t) result let check_addr_access 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}} ) @@ -139,7 +140,10 @@ and walk_access_expr ~on_last astate access_expr location = | [HilExp.Access.TakeAddress] -> Ok (astate, base_addr_trace) | _ -> - let action = InterprocAction.Immediate {imm= access_expr; location} in + 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 @@ -199,14 +203,18 @@ let write location access_expr addr astate = let invalidate cause location access_expr astate = materialize_address astate access_expr location >>= fun (astate, addr_trace) -> - check_addr_access access_expr (Immediate {imm= access_expr; location}) addr_trace astate + check_addr_access access_expr + (Immediate {imm= PulseAbductiveDomain.explain_access_expr access_expr astate; location}) + addr_trace astate >>| mark_invalid cause addr_trace 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= access_expr; location}) addr_trace astate + check_addr_access access_expr + (Immediate {imm= PulseAbductiveDomain.explain_access_expr access_expr astate; location}) + addr_trace astate >>| fun astate -> match Memory.find_opt (fst addr_trace) astate with | None -> @@ -315,7 +323,10 @@ module Closures = struct ~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= lambda; location}) addr_trace astate + check_addr_access lambda + (Immediate + {imm= PulseAbductiveDomain.explain_access_expr lambda astate; location}) + addr_trace astate >>| fun _ -> () else Ok () ) | _ -> @@ -326,7 +337,9 @@ module Closures = struct let write location access_expr pname captured astate = let closure_addr = AbstractAddress.mk_fresh () in write location access_expr - (closure_addr, [ValueHistory.Assignment {lhs= access_expr; location}]) + ( 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 @@ -341,7 +354,11 @@ module Closures = struct read location access_expr astate >>= fun (astate, (address, trace)) -> let new_trace = - ValueHistory.Capture {captured_as; captured= captured_access_expr; location} :: trace + ValueHistory.Capture + { captured_as + ; captured= PulseAbductiveDomain.explain_access_expr captured_access_expr astate + ; location } + :: trace in Ok (astate, (address, new_trace) :: captured) | _ -> diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index bc91ee602..0a21e46ce 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,47 +1,47 @@ -codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$5`,memory was invalidated by `delete` on `n$5` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,invalid access to `*n$0` here] -codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned to `n$6`,memory was invalidated by `delete` on `n$6` here,use-after-lifetime part of the trace starts here,assigned to `n$6`,invalid access to `n$6` 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,assigned to `n$0`,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,assigned to `n$2`,when calling `templated_wrapper_access_ok` here,invalid access to `n$0->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,assigned to `n$0`,when calling `templated_wrapper_delete_ok` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,assigned to `n$2`,when calling `templated_wrapper_access_ok` here,invalid access to `n$0->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,assigned to `n$0`,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(deduplication::A))`,assigned to `a`,assigned to `n$1`,when calling `deduplication::templated_access_function` here,invalid access to `n$0->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,assigned to `n$0`,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(deduplication::A))`,assigned to `a`,assigned to `n$1`,when calling `deduplication::templated_access_function` here,invalid access to `n$0->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,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,invalid access to `n$0` 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 `n$5`,assigned to `y`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,assigned to `n$4`,assigned to `z`,assigned to `n$0`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `n$0->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,assigned to `n$0`,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `n$0->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,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `n$0->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,assigned to `n$0`,when calling `wraps_delete()` here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` on `n$0` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access to `n$0->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`,assigned to `n$2`,when calling `may_return_invalid_ptr_ok()` here,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Y))`,assigned to `y`,assigned to `n$0`,assigned to `return`,returned from call to `may_return_invalid_ptr_ok()`,assigned to `y`,assigned to `n$0`,when calling `call_store()` here,when calling `store()` here,invalid access to `n$0->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 `n$13`,assigned to `result`,assigned to `n$9`,memory was invalidated by `delete` on `n$9` here,use-after-lifetime part of the trace starts here,assigned to `n$13`,assigned to `result`,assigned to `n$0`,invalid access to `*n$0` 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,assigned to `n$3`,when calling `getwrapperHeap()` here,when calling `~WrapsB` here,when calling `__infer_inner_destructor_~WrapsB` here,memory was invalidated by `delete` on `n$3` here,use-after-lifetime part of the trace starts here,assigned to `n$3`,assigned to `n$1->b`,returned from call to `ReferenceWrapperHeap::ReferenceWrapperHeap()`,assigned to `n$0`,invalid access to `n$0->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 `n$0->f` 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` 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/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`,assigned to `n$0`,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 `n$1`,assigned to `y`,assigned to `n$0`,returned 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`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$0`,invalid access to `n$0->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`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$2`,invalid access to `n$2` 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`,assigned to `n$5`,memory was invalidated by `delete` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$3`,when calling `Simple` here,invalid access to `n$2->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`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$0`,invalid access to `n$0` 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`,assigned to `n$1`,memory was invalidated by `delete` on `n$1` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$0`,invalid access to `n$0->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`,assigned to `n$8`,memory was invalidated by `delete` on `n$8` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$4`,when calling `Simple` here,invalid access to `n$2->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`,assigned to `n$5`,memory was invalidated by `delete` on `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(Simple))`,assigned to `s`,assigned to `n$2`,invalid access to `n$2->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,assigned to `n$3`,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `n$3` 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 `n$3` 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`,assigned to `n$4`,returned from call to `(sizeof(use_after_destructor::S),n$4)`,assigned to `alias`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` 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 `n$0`,invalid access to `n$0->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`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` 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 `n$4`,returned from call to `(sizeof(use_after_destructor::S),n$4)`,assigned to `alias`,assigned to `n$0`,invalid access to `n$0->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`,assigned to `n$2`,memory was invalidated by `delete` on `n$2` 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 `n$7`,assigned to `alias`,assigned to `n$0`,invalid access to `n$0->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,assigned to `n$3`,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `n$3` 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 `n$3` 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,assigned to `n$3`,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `n$3` here,use-after-lifetime part of the trace starts here,returned from call to `__new(sizeof(int))`,assigned to `n$3->f`,returned from call to `use_after_destructor::S::S()`,assigned to `n$8`,invalid access to `*n$8` 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,assigned to `n$3`,when calling `~S` here,when calling `__infer_inner_destructor_~S` here,memory was invalidated by `delete` on `n$3` 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 `n$3` 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 `n$0->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,assigned to `n$0`,when calling `free_global_pointer_ok()` here,memory was invalidated by call to `free()` on `n$0` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_ok()` here,invalid access to `n$0` 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,assigned to `n$2`,memory was invalidated by call to `free()` on `n$2` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,invalid access to `n$0` 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,assigned to `n$2`,memory was invalidated by call to `free()` on `n$2` here,use-after-lifetime part of the trace starts here,assigned to `n$0`,invalid access to `*n$0` 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 `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$10,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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 `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$9,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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`,assigned to `n$1`,invalid access to `*n$1` 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 `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$11,(unsigned long) 1)`,assigned to `elt`,assigned to `n$9`,assigned to `y`,assigned to `n$1`,invalid access to `*n$1` 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 `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$10,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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 `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$21,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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 `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$21,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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`,assigned to `n$1`,invalid access to `*n$1` 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 `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$12,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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 `n$5` here,use-after-lifetime part of the trace starts here,returned from call to `std::vector::at(n$9,(unsigned long) 1)`,assigned to `elt`,assigned to `n$1`,invalid access to `*n$1` 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/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 `alias` 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 `s` 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 `alias` 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::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_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]