From e43582b4806f52fb8310e44b3dac4cb46c109c9c Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 1 Jul 2021 17:35:13 -0700 Subject: [PATCH] [sledge] Add n-ary join to Domain and use in analysis Summary: The width of joins in the concurrency analysis is much wider, making it worthwhile to use an n-ary version of join in order to avoid repeated formula simplifiaction. Differential Revision: D29441154 fbshipit-source-id: ae17de37b --- sledge/cli/domain_itv.ml | 5 +++++ sledge/src/control.ml | 11 ++++++++--- sledge/src/domain_intf.ml | 1 + sledge/src/domain_relation.ml | 4 ++++ sledge/src/domain_sh.ml | 7 +++++++ sledge/src/domain_unit.ml | 1 + sledge/src/domain_used_globals.ml | 1 + sledge/src/sh.mli | 4 ++++ 8 files changed, 31 insertions(+), 3 deletions(-) diff --git a/sledge/cli/domain_itv.ml b/sledge/cli/domain_itv.ml index 8486afb17..03db10a15 100644 --- a/sledge/cli/domain_itv.ml +++ b/sledge/cli/domain_itv.ml @@ -20,6 +20,11 @@ let equal : t -> t -> bool = Poly.equal let compare : t -> t -> int = Poly.compare let man = lazy (Box.manager_alloc ()) let join l r = Abstract1.join (Lazy.force man) l r + +let joinN = function + | [] -> Abstract1.bottom (Lazy.force man) (Environment.make [||] [||]) + | x :: xs -> List.fold ~f:join xs x + 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 d21b00480..9a10d6857 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -447,9 +447,14 @@ module Make (Config : Config) (D : Domain) (Queue : Queue) = struct [%Trace.info " %i: %a [%a]@ | %a" depth Edge.pp edge Stack.pp edge.stk Queue.pp queue] ; - let state, depths = - List.fold elts (state, depths) ~f:(fun elt (state, depths) -> - (D.join elt.state state, Depths.join elt.depths depths) ) + let states, depths = + List.fold elts + ([state], depths) + ~f:(fun elt (states, depths) -> + (elt.state :: states, Depths.join elt.depths depths) ) + in + let state = + D.joinN (List.sort_uniq ~cmp:(Ord.opp D.compare) states) in (edge, state, depths, queue) diff --git a/sledge/src/domain_intf.ml b/sledge/src/domain_intf.ml index b0ba8724b..705df0044 100644 --- a/sledge/src/domain_intf.ml +++ b/sledge/src/domain_intf.ml @@ -12,6 +12,7 @@ module type Domain = sig val pp : t pp val init : Llair.GlobalDefn.t iarray -> t val join : t -> t -> t + val joinN : t list -> 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 05a8791db..f4e4f9c08 100644 --- a/sledge/src/domain_relation.ml +++ b/sledge/src/domain_relation.ml @@ -39,6 +39,10 @@ module Make (State_domain : State_domain_sig) = struct ( State_domain.join entry_a entry_b , State_domain.join current_a current_b ) + let joinN rs = + let entrys, currents = List.split rs in + (State_domain.joinN entrys, State_domain.joinN currents) + let exec_assume (entry, current) cnd = let+ next = State_domain.exec_assume current cnd in (entry, next) diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index b1564fd50..1509b3905 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -40,6 +40,13 @@ let join p q = |> [%Trace.retn fun {pf} -> pf "%a" pp] +let joinN qs = + [%Trace.call fun {pf} -> pf "@ %a" Sh.pp_djn qs] + ; + (match qs with [q] -> q | _ -> Sh.orN qs |> simplify) + |> + [%Trace.retn fun {pf} -> pf "%a" pp] + let dnf = Sh.dnf let exec_assume q b = diff --git a/sledge/src/domain_unit.ml b/sledge/src/domain_unit.ml index 8c55da22f..a92acc418 100644 --- a/sledge/src/domain_unit.ml +++ b/sledge/src/domain_unit.ml @@ -12,6 +12,7 @@ type t = unit [@@deriving compare, equal, sexp] let pp fs () = Format.pp_print_string fs "()" let init _ = () let join () () = () +let joinN _ = () 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 fcecfb7b6..3765bbca4 100644 --- a/sledge/src/domain_used_globals.ml +++ b/sledge/src/domain_used_globals.ml @@ -18,6 +18,7 @@ let init globals = empty let join l r = Llair.Global.Set.union l r +let joinN = function [] -> empty | x :: xs -> List.fold ~f:join xs x let recursion_beyond_bound = `skip let post _ _ state = state let retn _ _ from_call post = Llair.Global.Set.union from_call post diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli index c22d10a91..93d3af34c 100644 --- a/sledge/src/sh.mli +++ b/sledge/src/sh.mli @@ -59,6 +59,10 @@ val or_ : t -> t -> t (** Disjoin formulas, extending to a common vocabulary, and avoiding capturing existentials. *) +val orN : t list -> t +(** Disjoin formulas, extending to a common vocabulary, and avoiding + capturing existentials. *) + val pure : Formula.t -> t (** Atomic pure boolean constraint formula. *)