Organize more common modules into dune libraries

src/analyses/mCPRegistry.ml

@@ -215,7 +215,7 @@ struct
 
   let arbitrary () =
     let arbs = map (fun (n, (module D: Printable.S)) -> QCheck.map ~rev:(fun (_, o) -> obj o) (fun x -> (n, repr x)) @@ D.arbitrary ()) @@ domain_list () in
-    MyCheck.Arbitrary.sequence arbs
+    GobQCheck.Arbitrary.sequence arbs
 
   let relift = unop_map (fun (module S: Printable.S) x -> Obj.repr (S.relift (Obj.obj x)))
 end

src/cdomains/intDomain.ml

@@ -996,12 +996,12 @@ struct
 
   let arbitrary ik =
     let open QCheck.Iter in
-    (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint MyCheck.Arbitrary.big_int in *)
+    (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint GobQCheck.Arbitrary.big_int in *)
     (* TODO: apparently bigints are really slow compared to int64 for domaintest *)
-    let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 in
+    let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in
     let pair_arb = QCheck.pair int_arb int_arb in
     let shrink = function
-      | Some (l, u) -> (return None) <+> (MyCheck.shrink pair_arb (l, u) >|= of_interval ik >|= fst)
+      | Some (l, u) -> (return None) <+> (GobQCheck.shrink pair_arb (l, u) >|= of_interval ik >|= fst)
       | None -> empty
     in
     QCheck.(set_shrink shrink @@ set_print show @@ map (*~rev:BatOption.get*) (fun x -> of_interval ik x |> fst ) pair_arb)
@@ -1601,13 +1601,13 @@ struct
 
   let arbitrary ik =
     let open QCheck.Iter in
-    (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint MyCheck.Arbitrary.big_int in *)
+    (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint GobQCheck.Arbitrary.big_int in *)
     (* TODO: apparently bigints are really slow compared to int64 for domaintest *)
-    let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 in
+    let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in
     let pair_arb = QCheck.pair int_arb int_arb in
     let list_pair_arb = QCheck.small_list pair_arb in
     let canonize_randomly_generated_list = (fun x -> norm_intvs ik  x |> fst) in
-    let shrink xs = MyCheck.shrink list_pair_arb xs >|= canonize_randomly_generated_list
+    let shrink xs = GobQCheck.shrink list_pair_arb xs >|= canonize_randomly_generated_list
     in QCheck.(set_shrink shrink @@ set_print show @@ map (*~rev:BatOption.get*) canonize_randomly_generated_list list_pair_arb)
 end
 
@@ -1695,7 +1695,7 @@ struct
   let logand n1 n2 = of_bool ((to_bool' n1) && (to_bool' n2))
   let logor  n1 n2 = of_bool ((to_bool' n1) || (to_bool' n2))
   let cast_to ?torg t x =  failwith @@ "Cast_to not implemented for " ^ (name ()) ^ "."
-  let arbitrary ik = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 (* TODO: use ikind *)
+  let arbitrary ik = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 (* TODO: use ikind *)
   let invariant _ _ = Invariant.none (* TODO *)
 end
 
@@ -2402,8 +2402,8 @@ struct
     let excluded s = from_excl ik s in
     let definite x = of_int ik x in
     let shrink = function
-      | `Excluded (s, _) -> MyCheck.shrink (S.arbitrary ()) s >|= excluded (* S TODO: possibly shrink excluded to definite *)
-      | `Definite x -> (return `Bot) <+> (MyCheck.shrink (BigInt.arbitrary ()) x >|= definite)
+      | `Excluded (s, _) -> GobQCheck.shrink (S.arbitrary ()) s >|= excluded (* S TODO: possibly shrink excluded to definite *)
+      | `Definite x -> (return `Bot) <+> (GobQCheck.shrink (BigInt.arbitrary ()) x >|= definite)
       | `Bot -> empty
     in
     QCheck.frequency ~shrink ~print:show [
@@ -2816,8 +2816,8 @@ module Enums : S with type int_t = BigInt.t = struct
     let neg s = of_excl_list ik (BISet.elements s) in
     let pos s = norm ik (Inc s) in
     let shrink = function
-      | Exc (s, _) -> MyCheck.shrink (BISet.arbitrary ()) s >|= neg (* S TODO: possibly shrink neg to pos *)
-      | Inc s -> MyCheck.shrink (BISet.arbitrary ()) s >|= pos
+      | Exc (s, _) -> GobQCheck.shrink (BISet.arbitrary ()) s >|= neg (* S TODO: possibly shrink neg to pos *)
+      | Inc s -> GobQCheck.shrink (BISet.arbitrary ()) s >|= pos
     in
     QCheck.frequency ~shrink ~print:show [
       20, QCheck.map neg (BISet.arbitrary ());
@@ -3307,7 +3307,7 @@ struct
 
   let arbitrary ik =
     let open QCheck in
-    let int_arb = map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 in
+    let int_arb = map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in
     let cong_arb = pair int_arb int_arb in
     let of_pair ik p = normalize ik (Some p) in
     let to_pair = Option.get in

src/common/cdomains/basetype.ml

@@ -20,8 +20,6 @@ struct
     | _ -> Local
   let name () = "variables"
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
-
-  let arbitrary () = MyCheck.Arbitrary.varinfo
 end
 
 module RawStrings: Printable.S with type t = string =
@@ -35,12 +33,6 @@ struct
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
 end
 
-module Strings: Lattice.S with type t = [`Bot | `Lifted of string | `Top] =
-  Lattice.Flat (RawStrings) (struct
-    let top_name = "?"
-    let bot_name = "-"
-  end)
-
 module RawBools: Printable.S with type t = bool =
 struct
   include Printable.StdLeaf
