[pulse] record attributes of address not edge-reachable in the post

Summary:
Sometimes the post of a function call has attributes on addresses that
were mentioned in the pre but are no longer reachable in the post. We
don't want to forget these, see added test.

Reviewed By: mbouaziz

Differential Revision: D16050050

fbshipit-source-id: 1ce522b97

infer/src/pulse/PulseAbductiveDomain.ml

@@ -671,6 +671,32 @@ module PrePost = struct
         call_state
 
 
+  let record_post_remaining_attributes callee_proc_name call_loc pre_post call_state =
+    let heap0 = (call_state.astate.post :> base_domain).heap in
+    let heap =
+      PulseDomain.Memory.fold_attrs
+        (fun addr_callee attrs heap ->
+          if AddressSet.mem addr_callee call_state.visited then
+            (* already recorded the attributes when we were walking the edges map *) heap
+          else
+            match AddressMap.find_opt addr_callee call_state.subst with
+            | None ->
+                (* callee address has no meaning for the caller *) heap
+            | Some addr_caller ->
+                let attrs' =
+                  Attributes.map
+                    ~f:(fun attr -> add_call_to_attr callee_proc_name call_loc attr)
+                    attrs
+                in
+                PulseDomain.Memory.set_attrs addr_caller attrs' heap )
+        (pre_post.post :> PulseDomain.t).heap heap0
+    in
+    if phys_equal heap heap0 then call_state
+    else
+      let post = Domain.make (call_state.astate.post :> PulseDomain.t).stack heap in
+      {call_state with astate= {call_state.astate with post}}
+
+
   let apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state =
     PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ;
     let r =
@@ -678,7 +704,10 @@ module PrePost = struct
         call_state
       |> apply_post_for_globals callee_proc_name call_location pre_post
       |> record_post_for_return callee_proc_name call_location pre_post
-      |> fun ({astate; _}, return_caller) -> (astate, return_caller)
+      |> fun (call_state, return_caller) ->
+      ( record_post_remaining_attributes callee_proc_name call_location pre_post call_state
+      , return_caller )
+      |> fun ({astate}, return_caller) -> (astate, return_caller)
     in
     PerfEvent.(log (fun logger -> log_end_event logger ())) ;
     r

infer/src/pulse/PulseDomain.ml

@@ -384,6 +384,8 @@ module Memory : sig
 
   val find_opt : AbstractAddress.t -> t -> cell option
 
+  val fold_attrs : (AbstractAddress.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc
+
   val set_attrs : AbstractAddress.t -> Attributes.t -> t -> t
 
   val set_edges : AbstractAddress.t -> edges -> t -> t
@@ -515,6 +517,8 @@ end = struct
         Some (edges, attrs)
 
 
+  let fold_attrs f memory init = Graph.fold f (snd memory) init
+
   let set_attrs addr attrs memory = (fst memory, Graph.add addr attrs (snd memory))
 
   let set_edges addr edges memory = (Graph.add addr edges (fst memory), snd memory)

infer/src/pulse/PulseDomain.mli

@@ -143,6 +143,8 @@ module Memory : sig
 
   val find_opt : AbstractAddress.t -> t -> cell option
 
+  val fold_attrs : (AbstractAddress.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc
+
   val set_attrs : AbstractAddress.t -> Attributes.t -> t -> t
 
   val set_edges : AbstractAddress.t -> edges -> t -> t

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

@@ -94,3 +94,14 @@ void feed_invalid_into_access_bad() {
   struct Y* y = may_return_invalid_ptr_ok();
   call_store(y);
 }
+
+void invalidate_and_set_to_null(struct X** x_ptr) {
+  delete (*x_ptr);
+  *x_ptr = nullptr;
+}
+
+void access_to_invalidated_alias(struct X* x, struct X* y) {
+  y = x;
+  invalidate_and_set_to_null(&x);
+  wraps_read(*y);
+}

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

@@ -9,6 +9,7 @@ codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::SomeTemplatedClass<int
 codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<_Bool>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function` here,invalid access occurs here here]
 codetoanalyze/cpp/pulse/deduplication.cpp, deduplication::templated_function_bad<int>, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `deduplication::templated_delete_function` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `deduplication::templated_access_function` here,invalid access occurs here here]
 codetoanalyze/cpp/pulse/folly_DestructorGuard.cpp, UsingDelayedDestruction::double_delete_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,invalid access occurs here here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, 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 here]
 codetoanalyze/cpp/pulse/interprocedural.cpp, delete_aliased_then_read_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,assigned,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here]
 codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `wraps_delete_inner()` here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here]
 codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,memory was invalidated by `delete` here,use-after-lifetime part of the trace starts here,when calling `wraps_read()` here,when calling `wraps_read_inner()` here,invalid access occurs here here]