[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

@@ -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) =

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)
 

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

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)

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 =

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

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

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. *)