[pulse] do not create `&` back-edges eagerly

Summary:
This mostly doesn't make sense. The only thing this would have been good
for was to give the most accurate result on access paths such as
`*(&(x.f))`, but these are normalised anyway (into `x.f`) so we actually
never see these. That said there might be some use to some similar logic
in the future, but in the meantime let's delete the current feature as
it wasn't thought through.

Reviewed By: ezgicicek

Differential Revision: D14753492

fbshipit-source-id: 597cec027

infer/src/pulse/PulseAbductiveDomain.ml

@@ -161,11 +161,6 @@ module Memory = struct
     map_post_heap astate ~f:(fun heap -> BaseMemory.add_edge addr access new_addr_trace heap)
 
 
-  let add_edge_and_back_edge addr access new_addr_trace astate =
-    map_post_heap astate ~f:(fun heap ->
-        BaseMemory.add_edge_and_back_edge addr access new_addr_trace heap )
-
-
   let materialize_edge addr access astate =
     match BaseMemory.find_edge_opt addr access (astate.post :> base_domain).heap with
     | Some addr_trace' ->
@@ -173,13 +168,11 @@ module Memory = struct
     | None ->
         let addr_trace' = (AbstractAddress.mk_fresh (), []) in
         let post_heap =
-          BaseMemory.add_edge_and_back_edge addr access addr_trace'
+          BaseMemory.add_edge addr access addr_trace' (astate.post :> base_domain).heap
-            (astate.post :> base_domain).heap
         in
         let foot_heap =
           if BaseMemory.mem_edges addr (astate.pre :> base_domain).heap then
-            BaseMemory.add_edge_and_back_edge addr access addr_trace'
+            BaseMemory.add_edge addr access addr_trace' (astate.pre :> base_domain).heap
-              (astate.pre :> base_domain).heap
             |> BaseMemory.register_address (fst addr_trace')
           else (astate.pre :> base_domain).heap
         in

infer/src/pulse/PulseAbductiveDomain.mli

@@ -42,9 +42,6 @@ module Memory : sig
 
   val add_edge : AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t
 
-  val add_edge_and_back_edge :
-    AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t
-
   val check_valid :
        HilExp.AccessExpression.t PulseTrace.action
     -> AbstractAddress.t

infer/src/pulse/PulseDomain.ml

@@ -171,8 +171,6 @@ module Memory : sig
 
   val add_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t
 
-  val add_edge_and_back_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t
-
   val find_edge_opt : AbstractAddress.t -> Access.t -> t -> AddrTracePair.t option
 
   val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t
@@ -223,19 +221,6 @@ end = struct
     else (Graph.add addr_src new_edges (fst memory), snd memory)
 
 
-  (** [Dereference] edges induce a [TakeAddress] back edge and vice-versa, because
-      [*(&x) = &( *x ) = x]. *)
-  let add_edge_and_back_edge addr_src (access : Access.t) addr_trace_dst memory =
-    let memory = add_edge addr_src access addr_trace_dst memory in
-    match access with
-    | ArrayAccess _ | FieldAccess _ ->
-        memory
-    | TakeAddress ->
-        add_edge (fst addr_trace_dst) Dereference (addr_src, []) memory
-    | Dereference ->
-        add_edge (fst addr_trace_dst) TakeAddress (addr_src, []) memory
-
-
   let find_edge_opt addr access memory =
     let open Option.Monad_infix in
     Graph.find_opt addr (fst memory) >>= Edges.find_opt access

infer/src/pulse/PulseDomain.mli

@@ -89,8 +89,6 @@ module Memory : sig
 
   val add_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t
 
-  val add_edge_and_back_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t
-
   val find_edge_opt : AbstractAddress.t -> Access.t -> t -> AddrTracePair.t option
 
   val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t

infer/src/pulse/PulseOperations.ml

@@ -52,7 +52,7 @@ let rec walk ~dereference_to_ignore action ~on_last addr_trace path astate =
   | [a], `Overwrite new_addr_trace ->
       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
+      let astate = Memory.add_edge (fst addr_trace) a new_addr_trace astate in
       (astate, new_addr_trace)
   | a :: path, _ ->
       check_addr_access_optional action addr_trace astate

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

@@ -21,7 +21,6 @@ codetoanalyze/cpp/pulse/use_after_delete.cpp, double_delete_bad, 3, USE_AFTER_DE
 codetoanalyze/cpp/pulse/use_after_delete.cpp, reassign_field_of_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by `delete` on `s` here,start of use after lifetime trace,accessed `s->f` here,start of value trace,assigned to `s`]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_branch_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by `delete` on `s` here,start of use after lifetime trace,accessed during call to `Simple` here,accessed `__param_0->f` here,start of value trace,assigned to `s`]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, use_in_loop_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by `delete` on `s` here,start of use after lifetime trace,accessed `s->f` here,start of value trace,assigned to `s`]
-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, [start of end of lifetime trace,invalidated by during call to `~S` here,invalidated by during call to `__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,start of use after lifetime trace,accessed during call to `S` here,accessed `*(this->f)` here,start of value trace,returned from call to `<placement new>(sizeof(use_after_destructor::S),&(s->f))`]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::double_destructor_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by during call to `~S` here,invalidated by during call to `__infer_inner_destructor_~S` here,invalidated by `delete` on `this->f` here,start of use after lifetime trace,accessed during call to `~S` here,accessed during call to `__infer_inner_destructor_~S` here,accessed `this->f` here,start of value trace,variable declared]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing1_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by `delete` on `alias` here,start of use after lifetime trace,accessed `s->f` here,start of value trace,assigned to `s`]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::placement_new_aliasing2_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [start of end of lifetime trace,invalidated by `delete` on `s` here,start of use after lifetime trace,accessed `alias->f` here,start of value trace,assigned to `s`,returned from call to `<placement new>(sizeof(use_after_destructor::S),s)`,assigned to `alias`]

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

@@ -135,7 +135,7 @@ int* destruct_pointer_contents_then_placement_new1_ok(S* s) {
   return s->f;
 }
 
-int* FP_destruct_pointer_contents_then_placement_new2_ok(S* s) {
+int* destruct_pointer_contents_then_placement_new2_ok(S* s) {
   s->~S();
   new (&(s->f)) S(1);
   return s->f;