Use prebuilt what4-solvers binaries (#1454)

* Use prebuilt what4-solvers binaries * Don't try to build ABC anymore (and remove submodule) * Don't use lazy file reading * Temporarily disable test_external_abc * Build Docker images on manual trigger
GaloisInc · Oct 1, 2021 · 5b6264b · 5b6264b
1 parent ffcaeb3
commit 5b6264b
Show file tree

Hide file tree

Showing 7 changed files with 28 additions and 115 deletions.
diff --git a/.github/ci.sh b/.github/ci.sh
@@ -50,61 +50,6 @@ setup_dist_bins() {
   strip dist/bin/saw* || echo "Strip failed: Ignoring harmless error"
 }
 
-install_z3() {
-  is_exe "$BIN" "z3" && return
-
-  case "$RUNNER_OS" in
-    Linux) file="ubuntu-18.04.zip" ;;
-    macOS) file="osx-10.15.7.zip" ;;
-    Windows) file="win.zip" ;;
-  esac
-  curl -o z3.zip -sL "https://github.com/Z3Prover/z3/releases/download/z3-$Z3_VERSION/z3-$Z3_VERSION-x64-$file"
-
-  if $IS_WIN; then 7z x -bd z3.zip; else unzip z3.zip; fi
-  cp z3-*/bin/z3$EXT $BIN/z3$EXT
-  $IS_WIN || chmod +x $BIN/z3
-  rm z3.zip
-}
-
-install_cvc4() {
-  is_exe "$BIN" "cvc4" && return
-  version="${CVC4_VERSION#4.}" # 4.y.z -> y.z
-
-  case "$RUNNER_OS" in
-    Linux) file="x86_64-linux-opt" ;;
-    Windows) file="win64-opt.exe" ;;
-    macOS) file="macos-opt" ;;
-  esac
-  # Temporary workaround
-  if [[ "$RUNNER_OS" == "Linux" ]]; then
-    curl -o cvc4$EXT -sL "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/cvc4-2020-08-18-x86_64-linux-opt"
-  else
-    curl -o cvc4$EXT -sL "https://github.com/CVC4/CVC4/releases/download/$version/cvc4-$version-$file"
-  fi
-  $IS_WIN || chmod +x cvc4$EXT
-  mv cvc4$EXT "$BIN/cvc4$EXT"
-}
-
-install_yices() {
-  is_exe "$BIN" "yices" && return
-  ext=".tar.gz"
-  case "$RUNNER_OS" in
-    Linux) file="pc-linux-gnu-static-gmp.tar.gz" ;;
-    macOS) file="apple-darwin18.7.0-static-gmp.tar.gz" ;;
-    Windows) file="pc-mingw32-static-gmp.zip" && ext=".zip" ;;
-  esac
-  curl -o "yices$ext" -sL "https://yices.csl.sri.com/releases/$YICES_VERSION/yices-$YICES_VERSION-x86_64-$file"
-
-  if $IS_WIN; then
-    7z x -bd "yices$ext"
-    mv "yices-$YICES_VERSION"/bin/*.exe "$BIN"
-  else
-    tar -xzf "yices$ext"
-    (cd "yices-$YICES_VERSION" && sudo ./install-yices)
-  fi
-  rm -rf "yices$ext" "yices-$YICES_VERSION"
-}
-
 build() {
   ghc_ver="$(ghc --numeric-version)"
   cp cabal.GHC-"$ghc_ver".config cabal.project.freeze
@@ -128,24 +73,10 @@ build() {
   fi
 }
 
-build_abc() {
-  arch=X86_64
-  case "$RUNNER_OS" in
-    Linux) os="Linux" ;;
-    macOS) os="OSX" ;;
-    Windows) os="Windows" ;;
-  esac
-  (cd deps/abcBridge &&
-    scripts/build-abc.sh $arch $os &&
-    cp abc-build/abc $BIN/abc)
-  output path $BIN/abc
-}
-
 install_system_deps() {
-  install_z3 &
-  install_cvc4 &
-  install_yices &
-  wait
+  (cd $BIN && curl -o bins.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/$SOLVER_PKG_VERSION/$BIN_ZIP_FILE" && unzip -o bins.zip && rm bins.zip)
+  chmod +x $BIN/*
+  cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT
   export PATH="$BIN:$PATH"
   echo "$BIN" >> "$GITHUB_PATH"
   is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" yices

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -10,14 +10,13 @@ on:
 
 env:
   CACHE_VERSION: 1
+  DISABLED_TESTS: "test0000 test_FNV_a1_rev test0010_jss_cnf_exp test0039_rust test_boilerplate test_external_abc"
 
   # Solver versions - also update in the following locations:
   # ./saw/Dockerfile
   # ./saw-remote-api/Dockerfile
   # ./s2nTests/docker/saw.dockerfile
-  Z3_VERSION: "4.8.10"
-  CVC4_VERSION: "4.1.8"
-  YICES_VERSION: "2.6.2"
+  SOLVER_PKG_VERSION: "snapshot-20210917"
 
   OCAML_VERSION: 4.09.x
 
@@ -71,8 +70,7 @@ jobs:
 
       - uses: actions/checkout@v2
       - run: |
-          git submodule update --init
-          git -C deps/abcBridge submodule update --init
+           git submodule update --init
 
       - id: config
         shell: bash
@@ -105,11 +103,6 @@ jobs:
             saw/SAWScript/Version.hs
           rm -f saw/SAWScript/Version.hs.bak
 
-      - id: abc
-        shell: bash
-        run: .github/ci.sh build_abc
-        if: runner.os != 'Windows'
-
       - shell: bash
         run: .github/ci.sh build
 
@@ -121,14 +114,6 @@ jobs:
             cryptol-saw-core-tc-test
           dest: dist-tests
 
-      - if: |
-          matrix.ghc == '8.10.3' &&
-          runner.os != 'Windows'
-        uses: actions/upload-artifact@v2
-        with:
-          path: ${{ steps.abc.outputs.path }}
-          name: abc-${{ runner.os }}
-
       - uses: actions/upload-artifact@v2
         if: "matrix.ghc == '8.10.3'"
         with:
@@ -185,6 +170,8 @@ jobs:
 
       - shell: bash
         run: .github/ci.sh install_system_deps
+        env:
+          BIN_ZIP_FILE: ${{ matrix.os }}-bin.zip
 
       - uses: actions/download-artifact@v2
         with:
@@ -236,18 +223,14 @@ jobs:
 
       - shell: bash
         run: .github/ci.sh install_system_deps
+        env:
+          BIN_ZIP_FILE: ${{ matrix.os }}-bin.zip
 
       - uses: actions/download-artifact@v2
         with:
           name: "${{ runner.os }}-bins"
           path: dist/bin
 
-      - if: runner.os != 'Windows'
-        uses: actions/download-artifact@v2
-        with:
-          path: dist/bin
-          name: abc-${{ runner.os }}
-
       - uses: actions/setup-python@v2
         with:
           python-version: '3.9'
@@ -284,6 +267,7 @@ jobs:
             continue-on-error: true  # https://github.com/GaloisInc/saw-script/issues/1135
           - suite: integration_tests
             os: windows-latest
+            timeout-minutes: 60
             continue-on-error: true  # https://github.com/GaloisInc/saw-script/issues/1135
         exclude:
           - suite: integration_tests
@@ -299,6 +283,8 @@ jobs:
 
       - shell: bash
         run: .github/ci.sh install_system_deps
+        env:
+          BIN_ZIP_FILE: ${{ matrix.os }}-bin.zip
 
       - uses: actions/download-artifact@v2
         with:
@@ -309,12 +295,6 @@ jobs:
         if: "runner.os != 'Windows'"
         run: chmod +x dist/bin/*
 
-      - if: runner.os != 'Windows'
-        uses: actions/download-artifact@v2
-        with:
-          path: bin
-          name: abc-${{ runner.os }}
-
       - shell: bash
         if: runner.os != 'Windows'
         run: chmod +x bin/*
@@ -345,7 +325,7 @@ jobs:
   build-push-image:
     runs-on: ubuntu-latest
     needs: [config]
-    if: github.event_name == 'schedule'
+    if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
     strategy:
       fail-fast: false
       matrix:
@@ -470,14 +450,11 @@ jobs:
           name: "saw-Linux-${{ matrix.ghc }}"
           path: ./s2nTests/bin
 
-      - uses: actions/download-artifact@v2
-        with:
-          path: ./s2nTests/bin
-          name: abc-${{ runner.os }}
-
       - shell: bash
         working-directory: s2nTests
         run: |
+          curl -o solvers-bin.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/$SOLVER_PKG_VERSION/ubuntu-18.04-bin.zip"
+          (cd bin && unzip ../solvers-bin.zip)
           docker-compose pull
           grep -h '^FROM' docker/*.dockerfile | sort -u | awk '{print $2}' | xargs -n1 -P8 docker pull
 

diff --git a/.gitmodules b/.gitmodules
@@ -1,6 +1,3 @@
-[submodule "deps/abcBridge"]
-	path = deps/abcBridge
-	url = https://github.com/GaloisInc/abcBridge.git
 [submodule "deps/aig"]
 	path = deps/aig
 	url = https://github.com/GaloisInc/aig.git

diff --git a/deps/abcBridge b/deps/abcBridge
diff --git a/s2nTests/docker/blst.dockerfile b/s2nTests/docker/blst.dockerfile
@@ -14,4 +14,4 @@ WORKDIR /workdir
 
 COPY scripts/blst-entrypoint.sh /entrypoint.sh
 ENTRYPOINT [ "/entrypoint.sh" ]
-CMD [ "/bin/bash" ]
+CMD [ "/bin/bash" ]
diff --git a/s2nTests/scripts/blst-entrypoint.sh b/s2nTests/scripts/blst-entrypoint.sh
@@ -4,11 +4,19 @@ set -xe
 cd /workdir
 ./scripts/install.sh
 cp /saw-bin/saw bin/saw
-cp /saw-bin/abc bin/abc
+
+wget --quiet -O solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20210917/ubuntu-20.04-bin.zip"
+(cd bin && unzip -o ../solvers.zip)
+chmod +x bin/*
 
 export PATH=/workdir/bin:$PATH
 export CRYPTOLPATH=/workdir/cryptol-specs:/workdir/spec
 
+abc -h || true
+z3 --version
+yices --version
+yices-smt2 --version
+
 ./scripts/build_x86.sh
 ./scripts/build_llvm.sh
 

diff --git a/src/SAWScript/Prover/ABC.hs b/src/SAWScript/Prover/ABC.hs
@@ -7,6 +7,7 @@ module SAWScript.Prover.ABC
 
 import Control.Monad (unless)
 import Control.Monad.IO.Class
+import qualified Data.ByteString.Char8 as C8
 import Data.Char (isSpace)
 import Data.List (isPrefixOf)
 import qualified Data.Map as Map
@@ -120,7 +121,7 @@ w4AbcExternal exporter argFn unints _hashcons goal =
        let execName = "abc"
            args = ["-q", argFn tmp tmpCex]
        (_out, _err) <- liftIO $ readProcessExitIfFailure execName args
-       cexText <- liftIO $ readFile tmpCex
+       cexText <- liftIO $ C8.unpack <$> C8.readFile tmpCex
        liftIO $ removeFile tmp
        liftIO $ removeFile tmpCex