Merge pull request #1890 from goblint/list-concat_map-map

Extract `GobLint.cartesian_*map` functions

Author: sim642

src/analyses/extractPthread.ml

@@ -1197,16 +1197,15 @@ module Spec : Analyses.MCPSpec = struct
       | Wait {cond = cond_var; mutex = mutex}, _, _ ->
         let cond_vars = ExprEval.eval_ptr man cond_var in
         let mutex_vars = ExprEval.eval_ptr man mutex in
-        let cond_var_action (v, m) =
+        let cond_var_action v m =
           let open Action in
           CondVarWait
             { cond_var_id = Tbls.CondVarIdTbl.get @@ Variable.show v
             ; mid = Tbls.MutexMidTbl.get @@ Variable.show m
             }
         in
         add_actions
-        @@ List.map cond_var_action
-        @@ List.cartesian_product cond_vars mutex_vars
+        @@ GobList.cartesian_map cond_var_action cond_vars mutex_vars
       | _ -> man.local
 
   let startstate v =

src/arg/myARG.ml

@@ -278,7 +278,7 @@ struct
   let next_opt _ = None
 end
 
-let cartesian_concat_paths (ps : cfg_path list) (qs : cfg_path list) : cfg_path list = List.concat_map (fun p -> List.map (fun q -> p @ q) qs) ps
+let cartesian_append: cfg_path list -> cfg_path list -> cfg_path list = GobList.cartesian_map (@)
 
 let partition_if_next if_next =
   let (if_next_trues, if_next_falses) = List.partition (function
@@ -318,8 +318,8 @@ struct
           if Node.equal if_false_next_n if_true_next_false_next_n then
             let exp = BinOp (LAnd, e, e2, intType) in
             Some [
-              (Test (exp, true), if_true_next_true_next_n, cartesian_concat_paths if_true_next_ps if_true_next_true_next_ps);
-              (Test (exp, false), if_true_next_false_next_n, if_false_next_ps @ cartesian_concat_paths if_true_next_ps if_true_next_false_next_ps) (* concat two different path families to same false node *)
+              (Test (exp, true), if_true_next_true_next_n, cartesian_append if_true_next_ps if_true_next_true_next_ps);
+              (Test (exp, false), if_true_next_false_next_n, if_false_next_ps @ cartesian_append if_true_next_ps if_true_next_false_next_ps) (* concat two different path families to same false node *)
             ]
           else
             None
@@ -330,8 +330,8 @@ struct
           if Node.equal if_true_next_n if_false_next_true_next_n then
             let exp = BinOp (LOr, e, e2, intType) in
             Some [
-              (Test (exp, true), if_false_next_true_next_n, if_true_next_ps @ cartesian_concat_paths if_false_next_ps if_false_next_true_next_ps); (* concat two different path families to same true node *)
-              (Test (exp, false), if_false_next_false_next_n, cartesian_concat_paths if_false_next_ps if_false_next_false_next_ps)
+              (Test (exp, true), if_false_next_true_next_n, if_true_next_ps @ cartesian_append if_false_next_ps if_false_next_true_next_ps); (* concat two different path families to same true node *)
+              (Test (exp, false), if_false_next_false_next_n, cartesian_append if_false_next_ps if_false_next_false_next_ps)
             ]
           else
             None
@@ -366,7 +366,7 @@ struct
         | [(Assign (v_true, e_true), if_true_next_next_n, if_true_next_next_ps)], [(Assign (v_false, e_false), if_false_next_next_n, if_false_next_next_ps)] when v_true = v_false && Node.equal if_true_next_next_n if_false_next_next_n ->
           let exp = ternary e_cond e_true e_false in
           Some [
-            (Assign (v_true, exp), if_true_next_next_n, cartesian_concat_paths if_true_next_ps if_true_next_next_ps @ cartesian_concat_paths if_false_next_ps if_false_next_next_ps) (* concat two different path families with same variable to same node *)
+            (Assign (v_true, exp), if_true_next_next_n, cartesian_append if_true_next_ps if_true_next_next_ps @ cartesian_append if_false_next_ps if_false_next_next_ps) (* concat two different path families with same variable to same node *)
           ]
         | _, _ -> None
       else

src/cdomain/value/cdomains/int/intervalSetDomain.ml

@@ -114,7 +114,7 @@ struct
   let binop (x: t) (y: t) op : t = match x, y with
     | [], _ -> []
     | _, [] -> []
-    | _, _ -> canonize @@ List.concat_map op (BatList.cartesian_product x y)
+    | _, _ -> canonize @@ GobList.cartesian_concat_map op x y
 
 
   include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)
