Merge branch 'master' into term

goblint · Oct 3, 2023 · 664cde9 · 664cde9
2 parents a6e4af4 + 7e57562
commit 664cde9
Show file tree

Hide file tree

Showing 237 changed files with 5,502 additions and 1,538 deletions.
diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
@@ -28,7 +28,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:

diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
@@ -35,21 +35,21 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
+        uses: docker/setup-buildx-action@v3 # needed for GitHub Actions Cache in build-push-action
 
       - name: Log in to the Container registry
-        uses: docker/login-action@v2
+        uses: docker/login-action@v3
         with:
           registry: ${{ env.REGISTRY }}
           username: ${{ github.actor }}
           password: ${{ secrets.GITHUB_TOKEN }}
 
       - name: Extract metadata (tags, labels) for Docker
         id: meta
-        uses: docker/metadata-action@v4
+        uses: docker/metadata-action@v5
         with:
           images: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}
           tags: |
@@ -59,7 +59,7 @@ jobs:
 
       - name: Build Docker image
         id: build
-        uses: docker/build-push-action@v4
+        uses: docker/build-push-action@v5
         with:
           context: .
           load: true # load into docker instead of immediately pushing
@@ -72,7 +72,7 @@ jobs:
         run: docker run --rm -v $(pwd):/data ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ steps.meta.outputs.version }} /data/tests/regression/04-mutex/01-simple_rc.c # run image by version in case multiple tags
 
       - name: Push Docker image
-        uses: docker/build-push-action@v4
+        uses: docker/build-push-action@v5
         with:
           context: .
           push: true

diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -30,7 +30,10 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
+
+      - name: Check for undocumented modules
+        run: python scripts/goblint-lib-modules.py
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:

diff --git a/.github/workflows/indentation.yml b/.github/workflows/indentation.yml
@@ -20,7 +20,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           fetch-depth: 0
 

diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
@@ -30,7 +30,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -104,7 +104,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:
@@ -144,7 +144,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         env:

diff --git a/.github/workflows/metadata.yml b/.github/workflows/metadata.yml
@@ -19,7 +19,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Validate CITATION.cff
         uses: docker://citationcff/cffconvert:latest
@@ -36,7 +36,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
         uses: actions/setup-node@v3

diff --git a/.github/workflows/options.yml b/.github/workflows/options.yml
@@ -15,7 +15,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Node.js ${{ matrix.node-version }}
         uses: actions/setup-node@v3

diff --git a/.github/workflows/semgrep.yml b/.github/workflows/semgrep.yml
@@ -16,10 +16,10 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Run semgrep
-        run: semgrep scan --sarif --output=semgrep.sarif
+        run: semgrep scan --config .semgrep/ --sarif > semgrep.sarif
 
       - name: Upload SARIF file to GitHub Advanced Security Dashboard
         uses: github/codeql-action/upload-sarif@v2

diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
@@ -18,6 +18,7 @@ jobs:
           - ubuntu-latest
           - macos-latest
         ocaml-compiler:
+          - 5.0.x
           - ocaml-variants.4.14.0+options,ocaml-option-flambda
           - 4.14.x
           - 4.13.x
@@ -45,7 +46,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2
@@ -131,7 +132,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2
@@ -208,14 +209,14 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
+        uses: docker/setup-buildx-action@v3 # needed for GitHub Actions Cache in build-push-action
 
       - name: Build dev Docker image
         id: build
-        uses: docker/build-push-action@v4
+        uses: docker/build-push-action@v5
         with:
           context: .
           target: dev
@@ -246,7 +247,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2

diff --git a/.semgrep/tracing.yml b/.semgrep/tracing.yml
@@ -9,6 +9,7 @@ rules:
         - pattern: Messages.traceu
         - pattern: Messages.traceli
       - pattern-not-inside: if Messages.tracing then ...
