diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml index 2e7f6de091..a3eb1b6458 100644 --- a/src/analyses/extractPthread.ml +++ b/src/analyses/extractPthread.ml @@ -1197,7 +1197,7 @@ 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 @@ -1205,8 +1205,7 @@ module Spec : Analyses.MCPSpec = struct } 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 = diff --git a/src/arg/myARG.ml b/src/arg/myARG.ml index c41a442f10..0b31147bb3 100644 --- a/src/arg/myARG.ml +++ b/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 diff --git a/src/cdomain/value/cdomains/int/intervalSetDomain.ml b/src/cdomain/value/cdomains/int/intervalSetDomain.ml index 5f51be410e..52c028a520 100644 --- a/src/cdomain/value/cdomains/int/intervalSetDomain.ml +++ b/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 diff --git a/src/cdomain/value/cdomains/structDomain.ml b/src/cdomain/value/cdomains/structDomain.ml index 0b70034442..29277b0dab 100644 --- a/src/cdomain/value/cdomains/structDomain.ml +++ b/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) diff --git a/src/cdomains/congruenceClosure.ml b/src/cdomains/congruenceClosure.ml index 7470684b68..e914c98c9f 100644 --- a/src/cdomains/congruenceClosure.ml +++ b/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 diff --git a/src/domain/hoareDomain.ml b/src/domain/hoareDomain.ml index 42dd89265c..1bd56c0d1d 100644 --- a/src/domain/hoareDomain.ml +++ b/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 *) diff --git a/src/domains/intDomainProperties.ml b/src/domains/intDomainProperties.ml index 52e5cbe221..411cfb9895 100644 --- a/src/domains/intDomainProperties.ml +++ b/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 diff --git a/src/util/std/gobList.ml b/src/util/std/gobList.ml index a81544715e..137a1d63ff 100644 --- a/src/util/std/gobList.ml +++ b/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 = diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml index af52b14abd..dd476cb2a6 100644 --- a/tests/unit/cdomains/intDomainTest.ml +++ b/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 ) diff --git a/tests/unit/dune b/tests/unit/dune index 85038e1da6..3065d0820b 100644 --- a/tests/unit/dune +++ b/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 diff --git a/tests/unit/maindomaintest.ml b/tests/unit/maindomaintest.ml index 3191fa4f34..7e3693e65e 100644 --- a/tests/unit/maindomaintest.ml +++ b/tests/unit/maindomaintest.ml @@ -88,12 +88,11 @@ let nonAssocTestsuite = ) let old_intdomains intDomains = - BatList.cartesian_product intDomains ikinds - |> List.map (fun (d, ik) -> + GobList.cartesian_map (fun d ik -> let module D = (val d: IntDomainProperties.S2) in let module Ikind = struct let ikind () = ik end in (module IntDomainProperties.WithIkind (D) (Ikind): IntDomainProperties.OldSWithIkind) - ) + ) intDomains ikinds let intTestsuite = old_intdomains intDomains |> List.concat_map (fun d ->