From 62936cba09c279b2c5ff964e9d8e04476bbc2fad 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.10 on AWSLC/BLST proofs This updates the `what4-solvers` snapshot to one that includes both Z3 4.8.10 and 4.8.14. While we continue to use 4.8.14 for most CI purposes, we fall back to 4.8.10 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 | 3 +++ s2nTests/scripts/blst-entrypoint.sh | 5 ++++- saw-remote-api/Dockerfile | 2 +- saw/Dockerfile | 2 +- 6 files changed, 16 insertions(+), 4 deletions(-) diff --git a/.github/ci.sh b/.github/ci.sh index 404e10af13..cfb455efce 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.10 and 4.8.14 so that we can fall + # back to 4.8.10 (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.10" 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 3a634279e0..be130c4d65 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-20221205" OCAML_VERSION: 4.09.x diff --git a/s2nTests/scripts/awslc-entrypoint.sh b/s2nTests/scripts/awslc-entrypoint.sh index afe2953913..df5cd3ffe0 100755 --- a/s2nTests/scripts/awslc-entrypoint.sh +++ b/s2nTests/scripts/awslc-entrypoint.sh @@ -6,6 +6,9 @@ cd /saw-script/aws-lc-verification/SAW rm bin/saw cp /saw-bin/saw bin/saw cp /saw-bin/abc bin/abc +# Z3 4.8.14 has been known to nondeterministically time out with the AWSLC +# proofs, so fall back to 4.8.10 instead. See #1772. +cp /saw-bin/z3-4.8.10 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..d29529b23b 100755 --- a/s2nTests/scripts/blst-entrypoint.sh +++ b/s2nTests/scripts/blst-entrypoint.sh @@ -5,9 +5,12 @@ cd /workdir ./scripts/install.sh 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" +wget --quiet -O solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20221205/ubuntu-22.04-bin.zip" (cd bin && unzip -o ../solvers.zip) chmod +x bin/* +# Z3 4.8.14 has been known to nondeterministically time out with the BLST +# proofs, so fall back to 4.8.10 instead. See #1772. +cp bin/z3-4.8.10 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..79171ca857 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-20221205/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..5ab6ebd6d1 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-20221205/ubuntu-22.04-bin.zip" RUN unzip solvers.zip && rm solvers.zip && chmod +x * USER root RUN chown -R root:root /home/saw/rootfs