From 493d38a6820304f6b49a83772e8b9fa7670888f6 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Fri, 28 Jun 2019 09:27:25 -0700
Subject: [PATCH] [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 | 22 ++++++++--------------
 infer/src/pulse/PulseDomain.ml          | 10 ++++++++--
 infer/src/pulse/PulseDomain.mli         |  6 ++++--
 3 files changed, 20 insertions(+), 18 deletions(-)

diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index 471c3c344..1341b7e40 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/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 attrs_post =
+    let heap = (call_state.astate.post :> base_domain).heap in
+    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.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
+      PulseDomain.Memory.set_attrs addr_caller attrs_post_caller heap
     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 new_edges =
+    let heap =
+      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_cell addr_caller (new_edges, new_attrs)
-           (call_state.astate.post :> base_domain).heap)
+      PulseDomain.Memory.set_edges addr_caller edges_post_caller 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}}
 
 
diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml
index 6d82c57bc..9b8e5af30 100644
--- a/infer/src/pulse/PulseDomain.ml
+++ b/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))
 
diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli
index 0a3ab71ba..0fc1b75b3 100644
--- a/infer/src/pulse/PulseDomain.mli
+++ b/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