From 3d14ef6c7732ce004a1f18ed166c555c69da2d71 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 28 Jun 2021 03:33:51 -0700
Subject: [PATCH] [sledge] Revise symbolic state joining

Summary:
Allow joining relations with distinct entry states, since the
destinations will be the same, there is no loss of context
sensitivity. As a result, check that the call stack of the
destinations of edges are equal before joining, as it is no longer
implicitly ensured by the equal entry state check.

This change leads to joining a state with itself often, as the entry
states are often idential, so this diff also adds an optimization of
join with a fast path for joining identical states.

Reviewed By: ngorogiannis

Differential Revision: D28907809

fbshipit-source-id: 2c66223ff
---
 sledge/src/control.ml         | 5 ++++-
 sledge/src/domain_relation.ml | 4 ++--
 sledge/src/domain_sh.ml       | 2 +-
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 7d4fd6871..d21b00480 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -421,7 +421,10 @@ module Make (Config : Config) (D : Domain) (Queue : Queue) = struct
       let pp ppf {depth; edge} =
         Format.fprintf ppf "%i: %a" depth Edge.pp edge
 
-      let joinable x y = Llair.Block.equal x.edge.dst y.edge.dst
+      let joinable x y =
+        Llair.Block.equal x.edge.dst y.edge.dst
+        && Stack.equal_as_inlined_location x.edge.stk y.edge.stk
+
       let dnf x = List.map ~f:(fun state -> {x with state}) (D.dnf x.state)
     end
 
diff --git a/sledge/src/domain_relation.ml b/sledge/src/domain_relation.ml
index be681dd2d..05a8791db 100644
--- a/sledge/src/domain_relation.ml
+++ b/sledge/src/domain_relation.ml
@@ -36,8 +36,8 @@ module Make (State_domain : State_domain_sig) = struct
   let init globals = embed (State_domain.init globals)
 
   let join (entry_a, current_a) (entry_b, current_b) =
-    assert (State_domain.equal entry_a entry_b) ;
-    (entry_a, State_domain.join current_a current_b)
+    ( State_domain.join entry_a entry_b
+    , State_domain.join current_a current_b )
 
   let exec_assume (entry, current) cnd =
     let+ next = State_domain.exec_assume current cnd in
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index d6f2f9139..b1564fd50 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -36,7 +36,7 @@ let init globals =
 let join p q =
   [%Trace.call fun {pf} -> pf "@ %a@ %a" pp p pp q]
   ;
-  Sh.or_ p q |> simplify
+  (if p == q then p else Sh.or_ p q |> simplify)
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]