+      - pattern-not-inside: if Messages.tracing && ... then ...
     message: trace functions should only be called if tracing is enabled at compile time
     languages: [ocaml]
     severity: WARNING
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,3 +1,27 @@
+## v2.2.1
+* Bump batteries lower bound to 3.5.0.
+* Fix flaky dead code elimination transformation test.
+
+## v2.2.0
+* Add `setjmp`/`longjmp` analysis (#887, #970, #1015, #1019).
+* Refactor race analysis to lazy distribution (#1084, #1089, #1136, #1016).
+* Add thread-unsafe library function call analysis (#723, #1082).
+* Add mutex type analysis and mutex API analysis (#800, #839, #1073).
+* Add interval set domain and string literals domain (#901, #966, #994, #1048).
+* Add affine equalities analysis (#592).
+* Add use-after-free analysis (#1050, #1114).
+* Add dead code elimination transformation (#850, #979).
+* Add taint analysis for partial contexts (#553, #952).
+* Add YAML witness validation via unassume (#796, #977, #1044, #1045, #1124).
+* Add incremental analysis rename detection (#774, #777).
+* Fix address sets unsoundness (#822, #967, #564, #1032, #998, #1031).
+* Fix thread escape analysis unsoundness (#939, #984, #1074, #1078).
+* Fix many incremental analysis issues (#627, #836, #835, #841, #932, #678, #942, #949, #950, #957, #955, #954, #960, #959, #1004, #558, #1010, #1091).
+* Fix server mode for abstract debugging (#983, #990, #997, #1000, #1001, #1013, #1018, #1017, #1026, #1027).
+* Add documentation for configuration JSON schema and OCaml API (#999, #1054, #1055, #1053).
+* Add many library function specifications (#962, #996, #1028, #1079, #1121, #1135, #1138).
+* Add OCaml 5.0 support (#1003, #945, #1162).
+
 ## v2.1.0
 Functionally equivalent to Goblint in SV-COMP 2023.
 

diff --git a/README.md b/README.md
@@ -13,6 +13,7 @@ Documentation can be browsed on [Read the Docs](https://goblint.readthedocs.io/e
 
 ## Installing
 Both for using an up-to-date version of Goblint or developing it, the best way is to install from source by cloning this repository.
+For benchmarking Goblint, please follow the [Benchmarking guide on Read the Docs](https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/).
 
 ### Linux
 1. Install [opam](https://opam.ocaml.org/doc/Install.html).

diff --git a/conf/bench-yaml-validate.json b/conf/bench-yaml-validate.json
@@ -52,14 +52,6 @@
       "tokens": true
     }
   },
-  "witness": {
-    "enabled": false,
-    "invariant": {
-      "loop-head": true,
-      "after-lock": true,
-      "other": false
-    }
-  },
   "sem": {
     "unknown_function": {
       "invalidate": {

diff --git a/conf/bench-yaml.json b/conf/bench-yaml.json
@@ -48,20 +48,6 @@
       ]
     }
   },
-  "witness": {
-    "enabled": false,
-    "yaml": {
-      "enabled": true
-    },
-    "invariant": {
-      "exact": false,
-      "exclude-vars": [
-        "tmp\\(___[0-9]+\\)?",
-        "cond",
-        "RETURN"
-      ]
-    }
-  },
   "sem": {
     "unknown_function": {
       "invalidate": {

diff --git a/conf/svcomp-yaml-validate.json b/conf/svcomp-yaml-validate.json
@@ -12,6 +12,10 @@
     "float": {
       "interval": true
     },
+    "apron": {
+      "domain": "polyhedra",
+      "strengthening": true
+    },
     "activated": [
       "base",
       "threadid",
@@ -31,6 +35,7 @@
       "region",
       "thread",
       "threadJoins",
+      "apron",
       "unassume"
     ],
     "context": {
@@ -74,14 +79,6 @@
   "exp": {
     "region-offsets": true
   },
-  "witness": {
-    "enabled": false,
-    "invariant": {
-      "loop-head": true,
-      "after-lock": false,
-      "other": false
-    }
-  },
   "solver": "td3",
   "sem": {
     "unknown_function": {

diff --git a/conf/svcomp-yaml.json b/conf/svcomp-yaml.json
@@ -12,6 +12,10 @@
     "float": {
       "interval": true
     },
+    "apron": {
+      "domain": "polyhedra",
+      "strengthening": true
+    },
     "activated": [
       "base",
       "threadid",
@@ -30,7 +34,8 @@
       "symb_locks",
       "region",
       "thread",
-      "threadJoins"
+      "threadJoins",
+      "apron"
     ],
     "context": {
       "widen": false
@@ -76,6 +81,9 @@
       "enabled": true
     },
     "invariant": {
+      "loop-head": true,
+      "other": false,
+      "accessed": false,
       "exact": false,
       "exclude-vars": [
         "tmp\\(___[0-9]+\\)?",

diff --git a/docs/developer-guide/releasing.md b/docs/developer-guide/releasing.md
@@ -45,13 +45,20 @@
     10. Check that analysis works: `goblint -v tests/regression/04-mutex/01-simple_rc.c`.
     11. Exit Docker container.
 
-12. Create a GitHub release with the git tag: `DUNE_RELEASE_DELEGATE=github-dune-release-delegate dune-release publish distrib`.
+12. Temporarily enable Zenodo GitHub webhook.
+
+    This is because we only want numbered version releases to automatically add a new version to our Zenodo artifact.
+    Other tags (like SV-COMP or paper artifacts) have manually created Zenodo artifacts anyway and thus shouldn't add new versions to the main Zenodo artifact.
+
+13. Create a GitHub release with the git tag: `DUNE_RELEASE_DELEGATE=github-dune-release-delegate dune-release publish distrib`.
 
     Explicitly specify `distrib` because we don't want to publish OCaml API docs.
     Environment variable workaround for the package having a Read the Docs `doc` URL (see <https://github.com/ocamllabs/dune-release/issues/154>).
 
-13. Create an opam package: `dune-release opam pkg`.
-14. Submit the opam package to opam-repository: `dune-release opam submit`.
+14. Re-disable Zenodo GitHub webhook.
+
+15. Create an opam package: `dune-release opam pkg`.
+16. Submit the opam package to opam-repository: `dune-release opam submit`.
 
 
 ## SV-COMP
@@ -104,15 +111,9 @@
 ### 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.
+2. Create GitHub release from the git tag and attach latest submitted archive as a download.
+3. 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.
+4. Release new semver version on opam. See above.