Merge branch 'master' into yaml-witness-ghost

goblint · Jul 31, 2024 · 1570adb · 1570adb
2 parents 7fcb10c + a592680
commit 1570adb
Show file tree

Hide file tree

Showing 104 changed files with 1,896 additions and 642 deletions.
diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
@@ -18,7 +18,7 @@ jobs:
         os:
           - ubuntu-latest
         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,10 +35,9 @@ 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' }}

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
@@ -18,7 +18,7 @@ jobs:
         os:
           - ubuntu-latest
         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
@@ -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
@@ -20,7 +20,7 @@ jobs:
           - ubuntu-latest
           - 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,10 +37,9 @@ 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' }}
@@ -73,7 +72,7 @@ jobs:
         os:
           - ubuntu-latest
         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,10 +86,9 @@ 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' }}
@@ -116,7 +114,7 @@ jobs:
         os:
           - ubuntu-latest
         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
@@ -21,7 +21,7 @@ jobs:
           - 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
@@ -45,10 +45,9 @@ 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' }}
@@ -92,7 +91,7 @@ jobs:
           - ubuntu-latest
           - 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,7 +108,6 @@ 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' }}
@@ -133,7 +131,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 +163,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
@@ -190,7 +188,7 @@ jobs:
           - ubuntu-latest
           - 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,10 +197,9 @@ 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' }}

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/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/conf/examples/medium-program.json b/conf/examples/medium-program.json
@@ -9,6 +9,7 @@
       "base",
       "threadid",
       "threadflag",
+      "threadreturn",
       "mallocWrapper",
       "mutexEvents",
       "mutex",
@@ -18,6 +19,7 @@
       "expRelation",
       "mhp",
       "assert",
+      "pthreadMutexType",
       "var_eq",
       "symb_locks",
       "region",

diff --git a/conf/examples/very-precise.json b/conf/examples/very-precise.json
@@ -22,6 +22,7 @@
       "base",
       "threadid",
       "threadflag",
+      "threadreturn",
       "mallocWrapper",
       "mutexEvents",
       "mutex",
@@ -31,6 +32,7 @@
       "expRelation",
       "mhp",
       "assert",
+      "pthreadMutexType",
       "var_eq",
       "symb_locks",
       "region",

diff --git a/docs/developer-guide/firstanalysis.md b/docs/developer-guide/firstanalysis.md
@@ -35,7 +35,7 @@ This program is in the Goblint repository: `tests/regression/99-tutorials/01-fir
 But if you run Goblint out of the box on this example, it will not work:
 
 ```console
-./goblint --enable warn.debug tests/regression/99-tutorials/01-first.c
+./goblint tests/regression/99-tutorials/01-first.c
 ```
 
 This will claim that the assertion in unknown.
@@ -74,10 +74,10 @@ For more information on the signature of the individual transfer functions, plea
 ## Extending the domain
 
 You could now enrich the lattice to also have a representation for non-negative (i.e., zero or positive) values.
-Then the join of `Zero` and `Pos` would be "non-negative" instead of `Top`, allowing you to prove that such join is greated than `Neg`.
+Then the join of `Zero` and `Pos` would be "non-negative" instead of `Top`, allowing you to prove that such join is greater than `Neg`.
 For example, have a look at the following program: `tests/regression/99-tutorials/02-first-extend.c`.
 
 _Hint:_
 The easiest way to do this is to use the powerset lattice of `{-, 0, +}`.
 For example, "non-negative" is represented by `{0, +}`, while negative is represented by `{-}`.
-To do this, modify `SL` by using `SetDomain.FiniteSet` (takes a `struct` with a list of finite elements as second parameter) instead of `Lattice.Flat` and reimplementing the two functions using `singleton` and `for_all`.
+To do this, modify `SL` by using `SetDomain.FiniteSet` (which needs a finite list of elements to be added to `Signs`) instead of `Lattice.Flat` and reimplementing the two functions using `singleton` and `for_all`.
diff --git a/docs/user-guide/assumptions.md b/docs/user-guide/assumptions.md
@@ -17,3 +17,22 @@ _NB! This list is likely incomplete._
 
     See [PR #1414](https://github.com/goblint/analyzer/pull/1414).
 
+2.  Pointer arithmetic does not overflow.
+
+    [C11's N1570][n1570] at 6.5.6.8 states that
+
+    > When an expression that has integer type is added to or subtracted from a pointer, the result has the type of the pointer operand.
+    > [...]
+    > the evaluation shall not produce an overflow; otherwise, the behavior is undefined.
+
+    after a long list of defined behaviors.
+
+    Goblint does not report overflow and out-of-bounds pointer arithmetic (when the pointer _is not dereferenced_).
+    This affects the overflow analysis (SV-COMP no-overflow property) in the `base` analysis.
+
+    This _does not_ affect the `memOutOfBounds` analysis (SV-COMP valid-memsafety property), which is for undefined behavior from _dereferencing_ such out-of-bounds pointers.
+
+    See [PR #1511](https://github.com/goblint/analyzer/pull/1511).
+
+
+[n1570]: https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf
diff --git a/dune-project b/dune-project
@@ -15,21 +15,34 @@
 (source (github goblint/analyzer))
 (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
+(authors "Simmo Saan" "Michael Schwarz" "Julian Erhard" "Sarah Tilscher" "Karoliine Holter" "Ralf Vogler" "Kalmer Apinis" "Vesal Vojdani" ) ; same authors as in .zenodo.json and CITATION.cff
 (maintainers "Simmo Saan <[email protected]>" "Michael Schwarz <[email protected]>" "Karoliine Holter")
 (license MIT)
 
 (package
   (name goblint)
   (synopsis "Static analysis framework for C")
+  (description "\
+Goblint is a sound static analysis framework for C programs using abstract interpretation.
+It specializes in thread-modular verification of multi-threaded programs, especially regarding data races.
+Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses.
+")
+  (tags (
+    "program analysis"
+    "program verification"
+    "static analysis"
+    "abstract interpretation"
+    "C"
+    "data race analysis"
+    "concurrency"))
   (depends
     (ocaml (>= 4.14))
     (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.1))
     (zarith (>= 1.10))
     (yojson (>= 2.0.0))
     (qcheck-core (>= 0.19))
-    ppx_deriving
+    (ppx_deriving (>= 6.0.2))
     (ppx_deriving_hash (>= 0.1.2))
     (ppx_deriving_yojson (>= 3.7.0))
     (ounit2 :with-test)
@@ -54,7 +67,7 @@
     conf-gcc ; ensures opam-repository CI installs real gcc from homebrew on MacOS
   )
   (depopts
-    apron
+    (apron (>= v0.9.15))
     z3
   )
   (conflicts