@@ -185,18 +185,18 @@ struct
   let binary_op_with_norm op (ik:ikind) (x: t) (y: t) : t*overflow_info = match x, y with
     | [], _ -> ([],{overflow=false; underflow=false})
     | _, [] -> ([],{overflow=false; underflow=false})
-    | _, _ -> norm_intvs ik @@ List.map (fun (x,y) -> op x y) (BatList.cartesian_product x y)
+    | _, _ -> norm_intvs ik @@ GobList.cartesian_map op x y
 
   let binary_op_concat_with_norm op (ik:ikind) (x: t) (y: t) : t*overflow_info = match x, y with
     | [], _ -> ([],{overflow=false; underflow=false})
     | _, [] -> ([],{overflow=false; underflow=false})
-    | _, _ -> norm_intvs ik @@ List.concat_map (fun (x,y) -> op x y) (BatList.cartesian_product x y)
+    | _, _ -> norm_intvs ik @@ GobList.cartesian_concat_map op x y
 
   let binary_op_with_ovc (x: t) (y: t) op : t*overflow_info = match x, y with
     | [], _ -> ([],{overflow=false; underflow=false})
     | _, [] -> ([],{overflow=false; underflow=false})
     | _, _ ->
-      let res = List.map op (BatList.cartesian_product x y) in
+      let res = GobList.cartesian_map op x y in
       let intvs = List.concat_map fst res in
       let underflow = List.exists (fun (_,{underflow; _}) -> underflow) res in
       let overflow = List.exists (fun (_,{overflow; _}) -> underflow) res in
@@ -307,7 +307,7 @@ struct
   let interval_to_int i = Interval.to_int (Some i)
   let interval_to_bool i = Interval.to_bool (Some i)
 
-  let log f ik (i1, i2) =
+  let log f ik i1 i2 =
     match (interval_to_bool i1, interval_to_bool i2) with
     | Some x, Some y -> of_bool ik (f x y)
     | _ -> top_of ik
@@ -319,7 +319,7 @@ struct
     | _ -> top_of ik
 
 
-  let bitcomp f ik (i1, i2) =
+  let bitcomp f ik i1 i2 =
     match (interval_to_int i1, interval_to_int i2) with
     | Some x, Some y -> (try of_int ik (f x y) with Division_by_zero | Invalid_argument _ -> (top_of ik,{overflow=false; underflow=false}))
     | _, _ -> (top_of ik,{overflow=false; underflow=false})
@@ -340,7 +340,7 @@ struct
     Ints_t.sub (Ints_t.shift_left Ints_t.one (Z.numbits @@ Z.abs @@ Ints_t.to_bigint x)) Ints_t.one
 
   (* TODO: deduplicate with IntervalDomain? *)
-  let interval_logand ik (i1, i2) =
+  let interval_logand ik i1 i2 =
     match bit Ints_t.logand ik (i1, i2) with
     | result when not (is_top_of ik result) -> result
     | _ ->
@@ -361,7 +361,7 @@ struct
   let logand ik x y = binop x y (interval_logand ik)
 
   (* TODO: deduplicate with IntervalDomain? *)
