Merge pull request #499 from goblint/json-schema

Replace `Defaults` module with JSON schema

Author: sim642

docs/user-guide/configuring.md

@@ -0,0 +1,20 @@
+# Configuring
+
+## JSON conf files
+
+### JSON schema
+
+#### VSCode
+In `.vscode/settings.json` add the following:
+```json
+{
+    "json.schemas": [
+        {
+            "fileMatch": [
+                "/conf/*.json"
+            ],
+            "url": "/src/util/options.schema.json"
+        }
+    ]
+}
+```

dune-project

@@ -32,10 +32,12 @@
     (ppx_distr_guards (>= 0.2))
     ppx_deriving
     ppx_deriving_yojson
+    (ppx_blob (>= 0.6.0))
     (ocaml-monadic (>= 0.5))
     (ounit2 :with-test)
     (odoc :with-doc)
     dune-site
+    json-data-encoding
     (sha (>= 1.12))
     (conf-gmp (>= 3)) ; only needed transitively, but they don't have lower bound, which is needed on MacOS
     (conf-ruby :with-test)

goblint.opam

@@ -28,10 +28,12 @@ depends: [
   "ppx_distr_guards" {>= "0.2"}
   "ppx_deriving"
   "ppx_deriving_yojson"
+  "ppx_blob" {>= "0.6.0"}
   "ocaml-monadic" {>= "0.5"}
   "ounit2" {with-test}
   "odoc" {with-doc}
   "dune-site"
+  "json-data-encoding"
   "sha" {>= "1.12"}
   "conf-gmp" {>= "3"}
   "conf-ruby" {with-test}

goblint.opam.locked

@@ -18,6 +18,7 @@ homepage: "https://goblint.in.tum.de"
 doc: "https://goblint.readthedocs.io/en/latest/"
 bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
+  "angstrom" {= "0.15.0"}
   "apron" {= "v0.9.13"}
   "astring" {= "0.8.5" & with-doc}
   "base-bigarray" {= "base"}
@@ -26,12 +27,15 @@ depends: [
   "base-unix" {= "base"}
   "batteries" {= "3.4.0"}
   "benchmark" {= "1.6" & with-test}
+  "bigarray-compat" {= "1.0.0"}
+  "bigstringaf" {= "0.7.0"}
   "biniou" {= "1.2.1"}
   "camlidl" {= "1.09"}
   "cmdliner" {= "1.0.4" & with-doc}
   "conf-gmp" {= "3"}
   "conf-mpfr" {= "2"}
   "conf-perl" {= "1"}
+  "conf-pkg-config" {= "2"}
   "conf-ruby" {= "1.0.0" & with-test}
   "cppo" {= "1.6.7"}
   "dune" {= "2.9.1"}
@@ -41,6 +45,7 @@ depends: [
   "fmt" {= "0.9.0" & with-doc}
   "fpath" {= "0.7.3" & with-doc}
   "goblint-cil" {= "1.8.2"}
+  "json-data-encoding" {= "0.10"}
   "logs" {= "0.7.0" & with-doc}
   "mlgmpidl" {= "1.2.13"}
   "num" {= "1.4"}
@@ -51,11 +56,13 @@ depends: [
   "ocaml-migrate-parsetree" {= "2.2.0" & with-doc}
   "ocaml-monadic" {= "0.5"}
   "ocaml-options-vanilla" {= "1"}
+  "ocaml-syntax-shims" {= "1.0.0"}
   "ocamlbuild" {= "0.14.0"}
   "ocamlfind" {= "1.9.1"}
   "odoc" {= "2.0.2" & with-doc}
   "odoc-parser" {= "0.9.0" & with-doc}
   "ounit2" {= "2.2.4" & with-test}
+  "ppx_blob" {= "0.7.2"}
   "ppx_derivers" {= "1.2.1"}
   "ppx_deriving" {= "5.2.1"}
   "ppx_deriving_yojson" {= "3.6.1"}
@@ -68,9 +75,11 @@ depends: [
   "sexplib0" {= "v0.14.0"}
   "sha" {= "1.15.1"}
   "stdlib-shims" {= "0.3.0"}
+  "stringext" {= "1.6.0"}
   "topkg" {= "1.0.3" & with-doc}
   "tyxml" {= "4.4.0" & with-doc}
   "uchar" {= "0.0.2" & with-doc}
+  "uri" {= "4.2.0"}
   "uutf" {= "1.0.2" & with-doc}
   "yojson" {= "1.7.0"}
   "zarith" {= "1.12"}

mkdocs.yml

@@ -18,6 +18,7 @@ nav:
   - Home: index.md
   - 'User guide':
     - user-guide/running.md
+    - user-guide/configuring.md
     - user-guide/inspecting.md
     - user-guide/annotating.md
   - 'Developer guide':

src/dune

@@ -8,7 +8,7 @@
   (public_name goblint.lib)
   (wrapped false)
   (modules :standard \ goblint mainarinc maindomaintest mainspec privPrecCompare apronPrecCompare)
-  (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha
+  (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding
     ; 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.
@@ -35,7 +35,8 @@
   )
   (preprocess
     (staged_pps ppx_deriving.std ppx_deriving_yojson
-      ppx_distr_guards ocaml-monadic))
+      ppx_distr_guards ocaml-monadic ppx_blob))
+  (preprocessor_deps (file util/options.schema.json))
 )
 
 ; Workaround for alternative dependencies with unqualified subdirs.

src/maindomaintest.ml

@@ -1,4 +1,4 @@
-open! Defaults (* Enums / ... need initialized conf *)
+(* open! Defaults (* Enums / ... need initialized conf *) *)
 
 module type FiniteSetElems =
 sig

src/maingoblint.ml

@@ -2,7 +2,6 @@
 
 open Prelude
 open GobConfig
-open Defaults
 open Printf
 open Goblintutil
 
@@ -83,10 +82,10 @@ let option_spec_list =
     set_bool "dbg.print_dead_code" true;
     set_string "result" "sarif"
   in
-  let defaults_spec_list = List.map (fun (_, (name, (_, _))) ->
+  let defaults_spec_list = List.map (fun path ->
       (* allow "--option value" as shorthand for "--set option value" *)
-      ("--" ^ name, Arg.String (set_auto name), "")
-    ) !Defaults.registrar
+      ("--" ^ path, Arg.String (set_auto path), "")
+    ) Options.paths
   in
   let tmp_arg = ref "" in
   [ "-o"                   , Arg.String (set_string "outfile"), ""
@@ -100,8 +99,8 @@ let option_spec_list =
   ; "--conf"               , Arg.String merge_file, ""
   ; "--writeconf"          , Arg.String (fun fn -> writeconffile := fn), ""
   ; "--version"            , Arg.Unit print_version, ""
-  ; "--print_options"      , Arg.Unit (fun _ -> printCategory stdout Std; exit 0), ""
-  ; "--print_all_options"  , Arg.Unit (fun _ -> printAllCategories stdout; exit 0), ""
+  ; "--print_options"            , Arg.Unit (fun () -> Options.print_options (); exit 0), ""
+  ; "--print_all_options"        , Arg.Unit (fun () -> Options.print_all_options (); exit 0), ""
   ; "--trace"              , Arg.String set_trace, ""
   ; "--tracevars"          , add_string Tracing.tracevars, ""
   ; "--tracelocs"          , add_int Tracing.tracelocs, ""
@@ -362,13 +361,12 @@ let do_analyze change_info merged_AST =
           Printexc.raise_with_backtrace e backtrace (* re-raise with captured inner backtrace *)
           (* Cilfacade.current_file := ast'; *)
       in
-      (* old style is ana.activated = [phase_1, ...] with phase_i = [ana_1, ...]
-         new style (Goblintutil.phase_config = true) is phases[i].ana.activated = [ana_1, ...]
+      (* new style is phases[i].ana.activated = [ana_1, ...]
          phases[i].ana.x overwrites setting ana.x *)
       let num_phases =
         let np,na,nt = Tuple3.mapn (List.length % get_list) ("phases", "ana.activated", "trans.activated") in
-        phase_config := np > 0; (* TODO what about wrong usage like { phases = [...], ana.activated = [...] }? should child-lists add to parent-lists? *)
-        if get_bool "dbg.verbose" then print_endline @@ "Using " ^ if !phase_config then "new" else "old" ^ " format for phases!";
+        (* TODO what about wrong usage like { phases = [...], ana.activated = [...] }? should child-lists add to parent-lists? *)
+        if get_bool "dbg.verbose" then print_endline @@ "Using new format for phases!";
         if np = 0 && na = 0 && nt = 0 then failwith "No phases and no activated analyses or transformations!";
         max np 1
       in