Merge branch 'master' into klever

.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/

docs/developer-guide/messaging.md

@@ -47,16 +47,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

@@ -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

@@ -22,7 +22,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"}

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",

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

sv-comp/archive.sh → scripts/sv-comp/archive.sh

@@ -23,9 +23,9 @@ wget -O lib/LICENSE.APRON https://raw.githubusercontent.com/antoinemine/apron/ma
 # done outside to ensure archive contains goblint/ directory
 cd ..
 
-rm goblint/sv-comp/goblint.zip
+rm goblint/scripts/sv-comp/goblint.zip
 
-zip goblint/sv-comp/goblint.zip \
+zip goblint/scripts/sv-comp/goblint.zip \
     goblint/goblint \
     goblint/lib/libapron.so \
     goblint/lib/liboctD.so \

src/analyses/accessAnalysis.ml

@@ -29,7 +29,7 @@ struct
   let init _ =
     collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed";
     let activated = get_string_list "ana.activated" in
-    emit_single_threaded := List.mem (ModifiedSinceLongjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
+    emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
 
   let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (kind:AccessKind.t) (reach:bool) (e:exp) =
     if M.tracing then M.trace "access" "do_access %a %a %B\n" d_exp e AccessKind.pretty kind reach;

src/analyses/apron/affineEqualityAnalysis.apron.ml

@@ -11,7 +11,6 @@ let spec_module: (module MCPSpec) Lazy.t =
     let module AD = AffineEqualityDomain.D2 (VectorMatrix.ArrayVector) (VectorMatrix.ArrayMatrix) in
     let module RD: RelationDomain.RD =
     struct
-      module Var = AffineEqualityDomain.Var
       module V = AffineEqualityDomain.V
       include AD
     end

src/analyses/apron/apronAnalysis.apron.ml

@@ -12,10 +12,9 @@ let spec_module: (module MCPSpec) Lazy.t =
     let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): ApronDomain.S3) else (module AD)) in
     let module RD: RelationDomain.RD =
     struct
-      module Var = ApronDomain.Var
       module V = ApronDomain.V
       include AD
-      type var = ApronDomain.Var.t
+      type var = Apron.Var.t
     end
     in
     let module Priv = (val RelationPriv.get_priv ()) in