[pulse][interproc 3/3] interproc call

Summary: biggest_diff

Reviewed By: jberdine

Differential Revision: D14387150

fbshipit-source-id: 6d6ddeffc

infer/src/IR/HilExp.mli

@@ -54,6 +54,8 @@ module AccessExpression : sig
     [@@warning "-32"]
   (** address_of doesn't always make sense, eg [address_of (Dereference t)] is [None] *)
 
+  val address_of_base : AccessPath.base -> access_expression
+
   val to_accesses_fold :
        access_expression
     -> init:'accum

infer/src/IR/Var.ml

@@ -40,8 +40,6 @@ let is_global = function ProgramVar pvar -> Pvar.is_global pvar | LogicalVar _ -
 
 let is_return = function ProgramVar pvar -> Pvar.is_return pvar | LogicalVar _ -> false
 
-let is_this = function ProgramVar pvar -> Pvar.is_this pvar | LogicalVar _ -> false
-
 let is_footprint = function ProgramVar _ -> false | LogicalVar id -> Ident.is_footprint id
 
 let is_none = function LogicalVar id -> Ident.is_none id | _ -> false

infer/src/IR/Var.mli

@@ -37,9 +37,6 @@ val is_local_to_procedure : Typ.Procname.t -> t -> bool
 
 val is_return : t -> bool
 
-val is_this : t -> bool
-(** return whether the var is the special "this" var *)
-
 val is_footprint : t -> bool
 
 val is_none : t -> bool

infer/src/backend/Payloads.ml

@@ -17,6 +17,7 @@ type t =
   ; cost: CostDomain.summary option
   ; lab_resource_leaks: ResourceLeakDomain.summary option
   ; litho: LithoDomain.t option
+  ; pulse: PulseSummary.t option
   ; purity: PurityDomain.summary option
   ; quandary: QuandarySummary.t option
   ; racerd: RacerDDomain.summary option
@@ -34,6 +35,7 @@ let pp pe fmt
     ; cost
     ; lab_resource_leaks
     ; litho
+    ; pulse
     ; purity
     ; quandary
     ; racerd
@@ -47,7 +49,7 @@ let pp pe fmt
     | None ->
         ()
   in
-  F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a%a%a%a%a@\n"
+  F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a%a%a%a%a%a@\n"
     (pp_opt "AnnotationReachability" AnnotReachabilityDomain.pp)
     annot_map
     (pp_opt "Biabduction" (BiabductionSummary.pp pe))
@@ -59,7 +61,7 @@ let pp pe fmt
     (pp_opt "ClassLoads" ClassLoadsDomain.pp_summary)
     class_loads
     (pp_opt "Cost" CostDomain.pp_summary)
-    cost (pp_opt "Litho" LithoDomain.pp) litho
+    cost (pp_opt "Litho" LithoDomain.pp) litho (pp_opt "Pulse" PulseSummary.pp) pulse
     (pp_opt "Purity" PurityDomain.pp_summary)
     purity
     (pp_opt "Quandary" QuandarySummary.pp)
@@ -85,6 +87,7 @@ let empty =
   ; cost= None
   ; lab_resource_leaks= None
   ; litho= None
+  ; pulse= None
   ; purity= None
   ; quandary= None
   ; racerd= None

infer/src/backend/Payloads.mli

@@ -17,6 +17,7 @@ type t =
   ; cost: CostDomain.summary option
   ; lab_resource_leaks: ResourceLeakDomain.summary option
   ; litho: LithoDomain.t option
+  ; pulse: PulseSummary.t option
   ; purity: PurityDomain.summary option
   ; quandary: QuandarySummary.t option
   ; racerd: RacerDDomain.summary option

infer/src/istd/IList.ml

@@ -194,3 +194,8 @@ let pp_print_list ~max ?(pp_sep = Format.pp_print_cut) pp_v ppf =
           aux (n + 1) rest )
   in
   function [] -> () | [v] -> pp_v ppf v | v :: rest -> pp_v ppf v ; aux 1 rest
+
+
+let fold2_result ~init ~f l1 l2 =
+  List.fold2 l1 l2 ~init:(Ok init) ~f:(fun result x1 x2 ->
+      Result.bind result ~f:(fun acc -> f acc x1 x2) )

infer/src/istd/IList.mli

@@ -53,3 +53,10 @@ val pp_print_list :
   -> Format.formatter
   -> 'a list
   -> unit
+
+val fold2_result :
+     init:'acc
+  -> f:('acc -> 'a -> 'b -> ('acc, 'err) result)
+  -> 'a list
+  -> 'b list
+  -> ('acc, 'err) result Base.List.Or_unequal_lengths.t

infer/src/istd/Pp.ml

@@ -173,3 +173,5 @@ let cli_args fmt args =
 
 
 let pair ~fst ~snd fmt (a, b) = F.fprintf fmt "(%a,@,%a)" fst a snd b
+
+let in_backticks pp fmt x = F.fprintf fmt "`%a`" pp x

infer/src/istd/Pp.mli

@@ -100,3 +100,5 @@ val pair :
   -> F.formatter
   -> 'a * 'b
   -> unit
+
+val in_backticks : (F.formatter -> 'a -> unit) -> F.formatter -> 'a -> unit

infer/src/istd/PrettyPrintable.ml

@@ -119,6 +119,8 @@ end
 module type PPMap = sig
   include Caml.Map.S
 
+  val fold_map : 'a t -> init:'b -> f:('b -> 'a -> 'b * 'c) -> 'b * 'c t
+
   val is_singleton_or_more : 'a t -> (key * 'a) IContainer.singleton_or_more
 
   val pp_key : F.formatter -> key -> unit
@@ -147,6 +149,19 @@ end
 module MakePPMap (Ord : PrintableOrderedType) = struct
   include Caml.Map.Make (Ord)
 
+  let fold_map m ~init ~f =
+    let acc = ref init in
+    let new_map =
+      map
+        (fun value ->
+          let acc', res = f !acc value in
+          acc := acc' ;
+          res )
+        m
+    in
+    (!acc, new_map)
+
+
   let is_singleton_or_more m =
     if is_empty m then IContainer.Empty
     else

infer/src/istd/PrettyPrintable.mli

@@ -121,6 +121,8 @@ end
 module type PPMap = sig
   include Caml.Map.S
 
+  val fold_map : 'a t -> init:'b -> f:('b -> 'a -> 'b * 'c) -> 'b * 'c t
+
   val is_singleton_or_more : 'a t -> (key * 'a) IContainer.singleton_or_more
 
   val pp_key : F.formatter -> key -> unit

infer/src/pulse/Pulse.ml

@@ -37,6 +37,14 @@ let check_error summary = function
       raise_notrace AbstractDomain.Stop_analysis
 
 
+module Payload = SummaryPayload.Make (struct
+  type t = PulseSummary.t
+
+  let update_payloads astate (payloads : Payloads.t) = {payloads with pulse= Some astate}
+
+  let of_payloads (payloads : Payloads.t) = payloads.pulse
+end)
+
 module PulseTransferFunctions = struct
   module CFG = ProcCfg.Exceptional
   module Domain = PulseAbductiveDomain
@@ -80,25 +88,13 @@ module PulseTransferFunctions = struct
         >>= PulseOperations.havoc [crumb] loc lhs_access
 
 
