Merge branch 'master' into issue_718

goblint · Nov 27, 2022 · 32257f8 · 32257f8
2 parents afd4153 + 4828e7b
commit 32257f8
Show file tree

Hide file tree

Showing 170 changed files with 4,038 additions and 1,616 deletions.
diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
@@ -67,6 +67,9 @@ jobs:
       - name: Test incremental regression
         run: ruby scripts/update_suite.rb -i
 
+      - name: Test incremental regression with cfg comparison
+        run: ruby scripts/update_suite.rb -c
+
   extraction:
     if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
 

diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
@@ -95,6 +95,9 @@ jobs:
       - name: Test incremental regression
         run: ruby scripts/update_suite.rb -i
 
+      - name: Test incremental regression with cfg comparison
+        run: ruby scripts/update_suite.rb -c
+
   lower-bounds-downgrade:
     # use external 0install solver to downgrade: https://github.com/ocaml-opam/opam-0install-solver
     # TODO: will be built in in opam 2.2: https://github.com/ocaml/opam/pull/4909
@@ -174,6 +177,9 @@ jobs:
       - name: Test incremental regression
         run: ruby scripts/update_suite.rb -i
 
+      - name: Test incremental regression with cfg comparison
+        run: ruby scripts/update_suite.rb -c
+
   lower-bounds-docker:
     # use builtin-0install solver to remove and downgrade, opam normally compiled without, Docker images have it compiled
 
@@ -265,3 +271,6 @@ jobs:
 
       - name: Test incremental regression
         run: ruby scripts/update_suite.rb -i
