[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

@@ -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
 

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

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]