Merge branch 'master' into delay-widening

goblint · Dec 20, 2024 · 92ee72f · 92ee72f
2 parents 2eca6d6 + e36e738
commit 92ee72f
Show file tree

Hide file tree

Showing 555 changed files with 18,014 additions and 9,605 deletions.
diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
@@ -37,3 +37,6 @@ c3e2cc848479ae86de5542b6ab0e75a74e9cf8c9
 
 # Fix LibraryFunctions.invalidate_actions indentation
 5662024232f32fe74dd25c9317dee4436ecb212d
+
+# Rename ctx -> man
+0c155e68607fede6fab17704a9a7aee38df5408e
diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
@@ -16,9 +16,9 @@ jobs:
       fail-fast: false
       matrix:
         os:
-          - ubuntu-latest
+          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}
@@ -35,13 +35,12 @@ jobs:
           # otherwise setup-ocaml pins non-locked dependencies
           # https://github.com/ocaml/setup-ocaml/issues/166
           OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
-        if: ${{ matrix.os == 'ubuntu-latest' }}
+        if: ${{ matrix.os == 'ubuntu-22.04' }}
         run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies

diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
@@ -59,7 +59,7 @@ jobs:
 
       - name: Build Docker image
         id: build
-        uses: docker/build-push-action@v5
+        uses: docker/build-push-action@v6
         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@v5
+        uses: docker/build-push-action@v6
         with:
           context: .
           push: true

diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -16,9 +16,9 @@ jobs:
     strategy:
       matrix:
         os:
-          - ubuntu-latest
+          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}
@@ -35,7 +35,7 @@ jobs:
           # otherwise setup-ocaml pins non-locked dependencies
           # https://github.com/ocaml/setup-ocaml/issues/166
           OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 

diff --git a/.github/workflows/indentation.yml b/.github/workflows/indentation.yml
@@ -10,7 +10,7 @@ jobs:
     strategy:
       matrix:
         os:
-          - ubuntu-latest
+          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
         ocaml-compiler:
           - 4.14.x
 
@@ -25,7 +25,7 @@ jobs:
           fetch-depth: 0
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 

diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
@@ -17,10 +17,10 @@ jobs:
       fail-fast: false
       matrix:
         os:
-          - ubuntu-latest
+          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
           - macos-13
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}
@@ -37,13 +37,12 @@ jobs:
           # otherwise setup-ocaml pins non-locked dependencies
           # https://github.com/ocaml/setup-ocaml/issues/166
           OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
-        if: ${{ matrix.os == 'ubuntu-latest' }}
+        if: ${{ matrix.os == 'ubuntu-22.04' }}
         run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
@@ -71,9 +70,9 @@ jobs:
       fail-fast: false
       matrix:
         os:
-          - ubuntu-latest
+          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}
@@ -87,13 +86,12 @@ jobs:
           # otherwise setup-ocaml pins non-locked dependencies
           # https://github.com/ocaml/setup-ocaml/issues/166
           OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
-        if: ${{ matrix.os == 'ubuntu-latest' }}
+        if: ${{ matrix.os == 'ubuntu-22.04' }}
         run: sudo apt install -y libgraph-easy-perl
 
       - name: Install spin
@@ -114,9 +112,9 @@ jobs:
       fail-fast: false
       matrix:
         os:
-          - ubuntu-latest
+          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
         node-version:
           - 14
@@ -132,7 +130,7 @@ jobs:
           # otherwise setup-ocaml pins non-locked dependencies
           # https://github.com/ocaml/setup-ocaml/issues/166
           OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 

diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
@@ -15,13 +15,13 @@ jobs:
       fail-fast: false
       matrix:
         os:
-          - ubuntu-latest
+          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
           - macos-13
         ocaml-compiler:
           - 5.2.x
           - 5.1.x
           - 5.0.x
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda
           - 4.14.x
         apron:
           - false
@@ -30,9 +30,11 @@ jobs:
           - false
 
         include:
-          - os: ubuntu-latest
+          - os: ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
             ocaml-compiler: 4.14.x
             z3: true
+          - os: macos-latest
+            ocaml-compiler: 4.14.x
 
     # customize name to use readable string for apron instead of just a boolean
     # workaround for missing ternary operator: https://github.com/actions/runner/issues/409
@@ -45,13 +47,12 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
-        if: ${{ matrix.os == 'ubuntu-latest' }}
+        if: ${{ matrix.os == 'ubuntu-22.04' }}
         run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
@@ -89,10 +90,10 @@ jobs:
       fail-fast: false
       matrix:
         os:
-          - ubuntu-latest
+          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
           - macos-13
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
 
     name: lower-bounds (${{ matrix.os }}, ${{ matrix.ocaml-compiler }}, downgrade)
 
@@ -109,10 +110,9 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
-        if: ${{ matrix.os == 'ubuntu-latest' }}
+        if: ${{ matrix.os == 'ubuntu-22.04' }}
         run: sudo apt install -y libgraph-easy-perl
 
       - name: Install dependencies
@@ -133,7 +133,7 @@ jobs:
       - name: Downgrade dependencies
         # must specify ocaml-base-compiler again to prevent it from being downgraded
         # prevent num downgrade to avoid dune/jbuilder error: https://github.com/ocaml/dune/issues/5280
-        run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.0+options ocaml-option-flambda num.1.5)
+        run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.2+options ocaml-option-flambda num.1.5)
 
       - name: Build
         run: ./make.sh nat
@@ -165,7 +165,7 @@ jobs:
 
       - name: Build dev Docker image
         id: build
-        uses: docker/build-push-action@v5
+        uses: docker/build-push-action@v6
         with:
           context: .
           target: dev
