Merge branch 'master' into malloc_uniqueness

Author: michael-schwarz

.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,13 @@
+
+(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
+    svcomp.json
+    svcomp21.json
+    svcomp22.json
+    ; 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,16 @@
 # 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`. If Goblint is installed these can
+be accessed without the conf prefix, e.g. with `./goblint --conf examples/large-programs.json`.
+
+- `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

@@ -30,7 +30,6 @@
     (zarith (>= 1.8))
     (yojson (>= 2.0.0))
     qcheck-core
-    (ppx_distr_guards (>= 0.2))
     ppx_deriving
     ppx_deriving_hash
     ppx_deriving_yojson
@@ -55,5 +54,5 @@
     apron
     z3
   )
-  (sites (share includes))
+  (sites (share includes) (share conf))
 )

g2html

@@ -26,7 +26,6 @@ depends: [
   "zarith" {>= "1.8"}
   "yojson" {>= "2.0.0"}
   "qcheck-core"
-  "ppx_distr_guards" {>= "0.2"}
   "ppx_deriving"
   "ppx_deriving_hash"
   "ppx_deriving_yojson"