From 886a47402dbf9197cd28ba9b7ff4639e180a0f21 Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Thu, 18 Feb 2021 07:49:14 -0800
Subject: [PATCH] [pulse] do not canonicalize preconditions

Summary:
There should be no equalities relevant to the precondition to
canonicalize against in the first place: equalities come either from
assignments (hence strictly to the post condition) or from PRUNE
statements, and we don't use the latter to canonicalize states anyway.

Reviewed By: skcho

Differential Revision: D26488378

fbshipit-source-id: 7923f71ea
---
 infer/src/pulse/PulseAbductiveDomain.ml | 28 ++++++++++---------------
 infer/src/pulse/PulseBaseStack.ml       |  1 +
 2 files changed, 12 insertions(+), 17 deletions(-)

diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index cd7d18ee5..03895fcc1 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -710,29 +710,23 @@ let incorporate_new_eqs astate new_eqs =
 let canonicalize astate =
   let open SatUnsat.Import in
   let get_var_repr v = PathCondition.get_var_repr astate.path_condition v in
-  let canonicalize_base stack heap attrs =
-    let stack' = BaseStack.canonicalize ~get_var_repr stack in
-    (* note: this step also de-registers addresses pointing to empty edges *)
-    let+ heap' = BaseMemory.canonicalize ~get_var_repr heap in
-    let attrs' = BaseAddressAttributes.canonicalize ~get_var_repr attrs in
-    (stack', heap', attrs')
-  in
-  (* need different functions for pre and post to appease the type system *)
   let canonicalize_pre (pre : PreDomain.t) =
-    let+ stack', heap', attrs' =
-      canonicalize_base (pre :> BaseDomain.t).stack (pre :> BaseDomain.t).heap
-        (pre :> BaseDomain.t).attrs
+    (* TODO: detect contradictions when equal addresses are pointing to different locations *)
+    let heap' =
+      BaseMemory.filter
+        (fun _ edges -> not (BaseMemory.Edges.is_empty edges))
+        (pre :> BaseDomain.t).heap
     in
-    PreDomain.update ~stack:stack' ~heap:heap' ~attrs:attrs' pre
+    PreDomain.update ~heap:heap' pre
   in
   let canonicalize_post (post : PostDomain.t) =
-    let+ stack', heap', attrs' =
-      canonicalize_base (post :> BaseDomain.t).stack (post :> BaseDomain.t).heap
-        (post :> BaseDomain.t).attrs
-    in
+    let stack' = BaseStack.canonicalize ~get_var_repr (post :> BaseDomain.t).stack in
+    (* note: this step also de-registers addresses pointing to empty edges *)
+    let+ heap' = BaseMemory.canonicalize ~get_var_repr (post :> BaseDomain.t).heap in
+    let attrs' = BaseAddressAttributes.canonicalize ~get_var_repr (post :> BaseDomain.t).attrs in
     PostDomain.update ~stack:stack' ~heap:heap' ~attrs:attrs' post
   in
-  let* pre = canonicalize_pre astate.pre in
+  let pre = canonicalize_pre astate.pre in
   let+ post = canonicalize_post astate.post in
   {astate with pre; post}
 
diff --git a/infer/src/pulse/PulseBaseStack.ml b/infer/src/pulse/PulseBaseStack.ml
index 1067f67c6..f7d83618b 100644
--- a/infer/src/pulse/PulseBaseStack.ml
+++ b/infer/src/pulse/PulseBaseStack.ml
@@ -32,6 +32,7 @@ module M = PrettyPrintable.MakePPMonoMap (VarAddress) (AddrHistPair)
 let yojson_of_t m = [%yojson_of: (VarAddress.t * AddrHistPair.t) list] (M.bindings m)
 
 let canonicalize ~get_var_repr stack =
+  (* TODO: detect contradictions when the addresses of two different program variables are equal *)
   let changed = ref false in
   let stack' =
     M.map