Merge remote-tracking branch 'origin/master' into mrs-solver

Author: m-yac

.github/ci.sh

@@ -80,7 +80,7 @@ install_system_deps() {
   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
+  is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" cvc5 && is_exe "$BIN" yices
 }
 
 build_cryptol() {
@@ -127,6 +127,7 @@ zip_dist_with_solvers() {
   # dependencies) as the SAW binaries.
   cp "$BIN/abc"        dist/bin/
   cp "$BIN/cvc4"       dist/bin/
+  cp "$BIN/cvc5"       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

.github/workflows/ci.yml

@@ -68,27 +68,28 @@ jobs:
       fail-fast: false
       matrix:
         os: [ubuntu-22.04, macos-12, windows-latest]
-        ghc: ["8.8.4", "8.10.7", "9.0.2"]
+        cabal: ["3.8.1.0"]
+        ghc: ["8.8.4", "8.10.7", "9.2.7"]
         run-tests: [true]
         include:
+          # We include one job from an older Ubuntu LTS release to increase our
+          # coverage of possible Linux configurations. Since we already run the
+          # tests with the newest LTS release, we won't bother testing this one.
           - os: ubuntu-20.04
             ghc: "8.10.7"
+            cabal: "3.8.1.0"
             run-tests: false
         exclude:
           # Exclude 8.8 on macOS 12 due to
           # https://gitlab.haskell.org/ghc/ghc/-/issues/18446
           - os: macos-12
             ghc: "8.8.4"
+            cabal: "3.8.1.0"
             run-tests: true
           - os: windows-latest
             ghc: "8.8.4"
+            cabal: "3.8.1.0"
             run-tests: true
-          # Exclude 9.0 on Windows for now until
-          # https://github.com/commercialhaskell/stackage/issues/6400
-          # is resolved
-          - os: windows-latest
-            ghc: "9.0.2"
-            run-tests: false
     outputs:
       cabal-test-suites-json: ${{ steps.cabal-test-suites.outputs.targets-json }}
     steps:
@@ -108,6 +109,7 @@ jobs:
         id: setup-haskell
         with:
           ghc-version: ${{ matrix.ghc }}
+          cabal-version: ${{ matrix.cabal }}
 
       - name: Post-GHC installation fixups on Windows
         shell: bash
@@ -122,8 +124,8 @@ jobs:
         env:
           BUILD_TARGET_OS: ${{ matrix.os }}
 
-      - uses: actions/cache@v2
-        name: Cache cabal store
+      - uses: actions/cache/restore@v3
+        name: Restore cabal store cache
         with:
           path: |
             ${{ steps.setup-haskell.outputs.cabal-store }}
@@ -149,7 +151,7 @@ jobs:
           RELEASE: ${{ needs.config.outputs.release }}
         run: .github/ci.sh build_cryptol
 
-      - uses: GaloisInc/.github/actions/cabal-collect-bins@v1
+      - uses: GaloisInc/.github/actions/cabal-collect-bins@v1.1.1
         id: cabal-test-suites
         with:
           targets: |
@@ -213,6 +215,16 @@ jobs:
           path: dist/bin
           name: ${{ runner.os }}-bins
 
+      - uses: actions/cache/save@v3
+        name: Save cabal store cache
+        if: always()
+        with:
+          path: |
+            ${{ steps.setup-haskell.outputs.cabal-store }}
+            dist-newstyle
+          key: ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-${{ github.sha }}
+            ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-
+
   mr-solver-tests:
     needs: [build]
     strategy:
@@ -561,9 +573,6 @@ jobs:
           docker-compose pull
           grep -h '^FROM' docker/*.dockerfile | sort -u | awk '{print $2}' | xargs -n1 -P8 docker pull
 
-      - uses: jpribyl/[email protected]
-        continue-on-error: true
-
       - shell: bash
         name: "make s2n"
         working-directory: s2nTests
@@ -594,9 +603,6 @@ jobs:
           name: "${{ runner.os }}-bins"
           path: ./exercises/bin
 
-      - uses: jpribyl/[email protected]
-        continue-on-error: true
-
       - shell: bash
         name: "make exercises container"
         working-directory: exercises

CHANGES.md

@@ -90,6 +90,11 @@
   allows verification certain kinds of simple loops by using a
   user-provided loop invariant.
 
+* Add a `cvc5` family of proof scripts that use the CVC5 SMT solver.
+  (Note that the `sbv_cvc5` and `sbv_unint_cvc5` are non-functional
+  on Windows at this time due to a downstream issue with CVC5 1.0.4 and
+  earlier.)
+
 # Version 0.9
 
 ## New Features

README.md

@@ -42,7 +42,7 @@ To build SAWScript and related utilities from source:
   * Ensure that you have the `cabal` and `ghc` executables in your
     `PATH`. If you don't already have them, we recommend using `ghcup`
     to install them: <https://www.haskell.org/ghcup/>. We recommend
-    Cabal 3.4 or newer, and GHC 8.8, 8.10, or 9.0.
+    Cabal 3.4 or newer, and GHC 8.8, 8.10, or 9.2.
 
   * Ensure that you have the C libraries and header files for
     `terminfo`, which generally comes as part of `ncurses` on most