Merge branch 'master' into priv-atomic

.github/workflows/coverage.yml

@@ -88,7 +88,7 @@ jobs:
           COVERALLS_REPO_TOKEN: ${{ secrets.COVERALLS_REPO_TOKEN }}
           PULL_REQUEST_NUMBER: ${{ github.event.number }}
 
-      - uses: actions/upload-artifact@v3
+      - uses: actions/upload-artifact@v4
         if: always()
         with:
           name: suite_result

.github/workflows/docs.yml

@@ -46,7 +46,7 @@ jobs:
 
       - name: Setup Pages
         id: pages
-        uses: actions/configure-pages@v3
+        uses: actions/configure-pages@v4
 
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-doc
@@ -68,4 +68,4 @@ jobs:
     steps:
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v2
+        uses: actions/deploy-pages@v3

.github/workflows/locked.yml

@@ -82,10 +82,10 @@ jobs:
       - name: Test incremental regression with cfg comparison
         run: ruby scripts/update_suite.rb -c
 
-      - uses: actions/upload-artifact@v3
+      - uses: actions/upload-artifact@v4
         if: always()
         with:
-          name: suite_result
+          name: suite_result-${{ matrix.os }}
           path: tests/suite_result/
 
   extraction:

.github/workflows/options.yml

@@ -26,10 +26,10 @@ jobs:
         run: npm install -g ajv-cli
 
       - name: Migrate schema # https://github.com/ajv-validator/ajv-cli/issues/199
-        run: ajv migrate -s src/common/util/options.schema.json
+        run: ajv migrate -s src/config/options.schema.json
 
       - name: Validate conf
-        run: ajv validate -s src/common/util/options.schema.json -d "conf/**/*.json"
+        run: ajv validate -s src/config/options.schema.json -d "conf/**/*.json"
 
       - name: Validate incremental tests
-        run: ajv validate -s src/common/util/options.schema.json -d "tests/incremental/*/*.json"
+        run: ajv validate -s src/config/options.schema.json -d "tests/incremental/*/*.json"

.github/workflows/semgrep.yml

@@ -22,7 +22,7 @@ jobs:
         run: semgrep scan --config .semgrep/ --sarif > semgrep.sarif
 
       - name: Upload SARIF file to GitHub Advanced Security Dashboard
-        uses: github/codeql-action/upload-sarif@v2
+        uses: github/codeql-action/upload-sarif@v3
         with:
           sarif_file: semgrep.sarif
         if: always()

.gitignore

@@ -29,7 +29,6 @@ linux-headers
 .goblint*/
 goblint_temp_*/
 
-src/spec/graph
 .vagrant
 
 g2html.jar

.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/common/util/options.schema.json _readthedocs/html/jsfh/
+      - generate-schema-doc --config-file jsfh.yml src/config/options.schema.json _readthedocs/html/jsfh/

conf/ldv-races.json

@@ -29,7 +29,9 @@
       "escape",
       "expRelation",
       "mhp",
-      "assert"
+      "assert",
+      "var_eq",
+      "symb_locks"
     ],
     "malloc": {
       "wrappers": [
@@ -52,6 +54,19 @@
       ]
     }
   },
