Skip to content

Commit e718562

Browse files
sim642sim642
committed
Merge branch 'master' into queries-ad-cont
2 parents 2917999 + 5347c08 commit e718562

42 files changed

Lines changed: 604 additions & 164 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/docker.yml‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -38,18 +38,18 @@ jobs:
3838
uses: actions/checkout@v4
3939

4040
- name: Set up Docker Buildx
41-
uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
41+
uses: docker/setup-buildx-action@v3 # needed for GitHub Actions Cache in build-push-action
4242

4343
- name: Log in to the Container registry
44-
uses: docker/login-action@v2
44+
uses: docker/login-action@v3
4545
with:
4646
registry: ${{ env.REGISTRY }}
4747
username: ${{ github.actor }}
4848
password: ${{ secrets.GITHUB_TOKEN }}
4949

5050
- name: Extract metadata (tags, labels) for Docker
5151
id: meta
52-
uses: docker/metadata-action@v4
52+
uses: docker/metadata-action@v5
5353
with:
5454
images: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}
5555
tags: |
@@ -59,7 +59,7 @@ jobs:
5959
6060
- name: Build Docker image
6161
id: build
62-
uses: docker/build-push-action@v4
62+
uses: docker/build-push-action@v5
6363
with:
6464
context: .
6565
load: true # load into docker instead of immediately pushing
@@ -72,7 +72,7 @@ jobs:
7272
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
7373

7474
- name: Push Docker image
75-
uses: docker/build-push-action@v4
75+
uses: docker/build-push-action@v5
7676
with:
7777
context: .
7878
push: true

‎.github/workflows/unlocked.yml‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ jobs:
1818
- ubuntu-latest
1919
- macos-latest
2020
ocaml-compiler:
21+
- 5.0.x
2122
- ocaml-variants.4.14.0+options,ocaml-option-flambda
2223
- 4.14.x
2324
- 4.13.x
@@ -211,11 +212,11 @@ jobs:
211212
uses: actions/checkout@v4
212213

213214
- name: Set up Docker Buildx
214-
uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
215+
uses: docker/setup-buildx-action@v3 # needed for GitHub Actions Cache in build-push-action
215216

216217
- name: Build dev Docker image
217218
id: build
218-
uses: docker/build-push-action@v4
219+
uses: docker/build-push-action@v5
219220
with:
220221
context: .
221222
target: dev

