[sledge] Revise type of Domain join operation, it is not partial

Summary:
The only domain with a partial join is the lifting of a predicate
domain to a relation one, where the entry states are required to be
equal. This situation now indicates a programming error in the
analysis, rather than something that the domain should be responsible
for. Therefore this diff changes that check to an assertion and
simplifies the remaining join operations which are all total.

Reviewed By: jvillard

Differential Revision: D27828763

fbshipit-source-id: ec52ff741

sledge/cli/domain_itv.ml

@@ -19,7 +19,7 @@ type t = Box.t Abstract1.t
 let equal : t -> t -> bool = Poly.equal
 let compare : t -> t -> int = Poly.compare
 let man = lazy (Box.manager_alloc ())
-let join l r = Some (Abstract1.join (Lazy.force man) l r)
+let join l r = Abstract1.join (Lazy.force man) l r
 let is_false x = Abstract1.is_bottom (Lazy.force man) x
 
 let bindings (itv : t) =

sledge/src/control.ml

@@ -267,12 +267,10 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct
       let state, depths, queue =
         List.fold elts (state, depths, queue)
           ~f:(fun elt (state, depths, queue) ->
-            match Dom.join elt.state state with
+            let state = Dom.join elt.state state in
-            | Some state ->
             let depths = Depths.join elt.depths depths in
             let queue = PrioQueue.remove elt queue in
-                (state, depths, queue)
+            (state, depths, queue) )
-            | None -> (state, depths, queue) )
       in
       (edge, state, depths, queue)
 

sledge/src/domain_intf.ml

@@ -11,7 +11,7 @@ module type Dom = sig
 
   val pp : t pp
   val init : Llair.GlobalDefn.t iarray -> t
-  val join : t -> t -> t option
+  val join : t -> t -> t
   val dnf : t -> t list
   val exec_assume : t -> Llair.Exp.t -> t option
   val exec_kill : Llair.Reg.t -> t -> t

sledge/src/domain_relation.ml

@@ -34,10 +34,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) =
-    if State_domain.equal entry_a entry_b then
+    assert (State_domain.equal entry_a entry_b) ;
-      let+ next = State_domain.join current_a current_b in
+    (entry_a, State_domain.join current_a current_b)
-      (entry_a, next)
-    else None
 
   let exec_assume (entry, current) cnd =
     let+ next = State_domain.exec_assume current cnd in

sledge/src/domain_sh.ml

@@ -36,9 +36,9 @@ let init globals =
 let join p q =
   [%Trace.call fun {pf} -> pf "@ %a@ %a" pp p pp q]
   ;
-  Some (Sh.or_ p q) |> Option.map ~f:simplify
+  Sh.or_ p q |> simplify
   |>
-  [%Trace.retn fun {pf} -> pf "%a" (Option.pp "%a" pp)]
+  [%Trace.retn fun {pf} -> pf "%a" pp]
 
 let dnf = Sh.dnf
 

sledge/src/domain_unit.ml

@@ -11,7 +11,7 @@ type t = unit [@@deriving compare, equal, sexp]
 
 let pp fs () = Format.pp_print_string fs "()"
 let init _ = ()
-let join () () = Some ()
+let join () () = ()
 let exec_assume () _ = Some ()
 let exec_kill _ () = ()
 let exec_move _ () = ()

sledge/src/domain_used_globals.ml

@@ -17,7 +17,7 @@ let init globals =
     " globals: {%a}" (IArray.pp ", " Llair.GlobalDefn.pp) globals] ;
   empty
 
-let join l r = Some (Llair.Global.Set.union l r)
+let join l r = Llair.Global.Set.union l r
 let recursion_beyond_bound = `skip
 let post _ _ state = state
 let retn _ _ from_call post = Llair.Global.Set.union from_call post