Merge pull request #1313 from goblint/goblint-dune-libs-3

Organize constraint system and value domain modules into dune libraries
goblint · Dec 29, 2023 · 9d1dc02 · 9d1dc02
2 parents b671ffa + cedbc19
commit 9d1dc02
Show file tree

Hide file tree

Showing 82 changed files with 776 additions and 595 deletions.
diff --git a/gobview b/gobview
diff --git a/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py
@@ -8,6 +8,7 @@
 
 goblint_lib_paths = [
     src_root_path / "goblint_lib.ml",
+    src_root_path / "solver" / "goblint_solver.ml",
     src_root_path / "util" / "std" / "goblint_std.ml",
 ]
 goblint_lib_modules = set()
@@ -33,6 +34,7 @@
 
     # libraries
     "Goblint_std",
+    "Goblint_solver",
     "Goblint_timing",
     "Goblint_backtrace",
     "Goblint_tracing",

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -2871,7 +2871,7 @@ struct
         | "once" ->
           f (D.bot ())
         | "fixpoint" ->
-          let module DFP = LocalFixpoint.Make (D) in
+          let module DFP = Goblint_solver.LocalFixpoint.Make (D) in
           DFP.lfp f
         | _ ->
           assert false

diff --git a/src/analyses/wrapperFunctionAnalysis0.ml → ...alue/analyses/wrapperFunctionAnalysis0.ml b/src/analyses/wrapperFunctionAnalysis0.ml → ...alue/analyses/wrapperFunctionAnalysis0.ml
diff --git a/src/cdomain/value/cdomain_value.mld b/src/cdomain/value/cdomain_value.mld
@@ -0,0 +1,71 @@
+{0 Library goblint.cdomain.value}
+This library is unwrapped and provides the following top-level modules.
+For better context, see {!Goblint_lib} which also documents these modules.
+
+
+{1 Domains}
+
+{2 Analysis-specific}
+
+{3 Value}
+
+{4 Non-relational}
+
+{5 Numeric}
+{!modules:
+IntDomain
+FloatDomain
+}
+
+{5 Addresses}
+{!modules:
+Mval
+Offset
+StringDomain
+AddressDomain
+}
+
+{5 Complex}
+{!modules:
+StructDomain
+UnionDomain
+ArrayDomain
+NullByteSet
+JmpBufDomain
+}
+
+{5 Combined}
+{!modules:
+ValueDomain
+ValueDomainQueries
+}
+
+{3 Concurrency}
+{!modules:
+MutexAttrDomain
+ThreadIdDomain
+ConcDomain
+}
+
+{3 Other}
+{!modules:
+Lval
+}
+
+
+{1 I/O}
+
+{2 Witnesses}
+{!modules:
+Invariant
+InvariantCil
+}
+
+
+{1 Utilities}
+
+{2 Analysis-specific}
+{!modules:
+PrecisionUtil
+WideningThresholds
+}
diff --git a/src/cdomains/addressDomain.ml → src/cdomain/value/cdomains/addressDomain.ml b/src/cdomains/addressDomain.ml → src/cdomain/value/cdomains/addressDomain.ml
diff --git a/src/cdomains/addressDomain.mli → src/cdomain/value/cdomains/addressDomain.mli b/src/cdomains/addressDomain.mli → src/cdomain/value/cdomains/addressDomain.mli
diff --git a/src/cdomains/addressDomain_intf.ml → ...main/value/cdomains/addressDomain_intf.ml b/src/cdomains/addressDomain_intf.ml → ...main/value/cdomains/addressDomain_intf.ml
diff --git a/src/cdomains/arrayDomain.ml → src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml → src/cdomain/value/cdomains/arrayDomain.ml
diff --git a/src/cdomains/arrayDomain.mli → src/cdomain/value/cdomains/arrayDomain.mli b/src/cdomains/arrayDomain.mli → src/cdomain/value/cdomains/arrayDomain.mli
diff --git a/src/cdomains/concDomain.ml → src/cdomain/value/cdomains/concDomain.ml b/src/cdomains/concDomain.ml → src/cdomain/value/cdomains/concDomain.ml
diff --git a/src/cdomains/floatDomain.ml → src/cdomain/value/cdomains/floatDomain.ml b/src/cdomains/floatDomain.ml → src/cdomain/value/cdomains/floatDomain.ml
diff --git a/src/cdomains/floatDomain.mli → src/cdomain/value/cdomains/floatDomain.mli b/src/cdomains/floatDomain.mli → src/cdomain/value/cdomains/floatDomain.mli
diff --git a/src/cdomains/intDomain.ml → src/cdomain/value/cdomains/intDomain.ml b/src/cdomains/intDomain.ml → src/cdomain/value/cdomains/intDomain.ml
diff --git a/src/cdomains/intDomain.mli → src/cdomain/value/cdomains/intDomain.mli b/src/cdomains/intDomain.mli → src/cdomain/value/cdomains/intDomain.mli
diff --git a/src/cdomains/jmpBufDomain.ml → src/cdomain/value/cdomains/jmpBufDomain.ml b/src/cdomains/jmpBufDomain.ml → src/cdomain/value/cdomains/jmpBufDomain.ml
diff --git a/src/cdomains/lval.ml → src/cdomain/value/cdomains/lval.ml b/src/cdomains/lval.ml → src/cdomain/value/cdomains/lval.ml
diff --git a/src/cdomains/mutexAttrDomain.ml → ...cdomain/value/cdomains/mutexAttrDomain.ml b/src/cdomains/mutexAttrDomain.ml → ...cdomain/value/cdomains/mutexAttrDomain.ml
diff --git a/src/cdomains/mval.ml → src/cdomain/value/cdomains/mval.ml b/src/cdomains/mval.ml → src/cdomain/value/cdomains/mval.ml
diff --git a/src/cdomains/mval.mli → src/cdomain/value/cdomains/mval.mli b/src/cdomains/mval.mli → src/cdomain/value/cdomains/mval.mli
diff --git a/src/cdomains/mval_intf.ml → src/cdomain/value/cdomains/mval_intf.ml b/src/cdomains/mval_intf.ml → src/cdomain/value/cdomains/mval_intf.ml
diff --git a/src/cdomains/nullByteSet.ml → src/cdomain/value/cdomains/nullByteSet.ml b/src/cdomains/nullByteSet.ml → src/cdomain/value/cdomains/nullByteSet.ml
diff --git a/src/cdomains/offset.ml → src/cdomain/value/cdomains/offset.ml b/src/cdomains/offset.ml → src/cdomain/value/cdomains/offset.ml
diff --git a/src/cdomains/offset.mli → src/cdomain/value/cdomains/offset.mli b/src/cdomains/offset.mli → src/cdomain/value/cdomains/offset.mli
diff --git a/src/cdomains/offset_intf.ml → src/cdomain/value/cdomains/offset_intf.ml b/src/cdomains/offset_intf.ml → src/cdomain/value/cdomains/offset_intf.ml
diff --git a/src/cdomains/preValueDomain.ml → src/cdomain/value/cdomains/preValueDomain.ml b/src/cdomains/preValueDomain.ml → src/cdomain/value/cdomains/preValueDomain.ml
diff --git a/src/cdomains/stringDomain.ml → src/cdomain/value/cdomains/stringDomain.ml b/src/cdomains/stringDomain.ml → src/cdomain/value/cdomains/stringDomain.ml
diff --git a/src/cdomains/stringDomain.mli → src/cdomain/value/cdomains/stringDomain.mli b/src/cdomains/stringDomain.mli → src/cdomain/value/cdomains/stringDomain.mli
diff --git a/src/cdomains/structDomain.ml → src/cdomain/value/cdomains/structDomain.ml b/src/cdomains/structDomain.ml → src/cdomain/value/cdomains/structDomain.ml
diff --git a/src/cdomains/structDomain.mli → src/cdomain/value/cdomains/structDomain.mli b/src/cdomains/structDomain.mli → src/cdomain/value/cdomains/structDomain.mli
diff --git a/src/cdomains/threadIdDomain.ml → src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomains/threadIdDomain.ml → src/cdomain/value/cdomains/threadIdDomain.ml
diff --git a/src/cdomains/unionDomain.ml → src/cdomain/value/cdomains/unionDomain.ml b/src/cdomains/unionDomain.ml → src/cdomain/value/cdomains/unionDomain.ml
diff --git a/src/cdomains/valueDomain.ml → src/cdomain/value/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml → src/cdomain/value/cdomains/valueDomain.ml
diff --git a/src/domains/invariant.ml → src/cdomain/value/domains/invariant.ml b/src/domains/invariant.ml → src/cdomain/value/domains/invariant.ml
diff --git a/src/domains/invariantCil.ml → src/cdomain/value/domains/invariantCil.ml b/src/domains/invariantCil.ml → src/cdomain/value/domains/invariantCil.ml
diff --git a/src/domains/valueDomainQueries.ml → ...omain/value/domains/valueDomainQueries.ml b/src/domains/valueDomainQueries.ml → ...omain/value/domains/valueDomainQueries.ml
diff --git a/src/cdomain/value/dune b/src/cdomain/value/dune
@@ -0,0 +1,24 @@
+(include_subdirs unqualified)
+
+(library
+ (name goblint_cdomain_value)
+ (public_name goblint.cdomain.value)
+ (wrapped false) ; TODO: wrap
+ (libraries
+   batteries.unthreaded
+   goblint_std
+   goblint_common
+   goblint_config
+   goblint_library
+   goblint_domain
+   goblint_incremental
+   goblint-cil)
+ (flags :standard -open Goblint_std)
+ (preprocess
+  (pps
+    ppx_deriving.std
+    ppx_deriving_hash
+    ppx_deriving_yojson))
+ (instrumentation (backend bisect_ppx)))
+
+(documentation)
diff --git a/src/util/precisionUtil.ml → src/cdomain/value/util/precisionUtil.ml b/src/util/precisionUtil.ml → src/cdomain/value/util/precisionUtil.ml
diff --git a/src/util/wideningThresholds.ml → src/cdomain/value/util/wideningThresholds.ml b/src/util/wideningThresholds.ml → src/cdomain/value/util/wideningThresholds.ml
diff --git a/src/util/wideningThresholds.mli → ...cdomain/value/util/wideningThresholds.mli b/src/util/wideningThresholds.mli → ...cdomain/value/util/wideningThresholds.mli
diff --git a/src/cdomains/floatOps/floatOps.ml → src/common/cdomains/floatOps/floatOps.ml b/src/cdomains/floatOps/floatOps.ml → src/common/cdomains/floatOps/floatOps.ml
diff --git a/src/cdomains/floatOps/floatOps.mli → src/common/cdomains/floatOps/floatOps.mli b/src/cdomains/floatOps/floatOps.mli → src/common/cdomains/floatOps/floatOps.mli
diff --git a/src/cdomains/floatOps/stubs.c → src/common/cdomains/floatOps/stubs.c b/src/cdomains/floatOps/stubs.c → src/common/cdomains/floatOps/stubs.c
diff --git a/src/common/common.mld b/src/common/common.mld
@@ -16,6 +16,7 @@ CfgTools
 {2 Specification}
 {!modules:
 AnalysisState
+AnalysisStateUtil
 ControlSpecC
 }
 
@@ -42,6 +43,7 @@ Messages
 
 {2 General}
 {!modules:
+IntOps
 LazyEval
 ResettableLazy
 MessageUtil
@@ -55,6 +57,11 @@ Cilfacade
 RichVarinfo
 }
 
+{2 Analysis-specific}
+{!modules:
+ContextUtil
+}
+
 
 {1 Library extensions}
 

diff --git a/src/common/dune b/src/common/dune
@@ -16,6 +16,8 @@
    goblint_timing
    qcheck-core.runner)
  (flags :standard -open Goblint_std)
+ (foreign_stubs (language c) (names stubs))
+ (ocamlopt_flags :standard -no-float-const-prop)
  (preprocess
   (pps
     ppx_deriving.std

diff --git a/src/util/analysisStateUtil.ml → src/common/util/analysisStateUtil.ml b/src/util/analysisStateUtil.ml → src/common/util/analysisStateUtil.ml
diff --git a/src/util/contextUtil.ml → src/common/util/contextUtil.ml b/src/util/contextUtil.ml → src/common/util/contextUtil.ml
diff --git a/src/util/intOps.ml → src/common/util/intOps.ml b/src/util/intOps.ml → src/common/util/intOps.ml