Merge branch 'master' into issue_718

Author: michael-schwarz

.github/workflows/locked.yml

@@ -67,6 +67,9 @@ jobs:
       - name: Test incremental regression
         run: ruby scripts/update_suite.rb -i
 
+      - name: Test incremental regression with cfg comparison
+        run: ruby scripts/update_suite.rb -c
+
   extraction:
     if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
 

.github/workflows/unlocked.yml

@@ -95,6 +95,9 @@ jobs:
       - name: Test incremental regression
         run: ruby scripts/update_suite.rb -i
 
+      - name: Test incremental regression with cfg comparison
+        run: ruby scripts/update_suite.rb -c
+
   lower-bounds-downgrade:
     # use external 0install solver to downgrade: https://github.com/ocaml-opam/opam-0install-solver
     # TODO: will be built in in opam 2.2: https://github.com/ocaml/opam/pull/4909
@@ -174,6 +177,9 @@ jobs:
       - name: Test incremental regression
         run: ruby scripts/update_suite.rb -i
 
+      - name: Test incremental regression with cfg comparison
+        run: ruby scripts/update_suite.rb -c
+
   lower-bounds-docker:
     # use builtin-0install solver to remove and downgrade, opam normally compiled without, Docker images have it compiled
 
@@ -265,3 +271,6 @@ jobs:
 
       - name: Test incremental regression
         run: ruby scripts/update_suite.rb -i
+
+      - name: Test incremental regression with cfg comparison
+        run: ruby scripts/update_suite.rb -c

.gitignore

