From 75fed4b2f1d7f0f531375bb936dd1d9998c1cc7c Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 5 Dec 2022 07:48:53 -0500 Subject: [PATCH] Build both Z3 4.8.10 and 4.8.14 versions We now include both Z3 4.8.10 and 4.8.14 so that SAW's CI can revert back to 4.8.10 in certain cases, as 4.8.14 has been known to nondeterministically fail on certain jobs. See GaloisInc/saw-script#1772. --- .github/ci.sh | 15 +++++++++--- .github/workflows/ci.yml | 15 +++++++++++- .gitmodules | 7 ++++-- README.md | 50 +++++++++++++++++++++++++++++++++++++++- repos/z3-4.8.10 | 1 + repos/{z3 => z3-4.8.14} | 0 6 files changed, 81 insertions(+), 7 deletions(-) create mode 160000 repos/z3-4.8.10 rename repos/{z3 => z3-4.8.14} (100%) diff --git a/.github/ci.sh b/.github/ci.sh index dbfc529..b565c98 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -169,15 +169,24 @@ build_yices() { cleanup_bins } +build_z3-4.8.10() { + build_z3 "4.8.10" +} + +build_z3-4.8.14() { + build_z3 "4.8.14" +} + build_z3() { - pushd repos/z3 + Z3_BIN="z3-$1" + pushd repos/$Z3_BIN if $IS_WIN ; then sed -i.bak -e 's/STATIC_BIN=False/STATIC_BIN=True/' scripts/mk_util.py fi python scripts/mk_make.py - (cd build && make -j4 && cp z3$EXT $BIN) + (cd build && make -j4 && cp z3$EXT $BIN/$Z3_BIN$EXT) popd - (cd $BIN && ./z3$EXT --version && deps z3$EXT && ./z3$EXT $PROBLEM) + (cd $BIN && ./$Z3_BIN$EXT --version && deps $Z3_BIN$EXT && ./$Z3_BIN$EXT $PROBLEM) cleanup_bins } diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b274e40..671928e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -8,6 +8,7 @@ on: env: CACHE_VERSION: 1 + LATEST_Z3_VERSION: "4.8.14" jobs: build: @@ -16,7 +17,7 @@ jobs: fail-fast: false matrix: os: [ubuntu-22.04, ubuntu-20.04, macos-12, windows-2019] - solver: [abc, boolector, cvc4, cvc5, yices, z3] + solver: [abc, boolector, cvc4, cvc5, yices, z3-4.8.10, z3-4.8.14] steps: - uses: actions/checkout@v2 with: @@ -126,6 +127,18 @@ jobs: name: "${{ matrix.os }}-z3-bin" path: bin + # Make z3 a symlink for z3-. + - name: Alias latest Z3 version (non-Windows) + shell: bash + run: ln -s bin/z3-${{ env.LATEST_Z3_VERSION }} bin/z3 + if: runner.os != 'Windows' + + # Windows doesn't support symlinks, so just copy the binary on Windows. + - name: Alias latest Z3 version (Windows) + shell: msys2 {0} + run: cp bin/z3-${{ env.LATEST_Z3_VERSION }} bin/z3 + if: runner.os == 'Windows' + - uses: actions/upload-artifact@v2 with: path: bin diff --git a/.gitmodules b/.gitmodules index d9db92d..ddcefb7 100644 --- a/.gitmodules +++ b/.gitmodules @@ -16,8 +16,11 @@ [submodule "repos/yices2"] path = repos/yices2 url = https://github.com/SRI-CSL/yices2 -[submodule "repos/z3"] - path = repos/z3 +[submodule "repos/z3-4.8.10"] + path = repos/z3-4.8.10 + url = https://github.com/Z3Prover/z3 +[submodule "repos/z3-4.8.14"] + path = repos/z3-4.8.14 url = https://github.com/Z3Prover/z3 [submodule "repos/cvc5"] path = repos/cvc5 diff --git a/README.md b/README.md index f643452..59d6937 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,50 @@ # what4-solvers -Multi-platform binary creation for solvers of the versions most suitable for use with What4 + +Multi-platform binary creation for solvers of the versions most suitable for use +with [What4](https://github.com/GaloisInc/what4), as well as tools built on top +of What4, such as [Cryptol](https://cryptol.net/), +[Crux](https://crux.galois.com/), and [SAW](https://saw.galois.com/). + +Binary distributions can be found at the +[releases page](https://github.com/GaloisInc/what4-solvers/releases). +Currently, `what4-solvers` offers the following solver versions: + +* ABC - [99ab99bf](https://github.com/berkeley-abc/abc/tree/99ab99bfa6d1c2cc11d59af16aa26b273f611674) +* Boolector - [3.2.2](https://github.com/Boolector/boolector/tree/e7aba964f69cd52dbe509e46e818a4411b316cd3) +* CVC4 - [1.8](https://github.com/CVC4/CVC4-archived/tree/5247901077efbc7b9016ba35fded7a6ab459a379) +* CVC5 - [1.0.2](https://github.com/cvc5/cvc5/tree/ef35c1131976e5a3d981dace510d90aed2d11cef) +* Yices - [2.6.2](https://github.com/SRI-CSL/yices2/tree/8509cfb5c294df3c0ac3a4814483f39c58879606) +* Z3 - [4.8.10](https://github.com/Z3Prover/z3/tree/517d907567f4283ad8b48ff9c2a3f6dce838569e) and + [4.8.14](https://github.com/Z3Prover/z3/tree/df8f9d7dcb8b9f9b3de1072017b7c2b7f63f0af8) + +Built for the following operating systems: + +* macOS Monterey 12 +* Ubuntu 20.04 +* Ubuntu 22.04 +* Windows Server 2019 + +## FAQ + +### Why build for multiple Ubuntu versions? + +We attempt to offer somewhat broad coverage of different Linux versions. To +that end, we build each solver on the two most recent Ubuntu LTS releases. This +ensures relatively complete coverage of different shared library dependencies +(e.g., different `glibc` versions). + +### Why offer multiple Z3 versions? + +We use Z3 as the default SMT solver in many different projects' CI, including +the CI for Cryptol and SAW. Unfortunately, certain Z3 versions have been known +to non-deterministically fail or time out on certain SMT queries. See, for +example, [this Cryptol issue](https://github.com/GaloisInc/cryptol/issues/1107) +regarding Z3 4.8.10 and +[this SAW issue](https://github.com/GaloisInc/saw-script/issues/1772) regarding +Z3 4.8.14. As a consequence, it is very difficult to find a single Z3 version +that works reliably across all of our tools' CI. + +As a compromise, we offer multiple Z3 versions so that tools can pick one that +is known to work well for their particular needs. If we successfully identify a +later version of Z3 that is known to work reliably across all CI +configurations, we may reconsider this choice. diff --git a/repos/z3-4.8.10 b/repos/z3-4.8.10 new file mode 160000 index 0000000..517d907 --- /dev/null +++ b/repos/z3-4.8.10 @@ -0,0 +1 @@ +Subproject commit 517d907567f4283ad8b48ff9c2a3f6dce838569e diff --git a/repos/z3 b/repos/z3-4.8.14 similarity index 100% rename from repos/z3 rename to repos/z3-4.8.14