+  "lib": {
+    "activated": [
+      "c",
+      "posix",
+      "pthread",
+      "gcc",
+      "glibc",
+      "linux-userspace",
+      "goblint",
+      "ncurses",
+      "klever"
+    ]
+  },
   "witness": {
     "graphml": {
       "enabled": true,

conf/min-unsound.json

@@ -0,0 +1,6 @@
+{
+    "ana": {
+        "activated": [
+        ]
+    }
+}

docs/developer-guide/debugging.md

@@ -60,14 +60,14 @@ This will create a file called `goblint.byte`.
 ### Debugging Goblint with VS Code
 
 To debug OCaml programs, you can use the command line interface of `ocamldebug` or make use of the Visual Studio Code
-integration provided by `hackwaly.ocamlearlybird`.
+integration provided by `ocamllabs.ocaml-platform`.
 In the following, we describe the steps necessary to set up this VS Code extension to
 debug Goblint.
 
 ### Setting-up Earlybird
 
-Install the [`hackwaly.ocamlearlybird` extension](https://marketplace.visualstudio.com/items?itemName=hackwaly.ocamlearlybird) in your installation of Visual Studio Code.
-To be able to use this extension, you additionally need to install `ocamlearlybird` on the opam switch you use for Goblint.
+Install the [`ocamllabs.ocaml-platform` extension](https://marketplace.visualstudio.com/items?itemName=ocamllabs.ocaml-platform) in your installation of Visual Studio Code.
+To be able to use this extension, you additionally need to install `earlybird` on the opam switch you use for Goblint.
 To do so, run the following command in the `analyzer` directory:
 
 ```console
@@ -76,7 +76,7 @@ opam install earlybird
 
 ### Providing a Launch Configuration
 
-To let the `hackwaly.ocamlearlybird` extension know which executable it should debug, and which arguments it should pass, we have to provide a configuration file.
+To let the `ocamllabs.ocaml-platform` extension know which executable it should debug, and which arguments it should pass, we have to provide a configuration file.
 The configuration file has to be named `launch.json` and must reside in the `./.vscode` directory. Here is an example `launch.json`:
 
 ```JSON
@@ -92,6 +92,9 @@ The configuration file has to be named `launch.json` and must reside in the `./.
           "tests/regression/00-sanity/01-assert.c",
           "--enable", "ana.int.interval",
         ],
+        "env": {
+          "LD_LIBRARY_PATH": "$LD_LIBRARY_PATH:_build/default/src/common"
+        },
         "stopOnEntry": false,
       }
     ]

docs/developer-guide/messaging.md

@@ -18,7 +18,8 @@ A message consists of the following:
         3. **Context.** Optional. Currently completely abstract, so not very useful.
     * **Group.** For messages related to numerous locations with different texts. Contains the following:
         1. **Group text.** An overall description of the group message.
-        2. **Pieces.** A list of single messages as described above.
+        2. **Group location.** Optional. An overall location of the group message.
+        3. **Pieces.** A list of single messages as described above.
 
 ## Creating
 
@@ -47,16 +48,3 @@ The `~loc` argument is optional and defaults to the current location, but allows
 The `_noloc` suffixed functions allow general messages without any location (not even current).
 
 By convention, may-warnings (the usual case) should use warning severity and  must-warnings should use error severity.
-
-### Spec analysis
-
-Warnings inside `.spec` files are converted to warnings.
-They parsed from string warnings: the first space-delimited substring determines the category and the rest determines the text.
-
-For example:
-```
-w1 "behavior.undefined.use_after_free"
-w2 "integer.overflow"
-w3 "unknown my message"
-w4 "integer.overflow some text describing the warning"
-```

docs/developer-guide/releasing.md

@@ -70,7 +70,7 @@
 
     This is required such that the created archive would have everything in a single directory called `goblint`.
 
-4. Update SV-COMP year in `sv-comp/archive.sh`.
+4. Update SV-COMP year in `scripts/sv-comp/archive.sh`.
 
     This includes: git tag name, git tag message and zipped conf file.
 
@@ -83,9 +83,9 @@
 
 2. Make sure you have nothing valuable that would be deleted by `make clean`.
 3. Delete git tag from previous prerun: `git tag -d svcompXY`.
-4. Create archive: `./sv-comp/archive.sh`.
+4. Create archive: `./scripts/sv-comp/archive.sh`.
 
-    The resulting archive is `sv-comp/goblint.zip`.
+    The resulting archive is `scripts/sv-comp/goblint.zip`.
 
 5. Check unextracted archive in latest SV-COMP container image: <https://gitlab.com/sosy-lab/benchmarking/competition-scripts/#container-image>.
 

docs/user-guide/configuring.md

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

docs/user-guide/inspecting.md

@@ -23,3 +23,20 @@ To build GobView (also for development):
 `./_build/default/gobview/goblint-http-server/goblint_http.exe -with-goblint ../analyzer/goblint -goblint --set files[+] "../analyzer/tests/regression/00-sanity/01-assert.c"`
 
 4. Visit <http://localhost:8080>
+
+## Witnesses
+
+### GraphML
+
+#### yEd
+
+1. Open (Ctrl+o) `witness.graphml` from Goblint root directory.
+2. Click menu "Edit" → "Properties Mapper".
+    1. _First time:_  Click button "Imports additional configurations" and open `scripts/sv-comp/yed-sv-comp.cnfx`.
+    2. Select "SV-COMP (Node)" and click "Apply".
+    3. Select "SV-COMP (Edge)" and click "Ok".
+3. Click menu "Layout" → "Hierarchial" (Alt+shift+h).
+    1. _First time:_ Click tab "Labeling", select "Hierarchic" in "Edge Labeling".
+    2. Click "Ok".
+
+yEd manual for the Properties Mapper: <https://yed.yworks.com/support/manual/properties_mapper.html>.

docs/user-guide/running.md

@@ -67,3 +67,20 @@ Here is a list of issues and workarounds for different compilation database gene
 #### bear
 1. Bear 2.3.11 from Ubuntu 18.04 produces incomplete database (<https://github.com/goblint/bench/issues/7#issuecomment-1011055984>, <https://github.com/goblint/bench/issues/7#issuecomment-1011987188>).
     * Bear 3.0.8 seems fine.
+
+
+## SV-COMP
+The most up-to-date SV-COMP configuration is in `conf/svcomp.json`.
+There are also per-year configurations (e.g. `conf/svcomp24.json`) which try to reflect that year's submission using current option names.
+Due to unconfigurable changes (e.g. bug fixes) these do not _exactly_ behave as that year's submission.
+See SV-COMP submissions in GitHub releases for exact submitted versions.
+
+In SV-COMP Goblint is run as follows:
+```console
+./goblint --conf conf/svcomp.json --set ana.specification property.prp --set exp.architecture {32bit,64bit} input.c
+```
+
+Goblint YAML correctness witness validator is run as:
+```console
+./goblint --conf conf/svcomp.json --set ana.specification property.prp --set exp.architecture {32bit,64bit} --set witness.yaml.unassume witness.yml --set witness.yaml.validate witness.yml input.c
+```

dune-project

@@ -16,7 +16,7 @@
 (homepage "https://goblint.in.tum.de")
 (documentation "https://goblint.readthedocs.io/en/latest/")
 (authors "Simmo Saan" "Michael Schwarz" "Julian Erhard" "Sarah Tilscher" "Ralf Vogler" "Kalmer Apinis" "Vesal Vojdani" ) ; same authors as in .zenodo.json and CITATION.cff
-(maintainers "Simmo Saan <[email protected]>" "Michael Schwarz <[email protected]>")
+(maintainers "Simmo Saan <[email protected]>" "Michael Schwarz <[email protected]>" "Karoliine Holter")
 (license MIT)
 
 (package
@@ -25,7 +25,7 @@
   (depends
     (ocaml (>= 4.10))
     (goblint-cil (>= 2.0.3)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
-    (batteries (>= 3.5.0))
+    (batteries (>= 3.5.1))
     (zarith (>= 1.8))
     (yojson (>= 2.0.0))
     (qcheck-core (>= 0.19))

goblint.opam

@@ -4,6 +4,7 @@ synopsis: "Static analysis framework for C"
 maintainer: [
   "Simmo Saan <[email protected]>"
   "Michael Schwarz <[email protected]>"
+  "Karoliine Holter"
 ]
 authors: [
   "Simmo Saan"
@@ -22,7 +23,7 @@ depends: [
   "dune" {>= "3.7"}
   "ocaml" {>= "4.10"}
   "goblint-cil" {>= "2.0.3"}
-  "batteries" {>= "3.5.0"}
+  "batteries" {>= "3.5.1"}
   "zarith" {>= "1.8"}
   "yojson" {>= "2.0.0"}
   "qcheck-core" {>= "0.19"}

goblint.opam.locked

@@ -5,6 +5,7 @@ synopsis: "Static analysis framework for C"
 maintainer: [
   "Simmo Saan <[email protected]>"
   "Michael Schwarz <[email protected]>"
+  "Karoliine Holter"
 ]
 authors: [
   "Simmo Saan"

scripts/goblint-lib-modules.py

@@ -8,6 +8,7 @@
 
 goblint_lib_paths = [
     src_root_path / "goblint_lib.ml",
+    src_root_path / "solver" / "goblint_solver.ml",
     src_root_path / "util" / "std" / "goblint_std.ml",
 ]
 goblint_lib_modules = set()
@@ -30,20 +31,19 @@
     "MessagesCompare",
     "PrivPrecCompare",
     "ApronPrecCompare",
-    "Mainspec",
 
     # libraries
     "Goblint_std",
+    "Goblint_solver",
     "Goblint_timing",
     "Goblint_backtrace",
+    "Goblint_tracing",
     "Goblint_sites",
     "Goblint_build_info",
     "Dune_build_info",
 
     "MessageCategory", # included in Messages
     "PreValueDomain", # included in ValueDomain
-    "SpecCore", # spec stuff
-    "SpecUtil", # spec stuff
 
     "ConfigVersion",
     "ConfigProfile",
@@ -65,5 +65,5 @@
 
 missing_modules = src_modules - goblint_lib_modules
 if len(missing_modules) > 0:
-    print(f"Modules missing from {goblint_lib_path}: {missing_modules}")
+    print(f"Modules missing from {goblint_lib_paths[0]}: {missing_modules}")
     sys.exit(1)

scripts/regression2sv-benchmarks.py

@@ -31,7 +31,6 @@
     "09-regions_34-escape_rc", # duplicate of 04/45
     "09-regions_35-list2_rc-offsets-thread", # duplicate of 09/03
     "10-synch_17-glob_fld_nr", # duplicate of 05/08
-    "19-spec_02-mutex_rc", # duplicate of 04/01
 
     "29-svcomp_01-race-2_3b-container_of", # duplicate sv-benchmarks
     "29-svcomp_01-race-2_4b-container_of", # duplicate sv-benchmarks