@@ -52,12 +44,6 @@ struct
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (show x)
 end
 
-module Bools: Lattice.S with type t = [`Bot | `Lifted of bool | `Top] =
-  Lattice.Flat (RawBools) (struct
-    let top_name = "?"
-    let bot_name = "-"
-  end)
-
 module CilExp =
 struct
   include CilType.Exp

src/common/common.mld

@@ -69,6 +69,3 @@ RichVarinfo
 
 {2 Standard library}
 {!modules:GobFormat}
-
-{2 Other libraries}
-{!modules:MyCheck}

src/common/domains/lattice.ml

@@ -148,18 +148,14 @@ struct
 end
 
 (* HAS SIDE-EFFECTS ---- PLEASE INSTANCIATE ONLY ONCE!!! *)
-module HConsed (Base:S) =
+module HConsed (Base:S) (Arg: sig val assume_idempotent: bool end) =
 struct
   include Printable.HConsed (Base)
 
-  (* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues if we assume x op x = x *)
-  (* see https://github.com/goblint/analyzer/issues/1005 *)
-  let int_refine_active = GobConfig.get_string "ana.int.refinement" <> "never"
-
   let lift_f2 f x y = f (unlift x) (unlift y)
-  let narrow x y = if (not int_refine_active) && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.narrow x y)
+  let narrow x y = if Arg.assume_idempotent && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.narrow x y)
   let widen x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.widen x y)
-  let meet x y = if (not int_refine_active) && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.meet x y)
+  let meet x y = if Arg.assume_idempotent && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.meet x y)
   let join x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.join x y)
   let leq x y = (x.BatHashcons.tag == y.BatHashcons.tag) || lift_f2 Base.leq x y
   let is_top = lift_f Base.is_top

src/common/domains/printable.ml

@@ -233,9 +233,9 @@ struct
   let arbitrary () =
     let open QCheck.Iter in
     let shrink = function
-      | `Lifted x -> (return `Bot) <+> (MyCheck.shrink (Base.arbitrary ()) x >|= lift)
+      | `Lifted x -> (return `Bot) <+> (GobQCheck.shrink (Base.arbitrary ()) x >|= lift)
       | `Bot -> empty
-      | `Top -> MyCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift
+      | `Top -> GobQCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift
     in
     QCheck.frequency ~shrink ~print:show [
       20, QCheck.map lift (Base.arbitrary ());
@@ -626,8 +626,8 @@ struct
   let arbitrary () =
     let open QCheck.Iter in
     let shrink = function
-      | `Lifted x -> MyCheck.shrink (Base.arbitrary ()) x >|= lift
-      | `Top -> MyCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift
+      | `Lifted x -> GobQCheck.shrink (Base.arbitrary ()) x >|= lift
+      | `Top -> GobQCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift
     in
     QCheck.frequency ~shrink ~print:show [
       20, QCheck.map lift (Base.arbitrary ());

src/domains/boolDomain.ml

@@ -38,4 +38,10 @@ struct
   let widen = (&&)
   let meet = (||)
   let narrow = (||)
-end
+end
+
+module FlatBool: Lattice.S with type t = [`Bot | `Lifted of bool | `Top] =
+  Lattice.Flat (Bool) (struct
+    let top_name = "?"
+    let bot_name = "-"
+  end)

src/domains/mapDomain.ml

@@ -263,7 +263,7 @@ module HConsed (M: S) : S with
   type key = M.key and
   type value = M.value =
 struct
-  include Lattice.HConsed (M)
+  include Lattice.HConsed (M) (struct let assume_idempotent = false end)
 
   type key = M.key
   type value = M.value

src/domains/queries.ml

@@ -32,7 +32,11 @@ module FlatYojson = Lattice.Flat (Printable.Yojson) (struct
     let bot_name = "bot yojson"
   end)
 
-module SD = Basetype.Strings
+module SD: Lattice.S with type t = [`Bot | `Lifted of string | `Top] =
+  Lattice.Flat (Basetype.RawStrings) (struct
+    let top_name = "?"
+    let bot_name = "-"
+  end)
 module VD = ValueDomain.Compound
 module AD = ValueDomain.AD
 

src/framework/constraints.ml

@@ -12,12 +12,17 @@ module M = Messages
 
 (** Lifts a [Spec] so that the domain is [Hashcons]d *)
 module HashconsLifter (S:Spec)
-  : Spec with module D = Lattice.HConsed (S.D)
-          and module G = S.G
+  : Spec with module G = S.G
           and module C = S.C
 =
 struct
-  module D = Lattice.HConsed (S.D)
+  module HConsedArg =
+  struct
+    (* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues if we assume x op x = x *)
+    (* see https://github.com/goblint/analyzer/issues/1005 *)
+    let assume_idempotent = GobConfig.get_string "ana.int.refinement" = "never"
+  end
+  module D = Lattice.HConsed (S.D) (HConsedArg)
   module G = S.G
   module C = S.C
   module V = S.V
@@ -1344,7 +1349,7 @@ struct
 
   module EM =
   struct
-    include MapDomain.MapBot (Basetype.CilExp) (Basetype.Bools)
+    include MapDomain.MapBot (Basetype.CilExp) (BoolDomain.FlatBool)
     let name () = "branches"
   end
 

src/goblint_lib.ml

@@ -461,9 +461,3 @@ module ApronPrecCompareUtil = ApronPrecCompareUtil
     OCaml standard library extensions which are not provided by {!Batteries}. *)
 
 module GobFormat = GobFormat
-
-(** {2 Other libraries}
-
-    External library extensions. *)
-
-module MyCheck = MyCheck

src/util/std/dune

@@ -9,7 +9,8 @@
    goblint-cil
    fpath
    yojson
-   yaml)
+   yaml
+   qcheck-core)
  (preprocess
   (pps
    ppx_deriving.std

src/common/domains/myCheck.ml → src/util/std/gobQCheck.ml

@@ -56,7 +56,4 @@ struct
     let gens = List.map gen arbs in
     let shrinks = List.map shrink arbs in
     make ~shrink:(Shrink.sequence shrinks) (Gen.sequence gens)
-
-  open GoblintCil
-  let varinfo: Cil.varinfo arbitrary = QCheck.always (Cil.makeGlobalVar "arbVar" Cil.voidPtrType) (* S TODO: how to generate this *)
 end

src/util/std/goblint_std.ml

@@ -19,6 +19,7 @@ module GobUnix = GobUnix
 
 module GobFpath = GobFpath
 module GobPretty = GobPretty
+module GobQCheck = GobQCheck
 module GobYaml = GobYaml
 module GobYojson = GobYojson
 module GobZ = GobZ

unittest/util/intOpsTest.ml

@@ -10,13 +10,13 @@ let old_div a b = if Z.lt a Z.zero then Z.neg (Z.ediv (Z.neg a) b) else Z.ediv a
 let old_rem a b = Z.sub a (Z.mul b (old_div a b))
 
 let test_bigint_div =
-  QCheck.(Test.make ~name:"div" (pair MyCheck.Arbitrary.big_int MyCheck.Arbitrary.big_int) (fun (x, y) ->
+  QCheck.(Test.make ~name:"div" (pair GobQCheck.Arbitrary.big_int GobQCheck.Arbitrary.big_int) (fun (x, y) ->
       assume (Z.compare y Z.zero <> 0);
       Z.equal (Z.div x y) (old_div x y)
     ))
 
 let test_bigint_rem =
-  QCheck.(Test.make ~name:"rem" (pair MyCheck.Arbitrary.big_int MyCheck.Arbitrary.big_int) (fun (x, y) ->
+  QCheck.(Test.make ~name:"rem" (pair GobQCheck.Arbitrary.big_int GobQCheck.Arbitrary.big_int) (fun (x, y) ->
       assume (Z.compare y Z.zero <> 0);
       Z.equal (Z.rem x y) (old_rem x y)
     ))