From 7ec2830d926fb22ce88ef87ea155d0f4d2cff9f3 Mon Sep 17 00:00:00 2001
From: Benno Stein <bennostein@fb.com>
Date: Thu, 26 Sep 2019 01:56:54 -0700
Subject: [PATCH] [sledge] Only merge worklist states that share a calling
 context

Summary:
This diff allows domains to specify which abstract states can or can't
be merged together by the worklist.  In particular, this is needed for
relational domains to ensure that Hoare triples are joined only when
they share a precondition.

Reviewed By: jberdine

Differential Revision: D17571148

fbshipit-source-id: d9345fdc9
---
 sledge/src/control.ml               | 10 ++++++++--
 sledge/src/domain/domain_sig.ml     |  2 +-
 sledge/src/domain/relation.ml       |  6 ++++--
 sledge/src/domain/unit.ml           |  2 +-
 sledge/src/domain/used_globals.ml   |  2 +-
 sledge/src/symbheap/state_domain.ml |  2 +-
 6 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 3dad80fe5..e3472d78d 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -232,9 +232,15 @@ module Make (Dom : Domain_sig.Dom) = struct
       match Fheap.pop pq0 with
       | Some ((_, ({Edge.dst; stk} as edge)), pq) -> (
         match Map.find_and_remove ws dst with
-        | Some (state :: states, ws) ->
+        | Some (q :: qs, ws) ->
             let join (qa, da) (q, d) = (Dom.join q qa, Depths.join d da) in
-            let qs, depths = List.fold ~f:join ~init:state states in
+            let skipped, (qs, depths) =
+              List.fold qs ~init:([], q) ~f:(fun (skipped, joined) curr ->
+                  match join curr joined with
+                  | Some joined, depths -> (skipped, (joined, depths))
+                  | None, _ -> (curr :: skipped, joined) )
+            in
+            let ws = Map.add_exn ws ~key:dst ~data:skipped in
             run ~f (f stk qs dst depths (pq, ws, bnd))
         | _ ->
             [%Trace.info "done: %a" Edge.pp edge] ;
diff --git a/sledge/src/domain/domain_sig.ml b/sledge/src/domain/domain_sig.ml
index a38400c25..70b95e4e0 100644
--- a/sledge/src/domain/domain_sig.ml
+++ b/sledge/src/domain/domain_sig.ml
@@ -12,7 +12,7 @@ module type Dom = sig
   val pp : t pp
   val report_fmt_thunk : t -> Formatter.t -> unit
   val init : Global.t vector -> t
-  val join : t -> t -> t
+  val join : t -> t -> t option
   val is_false : t -> bool
   val exec_assume : t -> Exp.t -> t option
   val exec_kill : t -> Var.t -> t
diff --git a/sledge/src/domain/relation.ml b/sledge/src/domain/relation.ml
index bb644f667..a1fb3f4cc 100644
--- a/sledge/src/domain/relation.ml
+++ b/sledge/src/domain/relation.ml
@@ -32,8 +32,10 @@ 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_b entry_a) ;
-    (entry_a, State_domain.join current_a current_b)
+    if State_domain.equal entry_b entry_a then
+      State_domain.join current_a current_b
+      >>= fun curr -> Some (entry_a, curr)
+    else None
 
   let is_false (_, curr) = State_domain.is_false curr
 
diff --git a/sledge/src/domain/unit.ml b/sledge/src/domain/unit.ml
index eaf392374..ce7e375f4 100644
--- a/sledge/src/domain/unit.ml
+++ b/sledge/src/domain/unit.ml
@@ -12,7 +12,7 @@ type t = unit [@@deriving equal, sexp_of]
 let pp fs () = Format.pp_print_string fs "()"
 let report_fmt_thunk () fs = pp fs ()
 let init _ = ()
-let join () () = ()
+let join () () = Some ()
 let is_false _ = false
 let exec_assume () _ = Some ()
 let exec_kill () _ = ()
diff --git a/sledge/src/domain/used_globals.ml b/sledge/src/domain/used_globals.ml
index a6f78f34e..d6ec071d4 100644
--- a/sledge/src/domain/used_globals.ml
+++ b/sledge/src/domain/used_globals.ml
@@ -18,7 +18,7 @@ let init globals =
     "pgm globals: {%a}" (Vector.pp ", " Llair_.Global.pp) globals] ;
   empty
 
-let join = Set.union
+let join l r = Some (Set.union l r)
 let recursion_beyond_bound = `skip
 let is_false _ = false
 let post _ _ state = state
diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml
index 783fbede5..bc3d14967 100644
--- a/sledge/src/symbheap/state_domain.ml
+++ b/sledge/src/symbheap/state_domain.ml
@@ -25,7 +25,7 @@ let init globals =
         Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr})
     | _ -> q )
 
-let join = Sh.or_
+let join l r = Some (Sh.or_ l r)
 let is_false = Sh.is_false
 let exec_assume = Exec.assume
 let exec_kill = Exec.kill