From 6a738045fdf89bdc76546f05779fdf20fdff8860 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 17 Oct 2019 03:39:49 -0700 Subject: [PATCH] [pulse] interprocedural histories and traces Summary: bigmacro_bender There are 3 ways pulse tracks history. This is at least one too many. So far, we have: 1. "histories": a humble list of "events" like "assigned here", "returned from call", ... 2. "interproc actions": a structured nesting of calls with a final "action", eg "f calls g calls h which does blah" 3. "traces", which combine one history with one interproc action This diff gets rid of interproc actions and makes histories include "nested" callee histories too. This allows pulse to track and display how a value got assigned across function calls. Traces are now more powerful and interleave histories and interproc actions. This allows pulse to track how a value is fed into an action, for instance performed in callee, which itself creates some more (potentially now interprocedural) history before going to the next step of the action (either another call or the action itself). This gives much better traces, and some examples are added to showcase this. There are a lot of changes when applying summaries to keep track of histories more accurately than was done before, but also a few simplifications that give additional evidence that this is the right concept. Reviewed By: skcho Differential Revision: D17908942 fbshipit-source-id: 3b62eaf78 --- infer/src/checkers/impurityDomain.ml | 42 ++- infer/src/checkers/impurityDomain.mli | 3 +- infer/src/pulse/Pulse.ml | 14 +- infer/src/pulse/PulseAbductiveDomain.ml | 246 ++++++++++-------- infer/src/pulse/PulseAbductiveDomain.mli | 38 +-- infer/src/pulse/PulseDiagnostic.ml | 79 +++--- infer/src/pulse/PulseDiagnostic.mli | 12 +- infer/src/pulse/PulseDomain.ml | 221 ++++++++-------- infer/src/pulse/PulseDomain.mli | 41 +-- infer/src/pulse/PulseModels.ml | 77 +++--- infer/src/pulse/PulseOperations.ml | 84 +++--- infer/src/pulse/PulseOperations.mli | 25 +- .../codetoanalyze/cpp/impurity/issues.exp | 52 ++-- .../codetoanalyze/cpp/pulse/fbstring.cpp | 98 +++++++ .../cpp/pulse/interprocedural.cpp | 8 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 123 ++++----- infer/tests/codetoanalyze/cpp/pulse/trace.cpp | 22 ++ .../codetoanalyze/java/impurity/issues.exp | 40 +-- .../tests/codetoanalyze/objc/pulse/issues.exp | 4 +- .../codetoanalyze/objcpp/pulse/issues.exp | 4 +- 20 files changed, 686 insertions(+), 547 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp create mode 100644 infer/tests/codetoanalyze/cpp/pulse/trace.cpp diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml index a550a8b57..ab262542c 100644 --- a/infer/src/checkers/impurityDomain.ml +++ b/infer/src/checkers/impurityDomain.ml @@ -9,7 +9,7 @@ open! IStd module F = Format type trace = - | WrittenTo of unit PulseDomain.InterprocAction.t + | WrittenTo of unit PulseDomain.Trace.t | Invalid of PulseDomain.Invalidation.t PulseDomain.Trace.t [@@deriving compare] @@ -53,31 +53,19 @@ let pp_param_source fmt = function let add_to_errlog ~nesting param_source ModifiedVar.{var; trace_list} errlog = - let rec aux ~nesting rev_errlog action = - match action with - | WrittenTo (PulseDomain.InterprocAction.Immediate {location}) -> - let rev_errlog = - Errlog.make_trace_element nesting location - (F.asprintf "%a '%a' is modified at %a" pp_param_source param_source Var.pp var - Location.pp location) - [] - :: rev_errlog - in - List.rev_append rev_errlog errlog - | WrittenTo (PulseDomain.InterprocAction.ViaCall {action; f; location}) -> - aux ~nesting:(nesting + 1) - ( Errlog.make_trace_element nesting location - (F.asprintf "%a '%a' is modified when calling %a at %a" pp_param_source param_source - Var.pp var PulseDomain.CallEvent.describe f Location.pp location) - [] - :: rev_errlog ) - (WrittenTo action) - | Invalid trace -> - PulseDomain.Trace.add_to_errlog - ~header:(F.asprintf "%a '%a'" pp_param_source param_source Var.pp var) - (fun f invalidation -> - F.fprintf f "%a here" PulseDomain.Invalidation.describe invalidation ) - trace rev_errlog + let aux ~nesting errlog trace = + match trace with + | WrittenTo access_trace -> + PulseDomain.Trace.add_to_errlog ~nesting + (fun fmt () -> + F.fprintf fmt "%a `%a` modified here" pp_param_source param_source Var.pp var ) + access_trace errlog + | Invalid invalidation_trace -> + PulseDomain.Trace.add_to_errlog ~nesting + (fun fmt invalid -> + F.fprintf fmt "%a `%a` %a here" pp_param_source param_source Var.pp var + PulseDomain.Invalidation.describe invalid ) + invalidation_trace errlog in let first_trace, rest = trace_list in - List.fold_left rest ~init:(aux ~nesting [] first_trace) ~f:(aux ~nesting) + List.fold_left rest ~init:(aux ~nesting errlog first_trace) ~f:(aux ~nesting) diff --git a/infer/src/checkers/impurityDomain.mli b/infer/src/checkers/impurityDomain.mli index 9babc56b0..349b4a920 100644 --- a/infer/src/checkers/impurityDomain.mli +++ b/infer/src/checkers/impurityDomain.mli @@ -7,9 +7,8 @@ open! IStd type trace = - | WrittenTo of unit PulseDomain.InterprocAction.t + | WrittenTo of unit PulseDomain.Trace.t | Invalid of PulseDomain.Invalidation.t PulseDomain.Trace.t -[@@deriving compare] module ModifiedVar : sig type nonempty_action_type = trace * trace list diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index a7902e860..9e6dc096f 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -9,7 +9,6 @@ module F = Format module L = Logging open Result.Monad_infix module AbstractAddress = PulseDomain.AbstractAddress -module InterprocAction = PulseDomain.InterprocAction module Invalidation = PulseDomain.Invalidation module ValueHistory = PulseDomain.ValueHistory @@ -55,7 +54,7 @@ module PulseTransferFunctions = struct type extras = unit let exec_unknown_call reason ret call actuals _flags call_loc astate = - let event = ValueHistory.Call {f= reason; location= call_loc} in + let event = ValueHistory.Call {f= reason; location= call_loc; in_call= []} 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 -> ( @@ -105,14 +104,12 @@ 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 = - let event = - InterprocAction.Immediate {imm= Invalidation.GoneOutOfScope (pvar, typ); location= call_loc} - in + let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in (* 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 + PulseOperations.invalidate_deref call_loc gone_out_of_scope out_of_scope_base astate + >>= PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base let dispatch_call summary ret call_exp actuals call_loc flags astate = @@ -161,8 +158,7 @@ module PulseTransferFunctions = struct (* [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 + >>| fun (astate, rhs_addr_hist) -> PulseOperations.write_id lhs_id rhs_addr_hist astate in [check_error summary result] | Store {e1= lhs_exp; e2= rhs_exp; loc} -> diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index fff5cdc70..494bd89fb 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -10,6 +10,9 @@ module L = Logging module AbstractAddress = PulseDomain.AbstractAddress module Attribute = PulseDomain.Attribute module Attributes = PulseDomain.Attributes +module Invalidation = PulseDomain.Invalidation +module Trace = PulseDomain.Trace +module ValueHistory = PulseDomain.ValueHistory module BaseStack = PulseDomain.Stack module BaseMemory = PulseDomain.Memory @@ -98,21 +101,21 @@ module Stack = struct if phys_equal new_post astate.post then astate else {astate with post= new_post} - let eval var astate = + let eval origin var astate = match BaseStack.find_opt var (astate.post :> base_domain).stack with | Some addr_hist -> (astate, addr_hist) | None -> - let addr_hist = (AbstractAddress.mk_fresh (), []) in + let addr = AbstractAddress.mk_fresh () in + let addr_hist = (addr, origin) 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_hist (astate.pre :> base_domain).stack in - let foot_heap = - BaseMemory.register_address (fst addr_hist) (astate.pre :> base_domain).heap - in + (* HACK: do not record the history of values in the pre as they are unused *) + let foot_stack = BaseStack.add var (addr, []) (astate.pre :> base_domain).stack in + let foot_heap = BaseMemory.register_address addr (astate.pre :> base_domain).heap in InvertedDomain.make foot_stack foot_heap else astate.pre in @@ -152,53 +155,56 @@ module Memory = struct (** if [address] is in [pre] and it should be valid then that fact goes in the precondition *) - let record_must_be_valid action address (pre : InvertedDomain.t) = + let record_must_be_valid access_trace address (pre : InvertedDomain.t) = if BaseMemory.mem_edges address (pre :> base_domain).heap then InvertedDomain.update pre - ~heap:(BaseMemory.add_attribute address (MustBeValid action) (pre :> base_domain).heap) + ~heap: + (BaseMemory.add_attribute address (MustBeValid access_trace) (pre :> base_domain).heap) else pre - let check_valid action addr ({post; pre} as astate) = + let check_valid access_trace addr ({post; pre} as astate) = BaseMemory.check_valid addr (post :> base_domain).heap >>| fun () -> - let new_pre = record_must_be_valid action addr pre in + let new_pre = record_must_be_valid access_trace addr pre in if phys_equal new_pre pre then astate else {astate with pre= new_pre} - let add_edge addr access new_addr_trace loc astate = + let add_edge (addr, history) access new_addr_hist location astate = map_post_heap astate ~f:(fun heap -> - BaseMemory.add_edge addr access new_addr_trace heap - |> BaseMemory.add_attribute addr - (WrittenTo (PulseDomain.InterprocAction.Immediate {imm= (); location= loc})) ) + BaseMemory.add_edge addr access new_addr_hist heap + |> BaseMemory.add_attribute addr (WrittenTo (Trace.Immediate {imm= (); location; history})) + ) let find_edge_opt address access astate = BaseMemory.find_edge_opt address access (astate.post :> base_domain).heap - let eval_edge addr access astate = - match find_edge_opt addr access astate with - | Some addr_trace' -> - (astate, addr_trace') + let eval_edge (addr_src, hist_src) access astate = + match find_edge_opt addr_src access astate with + | Some addr_hist_dst -> + (astate, addr_hist_dst) | None -> - let addr_trace' = (AbstractAddress.mk_fresh (), []) in + let addr_dst = AbstractAddress.mk_fresh () in + let addr_hist_dst = (addr_dst, hist_src) in let post_heap = - BaseMemory.add_edge addr access addr_trace' (astate.post :> base_domain).heap + BaseMemory.add_edge addr_src access addr_hist_dst (astate.post :> base_domain).heap in let foot_heap = - if BaseMemory.mem_edges addr (astate.pre :> base_domain).heap then - BaseMemory.add_edge addr access addr_trace' (astate.pre :> base_domain).heap - |> BaseMemory.register_address (fst addr_trace') + if BaseMemory.mem_edges addr_src (astate.pre :> base_domain).heap then + (* HACK: do not record the history of values in the pre as they are unused *) + BaseMemory.add_edge addr_src access (addr_dst, []) (astate.pre :> base_domain).heap + |> BaseMemory.register_address addr_dst else (astate.pre :> base_domain).heap in ( { post= Domain.update astate.post ~heap:post_heap ; pre= InvertedDomain.update astate.pre ~heap:foot_heap } - , addr_trace' ) + , addr_hist_dst ) - let invalidate address action astate = - map_post_heap astate ~f:(fun heap -> BaseMemory.invalidate address action heap) + let invalidate address invalidation location astate = + map_post_heap astate ~f:(fun heap -> BaseMemory.invalidate address invalidation location heap) let add_attribute address attributes astate = @@ -221,11 +227,11 @@ module Memory = struct let find_opt address astate = BaseMemory.find_opt address (astate.post :> base_domain).heap - let set_cell addr cell loc astate = + let set_cell (addr, history) cell location astate = map_post_heap astate ~f:(fun heap -> BaseMemory.set_cell addr cell heap - |> BaseMemory.add_attribute addr - (WrittenTo (PulseDomain.InterprocAction.Immediate {imm= (); location= loc})) ) + |> BaseMemory.add_attribute addr (WrittenTo (Trace.Immediate {imm= (); location; history})) + ) module Edges = BaseMemory.Edges @@ -241,8 +247,7 @@ let mk_initial proc_desc = |> List.map ~f:(fun (mangled, _) -> let pvar = Pvar.mk mangled proc_name in ( Var.of_pvar pvar - , ( AbstractAddress.mk_fresh () - , [PulseDomain.ValueHistory.FormalDeclared (pvar, location)] ) ) ) + , (AbstractAddress.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)]) ) ) in let initial_stack = List.fold formals ~init:(InvertedDomain.empty :> PulseDomain.t).stack @@ -305,11 +310,10 @@ module PrePost = struct let add_out_of_scope_attribute addr pvar location history heap typ = - let action = - PulseDomain.InterprocAction.Immediate - {imm= PulseDomain.Invalidation.GoneOutOfScope (pvar, typ); location} + let attr = + Attribute.Invalid (Immediate {imm= GoneOutOfScope (pvar, typ); location; history}) in - BaseMemory.add_attribute addr (Invalid {action; history}) heap + BaseMemory.add_attribute addr attr heap (** invalidate local variables going out of scope *) @@ -356,8 +360,8 @@ module PrePost = struct (** stuff we carry around when computing the result of applying one pre/post pair *) type call_state = { astate: t (** caller's abstract state computed so far *) - ; subst: AbstractAddress.t AddressMap.t - (** translation from callee addresses to caller addresses *) + ; subst: (AbstractAddress.t * ValueHistory.t) AddressMap.t + (** translation from callee addresses to caller addresses and their caller histories *) ; rev_subst: AbstractAddress.t AddressMap.t (** the inverse translation from [subst] from caller addresses to callee addresses *) ; visited: AddressSet.t @@ -373,28 +377,31 @@ module PrePost = struct "@[{ astate=@[%a@];@, subst=@[%a@];@, rev_subst=@[%a@];@, \ visited=@[%a@]@, }@]" pp astate - (AddressMap.pp ~pp_value:AbstractAddress.pp) + (AddressMap.pp ~pp_value:(fun fmt (addr, _) -> AbstractAddress.pp fmt addr)) subst (AddressMap.pp ~pp_value:AbstractAddress.pp) rev_subst AddressSet.pp visited - let fold_globals_of_stack stack call_state ~f = + let fold_globals_of_stack call_loc 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) -> 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 + let call_state, addr_hist_caller = + let astate, var_value = + Stack.eval [ValueHistory.VariableAccessed (pvar, call_loc)] 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 + f pvar ~stack_value ~addr_hist_caller call_state | _ -> Ok call_state ) - let visit call_state ~addr_callee ~addr_caller = + let visit call_state ~addr_callee ~addr_hist_caller = + let addr_caller = fst addr_hist_caller in ( match AddressMap.find_opt addr_caller call_state.rev_subst with | Some addr_callee' when not (AbstractAddress.equal addr_callee addr_callee') -> L.d_printfln "Huho, address %a in post already bound to %a, not %a@\nState=%a" @@ -408,7 +415,7 @@ module PrePost = struct ( `NotAlreadyVisited , { call_state with visited= AddressSet.add addr_callee call_state.visited - ; subst= AddressMap.add addr_callee addr_caller call_state.subst + ; subst= AddressMap.add addr_callee addr_hist_caller call_state.subst ; rev_subst= AddressMap.add addr_caller addr_callee call_state.rev_subst } ) @@ -422,13 +429,16 @@ 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 ~pre ~addr_pre ~addr_caller - history call_state = - let mk_action action = - PulseDomain.InterprocAction.ViaCall - {action; f= Call callee_proc_name; location= call_location} + let rec materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre + ~addr_hist_caller call_state = + let add_call trace = + Trace.ViaCall + { in_call= trace + ; f= Call callee_proc_name + ; location= call_location + ; history= snd addr_hist_caller } in - match visit call_state ~addr_callee:addr_pre ~addr_caller with + match visit call_state ~addr_callee:addr_pre ~addr_hist_caller with | `AlreadyVisited, call_state -> Ok call_state | `NotAlreadyVisited, call_state -> ( @@ -436,24 +446,23 @@ module PrePost = struct BaseMemory.find_opt addr_pre pre.PulseDomain.heap >>= fun (edges_pre, attrs_pre) -> Attributes.get_must_be_valid attrs_pre - >>| fun callee_action -> - let action = mk_action callee_action in - match Memory.check_valid action addr_caller call_state.astate with + >>| fun callee_access_trace -> + let access_trace = add_call callee_access_trace in + match Memory.check_valid access_trace (fst addr_hist_caller) call_state.astate with | Error invalidated_by -> Error - (PulseDiagnostic.AccessToInvalidAddress - {invalidated_by; accessed_by= {action; history}}) + (PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= access_trace}) | 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.eval_edge addr_caller access call_state.astate + let astate, addr_hist_dest_caller = + Memory.eval_edge addr_hist_caller access call_state.astate in let call_state = {call_state with astate} in materialize_pre_from_address callee_proc_name call_location ~pre - ~addr_pre:addr_pre_dest ~addr_caller:addr_caller_dest history call_state )) + ~addr_pre:addr_pre_dest ~addr_hist_caller:addr_hist_dest_caller call_state )) |> function Some result -> result | None -> Ok call_state ) @@ -461,15 +470,14 @@ 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 = - let addr_caller, trace = actual in - L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal AbstractAddress.pp addr_caller ; + L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal AbstractAddress.pp (fst actual) ; (let open Option.Monad_infix in BaseStack.find_opt formal pre.PulseDomain.stack >>= fun (addr_formal_pre, _) -> BaseMemory.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) + ~addr_hist_caller:actual call_state) |> function Some result -> result | None -> Ok call_state @@ -514,11 +522,11 @@ 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, history) ~addr_caller call_state -> + fold_globals_of_stack call_location (pre_post.pre :> PulseDomain.t).stack call_state + ~f:(fun _var ~stack_value:(addr_pre, _) ~addr_hist_caller call_state -> materialize_pre_from_address callee_proc_name call_location ~pre:(pre_post.pre :> PulseDomain.t) - ~addr_pre ~addr_caller history call_state ) + ~addr_pre ~addr_hist_caller call_state ) let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state = @@ -537,19 +545,21 @@ module PrePost = struct (* {3 applying the post to the current state} *) - let subst_find_or_new subst addr_callee = + let subst_find_or_new subst addr_callee ~default_hist_caller = match AddressMap.find_opt addr_callee subst with | None -> - let addr_fresh = AbstractAddress.mk_fresh () in - (addr_fresh, AddressMap.add addr_callee addr_fresh subst) - | Some addr_caller -> - (addr_caller, subst) + let addr_hist_fresh = (AbstractAddress.mk_fresh (), default_hist_caller) in + (AddressMap.add addr_callee addr_hist_fresh subst, addr_hist_fresh) + | Some addr_hist_caller -> + (subst, addr_hist_caller) - let call_state_subst_find_or_new call_state addr_callee = - let addr_caller, new_subst = subst_find_or_new call_state.subst addr_callee in - if phys_equal new_subst call_state.subst then (call_state, addr_caller) - else ({call_state with subst= new_subst}, addr_caller) + let call_state_subst_find_or_new call_state addr_callee ~default_hist_caller = + let new_subst, addr_hist_caller = + subst_find_or_new call_state.subst addr_callee ~default_hist_caller + in + if phys_equal new_subst call_state.subst then (call_state, addr_hist_caller) + else ({call_state with subst= new_subst}, addr_hist_caller) let delete_edges_in_callee_pre_from_caller ~addr_callee:_ ~cell_pre_opt ~addr_caller call_state = @@ -572,14 +582,15 @@ module PrePost = struct old_post_edges edges_pre ) - let add_call_to_attr proc_name location attr = + let add_call_to_attr proc_name call_location caller_history attr = match (attr : Attribute.t) with - | Invalid trace -> + | Invalid invalidation -> Attribute.Invalid - { action= - PulseDomain.InterprocAction.ViaCall - {action= trace.action; f= Call proc_name; location} - ; history= trace.history } + (ViaCall + { f= Call proc_name + ; location= call_location + ; history= caller_history + ; in_call= invalidation }) | AddressOfCppTemporary (_, _) | AddressOfStackVariable (_, _, _) | Closure _ @@ -591,25 +602,28 @@ module PrePost = struct let record_post_cell callee_proc_name call_loc ~addr_callee ~cell_pre_opt - ~cell_post:(edges_post, attrs_post) ~addr_caller call_state = + ~cell_post:(edges_post, attrs_post) ~addr_hist_caller:(addr_caller, hist_caller) call_state = let post_edges_minus_pre = delete_edges_in_callee_pre_from_caller ~addr_callee ~cell_pre_opt ~addr_caller call_state in let heap = (call_state.astate.post :> base_domain).heap in let heap = let attrs_post_caller = - Attributes.map ~f:(fun attr -> add_call_to_attr callee_proc_name call_loc attr) attrs_post + Attributes.map attrs_post ~f:(fun attr -> + add_call_to_attr callee_proc_name call_loc hist_caller attr ) in BaseMemory.set_attrs addr_caller attrs_post_caller heap in let subst, translated_post_edges = BaseMemory.Edges.fold_map ~init:call_state.subst edges_post ~f:(fun subst (addr_callee, trace_post) -> - let addr_curr, subst = subst_find_or_new subst addr_callee in + let subst, (addr_curr, hist_curr) = + subst_find_or_new subst addr_callee ~default_hist_caller:hist_caller + in ( subst , ( addr_curr - , PulseDomain.ValueHistory.Call {f= Call callee_proc_name; location= call_loc} - :: trace_post ) ) ) + , ValueHistory.Call {f= Call callee_proc_name; location= call_loc; in_call= trace_post} + :: hist_curr ) ) ) in let heap = let edges_post_caller = @@ -618,14 +632,23 @@ module PrePost = struct post_edges_minus_pre translated_post_edges in let written_to = - (let open Option.Monad_infix in + let open Option.Monad_infix in BaseMemory.find_opt addr_caller heap - >>= fun (_edges, attrs) -> - Attributes.get_written_to attrs - >>| fun callee_action -> + >>= (fun (_edges, attrs) -> Attributes.get_written_to attrs) + |> fun written_to_callee_opt -> + let callee_trace = + match written_to_callee_opt with + | None -> + Trace.Immediate {imm= (); location= call_loc; history= []} + | Some access_trace -> + access_trace + in Attribute.WrittenTo - (ViaCall {action= callee_action; f= Call callee_proc_name; location= call_loc})) - |> Option.value ~default:(Attribute.WrittenTo (Immediate {imm= (); location= call_loc})) + (ViaCall + { in_call= callee_trace + ; f= Call callee_proc_name + ; location= call_loc + ; history= hist_caller }) in BaseMemory.set_edges addr_caller edges_post_caller heap |> BaseMemory.add_attribute addr_caller written_to @@ -635,9 +658,9 @@ module PrePost = struct let rec record_post_for_address callee_proc_name call_loc ({pre; post} as pre_post) ~addr_callee - ~addr_caller call_state = - L.d_printfln "%a<->%a" AbstractAddress.pp addr_callee AbstractAddress.pp addr_caller ; - match visit call_state ~addr_callee ~addr_caller with + ~addr_hist_caller call_state = + L.d_printfln "%a<->%a" AbstractAddress.pp addr_callee AbstractAddress.pp (fst addr_hist_caller) ; + match visit call_state ~addr_callee ~addr_hist_caller with | `AlreadyVisited, call_state -> call_state | `NotAlreadyVisited, call_state -> ( @@ -651,23 +674,23 @@ module PrePost = struct let call_state_after_post = if is_cell_read_only ~cell_pre_opt ~cell_post then call_state else - record_post_cell callee_proc_name call_loc ~addr_callee ~cell_pre_opt ~addr_caller - ~cell_post call_state + record_post_cell callee_proc_name call_loc ~addr_callee ~cell_pre_opt + ~addr_hist_caller ~cell_post call_state in IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold ~init:call_state_after_post edges_post ~f:(fun call_state (_access, (addr_callee_dest, _)) -> - let call_state, addr_curr_dest = + let call_state, addr_hist_curr_dest = call_state_subst_find_or_new call_state addr_callee_dest + ~default_hist_caller:(snd addr_hist_caller) in record_post_for_address callee_proc_name call_loc pre_post - ~addr_callee:addr_callee_dest ~addr_caller:addr_curr_dest call_state ) ) + ~addr_callee:addr_callee_dest ~addr_hist_caller:addr_hist_curr_dest call_state ) ) let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual call_state = - let addr_caller, _ = actual in L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal AbstractAddress.pp - addr_caller ; + (fst actual) ; match let open Option.Monad_infix in BaseStack.find_opt formal (pre_post.pre :> PulseDomain.t).PulseDomain.stack @@ -676,7 +699,7 @@ module PrePost = struct (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 + ~addr_hist_caller:actual call_state with | Some call_state -> call_state @@ -697,18 +720,19 @@ module PrePost = struct | None -> (call_state, None) | Some (return_callee, _) -> - let return_caller = + let return_caller_addr_hist = match AddressMap.find_opt return_callee call_state.subst with - | Some return_caller -> - return_caller + | Some return_caller_hist -> + return_caller_hist | None -> - AbstractAddress.mk_fresh () + ( AbstractAddress.mk_fresh () + , [ (* this could maybe include an event like "returned here" *) ] ) 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 + ~addr_hist_caller:return_caller_addr_hist call_state in - (call_state, Some return_caller) ) + (call_state, Some return_caller_addr_hist) ) let apply_post_for_parameters callee_proc_name call_location pre_post ~formals ~actuals @@ -732,11 +756,11 @@ module PrePost = struct let apply_post_for_globals callee_proc_name call_location pre_post call_state = match - fold_globals_of_stack (pre_post.pre :> PulseDomain.t).stack call_state - ~f:(fun _var ~stack_value:(addr_callee, _) ~addr_caller call_state -> + fold_globals_of_stack call_location (pre_post.pre :> PulseDomain.t).stack call_state + ~f:(fun _var ~stack_value:(addr_callee, _) ~addr_hist_caller call_state -> Ok (record_post_for_address callee_proc_name call_location pre_post ~addr_callee - ~addr_caller call_state) ) + ~addr_hist_caller call_state) ) with | Error _ -> (* always return [Ok _] above *) assert false @@ -755,10 +779,10 @@ module PrePost = struct match AddressMap.find_opt addr_callee call_state.subst with | None -> (* callee address has no meaning for the caller *) heap - | Some addr_caller -> + | Some (addr_caller, history) -> let attrs' = Attributes.map - ~f:(fun attr -> add_call_to_attr callee_proc_name call_loc attr) + ~f:(fun attr -> add_call_to_attr callee_proc_name call_loc history attr) attrs in BaseMemory.set_attrs addr_caller attrs' heap ) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 7cf77765a..fc325e72c 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -7,6 +7,9 @@ open! IStd module AbstractAddress = PulseDomain.AbstractAddress module Attribute = PulseDomain.Attribute +module Invalidation = PulseDomain.Invalidation +module Trace = PulseDomain.Trace +module ValueHistory = PulseDomain.ValueHistory (* layer on top of {!PulseDomain} to propagate operations on the current state to the pre-condition when necessary @@ -29,7 +32,7 @@ module Stack : sig val find_opt : Var.t -> t -> PulseDomain.Stack.value option - val eval : Var.t -> t -> t * PulseDomain.AddrTracePair.t + val eval : ValueHistory.t -> 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 @@ -46,25 +49,23 @@ module Memory : sig val add_attribute : AbstractAddress.t -> Attribute.t -> t -> t val add_edge : - AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> Location.t -> t -> t - - val check_valid : - unit PulseDomain.InterprocAction.t - -> AbstractAddress.t + AbstractAddress.t * ValueHistory.t + -> Access.t + -> PulseDomain.AddrTracePair.t + -> Location.t + -> t -> t - -> (t, PulseDomain.Invalidation.t PulseDomain.Trace.t) result + + val check_valid : unit Trace.t -> AbstractAddress.t -> t -> (t, Invalidation.t Trace.t) result val find_opt : AbstractAddress.t -> t -> PulseDomain.Memory.cell option val find_edge_opt : AbstractAddress.t -> Access.t -> t -> PulseDomain.AddrTracePair.t option - val set_cell : AbstractAddress.t -> PulseDomain.Memory.cell -> Location.t -> t -> t + val set_cell : + AbstractAddress.t * ValueHistory.t -> PulseDomain.Memory.cell -> Location.t -> t -> t - val invalidate : - AbstractAddress.t * PulseDomain.ValueHistory.t - -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t - -> t - -> t + val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option @@ -72,9 +73,10 @@ module Memory : sig val std_vector_reserve : AbstractAddress.t -> t -> 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. *) + val eval_edge : + AbstractAddress.t * ValueHistory.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t + (** [eval_edge (addr,hist) 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. *) val get_constant : AbstractAddress.t -> t -> Const.t option end @@ -95,9 +97,9 @@ module PrePost : sig -> Location.t -> t -> formals:Var.t list - -> actuals:((AbstractAddress.t * PulseDomain.ValueHistory.t) * Typ.t) list + -> actuals:((AbstractAddress.t * ValueHistory.t) * Typ.t) list -> domain_t - -> (domain_t * AbstractAddress.t option, PulseDiagnostic.t) result + -> (domain_t * (AbstractAddress.t * ValueHistory.t) option, PulseDiagnostic.t) result (** return the abstract state after the call along with an optional return value *) end diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index cc33cc9be..cf5fa393a 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -7,25 +7,24 @@ open! IStd module F = Format +module CallEvent = PulseDomain.CallEvent +module Invalidation = PulseDomain.Invalidation +module Trace = PulseDomain.Trace +module ValueHistory = PulseDomain.ValueHistory type t = - | AccessToInvalidAddress of - { invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t - ; accessed_by: unit PulseDomain.Trace.t } - | StackVariableAddressEscape of - { variable: Var.t - ; history: PulseDomain.ValueHistory.t - ; location: Location.t } + | AccessToInvalidAddress of {invalidated_by: Invalidation.t Trace.t; accessed_by: unit Trace.t} + | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t} let get_location = function | AccessToInvalidAddress {accessed_by} -> - PulseDomain.InterprocAction.to_outer_location accessed_by.action + Trace.get_outer_location accessed_by | StackVariableAddressEscape {location} -> location let get_message = function - | AccessToInvalidAddress {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 @@ -43,31 +42,27 @@ 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 fmt (trace : _ PulseDomain.Trace.t) = - match trace.action with - | Immediate {imm= _; _} -> + let pp_access_trace fmt (trace : unit Trace.t) = + match trace with + | Immediate {imm= (); _} -> F.fprintf fmt "accessing memory that " | ViaCall {f; _} -> - F.fprintf fmt "call to %a eventually accesses memory that " - PulseDomain.CallEvent.describe f + F.fprintf fmt "call to %a eventually accesses memory that " CallEvent.describe f in - let pp_invalidation_trace line fmt trace = - match trace.PulseDomain.Trace.action with - | Immediate {imm= invalidation; _} -> - F.fprintf fmt "%a on line %d" PulseDomain.Invalidation.describe invalidation line - | ViaCall {action; f; _} -> - F.fprintf fmt "%a on line %d indirectly during the call to %a" - PulseDomain.Invalidation.describe - (PulseDomain.InterprocAction.get_immediate action) - line PulseDomain.CallEvent.describe f + let pp_invalidation_trace line fmt (trace : Invalidation.t Trace.t) = + let pp_line fmt line = F.fprintf fmt " on line %d" line in + match trace with + | ViaCall {f; in_call} -> + let invalid = Trace.get_immediate in_call in + F.fprintf fmt "%a%a indirectly during the call to %a" Invalidation.describe invalid + pp_line line CallEvent.describe f + | Immediate {imm= invalid} -> + F.fprintf fmt "%a%a" Invalidation.describe invalid pp_line line in - let line_of_trace trace = - let {Location.line; _} = - PulseDomain.InterprocAction.to_outer_location trace.PulseDomain.Trace.action - in + let invalidation_line = + let {Location.line; _} = Trace.get_outer_location invalidated_by in line in - let invalidation_line = line_of_trace invalidated_by in F.asprintf "%a%a" pp_access_trace accessed_by (pp_invalidation_trace invalidation_line) invalidated_by @@ -79,18 +74,29 @@ let get_message = function F.asprintf "address of %a is returned by the function" pp_var variable +let add_errlog_header ~title location errlog = + let depth = 0 in + let tags = [] in + Errlog.make_trace_element depth location title tags :: errlog + + let get_trace = function | AccessToInvalidAddress {accessed_by; invalidated_by} -> - PulseDomain.Trace.add_to_errlog ~header:"invalidation part of the trace starts here" - (fun f invalidation -> - F.fprintf f "memory %a here" PulseDomain.Invalidation.describe invalidation ) - invalidated_by - @@ PulseDomain.Trace.add_to_errlog ~header:"use-after-lifetime part of the trace starts here" - (fun f () -> F.pp_print_string f "invalid access occurs here") + let start_location = Trace.get_start_location invalidated_by in + add_errlog_header ~title:"invalidation part of the trace starts here" start_location + @@ Trace.add_to_errlog ~nesting:1 + (fun fmt invalid -> F.fprintf fmt "%a" Invalidation.describe invalid) + invalidated_by + @@ + let access_start_location = Trace.get_start_location accessed_by in + add_errlog_header ~title:"use-after-lifetime part of the trace starts here" + access_start_location + @@ Trace.add_to_errlog ~nesting:1 + (fun fmt () -> F.pp_print_string fmt "invalid access occurs here") accessed_by @@ [] | StackVariableAddressEscape {history; location; _} -> - PulseDomain.ValueHistory.add_to_errlog ~nesting:0 history + ValueHistory.add_to_errlog ~nesting:0 history @@ let nesting = 0 in [Errlog.make_trace_element nesting location "returned here" []] @@ -98,7 +104,6 @@ let get_trace = function let get_issue_type = function | AccessToInvalidAddress {invalidated_by} -> - PulseDomain.InterprocAction.get_immediate invalidated_by.action - |> PulseDomain.Invalidation.issue_type_of_cause + Trace.get_immediate invalidated_by |> Invalidation.issue_type_of_cause | StackVariableAddressEscape _ -> IssueType.stack_variable_address_escape diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index 090726cac..9f7652b46 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -6,16 +6,14 @@ *) open! IStd +module Invalidation = PulseDomain.Invalidation +module Trace = PulseDomain.Trace +module ValueHistory = PulseDomain.ValueHistory (** an error to report to the user *) type t = - | AccessToInvalidAddress of - { invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t - ; accessed_by: unit PulseDomain.Trace.t } - | StackVariableAddressEscape of - { variable: Var.t - ; history: PulseDomain.ValueHistory.t - ; location: Location.t } + | AccessToInvalidAddress of {invalidated_by: Invalidation.t Trace.t; accessed_by: unit Trace.t} + | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t} val get_message : t -> string diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index a057a2823..bc2b9e94d 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -124,18 +124,26 @@ end module ValueHistory = struct type event = | Assignment of Location.t - | Call of {f: CallEvent.t; location: Location.t} + | Call of {f: CallEvent.t; location: Location.t; in_call: t} | Capture of {captured_as: Pvar.t; location: Location.t} | CppTemporaryCreated of Location.t | FormalDeclared of Pvar.t * Location.t + | VariableAccessed of Pvar.t * Location.t | VariableDeclared of Pvar.t * Location.t - [@@deriving compare] - let pp_event_no_location fmt = function + and t = event list [@@deriving compare] + + let pp_event_no_location fmt event = + let pp_pvar fmt pvar = + if Pvar.is_global pvar then + F.fprintf fmt "global variable `%a`" Pvar.pp_value_non_verbose pvar + else F.fprintf fmt "variable `%a`" Pvar.pp_value_non_verbose pvar + in + match event with | Assignment _ -> F.pp_print_string fmt "assigned" | Call {f; location= _} -> - F.fprintf fmt "returned from call to %a" CallEvent.pp f + F.fprintf fmt "passed as argument to %a" CallEvent.pp f | Capture {captured_as; location= _} -> F.fprintf fmt "value captured as `%a`" Pvar.pp_value_non_verbose captured_as | CppTemporaryCreated _ -> @@ -146,8 +154,10 @@ module ValueHistory = struct |> Option.iter ~f:(fun proc_name -> F.fprintf fmt " of %a" Typ.Procname.pp proc_name) in F.fprintf fmt "parameter `%a`%a" Pvar.pp_value_non_verbose pvar pp_proc pvar + | VariableAccessed (pvar, _) -> + F.fprintf fmt "%a accessed here" pp_pvar pvar | VariableDeclared (pvar, _) -> - F.fprintf fmt "variable `%a` declared here" Pvar.pp_value_non_verbose pvar + F.fprintf fmt "%a declared here" pp_pvar pvar let location_of_event = function @@ -156,105 +166,115 @@ module ValueHistory = struct | Capture {location} | CppTemporaryCreated location | FormalDeclared (_, location) + | VariableAccessed (_, location) | VariableDeclared (_, location) -> location - let pp_event fmt crumb = - F.fprintf fmt "%a at %a" pp_event_no_location crumb Location.pp_line (location_of_event crumb) - - - let errlog_trace_elem_of_event ~nesting crumb = - let location = location_of_event crumb in - let description = F.asprintf "%a" pp_event_no_location crumb in - let tags = [] in - Errlog.make_trace_element nesting location description tags + let pp_event fmt event = + F.fprintf fmt "%a at %a" pp_event_no_location event Location.pp_line (location_of_event event) - type t = event list [@@deriving compare] + let pp fmt history = + let rec pp_aux fmt = function + | [] -> + () + | (Call {f; in_call} as event) :: tail -> + F.fprintf fmt "%a@;" pp_event event ; + F.fprintf fmt "[%a]@;" pp_aux (List.rev in_call) ; + if not (List.is_empty tail) then F.fprintf fmt "return from call to %a@;" CallEvent.pp f ; + pp_aux fmt tail + | event :: tail -> + F.fprintf fmt "%a@;" pp_event event ; + pp_aux fmt tail + in + F.fprintf fmt "@[%a@]" pp_aux (List.rev history) - let pp f events = Pp.seq ~print_env:Pp.text_break pp_event f events - let add_to_errlog ~nesting events errlog = - List.rev_map_append ~f:(errlog_trace_elem_of_event ~nesting) events errlog + let add_event_to_errlog ~nesting event errlog = + let location = location_of_event event in + let description = F.asprintf "%a" pp_event_no_location event in + let tags = [] in + Errlog.make_trace_element nesting location description tags :: errlog - let get_start_location = function [] -> None | crumb :: _ -> Some (location_of_event crumb) + let add_returned_from_call_to_errlog ~nesting f location errlog = + let description = F.asprintf "return from call to %a" CallEvent.pp f in + let tags = [] in + Errlog.make_trace_element nesting location description tags :: errlog + + + let add_to_errlog ~nesting history errlog = + let rec add_to_errlog_aux ~nesting history errlog = + match history with + | [] -> + errlog + | (Call {f; location; in_call} as event) :: tail -> + add_to_errlog_aux ~nesting tail + @@ add_event_to_errlog ~nesting event + @@ add_to_errlog_aux ~nesting:(nesting + 1) in_call + @@ add_returned_from_call_to_errlog ~nesting f location + @@ errlog + | event :: tail -> + add_to_errlog_aux ~nesting tail @@ add_event_to_errlog ~nesting event @@ errlog + in + add_to_errlog_aux ~nesting history errlog end -module InterprocAction = struct +module Trace = struct type 'a t = - | Immediate of {imm: 'a; location: Location.t} - | ViaCall of {action: 'a t; f: CallEvent.t; location: Location.t} + | Immediate of {imm: 'a; location: Location.t; history: ValueHistory.t} + | ViaCall of {f: CallEvent.t; location: Location.t; history: ValueHistory.t; in_call: 'a t} [@@deriving compare] - let dummy = Immediate {imm= (); location= Location.dummy} + (** only for use in the attributes' [*_rank] functions *) + let mk_dummy imm = Immediate {imm; location= Location.dummy; history= []} let rec get_immediate = function | Immediate {imm; _} -> imm - | ViaCall {action; _} -> - get_immediate action + | ViaCall {in_call; _} -> + get_immediate in_call - let pp pp_immediate fmt = function - | Immediate {imm; _} -> - pp_immediate fmt imm - | ViaCall {f; action; _} -> - F.fprintf fmt "%a in call to %a" pp_immediate (get_immediate action) CallEvent.pp f - - - let add_to_errlog ~nesting pp_immediate action errlog = - let rec aux ~nesting rev_errlog action = - match action with - | Immediate {imm; location} -> - let rev_errlog = - Errlog.make_trace_element nesting location (F.asprintf "%a" pp_immediate imm) [] - :: rev_errlog - in - List.rev_append rev_errlog errlog - | ViaCall {action; f; location} -> - aux ~nesting:(nesting + 1) - ( Errlog.make_trace_element nesting location - (F.asprintf "when calling %a here" CallEvent.pp f) - [] - :: rev_errlog ) - action - in - aux ~nesting [] action + let get_outer_location = function Immediate {location; _} | ViaCall {location; _} -> location + let get_history = function Immediate {history; _} | ViaCall {history; _} -> history - let to_outer_location = function Immediate {location} | ViaCall {location} -> location -end - -module Trace = struct - type 'a t = {action: 'a InterprocAction.t; history: ValueHistory.t} [@@deriving compare] - - let pp pp_immediate f {action; history} = - if Config.debug_level_analysis < 3 then InterprocAction.pp pp_immediate f action - else - F.fprintf f "{@[action=@[%a@]@;history=@[%a@]@]}" (InterprocAction.pp pp_immediate) action - ValueHistory.pp history - - - let add_errlog_header ~title location errlog = - let depth = 0 in - let tags = [] in - Errlog.make_trace_element depth location title tags :: errlog - - - let add_to_errlog ~header pp_immediate trace errlog = - let start_location = - match ValueHistory.get_start_location trace.history with - | Some location -> - location - | None -> - InterprocAction.to_outer_location trace.action - in - add_errlog_header ~title:header start_location - @@ ValueHistory.add_to_errlog ~nesting:1 trace.history - @@ InterprocAction.add_to_errlog ~nesting:1 pp_immediate trace.action - @@ errlog + let get_start_location trace = + match get_history trace |> List.last with + | Some event -> + ValueHistory.location_of_event event + | None -> + get_outer_location trace + + + let rec pp pp_immediate fmt = function + | Immediate {imm; location= _; history} -> + if Config.debug_level_analysis < 3 then pp_immediate fmt imm + else F.fprintf fmt "%a::%a" ValueHistory.pp history pp_immediate imm + | ViaCall {f; location= _; history; in_call} -> + if Config.debug_level_analysis < 3 then pp pp_immediate fmt in_call + else + F.fprintf fmt "%a::%a[%a]" ValueHistory.pp history CallEvent.pp f (pp pp_immediate) + in_call + + + let rec add_to_errlog ~nesting pp_immediate trace errlog = + match trace with + | Immediate {imm; location; history} -> + ValueHistory.add_to_errlog ~nesting history + @@ Errlog.make_trace_element nesting location (F.asprintf "%a" pp_immediate imm) [] + :: errlog + | ViaCall {f; location; in_call; history} -> + ValueHistory.add_to_errlog ~nesting history + @@ (fun errlog -> + Errlog.make_trace_element nesting location + (F.asprintf "when calling %a here" CallEvent.pp f) + [] + :: errlog ) + @@ add_to_errlog ~nesting:(nesting + 1) pp_immediate in_call + @@ errlog end module Attribute = struct @@ -272,9 +292,9 @@ module Attribute = struct | Closure of Typ.Procname.t | Constant of Const.t | Invalid of Invalidation.t Trace.t - | MustBeValid of unit InterprocAction.t + | MustBeValid of unit Trace.t | StdVectorReserve - | WrittenTo of unit InterprocAction.t + | WrittenTo of unit Trace.t [@@deriving compare, variants] let equal = [%compare.equal: t] @@ -283,7 +303,7 @@ module Attribute = struct let closure_rank = Variants.to_rank (Closure (Typ.Procname.from_string_c_fun "")) - let written_to_rank = Variants.to_rank (WrittenTo InterprocAction.dummy) + let written_to_rank = Variants.to_rank (WrittenTo (Trace.mk_dummy ())) let address_of_stack_variable_rank = let pname = Typ.Procname.from_string_c_fun "" in @@ -292,19 +312,19 @@ module Attribute = struct Variants.to_rank (AddressOfStackVariable (var, location, [])) - let invalid_rank = - Variants.to_rank - (Invalid - {action= Immediate {imm= Invalidation.Nullptr; location= Location.dummy}; history= []}) - + let invalid_rank = Variants.to_rank (Invalid (Trace.mk_dummy Invalidation.Nullptr)) - let must_be_valid_rank = Variants.to_rank (MustBeValid InterprocAction.dummy) + let must_be_valid_rank = Variants.to_rank (MustBeValid (Trace.mk_dummy ())) let std_vector_reserve_rank = Variants.to_rank StdVectorReserve let const_rank = Variants.to_rank (Constant (Const.Cint IntLit.zero)) - let pp f = function + let pp f attribute = + let pp_string_if_debug string fmt () = + if Config.debug_level_analysis >= 3 then F.pp_print_string fmt string + in + match attribute with | AddressOfCppTemporary (var, history) -> F.fprintf f "t&%a (%a)" Var.pp var ValueHistory.pp history | AddressOfStackVariable (var, location, history) -> @@ -314,19 +334,13 @@ module Attribute = struct | Constant c -> F.fprintf f "=%a" (Const.pp Pp.text) c | Invalid invalidation -> - (Trace.pp Invalidation.pp) f invalidation + F.fprintf f "Invalid %a" (Trace.pp Invalidation.pp) invalidation | MustBeValid action -> - F.fprintf f "MustBeValid (read by %a @ %a)" - (InterprocAction.pp (fun _ () -> ())) - action Location.pp - (InterprocAction.to_outer_location action) + F.fprintf f "MustBeValid %a" (Trace.pp (pp_string_if_debug "access")) action | StdVectorReserve -> F.pp_print_string f "std::vector::reserve()" | WrittenTo action -> - F.fprintf f "WrittenTo (written by %a @ %a)" - (InterprocAction.pp (fun _ () -> ())) - action Location.pp - (InterprocAction.to_outer_location action) + F.fprintf f "WrittenTo %a" (Trace.pp (pp_string_if_debug "mutation")) action end module Attributes = struct @@ -489,7 +503,7 @@ module Memory : sig val add_attribute : AbstractAddress.t -> Attribute.t -> t -> t - val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t InterprocAction.t -> t -> t + val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t Trace.t) result @@ -553,8 +567,9 @@ end = struct (fst memory, Graph.add addr new_attrs (snd memory)) - let invalidate (address, history) invalidation memory = - add_attribute address (Attribute.Invalid {action= invalidation; history}) memory + let invalidate (address, history) invalid location memory = + let invalidation = Trace.Immediate {imm= invalid; location; history} in + add_attribute address (Attribute.Invalid invalidation) memory let check_valid address memory = diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index 9a4d1d80f..d03b40f56 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -48,34 +48,39 @@ end module ValueHistory : sig type event = | Assignment of Location.t - | Call of {f: CallEvent.t; location: Location.t} + | Call of {f: CallEvent.t; location: Location.t; in_call: t} | Capture of {captured_as: Pvar.t; location: Location.t} | CppTemporaryCreated of Location.t | FormalDeclared of Pvar.t * Location.t + | VariableAccessed of Pvar.t * Location.t | VariableDeclared of Pvar.t * Location.t - type t = event list [@@deriving compare] + and t = event list [@@deriving compare] - val add_to_errlog : - nesting:int -> event list -> Errlog.loc_trace_elem list -> Errlog.loc_trace_elem list + val add_to_errlog : nesting:int -> t -> Errlog.loc_trace_elem list -> Errlog.loc_trace_elem list end -module InterprocAction : sig +module Trace : sig type 'a t = - | Immediate of {imm: 'a; location: Location.t} - | ViaCall of {action: 'a t; f: CallEvent.t; location: Location.t} + | Immediate of {imm: 'a; location: Location.t; history: ValueHistory.t} + | ViaCall of + { f: CallEvent.t + ; location: Location.t (** location of the call event *) + ; history: ValueHistory.t (** the call involves a value with this prior history *) + ; in_call: 'a t (** last step of the trace is in a call to [f] made at [location] *) } [@@deriving compare] - val get_immediate : 'a t -> 'a + val get_outer_location : 'a t -> Location.t + (** skip histories and go straight to the where the action is: either the action itself or the + call that leads to the action *) - val to_outer_location : 'a t -> Location.t -end + val get_start_location : 'a t -> Location.t + (** initial step in the history if not empty, or else same as {!get_outer_location} *) -module Trace : sig - type 'a t = {action: 'a InterprocAction.t; history: ValueHistory.t} [@@deriving compare] + val get_immediate : 'a t -> 'a val add_to_errlog : - header:string + nesting:int -> (F.formatter -> 'a -> unit) -> 'a t -> Errlog.loc_trace_elem list @@ -89,20 +94,20 @@ module Attribute : sig | Closure of Typ.Procname.t | Constant of Const.t | Invalid of Invalidation.t Trace.t - | MustBeValid of unit InterprocAction.t + | MustBeValid of unit Trace.t | StdVectorReserve - | WrittenTo of unit InterprocAction.t + | WrittenTo of unit Trace.t [@@deriving compare] end module Attributes : sig include PrettyPrintable.PPUniqRankSet with type elt = Attribute.t - val get_must_be_valid : t -> unit InterprocAction.t option + val get_must_be_valid : t -> unit Trace.t option val get_invalid : t -> Invalidation.t Trace.t option - val get_written_to : t -> unit InterprocAction.t option + val get_written_to : t -> unit Trace.t option val get_address_of_stack_variable : t -> (Var.t * Location.t * ValueHistory.t) option @@ -183,7 +188,7 @@ module Memory : sig val add_attribute : AbstractAddress.t -> Attribute.t -> t -> t - val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t InterprocAction.t -> t -> t + val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t Trace.t) result diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 1f8f7f59f..1d3ffe11b 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -20,16 +20,15 @@ type model = exec_fun module Misc = struct let shallow_copy model_desc : model = fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> - let event = PulseDomain.ValueHistory.Call {f= Model model_desc; location} in + let event = PulseDomain.ValueHistory.Call {f= Model model_desc; location; in_call= []} in ( match actuals with | [(dest_pointer_hist, _); (src_pointer_hist, _)] -> PulseOperations.eval_access location src_pointer_hist Dereference astate >>= fun (astate, obj) -> PulseOperations.shallow_copy location obj astate >>= fun (astate, obj_copy) -> - let obj_hist = snd obj in PulseOperations.write_deref location ~ref:dest_pointer_hist - ~obj:(obj_copy, event :: obj_hist) + ~obj:(fst obj_copy, event :: snd obj_copy) astate | _ -> Ok astate ) @@ -46,9 +45,7 @@ module C = struct fun ~caller_summary:_ location ~ret:_ ~actuals astate -> match actuals with | [(deleted_access, _)] -> - PulseOperations.invalidate location - (PulseDomain.InterprocAction.Immediate {imm= PulseDomain.Invalidation.CFree; location}) - deleted_access astate + PulseOperations.invalidate location PulseDomain.Invalidation.CFree deleted_access astate >>| List.return | _ -> Ok [astate] @@ -59,9 +56,8 @@ module Cplusplus = struct fun ~caller_summary:_ location ~ret:_ ~actuals astate -> match actuals with | [(deleted_access, _)] -> - PulseOperations.invalidate location - (PulseDomain.InterprocAction.Immediate {imm= PulseDomain.Invalidation.CppDelete; location}) - deleted_access astate + PulseOperations.invalidate location PulseDomain.Invalidation.CppDelete deleted_access + astate >>| List.return | _ -> Ok [astate] @@ -69,10 +65,12 @@ module Cplusplus = struct let placement_new : model = fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> - let event = PulseDomain.ValueHistory.Call {f= Model "()"; location} in + let event = + PulseDomain.ValueHistory.Call {f= Model "()"; location; in_call= []} + in match List.rev actuals with - | ((address, _), _) :: _ -> - Ok [PulseOperations.write_id ret_id (address, [event]) astate] + | ((address, hist), _) :: _ -> + Ok [PulseOperations.write_id ret_id (address, event :: hist) astate] | _ -> Ok [PulseOperations.havoc_id ret_id [event] astate] end @@ -92,7 +90,9 @@ module StdBasicString = struct let data : model = fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> - let event = PulseDomain.ValueHistory.Call {f= Model "std::basic_string::data()"; location} in + let event = + PulseDomain.ValueHistory.Call {f= Model "std::basic_string::data()"; location; in_call= []} + in match actuals with | [(this_hist, _)] -> to_internal_string location this_hist astate @@ -107,24 +107,15 @@ module StdBasicString = struct let destructor : model = fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> let model = PulseDomain.CallEvent.Model "std::basic_string::~basic_string()" in - let call_event = PulseDomain.ValueHistory.Call {f= model; location} in + let call_event = PulseDomain.ValueHistory.Call {f= model; location; in_call= []} in match actuals with | [(this_hist, _)] -> to_internal_string location this_hist astate - >>= fun (astate, string_addr_hist) -> - let invalidation = - PulseDomain.InterprocAction.ViaCall - { location - ; f= model - ; action= - ViaCall - { location - ; f= Model "deleting the underlying string" - ; action= Immediate {imm= PulseDomain.Invalidation.CppDelete; location} } } - in - PulseOperations.invalidate_deref location invalidation string_addr_hist astate + >>= fun (astate, (string_addr, string_hist)) -> + let string_addr_hist = (string_addr, call_event :: string_hist) in + PulseOperations.invalidate_deref location CppDelete string_addr_hist astate >>= fun astate -> - PulseOperations.invalidate location invalidation string_addr_hist astate + PulseOperations.invalidate location CppDelete string_addr_hist astate >>| fun astate -> [astate] | _ -> Ok [PulseOperations.havoc_id ret_id [call_event] astate] @@ -134,7 +125,9 @@ module StdFunction = struct let operator_call : model = fun ~caller_summary location ~ret ~actuals astate -> let havoc_ret (ret_id, _) astate = - let event = PulseDomain.ValueHistory.Call {f= Model "std::function::operator()"; location} in + let event = + PulseDomain.ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} + in [PulseOperations.havoc_id ret_id [event] astate] in match actuals with @@ -143,9 +136,7 @@ module StdFunction = struct | (lambda_ptr_hist, _) :: actuals -> ( PulseOperations.eval_access location lambda_ptr_hist Dereference astate >>= fun (astate, (lambda, _)) -> - PulseOperations.Closures.check_captured_addresses - (PulseDomain.InterprocAction.Immediate {imm= (); location}) - lambda astate + PulseOperations.Closures.check_captured_addresses location lambda astate >>= fun astate -> match PulseAbductiveDomain.Memory.get_closure_proc_name lambda astate with | None -> @@ -178,12 +169,8 @@ module StdVector = struct let reallocate_internal_array trace vector vector_f location astate = to_internal_array location vector astate >>= fun (astate, array_address) -> - let invalidation = - PulseDomain.InterprocAction.Immediate - {imm= PulseDomain.Invalidation.StdVector vector_f; location} - in - PulseOperations.invalidate_array_elements location invalidation array_address astate - >>= PulseOperations.invalidate_deref location invalidation array_address + PulseOperations.invalidate_array_elements location (StdVector vector_f) array_address astate + >>= PulseOperations.invalidate_deref location (StdVector vector_f) array_address >>= PulseOperations.havoc_field location vector internal_array trace @@ -196,7 +183,8 @@ module StdVector = struct { f= Model (Format.asprintf "%a()" PulseDomain.Invalidation.pp_std_vector_function vector_f) - ; location } + ; location + ; in_call= [] } in reallocate_internal_array [crumb] vector vector_f location astate >>| List.return | _ -> @@ -205,11 +193,14 @@ module StdVector = struct let at : model = fun ~caller_summary:_ location ~ret ~actuals astate -> - let event = PulseDomain.ValueHistory.Call {f= Model "std::vector::at()"; location} in + let event = + PulseDomain.ValueHistory.Call {f= Model "std::vector::at()"; location; in_call= []} + in match actuals with | [(vector, _); (index, _)] -> element_of_internal_array location vector (fst index) astate - >>| fun (astate, (addr, _)) -> [PulseOperations.write_id (fst ret) (addr, [event]) astate] + >>| fun (astate, (addr, hist)) -> + [PulseOperations.write_id (fst ret) (addr, event :: hist) astate] | _ -> Ok [PulseOperations.havoc_id (fst ret) [event] astate] @@ -218,7 +209,9 @@ module StdVector = struct fun ~caller_summary:_ location ~ret:_ ~actuals astate -> match actuals with | [(vector, _); _value] -> - let crumb = PulseDomain.ValueHistory.Call {f= Model "std::vector::reserve()"; location} in + let crumb = + PulseDomain.ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []} + in reallocate_internal_array [crumb] vector Reserve location astate >>| PulseAbductiveDomain.Memory.std_vector_reserve (fst vector) >>| List.return @@ -231,7 +224,7 @@ module StdVector = struct match actuals with | [(vector, _); _value] -> let crumb = - PulseDomain.ValueHistory.Call {f= Model "std::vector::push_back()"; location} + PulseDomain.ValueHistory.Call {f= Model "std::vector::push_back()"; location; in_call= []} 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 diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index c1b24e332..915abb454 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -9,7 +9,7 @@ module L = Logging module AbstractAddress = PulseDomain.AbstractAddress module Attribute = PulseDomain.Attribute module Attributes = PulseDomain.Attributes -module InterprocAction = PulseDomain.InterprocAction +module Trace = PulseDomain.Trace module ValueHistory = PulseDomain.ValueHistory module Memory = PulseAbductiveDomain.Memory module Stack = PulseAbductiveDomain.Stack @@ -28,10 +28,11 @@ 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 action (address, history) astate = - Memory.check_valid action address astate +let check_addr_access location (address, history) astate = + let accessed_by = Trace.Immediate {imm= (); location; history} in + Memory.check_valid accessed_by address astate |> Result.map_error ~f:(fun invalidated_by -> - PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= {action; history}} ) + PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by} ) module Closures = struct @@ -93,45 +94,43 @@ module Closures = struct let new_trace = ValueHistory.Capture {captured_as; location} :: trace_captured in Some (address_captured, new_trace) ) in - let closure_addr = AbstractAddress.mk_fresh () in + let closure_addr_hist = (AbstractAddress.mk_fresh (), [ValueHistory.Assignment location]) in let fake_capture_edges = mk_capture_edges captured_addresses in let astate = - Memory.set_cell closure_addr + Memory.set_cell closure_addr_hist (fake_capture_edges, Attributes.singleton (Closure pname)) location astate in - (astate, (closure_addr, (* TODO: trace *) [])) + (astate, closure_addr_hist) 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_access location addr_hist access astate = + check_addr_access location addr_hist astate + >>| fun astate -> Memory.eval_edge addr_hist 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) + Ok (eval_var (* error in case of missing history? *) [] (Var.of_id id) astate) | Lvar pvar -> - Ok (eval_var (Var.of_pvar pvar) astate) + Ok (eval_var [ValueHistory.VariableAccessed (pvar, location)] (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 + >>= fun (astate, addr_hist) -> + check_addr_access location addr_hist astate + >>| fun astate -> Memory.eval_edge addr_hist (FieldAccess field) astate | Lindex (exp', exp_index) -> eval exp_index astate - >>= fun (astate, addr_trace_index) -> + >>= fun (astate, addr_hist_index) -> eval exp' astate - >>= fun (astate, addr_trace) -> - check_addr_access action addr_trace astate + >>= fun (astate, addr_hist) -> + check_addr_access location addr_hist astate >>| fun astate -> - Memory.eval_edge (fst addr_trace) (ArrayAccess (Typ.void, fst addr_trace_index)) astate + Memory.eval_edge addr_hist (ArrayAccess (Typ.void, fst addr_hist_index)) astate | Closure {name; captured_vars} -> List.fold_result captured_vars ~init:(astate, []) ~f:(fun (astate, rev_captured) (capt_exp, captured_as, _) -> @@ -219,10 +218,9 @@ let assert_is_true location ~condition astate = eval_cond ~negated:false locatio 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 + >>= fun (astate, addr_hist) -> + check_addr_access location addr_hist astate + >>| fun astate -> Memory.eval_edge addr_hist Dereference astate let realloc_pvar pvar location astate = @@ -238,12 +236,9 @@ let havoc_id id loc_opt astate = else 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 location + check_addr_access location addr_trace_ref astate + >>| Memory.add_edge addr_trace_ref access addr_trace_obj location let write_deref location ~ref:addr_trace_ref ~obj:addr_trace_obj astate = @@ -263,18 +258,16 @@ let havoc_field location addr_trace field 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 + check_addr_access location addr_trace astate >>| Memory.invalidate addr_trace cause location -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_deref location cause ref_addr_hist astate = + let astate, (addr_obj, _) = Memory.eval_edge ref_addr_hist Dereference astate in + invalidate location cause (addr_obj, snd ref_addr_hist) astate let invalidate_array_elements location cause addr_trace astate = - let action = action_of_address location in - check_addr_access action addr_trace astate + check_addr_access location addr_trace astate >>| fun astate -> match Memory.find_opt (fst addr_trace) astate with | None -> @@ -284,15 +277,14 @@ let invalidate_array_elements location cause addr_trace astate = (fun access dest_addr_trace astate -> match (access : Memory.Access.t) with | ArrayAccess _ -> - Memory.invalidate dest_addr_trace cause astate + Memory.invalidate dest_addr_trace cause location astate | _ -> astate ) edges astate let shallow_copy location addr_hist astate = - let action = action_of_address location in - check_addr_access action addr_hist astate + check_addr_access location addr_hist astate >>| fun astate -> let cell = match Memory.find_opt (fst addr_hist) astate with @@ -301,7 +293,7 @@ let shallow_copy location addr_hist astate = | Some cell -> cell in - let copy = AbstractAddress.mk_fresh () in + let copy = (AbstractAddress.mk_fresh (), [ValueHistory.Assignment location]) in (Memory.set_cell copy cell location astate, copy) @@ -391,11 +383,11 @@ let call ~caller_summary call_loc callee_pname ~ret ~actuals astate = PulseAbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~actuals astate >>| fun (post, return_val_opt) -> - let event = ValueHistory.Call {f= Call callee_pname; location= call_loc} in + let event = ValueHistory.Call {f= Call callee_pname; location= call_loc; in_call= []} in let post = match return_val_opt with - | Some return_val -> - write_id (fst ret) (return_val, [event]) post + | Some (return_val, return_hist) -> + write_id (fst ret) (return_val, event :: return_hist) post | None -> havoc_id (fst ret) [event] post in @@ -403,5 +395,7 @@ let call ~caller_summary call_loc callee_pname ~ret ~actuals astate = | None -> (* no spec found for some reason (unknown function, ...) *) L.d_printfln "No spec found for %a@\n" Typ.Procname.pp callee_pname ; - let event = ValueHistory.Call {f= SkippedKnownCall callee_pname; location= call_loc} in + let event = + ValueHistory.Call {f= SkippedKnownCall callee_pname; location= call_loc; in_call= []} + in Ok [havoc_id (fst ret) [event] astate] diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 9719a77ff..344ca622b 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -14,7 +14,7 @@ type 'a access_result = ('a, PulseDiagnostic.t) result module Closures : sig val check_captured_addresses : - unit PulseDomain.InterprocAction.t -> AbstractAddress.t -> t -> (t, PulseDiagnostic.t) result + Location.t -> AbstractAddress.t -> t -> (t, PulseDiagnostic.t) result (** assert the validity of the addresses captured by the lambda *) end @@ -70,31 +70,22 @@ val write_deref : (** write the edge [ref --*--> obj] *) val invalidate : - Location.t - -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t - -> PulseDomain.AddrTracePair.t - -> t - -> t access_result + Location.t -> PulseDomain.Invalidation.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 + Location.t -> PulseDomain.Invalidation.t -> PulseDomain.AddrTracePair.t -> t -> t access_result (** record that what the address points to is invalid *) val invalidate_array_elements : - Location.t - -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t - -> PulseDomain.AddrTracePair.t - -> t - -> t access_result + Location.t -> PulseDomain.Invalidation.t -> PulseDomain.AddrTracePair.t -> t -> t access_result (** record that all the array elements that address points to is invalid *) val shallow_copy : - Location.t -> PulseDomain.AddrTracePair.t -> t -> (t * AbstractAddress.t) access_result + Location.t + -> PulseDomain.AddrTracePair.t + -> t + -> (t * (AbstractAddress.t * PulseDomain.ValueHistory.t)) access_result (** returns the address of a new cell with the same edges as the original *) val remove_vars : Var.t list -> Location.t -> t -> t diff --git a/infer/tests/codetoanalyze/cpp/impurity/issues.exp b/infer/tests/codetoanalyze/cpp/impurity/issues.exp index ad4243d46..9a5df05bc 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/issues.exp +++ b/infer/tests/codetoanalyze/cpp/impurity/issues.exp @@ -1,27 +1,27 @@ -../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter::operator++,parameter 'this' is modified at line 1390, column 9] -../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter::operator++,parameter 'this' is modified at line 1390, column 9] -codetoanalyze/cpp/impurity/array_test.cpp, alias_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function alias_mod_impure,parameter 'array' is modified at line 33, column 3] -codetoanalyze/cpp/impurity/array_test.cpp, array_mod_both_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_both_impure,parameter 'a' is modified at line 15, column 3,parameter 'a' is modified at line 16, column 3] -codetoanalyze/cpp/impurity/array_test.cpp, array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_impure,parameter 'b' is modified at line 10, column 3,parameter 'a' is modified at line 9, column 3] -codetoanalyze/cpp/impurity/array_test.cpp, call_array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function call_array_mod_impure,parameter 'a' is modified when calling `array_mod_impure()` at line 22, column 3,parameter 'a' is modified at line 9, column 3] -codetoanalyze/cpp/impurity/array_test.cpp, modify_direct_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_direct_impure,parameter 'array' is modified at line 40, column 60] -codetoanalyze/cpp/impurity/array_test.cpp, modify_ptr_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_ptr_impure,parameter 'array' is modified at line 44, column 3] -codetoanalyze/cpp/impurity/global_test.cpp, call_modify_global, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function call_modify_global,global variable 'a' is modified when calling `modify_global_array_impure()` at line 16, column 3,global variable 'a' is modified at line 12, column 37,global variable 'x' is modified when calling `modify_global_primitive_impure()` at line 15, column 3,global variable 'x' is modified at line 10, column 41] -codetoanalyze/cpp/impurity/global_test.cpp, local_static_var_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function local_static_var_impure,global variable 'local_static_var_impure.arr' is modified at line 26, column 3,global variable 'local_static_var_impure.arr' is modified at line 27, column 3] -codetoanalyze/cpp/impurity/global_test.cpp, modify_global_array_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_array_impure,global variable 'a' is modified at line 12, column 37] -codetoanalyze/cpp/impurity/global_test.cpp, modify_global_inside_lamda_impure::lambda_global_test.cpp:33:14::operator(), 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_inside_lamda_impure::lambda_global_test.cpp:33:14::operator(),global variable 'x' is modified at line 33, column 22] -codetoanalyze/cpp/impurity/global_test.cpp, modify_global_primitive_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_primitive_impure,global variable 'x' is modified at line 10, column 41] -codetoanalyze/cpp/impurity/invalid_test.cpp, delete_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function delete_param_impure,parameter 's',was invalidated by `delete` here] +../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter::operator++,parameter `this` of std::__wrap_iter::operator++,parameter `this` modified here] +../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter::operator++,parameter `this` of std::__wrap_iter::operator++,parameter `this` modified here] +codetoanalyze/cpp/impurity/array_test.cpp, alias_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function alias_mod_impure,parameter `array` of alias_mod_impure,assigned,parameter `array` modified here] +codetoanalyze/cpp/impurity/array_test.cpp, array_mod_both_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_both_impure,parameter `a` of array_mod_both_impure,parameter `a` modified here,parameter `a` of array_mod_both_impure,parameter `a` modified here] +codetoanalyze/cpp/impurity/array_test.cpp, array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_impure,parameter `b` of array_mod_impure,parameter `b` modified here,parameter `a` of array_mod_impure,parameter `a` modified here] +codetoanalyze/cpp/impurity/array_test.cpp, call_array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function call_array_mod_impure,parameter `a` of call_array_mod_impure,when calling `array_mod_impure` here,parameter `a` of array_mod_impure,parameter `a` modified here] +codetoanalyze/cpp/impurity/array_test.cpp, modify_direct_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_direct_impure,parameter `array` of modify_direct_impure,parameter `array` modified here] +codetoanalyze/cpp/impurity/array_test.cpp, modify_ptr_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_ptr_impure,parameter `array` of modify_ptr_impure,assigned,parameter `array` modified here] +codetoanalyze/cpp/impurity/global_test.cpp, call_modify_global, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function call_modify_global,global variable `a` accessed here,when calling `modify_global_array_impure` here,global variable `a` accessed here,global variable `a` modified here,global variable `x` accessed here,when calling `modify_global_primitive_impure` here,global variable `x` accessed here,global variable `x` modified here] +codetoanalyze/cpp/impurity/global_test.cpp, local_static_var_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function local_static_var_impure,global variable `local_static_var_impure.arr` accessed here,global variable `local_static_var_impure.arr` modified here,global variable `local_static_var_impure.arr` accessed here,global variable `local_static_var_impure.arr` modified here] +codetoanalyze/cpp/impurity/global_test.cpp, modify_global_array_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_array_impure,global variable `a` accessed here,global variable `a` modified here] +codetoanalyze/cpp/impurity/global_test.cpp, modify_global_inside_lamda_impure::lambda_global_test.cpp:33:14::operator(), 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_inside_lamda_impure::lambda_global_test.cpp:33:14::operator(),global variable `x` accessed here,global variable `x` modified here] +codetoanalyze/cpp/impurity/global_test.cpp, modify_global_primitive_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_primitive_impure,global variable `x` accessed here,global variable `x` modified here] +codetoanalyze/cpp/impurity/invalid_test.cpp, delete_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function delete_param_impure,parameter `s` of delete_param_impure,parameter `s` was invalidated by `delete` here] codetoanalyze/cpp/impurity/invalid_test.cpp, double_free_global_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function double_free_global_impure] -codetoanalyze/cpp/impurity/invalid_test.cpp, double_free_global_impure, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_global_pointer_impure` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,when calling `free_global_pointer_impure` here,invalid access occurs here] -codetoanalyze/cpp/impurity/invalid_test.cpp, free_global_pointer_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_global_pointer_impure,global variable 'global_pointer',was invalidated by call to `free()` here] -codetoanalyze/cpp/impurity/invalid_test.cpp, free_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_param_impure,parameter 'x',was invalidated by call to `free()` here] -codetoanalyze/cpp/impurity/invalid_test.cpp, reassign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function reassign_impure,parameter 's' is modified at line 34, column 3] -codetoanalyze/cpp/impurity/param_test.cpp, create_cycle_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function create_cycle_impure,parameter 'x' is modified at line 23, column 44] -codetoanalyze/cpp/impurity/param_test.cpp, invalidate_local_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function invalidate_local_impure,parameter 'pp' is modified at line 27, column 3] -codetoanalyze/cpp/impurity/param_test.cpp, modify_mut_ref_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_mut_ref_impure,parameter 'x' is modified at line 8, column 38] -codetoanalyze/cpp/impurity/vector.cpp, assign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function assign_impure,parameter 'vec' is modified at line 29, column 45] -codetoanalyze/cpp/impurity/vector.cpp, clear_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function clear_impure,parameter 'vec' is modified at line 26, column 44] -codetoanalyze/cpp/impurity/vector.cpp, insert_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function insert_impure,parameter 'vec' is modified at line 8, column 45] -codetoanalyze/cpp/impurity/vector.cpp, push_back_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_impure,parameter 'vec' is modified at line 10, column 48] -codetoanalyze/cpp/impurity/vector.cpp, push_back_in_loop_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_in_loop_impure,parameter 'vec' is modified at line 21, column 5] +codetoanalyze/cpp/impurity/invalid_test.cpp, double_free_global_impure, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_impure` here,global variable `global_pointer` accessed here,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_impure` here,global variable `global_pointer` accessed here,invalid access occurs here] +codetoanalyze/cpp/impurity/invalid_test.cpp, free_global_pointer_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_global_pointer_impure,global variable `global_pointer` accessed here,global variable `global_pointer` was invalidated by call to `free()` here] +codetoanalyze/cpp/impurity/invalid_test.cpp, free_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_param_impure,parameter `x` of free_param_impure,parameter `x` was invalidated by call to `free()` here] +codetoanalyze/cpp/impurity/invalid_test.cpp, reassign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function reassign_impure,parameter `s` of reassign_impure,parameter `s` modified here] +codetoanalyze/cpp/impurity/param_test.cpp, create_cycle_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function create_cycle_impure,parameter `x` of create_cycle_impure,parameter `x` modified here] +codetoanalyze/cpp/impurity/param_test.cpp, invalidate_local_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function invalidate_local_impure,parameter `pp` of invalidate_local_impure,parameter `pp` modified here] +codetoanalyze/cpp/impurity/param_test.cpp, modify_mut_ref_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_mut_ref_impure,parameter `x` of modify_mut_ref_impure,parameter `x` modified here] +codetoanalyze/cpp/impurity/vector.cpp, assign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function assign_impure,parameter `vec` of assign_impure,parameter `vec` modified here] +codetoanalyze/cpp/impurity/vector.cpp, clear_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function clear_impure,parameter `vec` of clear_impure,parameter `vec` modified here] +codetoanalyze/cpp/impurity/vector.cpp, insert_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function insert_impure,parameter `vec` of insert_impure,parameter `vec` modified here] +codetoanalyze/cpp/impurity/vector.cpp, push_back_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_impure,parameter `vec` of push_back_impure,parameter `vec` modified here] +codetoanalyze/cpp/impurity/vector.cpp, push_back_in_loop_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_in_loop_impure,parameter `vec` of push_back_in_loop_impure,parameter `vec` modified here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp b/infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp new file mode 100644 index 000000000..93d5ddde6 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp @@ -0,0 +1,98 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#include + +// Caricature of folly::basic_fbstring without the union between small +// and medium/large data representations, and with an explicit field +// for category_ instead of bitmasking part of the data value. +// ref: +// https://github.com/facebook/folly/blob/72850c2ebfb94d87bea74d89fcf79f3aaa91a627/folly/FBString.h + +enum category { + small = 0, // ignore small strings for now + medium = 1, + large = 2, +}; + +void* checkedMalloc(size_t size) { + void* ptr = malloc(size); + if (ptr == nullptr) { + exit(1); + } + return ptr; +} + +struct LikeFBString { + int category_; + char* buffer_; + size_t size_; + unsigned int refcount; + + LikeFBString() {} + + LikeFBString(const LikeFBString& src) { + category_ = src.category(); + switch (src.category_) { + case medium: + copyMedium(src); + break; + case large: + copyLarge(src); + break; + default: + exit(2); + } + } + + ~LikeFBString() { + if (category() == medium) { + free(buffer_); + } else { + decr_ref_count(); + } + } + + void copySmall(const LikeFBString& src) {} + + void copyMedium(const LikeFBString& src) { + buffer_ = (char*)checkedMalloc(src.size_); + size_ = src.size_; + } + + void copyLarge(const LikeFBString& src) { + refcount++; + buffer_ = src.buffer_; + size_ = src.size_; + } + + int category() const { return category_; } + + void incr_ref_count() { refcount++; } + + void decr_ref_count() { + refcount--; + if (refcount == 0) { + free(buffer_); + } + } +}; + +void copy_fbstring(LikeFBString& s) { + // this might alias the underlying buffers if the string is large in + // that case the destruction of t does not de-allocate its buffer + // but pulse might think it does if it fails to remember which + // category t belongs to and follows impossibly control flow + LikeFBString t = s; +} + +void FP_pass_to_copy_ok() { + // Currently pulse follows impossible control flow and thinks the + // underlying buffer of s is freed twice: once per copy. That is + // caused by manual ref-counting in the case of large strings. + LikeFBString s; + copy_fbstring(s); +} diff --git a/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp b/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp index 4fbff9995..0c5710580 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp @@ -100,8 +100,14 @@ void invalidate_and_set_to_null(struct X** x_ptr) { *x_ptr = nullptr; } -void access_to_invalidated_alias(struct X* x, struct X* y) { +void access_to_invalidated_alias_bad(struct X* x, struct X* y) { y = x; invalidate_and_set_to_null(&x); wraps_read(*y); } + +void access_to_invalidated_alias2_bad(struct X* x, struct X* y) { + y = x; + invalidate_and_set_to_null(&y); + wraps_read(*x); +} diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index f529bf564..e5f751807 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,64 +1,67 @@ -codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `setLanguage` here,when calling `std::basic_string::~basic_string()` (modelled) here,when calling `deleting the underlying string` (modelled) here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `Range::operator[]` here,invalid access occurs 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] -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] -codetoanalyze/cpp/pulse/closures.cpp, call_lambda_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 `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,invalid access occurs here] -codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here] -codetoanalyze/cpp/pulse/closures.cpp, reassign_lambda_capture_destroy_invoke_bad, 9, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here] -codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,memory is the address of a stack variable `s` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here] -codetoanalyze/cpp/pulse/conditionals.cpp, FP_unreachable_ne_then_eq_ok, 5, 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] -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 `deduplication::SomeTemplatedClass::templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `deduplication::SomeTemplatedClass::templated_wrapper_access_ok` here,invalid access occurs 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 `deduplication::SomeTemplatedClass::templated_wrapper_delete_ok` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `deduplication::SomeTemplatedClass::templated_wrapper_access_ok` here,invalid access occurs 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<_Bool>` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function<_Bool>` here,invalid access occurs 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] -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] -codetoanalyze/cpp/pulse/frontend.cpp, deref_null_namespace_alias_ptr_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,when calling `some::thing::bad_ptr` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `some::thing::bad_ptr`,assigned,invalid access occurs here] -codetoanalyze/cpp/pulse/interprocedural.cpp, access_to_invalidated_alias, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `invalidate_and_set_to_null` here,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] -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] -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] -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] -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] -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 `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,when calling `store` here,invalid access occurs 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] -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::~WrapsB` here,when calling `WrapsB::__infer_inner_destructor_~WrapsB` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `WrapsB::getb`,assigned,returned from call to `ReferenceWrapperHeap::ReferenceWrapperHeap`,returned from call to `getwrapperHeap`,invalid access occurs 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 `b` declared 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,assigned,returned from call to `ReferenceWrapperStack::ReferenceWrapperStack`,returned from call to `getwrapperStack`,invalid access occurs here] +codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,when calling `setLanguage` here,variable `C++ temporary` declared here,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `s` declared here,passed as argument to `setLanguage`,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],invalid access occurs here] +codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,invalid access occurs here] +codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,invalid access occurs here] +codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,parameter `s` of call_lambda_bad::lambda_closures.cpp:163:12::operator(),invalid access occurs here] +codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here] +codetoanalyze/cpp/pulse/closures.cpp, reassign_lambda_capture_destroy_invoke_bad, 9, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here] +codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,is the address of a stack variable `s` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `s` declared here,value captured as `s`,invalid access occurs here] +codetoanalyze/cpp/pulse/conditionals.cpp, FP_unreachable_ne_then_eq_ok, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of FP_unreachable_ne_then_eq_ok,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_unreachable_ne_then_eq_ok,invalid access occurs 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,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass::templated_wrapper_access_ok,invalid access occurs 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,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_delete_ok` here,parameter `a` of deduplication::SomeTemplatedClass::templated_wrapper_delete_ok,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `a` of deduplication::SomeTemplatedClass::lifetime_error_bad,when calling `deduplication::SomeTemplatedClass::templated_wrapper_access_ok` here,parameter `a` of deduplication::SomeTemplatedClass::templated_wrapper_access_ok,invalid access occurs 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,when calling `deduplication::templated_delete_function<_Bool>` here,parameter `a` of deduplication::templated_delete_function<_Bool>,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function<_Bool>` here,parameter `a` of deduplication::templated_access_function<_Bool>,invalid access occurs 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,when calling `deduplication::templated_delete_function` here,parameter `a` of deduplication::templated_delete_function,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function` here,parameter `a` of deduplication::templated_access_function,invalid access occurs here] +codetoanalyze/cpp/pulse/fbstring.cpp, FP_pass_to_copy_ok, 6, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,when calling `copy_fbstring` here,parameter `s` of copy_fbstring,passed as argument to `LikeFBString::LikeFBString`,parameter `src` of LikeFBString::LikeFBString,passed as argument to `LikeFBString::copyLarge`,parameter `src` of LikeFBString::copyLarge,assigned,return from call to `LikeFBString::copyLarge`,return from call to `LikeFBString::LikeFBString`,when calling `LikeFBString::~LikeFBString` here,parameter `this` of LikeFBString::~LikeFBString,when calling `LikeFBString::__infer_inner_destructor_~LikeFBString` here,parameter `this` of LikeFBString::__infer_inner_destructor_~LikeFBString,when calling `LikeFBString::decr_ref_count` here,parameter `this` of LikeFBString::decr_ref_count,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `LikeFBString::~LikeFBString` here,parameter `this` of LikeFBString::~LikeFBString,when calling `LikeFBString::__infer_inner_destructor_~LikeFBString` here,parameter `this` of LikeFBString::__infer_inner_destructor_~LikeFBString,invalid access occurs 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,parameter `this` of UsingDelayedDestruction::double_delete_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `this` of UsingDelayedDestruction::double_delete_bad,invalid access occurs here] +codetoanalyze/cpp/pulse/frontend.cpp, deref_null_namespace_alias_ptr_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `some::thing::bad_ptr` here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `some::thing::bad_ptr`,return from call to `some::thing::bad_ptr`,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/interprocedural.cpp, access_to_invalidated_alias2_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of access_to_invalidated_alias2_bad,assigned,when calling `invalidate_and_set_to_null` here,parameter `x_ptr` of invalidate_and_set_to_null,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of access_to_invalidated_alias2_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here] +codetoanalyze/cpp/pulse/interprocedural.cpp, access_to_invalidated_alias_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of access_to_invalidated_alias_bad,when calling `invalidate_and_set_to_null` here,parameter `x_ptr` of invalidate_and_set_to_null,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of access_to_invalidated_alias_bad,assigned,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs 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,parameter `x` of delete_aliased_then_read_bad,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_aliased_then_read_bad,assigned,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs 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,parameter `x` of delete_inner_then_write_bad,when calling `wraps_delete_inner` here,parameter `x` of wraps_delete_inner,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_inner_then_write_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here] +codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_read_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_read_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here] +codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_delete` here,parameter `x` of wraps_delete,when calling `wraps_delete_inner` here,parameter `x` of wraps_delete_inner,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs 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,when calling `may_return_invalid_ptr_ok` here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `may_return_invalid_ptr_ok`,return from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,parameter `y` of call_store,when calling `store` here,parameter `y` of store,invalid access occurs here] +codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_bad,assigned,assigned,assigned,invalid access occurs 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,variable `rw` declared here,when calling `getwrapperHeap` here,variable `a` declared here,passed as argument to `WrapsB::WrapsB`,assigned,return from call to `WrapsB::WrapsB`,when calling `WrapsB::~WrapsB` here,parameter `this` of WrapsB::~WrapsB,when calling `WrapsB::__infer_inner_destructor_~WrapsB` here,parameter `this` of WrapsB::__infer_inner_destructor_~WrapsB,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `rw` declared here,passed as argument to `getwrapperHeap`,variable `a` declared here,passed as argument to `WrapsB::WrapsB`,assigned,return from call to `WrapsB::WrapsB`,passed as argument to `ReferenceWrapperHeap::ReferenceWrapperHeap`,parameter `a` of ReferenceWrapperHeap::ReferenceWrapperHeap,passed as argument to `WrapsB::getb`,return from call to `WrapsB::getb`,assigned,return from call to `ReferenceWrapperHeap::ReferenceWrapperHeap`,return from call to `getwrapperHeap`,invalid access occurs 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 `rw` declared here,when calling `getwrapperStack` here,variable `b` declared here,is the address of a stack variable `b` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `rw` declared here,passed as argument to `getwrapperStack`,variable `b` declared here,passed as argument to `ReferenceWrapperStack::ReferenceWrapperStack`,parameter `bref` of ReferenceWrapperStack::ReferenceWrapperStack,assigned,return from call to `ReferenceWrapperStack::ReferenceWrapperStack`,return from call to `getwrapperStack`,invalid access occurs here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,returned here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `x` declared here,returned here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 2, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,assigned,returned here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 3, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, [variable `C++ temporary` declared here,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 `temporaries::UniquePtr::~UniquePtr` here,when calling `temporaries::UniquePtr::__infer_inner_destructor_~UniquePtr` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,returned from call to `temporaries::UniquePtr::get`,assigned,invalid access occurs 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] -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] -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::Simple` here,invalid access occurs 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] -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] -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::Simple` here,invalid access occurs 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] -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 `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs 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 `()` (modelled),assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,invalid access occurs 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 `()` (modelled),assigned,invalid access occurs 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] -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 `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs 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 `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__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 `use_after_destructor::S::operator=`,invalid access occurs 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 `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__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 `use_after_destructor::S::S`,invalid access occurs 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 `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs 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 `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,variable `s` declared here,when calling `use_after_destructor::S::~S` here,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,invalid access occurs 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 `c` declared here,memory is the address of a stack variable `c` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable `c` declared here,assigned,invalid access occurs 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] -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] -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] -codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `t` declared here,when calling `invalidate_local_ok` here,memory is the address of a stack variable `t` whose lifetime has ended here,use-after-lifetime part of the trace starts here,variable `t` declared here,assigned,returned from call to `invalidate_local_ok`,invalid access occurs here] -codetoanalyze/cpp/pulse/values.cpp, FP_infeasible_tricky_ok, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_if` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here] -codetoanalyze/cpp/pulse/values.cpp, FP_no_free_if_ok, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_if` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here] -codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, 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] -codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `free_if` here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs 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()` (modelled),assigned,invalid access occurs 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()` (modelled),assigned,invalid access occurs 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()` (modelled),assigned,invalid access occurs 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()` (modelled),assigned,invalid access occurs 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()` (modelled),assigned,assigned,invalid access occurs 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()` (modelled),assigned,invalid access occurs 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()` (modelled),assigned,invalid access occurs 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()` (modelled),assigned,invalid access occurs 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()` (modelled),assigned,invalid access occurs 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()` (modelled),assigned,invalid access occurs 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()` (modelled),assigned,invalid access occurs 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,variable `C++ temporary` declared here,passed as argument to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr::UniquePtr`,parameter `y` of temporaries::UniquePtr::UniquePtr,assigned,return from call to `temporaries::UniquePtr::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,when calling `temporaries::UniquePtr::~UniquePtr` here,parameter `this` of temporaries::UniquePtr::~UniquePtr,when calling `temporaries::UniquePtr::__infer_inner_destructor_~UniquePtr` here,parameter `this` of temporaries::UniquePtr::__infer_inner_destructor_~UniquePtr,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr::UniquePtr`,parameter `y` of temporaries::UniquePtr::UniquePtr,assigned,return from call to `temporaries::UniquePtr::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr::get`,return from call to `temporaries::UniquePtr::get`,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/trace.cpp, trace_free_bad, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of trace_free_bad,passed as argument to `make_alias`,parameter `src` of make_alias,assigned,return from call to `make_alias`,when calling `do_free` here,parameter `x` of do_free,assigned,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of trace_free_bad,invalid access occurs 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,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,invalid access occurs 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,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,invalid access occurs 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,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs 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,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,invalid access occurs 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,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,invalid access occurs 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,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs 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,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,invalid access occurs 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,variable `s` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `s` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,invalid access occurs 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,assigned,passed as argument to `()` (modelled),return from call to `()` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,invalid access occurs 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,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,passed as argument to `()` (modelled),return from call to `()` (modelled),assigned,invalid access occurs 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,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,assigned,invalid access occurs 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,variable `s2` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `s2` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,passed as argument to `use_after_destructor::S::operator=`,parameter `__param_0` of use_after_destructor::S::operator=,assigned,return from call to `use_after_destructor::S::operator=`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,invalid access occurs 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,variable `C++ temporary` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,passed as argument to `use_after_destructor::S::operator=`,parameter `__param_0` of use_after_destructor::S::operator=,assigned,return from call to `use_after_destructor::S::operator=`,invalid access occurs 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,variable `s` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `s` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,invalid access occurs 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,variable `tmp` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `tmp` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,passed as argument to `use_after_destructor::S::operator=`,parameter `__param_0` of use_after_destructor::S::operator=,assigned,return from call to `use_after_destructor::S::operator=`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,invalid access occurs 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,variable `C++ temporary` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `C++ temporary` declared here,passed as argument to `use_after_destructor::S::S`,assigned,return from call to `use_after_destructor::S::S`,passed as argument to `use_after_destructor::S::operator=`,parameter `__param_0` of use_after_destructor::S::operator=,assigned,return from call to `use_after_destructor::S::operator=`,when calling `use_after_destructor::S::~S` here,parameter `this` of use_after_destructor::S::~S,when calling `use_after_destructor::S::__infer_inner_destructor_~S` here,parameter `this` of use_after_destructor::S::__infer_inner_destructor_~S,invalid access occurs 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 `c` declared here,is the address of a stack variable `c` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `c` declared here,assigned,invalid access occurs 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,global variable `global_pointer` accessed here,when calling `free_global_pointer_ok` here,global variable `global_pointer` accessed here,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_ok` here,global variable `global_pointer` accessed here,invalid access occurs 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,parameter `x` of double_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of double_free_simple_bad,invalid access occurs 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,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here] +codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `p` declared here,when calling `invalidate_local_ok` here,variable `t` declared here,is the address of a stack variable `t` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `p` declared here,passed as argument to `invalidate_local_ok`,variable `t` declared here,assigned,return from call to `invalidate_local_ok`,invalid access occurs here] +codetoanalyze/cpp/pulse/values.cpp, FP_infeasible_tricky_ok, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of FP_infeasible_tricky_ok,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_infeasible_tricky_ok,invalid access occurs here] +codetoanalyze/cpp/pulse/values.cpp, FP_no_free_if_ok, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of FP_no_free_if_ok,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of FP_no_free_if_ok,invalid access occurs here] +codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,invalid access occurs here] +codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of free_if_deref_bad,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of free_if_deref_bad,invalid access occurs 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,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of assign_bad,was potentially invalidated by `std::vector::assign()`,use-after-lifetime part of the trace starts here,parameter `vec` of assign_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of clear_bad,was potentially invalidated by `std::vector::clear()`,use-after-lifetime part of the trace starts here,parameter `vec` of clear_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs 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,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs 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,parameter `vec` of deref_vector_element_after_push_back_bad,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of deref_vector_element_after_push_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of emplace_back_bad,was potentially invalidated by `std::vector::emplace_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of emplace_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,parameter `vec` of emplace_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of insert_bad,was potentially invalidated by `std::vector::insert()`,use-after-lifetime part of the trace starts here,parameter `vec` of insert_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of reserve_bad,was potentially invalidated by `std::vector::reserve()`,use-after-lifetime part of the trace starts here,parameter `vec` of reserve_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of shrink_to_fit_bad,was potentially invalidated by `std::vector::shrink_to_fit()`,use-after-lifetime part of the trace starts here,parameter `vec` of shrink_to_fit_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/trace.cpp b/infer/tests/codetoanalyze/cpp/pulse/trace.cpp new file mode 100644 index 000000000..5db4ec6cb --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/trace.cpp @@ -0,0 +1,22 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +#include + +void make_alias(int** src, int** dst) { *dst = *src; } + +void do_free(int* x) { + int* y = x; + int* z = y; + free(y); +} + +void trace_free_bad(int* x) { + int* y; + make_alias(&x, &y); + do_free(y); + int i = *x; +} diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index 10a59609a..1591496de 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -1,20 +1,20 @@ -codetoanalyze/java/impurity/GlobalTest.java, GlobalTest$Foo.set_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest$Foo.set_impure(),global variable 'GlobalTest' is modified at line 16] -codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.call_set_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.call_set_impure(),global variable 'GlobalTest' is modified when calling `GlobalTest$Foo.set_impure()` at line 27,global variable 'GlobalTest' is modified at line 16] -codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.global_mod_via_argument_passing_impure(int,GlobalTest$Foo):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.global_mod_via_argument_passing_impure(int,GlobalTest$Foo),global variable 'GlobalTest' is modified when calling `GlobalTest.incr(...)` at line 33,global variable 'GlobalTest' is modified at line 21] -codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.global_mod_via_argument_passing_impure_aliased(int,GlobalTest$Foo):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.global_mod_via_argument_passing_impure_aliased(int,GlobalTest$Foo),global variable 'GlobalTest' is modified when calling `GlobalTest.incr(...)` at line 42,global variable 'GlobalTest' is modified at line 21] -codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.incr(GlobalTest$Foo,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.incr(GlobalTest$Foo,int),parameter 'foo' is modified at line 21] -codetoanalyze/java/impurity/Localities.java, Localities$Counter.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Counter.inc_impure(),parameter 'this' is modified at line 67] -codetoanalyze/java/impurity/Localities.java, Localities$Foo.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Foo.inc_impure(),parameter 'this' is modified at line 57] -codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_impure(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_impure(int[],int),parameter 'a' is modified at line 150] -codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_pure_FP(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_pure_FP(int[],int),parameter 'a' is modified at line 142] -codetoanalyze/java/impurity/Localities.java, Localities.get_array_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo[], 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),parameter 'array' is modified at line 125] -codetoanalyze/java/impurity/Localities.java, Localities.get_f_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),parameter 'array' is modified at line 118] -codetoanalyze/java/impurity/Localities.java, Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo):Localities$Bar, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),parameter 'array' is modified at line 134,parameter 'array' is modified at line 132] -codetoanalyze/java/impurity/Test.java, Test.Test(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.Test(int),global variable 'Test' is modified at line 15] -codetoanalyze/java/impurity/Test.java, Test.alias_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.alias_impure(int[],int,int),parameter 'array' is modified at line 77] -codetoanalyze/java/impurity/Test.java, Test.call_impure_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.call_impure_impure(int),parameter 'this' is modified when calling `Test.set_impure(...)` at line 41,parameter 'this' is modified at line 19] -codetoanalyze/java/impurity/Test.java, Test.global_array_set_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.global_array_set_impure(int,int),global variable 'Test' is modified at line 23] -codetoanalyze/java/impurity/Test.java, Test.local_field_write_impure(Test):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.local_field_write_impure(Test),parameter 'x' is modified at line 66] -codetoanalyze/java/impurity/Test.java, Test.parameter_field_write_impure(Test,boolean):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.parameter_field_write_impure(Test,boolean),parameter 'test' is modified at line 56] -codetoanalyze/java/impurity/Test.java, Test.set_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.set_impure(int,int),parameter 'this' is modified at line 19] -codetoanalyze/java/impurity/Test.java, Test.swap_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.swap_impure(int[],int,int),parameter 'array' is modified at line 71,parameter 'array' is modified at line 71,parameter 'array' is modified at line 72,parameter 'array' is modified at line 71] +codetoanalyze/java/impurity/GlobalTest.java, GlobalTest$Foo.set_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest$Foo.set_impure(),global variable `GlobalTest` accessed here,global variable `GlobalTest` modified here] +codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.call_set_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.call_set_impure(),global variable `GlobalTest` accessed here,when calling `void GlobalTest$Foo.set_impure()` here,global variable `GlobalTest` accessed here,global variable `GlobalTest` modified here] +codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.global_mod_via_argument_passing_impure(int,GlobalTest$Foo):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.global_mod_via_argument_passing_impure(int,GlobalTest$Foo),global variable `GlobalTest` accessed here,when calling `void GlobalTest.incr(GlobalTest$Foo,int)` here,parameter `foo` of void GlobalTest.incr(GlobalTest$Foo,int),global variable `GlobalTest` modified here] +codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.global_mod_via_argument_passing_impure_aliased(int,GlobalTest$Foo):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.global_mod_via_argument_passing_impure_aliased(int,GlobalTest$Foo),global variable `GlobalTest` accessed here,assigned,when calling `void GlobalTest.incr(GlobalTest$Foo,int)` here,parameter `foo` of void GlobalTest.incr(GlobalTest$Foo,int),global variable `GlobalTest` modified here] +codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.incr(GlobalTest$Foo,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.incr(GlobalTest$Foo,int),parameter `foo` of void GlobalTest.incr(GlobalTest$Foo,int),parameter `foo` modified here] +codetoanalyze/java/impurity/Localities.java, Localities$Counter.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Counter.inc_impure(),parameter `this` of void Localities$Counter.inc_impure(),parameter `this` modified here] +codetoanalyze/java/impurity/Localities.java, Localities$Foo.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Foo.inc_impure(),parameter `this` of void Localities$Foo.inc_impure(),parameter `this` modified here] +codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_impure(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_impure(int[],int),parameter `a` of boolean Localities.copy_ref_impure(int[],int),parameter `a` modified here] +codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_pure_FP(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_pure_FP(int[],int),parameter `a` of boolean Localities.copy_ref_pure_FP(int[],int),parameter `a` modified here] +codetoanalyze/java/impurity/Localities.java, Localities.get_array_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo[], 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),parameter `array` of Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),assigned,parameter `array` modified here] +codetoanalyze/java/impurity/Localities.java, Localities.get_f_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),parameter `array` of Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),assigned,parameter `array` modified here] +codetoanalyze/java/impurity/Localities.java, Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo):Localities$Bar, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),parameter `array` of Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),assigned,parameter `array` modified here,parameter `array` of Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),assigned,parameter `array` modified here] +codetoanalyze/java/impurity/Test.java, Test.Test(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.Test(int),global variable `Test` accessed here,global variable `Test` modified here] +codetoanalyze/java/impurity/Test.java, Test.alias_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.alias_impure(int[],int,int),parameter `array` of void Test.alias_impure(int[],int,int),assigned,parameter `array` modified here] +codetoanalyze/java/impurity/Test.java, Test.call_impure_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.call_impure_impure(int),parameter `this` of void Test.call_impure_impure(int),when calling `void Test.set_impure(int,int)` here,parameter `this` of void Test.set_impure(int,int),parameter `this` modified here] +codetoanalyze/java/impurity/Test.java, Test.global_array_set_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.global_array_set_impure(int,int),global variable `Test` accessed here,assigned,global variable `Test` modified here] +codetoanalyze/java/impurity/Test.java, Test.local_field_write_impure(Test):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.local_field_write_impure(Test),parameter `x` of void Test.local_field_write_impure(Test),assigned,parameter `x` modified here] +codetoanalyze/java/impurity/Test.java, Test.parameter_field_write_impure(Test,boolean):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.parameter_field_write_impure(Test,boolean),parameter `test` of void Test.parameter_field_write_impure(Test,boolean),parameter `test` modified here] +codetoanalyze/java/impurity/Test.java, Test.set_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.set_impure(int,int),parameter `this` of void Test.set_impure(int,int),parameter `this` modified here] +codetoanalyze/java/impurity/Test.java, Test.swap_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.swap_impure(int[],int,int),parameter `array` of void Test.swap_impure(int[],int,int),parameter `array` modified here,parameter `array` of void Test.swap_impure(int[],int,int),parameter `array` modified here,parameter `array` of void Test.swap_impure(int[],int,int),parameter `array` modified here] diff --git a/infer/tests/codetoanalyze/objc/pulse/issues.exp b/infer/tests/codetoanalyze/objc/pulse/issues.exp index 02b17e870..3acec4e7a 100644 --- a/infer/tests/codetoanalyze/objc/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objc/pulse/issues.exp @@ -1,2 +1,2 @@ -codetoanalyze/objc/pulse/use_after_free.m, PulseTest::use_after_free_simple_in_objc_method_bad:, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here] -codetoanalyze/objc/pulse/use_after_free.m, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by call to `free()` here,use-after-lifetime part of the trace starts here,invalid access occurs here] +codetoanalyze/objc/pulse/use_after_free.m, PulseTest::use_after_free_simple_in_objc_method_bad:, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of PulseTest::use_after_free_simple_in_objc_method_bad:,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of PulseTest::use_after_free_simple_in_objc_method_bad:,invalid access occurs here] +codetoanalyze/objc/pulse/use_after_free.m, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp index 675be8a89..76d89f920 100644 --- a/infer/tests/codetoanalyze/objcpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objcpp/pulse/issues.exp @@ -1,2 +1,2 @@ -codetoanalyze/objcpp/pulse/use_after_delete.mm, PulseTest::deref_deleted_in_objc_method_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::Simple` here,invalid access occurs here] -codetoanalyze/objcpp/pulse/use_after_delete.mm, 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::Simple` here,invalid access occurs here] +codetoanalyze/objcpp/pulse/use_after_delete.mm, PulseTest::deref_deleted_in_objc_method_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here] +codetoanalyze/objcpp/pulse/use_after_delete.mm, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]