@@ -87,3 +87,6 @@ gobview_out/*
 # witnesses
 witness.yml
 witness.certificate.yml
+
+# transformations
+transformed.c

CHANGELOG.md

@@ -1,3 +1,12 @@
+## v2.1.0
+Functionally equivalent to Goblint in SV-COMP 2023.
+
+* Add automatic configuration tuning (#772).
+* Add many library function specifications (#865, #868, #878, #884, #886).
+* Reorganize library stubs (#814, #845).
+* Add Trace Event Format output to timing (#844).
+* Optimize domains for address and path sets (#803, #809).
+
 ## v2.0.1
 * Fix compilation with z3.
 

README.md

@@ -12,18 +12,18 @@ Both for using an up-to-date version of Goblint or developing it, the best way i
 
 ### Linux
 1. Install [opam](https://opam.ocaml.org/doc/Install.html).
-2. Make sure the following are installed: `git patch m4 autoconf libgmp-dev libmpfr-dev pkg-config`.
+2. Make sure the following are installed: `git`, `patch`, `m4`, `autoconf`, `libgmp-dev`, `libmpfr-dev` and `pkg-config`.
 3. Run `make setup` to install OCaml and dependencies via opam.
 4. Run `make` to build Goblint itself.
 5. Run `make install` to install Goblint into the opam switch for usage via switch's `PATH`.
 
 ### MacOS
 1. Install GCC with `brew install gcc` (first run `xcode-select --install` if you don't want to build it from source). Goblint requires GCC while macOS's default `cpp` is Clang, which will not work.
 2. ONLY for M1 (ARM64) processor: homebrew changed its install location from `/usr/local/` to `/opt/homebrew/`. For packages to find their dependecies execute `sudo ln -s /opt/homebrew/{include,lib} /usr/local/`.
-3. Continue using Linux instructions (the formulae in brew for `patch libgmp-dev libmpfr-dev` are `gpatch gmp mpfr`, respectively).
+3. Continue using Linux instructions (the formulae in brew for `patch`, `libgmp-dev`, `libmpfr-dev` are `gpatch`, `gmp`, `mpfr`, respectively).
 
 ### Windows
-1. Install [WSL](https://docs.microsoft.com/en-us/windows/wsl/install-win10).
+1. Install [WSL2](https://docs.microsoft.com/en-us/windows/wsl/install-win10). Goblint is not compatible with WSL1.
 2. Continue using Linux instructions in WSL.
 
 ### Other

conf/svcomp.json

@@ -9,6 +9,9 @@
       "enums": false,
       "interval": true
     },
+    "float": {
+      "interval": true
+    },
     "activated": [
       "base",
       "threadid",
@@ -21,12 +24,13 @@
       "race",
       "escape",
       "expRelation",
-      "assert",
       "mhp",
+      "assert",
       "var_eq",
       "symb_locks",
       "region",
-      "thread"
+      "thread",
+      "threadJoins"
     ],
     "context": {
       "widen": false
@@ -55,6 +59,19 @@
       "arrays": {
         "domain": "partitioned"
       }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic"
+      ]
     }
   },
   "exp": {

conf/svcomp23.json

@@ -29,7 +29,8 @@
       "var_eq",
       "symb_locks",
       "region",
-      "thread"
+      "thread",
+      "threadJoins"
     ],
     "context": {
       "widen": false
@@ -66,9 +67,10 @@
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",
-        "arrayDomain",
+        "congruence",
         "octagon",
-        "wideningThresholds"
+        "wideningThresholds",
+        "loopUnrollHeuristic"
       ]
     }
   },

docs/developer-guide/developing.md

@@ -1,6 +1,8 @@
 # Developing
 
-Running `make dev` does the following:
+For development, Goblint must be installed from source: <https://github.com/goblint/analyzer#installing>.
+
+Then running `make dev` does the following:
 
 1. Installs some additional opam packages useful for developing.
 2. Installs a Git pre-commit hook for ocp-indent (see below).

docs/developer-guide/releasing.md

@@ -1,5 +1,7 @@
 # Releasing
 
+## opam
+
 1. Update list of authors and contributors in `.zenodo.json`, `CITATION.cff` and `dune-project`.
 2. Update `CHANGELOG.md`:
 
@@ -36,7 +38,7 @@
     3. Run Docker container in extracted directory: `docker run -it --rm -v $(pwd):/goblint ocaml/opam:ubuntu-22.04-ocaml-4.14` (or newer).
     4. Navigate to distribution archive inside Docker container: `cd /goblint`.
     5. Pin package from distribution archive: `opam pin add --no-action .`.
-    6. Install depexts: `opam depext goblint`.
+    6. Install depexts: `opam depext --with-test goblint`.
     7. Install and test package: `opam install --with-test goblint`.
     8. Activate opam environment: `eval $(opam env)`.
     9. Check version: `goblint --version`.
@@ -50,3 +52,67 @@
 
 13. Create an opam package: `dune-release opam pkg`.
 14. Submit the opam package to opam-repository: `dune-release opam submit`.
+
+
+## SV-COMP
+
+### Before all preruns
+
+1. Make sure you are running the same Ubuntu version as will be used for SV-COMP.
+2. Create conf file for SV-COMP year.
+3. Make sure this repository is checked out into a directory called `goblint`, not the default `analyzer`.
+
+    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`.
+
+    This includes: git tag name, git tag message and zipped conf file.
+
+### For each prerun
+
+1. Update opam pins:
+
+    1. Make sure you have the same `goblint-cil` version pinned as `goblint.opam` specifies.
+    2. Unpin `zarith.1.12-gob0`, because Gobview compatibility is not required.
+
+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`.
+
+    The resulting archive is `sv-comp/goblint.zip`.
+
+5. Check unextracted archive in latest SV-COMP container image: <https://gitlab.com/sosy-lab/benchmarking/competition-scripts/#container-image>.
+
+    Inside Docker:
+
+    1. Check version: `./goblint --version`.
+    2. Mount some sv-benchmarks and properties, e.g. as `/tool-test`, and run Goblint on them manually.
+
+    This ensures that the environment and the archive have all the correct system libraries.
+
+6. Commit and push the archive to an SV-COMP archives repository branch (but don't open a MR yet): <https://gitlab.com/sosy-lab/sv-comp/archives-2023#sparse-checkout> (SV-COMP 2023).
+7. Check pushed archive via CoveriTeam-Remote: <https://gitlab.com/sosy-lab/software/coveriteam/-/blob/main/doc/competition-help.md>.
+
+    1. Clone coveriteam repository.
+    2. Locally modify `actors/goblint.yml` archive location to the raw URL of the pushed archive.
+    3. Run Goblint on some sv-benchmarks and properties via CoveriTeam.
+
+    This ensures that Goblint runs on SoSy-Lab servers.
+
+8. Open MR to the SV-COMP archives repository.
+
+### After all preruns
+
+1. Push git tag from last prerun: `git push origin svcompXY`.
+2. Temporarily disable Zenodo webhook.
+
+    This is because we don't want a new out-of-place version of Goblint in our Zenodo artifact.
+    A separate Zenodo artifact for the SV-COMP version can be created later if tool paper is submitted.
+
+3. Create GitHub release from the git tag and attach latest submitted archive as a download.
+4. Manually run `docker` workflow on `svcompXY` git tag and targeting `svcompXY` Docker tag.
+
+    This is because the usual `docker` workflow only handles semver releases.
+
+5. Re-enable Zenodo webhook.
+6. Release new semver version on opam. See above.

docs/developer-guide/testing.md

@@ -33,7 +33,8 @@ incrementally (activating the option `incremental.load`) with some changes to th
 configuration. The respective `asserts` and expected results are checked in both runs.
 
 ### Running
-The incremental tests can be run with `./scripts/update_suite.rb -i`.
+The incremental tests can be run with `./scripts/update_suite.rb -i`. With `./scripts/update_suite.rb -c` the
+incremental tests are run using the more fine-grained cfg-based change detection.
 
 ### Writing
 An incremental test case consists of three files with the same file name: the `.c` file with the initial program, a