[pulse] Remove bindings with empty edges in pre

Reviewed By: jvillard

Differential Revision: D16419183

fbshipit-source-id: 858958ddd

infer/src/pulse/PulseAbductiveDomain.ml

@@ -286,7 +286,14 @@ module PrePost = struct
         (fun var _ -> Var.is_return var || Stack.is_abducible astate var)
         (astate.post :> PulseDomain.t).stack
     in
-    {astate with post= Domain.update ~stack:post_stack astate.post}
+    (* deregister empty edges in pre *)
+    let pre_heap =
+      BaseMemory.filter_heap
+        (fun _addr edges -> not (BaseMemory.Edges.is_empty edges))
+        (astate.pre :> base_domain).heap
+    in
+    { pre= InvertedDomain.update astate.pre ~heap:pre_heap
+    ; post= Domain.update ~stack:post_stack astate.post }
 
 
   let of_post astate = filter_for_summary astate |> discard_unreachable

infer/src/pulse/PulseDomain.ml

@@ -389,6 +389,8 @@ module Memory : sig
 
   val filter : (AbstractAddress.t -> bool) -> t -> t
 
+  val filter_heap : (AbstractAddress.t -> edges -> bool) -> t -> t
+
   val find_opt : AbstractAddress.t -> t -> cell option
 
   val fold_attrs : (AbstractAddress.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc
@@ -540,6 +542,11 @@ end = struct
     if phys_equal heap (fst memory) && phys_equal attrs (snd memory) then memory else (heap, attrs)
 
 
+  let filter_heap f memory =
+    let heap = Graph.filter f (fst memory) in
+    if phys_equal heap (fst memory) then memory else (heap, snd memory)
+
+
   let mem_edges addr memory = Graph.mem addr (fst memory)
 end
 

infer/src/pulse/PulseDomain.mli

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