Merge pull request #1206 from goblint/goblint-dune-libs

Organize some general modules into dune libraries

.github/workflows/options.yml

@@ -26,10 +26,10 @@ jobs:
         run: npm install -g ajv-cli
 
       - name: Migrate schema # https://github.com/ajv-validator/ajv-cli/issues/199
-        run: ajv migrate -s src/util/options.schema.json
+        run: ajv migrate -s src/common/util/options.schema.json
 
       - name: Validate conf
-        run: ajv validate -s src/util/options.schema.json -d "conf/**/*.json"
+        run: ajv validate -s src/common/util/options.schema.json -d "conf/**/*.json"
 
       - name: Validate incremental tests
-        run: ajv validate -s src/util/options.schema.json -d "tests/incremental/*/*.json"
+        run: ajv validate -s src/common/util/options.schema.json -d "tests/incremental/*/*.json"

.readthedocs.yaml

@@ -20,4 +20,4 @@ build:
       - pip install json-schema-for-humans
     post_build:
       - mkdir _readthedocs/html/jsfh/
-      - generate-schema-doc --config-file jsfh.yml src/util/options.schema.json _readthedocs/html/jsfh/
+      - generate-schema-doc --config-file jsfh.yml src/common/util/options.schema.json _readthedocs/html/jsfh/

docs/user-guide/configuring.md

@@ -24,7 +24,7 @@ In `.vscode/settings.json` add the following:
                 "/conf/*.json",
                 "/tests/incremental/*/*.json"
             ],
-            "url": "/src/util/options.schema.json"
+            "url": "/src/common/util/options.schema.json"
         }
     ]
 }

mkdocs.yml

@@ -30,7 +30,7 @@ nav:
     - 👶 Your first analysis: developer-guide/firstanalysis.md
     - 🏫 Extending library: developer-guide/extending-library.md
     - 📢 Messaging: developer-guide/messaging.md
-    - 🗃️ API reference: https://goblint.github.io/analyzer/
+    - 🗃️ API reference: https://goblint.github.io/analyzer/goblint/
     - 🚨 Testing: developer-guide/testing.md
     - 🪲 Debugging: developer-guide/debugging.md
     - 📉 Profiling: developer-guide/profiling.md

src/build-info/.gitignore

@@ -0,0 +1 @@
+config*.ml

src/build-info/dune

@@ -8,4 +8,22 @@
 (library
   (name goblint_build_info)
   (public_name goblint.build-info)
-  (virtual_modules goblint_build_info))
+  (libraries batteries.unthreaded)
+  (virtual_modules dune_build_info))
+
+(rule
+  (target configVersion.ml)
+  (mode (promote (until-clean) (only configVersion.ml))) ; replace existing file in source tree, even if releasing (only overrides)
+  (deps (universe)) ; do not cache, always regenerate
+  (action (pipe-stdout (bash "git describe --all --long --dirty || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet version = \"%s\"'")))))
+
+(rule
+  (target configProfile.ml)
+  (mode (promote (until-clean) (only configProfile.ml))) ; replace existing file in source tree, even if releasing (only overrides)
+  (action (write-file %{target} "(* Automatically regenerated, changes do not persist! *)\nlet profile = \"%{profile}\"")))
+
+(rule
+  (target configOcaml.ml)
+  (mode (promote (until-clean) (only configOcaml.ml))) ; replace existing file in source tree, even if releasing (only overrides)
+  (action (write-file %{target} "(* Automatically regenerated, changes do not persist! *)\nlet flambda = \"%{ocaml-config:flambda}\"")))
+

src/build-info/goblint_build_info.ml

@@ -0,0 +1,34 @@
+(** Goblint build info. *)
+
+(** OCaml compiler flambda status. *)
+let ocaml_flambda = ConfigOcaml.flambda
+
+(** Dune profile. *)
+let dune_profile = ConfigProfile.profile
+
+(** Goblint version from git. *)
+let git_version = ConfigVersion.version
+
+(** Goblint version from release archive. *)
+let release_version = "%%VERSION_NUM%%"
+
+(** Goblint git commit from release archive. *)
+let release_commit = "%%VCS_COMMIT_ID%%"
+
+(** Goblint version. *)
+let version =
+  let commit = ConfigVersion.version in
+  if BatString.starts_with release_version "%" then
+    commit
+  else (
+    let commit =
+      if commit = "n/a" then (* released archive has no .git *)
+        release_commit
+      else
+        commit
+    in
+    Format.sprintf "%s (%s)" release_version commit
+  )
+
+(** Statically linked libraries with versions. *)
+let statically_linked_libraries = Dune_build_info.statically_linked_libraries