-  let interval_logor ik (i1, i2) =
+  let interval_logor ik i1 i2 =
     match bit Ints_t.logor ik (i1, i2) with
     | result when not (is_top_of ik result) -> result
     | _ ->
@@ -381,7 +381,7 @@ struct
   let logor ik x y = binop x y (interval_logor ik)
 
   (* TODO: deduplicate with IntervalDomain? *)
-  let interval_logxor ik (i1, i2) =
+  let interval_logxor ik i1 i2 =
     match bit Ints_t.logxor ik (i1, i2) with
     | result when not (is_top_of ik result) && not (is_bot result) -> result (* TODO: why bot check here, but not elsewhere? *)
     | _ ->
@@ -426,7 +426,7 @@ struct
     binary_op_with_ovc x y interval_shiftleft
 
   (* TODO: deduplicate with IntervalDomain? *)
-  let interval_shiftright ik (i1, i2) =
+  let interval_shiftright ik i1 i2 =
     match interval_to_int i1, interval_to_int i2 with
     | Some x, Some y -> (try of_int ik (Ints_t.shift_right x (Ints_t.to_int y)) with Division_by_zero | Invalid_argument _ -> (top_of ik, {overflow=false; underflow=false}))
     | _, _ ->
@@ -472,7 +472,7 @@ struct
     binary_op_concat_with_norm interval_div ik x y
 
   let rem ik x y =
-    let interval_rem (x, y) =
+    let interval_rem x y =
       if Interval.is_top_of ik (Some x) && Interval.is_top_of ik (Some y) then
         top_of ik
       else

src/cdomain/value/cdomains/structDomain.ml

@@ -177,7 +177,8 @@ struct
     in
     let x_list = HS.elements x in
     let y_list = HS.elements y in
-    List.concat_map (fun xss -> List.map (fun yss -> (xss, yss)) y_list) x_list
+    (* TODO: GobList.cartesian_filter_map? or just Seq? *)
+    BatList.cartesian_product x_list y_list
     |> List.filter (fun (ssx, ssy) -> maps_overlap ssx ssy)
     |> List.map (fun (ssx, ssy) -> f ssx ssy)
     |> HS.of_list
@@ -195,7 +196,7 @@ struct
   let widen_with_fct f =
     let product_widen op a b = (* assumes b to be bigger than a *) (* from HS.product_widen *)
       let xs,ys = HS.elements a, HS.elements b in
-      List.concat_map (fun x -> List.map (fun y -> op x y) ys) xs |> fun x -> HS.of_list (List.append x ys)
+      GobList.cartesian_map op xs ys |> fun x -> HS.of_list (List.append x ys)
     in
     product_widen (fun x y -> if SS.leq x y then (SS.widen_with_fct f) x y else SS.bot ())
 
@@ -367,7 +368,7 @@ struct
       let ((sx, kx), (sy, ky)) = (x, y) in
       let x_list = HS.elements sx in
       let y_list = HS.elements sy in
-      let s = List.concat_map (fun xss -> List.map (fun yss -> (xss, yss)) y_list) x_list
+      let s = BatList.cartesian_product x_list y_list (* TODO: GobList.cartesian_filter_map? or just Seq? *)
               |> List.filter (fun (ssx, ssy) -> maps_overlap ssx ssy)
               |> List.map (fun (ssx, ssy) -> f ssx ssy)
               |> HS.of_list
@@ -395,7 +396,7 @@ struct
   let widen_with_fct f (x, kx) (y, ky) =
     let product_widen op a b = (* assumes b to be bigger than a *) (* from HS.product_widen *)
       let xs,ys = HS.elements a, HS.elements b in
-      List.concat_map (fun x -> List.map (op x) ys) xs |> fun x -> HS.of_list (List.append x ys)
+      GobList.cartesian_map op xs ys |> fun x -> HS.of_list (List.append x ys)
     in
     let s = product_widen (fun x y -> if SS.leq x y then (SS.widen_with_fct f) x y else SS.bot ()) x y
     in reduce_key (s, take_some_key kx ky s)

