Provide Common Configurations

.github/workflows/options.yml

@@ -30,7 +30,7 @@ jobs:
           sed -i 's|"$schema": "http://json-schema.org/draft-04/schema#",||' src/util/options.schema.json
 
       - name: Validate conf
-        run: ajv validate -s src/util/options.schema.json -d "conf/*.json"
+        run: ajv validate -s src/util/options.schema.json -d "conf/**/*.json"
 
       - name: Validate incremental tests
         run: ajv validate -s src/util/options.schema.json -d "tests/incremental/*/*.json"

conf/dune

@@ -0,0 +1,10 @@
+
+(install
+  (section (site (goblint conf)))
+  (files
+    (examples/large-program.json as examples/large-program.json) ; must repeat directory, otherwise gets stripped from target
+    (examples/medium-program.json as examples/medium-program.json) ; must repeat directory, otherwise gets stripped from target
+    (examples/very-precise.json as examples/very-precise.json) ; must repeat directory, otherwise gets stripped from target
+    ; no way to glob here...
+  )
+)

conf/examples/large-program.json

@@ -0,0 +1,20 @@
+{
+    "ana": {
+      "activated": [
+        "base", "mallocWrapper","escape","mutex","mutexEvents","access"
+      ],
+      "base": {
+        "privatization": "none",
+        "context": {
+          "non-ptr": false
+        }
+      },
+      "thread": {
+        "domain": "plain",
+        "include-node": false
+      }
+    },
+    "exp": {
+      "earlyglobs": true
+    }
+  }

conf/examples/medium-program.json

@@ -0,0 +1,29 @@
+{
+  "ana": {
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "escape",
+      "expRelation",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread"
+    ],
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    }
+  }
+}

conf/examples/very-precise.json

@@ -0,0 +1,65 @@
+{
+  "ana": {
+    "int": {
+      "def_exc": true,
+      "enums": true,
+      "interval": true,
+      "congruence": true,
+      "refinement": "fixpoint",
+      "interval_threshold_widening" : true,
+      "def_exc_widen_by_join" : true
+    },
+    "path_sens" : [ "mutex", "malloc_null", "uninit","threadflag" ],
+    "apron" : {
+      "domain": "octagon",
+      "threshold_widening": true,
+      "privatization": "mutex-meet-tid-cluster12",
+      "strengthening": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "escape",
+      "expRelation",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "apron"
+    ],
+    "context": {
+      "widen": false
+    },
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+        "ldv_malloc",
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc"
+      ]
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      },
+      "structs" : {
+        "domain" : "combined-sk"
+      }
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3"
+}

docs/user-guide/configuring.md

@@ -1,6 +1,15 @@
 # Configuring
 
-## JSON conf files
+On top of passing options via the command line, Goblint can be configured with `json` files following the schema outlined in `/src/util/options.schema.json`
+or using one of the default configurations we provide.
+
+# Example Configurations for Goblint
+
+The repository contains some example configurations for the Goblint analyzer in the folder `conf/examples`.
+
+- `very-precise.json`: Enables some of the more expensive abstract domains and features, especially useful for smaller programs
+- `medium-program.json`: Enables some costly features, but staying away from the very expensive ones. This is very close to, e.g. the configuration we use for SV-COMP
+- `large-programs.json`: Minimal configuration for larger programs, should run fast even for large programs, but usually needs to be made more precise by adding further features.
 
 ### JSON schema
 

docs/user-guide/running.md

@@ -25,6 +25,12 @@ For a list of all options and their possible configurations, run:
 ./goblint --print_all_options
 ```
 
+To use one of the pre-defined configurations, run:
+
+```console
+./goblint --conf path/to/config.json files
+```
+
 ## Analyzing Recursive Programs
 In some cases, when using the default configuration, Goblint might not terminate in reasonable time on recursive programs, or
 crash in a stack overflow (indicated by the error message `exception Stack overflow`). If the stack overflow occurs within a C function called by Goblint, it will result in the following error message: `Command terminated by signal 11`.

dune-project

@@ -55,5 +55,5 @@
     apron
     z3
   )
-  (sites (share includes))
+  (sites (share includes) (share conf))
 )

src/maingoblint.ml

@@ -36,6 +36,7 @@ let print_help ch =
   fprintf ch " are used instead of double-quotes (\").\n\n";
   fprintf ch "A <jpath> is a path in a json structure. E.g. 'field.another_field[42]';\n";
   fprintf ch "in addition to the normal syntax you can use 'field[+]' append to an array.\n\n";
+  fprintf ch "Some common configurations to start from can be found in conf/examples/*\n";
   exit 0
 
 (** [Arg] option specification *)

src/sites/goblint_sites.mli

@@ -1 +1,2 @@
 val includes: string list
+val conf: string list

src/sites/sites_dune/goblint_sites.ml

@@ -1 +1,2 @@
 let includes = Dunesite.Sites.includes (* export without all the intermediate modules *)
+let conf = Dunesite.Sites.conf

src/util/gobConfig.ml

@@ -351,7 +351,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 (Fpath.to_string fn) in
+    let file = Fpath.to_string fn in
+    let path = if Sys.file_exists file then file else
+        let configs = List.map Fpath.v Goblint_sites.conf in
+        let r = List.find_opt (fun v -> Fpath.filename fn = Fpath.filename v) configs in
+        match r with
+        | Some r -> Fpath.to_string r
+        | _ -> file
+    in
+    let v = Yojson.Safe.from_channel % BatIO.to_input_channel |> File.with_file_in path in
     merge v;
     if tracing then trace "conf" "Merging with '%a', resulting\n%a.\n" GobFpath.pretty fn GobYojson.pretty !json_conf
 end