From ec455d76528de00f8de7e30ea3c153830a5aa3c2 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 5 Dec 2022 15:33:58 -0500 Subject: [PATCH] Fall back to Z3 4.8.8 on AWSLC/BLST proofs This updates the `what4-solvers` snapshot to one that includes both Z3 4.8.8 and 4.8.14. While we continue to use 4.8.14 for most CI purposes, we fall back to 4.8.8 specifically when running the AWSLC or BLST proofs, which have been known to nondeterministically time out with those versions. Hopefully, this should resolve our CI woes. This avoids the main issue in #1772, although the underlying cause still has yet to be investigated. --- .github/ci.sh | 6 ++++++ .github/workflows/ci.yml | 2 +- s2nTests/scripts/awslc-entrypoint.sh | 4 ++++ s2nTests/scripts/blst-entrypoint.sh | 10 ++++++---- saw-remote-api/Dockerfile | 2 +- saw/Dockerfile | 2 +- 6 files changed, 19 insertions(+), 7 deletions(-) diff --git a/.github/ci.sh b/.github/ci.sh index 404e10af13..fb6acf2018 100755 --- 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 index 816aee7e2f..0009df81ab 100644 --- 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 index afe2953913..87aa7ccf72 100755 --- 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 index 4d8035b702..3d8ed77817 100755 --- 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 index 81ab9c3354..2cef115912 100644 --- 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 index a61edafeb7..13998eda67 100644 --- 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