src/cdomains/congruenceClosure.ml

@@ -209,15 +209,12 @@ module Disequalities = struct
     let arg = List.fold_left do_bindings TMap.empty clist in
     (uf, cmap, arg)
 
+  (* TODO: GobList.cartesian_fold_left? *)
   let fold_left2 f acc l1 l2 =
     List.fold_left (
       fun acc x -> List.fold_left (
           fun acc y -> f acc x y) acc l2) acc l1
 
-  let map2 f l1 l2 =
-    let map_f x = List.map (f x) l2 in
-    List.concat_map map_f l1
-
   let map_find_opt (v,r) map =
     let inner_map = TMap.find_opt v map in
     BatOption.map_default (ZMap.find_opt r) None inner_map
@@ -382,10 +379,10 @@ module Disequalities = struct
     let comp_closure (r1,r2,z) =
       let eq_class1 = LMap.comp_t_cmap_repr cmap r1 in
       let eq_class2 = LMap.comp_t_cmap_repr cmap r2 in
-      let to_diseq ((z1, nt1), (z2, nt2)) =
+      let to_diseq (z1, nt1) (z2, nt2) =
         (nt1, nt2, Z.(-z2+z+z1))
       in
-      List.map to_diseq (BatList.cartesian_product eq_class1 eq_class2)
+      GobList.cartesian_map to_diseq eq_class1 eq_class2
     in
     List.concat_map comp_closure diseqs
 end

src/domain/hoareDomain.ml

@@ -199,10 +199,10 @@ struct
   let reduce s = filter (fun x -> not (exists (le x) s)) s
   let product_bot op a b =
     let a,b = elements a, elements b in
-    List.concat_map (fun x -> List.map (fun y -> op x y) b) a |> fun x -> reduce (of_list x)
+    GobList.cartesian_map op a b |> fun x -> reduce (of_list x)
   let product_widen op a b = (* assumes b to be bigger than a *)
     let xs,ys = elements a, elements b in
-    List.concat_map (fun x -> List.map (fun y -> op x y) ys) xs |> fun x -> reduce (union b (of_list x))
+    GobList.cartesian_map op xs ys |> fun x -> reduce (union b (of_list x))
   let widen = product_widen (fun x y -> if B.leq x y then B.widen x y else B.bot ())
   let narrow = product_bot (fun x y -> if B.leq y x then B.narrow x y else x)
 
@@ -302,18 +302,18 @@ struct
     maximals
   let product_bot op op2 a b =
     let a,b = elements a, elements b in
-    List.concat_map (fun (x,xr) -> List.map (fun (y,yr) -> (op x y, op2 xr yr)) b) a |> fun x -> reduce (of_list x)
+    GobList.cartesian_map (fun (x,xr) (y,yr) -> (op x y, op2 xr yr)) a b |> fun x -> reduce (of_list x)
   let product_bot2 op2 a b =
     let a,b = elements a, elements b in
-    List.concat_map (fun (x,xr) -> List.map (fun (y,yr) -> op2 (x, xr) (y, yr)) b) a |> fun x -> reduce (of_list x)
+    GobList.cartesian_map op2 a b |> fun x -> reduce (of_list x)
   (* why are type annotations needed for product_widen? *)
   (* TODO: unused now *)
   let product_widen op op2 (a:t) (b:t): t = (* assumes b to be bigger than a *)
     let xs,ys = elements a, elements b in
-    List.concat_map (fun (x,xr) -> List.map (fun (y,yr) -> (op x y, op2 xr yr)) ys) xs |> fun x -> reduce (join b (of_list x)) (* join instead of union because R is HoareDomain.Set for witness generation *)
+    GobList.cartesian_map (fun (x,xr) (y,yr) -> (op x y, op2 xr yr)) xs ys |> fun x -> reduce (join b (of_list x)) (* join instead of union because R is HoareDomain.Set for witness generation *)
   let product_widen2 op2 (a:t) (b:t): t = (* assumes b to be bigger than a *)
     let xs,ys = elements a, elements b in