src/common/common.mld

@@ -0,0 +1,74 @@
+{0 Library goblint.common}
+This library is unwrapped and provides the following top-level modules.
+For better context, see {!Goblint_lib} which also documents these modules.
+
+
+{1 Framework}
+
+{2 CFG}
+{!modules:
+Node
+Edge
+MyCFG
+}
+
+{2 Specification}
+{!modules:
+AnalysisState
+ControlSpecC
+}
+
+{2 Configuration}
+{!modules:
+GobConfig
+AfterConfig
+JsonSchema
+Options
+}
+
+
+{1 Domains}
+{!modules:
+Printable
+Lattice
+}
+
+{2 Analysis-specific}
+
+{3 Other}
+{!modules:Basetype}
+
+
+{1 I/O}
+{!modules:
+Messages
+Tracing
+}
+
+
+{1 Utilities}
+{!modules:Timing}
+
+{2 General}
+{!modules:
+LazyEval
+ResettableLazy
+MessageUtil
+XmlUtil
+}
+
+{2 CIL}
+{!modules:
+CilType
+Cilfacade
+RichVarinfo
+}
+
+
+{1 Library extensions}
+
+{2 Standard library}
+{!modules:GobFormat}
+
+{2 Other libraries}
+{!modules:MyCheck}

src/domains/lattice.ml → src/common/domains/lattice.ml

@@ -4,12 +4,12 @@
 module Pretty = GoblintCil.Pretty
 
 (* module type Rel =
-sig
-  type t
-  type relation = Less | Equal | Greater | Uncomparable
-  val rel : t -> t -> relation
-  val in_rel : t -> relation -> t -> bool
-end *)
+   sig
+     type t
+     type relation = Less | Equal | Greater | Uncomparable
+     val rel : t -> t -> relation
+     val in_rel : t -> relation -> t -> bool
+   end *)
 
 (* partial order: elements might not be comparable and no bot/top -> join etc. might fail with exception Uncomparable *)
 exception Uncomparable
@@ -324,14 +324,14 @@ struct
     match (x,y) with
     | (`Lifted x, `Lifted y) ->
       (try `Lifted (Base.widen x y)
-      with Uncomparable -> `Top)
+       with Uncomparable -> `Top)
     | _ -> y
 
   let narrow x y =
     match (x,y) with
     | (`Lifted x, `Lifted y) ->
       (try `Lifted (Base.narrow x y)
-      with Uncomparable -> `Bot)
+       with Uncomparable -> `Bot)
     | _ -> x
 end
 

src/common/dune

@@ -0,0 +1,29 @@
+(include_subdirs unqualified)
+
+(library
+ (name goblint_common)
+ (public_name goblint.common)
+ (wrapped false) ; TODO: wrap
+ (libraries
+   batteries.unthreaded
+   zarith
+   goblint_std
+   goblint-cil
+   fpath
+   yojson
+   json-data-encoding
+   cpu
+   goblint_timing
+   goblint_build_info
+   goblint.sites
+   qcheck-core.runner)
+ (flags :standard -open Goblint_std)
+ (preprocess
+  (pps
+    ppx_deriving.std
+    ppx_deriving_hash
+    ppx_deriving_yojson
+    ppx_blob))
+ (preprocessor_deps (file util/options.schema.json)))
+
+(documentation)

src/util/lazyEval.ml → src/common/util/lazyEval.ml

@@ -5,10 +5,10 @@
    Node -> CilType -> Printable -> Goblintutil -> GobConfig -> Tracing -> Node *)
 
 module Make (M : sig
-  type t
-  type result
-  val eval : t -> result
-end) : sig
+    type t
+    type result
+    val eval : t -> result
+  end) : sig
   type t
   val make : M.t -> t
   val force : t -> M.result
@@ -20,8 +20,8 @@ end = struct
   let force l =
     match l.value with
     | `Closure arg ->
-        let v = M.eval arg in
-        l.value <- `Computed v;
-        v
+      let v = M.eval arg in
+      l.value <- `Computed v;
+      v
     | `Computed v -> v
 end

src/util/messageCategory.ml → src/common/util/messageCategory.ml

@@ -260,8 +260,8 @@ let categoryName = function
 
   | Behavior x -> behaviorName x
   | Integer x -> (match x with
-    | Overflow -> "Overflow";
-    | DivByZero -> "DivByZero")
+      | Overflow -> "Overflow";
+      | DivByZero -> "DivByZero")
   | Float -> "Float"
 
 

