[pulse] overwrite attributes of modified cells in interproc calls

Summary:
Previously we would union them with the previous attributes. I don't
think that makes sense.

Also change the interface a bit in preparation for the next commit.

Reviewed By: mbouaziz

Differential Revision: D16050051

fbshipit-source-id: 2e8f88f4e

infer/src/pulse/PulseAbductiveDomain.ml

@@ -533,17 +533,12 @@ module PrePost = struct
     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 heap = (call_state.astate.post :> base_domain).heap in
-      let attrs_post =
+    let heap =
+      let attrs_post_caller =
         Attributes.map ~f:(fun attr -> add_call_to_attr callee_proc_name call_loc attr) attrs_post
       in
-      match
+      PulseDomain.Memory.set_attrs addr_caller attrs_post_caller heap
-        PulseDomain.Memory.find_attrs_opt addr_caller (call_state.astate.post :> base_domain).heap
-      with
-      | None ->
-          attrs_post
-      | Some old_attrs_post ->
-          Attributes.union_prefer_left old_attrs_post attrs_post
     in
     let subst, translated_post_edges =
       PulseDomain.Memory.Edges.fold_map ~init:call_state.subst edges_post
@@ -554,16 +549,15 @@ module PrePost = struct
             , PulseDomain.ValueHistory.Call {f= `Call callee_proc_name; location= call_loc}
               :: trace_post ) ) )
     in
-    let caller_post =
+    let heap =
-      let new_edges =
+      let edges_post_caller =
         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_edges addr_caller edges_post_caller heap
-        (PulseDomain.Memory.set_cell addr_caller (new_edges, new_attrs)
-           (call_state.astate.post :> base_domain).heap)
     in
+    let caller_post = Domain.make (call_state.astate.post :> base_domain).stack heap in
     {call_state with subst; astate= {call_state.astate with post= caller_post}}
 
 

infer/src/pulse/PulseDomain.ml

@@ -384,9 +384,11 @@ module Memory : sig
 
   val find_opt : AbstractAddress.t -> t -> cell option
 
-  val set_cell : AbstractAddress.t -> cell -> t -> t
+  val set_attrs : AbstractAddress.t -> Attributes.t -> t -> t
+
+  val set_edges : AbstractAddress.t -> edges -> t -> t
 
-  val find_attrs_opt : AbstractAddress.t -> t -> Attributes.t option
+  val set_cell : AbstractAddress.t -> cell -> t -> t
 
   val find_edges_opt : AbstractAddress.t -> t -> edges option
 
@@ -513,6 +515,10 @@ end = struct
         Some (edges, attrs)
 
 
+  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)
+
   let set_cell addr (edges, attrs) memory =
     (Graph.add addr edges (fst memory), Graph.add addr attrs (snd memory))
 

infer/src/pulse/PulseDomain.mli

@@ -143,9 +143,11 @@ module Memory : sig
 
   val find_opt : AbstractAddress.t -> t -> cell option
 
-  val set_cell : AbstractAddress.t -> cell -> t -> t
+  val set_attrs : AbstractAddress.t -> Attributes.t -> t -> t
+
+  val set_edges : AbstractAddress.t -> edges -> t -> t
 
-  val find_attrs_opt : AbstractAddress.t -> t -> Attributes.t option
+  val set_cell : AbstractAddress.t -> cell -> t -> t
 
   val find_edges_opt : AbstractAddress.t -> t -> edges option