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/dune-project b/dune-project index f6753e5218..bc5041205e 100644 --- a/dune-project +++ b/dune-project @@ -32,10 +32,12 @@ (ppx_distr_guards (>= 0.2)) ppx_deriving ppx_deriving_yojson + (ppx_blob (>= 0.6.0)) (ocaml-monadic (>= 0.5)) (ounit2 :with-test) (odoc :with-doc) dune-site + json-data-encoding (sha (>= 1.12)) (conf-gmp (>= 3)) ; only needed transitively, but they don't have lower bound, which is needed on MacOS (conf-ruby :with-test) diff --git a/goblint.opam b/goblint.opam index 80bf24f638..56ba97ae8e 100644 --- a/goblint.opam +++ b/goblint.opam @@ -28,10 +28,12 @@ depends: [ "ppx_distr_guards" {>= "0.2"} "ppx_deriving" "ppx_deriving_yojson" + "ppx_blob" {>= "0.6.0"} "ocaml-monadic" {>= "0.5"} "ounit2" {with-test} "odoc" {with-doc} "dune-site" + "json-data-encoding" "sha" {>= "1.12"} "conf-gmp" {>= "3"} "conf-ruby" {with-test} diff --git a/goblint.opam.locked b/goblint.opam.locked index 807e240820..97b225f9a7 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.4.0"} "benchmark" {= "1.6" & with-test} + "bigarray-compat" {= "1.0.0"} + "bigstringaf" {= "0.7.0"} "biniou" {= "1.2.1"} "camlidl" {= "1.09"} "cmdliner" {= "1.0.4" & with-doc} "conf-gmp" {= "3"} "conf-mpfr" {= "2"} "conf-perl" {= "1"} + "conf-pkg-config" {= "2"} "conf-ruby" {= "1.0.0" & with-test} "cppo" {= "1.6.7"} "dune" {= "2.9.1"} @@ -41,6 +45,7 @@ depends: [ "fmt" {= "0.9.0" & with-doc} "fpath" {= "0.7.3" & with-doc} "goblint-cil" {= "1.8.2"} + "json-data-encoding" {= "0.10"} "logs" {= "0.7.0" & with-doc} "mlgmpidl" {= "1.2.13"} "num" {= "1.4"} @@ -51,11 +56,13 @@ depends: [ "ocaml-migrate-parsetree" {= "2.2.0" & with-doc} "ocaml-monadic" {= "0.5"} "ocaml-options-vanilla" {= "1"} + "ocaml-syntax-shims" {= "1.0.0"} "ocamlbuild" {= "0.14.0"} "ocamlfind" {= "1.9.1"} "odoc" {= "2.0.2" & with-doc} "odoc-parser" {= "0.9.0" & with-doc} "ounit2" {= "2.2.4" & with-test} + "ppx_blob" {= "0.7.2"} "ppx_derivers" {= "1.2.1"} "ppx_deriving" {= "5.2.1"} "ppx_deriving_yojson" {= "3.6.1"} @@ -68,9 +75,11 @@ depends: [ "sexplib0" {= "v0.14.0"} "sha" {= "1.15.1"} "stdlib-shims" {= "0.3.0"} + "stringext" {= "1.6.0"} "topkg" {= "1.0.3" & with-doc} "tyxml" {= "4.4.0" & with-doc} "uchar" {= "0.0.2" & with-doc} + "uri" {= "4.2.0"} "uutf" {= "1.0.2" & with-doc} "yojson" {= "1.7.0"} "zarith" {= "1.12"} 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': diff --git a/src/dune b/src/dune index 95af13fb04..70c35126ae 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 json-data-encoding ; Conditionally compile based on whether apron optional dependency is installed or not. ; Alternative dependencies seem like the only way to optionally depend on optional dependencies. ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies. @@ -35,7 +35,8 @@ ) (preprocess (staged_pps ppx_deriving.std ppx_deriving_yojson - ppx_distr_guards ocaml-monadic)) + ppx_distr_guards ocaml-monadic ppx_blob)) + (preprocessor_deps (file util/options.schema.json)) ) ; Workaround for alternative dependencies with unqualified subdirs. 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 edeadd9b4e..dac23c604c 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -2,7 +2,6 @@ open Prelude open GobConfig -open Defaults open Printf open Goblintutil @@ -83,10 +82,10 @@ let option_spec_list = set_bool "dbg.print_dead_code" true; set_string "result" "sarif" in - let defaults_spec_list = List.map (fun (_, (name, (_, _))) -> + let defaults_spec_list = List.map (fun path -> (* allow "--option value" as shorthand for "--set option value" *) - ("--" ^ name, Arg.String (set_auto name), "") - ) !Defaults.registrar + ("--" ^ path, Arg.String (set_auto path), "") + ) Options.paths in let tmp_arg = ref "" in [ "-o" , Arg.String (set_string "outfile"), "" @@ -100,8 +99,8 @@ let option_spec_list = ; "--conf" , Arg.String merge_file, "" ; "--writeconf" , Arg.String (fun fn -> writeconffile := fn), "" ; "--version" , Arg.Unit print_version, "" - ; "--print_options" , Arg.Unit (fun _ -> printCategory stdout Std; exit 0), "" - ; "--print_all_options" , Arg.Unit (fun _ -> printAllCategories stdout; exit 0), "" + ; "--print_options" , Arg.Unit (fun () -> Options.print_options (); exit 0), "" + ; "--print_all_options" , Arg.Unit (fun () -> Options.print_all_options (); exit 0), "" ; "--trace" , Arg.String set_trace, "" ; "--tracevars" , add_string Tracing.tracevars, "" ; "--tracelocs" , add_int Tracing.tracelocs, "" @@ -362,13 +361,12 @@ let do_analyze change_info merged_AST = Printexc.raise_with_backtrace e backtrace (* re-raise with captured inner backtrace *) (* Cilfacade.current_file := ast'; *) in - (* old style is ana.activated = [phase_1, ...] with phase_i = [ana_1, ...] - new style (Goblintutil.phase_config = true) is phases[i].ana.activated = [ana_1, ...] + (* new style is phases[i].ana.activated = [ana_1, ...] phases[i].ana.x overwrites setting ana.x *) let num_phases = let np,na,nt = Tuple3.mapn (List.length % get_list) ("phases", "ana.activated", "trans.activated") in - phase_config := np > 0; (* TODO what about wrong usage like { phases = [...], ana.activated = [...] }? should child-lists add to parent-lists? *) - if get_bool "dbg.verbose" then print_endline @@ "Using " ^ if !phase_config then "new" else "old" ^ " format for phases!"; + (* TODO what about wrong usage like { phases = [...], ana.activated = [...] }? should child-lists add to parent-lists? *) + if get_bool "dbg.verbose" then print_endline @@ "Using new format for phases!"; if np = 0 && na = 0 && nt = 0 then failwith "No phases and no activated analyses or transformations!"; max np 1 in diff --git a/src/util/defaults.ml b/src/util/defaults.ml deleted file mode 100644 index a002065ac4..0000000000 --- a/src/util/defaults.ml +++ /dev/null @@ -1,384 +0,0 @@ -(** Default values for [GobConfig]-style configuration. *) - -open Prelude -open Printf -open List - -(* 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 [] - -(** 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) - -(** 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 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} - -let _ = - let v = Yojson.Safe.from_string default_schema in - GobConfig.addenum_sch v diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index 860705d8b5..072262a965 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -21,15 +21,16 @@ open Prelude open Tracing open Printf -open JsonSchema 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 -let phase_config = ref true + + +module Validator = JsonSchema.Validator (struct let schema = Options.schema end) +module ValidatorRequireAll = JsonSchema.Validator (struct let schema = Options.require_all end) (** The type for [gobConfig] module. *) module type S = @@ -77,8 +78,7 @@ 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 (** The implementation of the [gobConfig] module. *) @@ -166,18 +166,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 @@ -227,12 +215,20 @@ 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) - else - raise @@ ConfigError ("Unknown path "^ (sprintf2 "%a" print_path orig_pth)) + (* 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)) end | `List a, Index (Int i, pth) -> `List (List.modify_at i (fun o -> set_value v o pth) a) @@ -260,7 +256,7 @@ struct new_v in o := set_value v !o orig_pth; - validate conf_schema !json_conf + Validator.validate_exn !json_conf (** Helper function for reading values. Handles error messages. *) let get_path_string f st = @@ -268,11 +264,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 @@ -314,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 @@ -324,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. *) @@ -353,9 +346,15 @@ 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 + Validator.validate_exn v; json_conf := GobYojson.merge !json_conf v; + 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 include Impl + +let () = + json_conf := Options.defaults; + ValidatorRequireAll.validate_exn !json_conf diff --git a/src/util/jsonSchema.ml b/src/util/jsonSchema.ml index fac016a139..d0b4c1cc86 100644 --- a/src/util/jsonSchema.ml +++ b/src/util/jsonSchema.ml @@ -1,187 +1,143 @@ -(** 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 +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 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 + +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 -> + 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) -> + 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 top element) + else + dft name (encoding_of_schema_element top element) () + in + erase @@ merge_objs acc (obj1 field) + ) (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 = + let root = Json_schema.root schema in + Json_encoding.mu "" (fun top -> encoding_of_schema_element top root) + +open Json_encoding +open Json_schema + +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 + | None -> + begin match element.kind with + | Object object_specs -> + `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 "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 *) + +let rec element_require_all (element: element): element = + let kind' = match element.kind with + | String _ + | Boolean + | Id_ref _ + | 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; + } + in + Monomorphic_array (element_require_all element_element, array_specs') + | Object object_specs -> + 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 "element_require_all" 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 + { element with kind = kind' } + +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 () = 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 _ 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 _ 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_query: %a" (Json_encoding.print_error ?print_unknown:None) exn in + Some msg + | _ -> None (* for other exceptions *) + ) diff --git a/src/util/options.ml b/src/util/options.ml new file mode 100644 index 0000000000..261e36dbfa --- /dev/null +++ b/src/util/options.ml @@ -0,0 +1,96 @@ +open Json_encoding +open Json_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 = 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); _} -> + 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 + 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 = JsonSchema.schema_require_all schema + +let defaults = JsonSchema.schema_defaults schema + +let () = + (* 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; *) + () + +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 _ + | 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) diff --git a/src/util/options.schema.json b/src/util/options.schema.json new file mode 100644 index 0000000000..489669bfbd --- /dev/null +++ b/src/util/options.schema.json @@ -0,0 +1,1812 @@ +{ + "$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", + "enum": ["none", "fast_xml", "json", "pretty", "json-messages"], + "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", + "enum": ["auto", "always", "never"], + "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", + "enum": ["post", "never", "early"], + "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" ] + }, + "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", + "enum": ["never", "once", "fixpoint"], + "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", + "enum": ["octagon", "interval", "polyhedra"], + "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", + "enum": ["history", "plain"], + "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", + "enum": ["leq", "equal"], + "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", + "enum": ["ast", "cfg"], + "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", + "enum": ["assume_top", "assume_none", "assume_wraparound"], + "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": { + "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", + "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": { + "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", + "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": { + "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", + "enum": ["never", "always", "sides", "cycle", "unstable_called", "unstable_self", "sides-pp"], + "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 + } + }, + "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", + "enum": ["node", "enumerate"], + "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", + "enum": ["all", "loop_heads", "none"], + "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", + "enum": ["first", "last"], + "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", + "enum": ["simple", "sets", "keyed", "combined-all", "combined-sk"], + "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 + }, + "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 + } + }, + "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 + } + }, + "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/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