Merge branch 'goblint:master' into null-byte-arrayDomain

goblint · Sep 18, 2023 · bb373d2 · bb373d2
2 parents a0a501c + 3666c92
commit bb373d2
Show file tree

Hide file tree

Showing 77 changed files with 1,627 additions and 636 deletions.
diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
@@ -38,18 +38,18 @@ jobs:
         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/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
@@ -211,11 +212,11 @@ jobs:
         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

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/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.
diff --git a/docs/user-guide/benchmarking.md b/docs/user-guide/benchmarking.md
@@ -1,6 +1,31 @@
 # Benchmarking
+The following best practices should be followed when benchmarking Goblint.
+This is to ensure valid, reproducible and representative benchmarking results.
 
-To achieve reproducible builds and the best performance for benchmarking, it is recommended to compile Goblint using the `release` option:
+# External benchmarking
+External users should choose the version of Goblint to evaluate or benchmark as follows:
+
+1. Use the newest version release.
+
+    The version from git `master` branch or any other intermediate git commit come without any guarantees.
+    They are bleeding-edge and haven't gone through validation like the version releases.
+
+    SV-COMP releases are highly preferable since they've gone through rigorous validation in SV-COMP.
+
+2. Download the corresponding version from a Zenodo artifact or by checking out the respective git tag. **Do not install directly from opam repository!**
+
+    Goblint pins optimized versions of some dependencies which cannot be done on the opam repository releases.
+    Thus, using the latter would yield unrepresentative results.
+
+    Zenodo artifacts come with DOIs, which make them ideal for citation.
+
+3. Use OCaml 4.14. **Do not use OCaml 5!**
+
+    OCaml 5 has significant performance regressions, which yield unrepresentative benchmarking results.
+    Goblint's `make setup` installs the correct OCaml version into a new opam switch.
+
+# Release build
+To achieve the best performance for benchmarking, Goblint should be compiled using the `release` option:
 
 ```sh
 make release

diff --git a/dune-project b/dune-project
@@ -24,8 +24,8 @@
   (synopsis "Static analysis framework for C")
   (depends
     (ocaml (>= 4.10))
-    (goblint-cil (>= 2.0.1)) ; 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.4.0))
+    (goblint-cil (>= 2.0.2)) ; 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))
     (zarith (>= 1.8))
     (yojson (>= 2.0.0))
     (qcheck-core (>= 0.19))
@@ -44,7 +44,7 @@
     (fileutils (>= 0.6.4))
     cpu
     arg-complete
-    yaml
+    (yaml (>= 3.0.0))
     uuidm
     catapult
     catapult-file

diff --git a/goblint.opam b/goblint.opam
@@ -21,8 +21,8 @@ bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "dune" {>= "3.6"}
   "ocaml" {>= "4.10"}
-  "goblint-cil" {>= "2.0.1"}
-  "batteries" {>= "3.4.0"}
+  "goblint-cil" {>= "2.0.2"}
+  "batteries" {>= "3.5.0"}
   "zarith" {>= "1.8"}
   "yojson" {>= "2.0.0"}
   "qcheck-core" {>= "0.19"}
@@ -41,7 +41,7 @@ depends: [
   "fileutils" {>= "0.6.4"}
   "cpu"
   "arg-complete"
-  "yaml"
+  "yaml" {>= "3.0.0"}
   "uuidm"
   "catapult"
   "catapult-file"
@@ -74,10 +74,12 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
-pin-depends: [
-  [ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#4df989fe625d91ce07d94afe1d85b3b5c6cdd63e" ]
+# pin-depends: [
+  # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
+  # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
-  [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
-  # TODO: add back after release, only pinned for CI stability
-  [ "apron.v0.9.13" "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"]
+  # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
+# ]
+post-messages: [
+  "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
diff --git a/goblint.opam.locked b/goblint.opam.locked
@@ -21,7 +21,7 @@ doc: "https://goblint.readthedocs.io/en/latest/"
 bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "angstrom" {= "0.15.0"}
-  "apron" {= "v0.9.13"}
+  "apron" {= "v0.9.14~beta.2"}
   "arg-complete" {= "0.1.0"}
   "astring" {= "0.8.5"}
   "base-bigarray" {= "base"}
@@ -56,22 +56,22 @@ depends: [
   "dune-private-libs" {= "3.6.1"}
   "dune-site" {= "3.6.1"}
   "dyn" {= "3.6.1"}
+  "fileutils" {= "0.6.4"}
   "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}
-  "goblint-cil" {= "2.0.1"}
+  "goblint-cil" {= "2.0.2"}
   "integers" {= "0.7.0"}
   "json-data-encoding" {= "0.12.1"}
   "jsonrpc" {= "1.15.0~5.0preview1"}
-  "fileutils" {= "0.6.4"}
   "logs" {= "0.7.0"}
-  "mlgmpidl" {= "1.2.14"}
+  "mlgmpidl" {= "1.2.15"}
   "num" {= "1.4"}
   "ocaml" {= "4.14.0"}
-  "ocaml-variants" {= "4.14.0+options"}
   "ocaml-compiler-libs" {= "v0.12.4"}
   "ocaml-config" {= "2"}
   "ocaml-option-flambda" {= "1"}
   "ocaml-syntax-shims" {= "1.0.0"}
+  "ocaml-variants" {= "4.14.0+options"}
   "ocamlbuild" {= "0.14.2"}
   "ocamlfind" {= "1.9.5"}
   "odoc" {= "2.2.0" & with-doc}
@@ -125,18 +125,6 @@ available: os-distribution != "alpine" & arch != "arm64"
 conflicts: [
   "result" {< "1.5"}
 ]
-# TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936
-pin-depends: [
-  [
-    "goblint-cil.2.0.1"
-    "git+https://github.com/goblint/cil.git#4df989fe625d91ce07d94afe1d85b3b5c6cdd63e"
-  ]
-  [
-    "apron.v0.9.13"
-    "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"
-  ]
-  [
-    "ppx_deriving.5.2.1"
-    "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
-  ]
+post-messages: [
+  "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
diff --git a/goblint.opam.template b/goblint.opam.template
@@ -1,10 +1,12 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
-pin-depends: [
-  [ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#4df989fe625d91ce07d94afe1d85b3b5c6cdd63e" ]
+# pin-depends: [
+  # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
+  # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
-  [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
-  # TODO: add back after release, only pinned for CI stability
-  [ "apron.v0.9.13" "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"]
+  # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
+# ]
+post-messages: [
+  "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
diff --git a/gobview b/gobview
diff --git a/make.sh b/make.sh
@@ -8,7 +8,7 @@ opam_setup() {
   set -x
   opam init -y -a --bare $SANDBOXING # sandboxing is disabled in travis and docker
   opam update
-  opam switch -y create . --deps-only ocaml-variants.4.14.0+options ocaml-option-flambda --locked
+  opam switch -y create . --deps-only --packages=ocaml-variants.4.14.0+options,ocaml-option-flambda --locked
 }
 
 rule() {

diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb
@@ -41,7 +41,7 @@ def clearline
 
 $goblint = File.join(Dir.getwd,"goblint")
 goblintbyte = File.join(Dir.getwd,"goblint.byte")
-if File.exists?(goblintbyte) then
+if File.exist?(goblintbyte) then
   puts "Running the byte-code version! Continue? (y/n)"
   exit unless $stdin.gets()[0] == 'y'
   $goblint = goblintbyte
@@ -50,11 +50,11 @@ def clearline
 end
 $vrsn = `#{$goblint} --version`
 
