Merge branch 'master' into pldi-bench

.github/workflows/locked.yml

@@ -153,7 +153,7 @@ jobs:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 

.github/workflows/metadata.yml

@@ -39,7 +39,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 

.github/workflows/options.yml

@@ -18,18 +18,18 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
-        uses: actions/setup-node@v3
+        uses: actions/setup-node@v4
         with:
           node-version: ${{ matrix.node-version }}
 
       - name: Install ajv-cli
         run: npm install -g ajv-cli
 
       - name: Migrate schema # https://github.com/ajv-validator/ajv-cli/issues/199
-        run: ajv migrate -s src/util/options.schema.json
+        run: ajv migrate -s src/common/util/options.schema.json
 
       - name: Validate conf
-        run: ajv validate -s src/util/options.schema.json -d "conf/**/*.json"
+        run: ajv validate -s src/common/util/options.schema.json -d "conf/**/*.json"
 
       - name: Validate incremental tests
-        run: ajv validate -s src/util/options.schema.json -d "tests/incremental/*/*.json"
+        run: ajv validate -s src/common/util/options.schema.json -d "tests/incremental/*/*.json"

.readthedocs.yaml

@@ -20,4 +20,4 @@ build:
       - pip install json-schema-for-humans
     post_build:
       - mkdir _readthedocs/html/jsfh/
-      - generate-schema-doc --config-file jsfh.yml src/util/options.schema.json _readthedocs/html/jsfh/
+      - generate-schema-doc --config-file jsfh.yml src/common/util/options.schema.json _readthedocs/html/jsfh/

conf/ldv-races.json

@@ -53,8 +53,11 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   },
   "solver": "td3",
   "sem": {

conf/svcomp-yaml.json

@@ -76,7 +76,9 @@
     "region-offsets": true
   },
   "witness": {
-    "enabled": false,
+    "graphml": {
+      "enabled": false
+    },
     "yaml": {
       "enabled": true
     },

conf/svcomp.json

@@ -83,7 +83,8 @@
         "congruence",
         "octagon",
         "wideningThresholds",
-        "loopUnrollHeuristic"
+        "loopUnrollHeuristic",
+        "memsafetySpecification"
       ]
     }
   },
@@ -103,8 +104,11 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   },
   "pre": {
     "enabled": false

conf/svcomp21.json

@@ -64,6 +64,9 @@
     }
   },
   "witness": {
-    "id": "enumerate"
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate"
+    }
   }
 }

conf/svcomp22-intervals-novareq-affeq-apron.json

@@ -68,7 +68,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }

conf/svcomp22-intervals-novareq-affeq-native.json

@@ -65,7 +65,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }

conf/svcomp22-intervals-novareq-octagon-apron.json

@@ -68,7 +68,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }

conf/svcomp22-intervals-novareq-polyhedra-apron.json

@@ -68,7 +68,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }

conf/svcomp22.json

@@ -67,7 +67,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }

conf/svcomp23.json

@@ -90,7 +90,10 @@
     }
   },
   "witness": {
-    "id": "enumerate",
-    "unknown": false
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    }
   }
 }

docs/user-guide/configuring.md

@@ -24,7 +24,7 @@ In `.vscode/settings.json` add the following:
                 "/conf/*.json",
                 "/tests/incremental/*/*.json"
             ],
-            "url": "/src/util/options.schema.json"
+            "url": "/src/common/util/options.schema.json"
         }
     ]
 }

mkdocs.yml

@@ -30,7 +30,7 @@ nav:
     - 👶 Your first analysis: developer-guide/firstanalysis.md
     - 🏫 Extending library: developer-guide/extending-library.md
     - 📢 Messaging: developer-guide/messaging.md
-    - 🗃️ API reference: https://goblint.github.io/analyzer/
+    - 🗃️ API reference: https://goblint.github.io/analyzer/goblint/
     - 🚨 Testing: developer-guide/testing.md
     - 🪲 Debugging: developer-guide/debugging.md
     - 📉 Profiling: developer-guide/profiling.md

scripts/goblint-lib-modules.py

@@ -6,16 +6,20 @@
 
 src_root_path = Path("./src")
 
-goblint_lib_path = src_root_path / "goblint_lib.ml"
+goblint_lib_paths = [
+    src_root_path / "goblint_lib.ml",
+    src_root_path / "util" / "std" / "goblint_std.ml",
+]
 goblint_lib_modules = set()
 
-with goblint_lib_path.open() as goblint_lib_file:
-    for line in goblint_lib_file:
-        line = line.strip()
-        m = re.match(r"module (.*) = .*", line)
-        if m is not None:
-            module_name = m.group(1)
-            goblint_lib_modules.add(module_name)
+for goblint_lib_path in goblint_lib_paths:
+    with goblint_lib_path.open() as goblint_lib_file:
+        for line in goblint_lib_file:
+            line = line.strip()
+            m = re.match(r"module (.*) = .*", line)
+            if m is not None:
+                module_name = m.group(1)
+                goblint_lib_modules.add(module_name)
 
 src_vendor_path = src_root_path / "vendor"
 exclude_module_names = set([
@@ -29,15 +33,21 @@
     "Mainspec",
 
     # libraries
+    "Goblint_std",
     "Goblint_timing",
     "Goblint_backtrace",
     "Goblint_sites",
     "Goblint_build_info",
+    "Dune_build_info",
 
     "MessageCategory", # included in Messages
     "PreValueDomain", # included in ValueDomain
     "SpecCore", # spec stuff
     "SpecUtil", # spec stuff
+
+    "ConfigVersion",
+    "ConfigProfile",
+    "ConfigOcaml",
 ])
 
 src_modules = set()

src/analyses/abortUnless.ml

@@ -65,8 +65,8 @@ struct
     false
 
   let startstate v = false
-  let threadenter ctx lval f args = [false]
-  let threadspawn ctx lval f args fctx = false
+  let threadenter ctx ~multiple lval f args = [false]
+  let threadspawn ctx ~multiple lval f args fctx = false
   let exitstate v = false
 end
 

src/analyses/accessAnalysis.ml

@@ -54,7 +54,7 @@ struct
 
   (** We just lift start state, global and dependency functions: *)
   let startstate v = ()
-  let threadenter ctx lval f args = [()]
+  let threadenter ctx ~multiple lval f args = [()]
   let exitstate  v = ()
   let context fd d = ()
 
@@ -121,7 +121,7 @@ struct
     ctx.local
 
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx  ~multiple lval f args fctx =
     (* must explicitly access thread ID lval because special to pthread_create doesn't if singlethreaded before *)
     begin match lval with
       | None -> ()

src/analyses/activeLongjmp.ml

@@ -26,7 +26,7 @@ struct
 
   (* Initial values don't really matter: overwritten at longjmp call. *)
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =

src/analyses/activeSetjmp.ml

@@ -25,7 +25,7 @@ struct
     | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.bot ()]
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
   let exitstate v = D.top ()
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =

src/analyses/apron/relationAnalysis.apron.ml

@@ -647,7 +647,7 @@ struct
 
   (* Thread transfer functions. *)
 
-  let threadenter ctx lval f args =
+  let threadenter ctx ~multiple lval f args =
     let st = ctx.local in
     match Cilfacade.find_varinfo_fundec f with
     | fd ->
@@ -665,7 +665,7 @@ struct
       (* TODO: do something like base? *)
       failwith "relation.threadenter: unknown function"
 
-  let threadspawn ctx lval f args fctx =
+  let threadspawn ctx ~multiple lval f args fctx =
     ctx.local
 
   let event ctx e octx =