@@ -187,10 +187,10 @@ jobs:
       fail-fast: false
       matrix:
         os:
-          - ubuntu-latest
+          - ubuntu-22.04 # https://github.com/ocaml/setup-ocaml/issues/872
           - macos-13
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
 
     runs-on: ${{ matrix.os }}
 
@@ -199,13 +199,12 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
-        if: ${{ matrix.os == 'ubuntu-latest' }}
+        if: ${{ matrix.os == 'ubuntu-22.04' }}
         run: sudo apt install -y libgraph-easy-perl
 
       - name: Install Goblint with test

diff --git a/.semgrep/fold.yml b/.semgrep/fold.yml
@@ -0,0 +1,26 @@
+rules:
+  - id: fold-exists
+    patterns:
+      - pattern-either:
+        - pattern: $D.fold ... false
+        - pattern: $D.fold_left ... false
+        - pattern: $D.fold_right ... false
+        - pattern: fold ... false
+        - pattern: fold_left ... false
+        - pattern: fold_right ... false
+    message: consider replacing fold with exists
+    languages: [ocaml]
+    severity: WARNING
+
+  - id: fold-for_all
+    patterns:
+      - pattern-either:
+        - pattern: $D.fold ... true
+        - pattern: $D.fold_left ... true
+        - pattern: $D.fold_right ... true
+        - pattern: fold ... true
+        - pattern: fold_left ... true
+        - pattern: fold_right ... true
+    message: consider replacing fold with for_all
+    languages: [ocaml]
+    severity: WARNING
diff --git a/.semgrep/tracing.yml b/.semgrep/tracing.yml
@@ -8,8 +8,16 @@ rules:
         - pattern: Messages.tracec
         - pattern: Messages.traceu
         - pattern: Messages.traceli
+        - pattern: M.trace
+        - pattern: M.tracel
+        - pattern: M.tracei
+        - pattern: M.tracec
+        - pattern: M.traceu
+        - pattern: M.traceli
       - pattern-not-inside: if Messages.tracing then ...
       - pattern-not-inside: if Messages.tracing && ... then ...
+      - pattern-not-inside: if M.tracing then ...
+      - pattern-not-inside: if M.tracing && ... then ...
     message: trace functions should only be called if tracing is enabled at compile time
     languages: [ocaml]
     severity: WARNING
diff --git a/.zenodo.json b/.zenodo.json
@@ -23,6 +23,11 @@
       "affiliation": "Technische Universität München",
       "orcid": "0009-0009-9644-7475"
     },
+    {
+      "name": "Holter, Karoliine",
+      "affiliation": "University of Tartu",
+      "orcid": "0009-0008-3725-4131"
+    },
     {
       "name": "Vogler, Ralf",
       "affiliation": "Technische Universität München"

diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,3 +1,33 @@
+## v2.5.0
+Functionally equivalent to Goblint in SV-COMP 2025.
+
+* Add 32bit vs 64bit architecture support (#54, #1574).
+* Add per-function context gas analysis (#1569, #1570, #1598).
+* Adapt automatic static loop unrolling (#1516, #1582, #1583, #1584, #1590, #1595, #1599).
+* Adapt automatic configuration tuning (#1450, #1612, #1181, #1604).
+* Simplify non-relational integer invariants in witnesses (#1517).
+* Fix excessive hash collisions (#1594, #1602).
+* Clean up various code (#1095, #1523, #1554, #1575, #1588, #1597, #1614).
+
+## v2.4.0
+* Remove unmaintained analyses: spec, file (#1281).
+* Add linear two-variable equalities analysis (#1297, #1412, #1466).
+* Add callstring, loopfree callstring and context gas analyses (#1038, #1340, #1379, #1427, #1439).
+* Add non-relational thread-modular value analyses with thread IDs (#1366, #1398, #1399).
+* Add NULL byte array domain (#1076).
+* Fix spurious overflow warnings from internal evaluations (#1406, #1411, #1511).
+* Refactor non-definite mutex handling to fix unsoundness (#1430, #1500, #1503, #1409).
+* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (#1457, #1458).
+* Fix mutex type analysis unsoundness and enable it by default (#1414, #1416, #1510).
+* Add points-to set refinement on mutex path splitting (#1287, #1343, #1374, #1396, #1407).
+* Improve narrowing operators (#1502, #1540, #1543).
+* Extract automatic configuration tuning for soundness (#1469).
+* Fix many locations in witnesses (#1355, #1372, #1400, #1403).
+* Improve output readability (#1294, #1312, #1405, #1497).
+* Refactor logging (#1117).
+* Modernize all library function specifications (#1029, #688, #1174, #1289, #1447, #1487).
+* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (#1448).
+
 ## v2.3.0
 Functionally equivalent to Goblint in SV-COMP 2024.
 

diff --git a/CITATION.cff b/CITATION.cff
@@ -21,6 +21,10 @@ authors: # same authors as in .zenodo.json and dune-project
     family-names: Tilscher
     affiliation: "Technische Universität München"
     orcid: "https://orcid.org/0009-0009-9644-7475"
+  - given-names: Karoliine
+    family-names: Holter
+    affiliation: "University of Tartu"
+    orcid: "https://orcid.org/0009-0008-3725-4131"
   - given-names: Ralf
     family-names: Vogler
     affiliation: "Technische Universität München"

diff --git a/bench/basic/benchSet.ml b/bench/basic/benchSet.ml
@@ -73,7 +73,7 @@ let () =
         ]
       );
       "const" @> lazy (
-        let args = ((fun x -> 42), set1) in
+        let args = ((fun _ -> 42), set1) in
         throughputN 1 [
           ("map1", map1, args);
           ("map2", map2, args);