-if not File.exists? "linux-headers" then
+if not File.exist? "linux-headers" then
   puts "Missing linux-headers, will download now!"
   `make headers`
 end
-has_linux_headers = File.exists? "linux-headers" # skip kernel tests if make headers failed (e.g. on opam-repository opam-ci where network is forbidden)
+has_linux_headers = File.exist? "linux-headers" # skip kernel tests if make headers failed (e.g. on opam-repository opam-ci where network is forbidden)
 
 #Command line parameters
 #Either only run a single test, or

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
@@ -34,8 +34,8 @@ struct
   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;
     let reach_or_mpt: _ Queries.t = if reach then ReachableFrom e else MayPointTo e in
-    let ls = ctx.ask reach_or_mpt in
-    ctx.emit (Access {exp=e; lvals=ls; kind; reach})
+    let ad = ctx.ask reach_or_mpt in
+    ctx.emit (Access {exp=e; ad; kind; reach})
 
   (** Three access levels:
       + [deref=false], [reach=false] - Access [exp] without dereferencing, used for all normal reads and all function call arguments.
@@ -137,25 +137,20 @@ struct
 
   let event ctx e octx =
     match e with
-    | Events.Access {lvals; kind; _} when !collect_local && !AnalysisState.postsolving ->
-      begin match lvals with
-        | ls when Queries.LS.is_top ls ->
-          let access: AccessDomain.Event.t = {var_opt = None; offs_opt = None; kind} in
-          ctx.sideg ctx.node (G.singleton access)
-        | ls ->
-          let events = Queries.LS.fold (fun (var, offs) acc ->
-              let coffs = Offset.Exp.to_cil offs in
-              let access: AccessDomain.Event.t =
-                if CilType.Varinfo.equal var dummyFunDec.svar then
-                  {var_opt = None; offs_opt = (Some coffs); kind}
-                else
-                  {var_opt = (Some var); offs_opt = (Some coffs); kind}
-              in
-              G.add access acc
-            ) ls (G.empty ())
-          in
-          ctx.sideg ctx.node events
-      end
+    | Events.Access {ad; kind; _} when !collect_local && !AnalysisState.postsolving ->
+      let events = Queries.AD.fold (fun addr es ->
+          match addr with
+          | Queries.AD.Addr.Addr (var, offs) ->
+            let coffs = ValueDomain.Offs.to_cil offs in
+            let access: AccessDomain.Event.t = {var_opt = (Some var); offs_opt = (Some coffs); kind} in
+            G.add access es
+          | UnknownPtr ->
+            let access: AccessDomain.Event.t = {var_opt = None; offs_opt = None; kind} in
+            G.add access es
+          | _ -> es
+        ) ad (G.empty ())
+      in
+      ctx.sideg ctx.node events
     | _ ->
       ctx.local
 end
+3 −1		dune-project
+2 −1		gobview.opam
+3 −6		gobview.opam.locked
+1 −1		gobview.opam.template
+19 −0		runtime/stubs.js