-    List.concat_map (fun (x,xr) -> List.map (fun (y,yr) -> op2 (x, xr) (y, yr)) ys) xs |> fun x -> reduce (join b (of_list x)) (* join instead of union because R is HoareDomain.Set for witness generation *)
+    GobList.cartesian_map op2 xs ys |> fun x -> reduce (join b (of_list x)) (* join instead of union because R is HoareDomain.Set for witness generation *)
   let join a b = join a b |> reduce
   let meet = product_bot SpecD.meet R.inter
   (* let narrow = product_bot (fun x y -> if SpecD.leq y x then SpecD.narrow x y else x) R.narrow *)
@@ -368,7 +368,7 @@ struct
   (* TODO: move to Set above? *)
   let product_widen (op: elt -> elt -> elt option) a b = (* assumes b to be bigger than a *)
     let xs,ys = elements a, elements b in
-    List.concat_map (fun x -> List.filter_map (fun y -> op x y) ys) xs |> fun x -> join b (of_list x)
+    GobList.cartesian_filter_map op xs ys |> fun x -> join b (of_list x)
   let widen = product_widen (fun x y -> if E.leq x y then Some (E.widen x y) else None)
 
   (* above widen is actually extrapolation operator, so define connector-based widening instead *)

src/domains/intDomainProperties.ml

@@ -92,7 +92,7 @@ struct
   let name () = "integerset"
 
   let lift1 = map
-  let lift2 f x y = BatList.cartesian_product (elements x) (elements y) |> List.map (Batteries.uncurry f) |> of_list
+  let lift2 f x y = GobList.cartesian_map f (elements x) (elements y) |> of_list
 
   let neg  = lift1 Base.neg
   let add  = lift2 Base.add

src/util/std/gobList.ml

@@ -55,6 +55,15 @@ let until_last_with (pred: 'a -> bool) (xs: 'a list) =
   in
   until_last_helper [] [] xs
 
+let cartesian_map f l1 l2 =
+  List.concat_map (fun x -> List.map (f x) l2) l1
+
+let cartesian_filter_map f l1 l2 =
+  List.concat_map (fun x -> List.filter_map (f x) l2) l1
+
+let cartesian_concat_map f l1 l2 =
+  List.concat_map (fun x -> List.concat_map (f x) l2) l1
+
 
 (** Open this to use applicative functor/monad syntax for {!list}. *)
 module Syntax =

tests/unit/cdomains/intDomainTest.ml

@@ -483,7 +483,6 @@ struct
     assert_bool "-5 ?= not (4 | 12)" (I.equal_to (of_int (-5)) (I.lognot ik b12) = `Top)
 
   let of_list ik is = List.fold_left (fun acc x -> I.join ik acc (I.of_int ik x)) (I.bot ()) is
-  let cart_op op a b = List.map (BatTuple.Tuple2.uncurry op) (BatList.cartesian_product a b)
 
   let precision ik = snd @@ IntDomain.Size.bits ik
   let over_precision ik = Int.succ @@ precision ik
@@ -546,7 +545,7 @@ struct
     Test.make ~name:name ~print:shift_test_printer
       test_case_gen
       (fun (a,b) ->
-         let expected_subset = cart_op c_op a b |> of_list ik in
+         let expected_subset = GobList.cartesian_map c_op a b |> of_list ik in
          let result = a_op ik (of_list ik a) (of_list ik b) in
          I.leq expected_subset result
       )

tests/unit/dune

@@ -11,7 +11,7 @@
     )
   )
   (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson))
-  (flags :standard -linkall))
+  (flags :standard -open Goblint_std -linkall))
 
 (env
   (dev