‎CHANGELOG.md‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
1-
## v2.2.0
2-
* TODO OCaml 5 (#1003, #1137).
3-
* TODO Library #1138
4-
* TODO refactor race #1136
1+
## v2.2.1
2+
* Bump batteries lower bound to 3.5.0.
3+
* Fix flaky dead code elimination transformation test.
54

5+
## v2.2.0
66
* Add `setjmp`/`longjmp` analysis (#887, #970, #1015, #1019).
7-
* Refactor race analysis to lazy distribution (#1084, #1089, #1016).
7+
* Refactor race analysis to lazy distribution (#1084, #1089, #1136, #1016).
88
* Add thread-unsafe library function call analysis (#723, #1082).
99
* Add mutex type analysis and mutex API analysis (#800, #839, #1073).
1010
* Add interval set domain and string literals domain (#901, #966, #994, #1048).
@@ -19,8 +19,8 @@
1919
* Fix many incremental analysis issues (#627, #836, #835, #841, #932, #678, #942, #949, #950, #957, #955, #954, #960, #959, #1004, #558, #1010, #1091).
2020
* Fix server mode for abstract debugging (#983, #990, #997, #1000, #1001, #1013, #1018, #1017, #1026, #1027).
2121
* Add documentation for configuration JSON schema and OCaml API (#999, #1054, #1055, #1053).
22-
* Add many library function specifications (#962, #996, #1028, #1079, #1121, #1135).
23-
* Add OCaml 5.0 support (#945).
22+
* Add many library function specifications (#962, #996, #1028, #1079, #1121, #1135, #1138).
23+
* Add OCaml 5.0 support (#1003, #945, #1162).
2424

2525
## v2.1.0
2626
Functionally equivalent to Goblint in SV-COMP 2023.

‎README.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Documentation can be browsed on [Read the Docs](https://goblint.readthedocs.io/e
1313

1414
## Installing
1515
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.
16+
For benchmarking Goblint, please follow the [Benchmarking guide on Read the Docs](https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/).
1617

1718
### Linux
1819
1. Install [opam](https://opam.ocaml.org/doc/Install.html).

‎docs/developer-guide/releasing.md‎

Lines changed: 13 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -45,13 +45,20 @@
4545
10. Check that analysis works: `goblint -v tests/regression/04-mutex/01-simple_rc.c`.
4646
11. Exit Docker container.
4747

48-
12. Create a GitHub release with the git tag: `DUNE_RELEASE_DELEGATE=github-dune-release-delegate dune-release publish distrib`.
48+
12. Temporarily enable Zenodo GitHub webhook.
49+
50+
This is because we only want numbered version releases to automatically add a new version to our Zenodo artifact.
51+
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.
52+
53+
13. Create a GitHub release with the git tag: `DUNE_RELEASE_DELEGATE=github-dune-release-delegate dune-release publish distrib`.
4954

5055
Explicitly specify `distrib` because we don't want to publish OCaml API docs.
5156
Environment variable workaround for the package having a Read the Docs `doc` URL (see <https://github.com/ocamllabs/dune-release/issues/154>).
5257

53-
13. Create an opam package: `dune-release opam pkg`.
54-
14. Submit the opam package to opam-repository: `dune-release opam submit`.
58+
14. Re-disable Zenodo GitHub webhook.
59+
60+
15. Create an opam package: `dune-release opam pkg`.
61+
16. Submit the opam package to opam-repository: `dune-release opam submit`.
5562

5663

5764
## SV-COMP
@@ -104,15 +111,9 @@
104111
### After all preruns
105112

106113
1. Push git tag from last prerun: `git push origin svcompXY`.
107-
2. Temporarily disable Zenodo webhook.
108-
109-
This is because we don't want a new out-of-place version of Goblint in our Zenodo artifact.
110-
A separate Zenodo artifact for the SV-COMP version can be created later if tool paper is submitted.
111-
112-
3. Create GitHub release from the git tag and attach latest submitted archive as a download.
113-
4. Manually run `docker` workflow on `svcompXY` git tag and targeting `svcompXY` Docker tag.
114+
2. Create GitHub release from the git tag and attach latest submitted archive as a download.
115+
3. Manually run `docker` workflow on `svcompXY` git tag and targeting `svcompXY` Docker tag.
114116

115117
This is because the usual `docker` workflow only handles semver releases.
116118

117-
5. Re-enable Zenodo webhook.
118-
6. Release new semver version on opam. See above.
119+
4. Release new semver version on opam. See above.

‎docs/user-guide/benchmarking.md‎

Lines changed: 26 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,31 @@
11
# Benchmarking
2+
The following best practices should be followed when benchmarking Goblint.
3+
This is to ensure valid, reproducible and representative benchmarking results.
24

3-
To achieve reproducible builds and the best performance for benchmarking, it is recommended to compile Goblint using the `release` option:
5+
# External benchmarking
6+
External users should choose the version of Goblint to evaluate or benchmark as follows:
7+
8+
1. Use the newest version release.
9+
10+
The version from git `master` branch or any other intermediate git commit come without any guarantees.
11+
They are bleeding-edge and haven't gone through validation like the version releases.
12+
13+
SV-COMP releases are highly preferable since they've gone through rigorous validation in SV-COMP.
14+
15+
2. Download the corresponding version from a Zenodo artifact or by checking out the respective git tag. **Do not install directly from opam repository!**
16+
17+
Goblint pins optimized versions of some dependencies which cannot be done on the opam repository releases.
18+
Thus, using the latter would yield unrepresentative results.
19+
20+
Zenodo artifacts come with DOIs, which make them ideal for citation.
21+
22+
3. Use OCaml 4.14. **Do not use OCaml 5!**
23+
24+
OCaml 5 has significant performance regressions, which yield unrepresentative benchmarking results.
25+
Goblint's `make setup` installs the correct OCaml version into a new opam switch.
26+
27+
# Release build
28+
To achieve the best performance for benchmarking, Goblint should be compiled using the `release` option:
429

530
```sh
631
make release

‎dune-project‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,8 +24,8 @@
2424
(synopsis "Static analysis framework for C")
2525
(depends
2626
(ocaml (>= 4.10))
27-
(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.
28-
(batteries (>= 3.4.0))
27+
(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.
28+
(batteries (>= 3.5.0))
2929
(zarith (>= 1.8))
3030
(yojson (>= 2.0.0))
3131
(qcheck-core (>= 0.19))

‎goblint.opam‎

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,8 @@ bug-reports: "https://github.com/goblint/analyzer/issues"
2121
depends: [
2222
"dune" {>= "3.6"}
2323
"ocaml" {>= "4.10"}
24-
"goblint-cil" {>= "2.0.1"}
25-
"batteries" {>= "3.4.0"}
24+
"goblint-cil" {>= "2.0.2"}
25+
"batteries" {>= "3.5.0"}
2626
"zarith" {>= "1.8"}
2727
"yojson" {>= "2.0.0"}
2828
"qcheck-core" {>= "0.19"}
@@ -74,10 +74,12 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
7474
# on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
7575
# also remember to generate/adjust goblint.opam.locked!
7676
available: os-distribution != "alpine" & arch != "arm64"
77-
pin-depends: [
78-
[ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#4df989fe625d91ce07d94afe1d85b3b5c6cdd63e" ]
77+
# pin-depends: [
78+
# published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
79+
# [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
7980
# TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
80-
[ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
81-
# TODO: add back after release, only pinned for CI stability
82-
[ "apron.v0.9.13" "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"]
81+
# [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
82+
# ]
83+
post-messages: [
84+
"Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
8385
]

‎goblint.opam.locked‎

Lines changed: 7 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ doc: "https://goblint.readthedocs.io/en/latest/"
2121
bug-reports: "https://github.com/goblint/analyzer/issues"
2222
depends: [
2323
"angstrom" {= "0.15.0"}
24-
"apron" {= "v0.9.13"}
24+
"apron" {= "v0.9.14~beta.2"}
2525
"arg-complete" {= "0.1.0"}
2626
"astring" {= "0.8.5"}
2727
"base-bigarray" {= "base"}
@@ -56,22 +56,22 @@ depends: [
5656
"dune-private-libs" {= "3.6.1"}
5757
"dune-site" {= "3.6.1"}
5858
"dyn" {= "3.6.1"}
59+
"fileutils" {= "0.6.4"}
5960
"fmt" {= "0.9.0"}
6061
"fpath" {= "0.7.3"}
61-
"goblint-cil" {= "2.0.1"}
62+
"goblint-cil" {= "2.0.2"}
6263
"integers" {= "0.7.0"}
6364
"json-data-encoding" {= "0.12.1"}
6465
"jsonrpc" {= "1.15.0~5.0preview1"}
65-
"fileutils" {= "0.6.4"}
6666
"logs" {= "0.7.0"}
67-
"mlgmpidl" {= "1.2.14"}
67+
"mlgmpidl" {= "1.2.15"}
6868
"num" {= "1.4"}
6969
"ocaml" {= "4.14.0"}
70-
"ocaml-variants" {= "4.14.0+options"}
7170
"ocaml-compiler-libs" {= "v0.12.4"}
7271
"ocaml-config" {= "2"}
7372
"ocaml-option-flambda" {= "1"}
7473
"ocaml-syntax-shims" {= "1.0.0"}
74+
"ocaml-variants" {= "4.14.0+options"}
7575
"ocamlbuild" {= "0.14.2"}
7676
"ocamlfind" {= "1.9.5"}
7777
"odoc" {= "2.2.0" & with-doc}
@@ -125,18 +125,6 @@ available: os-distribution != "alpine" & arch != "arm64"
125125
conflicts: [
126126
"result" {< "1.5"}
127127
]
128-
# TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936
129-
pin-depends: [
130-
[
131-
"goblint-cil.2.0.1"
132-
"git+https://github.com/goblint/cil.git#4df989fe625d91ce07d94afe1d85b3b5c6cdd63e"
133-
]
134-
[
135-
"apron.v0.9.13"
136-
"git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"
137-
]
138-
[
139-
"ppx_deriving.5.2.1"
140-
"git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
141-
]
128+
post-messages: [
129+
"Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
142130
]

‎goblint.opam.template‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,12 @@
11
# on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
22
# also remember to generate/adjust goblint.opam.locked!
33
available: os-distribution != "alpine" & arch != "arm64"
4-
pin-depends: [
5-
[ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#4df989fe625d91ce07d94afe1d85b3b5c6cdd63e" ]
4+
# pin-depends: [
5+
# published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
6+
# [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
67
# TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
7-
[ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
8-
# TODO: add back after release, only pinned for CI stability
9-
[ "apron.v0.9.13" "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"]
8+
# [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
9+
# ]
10+
post-messages: [
11+
"Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
1012
]

0 commit comments

Comments
 (0)