From 20a6eda491684fb83a2789a68f62a1f0c9035d13 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 21 Apr 2021 15:34:54 -0700 Subject: [PATCH] [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 | 2 +- sledge/src/control.ml | 10 ++++------ sledge/src/domain_intf.ml | 2 +- sledge/src/domain_relation.ml | 6 ++---- sledge/src/domain_sh.ml | 4 ++-- sledge/src/domain_unit.ml | 2 +- sledge/src/domain_used_globals.ml | 2 +- 7 files changed, 12 insertions(+), 16 deletions(-) diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml index 5bb89b956..8486afb17 100644 --- a/sledge/cli/domain_itv.ml +++ b/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) = diff --git a/sledge/src/control.ml b/sledge/src/control.ml index b50c3777f..9f8461f9e 100644 --- a/sledge/src/control.ml +++ b/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 - | Some state -> - let depths = Depths.join elt.depths depths in - let queue = PrioQueue.remove elt queue in - (state, depths, queue) - | None -> (state, depths, queue) ) + let state = Dom.join elt.state state in + let depths = Depths.join elt.depths depths in + let queue = PrioQueue.remove elt queue in + (state, depths, queue) ) in (edge, state, depths, queue) diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml index 28eb833bc..d373aab82 100644 --- a/sledge/src/domain_intf.ml +++ b/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 diff --git a/sledge/src/domain_relation.ml b/sledge/src/domain_relation.ml index aab6d660a..65dbddd89 100644 --- a/sledge/src/domain_relation.ml +++ b/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 - let+ next = State_domain.join current_a current_b in - (entry_a, next) - else None + assert (State_domain.equal entry_a entry_b) ; + (entry_a, 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 ac970b1e0..d6f2f9139 100644 --- a/sledge/src/domain_sh.ml +++ b/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 diff --git a/sledge/src/domain_unit.ml b/sledge/src/domain_unit.ml index 48fbece28..8c55da22f 100644 --- a/sledge/src/domain_unit.ml +++ b/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 _ () = () diff --git a/sledge/src/domain_used_globals.ml b/sledge/src/domain_used_globals.ml index 72fcc9ac1..016624e19 100644 --- a/sledge/src/domain_used_globals.ml +++ b/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