[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

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

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

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) ;
+    if State_domain.equal entry_b entry_a then
-    (entry_a, State_domain.join current_a current_b)
+      State_domain.join current_a current_b
+      >>= fun curr -> Some (entry_a, curr)
+    else None
 
   let is_false (_, curr) = State_domain.is_false curr
 

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 () _ = ()

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

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