Merge pull request #1775 from GaloisInc/T1772

Fall back to Z3 4.8.8 on AWSLC/BLST proofs
GaloisInc · Dec 16, 2022 · 7fe24ae · 7fe24ae
2 parents 6170630 + 7d140db
commit 7fe24ae
Show file tree

Hide file tree

Showing 6 changed files with 19 additions and 7 deletions.
diff --git a/.github/ci.sh b/.github/ci.sh
@@ -129,7 +129,13 @@ zip_dist_with_solvers() {
   cp "$BIN/cvc4"       dist/bin/
   cp "$BIN/yices"      dist/bin/
   cp "$BIN/yices-smt2" dist/bin/
+  # Z3 4.8.14 has been known to nondeterministically time out with the AWSLC
+  # and BLST proofs, so we include both 4.8.8 and 4.8.14 so that we can fall
+  # back to 4.8.8 (a version known to work with the AWSLC and BLST proofs)
+  # where necessary. See #1772.
   cp "$BIN/z3"         dist/bin/
+  cp "$BIN/z3-4.8.8"   dist/bin/
+  cp "$BIN/z3-4.8.14"  dist/bin/
   cp -r dist "$sname"
   tar -cvzf "$sname".tar.gz "$sname"
 }

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -24,7 +24,7 @@ env:
   # ./saw-remote-api/Dockerfile
   # ./s2nTests/scripts/blst-entrypoint.sh
   # ./s2nTests/docker/saw.dockerfile
-  SOLVER_PKG_VERSION: "snapshot-20220902"
+  SOLVER_PKG_VERSION: "snapshot-20221212"
 
   OCAML_VERSION: 4.09.x
 

diff --git a/s2nTests/scripts/awslc-entrypoint.sh b/s2nTests/scripts/awslc-entrypoint.sh
@@ -6,6 +6,10 @@ cd /saw-script/aws-lc-verification/SAW
 rm bin/saw
 cp /saw-bin/saw bin/saw
 cp /saw-bin/abc bin/abc
+cp /saw-bin/yices bin/yices
+# Z3 4.8.14 has been known to nondeterministically time out with the BLST
+# proofs, so fall back to 4.8.8 instead. See #1772.
+cp /saw-bin/z3-4.8.8 bin/z3
 
 export PATH=/saw-script/aws-lc-verification/SAW/bin:$PATH
 export CRYPTOLPATH=/saw-script/aws-lc-verification/cryptol-specs

diff --git a/s2nTests/scripts/blst-entrypoint.sh b/s2nTests/scripts/blst-entrypoint.sh
@@ -3,11 +3,13 @@ set -xe
 
 cd /workdir
 ./scripts/install.sh
+cp /saw-bin/cryptol bin/cryptol
 cp /saw-bin/saw bin/saw
-
-wget --quiet -O solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-22.04-bin.zip"
-(cd bin && unzip -o ../solvers.zip)
-chmod +x bin/*
+cp /saw-bin/abc bin/abc
+cp /saw-bin/yices bin/yices
+# Z3 4.8.14 has been known to nondeterministically time out with the BLST
+# proofs, so fall back to 4.8.8 instead. See #1772.
+cp /saw-bin/z3-4.8.8 bin/z3
 
 export PATH=/workdir/bin:$PATH
 export CRYPTOLPATH=/workdir/cryptol-specs:/workdir/spec

diff --git a/saw-remote-api/Dockerfile b/saw-remote-api/Dockerfile
@@ -28,7 +28,7 @@ RUN cabal v2-update && cabal v2-build -j exe:saw-remote-api
 RUN mkdir -p /home/saw/rootfs/usr/local/bin
 RUN cp $(cabal v2-exec which saw-remote-api) /home/saw/rootfs/usr/local/bin/saw-remote-api
 WORKDIR /home/saw//rootfs/usr/local/bin
-RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-22.04-bin.zip"
+RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20221212/ubuntu-22.04-bin.zip"
 RUN unzip solvers.zip && rm solvers.zip && chmod +x *
 USER root
 RUN chown -R root:root /home/saw/rootfs

diff --git a/saw/Dockerfile b/saw/Dockerfile
@@ -29,7 +29,7 @@ RUN cabal v2-build
 RUN mkdir -p /home/saw/rootfs/usr/local/bin
 RUN cp $(cabal v2-exec which saw) /home/saw/rootfs/usr/local/bin/saw
 WORKDIR /home/saw//rootfs/usr/local/bin
-RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-22.04-bin.zip"
+RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20221212/ubuntu-22.04-bin.zip"
 RUN unzip solvers.zip && rm solvers.zip && chmod +x *
 USER root
 RUN chown -R root:root /home/saw/rootfs