+
+      - name: Test incremental regression with cfg comparison
+        run: ruby scripts/update_suite.rb -c
diff --git a/.gitignore b/.gitignore
@@ -87,3 +87,6 @@ gobview_out/*
 # witnesses
 witness.yml
 witness.certificate.yml
+
+# transformations
+transformed.c
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,3 +1,12 @@
+## v2.1.0
+Functionally equivalent to Goblint in SV-COMP 2023.
+
+* Add automatic configuration tuning (#772).
+* Add many library function specifications (#865, #868, #878, #884, #886).
+* Reorganize library stubs (#814, #845).
+* Add Trace Event Format output to timing (#844).
+* Optimize domains for address and path sets (#803, #809).
+
 ## v2.0.1
 * Fix compilation with z3.
 

diff --git a/README.md b/README.md
@@ -12,18 +12,18 @@ Both for using an up-to-date version of Goblint or developing it, the best way i
 
 ### Linux
 1. Install [opam](https://opam.ocaml.org/doc/Install.html).
-2. Make sure the following are installed: `git patch m4 autoconf libgmp-dev libmpfr-dev pkg-config`.
+2. Make sure the following are installed: `git`, `patch`, `m4`, `autoconf`, `libgmp-dev`, `libmpfr-dev` and `pkg-config`.
 3. Run `make setup` to install OCaml and dependencies via opam.
 4. Run `make` to build Goblint itself.
 5. Run `make install` to install Goblint into the opam switch for usage via switch's `PATH`.
 
 ### MacOS
 1. Install GCC with `brew install gcc` (first run `xcode-select --install` if you don't want to build it from source). Goblint requires GCC while macOS's default `cpp` is Clang, which will not work.
 2. ONLY for M1 (ARM64) processor: homebrew changed its install location from `/usr/local/` to `/opt/homebrew/`. For packages to find their dependecies execute `sudo ln -s /opt/homebrew/{include,lib} /usr/local/`.
-3. Continue using Linux instructions (the formulae in brew for `patch libgmp-dev libmpfr-dev` are `gpatch gmp mpfr`, respectively).
+3. Continue using Linux instructions (the formulae in brew for `patch`, `libgmp-dev`, `libmpfr-dev` are `gpatch`, `gmp`, `mpfr`, respectively).
 
 ### Windows
-1. Install [WSL](https://docs.microsoft.com/en-us/windows/wsl/install-win10).
+1. Install [WSL2](https://docs.microsoft.com/en-us/windows/wsl/install-win10). Goblint is not compatible with WSL1.
 2. Continue using Linux instructions in WSL.
 
 ### Other

diff --git a/conf/svcomp.json b/conf/svcomp.json
@@ -9,6 +9,9 @@
       "enums": false,
       "interval": true
     },
+    "float": {
+      "interval": true
+    },
     "activated": [
       "base",
       "threadid",
@@ -21,12 +24,13 @@
       "race",
       "escape",
       "expRelation",
-      "assert",
       "mhp",
+      "assert",
       "var_eq",
       "symb_locks",
       "region",
-      "thread"
+      "thread",
+      "threadJoins"
     ],
     "context": {
       "widen": false
@@ -55,6 +59,19 @@
       "arrays": {
         "domain": "partitioned"
       }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic"
+      ]
     }
   },
   "exp": {

diff --git a/conf/svcomp23.json b/conf/svcomp23.json
@@ -29,7 +29,8 @@
       "var_eq",
       "symb_locks",
       "region",
-      "thread"
+      "thread",
+      "threadJoins"
     ],
     "context": {
       "widen": false
@@ -66,9 +67,10 @@
         "mallocWrappers",
         "noRecursiveIntervals",
         "enums",
-        "arrayDomain",
+        "congruence",
         "octagon",
-        "wideningThresholds"
+        "wideningThresholds",
+        "loopUnrollHeuristic"
       ]
     }
   },

diff --git a/docs/developer-guide/developing.md b/docs/developer-guide/developing.md
@@ -1,6 +1,8 @@
 # Developing
 
-Running `make dev` does the following:
+For development, Goblint must be installed from source: <https://github.com/goblint/analyzer#installing>.
+
+Then running `make dev` does the following:
 
 1. Installs some additional opam packages useful for developing.
 2. Installs a Git pre-commit hook for ocp-indent (see below).

diff --git a/docs/developer-guide/releasing.md b/docs/developer-guide/releasing.md
@@ -1,5 +1,7 @@
 # Releasing
 
+## opam
+
 1. Update list of authors and contributors in `.zenodo.json`, `CITATION.cff` and `dune-project`.
 2. Update `CHANGELOG.md`:
 
@@ -36,7 +38,7 @@
     3. Run Docker container in extracted directory: `docker run -it --rm -v $(pwd):/goblint ocaml/opam:ubuntu-22.04-ocaml-4.14` (or newer).
     4. Navigate to distribution archive inside Docker container: `cd /goblint`.
     5. Pin package from distribution archive: `opam pin add --no-action .`.
-    6. Install depexts: `opam depext goblint`.
+    6. Install depexts: `opam depext --with-test goblint`.
     7. Install and test package: `opam install --with-test goblint`.
     8. Activate opam environment: `eval $(opam env)`.
     9. Check version: `goblint --version`.
@@ -50,3 +52,67 @@
 
 13. Create an opam package: `dune-release opam pkg`.
 14. Submit the opam package to opam-repository: `dune-release opam submit`.
+
+
+## SV-COMP
+
+### Before all preruns
+
+1. Make sure you are running the same Ubuntu version as will be used for SV-COMP.
+2. Create conf file for SV-COMP year.
+3. Make sure this repository is checked out into a directory called `goblint`, not the default `analyzer`.
+
+    This is required such that the created archive would have everything in a single directory called `goblint`.
+
+4. Update SV-COMP year in `sv-comp/archive.sh`.
+
+    This includes: git tag name, git tag message and zipped conf file.
+
+### For each prerun
+
+1. Update opam pins:
+
+    1. Make sure you have the same `goblint-cil` version pinned as `goblint.opam` specifies.
+    2. Unpin `zarith.1.12-gob0`, because Gobview compatibility is not required.
+
+2. Make sure you have nothing valuable that would be deleted by `make clean`.
+3. Delete git tag from previous prerun: `git tag -d svcompXY`.
+4. Create archive: `./sv-comp/archive.sh`.
+
+    The resulting archive is `sv-comp/goblint.zip`.
+
+5. Check unextracted archive in latest SV-COMP container image: <https://gitlab.com/sosy-lab/benchmarking/competition-scripts/#container-image>.
+
+    Inside Docker:
+
+    1. Check version: `./goblint --version`.
+    2. Mount some sv-benchmarks and properties, e.g. as `/tool-test`, and run Goblint on them manually.
+
+    This ensures that the environment and the archive have all the correct system libraries.
+
+6. Commit and push the archive to an SV-COMP archives repository branch (but don't open a MR yet): <https://gitlab.com/sosy-lab/sv-comp/archives-2023#sparse-checkout> (SV-COMP 2023).
+7. Check pushed archive via CoveriTeam-Remote: <https://gitlab.com/sosy-lab/software/coveriteam/-/blob/main/doc/competition-help.md>.
+
+    1. Clone coveriteam repository.
+    2. Locally modify `actors/goblint.yml` archive location to the raw URL of the pushed archive.
+    3. Run Goblint on some sv-benchmarks and properties via CoveriTeam.
+
+    This ensures that Goblint runs on SoSy-Lab servers.
+
+8. Open MR to the SV-COMP archives repository.
+
+### 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.
+
+    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.
diff --git a/docs/developer-guide/testing.md b/docs/developer-guide/testing.md
@@ -33,7 +33,8 @@ incrementally (activating the option `incremental.load`) with some changes to th
 configuration. The respective `asserts` and expected results are checked in both runs.
 
 ### Running
-The incremental tests can be run with `./scripts/update_suite.rb -i`.
+The incremental tests can be run with `./scripts/update_suite.rb -i`. With `./scripts/update_suite.rb -c` the
+incremental tests are run using the more fine-grained cfg-based change detection.
 
 ### Writing
 An incremental test case consists of three files with the same file name: the `.c` file with the initial program, a

diff --git a/dune-project b/dune-project
@@ -27,7 +27,7 @@
   (depends
     (ocaml (>= 4.10))
     (dune (>= 3.0)) ; 3.0 lower bound needed in tests/extraction ; 2.9.1 explicit lower bound needed for opam install (https://github.com/ocaml/dune/pull/4806), (lang dune 2.9.1) doesn't do this
-    (goblint-cil (>= 2.0.0)) ; 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.
+    (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))
     (zarith (>= 1.8))
     (yojson (>= 2.0.0))

diff --git a/goblint.opam b/goblint.opam
@@ -21,7 +21,7 @@ bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "ocaml" {>= "4.10"}
   "dune" {>= "3.0"}
-  "goblint-cil" {>= "2.0.0"}
+  "goblint-cil" {>= "2.0.1"}
   "batteries" {>= "3.4.0"}
   "zarith" {>= "1.8"}
   "yojson" {>= "2.0.0"}
@@ -74,7 +74,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#bfb977b48d6d92e0ecbdab2e04f2576095506107" ]
+  [ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#5a3b7bb7f4d9b67678826ab7698f8a9048891553" ]
   # 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

diff --git a/goblint.opam.locked b/goblint.opam.locked
@@ -56,7 +56,7 @@ depends: [
   "dune-configurator" {= "3.0.3"}
   "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}
-  "goblint-cil" {= "2.0.0"}
+  "goblint-cil" {= "2.0.1"}
   "integers" {= "0.7.0"}
   "json-data-encoding" {= "0.11"}
   "jsonrpc" {= "1.12.4"}
@@ -120,11 +120,14 @@ build: [
 ]
 dev-repo: "git+https://github.com/goblint/analyzer.git"
 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.0"
-    "git+https://github.com/goblint/cil.git#bfb977b48d6d92e0ecbdab2e04f2576095506107"
+    "goblint-cil.2.0.1"
+    "git+https://github.com/goblint/cil.git#5a3b7bb7f4d9b67678826ab7698f8a9048891553"
   ]
   [
     "apron.v0.9.13"

diff --git a/goblint.opam.template b/goblint.opam.template
@@ -2,7 +2,7 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#bfb977b48d6d92e0ecbdab2e04f2576095506107" ]
+  [ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#5a3b7bb7f4d9b67678826ab7698f8a9048891553" ]
   # 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

diff --git a/gobview b/gobview
diff --git a/lib/sv-comp/stub/src/sv-comp.c b/lib/sv-comp/stub/src/sv-comp.c
@@ -22,14 +22,23 @@ __VERIFIER_nondet(char)
 __VERIFIER_nondet(int)
 __VERIFIER_nondet(float)
 __VERIFIER_nondet(double)
-// __VERIFIER_nondet(loff_t)
+// loff_t in LibraryFunctions
 __VERIFIER_nondet(long)
 __VERIFIER_nondet2(char*, pchar)
+__VERIFIER_nondet2(char*, charp) // not in rules
+__VERIFIER_nondet2(const char*, const_char_pointer) // not in rules
+__VERIFIER_nondet2(__SIZE_TYPE__, size_t)
 // missing pthread_t
 // missing sector_t
 __VERIFIER_nondet(short)
-// __VERIFIER_nondet(size_t)
-// missing u32
+__VERIFIER_nondet2(unsigned int, u32)
+__VERIFIER_nondet2(unsigned short int, u16) // not in rules
+__VERIFIER_nondet2(unsigned char, u8) // not in rules
+__VERIFIER_nondet2(unsigned char, unsigned_char) // not in rules
+__VERIFIER_nondet2(long long, longlong) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
+__VERIFIER_nondet2(unsigned long long, ulonglong) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
+__VERIFIER_nondet2(__uint128_t, uint128) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
+__VERIFIER_nondet2(__int128_t, int128) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
 __VERIFIER_nondet2(unsigned char, uchar)
 __VERIFIER_nondet2(unsigned int, uint)
 __VERIFIER_nondet2(unsigned long, ulong)
@@ -40,4 +49,4 @@ __VERIFIER_nondet2(void*, pointer)
 
 // atomics are now special in Goblint
 // void __VERIFIER_atomic_begin() { }
-// void __VERIFIER_atomic_end() { }
+// void __VERIFIER_atomic_end() { }
diff --git a/mkdocs.yml b/mkdocs.yml
@@ -18,6 +18,7 @@ dev_addr: '127.0.0.1:8010' # different port from default python http.server for
 nav:
   - Home: index.md
   - 'User guide':
+    - Installing: https://github.com/goblint/analyzer#installing
     - user-guide/running.md
     - user-guide/configuring.md
     - user-guide/inspecting.md
+1 −1		gobview.opam.locked
+6 −6		src/state/gvGoblint.ml
+1 −1		src/state/search.ml