src/util/options.ml → src/common/util/options.ml

@@ -1,4 +1,4 @@
-(** [src/util/options.schema.json] low-level access. *)
+(** [src/common/util/options.schema.json] low-level access. *)
 
 open Json_schema
 

src/util/tracing.ml → src/common/util/tracing.ml

@@ -10,7 +10,7 @@ open Pretty
 module Strs = Set.Make (String)
 
 
-let tracing = ConfigProfile.profile = "trace"
+let tracing = Goblint_build_info.dune_profile = "trace"
 
 let current_loc = ref locUnknown
 let next_loc    = ref locUnknown

src/dune

@@ -7,7 +7,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (modules :standard \ goblint mainspec privPrecCompare apronPrecCompare messagesCompare)
-  (libraries goblint.sites goblint.build-info goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils
+  (libraries goblint.sites goblint.build-info goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_common
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
     ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies.
@@ -56,11 +56,11 @@
       (-> violationZ3.no-z3.ml)
     )
   )
+  (flags :standard -open Goblint_std)
   (foreign_stubs (language c) (names stubs))
   (ocamlopt_flags :standard -no-float-const-prop)
   (preprocess
     (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson ppx_blob))
-  (preprocessor_deps (file util/options.schema.json))
   (instrumentation (backend bisect_ppx))
 )
 
@@ -77,51 +77,35 @@
   (public_names goblint -)
   (modes byte native) ; https://dune.readthedocs.io/en/stable/dune-files.html#linking-modes
   (modules goblint mainspec)
-  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune)
+  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune goblint_std)
   (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson))
-  (flags :standard -linkall)
+  (flags :standard -linkall -open Goblint_std)
 )
 
 (executable
   (name privPrecCompare)
   (modules privPrecCompare)
-  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune)
+  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune goblint_std)
   (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson))
-  (flags :standard -linkall)
+  (flags :standard -linkall -open Goblint_std)
 )
 
 (executable
   (name apronPrecCompare)
   (modules apronPrecCompare)
-  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune)
+  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune goblint_std)
   (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson))
-  (flags :standard -linkall)
+  (flags :standard -linkall -open Goblint_std)
 )
 
 (executable
   (name messagesCompare)
   (modules messagesCompare)
-  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune)
+  (libraries goblint.lib goblint.sites.dune goblint.build-info.dune goblint_std)
   (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson))
-  (flags :standard -linkall)
+  (flags :standard -linkall -open Goblint_std)
 )
 
-(rule
-  (target configVersion.ml)
-  (mode (promote (until-clean) (only configVersion.ml))) ; replace existing file in source tree, even if releasing (only overrides)
-  (deps (universe)) ; do not cache, always regenerate
-  (action (pipe-stdout (bash "git describe --all --long --dirty || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet version = \"%s\"'")))))
-
-(rule
-  (target configProfile.ml)
-  (mode (promote (until-clean) (only configProfile.ml))) ; replace existing file in source tree, even if releasing (only overrides)
-  (action (write-file %{target} "(* Automatically regenerated, changes do not persist! *)\nlet profile = \"%{profile}\"")))
-
-(rule
-  (target configOcaml.ml)
-  (mode (promote (until-clean) (only configOcaml.ml))) ; replace existing file in source tree, even if releasing (only overrides)
-  (action (write-file %{target} "(* Automatically regenerated, changes do not persist! *)\nlet flambda = \"%{ocaml-config:flambda}\"")))
-
 (rule
   (alias runtest)
   (deps ../goblint ../scripts/update_suite.rb ../Makefile ../make.sh (source_tree ../tests/regression) (source_tree ../includes) (source_tree ../linux-headers))
@@ -141,3 +125,5 @@
     (flags (:standard -warn-error -A -w -unused-var-strict -w -unused-functor-parameter -w +9)) ; https://dune.readthedocs.io/en/stable/faq.html#how-to-make-warnings-non-fatal
   )
 )
+
+(documentation)

src/framework/control.ml

@@ -529,7 +529,7 @@ struct
             GobConfig.write_file config;
             let module Meta = struct
                 type t = { command : string; version: string; timestamp : float; localtime : string } [@@deriving to_yojson]
-                let json = to_yojson { command = GobSys.command_line; version = Version.goblint; timestamp = Unix.time (); localtime = GobUnix.localtime () }
+                let json = to_yojson { command = GobSys.command_line; version = Goblint_build_info.version; timestamp = Unix.time (); localtime = GobUnix.localtime () }
               end
             in
             (* Yojson.Safe.to_file meta Meta.json; *)