-  let exec_call summary _ret (call : HilInstr.call) (actuals : HilExp.t list) _flags call_loc
-      astate =
+  let exec_unknown_call summary _ret (call : HilInstr.call) (actuals : HilExp.t list) _flags
+      call_loc astate =
     let read_all args astate =
       PulseOperations.read_all call_loc (List.concat_map args ~f:HilExp.get_access_exprs) astate
     in
     let crumb = PulseTrace.Call {f= `HilCall call; actuals; location= call_loc} in
     match call with
-    | Direct callee_pname when is_destructor callee_pname -> (
-      match actuals with
-      | [AccessExpression (Base (destroyed_var, _))] when Var.is_this destroyed_var ->
-          (* do not invalidate [this] when it is destroyed by calls to [this->~Obj()] *)
-          Ok astate
-      | [AccessExpression destroyed_access] ->
-          let destroyed_object = HilExp.AccessExpression.dereference destroyed_access in
-          PulseOperations.invalidate
-            (CppDestructor (callee_pname, destroyed_object, call_loc))
-            call_loc destroyed_object astate
-      | _ ->
-          Ok astate )
     | Direct callee_pname when Typ.Procname.is_constructor callee_pname -> (
         L.d_printfln "constructor call detected@." ;
         match actuals with
@@ -129,6 +125,54 @@ module PulseTransferFunctions = struct
         read_all actuals astate
 
 
+  let interprocedural_call caller_summary ret (call : HilInstr.call) (actuals : HilExp.t list)
+      flags call_loc astate =
+    let unknown_function () =
+      exec_unknown_call caller_summary ret call actuals flags call_loc astate >>| List.return
+    in
+    match call with
+    | Direct callee_pname -> (
+      match Payload.read_full caller_summary.Summary.proc_desc callee_pname with
+      | Some (callee_proc_desc, preposts) ->
+          let formals =
+            Procdesc.get_formals callee_proc_desc
+            |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar)
+          in
+          PulseOperations.Interproc.call callee_pname ~formals ~ret ~actuals flags call_loc astate
+            preposts
+      | None ->
+          (* no spec found for some reason (unknown function, ...) *)
+          L.d_printfln "No spec found for %a@\n" Typ.Procname.pp callee_pname ;
+          unknown_function () )
+    | Indirect access_expression ->
+        L.d_printfln "Indirect call %a@\n" HilExp.AccessExpression.pp access_expression ;
+        unknown_function ()
+
+
+  (** has an object just gone out of scope? *)
+  let get_destructed_object (call : HilInstr.call) (actuals : HilExp.t list) (flags : CallFlags.t)
+      =
+    (* injected destructors are precisely inserted where an object goes out of scope *)
+    if flags.cf_injected_destructor then
+      match (call, actuals) with
+      | Direct callee_pname, [AccessExpression destroyed_access] when is_destructor callee_pname ->
+          Some (callee_pname, destroyed_access)
+      | _ ->
+          None
+    else None
+
+
+  (** [destroyed_access_expr] has just gone out of scope and in now invalid *)
+  let destruct_object callee_pname call_loc destroyed_access_expr astate =
+    let destroyed_object = HilExp.AccessExpression.dereference destroyed_access_expr in
+    (* TODO: need an [OutOfScope] invalidation reason instead of [CppDestructor]? *)
+    PulseOperations.invalidate
+      (PulseTrace.Immediate
+         { imm= PulseInvalidation.CppDestructor (callee_pname, destroyed_object, call_loc)
+         ; location= call_loc })
+      call_loc destroyed_object astate
+
+
   let dispatch_call summary ret (call : HilInstr.call) (actuals : HilExp.t list) flags call_loc
       astate =
     let model =
@@ -140,13 +184,23 @@ module PulseTransferFunctions = struct
           PulseModels.dispatch callee_pname flags
     in
     match model with
-    | None ->
-        exec_call summary ret call actuals flags call_loc astate
-        >>| PulseOperations.havoc_var
-              [PulseTrace.Call {f= `HilCall call; actuals; location= call_loc}]
-              (fst ret)
     | Some model ->
-        model call_loc ~ret ~actuals astate
+        model call_loc ~ret ~actuals astate >>| fun post -> [post]
+    | None -> (
+        (* do interprocedural call then destroy objects going out of scope *)
+        PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ;
+        let posts = interprocedural_call summary ret call actuals flags call_loc astate in
+        PerfEvent.(log (fun logger -> log_end_event logger ())) ;
+        match get_destructed_object call actuals flags with
+        | Some (destructor_pname, access_expr) ->
+            L.d_printfln "%a is going out of scope" HilExp.AccessExpression.pp access_expr ;
+            posts
+            >>= fun posts ->
+            List.map posts ~f:(fun astate ->
+                destruct_object destructor_pname call_loc access_expr astate )
+            |> Result.all
+        | None ->
+            posts )
 
 
   let exec_instr (astate : Domain.t) {ProcData.extras= summary} _cfg_node (instr : HilInstr.t) =
@@ -161,10 +215,10 @@ module PulseTransferFunctions = struct
         in
         [post]
     | Call (ret, call, actuals, flags, loc) ->
-        let post =
+        let posts =
           dispatch_call summary ret call actuals flags loc astate |> check_error summary
         in
-        [post]
+        posts
     | Metadata (ExitScope (vars, _)) ->
         let post = PulseOperations.remove_vars vars astate in
         [post]
@@ -202,9 +256,15 @@ module DisjunctiveAnalyzer =
 let checker {Callbacks.proc_desc; tenv; summary} =
   let proc_data = ProcData.make proc_desc tenv summary in
   AbstractAddress.init () ;
-  ( try
-      ignore
-        (DisjunctiveAnalyzer.compute_post proc_data
-           ~initial:(DisjunctiveTransferFunctions.Disjuncts.singleton PulseAbductiveDomain.empty))
-    with AbstractDomain.Stop_analysis -> () ) ;
-  summary
+  match
+    DisjunctiveAnalyzer.compute_post proc_data
+      ~initial:(DisjunctiveTransferFunctions.Disjuncts.singleton PulseAbductiveDomain.empty)
+  with
+  | Some posts ->
+      Payload.update_summary
+        (PulseSummary.of_posts (DisjunctiveTransferFunctions.Disjuncts.elements posts))
+        summary
+  | None ->
+      summary
+  | exception AbstractDomain.Stop_analysis ->
+      summary

infer/src/pulse/PulseAbductiveDomain.ml

@@ -6,6 +6,7 @@
  *)
 open! IStd
 module F = Format
+module L = Logging
 module AbstractAddress = PulseDomain.AbstractAddress
 module Attributes = PulseDomain.Attributes
 module BaseStack = PulseDomain.Stack
@@ -140,20 +141,20 @@ 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 actor address (pre : InvertedDomain.t) =
+  let record_must_be_valid action address (pre : InvertedDomain.t) =
     if BaseMemory.mem_edges address (pre :> base_domain).heap then
       InvertedDomain.update pre
         ~heap:
           (BaseMemory.add_attributes address
-             (Attributes.singleton (MustBeValid actor))
+             (Attributes.singleton (MustBeValid action))
              (pre :> base_domain).heap)
     else pre
 
 
-  let check_valid actor addr ({post; pre} as astate) =
+  let check_valid action addr ({post; pre} as astate) =
     BaseMemory.check_valid addr (post :> base_domain).heap
     >>| fun () ->
-    let new_pre = record_must_be_valid actor addr pre in
+    let new_pre = record_must_be_valid action addr pre in
     if phys_equal new_pre pre then astate else {astate with pre= new_pre}
 
 
@@ -188,8 +189,8 @@ module Memory = struct
         , addr_trace' )
 
 
-  let invalidate address actor astate =
-    map_post_heap astate ~f:(fun heap -> BaseMemory.invalidate address actor heap)
+  let invalidate address action astate =
+    map_post_heap astate ~f:(fun heap -> BaseMemory.invalidate address action heap)
 
 
   let add_attributes address attributes astate =
@@ -235,3 +236,396 @@ let discard_unreachable ({pre; post} as astate) =
   else
     { pre= InvertedDomain.make (pre :> PulseDomain.t).stack pre_new_heap
     ; post= Domain.make (post :> PulseDomain.t).stack post_new_heap }
