From ad9a90039529589fd51ba7e3076524edde487641 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 10 Dec 2021 17:14:23 +0200 Subject: [PATCH 01/55] Add ocplib-json-typed dependency --- dune-project | 1 + goblint.opam | 1 + goblint.opam.locked | 8 ++++++++ src/dune | 2 +- 4 files changed, 11 insertions(+), 1 deletion(-) diff --git a/dune-project b/dune-project index 71f5ed0801..d2ced52d52 100644 --- a/dune-project +++ b/dune-project @@ -36,6 +36,7 @@ (ounit2 :with-test) (odoc :with-doc) dune-site + ocplib-json-typed (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) diff --git a/goblint.opam b/goblint.opam index e7428cf930..7cd0a1f16a 100644 --- a/goblint.opam +++ b/goblint.opam @@ -32,6 +32,7 @@ depends: [ "ounit2" {with-test} "odoc" {with-doc} "dune-site" + "ocplib-json-typed" "sha" {>= "1.12"} "conf-gmp" {>= "3"} "conf-ruby" {with-test} diff --git a/goblint.opam.locked b/goblint.opam.locked index 45f3c14c0b..f1be2c3324 100644 --- a/goblint.opam.locked +++ b/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.3.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"} @@ -48,8 +52,10 @@ depends: [ "ocaml-config" {= "2"} "ocaml-monadic" {= "0.5"} "ocaml-options-vanilla" {= "1"} + "ocaml-syntax-shims" {= "1.0.0"} "ocamlbuild" {= "0.14.0"} "ocamlfind" {= "1.9.1"} + "ocplib-json-typed" {= "0.7.1"} "odoc" {= "1.5.2" & with-doc} "ounit2" {= "2.2.4" & with-test} "ppx_derivers" {= "1.2.1"} @@ -64,9 +70,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"} diff --git a/src/dune b/src/dune index 95af13fb04..f941d08830 100644 --- a/src/dune +++ b/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 ocplib-json-typed ; 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. From 110564196d143249e7778fe876e955d3b59ef6b8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 10 Dec 2021 17:14:50 +0200 Subject: [PATCH 02/55] Add JSON validation attempt --- src/util/gobConfig.ml | 5 +- src/util/jsonSchema2.ml | 103 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 107 insertions(+), 1 deletion(-) create mode 100644 src/util/jsonSchema2.ml diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index 860705d8b5..b42ba9f787 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -260,7 +260,10 @@ struct new_v in o := set_value v !o orig_pth; - validate conf_schema !json_conf + validate conf_schema !json_conf; + + if not !build_config then (* object incomplete during building *) + JsonSchema2.validate !json_conf (** Helper function for reading values. Handles error messages. *) let get_path_string f st = diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml new file mode 100644 index 0000000000..9f9d060298 --- /dev/null +++ b/src/util/jsonSchema2.ml @@ -0,0 +1,103 @@ +open Prelude + +module JS = Json_schema.Make (Json_repr.Yojson) +module JE = Json_encoding.Make (Json_repr.Yojson) + +let default_schema = {schema| +{ "id" : "root" +, "type" : "object" +, "required" : ["outfile", "includes", "kernel_includes", "custom_includes", "kernel-root", "justcil", "justcfg", "printstats", "verify", "mainfun", "exitfun", "otherfun", "allglobs", "keepcpp", "tempDir", "cppflags", "kernel", "dump_globs", "result", "solver", "allfuns", "nonstatic", "colors", "g2html"] +, "additionalProperties" : false +, "properties" : + { "ana" : + { "type" : "object" + , "additionalProperties" : true + , "required" : [] + } + , "sem" : {} + , "incremental" : {} + , "trans" : {} + , "phases" : {} + , "annotation" : + { "type" : "object" + , "additionalProperties" : true + , "required" : [] + } + , "exp" : + { "type" : "object" + , "additionalProperties" : true + , "required" : [] + } + , "dbg" : + { "type" : "object" + , "additionalProperties" : true + , "required" : [] + } + , "questions" : + { "file" : "" + } + , "outfile" : {} + , "includes" : {} + , "kernel_includes" : {} + , "custom_includes" : {} + , "kernel-root" : {} + , "justcil" : {} + , "justcfg" : {} + , "printstats" : {} + , "verify" : {} + , "mainfun" : {} + , "exitfun" : {} + , "otherfun" : {} + , "allglobs" : {} + , "keepcpp" : {} + , "tempDir" : + { "type" : "string" + } + , "cppflags" : {} + , "kernel" : {} + , "dump_globs" : {} + , "result" : + { "type" : "string" + } + , "solver" : {} + , "comparesolver" : {} + , "solverdiffs" : {} + , "allfuns" : {} + , "nonstatic" : {} + , "colors" : {} + , "g2html" : {} + , "interact" : {} + , "save_run" : {} + , "load_run" : {} + , "compare_runs" : {} + , "warn_at" : {} + , "warn" : + { "type" : "string" + , "additionalProperties" : true + , "required" : ["foo"] + } + , "gobview" : {} + } +}|schema} + +let schema = JS.of_json (Yojson.Safe.from_string default_schema) + + +let rec encoding_of_schema_element (schema_element: Json_schema.element): unit Json_encoding.encoding = + match schema_element.kind with + | Object object_specs -> + let open Json_encoding in + List.fold_left (fun acc (name, element, required, _) -> + conv (fun _ -> failwith "asd") (fun _ -> ()) @@ merge_objs acc (obj1 (if required then req name unit else dft name unit ())) + ) (Option.map_default encoding_of_schema_element empty object_specs.additional_properties) object_specs.properties + | _ -> failwith (Format.asprintf "%a" Json_schema.pp (Json_schema.create schema_element)) + +let encoding_of_schema (schema: Json_schema.schema): unit Json_encoding.encoding = + encoding_of_schema_element (Json_schema.root schema) + +let validate json = + match JE.destruct (encoding_of_schema schema) json with + | _ -> () + | exception (Json_encoding.Cannot_destruct _ as e) -> + Json_encoding.print_error Format.std_formatter e; + failwith "JsonSchema2.validate" \ No newline at end of file From bcc82b42cba513eadba67d62e89c19653cd80bff Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 10 Dec 2021 18:08:34 +0200 Subject: [PATCH 03/55] Add recursive validation of JSON schema objects --- src/util/jsonSchema2.ml | 19 ++++++++++++++----- src/util/jsonSchema2.mli | 1 + 2 files changed, 15 insertions(+), 5 deletions(-) create mode 100644 src/util/jsonSchema2.mli diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 9f9d060298..58d82c5716 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -72,7 +72,7 @@ let default_schema = {schema| , "compare_runs" : {} , "warn_at" : {} , "warn" : - { "type" : "string" + { "type" : "object" , "additionalProperties" : true , "required" : ["foo"] } @@ -84,13 +84,22 @@ let schema = JS.of_json (Yojson.Safe.from_string default_schema) let rec encoding_of_schema_element (schema_element: Json_schema.element): unit Json_encoding.encoding = + let open Json_encoding in + let erase: type t. t encoding -> unit encoding = fun encoding -> conv (fun _ -> failwith "asd") (fun _ -> ()) encoding in match schema_element.kind with + | Any -> unit + | String string_specs -> erase string | Object object_specs -> - let open Json_encoding in List.fold_left (fun acc (name, element, required, _) -> - conv (fun _ -> failwith "asd") (fun _ -> ()) @@ merge_objs acc (obj1 (if required then req name unit else dft name unit ())) + let field = + if required then + req name (encoding_of_schema_element element) + else + dft name (encoding_of_schema_element element) () + in + erase @@ merge_objs acc (obj1 field) ) (Option.map_default encoding_of_schema_element empty object_specs.additional_properties) object_specs.properties - | _ -> failwith (Format.asprintf "%a" Json_schema.pp (Json_schema.create schema_element)) + | _ -> failwith (Format.asprintf "encoding_of_schema_element: %a" Json_schema.pp (Json_schema.create schema_element)) let encoding_of_schema (schema: Json_schema.schema): unit Json_encoding.encoding = encoding_of_schema_element (Json_schema.root schema) @@ -99,5 +108,5 @@ let validate json = match JE.destruct (encoding_of_schema schema) json with | _ -> () | exception (Json_encoding.Cannot_destruct _ as e) -> - Json_encoding.print_error Format.std_formatter e; + Format.printf "validate: %a\n" (Json_encoding.print_error ?print_unknown:None) e; failwith "JsonSchema2.validate" \ No newline at end of file diff --git a/src/util/jsonSchema2.mli b/src/util/jsonSchema2.mli new file mode 100644 index 0000000000..a1a4835722 --- /dev/null +++ b/src/util/jsonSchema2.mli @@ -0,0 +1 @@ +val validate : Json_repr.yojson -> unit From 6db73d6495d62561a23d8dfa983eda76520f1e53 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 10 Dec 2021 18:52:38 +0200 Subject: [PATCH 04/55] Try JSON schema generation from defaults --- src/util/defaults.ml | 3 +- src/util/gobConfig.ml | 5 +- src/util/jsonSchema2.ml | 106 ++++++++++++++++++++++++++++++++++++++- src/util/jsonSchema2.mli | 2 + 4 files changed, 111 insertions(+), 5 deletions(-) diff --git a/src/util/defaults.ml b/src/util/defaults.ml index 36853892f9..1b26ab3451 100644 --- a/src/util/defaults.ml +++ b/src/util/defaults.ml @@ -366,4 +366,5 @@ let default_schema = {schema| let _ = let v = Yojson.Safe.from_string default_schema in - GobConfig.addenum_sch v + GobConfig.addenum_sch v; + JsonSchema2.convert_schema @@ List.map snd !registrar diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index b42ba9f787..bf1e7e22d0 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -262,8 +262,9 @@ struct o := set_value v !o orig_pth; validate conf_schema !json_conf; - if not !build_config then (* object incomplete during building *) - JsonSchema2.validate !json_conf + (* if not !build_config then (* object incomplete during building *) + JsonSchema2.validate !json_conf *) + () (** Helper function for reading values. Handles error messages. *) let get_path_string f st = diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 58d82c5716..ec6ab52a02 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -82,10 +82,10 @@ let default_schema = {schema| let schema = JS.of_json (Yojson.Safe.from_string default_schema) +let erase: type t. t Json_encoding.encoding -> unit Json_encoding.encoding = fun encoding -> Json_encoding.conv (fun _ -> failwith "asd") (fun _ -> ()) encoding let rec encoding_of_schema_element (schema_element: Json_schema.element): unit Json_encoding.encoding = let open Json_encoding in - let erase: type t. t encoding -> unit encoding = fun encoding -> conv (fun _ -> failwith "asd") (fun _ -> ()) encoding in match schema_element.kind with | Any -> unit | String string_specs -> erase string @@ -109,4 +109,106 @@ let validate json = | _ -> () | exception (Json_encoding.Cannot_destruct _ as e) -> Format.printf "validate: %a\n" (Json_encoding.print_error ?print_unknown:None) e; - failwith "JsonSchema2.validate" \ No newline at end of file + failwith "JsonSchema2.validate" + + +(** raise when you cannot parse the path *) +exception PathParseError + +(** raise when there is an type error *) +exception ConfTypeError + +(** Type of the index *) +type index = Int of int (** and integer *) + | App (** prepend to the list *) + | Rem (** remove from the list *) + | New (** create a new list *) + +(** Type of the path *) +type path = Here (** we are there *) + | Select of string * path (** we need to select an field *) + | Index of index * path (** we need to select an array index *) + +open Printf + +(** Path printing. *) +let rec print_path' ch = function + | Here -> () + | Select (s,p) -> fprintf ch ".%s%a" s print_path' p + | Index (Int i,p) -> fprintf ch "[%d]%a" i print_path' p + | Index (App ,p) -> fprintf ch "[+]%a" print_path' p + | Index (Rem ,p) -> fprintf ch "[-]%a" print_path' p + | Index (New ,p) -> fprintf ch "[*]%a" print_path' p + + +(** Parse an index. *) +let parse_index s = + try if s = "+" then App + else if s = "*" then New + else if s = "-" then Rem + else Int (int_of_string s) + with Failure _ -> raise PathParseError + +(** Helper function [split c1 c2 xs] that splits [xs] on [c1] or [c2] *) +let split c1 c2 xs = + let l = String.length xs in + let rec split' i = + if i + let fld, pth = split '.' '[' (String.lchop s) in + Select (fld, parse_path' pth) + | '[' -> + let idx, pth = String.split (String.lchop s) "]" in + Index (parse_index idx, parse_path' pth) + | _ -> raise PathParseError + +(** Parse a string path, but you may ignore the first dot. *) +let parse_path (s:string) : path = + let s = String.trim s in + try + if String.length s = 0 then Here else begin + let fld, pth = split '.' '[' s in + if fld = "" + then parse_path' pth + else Select (fld, parse_path' pth) + end + with PathParseError -> + eprintf "Error: Couldn't parse the json path '%s'\n%!" s; + failwith "parsing" + +open Json_encoding + +let convert_opt name desc def: unit encoding = + let rec convert_path = function + | Select (s, Here) -> + obj1 @@ dft ~title:name ~description:desc s unit () (* TODO: correct type *) + | Select (s, path') -> + let obj' = convert_path path' in + obj1 @@ dft s obj' () + | _ -> assert false + in + let path = parse_path name in + convert_path path + + +let convert_schema opts = + opts + |> List.map (fun (name, (desc, def)) -> convert_opt name desc def) + |> List.reduce (fun o1 o2 -> erase (merge_objs o1 o2)) + |> fun el -> + let sch = schema el in + (* Format.printf "schema: %a\n" Json_schema.pp sch; *) + Format.printf "schema2: %a\n" (Yojson.Safe.pretty_print ~std:true) (JS.to_json sch) diff --git a/src/util/jsonSchema2.mli b/src/util/jsonSchema2.mli index a1a4835722..6c43aa8057 100644 --- a/src/util/jsonSchema2.mli +++ b/src/util/jsonSchema2.mli @@ -1 +1,3 @@ val validate : Json_repr.yojson -> unit + +val convert_schema: (string * (string * string)) list -> unit From 5141f321ce9711a07b8be6cea8832014909b6ee8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 10 Dec 2021 19:17:55 +0200 Subject: [PATCH 05/55] Rewrite defaults JSON schema generation properly --- src/util/defaults.ml | 2 +- src/util/gobConfig.ml | 2 ++ src/util/jsonSchema2.ml | 37 +++++++++++++++++++++++++++++-------- src/util/jsonSchema2.mli | 2 +- 4 files changed, 33 insertions(+), 10 deletions(-) diff --git a/src/util/defaults.ml b/src/util/defaults.ml index 1b26ab3451..59599f7c50 100644 --- a/src/util/defaults.ml +++ b/src/util/defaults.ml @@ -367,4 +367,4 @@ let default_schema = {schema| let _ = let v = Yojson.Safe.from_string default_schema in GobConfig.addenum_sch v; - JsonSchema2.convert_schema @@ List.map snd !registrar + JsonSchema2.convert_schema !GobConfig.json_conf @@ List.map snd !registrar diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index bf1e7e22d0..d455062bf6 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -79,6 +79,8 @@ sig (** Add a schema to the conf*) val addenum_sch: Yojson.Safe.t -> unit + + val json_conf: Yojson.Safe.t ref end (** The implementation of the [gobConfig] module. *) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index ec6ab52a02..8830443b6e 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -203,12 +203,33 @@ let convert_opt name desc def: unit encoding = let path = parse_path name in convert_path path +open Json_schema -let convert_schema opts = - opts - |> List.map (fun (name, (desc, def)) -> convert_opt name desc def) - |> List.reduce (fun o1 o2 -> erase (merge_objs o1 o2)) - |> fun el -> - let sch = schema el in - (* Format.printf "schema: %a\n" Json_schema.pp sch; *) - Format.printf "schema2: %a\n" (Yojson.Safe.pretty_print ~std:true) (JS.to_json sch) +let rec convert_schema' (json: Yojson.Safe.t) opts (prefix: string): element = + let element' ekind = + let (desc, def) = List.assoc (BatString.lchop prefix) opts in + (* let name = BatString.lchop @@ Filename.extension prefix in *) + {(element ekind) with title = Some (BatString.lchop prefix); description = Some desc} + in + match json with + | `String s -> + element' @@ String string_specs + | `Bool b -> + element' @@ Boolean + | `Int i -> + element' @@ Number numeric_specs + | `List xs -> + element' @@ Monomorphic_array (element Any, array_specs) + | `Assoc xs -> + let properties = List.map (fun (key, value) -> + (key, convert_schema' value opts (prefix ^ "." ^ key), false, None) + ) xs + in + element @@ Object { object_specs with properties; additional_properties = None } + | _ -> failwith (Format.asprintf "convert_schema': %a" Yojson.Safe.pp json) + +let convert_schema json opts = + let sch = create @@ convert_schema' json opts "" in + (* Format.printf "schema: %a\n" Json_schema.pp sch; *) + (* Format.printf "schema2: %a\n" (Yojson.Safe.pretty_print ~std:true) (JS.to_json sch) *) + Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema.json") (JS.to_json sch) diff --git a/src/util/jsonSchema2.mli b/src/util/jsonSchema2.mli index 6c43aa8057..f8f135e764 100644 --- a/src/util/jsonSchema2.mli +++ b/src/util/jsonSchema2.mli @@ -1,3 +1,3 @@ val validate : Json_repr.yojson -> unit -val convert_schema: (string * (string * string)) list -> unit +val convert_schema: Yojson.Safe.t -> (string * (string * string)) list -> unit From 4a282a1629d94f0a5b3ecc22ffe984687f4b3b3c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 13 Dec 2021 10:32:55 +0200 Subject: [PATCH 06/55] Switch from ocplib-json-typed to json-data-encoding --- dune-project | 2 +- goblint.opam | 2 +- goblint.opam.locked | 2 +- src/dune | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/dune-project b/dune-project index d2ced52d52..426527ed30 100644 --- a/dune-project +++ b/dune-project @@ -36,7 +36,7 @@ (ounit2 :with-test) (odoc :with-doc) dune-site - ocplib-json-typed + 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) diff --git a/goblint.opam b/goblint.opam index 7cd0a1f16a..4388f92b7e 100644 --- a/goblint.opam +++ b/goblint.opam @@ -32,7 +32,7 @@ depends: [ "ounit2" {with-test} "odoc" {with-doc} "dune-site" - "ocplib-json-typed" + "json-data-encoding" "sha" {>= "1.12"} "conf-gmp" {>= "3"} "conf-ruby" {with-test} diff --git a/goblint.opam.locked b/goblint.opam.locked index f1be2c3324..3ae10ddf87 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -44,6 +44,7 @@ depends: [ "easy-format" {= "1.3.2"} "fpath" {= "0.7.3" & with-doc} "goblint-cil" {= "1.8.2"} + "json-data-encoding" {= "0.10"} "mlgmpidl" {= "1.2.13"} "num" {= "1.4"} "ocaml" {= "4.12.0"} @@ -55,7 +56,6 @@ depends: [ "ocaml-syntax-shims" {= "1.0.0"} "ocamlbuild" {= "0.14.0"} "ocamlfind" {= "1.9.1"} - "ocplib-json-typed" {= "0.7.1"} "odoc" {= "1.5.2" & with-doc} "ounit2" {= "2.2.4" & with-test} "ppx_derivers" {= "1.2.1"} diff --git a/src/dune b/src/dune index f941d08830..f538189f5f 100644 --- a/src/dune +++ b/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 ocplib-json-typed + (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. From 67bf73e18024836f01cfd37f993b8c4ef2d89960 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 13 Dec 2021 11:04:30 +0200 Subject: [PATCH 07/55] Add default values to generated schema --- src/util/jsonSchema2.ml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 8830443b6e..b793b2c324 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -205,11 +205,21 @@ let convert_opt name desc def: unit encoding = open Json_schema +(** The ultimate convenience function for writing values. *) +let one_quote = Str.regexp "\'" +let parse_goblint_json s = + try + let s' = Str.global_replace one_quote "\"" s in + let v = Yojson.Safe.from_string s' in + v + with Yojson.Json_error _ -> + `String s + let rec convert_schema' (json: Yojson.Safe.t) opts (prefix: string): element = let element' ekind = let (desc, def) = List.assoc (BatString.lchop prefix) opts in (* let name = BatString.lchop @@ Filename.extension prefix in *) - {(element ekind) with title = Some (BatString.lchop prefix); description = Some desc} + {(element ekind) with title = Some (BatString.lchop prefix); description = Some desc; default = Some (Json_repr.repr_to_any (module Json_repr.Yojson) (parse_goblint_json def))} in match json with | `String s -> From efa5ee0a0d47d534d3d68a9512688ba90ffb67f5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 13 Dec 2021 11:19:15 +0200 Subject: [PATCH 08/55] Add schema for array elements --- src/util/jsonSchema2.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index b793b2c324..d68685476d 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -229,7 +229,12 @@ let rec convert_schema' (json: Yojson.Safe.t) opts (prefix: string): element = | `Int i -> element' @@ Number numeric_specs | `List xs -> - element' @@ Monomorphic_array (element Any, array_specs) + let element_schema = match prefix with + | ".phases" -> element Any (* TODO: mu? *) + | ".ana.activated" -> element Any (* TODO: old-style phases? *) + | _ -> element (String string_specs) + in + element' @@ Monomorphic_array (element_schema, array_specs) | `Assoc xs -> let properties = List.map (fun (key, value) -> (key, convert_schema' value opts (prefix ^ "." ^ key), false, None) From 1764488ee2af0d592b9bb51de3e4926ff5a78920 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 13 Dec 2021 11:39:47 +0200 Subject: [PATCH 09/55] Add element schema to phases --- src/util/jsonSchema2.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index d68685476d..9ec681da76 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -230,7 +230,7 @@ let rec convert_schema' (json: Yojson.Safe.t) opts (prefix: string): element = element' @@ Number numeric_specs | `List xs -> let element_schema = match prefix with - | ".phases" -> element Any (* TODO: mu? *) + | ".phases" -> element (Id_ref "") (* refer to entire schema itself *) | ".ana.activated" -> element Any (* TODO: old-style phases? *) | _ -> element (String string_specs) in @@ -244,7 +244,10 @@ let rec convert_schema' (json: Yojson.Safe.t) opts (prefix: string): element = | _ -> failwith (Format.asprintf "convert_schema': %a" Yojson.Safe.pp json) let convert_schema json opts = - let sch = create @@ convert_schema' json opts "" in - (* Format.printf "schema: %a\n" Json_schema.pp sch; *) - (* Format.printf "schema2: %a\n" (Yojson.Safe.pretty_print ~std:true) (JS.to_json sch) *) - Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema.json") (JS.to_json sch) + try + let sch = create @@ {(convert_schema' json opts "") with id = Some ""} in (* add id to make create defs check happy, doesn't get outputted apparently *) + (* Format.printf "schema: %a\n" Json_schema.pp sch; *) + (* Format.printf "schema2: %a\n" (Yojson.Safe.pretty_print ~std:true) (JS.to_json sch) *) + Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema.json") (JS.to_json sch) + with (Json_schema.Dangling_reference u as e) -> + Json_schema.print_error Format.err_formatter e From 0fd4ddbc13f62438cddda1877c73228b75d167c8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 13 Dec 2021 11:45:07 +0200 Subject: [PATCH 10/55] Remove broken old-style phases --- src/maingoblint.ml | 7 +++---- src/util/gobConfig.ml | 8 ++------ 2 files changed, 5 insertions(+), 10 deletions(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index fc746bf84d..ebad804c4f 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -362,13 +362,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 diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index d455062bf6..717f075b74 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -29,7 +29,6 @@ let build_config = ref false (* Phase of the analysis (moved from GoblintUtil b/c of circular build...) *) let phase = ref 0 -let phase_config = ref true (** The type for [gobConfig] module. *) module type S = @@ -274,11 +273,8 @@ struct let st = String.trim st in let st, x = let g st = st, get_value !json_conf (parse_path st) in - if !phase_config then - try g ("phases["^ string_of_int !phase ^"]."^st) (* try to find value in config for current phase first *) - with _ -> g st (* do global lookup if undefined *) - else - g st (* just use the old format *) + try g ("phases["^ string_of_int !phase ^"]."^st) (* try to find value in config for current phase first *) + with _ -> g st (* do global lookup if undefined *) in if tracing then trace "conf-reads" "Reading '%s', it is %a.\n" st GobYojson.pretty x; try f x From 233360dd9f72b18e3738eb1efdb906dd175bec14 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 13 Dec 2021 11:46:34 +0200 Subject: [PATCH 11/55] Remove special case for old-style ana.activated from JSON schema --- src/util/jsonSchema2.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 9ec681da76..5520efea2f 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -231,7 +231,6 @@ let rec convert_schema' (json: Yojson.Safe.t) opts (prefix: string): element = | `List xs -> let element_schema = match prefix with | ".phases" -> element (Id_ref "") (* refer to entire schema itself *) - | ".ana.activated" -> element Any (* TODO: old-style phases? *) | _ -> element (String string_specs) in element' @@ Monomorphic_array (element_schema, array_specs) From bc6b2eef8e55ea3da54108d26dad8c3937661741 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 13 Dec 2021 12:27:29 +0200 Subject: [PATCH 12/55] Add category descriptions to generated JSON schema --- src/util/defaults.ml | 28 ++-------------------------- src/util/defaultsCategory.ml | 28 ++++++++++++++++++++++++++++ src/util/jsonSchema2.ml | 24 ++++++++++++++++++------ src/util/jsonSchema2.mli | 2 +- 4 files changed, 49 insertions(+), 33 deletions(-) create mode 100644 src/util/defaultsCategory.ml diff --git a/src/util/defaults.ml b/src/util/defaults.ml index 59599f7c50..453c15df1b 100644 --- a/src/util/defaults.ml +++ b/src/util/defaults.ml @@ -3,34 +3,10 @@ open Prelude open Printf open List +open DefaultsCategory (* TODO: add consistency checking *) -(** Main categories of configuration variables. *) -type category = Std (** Parsing input, includes, standard stuff, etc. *) - | Analyses (** Analyses *) - | Incremental (** Incremental features *) - | Semantics (** Semantics *) - | Transformations (** Transformations *) - | Annotation (** Features for annotations *) - | Experimental (** Experimental features of analyses *) - | Debugging (** Debugging, tracing, etc. *) - | Warnings (** Filtering warnings *) - [@@deriving enum] - -let all_categories = min_category -- max_category |> of_enum |> map (Option.get % category_of_enum) - -(** Description strings for categories. *) -let catDescription = function - | Std -> "Standard options for configuring input/output" - | Analyses -> "Options for analyses" - | Semantics -> "Options for semantics" - | Transformations -> "Options for transformations" - | Annotation -> "Options for annotations" - | Experimental -> "Experimental features" - | Debugging -> "Debugging options" - | Incremental -> "Incremental analysis options" - | Warnings -> "Filtering of warnings" (** A place to store registered variables *) let registrar = ref [] @@ -367,4 +343,4 @@ let default_schema = {schema| let _ = let v = Yojson.Safe.from_string default_schema in GobConfig.addenum_sch v; - JsonSchema2.convert_schema !GobConfig.json_conf @@ List.map snd !registrar + JsonSchema2.convert_schema !GobConfig.json_conf @@ List.map (fun (c, (n, p)) -> (n, (c, p))) !registrar diff --git a/src/util/defaultsCategory.ml b/src/util/defaultsCategory.ml new file mode 100644 index 0000000000..52931e300c --- /dev/null +++ b/src/util/defaultsCategory.ml @@ -0,0 +1,28 @@ +open Prelude +open List + +(** Main categories of configuration variables. *) +type category = Std (** Parsing input, includes, standard stuff, etc. *) + | Analyses (** Analyses *) + | Incremental (** Incremental features *) + | Semantics (** Semantics *) + | Transformations (** Transformations *) + | Annotation (** Features for annotations *) + | Experimental (** Experimental features of analyses *) + | Debugging (** Debugging, tracing, etc. *) + | Warnings (** Filtering warnings *) + [@@deriving enum, show { with_path = false }] + +let all_categories = min_category -- max_category |> of_enum |> map (Option.get % category_of_enum) + +(** Description strings for categories. *) +let catDescription = function + | Std -> "Standard options for configuring input/output" + | Analyses -> "Options for analyses" + | Semantics -> "Options for semantics" + | Transformations -> "Options for transformations" + | Annotation -> "Options for annotations" + | Experimental -> "Experimental features" + | Debugging -> "Debugging options" + | Incremental -> "Incremental analysis options" + | Warnings -> "Filtering of warnings" \ No newline at end of file diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 5520efea2f..4b8a9e871e 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -215,11 +215,11 @@ let parse_goblint_json s = with Yojson.Json_error _ -> `String s -let rec convert_schema' (json: Yojson.Safe.t) opts (prefix: string): element = +let rec convert_schema' (json: Yojson.Safe.t) opts (prefix: string): element * DefaultsCategory.category = let element' ekind = - let (desc, def) = List.assoc (BatString.lchop prefix) opts in + let (cat, (desc, def)) = List.assoc (BatString.lchop prefix) opts in (* let name = BatString.lchop @@ Filename.extension prefix in *) - {(element ekind) with title = Some (BatString.lchop prefix); description = Some desc; default = Some (Json_repr.repr_to_any (module Json_repr.Yojson) (parse_goblint_json def))} + ({(element ekind) with title = Some (BatString.lchop prefix); description = Some desc; default = Some (Json_repr.repr_to_any (module Json_repr.Yojson) (parse_goblint_json def))}, cat) in match json with | `String s -> @@ -235,16 +235,28 @@ let rec convert_schema' (json: Yojson.Safe.t) opts (prefix: string): element = in element' @@ Monomorphic_array (element_schema, array_specs) | `Assoc xs -> + let cat' = ref None in let properties = List.map (fun (key, value) -> - (key, convert_schema' value opts (prefix ^ "." ^ key), false, None) + let (inner, cat) = convert_schema' value opts (prefix ^ "." ^ key) in + cat' := Some cat; + (key, inner, false, None) ) xs in - element @@ Object { object_specs with properties; additional_properties = None } + let cat = Option.get !cat' in + let el = match BatString.index_after_n '.' 2 prefix with + | exception Not_found when prefix = ".interact" -> (* isn't Std *) + element @@ Object { object_specs with properties; additional_properties = None} + | exception Not_found -> + {(element @@ Object { object_specs with properties; additional_properties = None}) with title = Some (DefaultsCategory.show_category cat); description = Some (DefaultsCategory.catDescription cat)} + | _ -> + element @@ Object { object_specs with properties; additional_properties = None} + in + (el, cat) | _ -> failwith (Format.asprintf "convert_schema': %a" Yojson.Safe.pp json) let convert_schema json opts = try - let sch = create @@ {(convert_schema' json opts "") with id = Some ""} in (* add id to make create defs check happy, doesn't get outputted apparently *) + let sch = create @@ {(fst @@ convert_schema' json opts "") with id = Some ""} in (* add id to make create defs check happy, doesn't get outputted apparently *) (* Format.printf "schema: %a\n" Json_schema.pp sch; *) (* Format.printf "schema2: %a\n" (Yojson.Safe.pretty_print ~std:true) (JS.to_json sch) *) Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema.json") (JS.to_json sch) diff --git a/src/util/jsonSchema2.mli b/src/util/jsonSchema2.mli index f8f135e764..dfcfff7bf6 100644 --- a/src/util/jsonSchema2.mli +++ b/src/util/jsonSchema2.mli @@ -1,3 +1,3 @@ val validate : Json_repr.yojson -> unit -val convert_schema: Yojson.Safe.t -> (string * (string * string)) list -> unit +val convert_schema: Yojson.Safe.t -> (string * (DefaultsCategory.category * (string * string))) list -> unit From c74b4bc0be6d350a2110d21f1beb220bd34f8495 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 13 Dec 2021 12:39:32 +0200 Subject: [PATCH 13/55] Add defaults object generation from JSON schema --- src/util/jsonSchema2.ml | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 4b8a9e871e..8aae695c00 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -254,11 +254,28 @@ let rec convert_schema' (json: Yojson.Safe.t) opts (prefix: string): element * D (el, cat) | _ -> failwith (Format.asprintf "convert_schema': %a" Yojson.Safe.pp json) + +let rec create_defaults (element: element): Yojson.Safe.t = + match element.default with + | Some default -> Json_repr.any_to_repr (module Json_repr.Yojson) default + | None -> + begin match element.kind with + | Object object_specs -> + `Assoc (List.map (fun (name, el, _, _) -> + (name, create_defaults el) + ) object_specs.properties) + | _ -> + Format.printf "%a\n" Json_schema.pp (create element); + failwith "create_defaults" + end + let convert_schema json opts = try let sch = create @@ {(fst @@ convert_schema' json opts "") with id = Some ""} in (* add id to make create defs check happy, doesn't get outputted apparently *) (* Format.printf "schema: %a\n" Json_schema.pp sch; *) (* Format.printf "schema2: %a\n" (Yojson.Safe.pretty_print ~std:true) (JS.to_json sch) *) - Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema.json") (JS.to_json sch) + Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema.json") (JS.to_json sch); + let defaults = create_defaults (root sch) in + Yojson.Safe.pretty_to_channel (Stdlib.open_out "defaults.json") defaults with (Json_schema.Dangling_reference u as e) -> Json_schema.print_error Format.err_formatter e From 0db5c60d7a159230574a3bf49b16404a9f6e62c3 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 13 Dec 2021 12:48:41 +0200 Subject: [PATCH 14/55] Change GobConfig.set_value to preserve order --- src/util/gobConfig.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index 717f075b74..642bc77439 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -228,10 +228,17 @@ struct let rec set_value v o pth = match o, pth with | `Assoc m, Select (key,pth) -> - begin try `Assoc ((key, set_value v (List.assoc key m) pth) :: List.remove_assoc key m) + let rec modify = function + | [] -> raise Not_found + | (key', v') :: kvs when key' = key -> + (key, set_value v v' pth) :: kvs + | (key', v') :: kvs -> + (key', v') :: modify kvs + in + begin try `Assoc (modify m) with Not_found -> if !build_config then - `Assoc ((key, create_new v pth) :: m) + `Assoc (m @ [(key, create_new v pth)]) else raise @@ ConfigError ("Unknown path "^ (sprintf2 "%a" print_path orig_pth)) end From 75f886ba9e489953537465a842930b01ba38ecb0 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 13 Dec 2021 13:46:18 +0200 Subject: [PATCH 15/55] Remove unused GobConfig json path copy from JsonSchema2 --- src/util/jsonSchema2.ml | 91 ----------------------------------------- 1 file changed, 91 deletions(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 8aae695c00..88db86597e 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -111,98 +111,7 @@ let validate json = Format.printf "validate: %a\n" (Json_encoding.print_error ?print_unknown:None) e; failwith "JsonSchema2.validate" - -(** raise when you cannot parse the path *) -exception PathParseError - -(** raise when there is an type error *) -exception ConfTypeError - -(** Type of the index *) -type index = Int of int (** and integer *) - | App (** prepend to the list *) - | Rem (** remove from the list *) - | New (** create a new list *) - -(** Type of the path *) -type path = Here (** we are there *) - | Select of string * path (** we need to select an field *) - | Index of index * path (** we need to select an array index *) - -open Printf - -(** Path printing. *) -let rec print_path' ch = function - | Here -> () - | Select (s,p) -> fprintf ch ".%s%a" s print_path' p - | Index (Int i,p) -> fprintf ch "[%d]%a" i print_path' p - | Index (App ,p) -> fprintf ch "[+]%a" print_path' p - | Index (Rem ,p) -> fprintf ch "[-]%a" print_path' p - | Index (New ,p) -> fprintf ch "[*]%a" print_path' p - - -(** Parse an index. *) -let parse_index s = - try if s = "+" then App - else if s = "*" then New - else if s = "-" then Rem - else Int (int_of_string s) - with Failure _ -> raise PathParseError - -(** Helper function [split c1 c2 xs] that splits [xs] on [c1] or [c2] *) -let split c1 c2 xs = - let l = String.length xs in - let rec split' i = - if i - let fld, pth = split '.' '[' (String.lchop s) in - Select (fld, parse_path' pth) - | '[' -> - let idx, pth = String.split (String.lchop s) "]" in - Index (parse_index idx, parse_path' pth) - | _ -> raise PathParseError - -(** Parse a string path, but you may ignore the first dot. *) -let parse_path (s:string) : path = - let s = String.trim s in - try - if String.length s = 0 then Here else begin - let fld, pth = split '.' '[' s in - if fld = "" - then parse_path' pth - else Select (fld, parse_path' pth) - end - with PathParseError -> - eprintf "Error: Couldn't parse the json path '%s'\n%!" s; - failwith "parsing" - open Json_encoding - -let convert_opt name desc def: unit encoding = - let rec convert_path = function - | Select (s, Here) -> - obj1 @@ dft ~title:name ~description:desc s unit () (* TODO: correct type *) - | Select (s, path') -> - let obj' = convert_path path' in - obj1 @@ dft s obj' () - | _ -> assert false - in - let path = parse_path name in - convert_path path - open Json_schema (** The ultimate convenience function for writing values. *) From 02fba604dec8347ebb2cc380429666725968e4a3 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 13 Dec 2021 14:06:14 +0200 Subject: [PATCH 16/55] Fix integer JSON schema generation --- src/util/jsonSchema2.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 88db86597e..85fe081d07 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -136,7 +136,7 @@ let rec convert_schema' (json: Yojson.Safe.t) opts (prefix: string): element * D | `Bool b -> element' @@ Boolean | `Int i -> - element' @@ Number numeric_specs + element' @@ Integer numeric_specs | `List xs -> let element_schema = match prefix with | ".phases" -> element (Id_ref "") (* refer to entire schema itself *) From def40abf27268b368f272397efe1de13d4bfdf62 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 13 Dec 2021 14:06:31 +0200 Subject: [PATCH 17/55] Add schema conversion to all required fields --- src/util/jsonSchema2.ml | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 85fe081d07..9b15628039 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -178,12 +178,31 @@ let rec create_defaults (element: element): Yojson.Safe.t = failwith "create_defaults" end +let rec require_all (element: element): element = + let element_kind' = match element.kind with + | String _ + | Boolean + | Id_ref _ + | Integer _ + | Number _ -> element.kind + | Monomorphic_array (el, array_specs) -> + Monomorphic_array (require_all el, {array_specs with additional_items = Option.map require_all array_specs.additional_items}) + | Object object_specs -> + Object {object_specs with properties = List.map (fun (name, el, req, something) -> (name, require_all el, true, something)) object_specs.properties} + | _ -> + Format.printf "%a\n" Json_schema.pp (create element); + failwith "require_all" + in + {element with kind = element_kind'} + let convert_schema json opts = try let sch = create @@ {(fst @@ convert_schema' json opts "") with id = Some ""} in (* add id to make create defs check happy, doesn't get outputted apparently *) (* Format.printf "schema: %a\n" Json_schema.pp sch; *) (* Format.printf "schema2: %a\n" (Yojson.Safe.pretty_print ~std:true) (JS.to_json sch) *) Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema.json") (JS.to_json sch); + let sch_req = create @@ {(require_all (root sch)) with id = Some ""} in + Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema_require.json") (JS.to_json sch_req); let defaults = create_defaults (root sch) in Yojson.Safe.pretty_to_channel (Stdlib.open_out "defaults.json") defaults with (Json_schema.Dangling_reference u as e) -> From 3ee612a3cab85d19db03b25a7e1c8b119c7f4a70 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 13 Dec 2021 17:15:19 +0200 Subject: [PATCH 18/55] Remove category description from JSON schema root --- src/util/jsonSchema2.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 9b15628039..1744340222 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -153,7 +153,7 @@ let rec convert_schema' (json: Yojson.Safe.t) opts (prefix: string): element * D in let cat = Option.get !cat' in let el = match BatString.index_after_n '.' 2 prefix with - | exception Not_found when prefix = ".interact" -> (* isn't Std *) + | exception Not_found when prefix = ".interact" || prefix = "" -> (* isn't Std; is root *) element @@ Object { object_specs with properties; additional_properties = None} | exception Not_found -> {(element @@ Object { object_specs with properties; additional_properties = None}) with title = Some (DefaultsCategory.show_category cat); description = Some (DefaultsCategory.catDescription cat)} From bdb317d028fedd892afabb7823bea64ce0fdcd12 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Dec 2021 13:09:41 +0200 Subject: [PATCH 19/55] Add missing cases to encoding_of_schema_element --- src/util/jsonSchema2.ml | 25 ++++++++++++++++++------- 1 file changed, 18 insertions(+), 7 deletions(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 1744340222..60e09bc83b 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -82,27 +82,34 @@ let default_schema = {schema| let schema = JS.of_json (Yojson.Safe.from_string default_schema) -let erase: type t. t Json_encoding.encoding -> unit Json_encoding.encoding = fun encoding -> Json_encoding.conv (fun _ -> failwith "asd") (fun _ -> ()) encoding +let erase: type t. t Json_encoding.encoding -> unit Json_encoding.encoding = fun encoding -> Json_encoding.conv (fun _ -> failwith "erase construct") (fun _ -> ()) encoding -let rec encoding_of_schema_element (schema_element: Json_schema.element): unit Json_encoding.encoding = +let rec encoding_of_schema_element (top: unit Json_encoding.encoding) (schema_element: Json_schema.element): unit Json_encoding.encoding = let open Json_encoding in match schema_element.kind with | Any -> unit | String string_specs -> erase string + | Boolean -> erase bool + | Integer numeric_specs -> erase int + | Monomorphic_array (el, array_specs) -> + erase @@ array (encoding_of_schema_element top el) + | Id_ref "" -> + top | Object object_specs -> List.fold_left (fun acc (name, element, required, _) -> let field = if required then - req name (encoding_of_schema_element element) + req name (encoding_of_schema_element top element) else - dft name (encoding_of_schema_element element) () + dft name (encoding_of_schema_element top element) () in erase @@ merge_objs acc (obj1 field) - ) (Option.map_default encoding_of_schema_element empty object_specs.additional_properties) object_specs.properties + ) (Option.map_default (encoding_of_schema_element top) empty object_specs.additional_properties) object_specs.properties | _ -> failwith (Format.asprintf "encoding_of_schema_element: %a" Json_schema.pp (Json_schema.create schema_element)) let encoding_of_schema (schema: Json_schema.schema): unit Json_encoding.encoding = - encoding_of_schema_element (Json_schema.root schema) + let root = Json_schema.root schema in + Json_encoding.mu "" (fun top -> encoding_of_schema_element top root) let validate json = match JE.destruct (encoding_of_schema schema) json with @@ -204,6 +211,10 @@ let convert_schema json opts = let sch_req = create @@ {(require_all (root sch)) with id = Some ""} in Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema_require.json") (JS.to_json sch_req); let defaults = create_defaults (root sch) in - Yojson.Safe.pretty_to_channel (Stdlib.open_out "defaults.json") defaults + Yojson.Safe.pretty_to_channel (Stdlib.open_out "defaults.json") defaults; + (* let defaults2 = JE.construct ~include_default_fields:`Always (encoding_of_schema sch) () in *) + (* erase construct fails *) + (* Yojson.Safe.pretty_to_channel (Stdlib.open_out "defaults2.json") defaults2; *) + () with (Json_schema.Dangling_reference u as e) -> Json_schema.print_error Format.err_formatter e From 282751e4b4cf35e82e3d03c457b9f313d666b1ee Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Dec 2021 14:45:11 +0200 Subject: [PATCH 20/55] Add new JSON schema validation to options, including --conf --- src/util/gobConfig.ml | 6 ++++-- src/util/jsonSchema2.ml | 17 ++++++++++------- 2 files changed, 14 insertions(+), 9 deletions(-) diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index 642bc77439..b094413ac0 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -270,8 +270,8 @@ struct o := set_value v !o orig_pth; validate conf_schema !json_conf; - (* if not !build_config then (* object incomplete during building *) - JsonSchema2.validate !json_conf *) + if not !build_config then (* object incomplete during building *) + JsonSchema2.validate !json_conf; () (** Helper function for reading values. Handles error messages. *) @@ -362,7 +362,9 @@ struct (** Merge configurations form a file with current. *) let merge_file fn = let v = Yojson.Safe.from_channel % BatIO.to_input_channel |> File.with_file_in fn in + JsonSchema2.validate v; json_conf := GobYojson.merge !json_conf v; + JsonSchema2.validate !json_conf; drop_memo (); if tracing then trace "conf" "Merging with '%s', resulting\n%a.\n" fn GobYojson.pretty !json_conf end diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 60e09bc83b..9a0e3d7890 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -111,13 +111,6 @@ let encoding_of_schema (schema: Json_schema.schema): unit Json_encoding.encoding let root = Json_schema.root schema in Json_encoding.mu "" (fun top -> encoding_of_schema_element top root) -let validate json = - match JE.destruct (encoding_of_schema schema) json with - | _ -> () - | exception (Json_encoding.Cannot_destruct _ as e) -> - Format.printf "validate: %a\n" (Json_encoding.print_error ?print_unknown:None) e; - failwith "JsonSchema2.validate" - open Json_encoding open Json_schema @@ -202,9 +195,12 @@ let rec require_all (element: element): element = in {element with kind = element_kind'} +let global_schema = ref any + let convert_schema json opts = try let sch = create @@ {(fst @@ convert_schema' json opts "") with id = Some ""} in (* add id to make create defs check happy, doesn't get outputted apparently *) + global_schema := sch; (* Format.printf "schema: %a\n" Json_schema.pp sch; *) (* Format.printf "schema2: %a\n" (Yojson.Safe.pretty_print ~std:true) (JS.to_json sch) *) Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema.json") (JS.to_json sch); @@ -218,3 +214,10 @@ let convert_schema json opts = () with (Json_schema.Dangling_reference u as e) -> Json_schema.print_error Format.err_formatter e + +let validate json = + match JE.destruct (encoding_of_schema !global_schema) json with + | _ -> () + | exception (Json_encoding.Cannot_destruct _ as e) -> + Format.printf "validate: %a\n" (Json_encoding.print_error ?print_unknown:None) e; + failwith "JsonSchema2.validate" From 79f39d5dbf99b03922a2e3ec0d02d512a11a60cc Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Dec 2021 14:57:53 +0200 Subject: [PATCH 21/55] Reverse Defaults and GobConfig dependency --- src/util/defaults.ml | 8 +------- src/util/gobConfig.ml | 9 +++++++++ 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/src/util/defaults.ml b/src/util/defaults.ml index 453c15df1b..2de2367a2e 100644 --- a/src/util/defaults.ml +++ b/src/util/defaults.ml @@ -13,8 +13,7 @@ let registrar = ref [] (** A function to register a variable *) let reg (c:category) (n:string) (def:string) (desc:string) = - registrar := (c,(n,(desc,def))) :: !registrar; - GobConfig.(build_config := true; set_auto n def; build_config := false) + registrar := (c,(n,(desc,def))) :: !registrar (** find all associations in the list *) let rec assoc_all k = function @@ -339,8 +338,3 @@ let default_schema = {schema| , "gobview" : {} } }|schema} - -let _ = - let v = Yojson.Safe.from_string default_schema in - GobConfig.addenum_sch v; - JsonSchema2.convert_schema !GobConfig.json_conf @@ List.map (fun (c, (n, p)) -> (n, (c, p))) !registrar diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index b094413ac0..1285a4da2d 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -370,3 +370,12 @@ struct end include Impl + +let () = + build_config := true; + List.iter (fun (c, (n, (desc, def))) -> set_auto n def) !Defaults.registrar; + build_config := false; + + addenum_sch (Yojson.Safe.from_string Defaults.default_schema); + + JsonSchema2.convert_schema !json_conf @@ List.map (fun (c, (n, p)) -> (n, (c, p))) !Defaults.registrar From 60c368ee96ca8c9a76886362f24c9e36fd3fe454 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Dec 2021 15:03:07 +0200 Subject: [PATCH 22/55] Create Options module --- src/util/gobConfig.ml | 4 +--- src/util/options.ml | 2 ++ 2 files changed, 3 insertions(+), 3 deletions(-) create mode 100644 src/util/options.ml diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index 1285a4da2d..9ee1a708e4 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -376,6 +376,4 @@ let () = List.iter (fun (c, (n, (desc, def))) -> set_auto n def) !Defaults.registrar; build_config := false; - addenum_sch (Yojson.Safe.from_string Defaults.default_schema); - - JsonSchema2.convert_schema !json_conf @@ List.map (fun (c, (n, p)) -> (n, (c, p))) !Defaults.registrar + addenum_sch (Yojson.Safe.from_string Defaults.default_schema) diff --git a/src/util/options.ml b/src/util/options.ml new file mode 100644 index 0000000000..81dea39e2a --- /dev/null +++ b/src/util/options.ml @@ -0,0 +1,2 @@ +let () = + JsonSchema2.convert_schema !GobConfig.json_conf @@ List.map (fun (c, (n, p)) -> (n, (c, p))) !Defaults.registrar From 22bc7f5f6184fe9f5ba338f5a24bd3b85e57e75d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Dec 2021 15:08:43 +0200 Subject: [PATCH 23/55] Move defaults to schema conversion to Options --- src/util/jsonSchema2.ml | 68 ------------------------------------- src/util/jsonSchema2.mli | 3 -- src/util/options.ml | 72 +++++++++++++++++++++++++++++++++++++++- 3 files changed, 71 insertions(+), 72 deletions(-) delete mode 100644 src/util/jsonSchema2.mli diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 9a0e3d7890..e08e51c025 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -114,56 +114,6 @@ let encoding_of_schema (schema: Json_schema.schema): unit Json_encoding.encoding open Json_encoding open Json_schema -(** The ultimate convenience function for writing values. *) -let one_quote = Str.regexp "\'" -let parse_goblint_json s = - try - let s' = Str.global_replace one_quote "\"" s in - let v = Yojson.Safe.from_string s' in - v - with Yojson.Json_error _ -> - `String s - -let rec convert_schema' (json: Yojson.Safe.t) opts (prefix: string): element * DefaultsCategory.category = - let element' ekind = - let (cat, (desc, def)) = List.assoc (BatString.lchop prefix) opts in - (* let name = BatString.lchop @@ Filename.extension prefix in *) - ({(element ekind) with title = Some (BatString.lchop prefix); description = Some desc; default = Some (Json_repr.repr_to_any (module Json_repr.Yojson) (parse_goblint_json def))}, cat) - in - match json with - | `String s -> - element' @@ String string_specs - | `Bool b -> - element' @@ Boolean - | `Int i -> - element' @@ Integer numeric_specs - | `List xs -> - let element_schema = match prefix with - | ".phases" -> element (Id_ref "") (* refer to entire schema itself *) - | _ -> element (String string_specs) - in - element' @@ Monomorphic_array (element_schema, array_specs) - | `Assoc xs -> - let cat' = ref None in - let properties = List.map (fun (key, value) -> - let (inner, cat) = convert_schema' value opts (prefix ^ "." ^ key) in - cat' := Some cat; - (key, inner, false, None) - ) xs - in - let cat = Option.get !cat' in - let el = match BatString.index_after_n '.' 2 prefix with - | exception Not_found when prefix = ".interact" || prefix = "" -> (* isn't Std; is root *) - element @@ Object { object_specs with properties; additional_properties = None} - | exception Not_found -> - {(element @@ Object { object_specs with properties; additional_properties = None}) with title = Some (DefaultsCategory.show_category cat); description = Some (DefaultsCategory.catDescription cat)} - | _ -> - element @@ Object { object_specs with properties; additional_properties = None} - in - (el, cat) - | _ -> failwith (Format.asprintf "convert_schema': %a" Yojson.Safe.pp json) - - let rec create_defaults (element: element): Yojson.Safe.t = match element.default with | Some default -> Json_repr.any_to_repr (module Json_repr.Yojson) default @@ -197,24 +147,6 @@ let rec require_all (element: element): element = let global_schema = ref any -let convert_schema json opts = - try - let sch = create @@ {(fst @@ convert_schema' json opts "") with id = Some ""} in (* add id to make create defs check happy, doesn't get outputted apparently *) - global_schema := sch; - (* Format.printf "schema: %a\n" Json_schema.pp sch; *) - (* Format.printf "schema2: %a\n" (Yojson.Safe.pretty_print ~std:true) (JS.to_json sch) *) - Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema.json") (JS.to_json sch); - let sch_req = create @@ {(require_all (root sch)) with id = Some ""} in - Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema_require.json") (JS.to_json sch_req); - let defaults = create_defaults (root sch) in - Yojson.Safe.pretty_to_channel (Stdlib.open_out "defaults.json") defaults; - (* let defaults2 = JE.construct ~include_default_fields:`Always (encoding_of_schema sch) () in *) - (* erase construct fails *) - (* Yojson.Safe.pretty_to_channel (Stdlib.open_out "defaults2.json") defaults2; *) - () - with (Json_schema.Dangling_reference u as e) -> - Json_schema.print_error Format.err_formatter e - let validate json = match JE.destruct (encoding_of_schema !global_schema) json with | _ -> () diff --git a/src/util/jsonSchema2.mli b/src/util/jsonSchema2.mli deleted file mode 100644 index dfcfff7bf6..0000000000 --- a/src/util/jsonSchema2.mli +++ /dev/null @@ -1,3 +0,0 @@ -val validate : Json_repr.yojson -> unit - -val convert_schema: Yojson.Safe.t -> (string * (DefaultsCategory.category * (string * string))) list -> unit diff --git a/src/util/options.ml b/src/util/options.ml index 81dea39e2a..5689a6262e 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -1,2 +1,72 @@ +open Json_encoding +open Json_schema + +(** The ultimate convenience function for writing values. *) +let one_quote = Str.regexp "\'" +let parse_goblint_json s = + try + let s' = Str.global_replace one_quote "\"" s in + let v = Yojson.Safe.from_string s' in + v + with Yojson.Json_error _ -> + `String s + +let rec convert_schema' (json: Yojson.Safe.t) opts (prefix: string): element * DefaultsCategory.category = + let element' ekind = + let (cat, (desc, def)) = List.assoc (BatString.lchop prefix) opts in + (* let name = BatString.lchop @@ Filename.extension prefix in *) + ({(element ekind) with title = Some (BatString.lchop prefix); description = Some desc; default = Some (Json_repr.repr_to_any (module Json_repr.Yojson) (parse_goblint_json def))}, cat) + in + match json with + | `String s -> + element' @@ String string_specs + | `Bool b -> + element' @@ Boolean + | `Int i -> + element' @@ Integer numeric_specs + | `List xs -> + let element_schema = match prefix with + | ".phases" -> element (Id_ref "") (* refer to entire schema itself *) + | _ -> element (String string_specs) + in + element' @@ Monomorphic_array (element_schema, array_specs) + | `Assoc xs -> + let cat' = ref None in + let properties = List.map (fun (key, value) -> + let (inner, cat) = convert_schema' value opts (prefix ^ "." ^ key) in + cat' := Some cat; + (key, inner, false, None) + ) xs + in + let cat = Option.get !cat' in + let el = match BatString.index_after_n '.' 2 prefix with + | exception Not_found when prefix = ".interact" || prefix = "" -> (* isn't Std; is root *) + element @@ Object { object_specs with properties; additional_properties = None} + | exception Not_found -> + {(element @@ Object { object_specs with properties; additional_properties = None}) with title = Some (DefaultsCategory.show_category cat); description = Some (DefaultsCategory.catDescription cat)} + | _ -> + element @@ Object { object_specs with properties; additional_properties = None} + in + (el, cat) + | _ -> failwith (Format.asprintf "convert_schema': %a" Yojson.Safe.pp json) + +let convert_schema json opts = + try + let sch = create @@ {(fst @@ convert_schema' json opts "") with id = Some ""} in (* add id to make create defs check happy, doesn't get outputted apparently *) + JsonSchema2.global_schema := sch; + (* Format.printf "schema: %a\n" Json_schema.pp sch; *) + (* Format.printf "schema2: %a\n" (Yojson.Safe.pretty_print ~std:true) (JS.to_json sch) *) + Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema.json") (JsonSchema2.JS.to_json sch); + let sch_req = create @@ {(JsonSchema2.require_all (root sch)) with id = Some ""} in + Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema_require.json") (JsonSchema2.JS.to_json sch_req); + let defaults = JsonSchema2.create_defaults (root sch) in + Yojson.Safe.pretty_to_channel (Stdlib.open_out "defaults.json") defaults; + (* let defaults2 = JE.construct ~include_default_fields:`Always (encoding_of_schema sch) () in *) + (* erase construct fails *) + (* Yojson.Safe.pretty_to_channel (Stdlib.open_out "defaults2.json") defaults2; *) + () + with (Json_schema.Dangling_reference u as e) -> + Json_schema.print_error Format.err_formatter e + let () = - JsonSchema2.convert_schema !GobConfig.json_conf @@ List.map (fun (c, (n, p)) -> (n, (c, p))) !Defaults.registrar + convert_schema !GobConfig.json_conf @@ List.map (fun (c, (n, p)) -> (n, (c, p))) !Defaults.registrar From 077ce0cae989f58fcaa9f608fd45ee22df972230 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Dec 2021 15:09:42 +0200 Subject: [PATCH 24/55] Remove unused schema string from JsonSchema2 --- src/util/jsonSchema2.ml | 79 ----------------------------------------- 1 file changed, 79 deletions(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index e08e51c025..04330c4e80 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -3,85 +3,6 @@ open Prelude module JS = Json_schema.Make (Json_repr.Yojson) module JE = Json_encoding.Make (Json_repr.Yojson) -let default_schema = {schema| -{ "id" : "root" -, "type" : "object" -, "required" : ["outfile", "includes", "kernel_includes", "custom_includes", "kernel-root", "justcil", "justcfg", "printstats", "verify", "mainfun", "exitfun", "otherfun", "allglobs", "keepcpp", "tempDir", "cppflags", "kernel", "dump_globs", "result", "solver", "allfuns", "nonstatic", "colors", "g2html"] -, "additionalProperties" : false -, "properties" : - { "ana" : - { "type" : "object" - , "additionalProperties" : true - , "required" : [] - } - , "sem" : {} - , "incremental" : {} - , "trans" : {} - , "phases" : {} - , "annotation" : - { "type" : "object" - , "additionalProperties" : true - , "required" : [] - } - , "exp" : - { "type" : "object" - , "additionalProperties" : true - , "required" : [] - } - , "dbg" : - { "type" : "object" - , "additionalProperties" : true - , "required" : [] - } - , "questions" : - { "file" : "" - } - , "outfile" : {} - , "includes" : {} - , "kernel_includes" : {} - , "custom_includes" : {} - , "kernel-root" : {} - , "justcil" : {} - , "justcfg" : {} - , "printstats" : {} - , "verify" : {} - , "mainfun" : {} - , "exitfun" : {} - , "otherfun" : {} - , "allglobs" : {} - , "keepcpp" : {} - , "tempDir" : - { "type" : "string" - } - , "cppflags" : {} - , "kernel" : {} - , "dump_globs" : {} - , "result" : - { "type" : "string" - } - , "solver" : {} - , "comparesolver" : {} - , "solverdiffs" : {} - , "allfuns" : {} - , "nonstatic" : {} - , "colors" : {} - , "g2html" : {} - , "interact" : {} - , "save_run" : {} - , "load_run" : {} - , "compare_runs" : {} - , "warn_at" : {} - , "warn" : - { "type" : "object" - , "additionalProperties" : true - , "required" : ["foo"] - } - , "gobview" : {} - } -}|schema} - -let schema = JS.of_json (Yojson.Safe.from_string default_schema) - let erase: type t. t Json_encoding.encoding -> unit Json_encoding.encoding = fun encoding -> Json_encoding.conv (fun _ -> failwith "erase construct") (fun _ -> ()) encoding let rec encoding_of_schema_element (top: unit Json_encoding.encoding) (schema_element: Json_schema.element): unit Json_encoding.encoding = From 8067e0a943ce699f44b152b217bf2d51474bd000 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Dec 2021 15:33:31 +0200 Subject: [PATCH 25/55] Refactor element_category_of_defaults_json --- src/util/options.ml | 79 +++++++++++++++++++++++++++++---------------- 1 file changed, 51 insertions(+), 28 deletions(-) diff --git a/src/util/options.ml b/src/util/options.ml index 5689a6262e..59f86d5179 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -1,6 +1,7 @@ open Json_encoding open Json_schema +(* TODO: deduplicate with GobConfig *) (** The ultimate convenience function for writing values. *) let one_quote = Str.regexp "\'" let parse_goblint_json s = @@ -11,48 +12,69 @@ let parse_goblint_json s = with Yojson.Json_error _ -> `String s -let rec convert_schema' (json: Yojson.Safe.t) opts (prefix: string): element * DefaultsCategory.category = - let element' ekind = - let (cat, (desc, def)) = List.assoc (BatString.lchop prefix) opts in - (* let name = BatString.lchop @@ Filename.extension prefix in *) - ({(element ekind) with title = Some (BatString.lchop prefix); description = Some desc; default = Some (Json_repr.repr_to_any (module Json_repr.Yojson) (parse_goblint_json def))}, cat) +(* Convert old Defaults options to schema. *) + +type defaults = (string * (DefaultsCategory.category * string * string)) list + +let rec element_category_of_defaults_json (defaults: defaults) (json: Yojson.Safe.t) (path: string): element * DefaultsCategory.category = + let element_defaults kind = (* element with metadata from defaults *) + let name = BatString.lchop path in (* chop initial . *) + let (category, description, default) = List.assoc name defaults in + let default_json = parse_goblint_json default in + let element = { (element kind) with + title = Some name; + description = Some description; + default = Some (Json_repr.repr_to_any (module Json_repr.Yojson) default_json); + } + in + (element, category) in match json with | `String s -> - element' @@ String string_specs + element_defaults @@ String string_specs | `Bool b -> - element' @@ Boolean + element_defaults @@ Boolean | `Int i -> - element' @@ Integer numeric_specs + element_defaults @@ Integer numeric_specs | `List xs -> - let element_schema = match prefix with + let element_element = match path with | ".phases" -> element (Id_ref "") (* refer to entire schema itself *) - | _ -> element (String string_specs) + | _ -> element (String string_specs) (* all other lists contain strings *) in - element' @@ Monomorphic_array (element_schema, array_specs) + element_defaults @@ Monomorphic_array (element_element, array_specs) | `Assoc xs -> - let cat' = ref None in + let category = ref None in let properties = List.map (fun (key, value) -> - let (inner, cat) = convert_schema' value opts (prefix ^ "." ^ key) in - cat' := Some cat; - (key, inner, false, None) + let (field_element, field_category) = element_category_of_defaults_json defaults value (path ^ "." ^ key) in + category := Some field_category; (* category from defaults for object description *) + (key, field_element, false, None) ) xs in - let cat = Option.get !cat' in - let el = match BatString.index_after_n '.' 2 prefix with - | exception Not_found when prefix = ".interact" || prefix = "" -> (* isn't Std; is root *) - element @@ Object { object_specs with properties; additional_properties = None} - | exception Not_found -> - {(element @@ Object { object_specs with properties; additional_properties = None}) with title = Some (DefaultsCategory.show_category cat); description = Some (DefaultsCategory.catDescription cat)} - | _ -> - element @@ Object { object_specs with properties; additional_properties = None} + let category = Option.get !category in + let element = element @@ Object { + object_specs with + properties; + additional_properties = None; (* forbid additional properties *) + } + in + let element = match BatString.index_after_n '.' 2 path with + | exception Not_found when path = ".interact" || path = "" -> (* interact isn't Std or is root *) + element + | exception Not_found -> (* category *) + { element with + title = Some (DefaultsCategory.show_category category); + description = Some (DefaultsCategory.catDescription category); + } + | _ -> (* inner object, not category *) + element in - (el, cat) - | _ -> failwith (Format.asprintf "convert_schema': %a" Yojson.Safe.pp json) + (element, category) + | _ -> + failwith (Format.asprintf "element_category_of_defaults_json: %a" Yojson.Safe.pp json) -let convert_schema json opts = +let convert_schema opts json = try - let sch = create @@ {(fst @@ convert_schema' json opts "") with id = Some ""} in (* add id to make create defs check happy, doesn't get outputted apparently *) + let sch = create @@ {(fst @@ element_category_of_defaults_json opts json "") with id = Some ""} in (* add id to make create defs check happy, doesn't get outputted apparently *) JsonSchema2.global_schema := sch; (* Format.printf "schema: %a\n" Json_schema.pp sch; *) (* Format.printf "schema2: %a\n" (Yojson.Safe.pretty_print ~std:true) (JS.to_json sch) *) @@ -69,4 +91,5 @@ let convert_schema json opts = Json_schema.print_error Format.err_formatter e let () = - convert_schema !GobConfig.json_conf @@ List.map (fun (c, (n, p)) -> (n, (c, p))) !Defaults.registrar + let defaults = List.map (fun (c, (n, (desc, def))) -> (n, (c, desc, def))) !Defaults.registrar in (* transform for assoc list lookup by name *) + convert_schema defaults !GobConfig.json_conf From ea5fded8d6c1a65c881104197d1f4259510abb72 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Dec 2021 15:37:48 +0200 Subject: [PATCH 26/55] Refactor schema_of_defaults_json --- src/util/options.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/util/options.ml b/src/util/options.ml index 59f86d5179..fa4538a289 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -72,9 +72,16 @@ let rec element_category_of_defaults_json (defaults: defaults) (json: Yojson.Saf | _ -> failwith (Format.asprintf "element_category_of_defaults_json: %a" Yojson.Safe.pp json) +let create_schema element = + create @@ { element with id = Some "" } (* add id to make create defs check happy, doesn't get outputted apparently *) + +let schema_of_defaults_json defaults json = + let (element, _) = element_category_of_defaults_json defaults json "" in + create_schema element + let convert_schema opts json = try - let sch = create @@ {(fst @@ element_category_of_defaults_json opts json "") with id = Some ""} in (* add id to make create defs check happy, doesn't get outputted apparently *) + let sch = schema_of_defaults_json opts json in JsonSchema2.global_schema := sch; (* Format.printf "schema: %a\n" Json_schema.pp sch; *) (* Format.printf "schema2: %a\n" (Yojson.Safe.pretty_print ~std:true) (JS.to_json sch) *) From 51e0ca75d616a2576ae97cfc41b491e783b3862a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Dec 2021 15:49:02 +0200 Subject: [PATCH 27/55] Refactor schema_require_all --- src/util/jsonSchema2.ml | 28 +++++++++++++++++++++------- src/util/options.ml | 6 ++---- 2 files changed, 23 insertions(+), 11 deletions(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 04330c4e80..1f688e6492 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -49,22 +49,36 @@ let rec create_defaults (element: element): Yojson.Safe.t = failwith "create_defaults" end -let rec require_all (element: element): element = - let element_kind' = match element.kind with +let create_schema element = + create @@ { element with id = Some "" } (* add id to make create defs check happy for phases Id_ref, doesn't get outputted apparently *) + +let rec element_require_all (element: element): element = + let kind' = match element.kind with | String _ | Boolean | Id_ref _ | Integer _ | Number _ -> element.kind - | Monomorphic_array (el, array_specs) -> - Monomorphic_array (require_all el, {array_specs with additional_items = Option.map require_all array_specs.additional_items}) + | Monomorphic_array (element_element, array_specs) -> + let array_specs' = { array_specs with + additional_items = Option.map element_require_all array_specs.additional_items; + } + in + Monomorphic_array (element_require_all element_element, array_specs') | Object object_specs -> - Object {object_specs with properties = List.map (fun (name, el, req, something) -> (name, require_all el, true, something)) object_specs.properties} + let properties' = List.map (fun (name, field_element, required, unknown) -> + (name, element_require_all field_element, true, unknown) (* change required to true *) + ) object_specs.properties + in + Object { object_specs with properties = properties' } | _ -> Format.printf "%a\n" Json_schema.pp (create element); - failwith "require_all" + failwith "element_require_all" in - {element with kind = element_kind'} + { element with kind = kind' } + +let schema_require_all (schema: schema): schema = + create_schema (element_require_all (root schema)) let global_schema = ref any diff --git a/src/util/options.ml b/src/util/options.ml index fa4538a289..f266121c51 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -72,12 +72,10 @@ let rec element_category_of_defaults_json (defaults: defaults) (json: Yojson.Saf | _ -> failwith (Format.asprintf "element_category_of_defaults_json: %a" Yojson.Safe.pp json) -let create_schema element = - create @@ { element with id = Some "" } (* add id to make create defs check happy, doesn't get outputted apparently *) let schema_of_defaults_json defaults json = let (element, _) = element_category_of_defaults_json defaults json "" in - create_schema element + JsonSchema2.create_schema element let convert_schema opts json = try @@ -86,7 +84,7 @@ let convert_schema opts json = (* Format.printf "schema: %a\n" Json_schema.pp sch; *) (* Format.printf "schema2: %a\n" (Yojson.Safe.pretty_print ~std:true) (JS.to_json sch) *) Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema.json") (JsonSchema2.JS.to_json sch); - let sch_req = create @@ {(JsonSchema2.require_all (root sch)) with id = Some ""} in + let sch_req = JsonSchema2.schema_require_all sch in Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema_require.json") (JsonSchema2.JS.to_json sch_req); let defaults = JsonSchema2.create_defaults (root sch) in Yojson.Safe.pretty_to_channel (Stdlib.open_out "defaults.json") defaults; From 836bb7e5dd45bcc06ebe1599779f10087feef54d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Dec 2021 15:50:41 +0200 Subject: [PATCH 28/55] Reverse defaults to fix schema order --- src/util/defaults.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/util/defaults.ml b/src/util/defaults.ml index 2de2367a2e..55609b3dd8 100644 --- a/src/util/defaults.ml +++ b/src/util/defaults.ml @@ -262,6 +262,10 @@ let _ = () ; reg Warnings "warn.debug" "false" "Debug severity messages" ; reg Warnings "warn.success" "true" "Success severity messages" + +let () = + registrar := List.rev !registrar + let default_schema = {schema| { "id" : "root" , "type" : "object" From a4ed797c3669ec33c67dbfa4ec7cc1135996be19 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Dec 2021 15:58:37 +0200 Subject: [PATCH 29/55] Refactor schema_defaults --- src/util/jsonSchema2.ml | 14 +++++++++----- src/util/options.ml | 2 +- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 1f688e6492..af1bff0bb7 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -35,20 +35,24 @@ let encoding_of_schema (schema: Json_schema.schema): unit Json_encoding.encoding open Json_encoding open Json_schema -let rec create_defaults (element: element): Yojson.Safe.t = +let rec element_defaults (element: element): Yojson.Safe.t = match element.default with - | Some default -> Json_repr.any_to_repr (module Json_repr.Yojson) default + | Some default -> + Json_repr.any_to_repr (module Json_repr.Yojson) default | None -> begin match element.kind with | Object object_specs -> - `Assoc (List.map (fun (name, el, _, _) -> - (name, create_defaults el) + `Assoc (List.map (fun (name, field_element, _, _) -> + (name, element_defaults field_element) ) object_specs.properties) | _ -> Format.printf "%a\n" Json_schema.pp (create element); - failwith "create_defaults" + failwith "element_defaults" end +let schema_defaults (schema: schema): Yojson.Safe.t = + element_defaults (root schema) + let create_schema element = create @@ { element with id = Some "" } (* add id to make create defs check happy for phases Id_ref, doesn't get outputted apparently *) diff --git a/src/util/options.ml b/src/util/options.ml index f266121c51..e8f97f50e2 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -86,7 +86,7 @@ let convert_schema opts json = Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema.json") (JsonSchema2.JS.to_json sch); let sch_req = JsonSchema2.schema_require_all sch in Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema_require.json") (JsonSchema2.JS.to_json sch_req); - let defaults = JsonSchema2.create_defaults (root sch) in + let defaults = JsonSchema2.schema_defaults sch in Yojson.Safe.pretty_to_channel (Stdlib.open_out "defaults.json") defaults; (* let defaults2 = JE.construct ~include_default_fields:`Always (encoding_of_schema sch) () in *) (* erase construct fails *) From 8d142d214af7bafd594c93ba16ff27fc530ffdd9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Dec 2021 16:08:54 +0200 Subject: [PATCH 30/55] Refactor schema generation --- src/util/options.ml | 29 ++++++++++------------------- 1 file changed, 10 insertions(+), 19 deletions(-) diff --git a/src/util/options.ml b/src/util/options.ml index e8f97f50e2..89496fae79 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -72,29 +72,20 @@ let rec element_category_of_defaults_json (defaults: defaults) (json: Yojson.Saf | _ -> failwith (Format.asprintf "element_category_of_defaults_json: %a" Yojson.Safe.pp json) - let schema_of_defaults_json defaults json = let (element, _) = element_category_of_defaults_json defaults json "" in JsonSchema2.create_schema element -let convert_schema opts json = - try - let sch = schema_of_defaults_json opts json in - JsonSchema2.global_schema := sch; - (* Format.printf "schema: %a\n" Json_schema.pp sch; *) - (* Format.printf "schema2: %a\n" (Yojson.Safe.pretty_print ~std:true) (JS.to_json sch) *) - Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema.json") (JsonSchema2.JS.to_json sch); - let sch_req = JsonSchema2.schema_require_all sch in - Yojson.Safe.pretty_to_channel (Stdlib.open_out "schema_require.json") (JsonSchema2.JS.to_json sch_req); - let defaults = JsonSchema2.schema_defaults sch in - Yojson.Safe.pretty_to_channel (Stdlib.open_out "defaults.json") defaults; - (* let defaults2 = JE.construct ~include_default_fields:`Always (encoding_of_schema sch) () in *) - (* erase construct fails *) - (* Yojson.Safe.pretty_to_channel (Stdlib.open_out "defaults2.json") defaults2; *) - () - with (Json_schema.Dangling_reference u as e) -> - Json_schema.print_error Format.err_formatter e let () = let defaults = List.map (fun (c, (n, (desc, def))) -> (n, (c, desc, def))) !Defaults.registrar in (* transform for assoc list lookup by name *) - convert_schema defaults !GobConfig.json_conf + + let schema = schema_of_defaults_json defaults !GobConfig.json_conf in + JsonSchema2.global_schema := schema; + Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.schema.json") (JsonSchema2.JS.to_json schema); + + let require_all = JsonSchema2.schema_require_all schema in + Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.require-all.schema.json") (JsonSchema2.JS.to_json require_all); + + let defaults = JsonSchema2.schema_defaults schema in + Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.defaults.json") defaults From 2f866721566ab50c86021d36dd42f9d7f8c7a311 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 15 Dec 2021 13:09:17 +0200 Subject: [PATCH 31/55] Register json-data-encoding exception printers --- src/util/jsonSchema2.ml | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index af1bff0bb7..abb5aed9b1 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -92,3 +92,24 @@ let validate json = | exception (Json_encoding.Cannot_destruct _ as e) -> Format.printf "validate: %a\n" (Json_encoding.print_error ?print_unknown:None) e; failwith "JsonSchema2.validate" + +let () = Printexc.register_printer (function + | Json_encoding.Unexpected _ + | Json_encoding.No_case_matched _ + | Json_encoding.Bad_array_size _ + | Json_encoding.Missing_field _ + | Json_encoding.Unexpected_field _ + | Json_encoding.Bad_schema _ + | Json_encoding.Cannot_destruct _ + | Json_schema.Cannot_parse _ + | Json_schema.Dangling_reference _ + | Json_schema.Bad_reference _ + | Json_schema.Unexpected _ + | Json_schema.Duplicate_definition _ + | Json_query.Illegal_pointer_notation _ + | Json_query.Unsupported_path_item _ + | Json_query.Cannot_merge _ as exn -> + let msg = Format.asprintf "Json_encoding: %a" (Json_encoding.print_error ?print_unknown:None) exn in + Some msg + | _ -> None (* for other exceptions *) + ) From 0ccfe38ce3fd1f16268079349bd4e482d0885dbd Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 15 Dec 2021 13:11:05 +0200 Subject: [PATCH 32/55] Extract JSON schema Validator functor --- src/util/jsonSchema2.ml | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index abb5aed9b1..6844d08b5a 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -84,14 +84,28 @@ let rec element_require_all (element: element): element = let schema_require_all (schema: schema): schema = create_schema (element_require_all (root schema)) + +module type Schema = +sig + val schema: schema +end + +module Validator (Schema: Schema) = +struct + let schema_encoding = encoding_of_schema Schema.schema + + let validate_exn json = JE.destruct schema_encoding json + + (* TODO: bool-returning validate? *) +end + + let global_schema = ref any let validate json = - match JE.destruct (encoding_of_schema !global_schema) json with - | _ -> () - | exception (Json_encoding.Cannot_destruct _ as e) -> - Format.printf "validate: %a\n" (Json_encoding.print_error ?print_unknown:None) e; - failwith "JsonSchema2.validate" + let module Validator = Validator (struct let schema = !global_schema end) in + Validator.validate_exn json + let () = Printexc.register_printer (function | Json_encoding.Unexpected _ From f949d130bae5eba3ca605c289cc673fdc394e89f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 15 Dec 2021 15:23:26 +0200 Subject: [PATCH 33/55] Add --options and --all-options --- src/maingoblint.ml | 2 ++ src/util/options.ml | 61 +++++++++++++++++++++++++++++++++++++++------ 2 files changed, 56 insertions(+), 7 deletions(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index ebad804c4f..155fb199ba 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -102,6 +102,8 @@ let option_spec_list = ; "--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), "" + ; "--options" , Arg.Unit (fun () -> Options.print_options (); exit 0), "" + ; "--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, "" diff --git a/src/util/options.ml b/src/util/options.ml index 89496fae79..e828f86d04 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -17,8 +17,8 @@ let parse_goblint_json s = type defaults = (string * (DefaultsCategory.category * string * string)) list let rec element_category_of_defaults_json (defaults: defaults) (json: Yojson.Safe.t) (path: string): element * DefaultsCategory.category = + let name = BatString.lchop path in (* chop initial . *) let element_defaults kind = (* element with metadata from defaults *) - let name = BatString.lchop path in (* chop initial . *) let (category, description, default) = List.assoc name defaults in let default_json = parse_goblint_json default in let element = { (element kind) with @@ -58,7 +58,11 @@ let rec element_category_of_defaults_json (defaults: defaults) (json: Yojson.Saf } in let element = match BatString.index_after_n '.' 2 path with - | exception Not_found when path = ".interact" || path = "" -> (* interact isn't Std or is root *) + | exception Not_found when path = ".interact" -> (* interact isn't Std *) + { element with + title = Some name; + } + | exception Not_found when path = "" -> (* is root *) element | exception Not_found -> (* category *) { element with @@ -66,7 +70,9 @@ let rec element_category_of_defaults_json (defaults: defaults) (json: Yojson.Saf description = Some (DefaultsCategory.catDescription category); } | _ -> (* inner object, not category *) - element + { element with + title = Some name; + } in (element, category) | _ -> @@ -77,15 +83,56 @@ let schema_of_defaults_json defaults json = JsonSchema2.create_schema element -let () = + +let schema = let defaults = List.map (fun (c, (n, (desc, def))) -> (n, (c, desc, def))) !Defaults.registrar in (* transform for assoc list lookup by name *) + schema_of_defaults_json defaults !GobConfig.json_conf + +let require_all = JsonSchema2.schema_require_all schema - let schema = schema_of_defaults_json defaults !GobConfig.json_conf in +let defaults = JsonSchema2.schema_defaults schema + +let () = JsonSchema2.global_schema := schema; Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.schema.json") (JsonSchema2.JS.to_json schema); - let require_all = JsonSchema2.schema_require_all schema in Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.require-all.schema.json") (JsonSchema2.JS.to_json require_all); - let defaults = JsonSchema2.schema_defaults schema in Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.defaults.json") defaults + +let rec pp_options ~levels ppf (element: element) = + match element.kind with + | String _ + | Boolean + | Integer _ + | Number _ + | Monomorphic_array _ -> + (* Format.fprintf ppf "%s: %s (%a)" (Option.get element.title) (Option.get element.description) (Yojson.Safe.pretty_print ~std:false) (Json_repr.any_to_repr (module Json_repr.Yojson) (Option.get element.default)) *) + (* Yojson screws up box indentation somehow... *) + Format.fprintf ppf "%s: %s (%s)" (Option.get element.title) (Option.get element.description) (Yojson.Safe.to_string (Json_repr.any_to_repr (module Json_repr.Yojson) (Option.get element.default))) + | Object object_specs when levels > 0 -> + let properties = List.filter (fun (name, field_element, _, _) -> + match field_element.kind with + | Object _ when levels = 1 -> false (* avoid empty lines with --options *) + | _ -> true + ) object_specs.properties + in + let pp_property ppf (name, field_element, _, _) = + Format.fprintf ppf "%a" (pp_options ~levels:(levels - 1)) field_element + in + begin match element.title with + | Some title -> + Format.fprintf ppf "@[%s:@, @[%a@]@]" title (Format.pp_print_list pp_property) properties + | None -> + Format.fprintf ppf "@[%a@]" (Format.pp_print_list pp_property) properties + end + | Object _ -> + () + | _ -> + failwith "pp_options" + +let print_options () = + Format.printf "%a\n" (pp_options ~levels:1) (root schema) + +let print_all_options () = + Format.printf "%a\n" (pp_options ~levels:max_int) (root schema) From 45e92f8b9f309be8d2dd451ae02224b417bae86d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 15 Dec 2021 15:25:47 +0200 Subject: [PATCH 34/55] Add schema_to_yojson and schema_of_yojson --- src/util/jsonSchema2.ml | 3 +++ src/util/options.ml | 4 ++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 6844d08b5a..ab7dcdc72b 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -3,6 +3,9 @@ open Prelude module JS = Json_schema.Make (Json_repr.Yojson) module JE = Json_encoding.Make (Json_repr.Yojson) +let schema_to_yojson = JS.to_json +let schema_of_yojson = JS.of_json ?definitions_path:None + let erase: type t. t Json_encoding.encoding -> unit Json_encoding.encoding = fun encoding -> Json_encoding.conv (fun _ -> failwith "erase construct") (fun _ -> ()) encoding let rec encoding_of_schema_element (top: unit Json_encoding.encoding) (schema_element: Json_schema.element): unit Json_encoding.encoding = diff --git a/src/util/options.ml b/src/util/options.ml index e828f86d04..e8a1657255 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -94,9 +94,9 @@ let defaults = JsonSchema2.schema_defaults schema let () = JsonSchema2.global_schema := schema; - Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.schema.json") (JsonSchema2.JS.to_json schema); + Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.schema.json") (JsonSchema2.schema_to_yojson schema); - Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.require-all.schema.json") (JsonSchema2.JS.to_json require_all); + Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.require-all.schema.json") (JsonSchema2.schema_to_yojson require_all); Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.defaults.json") defaults From cb3b00c982e2cf2bbb781fef7aac72a24089dbf9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 15 Dec 2021 16:38:25 +0200 Subject: [PATCH 35/55] Fix exception names in json-data-encoding printer --- src/util/jsonSchema2.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index ab7dcdc72b..9419de59f7 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -117,16 +117,20 @@ let () = Printexc.register_printer (function | Json_encoding.Missing_field _ | Json_encoding.Unexpected_field _ | Json_encoding.Bad_schema _ - | Json_encoding.Cannot_destruct _ + | Json_encoding.Cannot_destruct _ as exn -> + let msg = Format.asprintf "Json_encoding: %a" (Json_encoding.print_error ?print_unknown:None) exn in + Some msg | Json_schema.Cannot_parse _ | Json_schema.Dangling_reference _ | Json_schema.Bad_reference _ | Json_schema.Unexpected _ - | Json_schema.Duplicate_definition _ + | Json_schema.Duplicate_definition _ as exn -> + let msg = Format.asprintf "Json_schema: %a" (Json_encoding.print_error ?print_unknown:None) exn in + Some msg | Json_query.Illegal_pointer_notation _ | Json_query.Unsupported_path_item _ | Json_query.Cannot_merge _ as exn -> - let msg = Format.asprintf "Json_encoding: %a" (Json_encoding.print_error ?print_unknown:None) exn in + let msg = Format.asprintf "Json_query: %a" (Json_encoding.print_error ?print_unknown:None) exn in Some msg | _ -> None (* for other exceptions *) ) From 2bf48b36993a33a85a0a821e53edeca1de2d4ebc Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 15 Dec 2021 16:41:53 +0200 Subject: [PATCH 36/55] Add parsing of options JSON schema --- src/util/jsonSchema2.ml | 1 + src/util/options.ml | 31 ++++++++++++++++++++++++++++--- 2 files changed, 29 insertions(+), 3 deletions(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 9419de59f7..a312201e8f 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -2,6 +2,7 @@ open Prelude module JS = Json_schema.Make (Json_repr.Yojson) module JE = Json_encoding.Make (Json_repr.Yojson) +module JQ = Json_query.Make (Json_repr.Yojson) let schema_to_yojson = JS.to_json let schema_of_yojson = JS.of_json ?definitions_path:None diff --git a/src/util/options.ml b/src/util/options.ml index e8a1657255..ff772e8a32 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -83,18 +83,43 @@ let schema_of_defaults_json defaults json = JsonSchema2.create_schema element - -let schema = +let defaults_schema = let defaults = List.map (fun (c, (n, (desc, def))) -> (n, (c, desc, def))) !Defaults.registrar in (* transform for assoc list lookup by name *) schema_of_defaults_json defaults !GobConfig.json_conf +let () = + Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.schema.json") (JsonSchema2.schema_to_yojson defaults_schema) + +let schema_of_yojson json = + (* workaround for json-data-encoding not handling recursive root reference correctly *) + (* remove the reference before parsing, hack it back afterwards *) + let json = JsonSchema2.JQ.replace [`Field "properties"; `Field "phases"; `Field "items"] (`Assoc []) json in + let schema = JsonSchema2.schema_of_yojson json in (* definitions_path doesn't work, "definitions" field still hardcoded *) + let element = Json_schema.root schema in + let element = match element with + | { kind = Object ({properties; _} as object_specs); _} -> + let rec modify = function + | [] -> assert false + | ("phases", ({ Json_schema.kind = Monomorphic_array (_, array_specs); _} as field_element), required, unknown) :: props -> + ("phases", {field_element with Json_schema.kind = Monomorphic_array (Json_schema.element (Id_ref ""), array_specs)}, required, unknown) :: props + | prop :: props -> + prop :: modify props + in + {element with kind = Object {object_specs with properties = modify properties}} + | _ -> + assert false + in + JsonSchema2.create_schema element + +let schema = + schema_of_yojson (Yojson.Safe.from_file "options.schema.json") + let require_all = JsonSchema2.schema_require_all schema let defaults = JsonSchema2.schema_defaults schema let () = JsonSchema2.global_schema := schema; - Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.schema.json") (JsonSchema2.schema_to_yojson schema); Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.require-all.schema.json") (JsonSchema2.schema_to_yojson require_all); From 89a56a1aedfe055a8b9b46c746d5dcbe33d95768 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 15 Dec 2021 17:04:43 +0200 Subject: [PATCH 37/55] Use new JSON schema validation --- options.schema.json | 1823 +++++++++++++++++++++++++++++++++++++++++ src/util/gobConfig.ml | 20 +- src/util/options.ml | 4 +- 3 files changed, 1840 insertions(+), 7 deletions(-) create mode 100644 options.schema.json diff --git a/options.schema.json b/options.schema.json new file mode 100644 index 0000000000..9ca399f53d --- /dev/null +++ b/options.schema.json @@ -0,0 +1,1823 @@ +{ + "$schema": "http://json-schema.org/draft-04/schema#", + "type": "object", + "properties": { + "outfile": { + "title": "outfile", + "description": "File to print output to.", + "type": "string", + "default": "" + }, + "includes": { + "title": "includes", + "description": "List of directories to include.", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "kernel_includes": { + "title": "kernel_includes", + "description": "List of kernel directories to include.", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "custom_includes": { + "title": "custom_includes", + "description": "List of custom directories to include.", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "kernel-root": { + "title": "kernel-root", + "description": "Root directory for Linux kernel (linux-headers)", + "type": "string", + "default": "" + }, + "justcil": { + "title": "justcil", + "description": "Just parse and output the CIL.", + "type": "boolean", + "default": false + }, + "justcfg": { + "title": "justcfg", + "description": "Only output the CFG in cfg.dot .", + "type": "boolean", + "default": false + }, + "printstats": { + "title": "printstats", + "description": "Outputs timing information.", + "type": "boolean", + "default": false + }, + "verify": { + "title": "verify", + "description": + "Verify that the solver reached a post-fixpoint. Beware that disabling this also disables output of warnings since post-processing of the results is done in the verification phase!", + "type": "boolean", + "default": true + }, + "mainfun": { + "title": "mainfun", + "description": "Sets the name of the main functions.", + "type": "array", + "items": { "type": "string" }, + "default": [ "main" ] + }, + "exitfun": { + "title": "exitfun", + "description": "Sets the name of the cleanup functions.", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "otherfun": { + "title": "otherfun", + "description": "Sets the name of other functions.", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "allglobs": { + "title": "allglobs", + "description": + "Prints access information about all globals, not just races.", + "type": "boolean", + "default": false + }, + "keepcpp": { + "title": "keepcpp", + "description": + "Keep the intermediate output of running the C preprocessor.", + "type": "boolean", + "default": false + }, + "tempDir": { + "title": "tempDir", + "description": "Reuse temporary directory for preprocessed files.", + "type": "string", + "default": "" + }, + "cppflags": { + "title": "cppflags", + "description": "Pre-processing parameters.", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "kernel": { + "title": "kernel", + "description": "For analyzing Linux Device Drivers.", + "type": "boolean", + "default": false + }, + "dump_globs": { + "title": "dump_globs", + "description": "Print out the global invariant.", + "type": "boolean", + "default": false + }, + "result": { + "title": "result", + "description": + "Result style: none, fast_xml, json, pretty, json-messages.", + "type": "string", + "default": "none" + }, + "solver": { + "title": "solver", + "description": "Picks the solver.", + "type": "string", + "default": "td3" + }, + "comparesolver": { + "title": "comparesolver", + "description": "Picks another solver for comparison.", + "type": "string", + "default": "" + }, + "solverdiffs": { + "title": "solverdiffs", + "description": "Print out solver differences.", + "type": "boolean", + "default": false + }, + "allfuns": { + "title": "allfuns", + "description": + "Analyzes all the functions (not just beginning from main). This requires exp.earlyglobs!", + "type": "boolean", + "default": false + }, + "nonstatic": { + "title": "nonstatic", + "description": "Analyzes all non-static functions.", + "type": "boolean", + "default": false + }, + "colors": { + "title": "colors", + "description": + "Colored output (via ANSI escape codes). 'auto': enabled if stdout is a terminal (instead of a pipe); 'always', 'never'.", + "type": "string", + "default": "auto" + }, + "g2html": { + "title": "g2html", + "description": "Run g2html.jar on the generated xml.", + "type": "boolean", + "default": false + }, + "interact": { + "title": "interact", + "type": "object", + "properties": { + "out": { + "title": "interact.out", + "description": "The result directory in interactive mode.", + "type": "string", + "default": "result" + }, + "enabled": { + "title": "interact.enabled", + "description": "Is interactive mode enabled.", + "type": "boolean", + "default": false + }, + "paused": { + "title": "interact.paused", + "description": "Start interactive in pause mode.", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false + }, + "phases": { + "title": "phases", + "description": + "List of phases. Per-phase settings overwrite global ones.", + "type": "array", + "items": { "$ref": "#" }, + "default": [] + }, + "save_run": { + "title": "save_run", + "description": + "Save the result of the solver, the current configuration and meta-data about the run to this directory (if set). The data can then be loaded (without solving again) to do post-processing like generating output in a different format or comparing results.", + "type": "string", + "default": "" + }, + "load_run": { + "title": "load_run", + "description": "Load a saved run. See save_run.", + "type": "string", + "default": "" + }, + "compare_runs": { + "title": "compare_runs", + "description": + "Load these saved runs and compare the results. Note that currently only two runs can be compared!", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "warn_at": { + "title": "warn_at", + "description": + "When to output warnings. Values: 'post' (default): after solving; 'never': no warnings; 'early': for debugging - outputs warnings already while solving (may lead to spurious warnings/asserts that would disappear after narrowing).", + "type": "string", + "default": "post" + }, + "gobview": { + "title": "gobview", + "description": + "Include additional information for Gobview (e.g., the Goblint warning messages) in the directory specified by 'save_run'.", + "type": "boolean", + "default": false + }, + "ana": { + "title": "Analyses", + "description": "Options for analyses", + "type": "object", + "properties": { + "activated": { + "title": "ana.activated", + "description": "Lists of activated analyses in this phase.", + "type": "array", + "items": { "type": "string" }, + "default": [ + "expRelation", "base", "threadid", "threadflag", "threadreturn", + "escape", "mutex", "mallocWrapper" + ] + }, + "path_sens": { + "title": "ana.path_sens", + "description": "List of path-sensitive analyses", + "type": "array", + "items": { "type": "string" }, + "default": [ "OSEK", "OSEK2", "mutex", "malloc_null", "uninit" ] + }, + "ctx_insens": { + "title": "ana.ctx_insens", + "description": "List of context-insensitive analyses", + "type": "array", + "items": { "type": "string" }, + "default": [ "OSEK2", "stack_loc", "stack_trace_set" ] + }, + "cont": { + "title": "ana.cont", + "type": "object", + "properties": { + "localclass": { + "title": "ana.cont.localclass", + "description": "Analyzes classes defined in main Class.", + "type": "boolean", + "default": false + }, + "class": { + "title": "ana.cont.class", + "description": + "Analyzes all the member functions of the class (CXX.json file required).", + "type": "string", + "default": "" + } + }, + "additionalProperties": false + }, + "osek": { + "title": "ana.osek", + "type": "object", + "properties": { + "oil": { + "title": "ana.osek.oil", + "description": "Oil file for the analyzed program", + "type": "string", + "default": "" + }, + "defaults": { + "title": "ana.osek.defaults", + "description": "Generate default definitions for TASK and ISR", + "type": "boolean", + "default": true + }, + "isrprefix": { + "title": "ana.osek.isrprefix", + "description": "Prefix added by the ISR macro", + "type": "string", + "default": "function_of_" + }, + "taskprefix": { + "title": "ana.osek.taskprefix", + "description": "Prefix added by the TASK macro", + "type": "string", + "default": "function_of_" + }, + "isrsuffix": { + "title": "ana.osek.isrsuffix", + "description": "Suffix added by the ISR macro", + "type": "string", + "default": "" + }, + "tasksuffix": { + "title": "ana.osek.tasksuffix", + "description": "Suffix added by the TASK macro", + "type": "string", + "default": "" + }, + "intrpts": { + "title": "ana.osek.intrpts", + "description": "Enable constraints for interrupts.", + "type": "boolean", + "default": false + }, + "check": { + "title": "ana.osek.check", + "description": + "Check if (assumed) OSEK conventions are fullfilled.", + "type": "boolean", + "default": false + }, + "names": { + "title": "ana.osek.names", + "description": + "OSEK API function (re)names for the analysed program", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "warnfiles": { + "title": "ana.osek.warnfiles", + "description": "Print all warning types to separate file", + "type": "boolean", + "default": false + }, + "safe_vars": { + "title": "ana.osek.safe_vars", + "description": "Suppress warnings on these vars", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "safe_task": { + "title": "ana.osek.safe_task", + "description": "Ignore accesses in these tasks", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "safe_isr": { + "title": "ana.osek.safe_isr", + "description": "Ignore accesses in these isr", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "flags": { + "title": "ana.osek.flags", + "description": "List of global variables that are flags.", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "def_header": { + "title": "ana.osek.def_header", + "description": + "Generate TASK/ISR macros with default structure", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false + }, + "int": { + "title": "ana.int", + "type": "object", + "properties": { + "def_exc": { + "title": "ana.int.def_exc", + "description": + "Use IntDomain.DefExc: definite value/exclusion set.", + "type": "boolean", + "default": true + }, + "interval": { + "title": "ana.int.interval", + "description": + "Use IntDomain.Interval32: (int64 * int64) option.", + "type": "boolean", + "default": false + }, + "enums": { + "title": "ana.int.enums", + "description": + "Use IntDomain.Enums: Inclusion/Exclusion sets. Go to top on arithmetic operations (except for some easy cases, e.g. multiplication with 0). Joins on widen, i.e. precise integers as long as not derived from arithmetic expressions.", + "type": "boolean", + "default": false + }, + "congruence": { + "title": "ana.int.congruence", + "description": + "Use IntDomain.Congruence: (c, m) option, meaning congruent to c modulo m", + "type": "boolean", + "default": false + }, + "refinement": { + "title": "ana.int.refinement", + "description": + "Use mutual refinement of integer domains. Either 'never', 'once' or 'fixpoint'", + "type": "string", + "default": "never" + } + }, + "additionalProperties": false + }, + "file": { + "title": "ana.file", + "type": "object", + "properties": { + "optimistic": { + "title": "ana.file.optimistic", + "description": "Assume fopen never fails.", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false + }, + "spec": { + "title": "ana.spec", + "type": "object", + "properties": { + "file": { + "title": "ana.spec.file", + "description": "Path to the specification file.", + "type": "string", + "default": "" + } + }, + "additionalProperties": false + }, + "pml": { + "title": "ana.pml", + "type": "object", + "properties": { + "debug": { + "title": "ana.pml.debug", + "description": + "Insert extra assertions into Promela code for debugging.", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false + }, + "arinc": { + "title": "ana.arinc", + "type": "object", + "properties": { + "assume_success": { + "title": "ana.arinc.assume_success", + "description": + "Assume that all ARINC functions succeed (sets return code to NO_ERROR, otherwise invalidates it).", + "type": "boolean", + "default": true + }, + "simplify": { + "title": "ana.arinc.simplify", + "description": + "Simplify the graph by merging functions consisting of the same edges and contracting call chains where functions just consist of another call.", + "type": "boolean", + "default": true + }, + "validate": { + "title": "ana.arinc.validate", + "description": + "Validate the graph and output warnings for: call to functions without edges, multi-edge-calls for intermediate contexts, branching on unset return variables.", + "type": "boolean", + "default": true + }, + "export": { + "title": "ana.arinc.export", + "description": + "Generate dot graph and Promela for ARINC calls right after analysis. Result is saved in result/arinc.out either way.", + "type": "boolean", + "default": true + }, + "merge_globals": { + "title": "ana.arinc.merge_globals", + "description": + "Merge all global return code variables into one.", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false + }, + "opt": { + "title": "ana.opt", + "type": "object", + "properties": { + "hashcons": { + "title": "ana.opt.hashcons", + "description": + "Should we try to save memory and speed up equality by hashconsing?", + "type": "boolean", + "default": true + }, + "equal": { + "title": "ana.opt.equal", + "description": + "First try physical equality (==) before {D,G,C}.equal (only done if hashcons is disabled since it basically does the same via its tags).", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false + }, + "mutex": { + "title": "ana.mutex", + "type": "object", + "properties": { + "disjoint_types": { + "title": "ana.mutex.disjoint_types", + "description": + "Do not propagate basic type writes to all struct fields", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false + }, + "sv-comp": { + "title": "ana.sv-comp", + "type": "object", + "properties": { + "enabled": { + "title": "ana.sv-comp.enabled", + "description": "SV-COMP mode", + "type": "boolean", + "default": false + }, + "functions": { + "title": "ana.sv-comp.functions", + "description": "Handle SV-COMP __VERIFIER* functions", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false + }, + "specification": { + "title": "ana.specification", + "description": "SV-COMP specification (path or string)", + "type": "string", + "default": "" + }, + "wp": { + "title": "ana.wp", + "description": + "Weakest precondition feasibility analysis for SV-COMP violations", + "type": "boolean", + "default": false + }, + "arrayoob": { + "title": "ana.arrayoob", + "description": "Array out of bounds check", + "type": "boolean", + "default": false + }, + "base": { + "title": "ana.base", + "type": "object", + "properties": { + "context": { + "title": "ana.base.context", + "type": "object", + "properties": { + "non-ptr": { + "title": "ana.base.context.non-ptr", + "description": "Non-address values in function contexts.", + "type": "boolean", + "default": true + }, + "int": { + "title": "ana.base.context.int", + "description": "Integer values in function contexts.", + "type": "boolean", + "default": true + }, + "interval": { + "title": "ana.base.context.interval", + "description": + "Integer values of the Interval domain in function contexts.", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false + } + }, + "additionalProperties": false + }, + "apron": { + "title": "ana.apron", + "type": "object", + "properties": { + "context": { + "title": "ana.apron.context", + "description": "Entire relation in function contexts.", + "type": "boolean", + "default": true + }, + "domain": { + "title": "ana.apron.domain", + "description": + "Which domain should be used for the Apron analysis. Can be 'octagon', 'interval' or 'polyhedra'", + "type": "string", + "default": "octagon" + }, + "threshold_widening": { + "title": "ana.apron.threshold_widening", + "description": + "Use constants appearing in program as threshold for widening", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false + }, + "context": { + "title": "ana.context", + "type": "object", + "properties": { + "widen": { + "title": "ana.context.widen", + "description": + "Do widening on contexts. Keeps a map of function to call state; enter will then return the widened local state for recursive calls.", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false + }, + "thread": { + "title": "ana.thread", + "type": "object", + "properties": { + "domain": { + "title": "ana.thread.domain", + "description": + "Which domain should be used for the thread ids. Can be 'history' or 'plain'", + "type": "string", + "default": "history" + } + }, + "additionalProperties": false + } + }, + "additionalProperties": false + }, + "incremental": { + "title": "Incremental", + "description": "Incremental analysis options", + "type": "object", + "properties": { + "load": { + "title": "incremental.load", + "description": + "Load incremental analysis results, in case any exist.", + "type": "boolean", + "default": false + }, + "only-rename": { + "title": "incremental.only-rename", + "description": + "Only reset IDs of unchanged objects in the AST. Do not reuse solver results. This option is mainly useful for benchmarking purposes.", + "type": "boolean", + "default": false + }, + "save": { + "title": "incremental.save", + "description": "Store incremental analysis results.", + "type": "boolean", + "default": false + }, + "stable": { + "title": "incremental.stable", + "description": + "Reuse the stable set and selectively destabilize it (recommended).", + "type": "boolean", + "default": true + }, + "wpoint": { + "title": "incremental.wpoint", + "description": + "Reuse the wpoint set (not recommended). Reusing the wpoint will combine existing results at previous widening points.", + "type": "boolean", + "default": false + }, + "reluctant": { + "title": "incremental.reluctant", + "type": "object", + "properties": { + "on": { + "title": "incremental.reluctant.on", + "description": + "Destabilize nodes in changed functions reluctantly", + "type": "boolean", + "default": true + }, + "compare": { + "title": "incremental.reluctant.compare", + "description": + "In order to reuse the function's old abstract value the new abstract value must be leq (focus on efficiency) or equal (focus on precision) compared to the old.", + "type": "string", + "default": "leq" + } + }, + "additionalProperties": false + }, + "compare": { + "title": "incremental.compare", + "description": + "Which comparison should be used for functions? 'ast'/'cfg' (cfg comparison also differentiates which nodes of a function have changed)", + "type": "string", + "default": "ast" + }, + "force-reanalyze": { + "title": "incremental.force-reanalyze", + "type": "object", + "properties": { + "funs": { + "title": "incremental.force-reanalyze.funs", + "description": + "List of functions that are to be re-analayzed from scratch", + "type": "array", + "items": { "type": "string" }, + "default": [] + } + }, + "additionalProperties": false + } + }, + "additionalProperties": false + }, + "sem": { + "title": "Semantics", + "description": "Options for semantics", + "type": "object", + "properties": { + "unknown_function": { + "title": "sem.unknown_function", + "type": "object", + "properties": { + "spawn": { + "title": "sem.unknown_function.spawn", + "description": + "Unknown function call spawns reachable functions", + "type": "boolean", + "default": true + }, + "invalidate": { + "title": "sem.unknown_function.invalidate", + "type": "object", + "properties": { + "globals": { + "title": "sem.unknown_function.invalidate.globals", + "description": + "Unknown function call invalidates all globals", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false + } + }, + "additionalProperties": false + }, + "builtin_unreachable": { + "title": "sem.builtin_unreachable", + "type": "object", + "properties": { + "dead_code": { + "title": "sem.builtin_unreachable.dead_code", + "description": + "__builtin_unreachable is assumed to be dead code", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false + }, + "int": { + "title": "sem.int", + "type": "object", + "properties": { + "signed_overflow": { + "title": "sem.int.signed_overflow", + "description": + "How to handle overflows of signed types. Values: 'assume_top' (default): Assume signed overflow results in a top value; 'assume_none': Assume program is free of signed overflows; 'assume_wraparound': Assume signed types wrap-around and two's complement representation of signed integers", + "type": "string", + "default": "assume_top" + } + }, + "additionalProperties": false + } + }, + "additionalProperties": false + }, + "trans": { + "title": "Transformations", + "description": "Options for transformations", + "type": "object", + "properties": { + "activated": { + "title": "trans.activated", + "description": + "Lists of activated transformations in this phase. Transformations happen after analyses.", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "expeval": { + "title": "trans.expeval", + "type": "object", + "properties": { + "query_file_name": { + "title": "trans.expeval.query_file_name", + "description": + "Path to the JSON file containing an expression evaluation query.", + "type": "string", + "default": "" + } + }, + "additionalProperties": false + } + }, + "additionalProperties": false + }, + "annotation": { + "title": "Annotation", + "description": "Options for annotations", + "type": "object", + "properties": { + "int": { + "title": "annotation.int", + "type": "object", + "properties": { + "enabled": { + "title": "annotation.int.enabled", + "description": + "Enable manual annotation of functions with desired precision, i.e. the activated IntDomains.", + "type": "boolean", + "default": false + }, + "privglobs": { + "title": "annotation.int.privglobs", + "description": + "Enables handling of privatized globals, by setting the precision to the heighest value, when annotation.int.enabled is true.", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false + }, + "goblint_context": { + "title": "annotation.goblint_context", + "type": "object", + "properties": { + "base": { + "title": "annotation.goblint_context.base", + "type": "object", + "properties": { + "no-non-ptr": { + "title": "annotation.goblint_context.base.no-non-ptr", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "non-ptr": { + "title": "annotation.goblint_context.base.non-ptr", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "no-int": { + "title": "annotation.goblint_context.base.no-int", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "int": { + "title": "annotation.goblint_context.base.int", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "no-interval": { + "title": "annotation.goblint_context.base.no-interval", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "interval": { + "title": "annotation.goblint_context.base.interval", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + } + }, + "additionalProperties": false + }, + "apron": { + "title": "annotation.goblint_context.apron", + "type": "object", + "properties": { + "no-context": { + "title": "annotation.goblint_context.apron.no-context", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "context": { + "title": "annotation.goblint_context.apron.context", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + } + }, + "additionalProperties": false + }, + "no-widen": { + "title": "annotation.goblint_context.no-widen", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "widen": { + "title": "annotation.goblint_context.widen", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + } + }, + "additionalProperties": false + }, + "goblint_precision": { + "title": "annotation.goblint_precision", + "type": "object", + "properties": { + "no-def_exc": { + "title": "annotation.goblint_precision.no-def_exc", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "def_exc": { + "title": "annotation.goblint_precision.def_exc", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "no-interval": { + "title": "annotation.goblint_precision.no-interval", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "interval": { + "title": "annotation.goblint_precision.interval", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "no-enums": { + "title": "annotation.goblint_precision.no-enums", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "enums": { + "title": "annotation.goblint_precision.enums", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "no-congruence": { + "title": "annotation.goblint_precision.no-congruence", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "congruence": { + "title": "annotation.goblint_precision.congruence", + "description": "", + "type": "array", + "items": { "type": "string" }, + "default": [] + } + }, + "additionalProperties": false + } + }, + "additionalProperties": false + }, + "exp": { + "title": "Experimental", + "description": "Experimental features", + "type": "object", + "properties": { + "lower-constants": { + "title": "exp.lower-constants", + "description": + "Use Cil.lowerConstants to simplify some constant? (assumes wrap-around for signed int)", + "type": "boolean", + "default": true + }, + "privatization": { + "title": "exp.privatization", + "description": + "Which privatization to use? none/protection-old/mutex-oplus/mutex-meet/protection/protection-read/protection-vesal/mine/mine-nothread/mine-W/mine-W-noinit/lock/write/write+lock", + "type": "string", + "default": "protection-read" + }, + "priv-prec-dump": { + "title": "exp.priv-prec-dump", + "description": "File to dump privatization precision data to.", + "type": "string", + "default": "" + }, + "priv-distr-init": { + "title": "exp.priv-distr-init", + "description": + "Distribute global initializations to all global invariants for more consistent widening dynamics.", + "type": "boolean", + "default": false + }, + "apron": { + "title": "exp.apron", + "type": "object", + "properties": { + "privatization": { + "title": "exp.apron.privatization", + "description": + "Which apron privatization to use? dummy/protection/protection-path/mutex-meet/mutex-meet-tid/mutex-meet-tid-cluster12/mutex-meet-tid-cluster2/mutex-meet-tid-cluster-max/mutex-meet-tid-cluster-power", + "type": "string", + "default": "mutex-meet" + }, + "priv": { + "title": "exp.apron.priv", + "type": "object", + "properties": { + "not-started": { + "title": "exp.apron.priv.not-started", + "description": + "Exclude writes from threads that may not be started yet", + "type": "boolean", + "default": true + }, + "must-joined": { + "title": "exp.apron.priv.must-joined", + "description": + "Exclude writes from threads that must have been joined", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false + }, + "prec-dump": { + "title": "exp.apron.prec-dump", + "description": "File to dump apron precision data to.", + "type": "string", + "default": "" + } + }, + "additionalProperties": false + }, + "cfgdot": { + "title": "exp.cfgdot", + "description": "Output CFG to dot files", + "type": "boolean", + "default": false + }, + "mincfg": { + "title": "exp.mincfg", + "description": "Try to minimize the number of CFG nodes.", + "type": "boolean", + "default": false + }, + "earlyglobs": { + "title": "exp.earlyglobs", + "description": + "Side-effecting of globals right after initialization.", + "type": "boolean", + "default": false + }, + "failing-locks": { + "title": "exp.failing-locks", + "description": + "Takes the possible failing of locking operations into account.", + "type": "boolean", + "default": false + }, + "region-offsets": { + "title": "exp.region-offsets", + "description": "Considers offsets for region accesses.", + "type": "boolean", + "default": false + }, + "unique": { + "title": "exp.unique", + "description": "For types that have only one value.", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "forward": { + "title": "exp.forward", + "description": + "Use implicit forward propagation instead of the demand driven approach.", + "type": "boolean", + "default": false + }, + "malloc": { + "title": "exp.malloc", + "type": "object", + "properties": { + "fail": { + "title": "exp.malloc.fail", + "description": + "Consider the case where malloc or calloc fails.", + "type": "boolean", + "default": false + }, + "wrappers": { + "title": "exp.malloc.wrappers", + "description": + "Loads a list of known malloc wrapper functions.", + "type": "array", + "items": { "type": "string" }, + "default": [ + "kmalloc", "__kmalloc", "usb_alloc_urb", "__builtin_alloca", + "kzalloc" + ] + } + }, + "additionalProperties": false + }, + "volatiles_are_top": { + "title": "exp.volatiles_are_top", + "description": + "volatile and extern keywords set variables permanently to top", + "type": "boolean", + "default": true + }, + "single-threaded": { + "title": "exp.single-threaded", + "description": "Ensures analyses that no threads are created.", + "type": "boolean", + "default": false + }, + "globs_are_top": { + "title": "exp.globs_are_top", + "description": "Set globals permanently to top.", + "type": "boolean", + "default": false + }, + "precious_globs": { + "title": "exp.precious_globs", + "description": + "Global variables that should be handled flow-sensitively when using earlyglobs.", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "list-type": { + "title": "exp.list-type", + "description": "Use a special abstract value for lists.", + "type": "boolean", + "default": false + }, + "g2html_path": { + "title": "exp.g2html_path", + "description": "Location of the g2html.jar file.", + "type": "string", + "default": "." + }, + "extraspecials": { + "title": "exp.extraspecials", + "description": + "List of functions that must be analyzed as unknown extern functions", + "type": "array", + "items": { "type": "string" }, + "default": [] + }, + "no-narrow": { + "title": "exp.no-narrow", + "description": "Overwrite narrow a b = a", + "type": "boolean", + "default": false + }, + "basic-blocks": { + "title": "exp.basic-blocks", + "description": + "Only keep values for basic blocks instead of for every node. Should take longer but need less space.", + "type": "boolean", + "default": false + }, + "solver": { + "title": "exp.solver", + "type": "object", + "properties": { + "td3": { + "title": "exp.solver.td3", + "type": "object", + "properties": { + "term": { + "title": "exp.solver.td3.term", + "description": + "Should the td3 solver use the phased/terminating strategy?", + "type": "boolean", + "default": true + }, + "side_widen": { + "title": "exp.solver.td3.side_widen", + "description": + "When to widen in side. never: never widen, always: always widen, sides: widen if there are multiple side-effects from the same var resulting in a new value, cycle: widen if a called or a start var get destabilized, unstable_called: widen if any called var gets destabilized, unstable_self: widen if side-effected var gets destabilized, sides-pp: widen if there are multiple side-effects from the same program point resulting in a new value.", + "type": "string", + "default": "sides" + }, + "space": { + "title": "exp.solver.td3.space", + "description": + "Should the td3 solver only keep values at widening points?", + "type": "boolean", + "default": false + }, + "space_cache": { + "title": "exp.solver.td3.space_cache", + "description": "Should the td3-space solver cache values?", + "type": "boolean", + "default": true + }, + "space_restore": { + "title": "exp.solver.td3.space_restore", + "description": + "Should the td3-space solver restore values for non-widening-points? Not needed for generating warnings, but needed for inspecting output!", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false + }, + "slr4": { + "title": "exp.solver.slr4", + "type": "object", + "properties": { + "restart_count": { + "title": "exp.solver.slr4.restart_count", + "description": + "How many times SLR4 is allowed to switch from restarting iteration to increasing iteration.", + "type": "integer", + "default": 1.0 + } + }, + "additionalProperties": false + } + }, + "additionalProperties": false + }, + "fast_global_inits": { + "title": "exp.fast_global_inits", + "description": + "Only generate one 'a[MyCFG.all_array_index_exp] = x' for all assignments a[...] = x for a global array a[n].", + "type": "boolean", + "default": true + }, + "uninit-ptr-safe": { + "title": "exp.uninit-ptr-safe", + "description": + "Assume that uninitialized stack-allocated pointers may only point to variables not in the program or null.", + "type": "boolean", + "default": false + }, + "ptr-arith-safe": { + "title": "exp.ptr-arith-safe", + "description": + "Assume that pointer arithmetic only yields safe addresses.", + "type": "boolean", + "default": false + }, + "witness": { + "title": "exp.witness", + "type": "object", + "properties": { + "path": { + "title": "exp.witness.path", + "description": "Witness output path", + "type": "string", + "default": "witness.graphml" + }, + "id": { + "title": "exp.witness.id", + "description": "Which witness node IDs to use? node/enumerate", + "type": "string", + "default": "node" + }, + "invariant": { + "title": "exp.witness.invariant", + "type": "object", + "properties": { + "nodes": { + "title": "exp.witness.invariant.nodes", + "description": + "Which witness nodes to add invariants to? all/loop_heads/none", + "type": "string", + "default": "all" + } + }, + "additionalProperties": false + }, + "minimize": { + "title": "exp.witness.minimize", + "description": "Try to minimize the witness", + "type": "boolean", + "default": false + }, + "uncil": { + "title": "exp.witness.uncil", + "description": + "Try to undo CIL control flow transformations in witness", + "type": "boolean", + "default": false + }, + "stack": { + "title": "exp.witness.stack", + "description": "Construct stacktrace-based witness nodes", + "type": "boolean", + "default": true + }, + "unknown": { + "title": "exp.witness.unknown", + "description": "Output witness for unknown result", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false + }, + "architecture": { + "title": "exp.architecture", + "description": "Architecture for analysis, currently for witness", + "type": "string", + "default": "64bit" + }, + "partition-arrays": { + "title": "exp.partition-arrays", + "type": "object", + "properties": { + "enabled": { + "title": "exp.partition-arrays.enabled", + "description": + "Employ the partitioning array domain. When this is on, make sure to enable the expRelation analysis as well.", + "type": "boolean", + "default": false + }, + "keep-expr": { + "title": "exp.partition-arrays.keep-expr", + "description": + "When using the partitioning which expression should be used for partitioning ('first', 'last')", + "type": "string", + "default": "first" + }, + "partition-by-const-on-return": { + "title": "exp.partition-arrays.partition-by-const-on-return", + "description": + "When using the partitioning should arrays be considered partitioned according to a constant if a var in the expression used for partitioning goes out of scope?", + "type": "boolean", + "default": false + }, + "smart-join": { + "title": "exp.partition-arrays.smart-join", + "description": + "When using the partitioning should the join of two arrays partitioned according to different expressions be partitioned as well if possible? If keep-expr is 'last' this behavior is enabled regardless of the flag value. Caution: Not always advantageous.", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false + }, + "structs": { + "title": "exp.structs", + "type": "object", + "properties": { + "domain": { + "title": "exp.structs.domain", + "description": + "The domain that should be used for structs. simple/sets/keyed/combined-all/combined-sk", + "type": "string", + "default": "simple" + }, + "key": { + "title": "exp.structs.key", + "type": "object", + "properties": { + "forward": { + "title": "exp.structs.key.forward", + "description": + "Whether the struct key should be picked going from first field to last.", + "type": "boolean", + "default": true + }, + "avoid-ints": { + "title": "exp.structs.key.avoid-ints", + "description": + "Whether integers should be avoided for key.", + "type": "boolean", + "default": true + }, + "prefer-ptrs": { + "title": "exp.structs.key.prefer-ptrs", + "description": + "Whether pointers should be preferred for key.", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false + } + }, + "additionalProperties": false + }, + "gcc_path": { + "title": "exp.gcc_path", + "description": + "Location of gcc. Used to combine source files with cilly. Change to gcc-9 or another version on OS X (with gcc being clang by default cilly will fail otherwise).", + "type": "string", + "default": "/usr/bin/gcc" + }, + "compdb": { + "title": "exp.compdb", + "type": "object", + "properties": { + "original-path": { + "title": "exp.compdb.original-path", + "description": + "Original absolute path of Compilation Database. Used to reroot all absolute paths in there if moved, e.g. in container mounts.", + "type": "string", + "default": "" + } + }, + "additionalProperties": false + }, + "cpp-path": { + "title": "exp.cpp-path", + "description": + "Path to C preprocessor (cpp) to use. If empty, then automatically searched.", + "type": "string", + "default": "" + } + }, + "additionalProperties": false + }, + "dbg": { + "title": "Debugging", + "description": "Debugging options", + "type": "object", + "properties": { + "debug": { + "title": "dbg.debug", + "description": "Debug mode: for testing the analyzer itself.", + "type": "boolean", + "default": false + }, + "verbose": { + "title": "dbg.verbose", + "description": "Prints some status information.", + "type": "boolean", + "default": false + }, + "trace": { + "title": "dbg.trace", + "type": "object", + "properties": { + "context": { + "title": "dbg.trace.context", + "description": "Also print the context of solver variables.", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false + }, + "showtemps": { + "title": "dbg.showtemps", + "description": + "Shows CIL's temporary variables when printing the state.", + "type": "boolean", + "default": false + }, + "uncalled": { + "title": "dbg.uncalled", + "description": "Display uncalled functions.", + "type": "boolean", + "default": true + }, + "dump": { + "title": "dbg.dump", + "description": "Dumps the results to the given path", + "type": "string", + "default": "" + }, + "cilout": { + "title": "dbg.cilout", + "description": "Where to dump cil output", + "type": "string", + "default": "" + }, + "timeout": { + "title": "dbg.timeout", + "description": + "Stop solver after this time. 0 means no timeout. Supports optional units h, m, s. E.g. 1m6s = 01m06s = 66; 6h = 6*60*60.", + "type": "string", + "default": "0" + }, + "solver-stats-interval": { + "title": "dbg.solver-stats-interval", + "description": + "Interval in seconds to print statistics while solving. Set to 0 to deactivate.", + "type": "integer", + "default": 10.0 + }, + "solver-signal": { + "title": "dbg.solver-signal", + "description": + "Signal to print statistics while solving. Possible values: sigint (Ctrl+C), sigtstp (Ctrl+Z), sigquit (Ctrl+\\), sigusr1, sigusr2, sigalrm, sigprof etc. (see signal_of_string in goblintutil.ml).", + "type": "string", + "default": "sigusr1" + }, + "backtrace-signal": { + "title": "dbg.backtrace-signal", + "description": + "Signal to print a raw backtrace on stderr. Possible values: sigint (Ctrl+C), sigtstp (Ctrl+Z), sigquit (Ctrl+\\), sigusr1, sigusr2, sigalrm, sigprof etc. (see signal_of_string in goblintutil.ml).", + "type": "string", + "default": "sigusr2" + }, + "solver-progress": { + "title": "dbg.solver-progress", + "description": + "Used for debugging. Prints out a symbol on solving a rhs.", + "type": "boolean", + "default": false + }, + "print_wpoints": { + "title": "dbg.print_wpoints", + "description": + "Print the widening points after solving (does not include the removed wpoints during solving by the slr solvers). Currently only implemented in: slr*, td3.", + "type": "boolean", + "default": false + }, + "print_dead_code": { + "title": "dbg.print_dead_code", + "description": "Print information about dead code", + "type": "boolean", + "default": false + }, + "slice": { + "title": "dbg.slice", + "type": "object", + "properties": { + "on": { + "title": "dbg.slice.on", + "description": "Turn slicer on or off.", + "type": "boolean", + "default": false + }, + "n": { + "title": "dbg.slice.n", + "description": "How deep function stack do we analyze.", + "type": "integer", + "default": 10.0 + } + }, + "additionalProperties": false + }, + "limit": { + "title": "dbg.limit", + "type": "object", + "properties": { + "widen": { + "title": "dbg.limit.widen", + "description": + "Limit for number of widenings per node (0 = no limit).", + "type": "integer", + "default": 0.0 + } + }, + "additionalProperties": false + }, + "warn_with_context": { + "title": "dbg.warn_with_context", + "description": + "Keep warnings for different contexts apart (currently only done for asserts).", + "type": "boolean", + "default": false + }, + "regression": { + "title": "dbg.regression", + "description": + "Only output warnings for assertions that have an unexpected result (no comment, comment FAIL, comment UNKNOWN)", + "type": "boolean", + "default": false + }, + "test": { + "title": "dbg.test", + "type": "object", + "properties": { + "domain": { + "title": "dbg.test.domain", + "description": "Test domain properties", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false + }, + "cilcfgdot": { + "title": "dbg.cilcfgdot", + "description": "Output dot files for CIL CFGs.", + "type": "boolean", + "default": false + }, + "cfg": { + "title": "dbg.cfg", + "type": "object", + "properties": { + "loop-clusters": { + "title": "dbg.cfg.loop-clusters", + "description": "Add loop SCC clusters to CFG .dot output.", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false + }, + "compare_runs": { + "title": "dbg.compare_runs", + "type": "object", + "properties": { + "glob": { + "title": "dbg.compare_runs.glob", + "description": "Compare GlobConstrSys in compare_runs", + "type": "boolean", + "default": true + }, + "eq": { + "title": "dbg.compare_runs.eq", + "description": "Compare EqConstrSys in compare_runs", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false + }, + "print_tids": { + "title": "dbg.print_tids", + "description": + "Should the analysis print information on the encountered TIDs", + "type": "boolean", + "default": false + }, + "print_protection": { + "title": "dbg.print_protection", + "description": + "Should the analysis print information on which globals are protected by which mutex?", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false + }, + "warn": { + "title": "Warnings", + "description": "Filtering of warnings", + "type": "object", + "properties": { + "assert": { + "title": "warn.assert", + "description": "Assert messages", + "type": "boolean", + "default": true + }, + "behavior": { + "title": "warn.behavior", + "description": "undefined behavior warnings", + "type": "boolean", + "default": true + }, + "integer": { + "title": "warn.integer", + "description": "integer (Overflow, Div_by_zero) warnings", + "type": "boolean", + "default": true + }, + "cast": { + "title": "warn.cast", + "description": "Cast (Type_mismatch(bug) warnings", + "type": "boolean", + "default": true + }, + "race": { + "title": "warn.race", + "description": "Race warnings", + "type": "boolean", + "default": true + }, + "deadcode": { + "title": "warn.deadcode", + "description": "Dead code warnings", + "type": "boolean", + "default": true + }, + "analyzer": { + "title": "warn.analyzer", + "description": "Analyzer messages", + "type": "boolean", + "default": true + }, + "unsound": { + "title": "warn.unsound", + "description": "Unsoundness messages", + "type": "boolean", + "default": true + }, + "imprecise": { + "title": "warn.imprecise", + "description": "Imprecision messages", + "type": "boolean", + "default": true + }, + "unknown": { + "title": "warn.unknown", + "description": "Unknown (of string) warnings", + "type": "boolean", + "default": true + }, + "error": { + "title": "warn.error", + "description": "Error severity messages", + "type": "boolean", + "default": true + }, + "warning": { + "title": "warn.warning", + "description": "Warning severity messages", + "type": "boolean", + "default": true + }, + "info": { + "title": "warn.info", + "description": "Info severity messages", + "type": "boolean", + "default": true + }, + "debug": { + "title": "warn.debug", + "description": "Debug severity messages", + "type": "boolean", + "default": false + }, + "success": { + "title": "warn.success", + "description": "Success severity messages", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false + } + }, + "additionalProperties": false +} \ No newline at end of file diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index 9ee1a708e4..0926970923 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -30,6 +30,12 @@ let build_config = ref false (* Phase of the analysis (moved from GoblintUtil b/c of circular build...) *) let phase = ref 0 + +module Validator = JsonSchema2.Validator (struct let schema = Options.schema end) +module ValidatorRequireAll = JsonSchema2.Validator (struct let schema = Options.require_all end) +(* module Validator = JsonSchema2.Validator (struct let schema = Json_schema.any end) +module ValidatorRequireAll = JsonSchema2.Validator (struct let schema = Json_schema.any end) *) + (** The type for [gobConfig] module. *) module type S = sig @@ -270,9 +276,10 @@ struct o := set_value v !o orig_pth; validate conf_schema !json_conf; - if not !build_config then (* object incomplete during building *) - JsonSchema2.validate !json_conf; - () + if not !build_config then ( (* object incomplete during building *) + Validator.validate_exn !json_conf; + (* JsonSchema2.validate !json_conf; *) + ) (** Helper function for reading values. Handles error messages. *) let get_path_string f st = @@ -362,9 +369,11 @@ struct (** Merge configurations form a file with current. *) let merge_file fn = let v = Yojson.Safe.from_channel % BatIO.to_input_channel |> File.with_file_in fn in - JsonSchema2.validate v; + (* JsonSchema2.validate v; *) + Validator.validate_exn v; json_conf := GobYojson.merge !json_conf v; - JsonSchema2.validate !json_conf; + (* JsonSchema2.validate !json_conf; *) + ValidatorRequireAll.validate_exn !json_conf; drop_memo (); if tracing then trace "conf" "Merging with '%s', resulting\n%a.\n" fn GobYojson.pretty !json_conf end @@ -375,5 +384,6 @@ let () = build_config := true; List.iter (fun (c, (n, (desc, def))) -> set_auto n def) !Defaults.registrar; build_config := false; + ValidatorRequireAll.validate_exn !json_conf; addenum_sch (Yojson.Safe.from_string Defaults.default_schema) diff --git a/src/util/options.ml b/src/util/options.ml index ff772e8a32..b7d1c31ccb 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -83,12 +83,12 @@ let schema_of_defaults_json defaults json = JsonSchema2.create_schema element -let defaults_schema = +(* let defaults_schema = let defaults = List.map (fun (c, (n, (desc, def))) -> (n, (c, desc, def))) !Defaults.registrar in (* transform for assoc list lookup by name *) schema_of_defaults_json defaults !GobConfig.json_conf let () = - Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.schema.json") (JsonSchema2.schema_to_yojson defaults_schema) + Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.schema.json") (JsonSchema2.schema_to_yojson defaults_schema) *) let schema_of_yojson json = (* workaround for json-data-encoding not handling recursive root reference correctly *) From 80acec926b18179cdc1fae2ecfdc8abbedcf783b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 15 Dec 2021 17:05:43 +0200 Subject: [PATCH 38/55] Remove new global schema --- src/util/jsonSchema2.ml | 7 ------- src/util/options.ml | 2 -- 2 files changed, 9 deletions(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index a312201e8f..19fba81706 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -104,13 +104,6 @@ struct end -let global_schema = ref any - -let validate json = - let module Validator = Validator (struct let schema = !global_schema end) in - Validator.validate_exn json - - let () = Printexc.register_printer (function | Json_encoding.Unexpected _ | Json_encoding.No_case_matched _ diff --git a/src/util/options.ml b/src/util/options.ml index b7d1c31ccb..865628b630 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -119,8 +119,6 @@ let require_all = JsonSchema2.schema_require_all schema let defaults = JsonSchema2.schema_defaults schema let () = - JsonSchema2.global_schema := schema; - Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.require-all.schema.json") (JsonSchema2.schema_to_yojson require_all); Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.defaults.json") defaults From eac376ff20baa063cd0d9963771a65f95cad4b59 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 15 Dec 2021 17:06:26 +0200 Subject: [PATCH 39/55] Disable require-all schema and defaults generation --- src/util/options.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/util/options.ml b/src/util/options.ml index 865628b630..d888e54fd5 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -119,9 +119,9 @@ let require_all = JsonSchema2.schema_require_all schema let defaults = JsonSchema2.schema_defaults schema let () = - Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.require-all.schema.json") (JsonSchema2.schema_to_yojson require_all); - - Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.defaults.json") defaults + (* Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.require-all.schema.json") (JsonSchema2.schema_to_yojson require_all); *) + (* Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.defaults.json") defaults; *) + () let rec pp_options ~levels ppf (element: element) = match element.kind with From 834de351446cb1d2ce7e03834c9affd484d2015d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 15 Dec 2021 17:10:41 +0200 Subject: [PATCH 40/55] Use default options from schema --- options.schema.json | 8 ++++---- src/util/gobConfig.ml | 5 +++-- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/options.schema.json b/options.schema.json index 9ca399f53d..13e94ade2b 100644 --- a/options.schema.json +++ b/options.schema.json @@ -1301,7 +1301,7 @@ "description": "How many times SLR4 is allowed to switch from restarting iteration to increasing iteration.", "type": "integer", - "default": 1.0 + "default": 1 } }, "additionalProperties": false @@ -1569,7 +1569,7 @@ "description": "Interval in seconds to print statistics while solving. Set to 0 to deactivate.", "type": "integer", - "default": 10.0 + "default": 10 }, "solver-signal": { "title": "dbg.solver-signal", @@ -1619,7 +1619,7 @@ "title": "dbg.slice.n", "description": "How deep function stack do we analyze.", "type": "integer", - "default": 10.0 + "default": 10 } }, "additionalProperties": false @@ -1633,7 +1633,7 @@ "description": "Limit for number of widenings per node (0 = no limit).", "type": "integer", - "default": 0.0 + "default": 0 } }, "additionalProperties": false diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index 0926970923..89777a253c 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -381,9 +381,10 @@ end include Impl let () = - build_config := true; + (* build_config := true; List.iter (fun (c, (n, (desc, def))) -> set_auto n def) !Defaults.registrar; - build_config := false; + build_config := false; *) + json_conf := Options.defaults; ValidatorRequireAll.validate_exn !json_conf; addenum_sch (Yojson.Safe.from_string Defaults.default_schema) From e78e144a449e1c9c19514fb8c6d7d8f1e704b348 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 15 Dec 2021 17:18:21 +0200 Subject: [PATCH 41/55] Use ppx_blob to embed JSON schema --- dune-project | 1 + goblint.opam | 1 + goblint.opam.locked | 1 + src/dune | 3 ++- src/util/options.ml | 3 ++- options.schema.json => src/util/options.schema.json | 0 6 files changed, 7 insertions(+), 2 deletions(-) rename options.schema.json => src/util/options.schema.json (100%) diff --git a/dune-project b/dune-project index bfe355bfdd..b5b87a2aa4 100644 --- a/dune-project +++ b/dune-project @@ -32,6 +32,7 @@ (ppx_distr_guards (>= 0.2)) ppx_deriving ppx_deriving_yojson + ppx_blob (ocaml-monadic (>= 0.5)) (ounit2 :with-test) (odoc :with-doc) diff --git a/goblint.opam b/goblint.opam index 073692331d..a47c6f6fac 100644 --- a/goblint.opam +++ b/goblint.opam @@ -28,6 +28,7 @@ depends: [ "ppx_distr_guards" {>= "0.2"} "ppx_deriving" "ppx_deriving_yojson" + "ppx_blob" "ocaml-monadic" {>= "0.5"} "ounit2" {with-test} "odoc" {with-doc} diff --git a/goblint.opam.locked b/goblint.opam.locked index b4920e8899..d080039fa4 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -58,6 +58,7 @@ depends: [ "ocamlfind" {= "1.9.1"} "odoc" {= "1.5.2" & 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"} diff --git a/src/dune b/src/dune index f538189f5f..70c35126ae 100644 --- a/src/dune +++ b/src/dune @@ -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. diff --git a/src/util/options.ml b/src/util/options.ml index d888e54fd5..030577738f 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -112,7 +112,8 @@ let schema_of_yojson json = JsonSchema2.create_schema element let schema = - schema_of_yojson (Yojson.Safe.from_file "options.schema.json") + (* schema_of_yojson (Yojson.Safe.from_file "options.schema.json") *) + schema_of_yojson (Yojson.Safe.from_string [%blob "options.schema.json"]) let require_all = JsonSchema2.schema_require_all schema diff --git a/options.schema.json b/src/util/options.schema.json similarity index 100% rename from options.schema.json rename to src/util/options.schema.json From bcd97627bc1b16085afe7abc35e391e2ac5b3376 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 15 Dec 2021 17:22:30 +0200 Subject: [PATCH 42/55] Document options JSON schema usage in VSCode --- docs/user-guide/configuring.md | 20 ++++++++++++++++++++ mkdocs.yml | 1 + 2 files changed, 21 insertions(+) create mode 100644 docs/user-guide/configuring.md diff --git a/docs/user-guide/configuring.md b/docs/user-guide/configuring.md new file mode 100644 index 0000000000..36055a6c91 --- /dev/null +++ b/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" + } + ] +} +``` diff --git a/mkdocs.yml b/mkdocs.yml index 58ea679fb9..d0d3ece34f 100644 --- a/mkdocs.yml +++ b/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': From 7e0cb954b232b4328c114bf29676c9b792439ed3 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 16 Dec 2021 10:19:47 +0200 Subject: [PATCH 43/55] Add ppx_blob >= 0.6.0 lower bound --- dune-project | 2 +- goblint.opam | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/dune-project b/dune-project index b5b87a2aa4..a38cec87db 100644 --- a/dune-project +++ b/dune-project @@ -32,7 +32,7 @@ (ppx_distr_guards (>= 0.2)) ppx_deriving ppx_deriving_yojson - ppx_blob + (ppx_blob (>= 0.6.0)) (ocaml-monadic (>= 0.5)) (ounit2 :with-test) (odoc :with-doc) diff --git a/goblint.opam b/goblint.opam index a47c6f6fac..5c6c174b67 100644 --- a/goblint.opam +++ b/goblint.opam @@ -28,7 +28,7 @@ depends: [ "ppx_distr_guards" {>= "0.2"} "ppx_deriving" "ppx_deriving_yojson" - "ppx_blob" + "ppx_blob" {>= "0.6.0"} "ocaml-monadic" {>= "0.5"} "ounit2" {with-test} "odoc" {with-doc} From 4ac625f5572b17ef1106768e31373a873370c0a5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 16 Dec 2021 10:54:16 +0200 Subject: [PATCH 44/55] Erasae Json_Schema of_json argument implicitly to improve json-data-encoding version compatibility --- src/util/jsonSchema2.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema2.ml index 19fba81706..8b69a38a97 100644 --- a/src/util/jsonSchema2.ml +++ b/src/util/jsonSchema2.ml @@ -4,8 +4,8 @@ module JS = Json_schema.Make (Json_repr.Yojson) module JE = Json_encoding.Make (Json_repr.Yojson) module JQ = Json_query.Make (Json_repr.Yojson) -let schema_to_yojson = JS.to_json -let schema_of_yojson = JS.of_json ?definitions_path:None +let schema_to_yojson schema = JS.to_json schema +let schema_of_yojson json = JS.of_json json let erase: type t. t Json_encoding.encoding -> unit Json_encoding.encoding = fun encoding -> Json_encoding.conv (fun _ -> failwith "erase construct") (fun _ -> ()) encoding From 74509ffca124545b67f61a170959dc1b5afb80dc Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Dec 2021 11:18:48 +0200 Subject: [PATCH 45/55] Regenerate options JSON schema from master changes --- src/util/options.schema.json | 27 --------------------------- 1 file changed, 27 deletions(-) diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 13e94ade2b..c2c7e9bcdb 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -268,26 +268,6 @@ "items": { "type": "string" }, "default": [ "OSEK2", "stack_loc", "stack_trace_set" ] }, - "cont": { - "title": "ana.cont", - "type": "object", - "properties": { - "localclass": { - "title": "ana.cont.localclass", - "description": "Analyzes classes defined in main Class.", - "type": "boolean", - "default": false - }, - "class": { - "title": "ana.cont.class", - "description": - "Analyzes all the member functions of the class (CXX.json file required).", - "type": "string", - "default": "" - } - }, - "additionalProperties": false - }, "osek": { "title": "ana.osek", "type": "object", @@ -1048,13 +1028,6 @@ "description": "Experimental features", "type": "object", "properties": { - "lower-constants": { - "title": "exp.lower-constants", - "description": - "Use Cil.lowerConstants to simplify some constant? (assumes wrap-around for signed int)", - "type": "boolean", - "default": true - }, "privatization": { "title": "exp.privatization", "description": From 2d562c0d1ebb78ad7a1d0081d26dd40b175d5ce0 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Dec 2021 11:32:48 +0200 Subject: [PATCH 46/55] Remove old JsonSchema module (PR #499) --- src/util/gobConfig.ml | 21 +---- src/util/jsonSchema.ml | 187 ----------------------------------------- 2 files changed, 1 insertion(+), 207 deletions(-) delete mode 100644 src/util/jsonSchema.ml diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index 89777a253c..767454c470 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -21,7 +21,6 @@ open Prelude open Tracing open Printf -open JsonSchema exception ConfigError of string @@ -82,9 +81,6 @@ sig (** Merge configurations form a file with current. *) val merge_file : string -> unit - (** Add a schema to the conf*) - val addenum_sch: Yojson.Safe.t -> unit - val json_conf: Yojson.Safe.t ref end @@ -173,18 +169,6 @@ struct (** Here we store the actual configuration. *) let json_conf : Yojson.Safe.t ref = ref `Null - (** The schema for the conf [json_conf] *) - let conf_schema : jschema = - { sid = Some "root" - ; sdescr = Some "Configuration root for the Goblint." - ; stype = None - ; sdefault = None - ; saddenum = [] - } - - (** Add the schema to [conf_schema]. *) - let addenum_sch jv = addenum conf_schema @@ fromJson jv - (** Helper function to print the conf using [printf "%t"] and alike. *) let print ch : unit = GobYojson.print ch !json_conf @@ -274,7 +258,6 @@ struct new_v in o := set_value v !o orig_pth; - validate conf_schema !json_conf; if not !build_config then ( (* object incomplete during building *) Validator.validate_exn !json_conf; @@ -385,6 +368,4 @@ let () = List.iter (fun (c, (n, (desc, def))) -> set_auto n def) !Defaults.registrar; build_config := false; *) json_conf := Options.defaults; - ValidatorRequireAll.validate_exn !json_conf; - - addenum_sch (Yojson.Safe.from_string Defaults.default_schema) + ValidatorRequireAll.validate_exn !json_conf diff --git a/src/util/jsonSchema.ml b/src/util/jsonSchema.ml deleted file mode 100644 index fac016a139..0000000000 --- a/src/util/jsonSchema.ml +++ /dev/null @@ -1,187 +0,0 @@ -(** A simpler schema than http://json-schema.org *) - -open Prelude - -(** type of a [jvalue] *) -type jtype = - | JBool | JInt | JNum | JNull | JString - | JArray of jarray - | JObj of jobj - -(** a schema for a [jvalue] *) -and jschema = - { sid : string option (** identificator *) - ; sdescr : string option (** description *) - ; stype : jtype option (** a type with possibly extra information *) - ; sdefault : Yojson.Safe.t option (** the default value *) - ; mutable saddenum : jschema list (** additional schemata that were loaded separately *) - } - -(** extra schema information for an array [jvalue] *) -and jarray = - { sitem : jschema (** the schema for all array elements *) - } - -(** extra schema information for an object [jvalue] *) -and jobj = - { sprops : (string * jschema) list (** properties *) - ; spatternprops : (string * jschema) list (** regular expression properties *) - ; sadditionalprops : bool (** are all properties acounted in the schema *) - ; srequired : string list (** list of required properties *) - } - -(** An exception that indicates that some [jschema] is was invalid. *) -exception JsonSchemaMalformed of string - -(** An exception that indicates that some [jvalue] was not valid according to some [jschema]. *) -exception JsonMalformed of string - - -(** Collect all ids from the [jschema]. *) -let collectIds (s:jschema) : string list = - let acc = ref [] in - let rec f_sc s = - let add_id id = - if List.mem id !acc - then raise (JsonSchemaMalformed "collectIds") - else acc := id :: !acc - in - Option.may add_id s.sid; - List.iter f_sc s.saddenum; - Option.may f_ty s.stype - and f_ty = function - | JBool | JInt | JNum | JNull | JString -> () - | JArray a -> f_sc a.sitem - | JObj o -> - List.iter (f_sc % snd) o.sprops; - List.iter (f_sc % snd) o.spatternprops; - in f_sc s; !acc - -(** Call to [validate s v] validates the [jvalue] [v] in the [jschema] [s]. - Invalidness is communicated using the exception [JsonMalformed]. *) -let validate (s:jschema) (v:Yojson.Safe.t) : unit = - let matches x y = Str.string_match (Str.regexp x) y 0 in - let rec assoc_regex k = function - | [] -> raise Not_found - | (k',c)::xs when matches k' k -> c - | _::xs -> assoc_regex k xs - in - let err n r = raise (JsonMalformed ("Json Validate: "^n^" is not "^r)) in - let rec f_sc n v s = - Option.may (f_ty n v) s.stype; - List.iter (f_sc n v) s.saddenum - and f_ty (n:string) (v:Yojson.Safe.t) (t:jtype) = - match (t,v) with - | JBool, `Bool _ -> () - | JBool,_ -> err n "of type boolean." - | JInt, `Int _ - | JInt, `Intlit _ -> () - | JInt, _ -> err n "of type integer." - | JNum, `Int _ - | JNum, `Intlit _ - | JNum, `Float _ -> () - | JNum, _ -> err n "of type number." - | JNull, `Null -> () - | JNull, _ -> err n "of type null." - | JString, `String _ -> () - | JString, _ -> err n "of type string." - | JArray a, `List b -> List.iter (fun x -> f_sc ("element of "^n) x a.sitem) b - | JArray _, _ -> err n "of type array." - | JObj o, `Assoc i -> - List.iter (one_map o) i; - let r = List.filter (not % flip List.mem_assoc i) o.srequired in - if r<>[] then err (List.hd r) "present." - | JObj o, _ -> err n "of type object." - and one_map o (k, v) = - try - f_sc k v (List.assoc k o.sprops) - with Not_found -> - try - f_sc k v (assoc_regex k o.spatternprops) - with Not_found -> - if not o.sadditionalprops then err k "in the mapping." - in - f_sc "root" v s - -(** Convert a [jvalue] to a [jschema] if possible. Raise [JsonSchemaMalformed] otherwise. *) -let rec fromJson (jv: Yojson.Safe.t) : jschema = - let open Yojson.Safe.Util in - let jarrayFromJson jv = - let item = try jv |> member "item" with Yojson.Safe.Util.Type_error _ -> raise (JsonSchemaMalformed "jarrayFromJson") in - { sitem = fromJson item } - in - let jobjFromJson jv = - let addit = - try jv |> member "additionalProps" |> to_bool - with Yojson.Safe.Util.Type_error _ -> raise (JsonSchemaMalformed "jobjFromJson.addit") - in - let req = - try jv |> member "required" |> to_list |> List.map to_string - with Yojson.Safe.Util.Type_error _ -> [] - in - let props = - try jv |> member "properties" |> to_assoc |> List.map (Tuple2.map2 fromJson) - with Yojson.Safe.Util.Type_error _ -> [] - in - let pprops = - try jv |> member "patternProperties" |> to_assoc |> List.map (Tuple2.map2 fromJson) - with Yojson.Safe.Util.Type_error _ -> [] - in - { sprops = props - ; spatternprops = pprops - ; sadditionalprops = addit - ; srequired = req - } - in - let typeFromJson jv = - let typ = try Some (jv |> member "type" |> to_string) with Yojson.Safe.Util.Type_error _ -> None in - Option.bind typ @@ fun typ -> - match typ with - | "string" -> Some JString - | "boolean" -> Some JBool - | "integer" -> Some JInt - | "number" -> Some JNum - | "null" -> Some JNull - | "array" -> Some (JArray (jarrayFromJson jv)) - | "object" -> Some (JObj (jobjFromJson jv)) - | _ -> raise (JsonSchemaMalformed "typeFromJson") - in - let id = try Some (jv |> member "id" |> to_string) with Yojson.Safe.Util.Type_error _ -> None in - let descr = try Some (jv |> member "description" |> to_string) with Yojson.Safe.Util.Type_error _ -> None in - let def = jv |> member "default" |> to_option Fun.id in - let typ = typeFromJson jv in - let r = - { sid = id - ; sdescr = descr - ; stype = typ - ; sdefault = def - ; saddenum = [] - } - in - Option.may (validate r) def; r - -(** Call to [addenum x y] extends [x] with [y] at the id [Option.get y.sid] *) -let addenum (r:jschema) (l:jschema) = - let addingJson s id l = - let rec f_sc s = - if Some id = s.sid then - s.saddenum <- l :: s.saddenum - else begin - List.iter f_sc s.saddenum; - Option.may f_ty s.stype - end - and f_ty = function - | JBool | JInt | JNum | JNull | JString -> () - | JArray a -> f_sc a.sitem - | JObj o -> - List.iter (f_sc % snd) o.sprops; - List.iter (f_sc % snd) o.spatternprops; - in f_sc r - in - match l.sid with - | None -> raise (JsonSchemaMalformed "addenum") - | Some id -> - if not @@ List.mem id @@ collectIds r then - raise (JsonSchemaMalformed "addenum") - else - addingJson r id l From df56976af675644c7f3f85b2f572acf6d72b7308 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Dec 2021 11:34:35 +0200 Subject: [PATCH 47/55] Rename new JsonSchema2 to JsonSchema (PR #499) --- src/util/gobConfig.ml | 14 +++++++------- src/util/{jsonSchema2.ml => jsonSchema.ml} | 0 src/util/options.ml | 16 ++++++++-------- 3 files changed, 15 insertions(+), 15 deletions(-) rename src/util/{jsonSchema2.ml => jsonSchema.ml} (100%) diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index 767454c470..8ddc09d796 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -30,10 +30,10 @@ let build_config = ref false let phase = ref 0 -module Validator = JsonSchema2.Validator (struct let schema = Options.schema end) -module ValidatorRequireAll = JsonSchema2.Validator (struct let schema = Options.require_all end) -(* module Validator = JsonSchema2.Validator (struct let schema = Json_schema.any end) -module ValidatorRequireAll = JsonSchema2.Validator (struct let schema = Json_schema.any end) *) +module Validator = JsonSchema.Validator (struct let schema = Options.schema end) +module ValidatorRequireAll = JsonSchema.Validator (struct let schema = Options.require_all end) +(* module Validator = JsonSchema.Validator (struct let schema = Json_schema.any end) +module ValidatorRequireAll = JsonSchema.Validator (struct let schema = Json_schema.any end) *) (** The type for [gobConfig] module. *) module type S = @@ -261,7 +261,7 @@ struct if not !build_config then ( (* object incomplete during building *) Validator.validate_exn !json_conf; - (* JsonSchema2.validate !json_conf; *) + (* JsonSchema.validate !json_conf; *) ) (** Helper function for reading values. Handles error messages. *) @@ -352,10 +352,10 @@ struct (** Merge configurations form a file with current. *) let merge_file fn = let v = Yojson.Safe.from_channel % BatIO.to_input_channel |> File.with_file_in fn in - (* JsonSchema2.validate v; *) + (* JsonSchema.validate v; *) Validator.validate_exn v; json_conf := GobYojson.merge !json_conf v; - (* JsonSchema2.validate !json_conf; *) + (* JsonSchema.validate !json_conf; *) ValidatorRequireAll.validate_exn !json_conf; drop_memo (); if tracing then trace "conf" "Merging with '%s', resulting\n%a.\n" fn GobYojson.pretty !json_conf diff --git a/src/util/jsonSchema2.ml b/src/util/jsonSchema.ml similarity index 100% rename from src/util/jsonSchema2.ml rename to src/util/jsonSchema.ml diff --git a/src/util/options.ml b/src/util/options.ml index 030577738f..02c7e991d9 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -80,7 +80,7 @@ let rec element_category_of_defaults_json (defaults: defaults) (json: Yojson.Saf let schema_of_defaults_json defaults json = let (element, _) = element_category_of_defaults_json defaults json "" in - JsonSchema2.create_schema element + JsonSchema.create_schema element (* let defaults_schema = @@ -88,13 +88,13 @@ let schema_of_defaults_json defaults json = schema_of_defaults_json defaults !GobConfig.json_conf let () = - Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.schema.json") (JsonSchema2.schema_to_yojson defaults_schema) *) + Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.schema.json") (JsonSchema.schema_to_yojson defaults_schema) *) let schema_of_yojson json = (* workaround for json-data-encoding not handling recursive root reference correctly *) (* remove the reference before parsing, hack it back afterwards *) - let json = JsonSchema2.JQ.replace [`Field "properties"; `Field "phases"; `Field "items"] (`Assoc []) json in - let schema = JsonSchema2.schema_of_yojson json in (* definitions_path doesn't work, "definitions" field still hardcoded *) + let json = JsonSchema.JQ.replace [`Field "properties"; `Field "phases"; `Field "items"] (`Assoc []) json in + let schema = JsonSchema.schema_of_yojson json in (* definitions_path doesn't work, "definitions" field still hardcoded *) let element = Json_schema.root schema in let element = match element with | { kind = Object ({properties; _} as object_specs); _} -> @@ -109,18 +109,18 @@ let schema_of_yojson json = | _ -> assert false in - JsonSchema2.create_schema element + JsonSchema.create_schema element let schema = (* schema_of_yojson (Yojson.Safe.from_file "options.schema.json") *) schema_of_yojson (Yojson.Safe.from_string [%blob "options.schema.json"]) -let require_all = JsonSchema2.schema_require_all schema +let require_all = JsonSchema.schema_require_all schema -let defaults = JsonSchema2.schema_defaults schema +let defaults = JsonSchema.schema_defaults schema let () = - (* Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.require-all.schema.json") (JsonSchema2.schema_to_yojson require_all); *) + (* Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.require-all.schema.json") (JsonSchema.schema_to_yojson require_all); *) (* Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.defaults.json") defaults; *) () From f2c22791411eacd0d23ddc47704c326535b5b111 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Dec 2021 11:35:57 +0200 Subject: [PATCH 48/55] Remove commented out JsonSchema validation --- src/util/gobConfig.ml | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index 8ddc09d796..827b86e1ca 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -32,8 +32,6 @@ let phase = ref 0 module Validator = JsonSchema.Validator (struct let schema = Options.schema end) module ValidatorRequireAll = JsonSchema.Validator (struct let schema = Options.require_all end) -(* module Validator = JsonSchema.Validator (struct let schema = Json_schema.any end) -module ValidatorRequireAll = JsonSchema.Validator (struct let schema = Json_schema.any end) *) (** The type for [gobConfig] module. *) module type S = @@ -259,10 +257,8 @@ struct in o := set_value v !o orig_pth; - if not !build_config then ( (* object incomplete during building *) - Validator.validate_exn !json_conf; - (* JsonSchema.validate !json_conf; *) - ) + if not !build_config then (* object incomplete during building *) + Validator.validate_exn !json_conf (** Helper function for reading values. Handles error messages. *) let get_path_string f st = @@ -352,10 +348,8 @@ struct (** Merge configurations form a file with current. *) let merge_file fn = let v = Yojson.Safe.from_channel % BatIO.to_input_channel |> File.with_file_in fn in - (* JsonSchema.validate v; *) Validator.validate_exn v; json_conf := GobYojson.merge !json_conf v; - (* JsonSchema.validate !json_conf; *) ValidatorRequireAll.validate_exn !json_conf; drop_memo (); if tracing then trace "conf" "Merging with '%s', resulting\n%a.\n" fn GobYojson.pretty !json_conf From 4918ccad975c8a5fb760970bf36ea64ee73992f9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Dec 2021 11:53:40 +0200 Subject: [PATCH 49/55] Reimplement options shorthand using Options --- src/maingoblint.ml | 6 +++--- src/util/options.ml | 22 ++++++++++++++++++++++ 2 files changed, 25 insertions(+), 3 deletions(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 0de89250b7..e8e1d0a57f 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -83,10 +83,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"), "" diff --git a/src/util/options.ml b/src/util/options.ml index 02c7e991d9..019230f14c 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -124,6 +124,28 @@ let () = (* Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.defaults.json") defaults; *) () +let rec element_paths (element: element): string list = + match element.kind with + | String _ + | Boolean + | Integer _ + | Number _ + | Monomorphic_array _ -> + [""] + | Object object_specs -> + List.concat_map (fun (name, field_element, _, _) -> + List.map (fun path -> name ^ "." ^ path) (element_paths field_element) + ) object_specs.properties + | _ -> + Format.printf "%a\n" Json_schema.pp (create element); + failwith "element_paths" + +let schema_paths (schema: schema): string list = + element_paths (root schema) + |> List.map BatString.rchop (* remove trailing '.' *) + +let paths = schema_paths schema + let rec pp_options ~levels ppf (element: element) = match element.kind with | String _ From 042c3232fbe083c5145c18830c0d92c9b6f77f44 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Dec 2021 11:55:32 +0200 Subject: [PATCH 50/55] Remove old Defaults module (PR #499) --- src/maindomaintest.ml | 2 +- src/maingoblint.ml | 7 +- src/util/defaults.ml | 359 ---------------------------------------- src/util/precCompare.ml | 2 +- unittest/mainTest.ml | 2 +- 5 files changed, 5 insertions(+), 367 deletions(-) delete mode 100644 src/util/defaults.ml diff --git a/src/maindomaintest.ml b/src/maindomaintest.ml index e73883cffc..b141293e47 100644 --- a/src/maindomaintest.ml +++ b/src/maindomaintest.ml @@ -1,4 +1,4 @@ -open! Defaults (* Enums / ... need initialized conf *) +(* open! Defaults (* Enums / ... need initialized conf *) *) module type FiniteSetElems = sig diff --git a/src/maingoblint.ml b/src/maingoblint.ml index e8e1d0a57f..dac23c604c 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -2,7 +2,6 @@ open Prelude open GobConfig -open Defaults open Printf open Goblintutil @@ -100,10 +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), "" - ; "--options" , Arg.Unit (fun () -> Options.print_options (); exit 0), "" - ; "--all-options" , Arg.Unit (fun () -> Options.print_all_options (); 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, "" diff --git a/src/util/defaults.ml b/src/util/defaults.ml deleted file mode 100644 index baf470e1c0..0000000000 --- a/src/util/defaults.ml +++ /dev/null @@ -1,359 +0,0 @@ -(** Default values for [GobConfig]-style configuration. *) - -open Prelude -open Printf -open List -open DefaultsCategory - -(* TODO: add consistency checking *) - - -(** A place to store registered variables *) -let registrar = ref [] - -(** A function to register a variable *) -let reg (c:category) (n:string) (def:string) (desc:string) = - registrar := (c,(n,(desc,def))) :: !registrar - -(** find all associations in the list *) -let rec assoc_all k = function - | [] -> [] - | (x1,x2)::xs when k=x1 -> x2 :: assoc_all k xs - | _::xs -> assoc_all k xs - -(** Prints out all registered options with descriptions and defaults for one category. *) -let printCategory ch k = - let print_one (n,(desc,def)) = - fprintf ch "%-4s%-30s%s\n%-34sDefault value: \"%s\"\n\n" "" n desc "" def - in - catDescription k |> fprintf ch "%s:\n"; - assoc_all k !registrar |> rev |> iter print_one - -(** Prints out all registered options. *) -let printAllCategories ch = - iter (printCategory ch) all_categories - -(* {4 category [Std]} *) -let _ = () - ; reg Std "outfile" "" "File to print output to." - ; reg Std "includes" "[]" "List of directories to include." - ; reg Std "kernel_includes" "[]" "List of kernel directories to include." - ; reg Std "custom_includes" "[]" "List of custom directories to include." - ; reg Std "kernel-root" "''" "Root directory for Linux kernel (linux-headers)" - ; reg Std "justcil" "false" "Just parse and output the CIL." - ; reg Std "justcfg" "false" "Only output the CFG in cfg.dot ." - ; reg Std "printstats" "false" "Outputs timing information." - ; reg Std "verify" "true" "Verify that the solver reached a post-fixpoint. Beware that disabling this also disables output of warnings since post-processing of the results is done in the verification phase!" - ; reg Std "mainfun" "['main']" "Sets the name of the main functions." - ; reg Std "exitfun" "[]" "Sets the name of the cleanup functions." - ; reg Std "otherfun" "[]" "Sets the name of other functions." - ; reg Std "allglobs" "false" "Prints access information about all globals, not just races." - ; reg Std "keepcpp" "false" "Keep the intermediate output of running the C preprocessor." - ; reg Std "tempDir" "''" "Reuse temporary directory for preprocessed files." - ; reg Std "cppflags" "[]" "Pre-processing parameters." - ; reg Std "kernel" "false" "For analyzing Linux Device Drivers." - ; reg Std "dump_globs" "false" "Print out the global invariant." - ; reg Std "result" "'none'" "Result style: none, fast_xml, json, pretty, json-messages." - ; reg Std "solver" "'td3'" "Picks the solver." - ; reg Std "comparesolver" "''" "Picks another solver for comparison." - ; reg Std "solverdiffs" "false" "Print out solver differences." - ; reg Std "allfuns" "false" "Analyzes all the functions (not just beginning from main). This requires exp.earlyglobs!" - ; reg Std "nonstatic" "false" "Analyzes all non-static functions." - ; reg Std "colors" "'auto'" "Colored output (via ANSI escape codes). 'auto': enabled if stdout is a terminal (instead of a pipe); 'always', 'never'." - ; reg Std "g2html" "false" "Run g2html.jar on the generated xml." - ; reg Std "interact.out" "'result'" "The result directory in interactive mode." - ; reg Std "interact.enabled" "false" "Is interactive mode enabled." - ; reg Std "interact.paused" "false" "Start interactive in pause mode." - ; reg Std "phases" "[]" "List of phases. Per-phase settings overwrite global ones." - ; reg Std "save_run" "''" "Save the result of the solver, the current configuration and meta-data about the run to this directory (if set). The data can then be loaded (without solving again) to do post-processing like generating output in a different format or comparing results." - ; reg Std "load_run" "''" "Load a saved run. See save_run." - ; reg Std "compare_runs" "[]" "Load these saved runs and compare the results. Note that currently only two runs can be compared!" - ; reg Std "warn_at" "'post'" "When to output warnings. Values: 'post' (default): after solving; 'never': no warnings; 'early': for debugging - outputs warnings already while solving (may lead to spurious warnings/asserts that would disappear after narrowing)." - ; reg Std "gobview" "false" "Include additional information for Gobview (e.g., the Goblint warning messages) in the directory specified by 'save_run'." - -(* {4 category [Analyses]} *) -let _ = () - ; reg Analyses "ana.activated" "['expRelation','base','threadid','threadflag','threadreturn','escape','mutex','mallocWrapper']" "Lists of activated analyses in this phase." - ; reg Analyses "ana.path_sens" "['OSEK','OSEK2','mutex','malloc_null','uninit']" "List of path-sensitive analyses" - (* apron adds itself to ana.path_sens such that there can be one defaults.ml both for the Apron and No-Apron configuration *) - ; reg Analyses "ana.ctx_insens" "['OSEK2','stack_loc','stack_trace_set']" "List of context-insensitive analyses" - ; reg Analyses "ana.osek.oil" "''" "Oil file for the analyzed program" - ; reg Analyses "ana.osek.defaults" "true" "Generate default definitions for TASK and ISR" - (* ; reg Analyses "ana.osek.tramp" "''" "Resource-ID-headers for the analyzed program" *) - ; reg Analyses "ana.osek.isrprefix" "'function_of_'" "Prefix added by the ISR macro" - ; reg Analyses "ana.osek.taskprefix" "'function_of_'" "Prefix added by the TASK macro" - ; reg Analyses "ana.osek.isrsuffix" "''" "Suffix added by the ISR macro" - ; reg Analyses "ana.osek.tasksuffix" "''" "Suffix added by the TASK macro" - ; reg Analyses "ana.osek.intrpts" "false" "Enable constraints for interrupts." - ; reg Analyses "ana.osek.check" "false" "Check if (assumed) OSEK conventions are fullfilled." - ; reg Analyses "ana.osek.names" "[]" "OSEK API function (re)names for the analysed program" - ; reg Analyses "ana.osek.warnfiles" "false" "Print all warning types to separate file" - ; reg Analyses "ana.osek.safe_vars" "[]" "Suppress warnings on these vars" - ; reg Analyses "ana.osek.safe_task" "[]" "Ignore accesses in these tasks" - ; reg Analyses "ana.osek.safe_isr" "[]" "Ignore accesses in these isr" - ; reg Analyses "ana.osek.flags" "[]" "List of global variables that are flags." - ; reg Analyses "ana.osek.def_header" "true" "Generate TASK/ISR macros with default structure" - ; reg Analyses "ana.int.def_exc" "true" "Use IntDomain.DefExc: definite value/exclusion set." - ; reg Analyses "ana.int.interval" "false" "Use IntDomain.Interval32: (int64 * int64) option." - ; reg Analyses "ana.int.enums" "false" "Use IntDomain.Enums: Inclusion/Exclusion sets. Go to top on arithmetic operations (except for some easy cases, e.g. multiplication with 0). Joins on widen, i.e. precise integers as long as not derived from arithmetic expressions." - ; reg Analyses "ana.int.congruence" "false" "Use IntDomain.Congruence: (c, m) option, meaning congruent to c modulo m" - ; reg Analyses "ana.int.refinement" "'never'" "Use mutual refinement of integer domains. Either 'never', 'once' or 'fixpoint'" - ; reg Analyses "ana.file.optimistic" "false" "Assume fopen never fails." - ; reg Analyses "ana.spec.file" "" "Path to the specification file." - ; reg Analyses "ana.pml.debug" "true" "Insert extra assertions into Promela code for debugging." - ; reg Analyses "ana.arinc.assume_success" "true" "Assume that all ARINC functions succeed (sets return code to NO_ERROR, otherwise invalidates it)." - ; reg Analyses "ana.arinc.simplify" "true" "Simplify the graph by merging functions consisting of the same edges and contracting call chains where functions just consist of another call." - ; reg Analyses "ana.arinc.validate" "true" "Validate the graph and output warnings for: call to functions without edges, multi-edge-calls for intermediate contexts, branching on unset return variables." - ; reg Analyses "ana.arinc.export" "true" "Generate dot graph and Promela for ARINC calls right after analysis. Result is saved in result/arinc.out either way." - ; reg Analyses "ana.arinc.merge_globals" "false" "Merge all global return code variables into one." - ; reg Analyses "ana.opt.hashcons" "true" "Should we try to save memory and speed up equality by hashconsing?" - ; reg Analyses "ana.opt.equal" "true" "First try physical equality (==) before {D,G,C}.equal (only done if hashcons is disabled since it basically does the same via its tags)." - ; reg Analyses "ana.mutex.disjoint_types" "true" "Do not propagate basic type writes to all struct fields" - ; reg Analyses "ana.sv-comp.enabled" "false" "SV-COMP mode" - ; reg Analyses "ana.sv-comp.functions" "false" "Handle SV-COMP __VERIFIER* functions" - ; reg Analyses "ana.specification" "" "SV-COMP specification (path or string)" - ; reg Analyses "ana.wp" "false" "Weakest precondition feasibility analysis for SV-COMP violations" - ; reg Analyses "ana.arrayoob" "false" "Array out of bounds check" - ; reg Analyses "ana.base.context.non-ptr" "true" "Non-address values in function contexts." - ; reg Analyses "ana.base.context.int" "true" "Integer values in function contexts." - ; reg Analyses "ana.base.context.interval" "true" "Integer values of the Interval domain in function contexts." - ; reg Analyses "ana.apron.context" "true" "Entire relation in function contexts." - ; reg Analyses "ana.apron.domain" "'octagon'" "Which domain should be used for the Apron analysis. Can be 'octagon', 'interval' or 'polyhedra'" - ; reg Analyses "ana.context.widen" "false" "Do widening on contexts. Keeps a map of function to call state; enter will then return the widened local state for recursive calls." - ; reg Analyses "ana.apron.threshold_widening" "false" "Use constants appearing in program as threshold for widening" - ; reg Analyses "ana.thread.domain" "'history'" "Which domain should be used for the thread ids. Can be 'history' or 'plain'" - - -(* {4 category [Incremental]} *) -let _ = () - ; reg Incremental "incremental.load" "false" "Load incremental analysis results, in case any exist." - ; reg Incremental "incremental.only-rename" "false" "Only reset IDs of unchanged objects in the AST. Do not reuse solver results. This option is mainly useful for benchmarking purposes." - ; reg Incremental "incremental.save" "false" "Store incremental analysis results." - ; reg Incremental "incremental.stable" "true" "Reuse the stable set and selectively destabilize it (recommended)." - ; reg Incremental "incremental.wpoint" "false" "Reuse the wpoint set (not recommended). Reusing the wpoint will combine existing results at previous widening points." - ; reg Incremental "incremental.reluctant.on" "true" "Destabilize nodes in changed functions reluctantly" - ; reg Incremental "incremental.reluctant.compare" "'leq'" "In order to reuse the function's old abstract value the new abstract value must be leq (focus on efficiency) or equal (focus on precision) compared to the old." - ; reg Incremental "incremental.compare" "'ast'" "Which comparison should be used for functions? 'ast'/'cfg' (cfg comparison also differentiates which nodes of a function have changed)" - ; reg Incremental "incremental.force-reanalyze.funs" "[]" "List of functions that are to be re-analayzed from scratch" - -(* {4 category [Semantics]} *) -let _ = () - (* TODO: split unknown_function to undefined_function and unknown_function_ptr *) - ; reg Semantics "sem.unknown_function.spawn" "true" "Unknown function call spawns reachable functions" - ; reg Semantics "sem.unknown_function.invalidate.globals" "true" "Unknown function call invalidates all globals" - ; reg Semantics "sem.builtin_unreachable.dead_code" "false" "__builtin_unreachable is assumed to be dead code" - ; reg Semantics "sem.int.signed_overflow" "'assume_top'" "How to handle overflows of signed types. Values: 'assume_top' (default): Assume signed overflow results in a top value; 'assume_none': Assume program is free of signed overflows; 'assume_wraparound': Assume signed types wrap-around and two's complement representation of signed integers" - - -(* {4 category [Transformations]} *) -let _ = () - ; reg Transformations "trans.activated" "[]" "Lists of activated transformations in this phase. Transformations happen after analyses." - ; reg Transformations "trans.expeval.query_file_name" "''" "Path to the JSON file containing an expression evaluation query." - -(* {4 category [Annotation]} *) -let _ = () - ; reg Annotation "annotation.int.enabled" "false" "Enable manual annotation of functions with desired precision, i.e. the activated IntDomains." - ; reg Annotation "annotation.int.privglobs" "true" "Enables handling of privatized globals, by setting the precision to the heighest value, when annotation.int.enabled is true." - ; reg Annotation "annotation.goblint_context.base.no-non-ptr" "[]" "" - ; reg Annotation "annotation.goblint_context.base.non-ptr" "[]" "" - ; reg Annotation "annotation.goblint_context.base.no-int" "[]" "" - ; reg Annotation "annotation.goblint_context.base.int" "[]" "" - ; reg Annotation "annotation.goblint_context.base.no-interval" "[]" "" - ; reg Annotation "annotation.goblint_context.base.interval" "[]" "" - ; reg Annotation "annotation.goblint_context.apron.no-context" "[]" "" - ; reg Annotation "annotation.goblint_context.apron.context" "[]" "" - ; reg Annotation "annotation.goblint_context.no-widen" "[]" "" - ; reg Annotation "annotation.goblint_context.widen" "[]" "" - ; reg Annotation "annotation.goblint_precision.no-def_exc" "[]" "" - ; reg Annotation "annotation.goblint_precision.def_exc" "[]" "" - ; reg Annotation "annotation.goblint_precision.no-interval" "[]" "" - ; reg Annotation "annotation.goblint_precision.interval" "[]" "" - ; reg Annotation "annotation.goblint_precision.no-enums" "[]" "" - ; reg Annotation "annotation.goblint_precision.enums" "[]" "" - ; reg Annotation "annotation.goblint_precision.no-congruence" "[]" "" - ; reg Annotation "annotation.goblint_precision.congruence" "[]" "" - -(* {4 category [Experimental]} *) -let _ = () - (* TODO: priv subobject *) - ; reg Experimental "exp.privatization" "'protection-read'" "Which privatization to use? none/protection-old/mutex-oplus/mutex-meet/protection/protection-read/protection-vesal/mine/mine-nothread/mine-W/mine-W-noinit/lock/write/write+lock" - ; reg Experimental "exp.priv-prec-dump" "''" "File to dump privatization precision data to." - ; reg Experimental "exp.priv-distr-init" "false" "Distribute global initializations to all global invariants for more consistent widening dynamics." - ; reg Experimental "exp.apron.privatization" "'mutex-meet'" "Which apron privatization to use? dummy/protection/protection-path/mutex-meet/mutex-meet-tid/mutex-meet-tid-cluster12/mutex-meet-tid-cluster2/mutex-meet-tid-cluster-max/mutex-meet-tid-cluster-power" - ; reg Experimental "exp.apron.priv.not-started" "true" "Exclude writes from threads that may not be started yet" - ; reg Experimental "exp.apron.priv.must-joined" "true" "Exclude writes from threads that must have been joined" - ; reg Experimental "exp.apron.prec-dump" "''" "File to dump apron precision data to." - ; reg Experimental "exp.cfgdot" "false" "Output CFG to dot files" - ; reg Experimental "exp.mincfg" "false" "Try to minimize the number of CFG nodes." - ; reg Experimental "exp.earlyglobs" "false" "Side-effecting of globals right after initialization." - ; reg Experimental "exp.failing-locks" "false" "Takes the possible failing of locking operations into account." - ; reg Experimental "exp.region-offsets" "false" "Considers offsets for region accesses." - ; reg Experimental "exp.unique" "[]" "For types that have only one value." - ; reg Experimental "exp.forward" "false" "Use implicit forward propagation instead of the demand driven approach." - ; reg Experimental "exp.malloc.fail" "false" "Consider the case where malloc or calloc fails." - ; reg Experimental "exp.malloc.wrappers" "['kmalloc','__kmalloc','usb_alloc_urb','__builtin_alloca','kzalloc']" "Loads a list of known malloc wrapper functions." (* When something new that maps to malloc or calloc is added to libraryFunctions.ml, it should also be added here.*) - ; reg Experimental "exp.volatiles_are_top" "true" "volatile and extern keywords set variables permanently to top" - ; reg Experimental "exp.single-threaded" "false" "Ensures analyses that no threads are created." - ; reg Experimental "exp.globs_are_top" "false" "Set globals permanently to top." - ; reg Experimental "exp.precious_globs" "[]" "Global variables that should be handled flow-sensitively when using earlyglobs." - ; reg Experimental "exp.list-type" "false" "Use a special abstract value for lists." - ; reg Experimental "exp.g2html_path" "'.'" "Location of the g2html.jar file." - ; reg Experimental "exp.extraspecials" "[]" "List of functions that must be analyzed as unknown extern functions" - ; reg Experimental "exp.no-narrow" "false" "Overwrite narrow a b = a" - ; reg Experimental "exp.basic-blocks" "false" "Only keep values for basic blocks instead of for every node. Should take longer but need less space." - ; reg Experimental "exp.solver.td3.term" "true" "Should the td3 solver use the phased/terminating strategy?" - ; reg Experimental "exp.solver.td3.side_widen" "'sides'" "When to widen in side. never: never widen, always: always widen, sides: widen if there are multiple side-effects from the same var resulting in a new value, cycle: widen if a called or a start var get destabilized, unstable_called: widen if any called var gets destabilized, unstable_self: widen if side-effected var gets destabilized, sides-pp: widen if there are multiple side-effects from the same program point resulting in a new value." - ; reg Experimental "exp.solver.td3.space" "false" "Should the td3 solver only keep values at widening points?" - ; reg Experimental "exp.solver.td3.space_cache" "true" "Should the td3-space solver cache values?" - ; reg Experimental "exp.solver.td3.space_restore" "true" "Should the td3-space solver restore values for non-widening-points? Not needed for generating warnings, but needed for inspecting output!" - ; reg Experimental "exp.solver.slr4.restart_count" "1" "How many times SLR4 is allowed to switch from restarting iteration to increasing iteration." - ; reg Experimental "exp.fast_global_inits" "true" "Only generate one 'a[MyCFG.all_array_index_exp] = x' for all assignments a[...] = x for a global array a[n]." - ; reg Experimental "exp.uninit-ptr-safe" "false" "Assume that uninitialized stack-allocated pointers may only point to variables not in the program or null." - ; reg Experimental "exp.ptr-arith-safe" "false" "Assume that pointer arithmetic only yields safe addresses." - ; reg Experimental "exp.witness.path" "'witness.graphml'" "Witness output path" - ; reg Experimental "exp.witness.id" "'node'" "Which witness node IDs to use? node/enumerate" - ; reg Experimental "exp.witness.invariant.nodes" "'all'" "Which witness nodes to add invariants to? all/loop_heads/none" - ; reg Experimental "exp.witness.minimize" "false" "Try to minimize the witness" - ; reg Experimental "exp.witness.uncil" "false" "Try to undo CIL control flow transformations in witness" - ; reg Experimental "exp.witness.stack" "true" "Construct stacktrace-based witness nodes" - ; reg Experimental "exp.witness.unknown" "true" "Output witness for unknown result" - ; reg Experimental "exp.architecture" "'64bit'" "Architecture for analysis, currently for witness" - ; reg Experimental "exp.partition-arrays.enabled" "false" "Employ the partitioning array domain. When this is on, make sure to enable the expRelation analysis as well." - ; reg Experimental "exp.partition-arrays.keep-expr" "'first'" "When using the partitioning which expression should be used for partitioning ('first', 'last')" - ; reg Experimental "exp.partition-arrays.partition-by-const-on-return" "false" "When using the partitioning should arrays be considered partitioned according to a constant if a var in the expression used for partitioning goes out of scope?" - ; reg Experimental "exp.partition-arrays.smart-join" "false" "When using the partitioning should the join of two arrays partitioned according to different expressions be partitioned as well if possible? If keep-expr is 'last' this behavior is enabled regardless of the flag value. Caution: Not always advantageous." - ; reg Experimental "exp.structs.domain" "'simple'" "The domain that should be used for structs. simple/sets/keyed/combined-all/combined-sk" - ; reg Experimental "exp.structs.key.forward" "true" "Whether the struct key should be picked going from first field to last." - ; reg Experimental "exp.structs.key.avoid-ints" "true" "Whether integers should be avoided for key." - ; reg Experimental "exp.structs.key.prefer-ptrs" "true" "Whether pointers should be preferred for key." - ; reg Experimental "exp.gcc_path" "'/usr/bin/gcc'" "Location of gcc. Used to combine source files with cilly. Change to gcc-9 or another version on OS X (with gcc being clang by default cilly will fail otherwise)." - ; reg Experimental "exp.compdb.original-path" "" "Original absolute path of Compilation Database. Used to reroot all absolute paths in there if moved, e.g. in container mounts." - ; reg Experimental "exp.cpp-path" "" "Path to C preprocessor (cpp) to use. If empty, then automatically searched." - -(* {4 category [Debugging]} *) -let _ = () - ; reg Debugging "dbg.debug" "false" "Debug mode: for testing the analyzer itself." - ; reg Debugging "dbg.verbose" "false" "Prints some status information." - ; reg Debugging "dbg.trace.context" "false" "Also print the context of solver variables." - ; reg Debugging "dbg.showtemps" "false" "Shows CIL's temporary variables when printing the state." - ; reg Debugging "dbg.uncalled" "true" "Display uncalled functions." - ; reg Debugging "dbg.dump" "" "Dumps the results to the given path" - ; reg Debugging "dbg.cilout" "" "Where to dump cil output" - ; reg Debugging "dbg.timeout" "'0'" "Stop solver after this time. 0 means no timeout. Supports optional units h, m, s. E.g. 1m6s = 01m06s = 66; 6h = 6*60*60." - ; reg Debugging "dbg.solver-stats-interval" "10" "Interval in seconds to print statistics while solving. Set to 0 to deactivate." - ; reg Debugging "dbg.solver-signal" "'sigusr1'" "Signal to print statistics while solving. Possible values: sigint (Ctrl+C), sigtstp (Ctrl+Z), sigquit (Ctrl+\\), sigusr1, sigusr2, sigalrm, sigprof etc. (see signal_of_string in goblintutil.ml)." - ; reg Debugging "dbg.backtrace-signal" "'sigusr2'" "Signal to print a raw backtrace on stderr. Possible values: sigint (Ctrl+C), sigtstp (Ctrl+Z), sigquit (Ctrl+\\), sigusr1, sigusr2, sigalrm, sigprof etc. (see signal_of_string in goblintutil.ml)." - ; reg Debugging "dbg.solver-progress" "false" "Used for debugging. Prints out a symbol on solving a rhs." - ; reg Debugging "dbg.print_wpoints" "false" "Print the widening points after solving (does not include the removed wpoints during solving by the slr solvers). Currently only implemented in: slr*, td3." - ; reg Debugging "dbg.print_dead_code" "false" "Print information about dead code" - ; reg Debugging "dbg.slice.on" "false" "Turn slicer on or off." - ; reg Debugging "dbg.slice.n" "10" "How deep function stack do we analyze." - ; reg Debugging "dbg.limit.widen" "0" "Limit for number of widenings per node (0 = no limit)." - ; reg Debugging "dbg.warn_with_context" "false" "Keep warnings for different contexts apart (currently only done for asserts)." - ; reg Debugging "dbg.regression" "false" "Only output warnings for assertions that have an unexpected result (no comment, comment FAIL, comment UNKNOWN)" - ; reg Debugging "dbg.test.domain" "false" "Test domain properties" - ; reg Debugging "dbg.cilcfgdot" "false" "Output dot files for CIL CFGs." - ; reg Debugging "dbg.cfg.loop-clusters" "false" "Add loop SCC clusters to CFG .dot output." - ; reg Debugging "dbg.compare_runs.glob" "true" "Compare GlobConstrSys in compare_runs" - ; reg Debugging "dbg.compare_runs.eq" "true" "Compare EqConstrSys in compare_runs" - ; reg Debugging "dbg.print_tids" "false" "Should the analysis print information on the encountered TIDs" - ; reg Debugging "dbg.print_protection" "false" "Should the analysis print information on which globals are protected by which mutex?" - -(* {4 category [Warnings]} *) -let _ = () - ; reg Warnings "warn.assert" "true" "Assert messages" - ; reg Warnings "warn.behavior" "true" "undefined behavior warnings" - ; reg Warnings "warn.integer" "true" "integer (Overflow, Div_by_zero) warnings" - ; reg Warnings "warn.cast" "true" "Cast (Type_mismatch(bug) warnings" - ; reg Warnings "warn.race" "true" "Race warnings" - ; reg Warnings "warn.deadcode" "true" "Dead code warnings" - ; reg Warnings "warn.analyzer" "true" "Analyzer messages" - ; reg Warnings "warn.unsound" "true" "Unsoundness messages" - ; reg Warnings "warn.imprecise" "true" "Imprecision messages" - ; reg Warnings "warn.unknown" "true" "Unknown (of string) warnings" - ; reg Warnings "warn.error" "true" "Error severity messages" - ; reg Warnings "warn.warning" "true" "Warning severity messages" - ; reg Warnings "warn.info" "true" "Info severity messages" - ; reg Warnings "warn.debug" "false" "Debug severity messages" - ; reg Warnings "warn.success" "true" "Success severity messages" - - -let () = - registrar := List.rev !registrar - -let default_schema = {schema| -{ "id" : "root" -, "type" : "object" -, "required" : ["outfile", "includes", "kernel_includes", "custom_includes", "kernel-root", "justcil", "justcfg", "printstats", "verify", "mainfun", "exitfun", "otherfun", "allglobs", "keepcpp", "tempDir", "cppflags", "kernel", "dump_globs", "result", "solver", "allfuns", "nonstatic", "colors", "g2html"] -, "additionalProps" : false -, "properties" : - { "ana" : - { "type" : "object" - , "additionalProps" : true - , "required" : [] - } - , "sem" : {} - , "incremental" : {} - , "trans" : {} - , "phases" : {} - , "annotation" : - { "type" : "object" - , "additionalProps" : true - , "required" : [] - } - , "exp" : - { "type" : "object" - , "additionalProps" : true - , "required" : [] - } - , "dbg" : - { "type" : "object" - , "additionalProps" : true - , "required" : [] - } - , "questions" : - { "file" : "" - } - , "outfile" : {} - , "includes" : {} - , "kernel_includes" : {} - , "custom_includes" : {} - , "kernel-root" : {} - , "justcil" : {} - , "justcfg" : {} - , "printstats" : {} - , "verify" : {} - , "mainfun" : {} - , "exitfun" : {} - , "otherfun" : {} - , "allglobs" : {} - , "keepcpp" : {} - , "tempDir" : - { "type" : "string" - } - , "cppflags" : {} - , "kernel" : {} - , "dump_globs" : {} - , "result" : - { "type" : "string" - } - , "solver" : {} - , "comparesolver" : {} - , "solverdiffs" : {} - , "allfuns" : {} - , "nonstatic" : {} - , "colors" : {} - , "g2html" : {} - , "interact" : {} - , "save_run" : {} - , "load_run" : {} - , "compare_runs" : {} - , "warn_at" : {} - , "warn" : - { "type" : "object" - , "additionalProps" : true - , "required" : [] - } - , "gobview" : {} - } -}|schema} diff --git a/src/util/precCompare.ml b/src/util/precCompare.ml index 8108f0eac8..673f4964ba 100644 --- a/src/util/precCompare.ml +++ b/src/util/precCompare.ml @@ -89,7 +89,7 @@ end module MakeDump (Util: PrecCompareUtil.S) = struct - open! Defaults (* CircInterval / Enums / ... need initialized conf *) + (* open! Defaults (* CircInterval / Enums / ... need initialized conf *) *) open! Batteries open Util diff --git a/unittest/mainTest.ml b/unittest/mainTest.ml index 9d04f830d3..fd8528f66b 100644 --- a/unittest/mainTest.ml +++ b/unittest/mainTest.ml @@ -11,7 +11,7 @@ let all_tests _ = ("" >::: let _ = (* first we need to load the default config which is done at the toplevel in Defaults *) - let module Ignore = Defaults in + (* let module Ignore = Defaults in *) let verbose = ref false in let set_verbose _ = verbose := true in Arg.parse From b843a0eb09f9d981257299c2892651c5b90d2a74 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Dec 2021 11:57:37 +0200 Subject: [PATCH 51/55] Remove Defaults to schema conversion (PR #499) --- src/util/defaultsCategory.ml | 28 ------------ src/util/options.ml | 88 ------------------------------------ 2 files changed, 116 deletions(-) delete mode 100644 src/util/defaultsCategory.ml diff --git a/src/util/defaultsCategory.ml b/src/util/defaultsCategory.ml deleted file mode 100644 index 41d6b389d3..0000000000 --- a/src/util/defaultsCategory.ml +++ /dev/null @@ -1,28 +0,0 @@ -open Prelude -open List - -(** Main categories of configuration variables. *) -type category = Std (** Parsing input, includes, standard stuff, etc. *) - | Analyses (** Analyses *) - | Incremental (** Incremental features *) - | Semantics (** Semantics *) - | Transformations (** Transformations *) - | Annotation (** Features for annotations *) - | Experimental (** Experimental features of analyses *) - | Debugging (** Debugging, tracing, etc. *) - | Warnings (** Filtering warnings *) - [@@deriving enum, show { with_path = false }] - -let all_categories = min_category -- max_category |> of_enum |> map (Option.get % category_of_enum) - -(** Description strings for categories. *) -let catDescription = function - | Std -> "Standard options for configuring input/output" - | Analyses -> "Options for analyses" - | Semantics -> "Options for semantics" - | Transformations -> "Options for transformations" - | Annotation -> "Options for annotations" - | Experimental -> "Experimental features" - | Debugging -> "Debugging options" - | Incremental -> "Incremental analysis options" - | Warnings -> "Filtering of warnings" \ No newline at end of file diff --git a/src/util/options.ml b/src/util/options.ml index 019230f14c..261e36dbfa 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -1,94 +1,6 @@ open Json_encoding open Json_schema -(* TODO: deduplicate with GobConfig *) -(** The ultimate convenience function for writing values. *) -let one_quote = Str.regexp "\'" -let parse_goblint_json s = - try - let s' = Str.global_replace one_quote "\"" s in - let v = Yojson.Safe.from_string s' in - v - with Yojson.Json_error _ -> - `String s - -(* Convert old Defaults options to schema. *) - -type defaults = (string * (DefaultsCategory.category * string * string)) list - -let rec element_category_of_defaults_json (defaults: defaults) (json: Yojson.Safe.t) (path: string): element * DefaultsCategory.category = - let name = BatString.lchop path in (* chop initial . *) - let element_defaults kind = (* element with metadata from defaults *) - let (category, description, default) = List.assoc name defaults in - let default_json = parse_goblint_json default in - let element = { (element kind) with - title = Some name; - description = Some description; - default = Some (Json_repr.repr_to_any (module Json_repr.Yojson) default_json); - } - in - (element, category) - in - match json with - | `String s -> - element_defaults @@ String string_specs - | `Bool b -> - element_defaults @@ Boolean - | `Int i -> - element_defaults @@ Integer numeric_specs - | `List xs -> - let element_element = match path with - | ".phases" -> element (Id_ref "") (* refer to entire schema itself *) - | _ -> element (String string_specs) (* all other lists contain strings *) - in - element_defaults @@ Monomorphic_array (element_element, array_specs) - | `Assoc xs -> - let category = ref None in - let properties = List.map (fun (key, value) -> - let (field_element, field_category) = element_category_of_defaults_json defaults value (path ^ "." ^ key) in - category := Some field_category; (* category from defaults for object description *) - (key, field_element, false, None) - ) xs - in - let category = Option.get !category in - let element = element @@ Object { - object_specs with - properties; - additional_properties = None; (* forbid additional properties *) - } - in - let element = match BatString.index_after_n '.' 2 path with - | exception Not_found when path = ".interact" -> (* interact isn't Std *) - { element with - title = Some name; - } - | exception Not_found when path = "" -> (* is root *) - element - | exception Not_found -> (* category *) - { element with - title = Some (DefaultsCategory.show_category category); - description = Some (DefaultsCategory.catDescription category); - } - | _ -> (* inner object, not category *) - { element with - title = Some name; - } - in - (element, category) - | _ -> - failwith (Format.asprintf "element_category_of_defaults_json: %a" Yojson.Safe.pp json) - -let schema_of_defaults_json defaults json = - let (element, _) = element_category_of_defaults_json defaults json "" in - JsonSchema.create_schema element - - -(* let defaults_schema = - let defaults = List.map (fun (c, (n, (desc, def))) -> (n, (c, desc, def))) !Defaults.registrar in (* transform for assoc list lookup by name *) - schema_of_defaults_json defaults !GobConfig.json_conf - -let () = - Yojson.Safe.pretty_to_channel (Stdlib.open_out "options.schema.json") (JsonSchema.schema_to_yojson defaults_schema) *) let schema_of_yojson json = (* workaround for json-data-encoding not handling recursive root reference correctly *) From e8bbecee05999bb54e8c9e7dadb0e7b96427cc89 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Dec 2021 12:02:10 +0200 Subject: [PATCH 52/55] Remove now unused GobConfig.build_config --- src/util/gobConfig.ml | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index 827b86e1ca..adab7c9592 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -24,7 +24,6 @@ open Printf exception ConfigError of string -let build_config = ref false (* Phase of the analysis (moved from GoblintUtil b/c of circular build...) *) let phase = ref 0 @@ -225,9 +224,10 @@ struct in begin try `Assoc (modify m) with Not_found -> - if !build_config then + (* TODO: allow unknown paths to create subobjects, will be validated against schema anyway *) + (* if !build_config then `Assoc (m @ [(key, create_new v pth)]) - else + else *) raise @@ ConfigError ("Unknown path "^ (sprintf2 "%a" print_path orig_pth)) end | `List a, Index (Int i, pth) -> @@ -256,9 +256,7 @@ struct new_v in o := set_value v !o orig_pth; - - if not !build_config then (* object incomplete during building *) - Validator.validate_exn !json_conf + Validator.validate_exn !json_conf (** Helper function for reading values. Handles error messages. *) let get_path_string f st = @@ -309,7 +307,7 @@ struct (** Helper functions for writing values. Handels the tracing. *) let set_path_string_trace st v = - if not !build_config then drop_memo (); + drop_memo (); if tracing then trace "conf" "Setting '%s' to %a.\n" st GobYojson.pretty v; set_path_string st v @@ -319,7 +317,7 @@ struct let set_string st i = set_path_string_trace st (`String i) let set_null st = set_path_string_trace st `Null let set_list st l = - if not !build_config then drop_memo (); + drop_memo (); set_value (`List l) json_conf (parse_path st) (** A convenience functions for writing values. *) @@ -358,8 +356,5 @@ end include Impl let () = - (* build_config := true; - List.iter (fun (c, (n, (desc, def))) -> set_auto n def) !Defaults.registrar; - build_config := false; *) json_conf := Options.defaults; ValidatorRequireAll.validate_exn !json_conf From 249360b8c455e321c785b2b70526f2d4e64524a3 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Dec 2021 12:12:35 +0200 Subject: [PATCH 53/55] Implement string enum validation in JSON --- src/util/jsonSchema.ml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/util/jsonSchema.ml b/src/util/jsonSchema.ml index 8b69a38a97..a3fd302cb3 100644 --- a/src/util/jsonSchema.ml +++ b/src/util/jsonSchema.ml @@ -13,7 +13,19 @@ let rec encoding_of_schema_element (top: unit Json_encoding.encoding) (schema_el let open Json_encoding in match schema_element.kind with | Any -> unit - | String string_specs -> erase string + | String string_specs -> + begin match schema_element.enum with + | None -> + erase string + | Some enum -> + enum + |> List.map (fun value -> + match Json_repr.any_to_repr (module Json_repr.Yojson) value with + | `String value -> (value, ()) + | _ -> failwith "encoding_of_schema_element: string_enum" + ) + |> string_enum + end | Boolean -> erase bool | Integer numeric_specs -> erase int | Monomorphic_array (el, array_specs) -> From cdd9719a8bcaa6357aa643243a6e8cc1ea60c096 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Dec 2021 12:22:19 +0200 Subject: [PATCH 54/55] Add string enums to options schema (PR #499) --- src/util/options.schema.json | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/util/options.schema.json b/src/util/options.schema.json index c2c7e9bcdb..489669bfbd 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -125,6 +125,7 @@ "description": "Result style: none, fast_xml, json, pretty, json-messages.", "type": "string", + "enum": ["none", "fast_xml", "json", "pretty", "json-messages"], "default": "none" }, "solver": { @@ -163,6 +164,7 @@ "description": "Colored output (via ANSI escape codes). 'auto': enabled if stdout is a terminal (instead of a pipe); 'always', 'never'.", "type": "string", + "enum": ["auto", "always", "never"], "default": "auto" }, "g2html": { @@ -230,6 +232,7 @@ "description": "When to output warnings. Values: 'post' (default): after solving; 'never': no warnings; 'early': for debugging - outputs warnings already while solving (may lead to spurious warnings/asserts that would disappear after narrowing).", "type": "string", + "enum": ["post", "never", "early"], "default": "post" }, "gobview": { @@ -410,6 +413,7 @@ "description": "Use mutual refinement of integer domains. Either 'never', 'once' or 'fixpoint'", "type": "string", + "enum": ["never", "once", "fixpoint"], "default": "never" } }, @@ -618,6 +622,7 @@ "description": "Which domain should be used for the Apron analysis. Can be 'octagon', 'interval' or 'polyhedra'", "type": "string", + "enum": ["octagon", "interval", "polyhedra"], "default": "octagon" }, "threshold_widening": { @@ -653,6 +658,7 @@ "description": "Which domain should be used for the thread ids. Can be 'history' or 'plain'", "type": "string", + "enum": ["history", "plain"], "default": "history" } }, @@ -716,6 +722,7 @@ "description": "In order to reuse the function's old abstract value the new abstract value must be leq (focus on efficiency) or equal (focus on precision) compared to the old.", "type": "string", + "enum": ["leq", "equal"], "default": "leq" } }, @@ -726,6 +733,7 @@ "description": "Which comparison should be used for functions? 'ast'/'cfg' (cfg comparison also differentiates which nodes of a function have changed)", "type": "string", + "enum": ["ast", "cfg"], "default": "ast" }, "force-reanalyze": { @@ -802,6 +810,7 @@ "description": "How to handle overflows of signed types. Values: 'assume_top' (default): Assume signed overflow results in a top value; 'assume_none': Assume program is free of signed overflows; 'assume_wraparound': Assume signed types wrap-around and two's complement representation of signed integers", "type": "string", + "enum": ["assume_top", "assume_none", "assume_wraparound"], "default": "assume_top" } }, @@ -1033,6 +1042,7 @@ "description": "Which privatization to use? none/protection-old/mutex-oplus/mutex-meet/protection/protection-read/protection-vesal/mine/mine-nothread/mine-W/mine-W-noinit/lock/write/write+lock", "type": "string", + "enum": ["none", "protection-old", "mutex-oplus", "mutex-meet", "protection", "protection-read", "protection-vesal", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "write", "write+lock"], "default": "protection-read" }, "priv-prec-dump": { @@ -1057,6 +1067,7 @@ "description": "Which apron privatization to use? dummy/protection/protection-path/mutex-meet/mutex-meet-tid/mutex-meet-tid-cluster12/mutex-meet-tid-cluster2/mutex-meet-tid-cluster-max/mutex-meet-tid-cluster-power", "type": "string", + "enum": ["dummy", "protection", "protection-path", "mutex-meet", "mutex-meet-tid", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"], "default": "mutex-meet" }, "priv": { @@ -1240,6 +1251,7 @@ "description": "When to widen in side. never: never widen, always: always widen, sides: widen if there are multiple side-effects from the same var resulting in a new value, cycle: widen if a called or a start var get destabilized, unstable_called: widen if any called var gets destabilized, unstable_self: widen if side-effected var gets destabilized, sides-pp: widen if there are multiple side-effects from the same program point resulting in a new value.", "type": "string", + "enum": ["never", "always", "sides", "cycle", "unstable_called", "unstable_self", "sides-pp"], "default": "sides" }, "space": { @@ -1317,6 +1329,7 @@ "title": "exp.witness.id", "description": "Which witness node IDs to use? node/enumerate", "type": "string", + "enum": ["node", "enumerate"], "default": "node" }, "invariant": { @@ -1328,6 +1341,7 @@ "description": "Which witness nodes to add invariants to? all/loop_heads/none", "type": "string", + "enum": ["all", "loop_heads", "none"], "default": "all" } }, @@ -1383,6 +1397,7 @@ "description": "When using the partitioning which expression should be used for partitioning ('first', 'last')", "type": "string", + "enum": ["first", "last"], "default": "first" }, "partition-by-const-on-return": { @@ -1411,6 +1426,7 @@ "description": "The domain that should be used for structs. simple/sets/keyed/combined-all/combined-sk", "type": "string", + "enum": ["simple", "sets", "keyed", "combined-all", "combined-sk"], "default": "simple" }, "key": { From 1f1deeb024050dc0d53d93e9e2bb916573b97833 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Dec 2021 12:23:21 +0200 Subject: [PATCH 55/55] Fix JSON schema indentation --- src/util/gobConfig.ml | 6 +++--- src/util/jsonSchema.ml | 7 ++++--- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index adab7c9592..072262a965 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -226,9 +226,9 @@ struct with Not_found -> (* TODO: allow unknown paths to create subobjects, will be validated against schema anyway *) (* if !build_config then - `Assoc (m @ [(key, create_new v pth)]) - else *) - raise @@ ConfigError ("Unknown path "^ (sprintf2 "%a" print_path orig_pth)) + `Assoc (m @ [(key, create_new v pth)]) + else *) + raise @@ ConfigError ("Unknown path "^ (sprintf2 "%a" print_path orig_pth)) end | `List a, Index (Int i, pth) -> `List (List.modify_at i (fun o -> set_value v o pth) a) diff --git a/src/util/jsonSchema.ml b/src/util/jsonSchema.ml index a3fd302cb3..d0b4c1cc86 100644 --- a/src/util/jsonSchema.ml +++ b/src/util/jsonSchema.ml @@ -80,9 +80,10 @@ let rec element_require_all (element: element): element = | Integer _ | Number _ -> element.kind | Monomorphic_array (element_element, array_specs) -> - let array_specs' = { array_specs with - additional_items = Option.map element_require_all array_specs.additional_items; - } + let array_specs' = + { array_specs with + additional_items = Option.map element_require_all array_specs.additional_items; + } in Monomorphic_array (element_require_all element_element, array_specs') | Object object_specs ->