Use Seq instead of constructing from scratch

Author: michael-schwarz

src/analyses/pthreadBarriers.ml

@@ -52,6 +52,19 @@ struct
     Queries.AD.to_var_may (a.f (Queries.MayPointTo barrier))
 
   let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    let exists_k pred k waiters =
+      let k_product elems =
+        let rec doit k =
+          if k = 1 then
+            Seq.map (Seq.return) elems
+          else
+            let arg = doit (k-1) in
+            Seq.map_product (Seq.cons) elems arg
+        in
+        doit k
+      in
+      Seq.exists pred (k_product (Waiters.to_seq waiters))
+    in
     let desc = LF.find f in
     match desc.special arglist with
     | BarrierWait barrier ->
@@ -88,16 +101,14 @@ struct
                   let must =
                     let waiters = Waiters.elements relevant_waiters in
                     let min_cap = Z.to_int min_cap in
-                    let lists = List.init (min_cap - 1) (fun _ -> waiters) in
-                    let candidates = BatList.n_cartesian_product lists in
-                    let can_proceed = List.exists (fun candidate ->
-                        let rec do_it = function
-                          | [] -> true
-                          | x::xs -> List.for_all (fun y -> MHPplusLock.mhp x y) xs  && do_it xs
-                        in
-                        do_it candidate
-                      ) candidates
+                    let can_proceed_pred seq =
+                      let rec doit seq = match Seq.uncons seq with
+                        | None -> true
+                        | Some (h, t) -> Seq.for_all (MHPplusLock.mhp h) t && doit t
+                      in
+                      doit seq
                     in
+                    let can_proceed = exists_k can_proceed_pred (min_cap - 1) relevant_waiters in
                     if not can_proceed then raise Analyses.Deadcode;
                     (* limit to this case to avoid having to construct all permutations above *)
                     if BatList.compare_length_with waiters (min_cap - 1) = 0 then

src/domain/disjointDomain.ml

@@ -117,6 +117,7 @@ struct
       add e acc
     ) (empty ()) es
   let elements m = fold List.cons m [] (* no intermediate per-bucket lists *)
+  let to_seq m = fold Seq.cons m Seq.empty
   let map f m = fold (fun e acc ->
       add (f e) acc
     ) m (empty ()) (* no intermediate lists *)
@@ -323,6 +324,7 @@ struct
       add e acc
     ) (empty ()) es
   let elements m = fold List.cons m [] (* no intermediate per-bucket lists *)
+  let to_seq m = fold Seq.cons m Seq.empty
   let map f s = fold (fun e acc ->
       add (f e) acc
     ) s (empty ()) (* no intermediate lists *)

src/domain/setDomain.ml

@@ -95,6 +95,12 @@ sig
       On set abstractions this lists only canonical elements,
       not all subsumed elements. *)
 
+  val to_seq: t -> elt Seq.t
+  (** See {!Set.S.to_seq}.
+
+      On set abstractions this lists only canonical elements,
+      not all subsumed elements. *)
+
   val of_list: elt list -> t
 
   val min_elt: t -> elt
@@ -332,6 +338,7 @@ struct
   let exists f = schema_default true (S.exists f)
   let filter f = schema (fun t -> `Lifted (S.filter f t)) "filter on `Top"
   let elements = schema S.elements "elements on `Top"
+  let to_seq = schema S.to_seq "to_seq on `Top"
   let of_list xs = `Lifted (S.of_list xs)
   let cardinal = schema S.cardinal "cardinal on `Top"
   let min_elt = schema S.min_elt "min_elt on `Top"
@@ -471,6 +478,7 @@ struct
   let mem e e' = E.leq e e'
   let choose e = e
   let elements e = [e]
+  let to_seq e = Seq.return e
   let remove e e' =
     if E.leq e' e then
       E.bot () (* NB! strong removal *)