+
+
+module PrePost = struct
+  type domain_t = t
+
+  type t = domain_t
+
+  let of_post astate = discard_unreachable astate
+
+  (* machinery to apply a pre/post pair corresponding to a function's summary in a function call to
+     the current state *)
+
+  module AddressSet = PulseDomain.AbstractAddressSet
+  module AddressMap = PulseDomain.AbstractAddressMap
+
+  (** raised when the pre/post pair and the current state disagree on the aliasing, i.e. some
+     addresses that are distinct in the pre/post are aliased in the current state. Typically raised
+     when calling [foo(z,z)] where the spec for [foo(x,y)] says that [x] and [y] are disjoint. *)
+  exception Aliasing
+
+  (** 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 *)
+    ; rev_subst: AbstractAddress.t AddressMap.t
+          (** the inverse translation from [subst] from caller addresses to callee addresses *)
+    ; visited: AddressSet.t
+          (** set of callee addresses that have been visited already
+
+               NOTE: this is not always equal to the domain of [rev_subst]: when applying the post
+               we visit each subgraph from each formal independently so we reset [visited] between
+              the visit of each formal *)
+    }
+
+  let pp_call_state fmt {astate; subst; rev_subst; visited} =
+    F.fprintf fmt
+      "@[<v>{ astate=@[<hv2>%a@];@, subst=@[<hv2>%a@];@, rev_subst=@[<hv2>%a@];@, \
+       visited=@[<hv2>%a@]@, }@]"
+      pp astate
+      (AddressMap.pp ~pp_value:AbstractAddress.pp)
+      subst
+      (AddressMap.pp ~pp_value:AbstractAddress.pp)
+      rev_subst AddressSet.pp visited
+
+
+  let visit call_state ~addr_callee ~addr_caller =
+    ( 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"
+          AbstractAddress.pp addr_caller AbstractAddress.pp addr_callee' AbstractAddress.pp
+          addr_callee pp_call_state call_state ;
+        raise Aliasing
+    | _ ->
+        () ) ;
+    if AddressSet.mem addr_callee call_state.visited then (`AlreadyVisited, call_state)
+    else
+      ( `NotAlreadyVisited
+      , { call_state with
+          visited= AddressSet.add addr_callee call_state.visited
+        ; subst= AddressMap.add addr_callee addr_caller call_state.subst
+        ; rev_subst= AddressMap.add addr_caller addr_callee call_state.rev_subst } )
+
+
+  let pp f {pre; post} =
+    F.fprintf f "PRE:@\n  @[%a@]@\n" PulseDomain.pp (pre :> PulseDomain.t) ;
+    F.fprintf f "POST:@\n  @[%a@]@\n" PulseDomain.pp (post :> PulseDomain.t)
+
+
+  (* reading the pre from the current state *)
+
+  (** 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
+      trace call_state =
+    let mk_action action =
+      PulseTrace.ViaCall {action; proc_name= callee_proc_name; location= call_location}
+    in
+    match visit call_state ~addr_callee:addr_pre ~addr_caller with
+    | `AlreadyVisited, call_state ->
+        Ok call_state
+    | `NotAlreadyVisited, call_state -> (
+        (let open Option.Monad_infix in
+        PulseDomain.Memory.find_opt addr_pre pre.PulseDomain.heap
+        >>= fun (edges_pre, attrs_pre) ->
+        PulseDomain.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
+        | Error invalidated_by ->
+            Error
+              (PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= action; 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.materialize_edge addr_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 trace call_state ))
+        |> function Some result -> result | None -> Ok call_state )
+
+
+  (** materialize subgraph of [pre] rooted at the address represented by a [formal] parameter that
+      has been instantiated with the corresponding [actual] into the current state
+      [call_state.astate] *)
+  let materialize_pre_from_actual callee_proc_name call_location ~pre ~formal ~actual call_state =
+    L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal (Pp.option AbstractAddress.pp)
+      (Option.map ~f:fst actual) ;
+    match actual with
+    | None ->
+        (* the expression representing the actual couldn't be evaluated down to an abstract address
+           *)
+        Ok call_state
+    | Some (addr_caller, trace) -> (
+        (let open Option.Monad_infix in
+        PulseDomain.Stack.find_opt formal pre.PulseDomain.stack
+        >>= fun (addr_formal_pre, _) ->
+        PulseDomain.Memory.find_edge_opt addr_formal_pre Dereference pre.PulseDomain.heap
+        >>| fun (formal_pre, _) ->
+        materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre:formal_pre
+          ~addr_caller trace call_state)
+        |> function Some result -> result | None -> Ok call_state )
+
+
+  let is_cell_read_only ~cell_pre_opt ~cell_post:(edges_post, attrs_post) =
+    match cell_pre_opt with
+    | None ->
+        false
+    | Some (edges_pre, _) ->
+        Attributes.is_empty attrs_post
+        && PulseDomain.Memory.Edges.equal
+             (fun (addr_dest_pre, _) (addr_dest_post, _) ->
+               (* NOTE: ignores traces
+
+                  TODO: can the traces be leveraged here? maybe easy to detect writes by looking at
+                  the post trace *)
+               AbstractAddress.equal addr_dest_pre addr_dest_post )
+             edges_pre edges_post
+
+
+  let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state =
+    (* For each [(formal, actual)] pair, resolve them to addresses in their respective states then
+       call [materialize_pre_from] on them.  Give up if calling the function introduces aliasing.
+       *)
+    match
+      PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call pre" ())) ;
+      let r =
+        IList.fold2_result formals actuals ~init:call_state ~f:(fun call_state formal actual ->
+            materialize_pre_from_actual callee_proc_name call_location
+              ~pre:(pre_post.pre :> PulseDomain.t)
+              ~formal ~actual call_state )
+      in
+      PerfEvent.(log (fun logger -> log_end_event logger ())) ;
+      r
+    with
+    | Ok result ->
+        Some result
+    | Unequal_lengths ->
+        L.d_printfln "ERROR: formals have length %d but actuals have length %d"
+          (List.length formals) (List.length actuals) ;
+        None
+    | exception Aliasing ->
+        (* can't make sense of the pre-condition in the current context: give up on that particular
+           pre/post pair *)
+        None
+
+
+  (* applying the post to the current state *)
+
+  let subst_find_or_new subst addr_callee =
+    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 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 delete_edges_in_callee_pre_from_caller ~addr_callee:_ ~cell_pre_opt ~addr_caller call_state =
+    match
+      PulseDomain.Memory.find_edges_opt addr_caller (call_state.astate.post :> base_domain).heap
+    with
+    | None ->
+        PulseDomain.Memory.Edges.empty
+    | Some old_post_edges -> (
+      match cell_pre_opt with
+      | None ->
+          old_post_edges
+      | Some (edges_pre, _) ->
+          PulseDomain.Memory.Edges.merge
+            (fun _access old_opt pre_opt ->
+              (* TODO: should apply [call_state.subst] to [_access]! Actually, should rewrite the
+                whole [cell_pre] beforehand so that [Edges.merge] makes sense. *)
+              if Option.is_some pre_opt then
+                (* delete edge if some edge for the same access exists in the pre *)
+                None
+              else (* keep old edge if it exists *) old_opt )
+            old_post_edges edges_pre )
+
+
+  let add_call_to_attr proc_name location attr =
+    match (attr : PulseDomain.Attribute.t) with
+    | Invalid action ->
+        PulseDomain.Attribute.Invalid (PulseTrace.ViaCall {action; proc_name; location})
+    | MustBeValid _ | AddressOfCppTemporary (_, _) | Closure _ | StdVectorReserve ->
+        attr
+
+
+  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@\n" AbstractAddress.pp addr_callee AbstractAddress.pp addr_caller ;
+    match visit call_state ~addr_callee ~addr_caller with
+    | `AlreadyVisited, call_state ->
+        call_state
+    | `NotAlreadyVisited, call_state -> (
+      match PulseDomain.Memory.find_opt addr_callee (post :> PulseDomain.t).PulseDomain.heap with
+      | None ->
+          call_state
+      | Some ((edges_post, _attrs_post) as cell_post) ->
+          let cell_pre_opt =
+            PulseDomain.Memory.find_opt addr_callee (pre :> PulseDomain.t).PulseDomain.heap
+          in
+          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
+          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 =
+                call_state_subst_find_or_new call_state addr_callee_dest
+              in
+              record_post_for_address callee_proc_name call_loc pre_post
+                ~addr_callee:addr_callee_dest ~addr_caller:addr_curr_dest call_state ) )
+
+
+  and record_post_cell callee_proc_name call_loc ~addr_callee ~cell_pre_opt
+      ~cell_post:(edges_post, attrs_post) ~addr_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 new_attrs =
+      let attrs_post = Attributes.map (add_call_to_attr callee_proc_name call_loc) attrs_post in
+      match
+        PulseDomain.Memory.find_attrs_opt addr_caller (call_state.astate.post :> base_domain).heap
+      with
+      | None ->
+          attrs_post
+      | Some old_attrs_post ->
+          Attributes.union old_attrs_post attrs_post
+    in
+    let subst, translated_post_edges =
+      PulseDomain.Memory.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
+          ( subst
+          , ( addr_curr
+            , PulseTrace.Call
+                {f= `HilCall (Direct callee_proc_name); actuals= [ (* TODO *) ]; location= call_loc}
+              :: trace_post ) ) )
+    in
+    let caller_post =
+      let new_edges =
+        PulseDomain.Memory.Edges.union
+          (fun _ _ post_cell -> Some post_cell)
+          post_edges_minus_pre translated_post_edges
+      in
+      Domain.make (call_state.astate.post :> base_domain).stack
+        (PulseDomain.Memory.set_cell addr_caller (new_edges, new_attrs)
+           (call_state.astate.post :> base_domain).heap)
+    in
+    {call_state with subst; astate= {call_state.astate with post= caller_post}}
+
+
+  let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual call_state =
+    L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal
+      (Pp.option AbstractAddress.pp) (Option.map ~f:fst actual) ;
+    match actual with
+    | None ->
+        call_state
+    | Some (addr_caller, _trace) -> (
+        let open Option.Monad_infix in
+        match
+          PulseDomain.Stack.find_opt formal (pre_post.pre :> PulseDomain.t).PulseDomain.stack
+          >>= fun (addr_formal_pre, _) ->
+          PulseDomain.Memory.find_edge_opt addr_formal_pre Dereference
+            (pre_post.pre :> PulseDomain.t).PulseDomain.heap
+          >>| fun (formal_pre, _) ->
+          record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:formal_pre
+            ~addr_caller call_state
+        with
+        | Some call_state ->
+            call_state
+        | None ->
+            call_state )
+
+
+  let record_post_for_return callee_proc_name call_loc pre_post ~ret call_state =
+    let return_var = Var.of_pvar (Pvar.get_ret_pvar callee_proc_name) in
+    match
+      PulseDomain.Stack.find_opt return_var (pre_post.pre :> PulseDomain.t).PulseDomain.stack
+    with
+    | Some (addr_return, _) ->
+        record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:addr_return
+          ~addr_caller:(fst ret) call_state
+    | None ->
+        call_state
+
+
+  let apply_post callee_proc_name call_location pre_post ~formals ~ret ~actuals call_state =
+    (* reset [visited] *)
+    let call_state_pre = {call_state with visited= AddressSet.empty} in
+    (* for each [(formal_i, actual_i)] pair, do [post_i = post union subst(graph reachable from
+       formal_i in post)], deleting previous info when comparing pre and post shows a difference
+       (TODO: record in the pre when a location is written to instead of just comparing values
+       between pre and post since it's unreliable, eg replace value read in pre with same value in
+       post but nuke other fields in the meantime? is that possible?).  *)
+    match
+      PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ;
+      let r =
+        List.fold2 formals actuals ~init:call_state_pre ~f:(fun call_state formal actual ->
+            record_post_for_actual callee_proc_name call_location pre_post ~formal ~actual
+              call_state )
+      in
+      PerfEvent.(log (fun logger -> log_end_event logger ())) ;
+      r
+    with
+    | Ok call_state ->
+        record_post_for_return callee_proc_name call_location pre_post ~ret call_state
+        |> fun {astate} -> Some astate
+    | exception Aliasing ->
+        None
+    | Unequal_lengths ->
+        (* should have been checked before by [materialize_pre] *)
+        assert false
+
+
+  (* - read all the pre, assert validity of addresses and materializes *everything* (to throw stuff
+       in the *current* pre as appropriate so that callers of the current procedure will also know
+       about the deeper reads)
+
+     - for each actual, write the post for that actual
+
+     - if aliasing is introduced at any time then give up
+
+     questions:
+
+     - what if some preconditions raise lifetime issues but others don't? Have to be careful with
+     the noise that this will introduce since we don't care about values. For instance, if the pre
+     is for a path where [formal != 0] and we pass [0] then it will be an FP. Maybe the solution is
+     to bake in some value analysis.  *)
+  let apply callee_proc_name call_location pre_post ~formals ~ret ~actuals astate =
+    L.d_printfln "Applying pre/post for %a(%a):@\n%a" Typ.Procname.pp callee_proc_name
+      (Pp.seq ~sep:"," Var.pp) formals pp pre_post ;
+    let empty_call_state =
+      {astate; subst= AddressMap.empty; rev_subst= AddressMap.empty; visited= AddressSet.empty}
+    in
+    (* read the precondition *)
+    match
+      materialize_pre callee_proc_name call_location pre_post ~formals ~actuals empty_call_state
+    with
+    | None ->
+        (* couldn't apply the pre for some technical reason (as in: not by the fault of the
+           programmer as far as we know) *)
+        Ok astate
+    | Some (Error _ as error) ->
+        (* error: the function call requires to read some state known to be invalid *)
+        error
+    | Some (Ok call_state) -> (
+      (* apply the postcondition *)
+      match
+        apply_post callee_proc_name call_location pre_post ~formals ~ret ~actuals call_state
+      with
+      | None ->
+          (* same as when trying to apply the pre: give up for that pre/post pair and return the
+             original state *)
+          Ok astate
+      | Some astate_post ->
+          Ok astate_post )
+end

infer/src/pulse/PulseAbductiveDomain.mli

@@ -46,13 +46,16 @@ module Memory : sig
     AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t
 
   val check_valid :
-    PulseDiagnostic.actor -> AbstractAddress.t -> t -> (t, PulseInvalidation.t) result
+       HilExp.AccessExpression.t PulseTrace.action
+    -> AbstractAddress.t
+    -> t
+    -> (t, PulseInvalidation.t PulseTrace.action) result
 
   val find_opt : AbstractAddress.t -> t -> PulseDomain.Memory.cell option
 
   val set_cell : AbstractAddress.t -> PulseDomain.Memory.cell -> t -> t
 
-  val invalidate : AbstractAddress.t -> PulseInvalidation.t -> t -> t
+  val invalidate : AbstractAddress.t -> PulseInvalidation.t PulseTrace.action -> t -> t
 
   val is_std_vector_reserved : AbstractAddress.t -> t -> bool
 
@@ -61,6 +64,26 @@ module Memory : sig
   val materialize_edge : AbstractAddress.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t
 end
 
+module PrePost : sig
+  type domain_t = t
+
+  type t = private domain_t
+
+  val pp : Format.formatter -> t -> unit
+
+  val of_post : domain_t -> t
+
+  val apply :
+       Typ.Procname.t
+    -> Location.t
+    -> t
+    -> formals:Var.t list
+    -> ret:AbstractAddress.t * PulseTrace.t
+    -> actuals:(AbstractAddress.t * PulseTrace.t) option list
+    -> domain_t
+    -> (domain_t, PulseDiagnostic.t) result
+end
+
 val discard_unreachable : t -> t
 (** garbage collect unreachable addresses in the state to make it smaller, just for convenience and
-   keep its size down *)
+    keep its size down *)

infer/src/pulse/PulseDiagnostic.ml

@@ -8,25 +8,28 @@
 open! IStd
 module F = Format
 
-type actor = {access_expr: HilExp.AccessExpression.t; location: Location.t} [@@deriving compare]
-
 type t =
   | AccessToInvalidAddress of
-      { invalidated_by: PulseInvalidation.t
-      ; accessed_by: actor
+      { invalidated_by: PulseInvalidation.t PulseTrace.action
+      ; accessed_by: HilExp.AccessExpression.t PulseTrace.action
       ; trace: PulseTrace.t }
   | StackVariableAddressEscape of {variable: Var.t; location: Location.t}
 
+let pp_access = PulseTrace.pp_action HilExp.AccessExpression.pp
+
+let pp_invalidation = PulseTrace.pp_action PulseInvalidation.pp
+
 let get_location = function
-  | AccessToInvalidAddress {accessed_by= {location}} | StackVariableAddressEscape {location} ->
+  | AccessToInvalidAddress {accessed_by} ->
+      PulseTrace.outer_location_of_action accessed_by
+  | StackVariableAddressEscape {location} ->
       location
 
 
 let get_message = function
   | AccessToInvalidAddress {accessed_by; invalidated_by; trace} ->
-      F.asprintf "`%a` accesses address %a%a past its lifetime" HilExp.AccessExpression.pp
-        accessed_by.access_expr PulseTrace.pp_interesting_events trace PulseInvalidation.pp
-        invalidated_by
+      F.asprintf "%a accesses address %a%a past its lifetime" pp_access accessed_by
+        PulseTrace.pp_interesting_events trace pp_invalidation invalidated_by
   | StackVariableAddressEscape {variable} ->
       let pp_var f var =
         if Var.is_cpp_temporary var then F.pp_print_string f "C++ temporary"
@@ -37,25 +40,17 @@ let get_message = function
 
 let get_trace = function
   | AccessToInvalidAddress {accessed_by; invalidated_by; trace} ->
-      let invalidated_by_trace =
-        PulseInvalidation.get_location invalidated_by
-        |> Option.map ~f:(fun location ->
-               Errlog.make_trace_element 0 location
-                 (F.asprintf "%a here" PulseInvalidation.pp invalidated_by)
-                 [] )
-        |> Option.to_list
-      in
       PulseTrace.make_errlog_trace ~depth:0 trace
-      @ invalidated_by_trace
-      @ [ Errlog.make_trace_element 0 accessed_by.location
-            (F.asprintf "accessed `%a` here" HilExp.AccessExpression.pp accessed_by.access_expr)
-            [] ]
+      @ PulseTrace.trace_of_action ~action_name:"invalidated" PulseInvalidation.pp invalidated_by
+      @ PulseTrace.trace_of_action ~action_name:"accessed"
+          (Pp.in_backticks HilExp.AccessExpression.pp)
+          accessed_by
   | StackVariableAddressEscape _ ->
       []
 
 
 let get_issue_type = function
   | AccessToInvalidAddress {invalidated_by} ->
-      PulseInvalidation.issue_type_of_cause invalidated_by
+      PulseTrace.immediate_of_action invalidated_by |> PulseInvalidation.issue_type_of_cause
   | StackVariableAddressEscape _ ->
       IssueType.stack_variable_address_escape

infer/src/pulse/PulseDiagnostic.mli

@@ -7,12 +7,10 @@
 
 open! IStd
 
-type actor = {access_expr: HilExp.AccessExpression.t; location: Location.t} [@@deriving compare]
-
 type t =
   | AccessToInvalidAddress of
-      { invalidated_by: PulseInvalidation.t
-      ; accessed_by: actor
+      { invalidated_by: PulseInvalidation.t PulseTrace.action
+      ; accessed_by: HilExp.AccessExpression.t PulseTrace.action
       ; trace: PulseTrace.t }
   | StackVariableAddressEscape of {variable: Var.t; location: Location.t}
 

infer/src/pulse/PulseDomain.ml

@@ -19,8 +19,8 @@ module Attribute = struct
        address is invalid) *)
   type t =
     (* DO NOT MOVE, see toplevel comment *)
-    | Invalid of Invalidation.t
-    | MustBeValid of PulseDiagnostic.actor
+    | Invalid of Invalidation.t PulseTrace.action
+    | MustBeValid of HilExp.AccessExpression.t PulseTrace.action
     | AddressOfCppTemporary of Var.t * Location.t option
     | Closure of Typ.Procname.t
     | StdVectorReserve
@@ -28,10 +28,12 @@ module Attribute = struct
 
   let pp f = function
     | Invalid invalidation ->
-        Invalidation.pp f invalidation
-    | MustBeValid actor ->
-        F.fprintf f "MustBeValid (read by %a @ %a)" HilExp.AccessExpression.pp actor.access_expr
-          Location.pp actor.location
+        (PulseTrace.pp_action Invalidation.pp) f invalidation
+    | MustBeValid action ->
+        F.fprintf f "MustBeValid (read by %a @ %a)"
+          (PulseTrace.pp_action HilExp.AccessExpression.pp)
+          action Location.pp
+          (PulseTrace.outer_location_of_action action)
     | AddressOfCppTemporary (var, location_opt) ->
         F.fprintf f "&%a (%a)" Var.pp var (Pp.option Location.pp) location_opt
     | Closure pname ->
@@ -48,6 +50,13 @@ module Attributes = struct
        [Invalid _] attributes are the smallest we can simply look at the first element to decide if
        an address is invalid or not. *)
     match min_elt_opt attrs with Some (Invalid invalidation) -> Some invalidation | _ -> None
+
+
+  let get_must_be_valid attrs =
+    find_first_opt (function MustBeValid _ -> true | _ -> false) attrs
+    |> Option.map ~f:(fun attr ->
+           let[@warning "-8"] (Attribute.MustBeValid action) = attr in
+           action )
 end
 
 (** An abstract address in memory. *)
@@ -91,6 +100,7 @@ end = struct
 end
 
 module AbstractAddressSet = PrettyPrintable.MakePPSet (AbstractAddress)
+module AbstractAddressMap = PrettyPrintable.MakePPMap (AbstractAddress)
 
 (* {3 Heap domain } *)
 
@@ -126,6 +136,10 @@ module Memory : sig
 
   val set_cell : AbstractAddress.t -> cell -> t -> t
 
+  val find_attrs_opt : AbstractAddress.t -> t -> Attributes.t option
+
+  val find_edges_opt : AbstractAddress.t -> t -> edges option
+
   val mem_edges : AbstractAddress.t -> t -> bool
 
   val pp : F.formatter -> t -> unit
@@ -140,9 +154,9 @@ module Memory : sig
 
   val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t
 
-  val invalidate : AbstractAddress.t -> Invalidation.t -> t -> t
+  val invalidate : AbstractAddress.t -> Invalidation.t PulseTrace.action -> t -> t
 
-  val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t) result
+  val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t PulseTrace.action) result
 
   val std_vector_reserve : AbstractAddress.t -> t -> t
 
@@ -245,8 +259,12 @@ end = struct
 
   let empty = (Graph.empty, Graph.empty)
 
+  let find_edges_opt addr memory = Graph.find_opt addr (fst memory)
+
+  let find_attrs_opt addr memory = Graph.find_opt addr (snd memory)
+
   let find_opt addr memory =
-    match (Graph.find_opt addr (fst memory), Graph.find_opt addr (snd memory)) with
+    match (find_edges_opt addr memory, find_attrs_opt addr memory) with
     | None, None ->
         None
     | edges_opt, attrs_opt ->

infer/src/pulse/PulseDomain.mli

@@ -10,15 +10,19 @@ module F = Format
 
 module Attribute : sig
   type t =
-    | Invalid of PulseInvalidation.t
-    | MustBeValid of PulseDiagnostic.actor
+    | Invalid of PulseInvalidation.t PulseTrace.action
+    | MustBeValid of HilExp.AccessExpression.t PulseTrace.action
     | AddressOfCppTemporary of Var.t * Location.t option
     | Closure of Typ.Procname.t
     | StdVectorReserve
   [@@deriving compare]
 end
 
-module Attributes : PrettyPrintable.PPSet with type elt = Attribute.t
+module Attributes : sig
+  include PrettyPrintable.PPSet with type elt = Attribute.t
+
+  val get_must_be_valid : t -> HilExp.AccessExpression.t PulseTrace.action option
+end
 
 module AbstractAddress : sig
   type t = private int [@@deriving compare]
@@ -40,6 +44,8 @@ end
 
 module AbstractAddressSet : PrettyPrintable.PPSet with type elt = AbstractAddress.t
 
+module AbstractAddressMap : PrettyPrintable.PPMap with type key = AbstractAddress.t
+
 module Stack : sig
   include
     PrettyPrintable.MonoMap
@@ -73,6 +79,10 @@ module Memory : sig
 
   val set_cell : AbstractAddress.t -> cell -> t -> t
 
+  val find_attrs_opt : AbstractAddress.t -> t -> Attributes.t option
+
+  val find_edges_opt : AbstractAddress.t -> t -> edges option
+
   val mem_edges : AbstractAddress.t -> t -> bool
 
   val register_address : AbstractAddress.t -> t -> t
@@ -85,9 +95,9 @@ module Memory : sig
 
   val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t
 
-  val invalidate : AbstractAddress.t -> PulseInvalidation.t -> t -> t
+  val invalidate : AbstractAddress.t -> PulseInvalidation.t PulseTrace.action -> t -> t
 
-  val check_valid : AbstractAddress.t -> t -> (unit, PulseInvalidation.t) result
+  val check_valid : AbstractAddress.t -> t -> (unit, PulseInvalidation.t PulseTrace.action) result
 
   val std_vector_reserve : AbstractAddress.t -> t -> t
 

infer/src/pulse/PulseInvalidation.ml

@@ -58,28 +58,16 @@ let issue_type_of_cause = function
       IssueType.vector_invalidation
 
 
-let get_location = function
-  | CFree (_, location)
-  | CppDelete (_, location)
-  | CppDestructor (_, _, location)
-  | StdVector (_, _, location) ->
-      Some location
-  | Nullptr ->
-      None
-
-
 let pp f = function
-  | CFree (access_expr, location) ->
-      F.fprintf f "invalidated by call to `free(%a)` at %a" HilExp.AccessExpression.pp access_expr
-        Location.pp_line location
-  | CppDelete (access_expr, location) ->
-      F.fprintf f "invalidated by call to `delete %a` at %a" HilExp.AccessExpression.pp access_expr
-        Location.pp_line location
-  | CppDestructor (proc_name, access_expr, location) ->
-      F.fprintf f "invalidated by destructor call `%a(%a)` at %a" Typ.Procname.pp proc_name
-        HilExp.AccessExpression.pp access_expr Location.pp_line location
+  | CFree (access_expr, _) ->
+      F.fprintf f "by call to `free()` on `%a`" HilExp.AccessExpression.pp access_expr
+  | CppDelete (access_expr, _) ->
+      F.fprintf f "by `delete` on `%a`" HilExp.AccessExpression.pp access_expr
+  | CppDestructor (proc_name, access_expr, _) ->
+      F.fprintf f "by destructor call `%a()` on `%a`" Typ.Procname.pp proc_name
+        HilExp.AccessExpression.pp access_expr
   | Nullptr ->
       F.fprintf f "null pointer"
-  | StdVector (std_vector_f, access_expr, location) ->
-      F.fprintf f "potentially invalidated by call to `%a(%a, ..)` at %a" pp_std_vector_function
-        std_vector_f HilExp.AccessExpression.pp access_expr Location.pp_line location
+  | StdVector (std_vector_f, access_expr, _) ->
+      F.fprintf f "potentially invalidated by call to `%a()` on `%a`" pp_std_vector_function
+        std_vector_f HilExp.AccessExpression.pp access_expr

infer/src/pulse/PulseInvalidation.mli

@@ -29,6 +29,4 @@ type t =
 
 val issue_type_of_cause : t -> IssueType.t
 
-val get_location : t -> Location.t option
-
 val pp : Format.formatter -> t -> unit

infer/src/pulse/PulseModels.ml

@@ -26,7 +26,7 @@ module C = struct
     match actuals with
     | [AccessExpression deleted_access] ->
         PulseOperations.invalidate
-          (CFree (deleted_access, location))
+          (PulseTrace.Immediate {imm= PulseInvalidation.CFree (deleted_access, location); location})
           location deleted_access astate
     | _ ->
         Ok astate
@@ -40,7 +40,8 @@ module Cplusplus = struct
     match actuals with
     | [AccessExpression deleted_access] ->
         PulseOperations.invalidate
-          (CppDelete (deleted_access, location))
+          (PulseTrace.Immediate
+             {imm= PulseInvalidation.CppDelete (deleted_access, location); location})
           location deleted_access astate
     | _ ->
         Ok astate
@@ -76,7 +77,7 @@ module Cplusplus = struct
         |> read_all other_actuals
     | _ :: other_actuals ->
         read_all other_actuals astate >>| PulseOperations.havoc_var [crumb] ret_var
-    | _ ->
+    | [] ->
         Ok (PulseOperations.havoc_var [crumb] ret_var astate)
 end
 
@@ -100,7 +101,9 @@ module StdVector = struct
   let reallocate_internal_array trace vector vector_f location astate =
     let array_address = to_internal_array vector in
     let array = deref_internal_array vector in
-    let invalidation = PulseInvalidation.StdVector (vector_f, vector, location) in
+    let invalidation =
+      PulseTrace.Immediate {imm= PulseInvalidation.StdVector (vector_f, vector, location); location}
+    in
     PulseOperations.invalidate_array_elements invalidation location array astate
     >>= PulseOperations.invalidate invalidation location array
     >>= PulseOperations.havoc trace location array_address

infer/src/pulse/PulseOperations.ml

@@ -26,23 +26,23 @@ 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 actor (address, trace) astate =
-  Memory.check_valid actor address astate
+let check_addr_access action (address, trace) astate =
+  Memory.check_valid action address astate
   |> Result.map_error ~f:(fun invalidated_by ->
-         PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; trace} )
+         PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= action; trace} )
 
 
 (** Walk the heap starting from [addr] and following [path]. Stop either at the element before last
    and return [new_addr] if [overwrite_last] is [Some new_addr], or go until the end of the path if it
    is [None]. Create more addresses into the heap as needed to follow the [path]. Check that each
    address reached is valid. *)
-let rec walk ~dereference_to_ignore actor ~on_last addr_trace path astate =
-  let check_addr_access_optional actor addr_trace astate =
+let rec walk ~dereference_to_ignore action ~on_last addr_trace path astate =
+  let check_addr_access_optional action addr_trace astate =
     match dereference_to_ignore with
     | Some 0 ->
         Ok astate
     | _ ->
-        check_addr_access actor addr_trace astate
+        check_addr_access action addr_trace astate
   in
   match (path, on_last) with
   | [], `Access ->
@@ -50,18 +50,18 @@ let rec walk ~dereference_to_ignore actor ~on_last addr_trace path astate =
   | [], `Overwrite _ ->
       L.die InternalError "Cannot overwrite last address in empty path"
   | [a], `Overwrite new_addr_trace ->
-      check_addr_access_optional actor addr_trace astate
+      check_addr_access_optional action addr_trace astate
       >>| fun astate ->
       let astate = Memory.add_edge_and_back_edge (fst addr_trace) a new_addr_trace astate in
       (astate, new_addr_trace)
   | a :: path, _ ->
-      check_addr_access_optional actor addr_trace astate
+      check_addr_access_optional action addr_trace astate
       >>= fun astate ->
       let dereference_to_ignore =
         Option.map ~f:(fun index -> max 0 (index - 1)) dereference_to_ignore
       in
       let astate, addr_trace' = Memory.materialize_edge (fst addr_trace) a astate in
-      walk ~dereference_to_ignore actor ~on_last addr_trace' path astate
+      walk ~dereference_to_ignore action ~on_last addr_trace' path astate
 
 
 let write_var var new_addr_trace astate =
@@ -130,8 +130,8 @@ and walk_access_expr ~on_last astate access_expr location =
       | [HilExp.Access.TakeAddress] ->
           Ok (astate, base_addr_trace)
       | _ ->
-          let actor = {PulseDiagnostic.access_expr; location} in
-          walk ~dereference_to_ignore actor ~on_last base_addr_trace
+          let action = PulseTrace.Immediate {imm= access_expr; location} in
+          walk ~dereference_to_ignore action ~on_last base_addr_trace
             (HilExp.Access.Dereference :: access_list)
             astate )
 
@@ -143,12 +143,7 @@ and walk_access_expr ~on_last astate access_expr location =
     known to be invalid. *)
 and materialize_address astate access_expr = walk_access_expr ~on_last:`Access astate access_expr
 
-and read location access_expr astate =
-  materialize_address astate access_expr location
-  >>= fun (astate, addr_trace) ->
-  let actor = {PulseDiagnostic.access_expr; location} in
-  check_addr_access actor addr_trace astate >>| fun astate -> (astate, addr_trace)
-
+and read location access_expr astate = materialize_address astate access_expr location
 
 and read_all location access_exprs astate =
   List.fold_result access_exprs ~init:astate ~f:(fun astate access_expr ->
@@ -174,7 +169,7 @@ let overwrite_address astate access_expr new_addr_trace =
 
 
 (** Add the given address to the set of know invalid addresses. *)
-let mark_invalid actor address astate = Memory.invalidate address actor astate
+let mark_invalid action address astate = Memory.invalidate address action astate
 
 let havoc_var trace var astate = write_var var (AbstractAddress.mk_fresh (), trace) astate
 
@@ -189,14 +184,14 @@ let write location access_expr addr astate =
 let invalidate cause location access_expr astate =
   materialize_address astate access_expr location
   >>= fun (astate, addr_trace) ->
-  check_addr_access {access_expr; location} addr_trace astate
+  check_addr_access (Immediate {imm= access_expr; location}) addr_trace astate
   >>| mark_invalid cause (fst addr_trace)
 
 
 let invalidate_array_elements cause location access_expr astate =
   materialize_address astate access_expr location
   >>= fun (astate, addr_trace) ->
-  check_addr_access {access_expr; location} addr_trace astate
+  check_addr_access (Immediate {imm= access_expr; location}) addr_trace astate
   >>| fun astate ->
   match Memory.find_opt (fst addr_trace) astate with
   | None ->
@@ -319,7 +314,7 @@ module Closures = struct
                 ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) edges
                 ~f:(fun (access, addr_trace) ->
                   if is_captured_fake_access access then
-                    check_addr_access {access_expr= lambda; location} addr_trace astate
+                    check_addr_access (Immediate {imm= lambda; location}) addr_trace astate
                     >>| fun _ -> ()
                   else Ok () )
           | _ ->
@@ -367,3 +362,28 @@ module StdVector = struct
     read location vector_access_expr astate
     >>| fun (astate, (addr, _)) -> Memory.std_vector_reserve addr astate
 end
+
+module Interproc = struct
+  open Result.Monad_infix
+
+  (* compute addresses for actuals and then call {!PulseAbductiveDomain.PrePost.apply} on each
+     pre/post pair in the summary. *)
+  let call callee_pname ~formals ~ret ~actuals _flags call_loc astate pre_posts =
+    L.d_printfln "PulseOperations.call" ;
+    List.fold_result actuals ~init:(astate, []) ~f:(fun (astate, rev_actual_addresses) actual ->
+        match actual with
+        | HilExp.AccessExpression access_expr ->
+            read call_loc access_expr astate
+            >>| fun (astate, (addr, trace)) -> (astate, Some (addr, trace) :: rev_actual_addresses)
+        | _ ->
+            Ok (astate, None :: rev_actual_addresses) )
+    >>= fun (astate, rev_actual_addresses) ->
+    let actuals = List.rev rev_actual_addresses in
+    read call_loc HilExp.AccessExpression.(address_of_base ret) astate
+    >>= fun (astate, ret) ->
+    List.fold_result pre_posts ~init:[] ~f:(fun posts pre_post ->
+        (* apply all pre/post specs *)
+        PulseAbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~ret ~actuals
+          astate
+        >>| fun post -> post :: posts )
+end

infer/src/pulse/PulseOperations.mli

@@ -59,10 +59,18 @@ val write :
   -> t access_result
 
 val invalidate :
-  PulseInvalidation.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result
+     PulseInvalidation.t PulseTrace.action
+  -> Location.t
+  -> HilExp.AccessExpression.t
+  -> t
+  -> t access_result
 
 val invalidate_array_elements :
-  PulseInvalidation.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result
+     PulseInvalidation.t PulseTrace.action
+  -> Location.t
+  -> HilExp.AccessExpression.t
+  -> t
+  -> t access_result
 
 val record_var_decl_location : Location.t -> Var.t -> t -> t
 
@@ -70,3 +78,16 @@ val remove_vars : Var.t list -> t -> t
 
 (* TODO: better name and pass location to report where we returned *)
 val check_address_of_local_variable : Procdesc.t -> AbstractAddress.t -> t -> t access_result
+
+module Interproc : sig
+  val call :
+       Typ.Procname.t
+    -> formals:Var.t list
+    -> ret:AccessPath.base
+    -> actuals:HilExp.t list
+    -> CallFlags.t
+    -> Location.t
+    -> t
+    -> PulseSummary.t
+    -> PulseAbductiveDomain.t list access_result
+end

infer/src/pulse/PulseSummary.ml

@@ -0,0 +1,14 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+type t = PulseAbductiveDomain.PrePost.t list
+
+let of_posts posts = List.map posts ~f:PulseAbductiveDomain.PrePost.of_post
+
+let pp fmt summary =
+  PrettyPrintable.pp_collection ~pp_item:PulseAbductiveDomain.PrePost.pp fmt summary

infer/src/pulse/PulseSummary.mli

@@ -0,0 +1,13 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+type t = PulseAbductiveDomain.PrePost.t list
+
+val of_posts : PulseAbductiveDomain.t list -> t
+
+val pp : Format.formatter -> t -> unit

infer/src/pulse/PulseTrace.ml

@@ -70,3 +70,44 @@ let pp_last_event f = function
 
 
 let pp_interesting_events f trace = pp_last_event f trace
+
+type 'a action =
+  | Immediate of {imm: 'a; location: Location.t}
+  | ViaCall of {action: 'a action; proc_name: Typ.Procname.t; location: Location.t}
+[@@deriving compare]
+
+let pp_action pp_immediate fmt = function
+  | Immediate {imm; _} ->
+      F.fprintf fmt "`%a`" pp_immediate imm
+  | ViaCall {proc_name; _} ->
+      F.fprintf fmt "call to `%a`" Typ.Procname.pp proc_name
+
+
+let rec immediate_of_action = function
+  | Immediate {imm; _} ->
+      imm
+  | ViaCall {action; _} ->
+      immediate_of_action action
+
+
+let trace_of_action ~action_name pp_immediate action =
+  let rec aux ~nesting rev_trace action =
+    match action with
+    | Immediate {imm; location} ->
+        Errlog.make_trace_element nesting location
+          (F.asprintf "%s %a here" action_name pp_immediate imm)
+          []
+        :: rev_trace
+        |> List.rev
+    | ViaCall {action; proc_name; location} ->
+        aux ~nesting:(nesting + 1)
+          ( Errlog.make_trace_element nesting location
+              (F.asprintf "%s during call to `%a` here" action_name Typ.Procname.pp proc_name)
+              []
+          :: rev_trace )
+          action
+  in
+  aux ~nesting:0 [] action
+
+
+let outer_location_of_action = function Immediate {location} | ViaCall {location} -> location

infer/src/pulse/PulseTrace.mli

@@ -6,6 +6,7 @@
  *)
 
 open! IStd
+module F = Format
 
 type breadcrumb =
   | VariableDeclaration of Location.t
@@ -21,8 +22,22 @@ type breadcrumb =
 
 type t = breadcrumb list [@@deriving compare]
 
-val pp : Format.formatter -> t -> unit
+val pp : F.formatter -> t -> unit
 
 val make_errlog_trace : depth:int -> t -> Errlog.loc_trace
 
-val pp_interesting_events : Format.formatter -> t -> unit
+val pp_interesting_events : F.formatter -> t -> unit
+
+type 'a action =
+  | Immediate of {imm: 'a; location: Location.t}
+  | ViaCall of {action: 'a action; proc_name: Typ.Procname.t; location: Location.t}
+[@@deriving compare]
+
+val pp_action : (F.formatter -> 'a -> unit) -> F.formatter -> 'a action -> unit
+
+val immediate_of_action : 'a action -> 'a
+
+val outer_location_of_action : 'a action -> Location.t
+
+val trace_of_action :
+  action_name:string -> (F.formatter -> 'a -> unit) -> 'a action -> Errlog.loc_trace_elem sexp_list

infer/tests/codetoanalyze/cpp/pulse/closures.cpp

@@ -31,7 +31,6 @@ int implicit_ref_capture_destroy_invoke_bad() {
   return f();
 }
 
-// need to understand copy constructor
 int FN_reassign_lambda_capture_destroy_invoke_bad() {
   std::function<int()> f;
   {
@@ -97,8 +96,12 @@ std::function<int()> ref_capture_read_lambda_ok() {
       f; // reading (but not invoking) the lambda doesn't use its captured vars
 }
 
-void delete_lambda_then_call_bad() {
+int FN_delete_lambda_then_call_bad() {
   std::function<int()> lambda = [] { return 1; };
+  // std::function<_>_~function() has no implementation so the call is
+  // skipped and we don't apply the logic for marking the object as
+  // destructed because it's an explicit call (as opposed to a call
+  // injected by the frontend)
   lambda.~function();
   return lambda();
 }
@@ -125,7 +128,7 @@ int ref_capture_return_local_lambda_ok() {
   return f().f;
 }
 
-S& FN_ref_capture_return_local_lambda_bad() {
+S& ref_capture_return_local_lambda_bad() {
   S x;
   auto f = [&x](void) -> S& {
     // no way to know if ok here

infer/tests/codetoanalyze/cpp/pulse/interprocedural.cpp

@@ -23,12 +23,12 @@ void wraps_delete_inner(struct X* x) { delete x; }
 
 void wraps_delete(struct X* x) { wraps_delete_inner(x); }
 
-void FP_delete_then_skip_ok(struct X& x) {
+void delete_then_skip_ok(struct X& x) {
   delete (&x);
   skip(x);
 }
 
-void FP_delete_then_skip_ptr_ok(struct X* x) {
+void delete_then_skip_ptr_ok(struct X* x) {
   delete x;
   skip_ptr(x);
 }
@@ -38,12 +38,12 @@ void delete_then_read_bad(struct X& x) {
   wraps_read(x);
 }
 
-void FN_delete_then_write_bad(struct X& x) {
+void delete_then_write_bad(struct X& x) {
   wraps_delete(&x);
   wraps_read(x);
 }
 
-void FN_delete_inner_then_write_bad(struct X& x) {
+void delete_inner_then_write_bad(struct X& x) {
   wraps_delete_inner(&x);
   wraps_read(x);
 }
@@ -75,7 +75,7 @@ void call_store(struct Y* y) {
 
 extern bool nondet_choice();
 
-struct Y* FP_may_return_invalid_ptr_ok() {
+struct Y* may_return_invalid_ptr_ok() {
   struct Y* y = new Y();
   if (nondet_choice()) {
     delete y;
@@ -83,7 +83,7 @@ struct Y* FP_may_return_invalid_ptr_ok() {
   return y;
 }
 
-void FN_feed_invalid_into_access_bad() {
-  struct Y* y = FP_may_return_invalid_ptr_ok();
+void feed_invalid_into_access_bad() {
+  struct Y* y = may_return_invalid_ptr_ok();
   call_store(y);
 }

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -1,43 +1,42 @@
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 58 here,accessed `*(ptr)` here]
-codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68 here,accessed `ptr` here]
-codetoanalyze/cpp/pulse/closures.cpp, delete_lambda_then_call_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `std::function<_fn_>::function(&(lambda),&(0$?%__sil_tmpSIL_materialize_temp__n$8))`,invalidated by destructor call `std::function<_fn_>::~function(lambda)` at line 102 here,accessed `lambda` here]
-codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S::S(&(s),&(0$?%__sil_tmpSIL_materialize_temp__n$11))`,`&(s)` captured as `s`,invalidated by destructor call `S::~S(s)` at line 30 here,accessed `&(f)` here]
-codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `S::S(&(s))`,`&(s)` captured as `s`,invalidated by destructor call `S::~S(s)` at line 21 here,accessed `&(f)` here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, FP_delete_then_skip_ok, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 27 here,accessed `x` here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, FP_delete_then_skip_ptr_ok, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 32 here,accessed `x` here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, FP_may_return_invalid_ptr_ok, 5, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Y))`,assigned to `y`,invalidated by call to `delete y` at line 81 here,accessed `y` here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 37 here,accessed `x` here]
-codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `result`,invalidated by call to `delete result` at line 30 here,accessed `*(result)` here]
-codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(int))`,assigned to `x`,invalidated by call to `delete x` at line 112 here,accessed `x` here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by `delete` on `ptr` here,accessed `*(ptr)` here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by `delete` on `ptr` here,accessed `ptr` here]
+codetoanalyze/cpp/pulse/closures.cpp, implicit_ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [variable declared,`&(s)` captured as `s`,invalidated by destructor call `S::~S()` on `s` here,accessed `&(f)` here]
+codetoanalyze/cpp/pulse/closures.cpp, ref_capture_destroy_invoke_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [variable declared,`&(s)` captured as `s`,invalidated by destructor call `S::~S()` on `s` here,accessed `&(f)` here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated during call to `wraps_delete_inner` here,invalidated by `delete` on `x` here,accessed during call to `wraps_read` here,accessed during call to `wraps_read_inner` here,accessed `x->f` here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by `delete` on `x` here,accessed during call to `wraps_read` here,accessed during call to `wraps_read_inner` here,accessed `x->f` here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated during call to `wraps_delete` here,invalidated during call to `wraps_delete_inner` here,invalidated by `delete` on `x` here,accessed during call to `wraps_read` here,accessed during call to `wraps_read_inner` here,accessed `x->f` here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `y`,assigned to `return`,returned from call to `may_return_invalid_ptr_ok()`,assigned to `y`,invalidated during call to `may_return_invalid_ptr_ok` here,invalidated by `delete` on `y` here,accessed during call to `call_store` here,accessed during call to `store` here,accessed `y->p` here]
+codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `result`,invalidated by `delete` on `result` here,accessed `*(result)` here]
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_literal_stack_reference_bad, 0, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_stack_pointer_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference1_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
 codetoanalyze/cpp/pulse/returns.cpp, returns::return_variable_stack_reference2_bad, 1, STACK_VARIABLE_ADDRESS_ESCAPE, no_bucket, ERROR, []
-codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 57 here,accessed `s->f` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 82 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 18 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 50 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 37 here,accessed `s->f` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, return_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 24 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 73 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(Simple))`,assigned to `s`,invalidated by call to `delete s` at line 102 here,accessed `s->f` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `use_after_destructor::S::S(&(s),1)`,invalidated by destructor call `use_after_destructor::S::~S(s)` at line 65 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,invalidated by call to `delete alias` at line 149 here,accessed `s` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,returned from call to `<placement new>(sizeof(use_after_destructor::S),s)`,assigned to `alias`,invalidated by call to `delete s` at line 157 here,accessed `alias` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `__new(sizeof(use_after_destructor::S))`,assigned to `s`,assigned to `alias`,invalidated by call to `delete s` at line 166 here,accessed `alias` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `use_after_destructor::S::S(&(s),1)`,invalidated by destructor call `use_after_destructor::S::~S(s)` at line 72 here,accessed `*(s.f)` here]
-codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [returned from call to `use_after_destructor::C::C(&(c),3)`,invalidated by destructor call `use_after_destructor::C::~C(c)` at line 211 here,accessed `pc->f` here]
-codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 15 here,accessed `x` here]
-codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10 here,accessed `*(x)` here]
-codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 65 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, VectorA::FP_push_back_value_field_ok, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 134 here,accessed `&(this->x)` here]
-codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::assign(vec, ..)` at line 93 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::clear(vec, ..)` at line 87 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 20 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,assigned to `y`,potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 13 here,accessed `*(y)` here]
-codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::emplace_back(vec, ..)` at line 117 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::emplace(vec, ..)` at line 111 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::insert(vec, ..)` at line 105 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 74 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::reserve(vec, ..)` at line 81 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,potentially invalidated by call to `std::vector::shrink_to_fit(vec, ..)` at line 99 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed `s->f` here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed `s` here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed during call to `Simple::Simple` here,accessed `__param_0->f` here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed `s` here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed `s->f` here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed during call to `Simple::Simple` here,accessed `__param_0->f` here]
+codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `s` here,accessed `s->f` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::FP_destruct_pointer_contents_then_placement_new2_ok, 2, USE_AFTER_DELETE, no_bucket, ERROR, [returned from call to `<placement new>(sizeof(use_after_destructor::S),&(s->f))`,invalidated during call to `use_after_destructor::S::~S` here,invalidated during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,accessed during call to `use_after_destructor::S::S` here,accessed `this->f` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [variable declared,invalidated during call to `use_after_destructor::S::~S` here,invalidated during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,accessed during call to `use_after_destructor::S::~S` here,accessed during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,accessed `this->f` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,invalidated by `delete` on `alias` here,accessed `s->f` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,returned from call to `<placement new>(sizeof(use_after_destructor::S),s)`,assigned to `alias`,invalidated by `delete` on `s` here,accessed `alias->f` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing3_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `s`,assigned to `alias`,invalidated by `delete` on `s` here,accessed `alias->f` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::reinit_after_explicit_destructor2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [variable declared,invalidated during call to `use_after_destructor::S::~S` here,invalidated during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,accessed during call to `use_after_destructor::S::~S` here,accessed during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,accessed `this->f` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_destructor_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [assigned to `this->f`,returned from call to `use_after_destructor::S::S()`,invalidated during call to `use_after_destructor::S::~S` here,invalidated during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,accessed `*(s.f)` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope1_bad, 7, USE_AFTER_DELETE, no_bucket, ERROR, [variable declared,invalidated during call to `use_after_destructor::S::~S` here,invalidated during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,accessed during call to `use_after_destructor::S::~S` here,accessed during call to `use_after_destructor::S::__infer_inner_destructor_~S` here,accessed `this->f` here]
+codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [variable declared,invalidated by destructor call `use_after_destructor::C::~C()` on `c` here,accessed `pc->f` here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free()` on `x` here,accessed `x` here]
+codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free()` on `x` here,accessed `*(x)` here]
+codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::push_back()` on `&(vec)` here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::assign()` on `vec` here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::clear()` on `vec` here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::push_back()` on `&(vec)` here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,assigned to `y`,invalidated potentially invalidated by call to `std::vector::push_back()` on `vec` here,accessed `*(y)` here]
+codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::emplace_back()` on `vec` here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::emplace()` on `vec` here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::insert()` on `vec` here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, push_back_loop_bad, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(&(vec),(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::push_back()` on `&(vec)` here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, reserve_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::reserve()` on `vec` here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, shrink_to_fit_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [returned from call to `std::vector::at(vec,(unsigned long) 1)`,assigned to `elt`,invalidated potentially invalidated by call to `std::vector::shrink_to_fit()` on `vec` here,accessed `*(elt)` here]

infer/tests/codetoanalyze/cpp/pulse/returns.cpp

@@ -106,7 +106,8 @@ S* return_static_local_inner_scope_ok(bool b) {
 
 int* return_formal_pointer_ok(int* formal) { return formal; }
 
-int* return_deleted_bad() {
+// this *could* be ok depending on what the caller does
+int* return_deleted_ok() {
   int* x = new int;
   *x = 2;
   delete x;

infer/tests/codetoanalyze/cpp/pulse/use_after_delete.cpp

@@ -19,7 +19,8 @@ void deref_deleted_bad() {
   Simple tmp = *s;
 }
 
-Simple* return_deleted_bad() {
+// could be ok depending on what the caller does
+Simple* return_deleted_ok() {
   auto s = new Simple{1};
   delete s;
   return s;

infer/tests/codetoanalyze/cpp/pulse/use_after_destructor.cpp

@@ -75,9 +75,8 @@ int use_after_destructor_bad() {
   return ret;
 }
 
-// can't get this yet because we assume operator= copies resources correctly
-// (but this isn't true for S)
-void FN_use_after_scope1_bad() {
+// S::operator= doesn't copy resources correctly
+void use_after_scope1_bad() {
   S s(1);
   {
     S tmp(2);
@@ -130,41 +129,41 @@ void basic_placement_new_ok() {
   delete[] ptr;
 }
 
-S* destruct_pointer_contents_then_placement_new1_ok(S* s) {
+int* destruct_pointer_contents_then_placement_new1_ok(S* s) {
   s->~S();
   new (s) S(1);
-  return s;
+  return s->f;
 }
 
-S* destruct_pointer_contents_then_placement_new2_ok(S* s) {
+int* FP_destruct_pointer_contents_then_placement_new2_ok(S* s) {
   s->~S();
   new (&(s->f)) S(1);
-  return s;
+  return s->f;
 }
 
-S* placement_new_aliasing1_bad() {
+int* placement_new_aliasing1_bad() {
   S* s = new S(1);
   s->~S();
   auto alias = new (s) S(2);
   delete alias; // this deletes s too
-  return s; // bad, returning freed memory
+  return s->f; // bad, accessing freed memory
 }
 
-S* placement_new_aliasing2_bad() {
+int* placement_new_aliasing2_bad() {
   S* s = new S(1);
   s->~S();
   auto alias = new (s) S(2);
   delete s; // this deletes alias too
-  return alias; // bad, returning freed memory
+  return alias->f; // bad, accessing freed memory
 }
 
-S* placement_new_aliasing3_bad() {
+int* placement_new_aliasing3_bad() {
   S* s = new S(1);
   s->~S();
   S* alias = s;
   auto alias_placement = new (s) S(2);
   delete s; // this deletes alias too
-  return alias; // bad, returning freed memory
+  return alias->f; // bad, accessing freed memory
 }
 
 void placement_new_non_var_ok() {

infer/tests/codetoanalyze/cpp/pulse/vector.cpp

@@ -129,7 +129,7 @@ void push_back_value_ok(std::vector<int>& vec) {
 struct VectorA {
   int x;
 
-  void FP_push_back_value_field_ok(std::vector<int>& vec) {
+  void push_back_value_field_ok(std::vector<int>& vec) {
     x = vec[0];
     vec.push_back(7);
     f(x);