Use solver result caching in CI (#1908)

Changes:
- Enable solver result caching on the CI for the integration tests and all the s2n tests
- Add a `--clean-mismatched-versions-solver-cache` command-line option to `saw` which provides a direct way to remove cache entries with out-of-date solver versions (this is run every time a cache is loaded on CI)
- Use the commit hash of the last commit to modify the `rme` directory as the version information for `rme` calls, instead of the commit hash of the entire repo (this ensures cached `rme` calls are actually used when CI is run on a later commit which does not modify the `rme` directory)

Commits:

* first try at turning on solver caching for intTests and s2nTests in CI

* add intTest which tests whether solver caching is even enabled

* use absolute paths for solver caching on CI

* fix dummy CI test file so it actually runs

* properly set SAW_SOLVER_CACHE_PATH env var in CI

* another attempt at setting SAW_SOLVER_CACHE_PATH on CI

* use github.ref instead of .sha for caching in CI, fix repeated key bug(?)

* make integration tests aware of SAW_SOLVER_CACHE_PATH env var

* enable solver caching for s2n tests; fix typo in ci.yml

* clean up solver caching bits in ci.yml, add debugging to blst

* remove debugging from intTests, tweak debugging for s2n-blst

* more tweaks to CI blst debugging and cache keys

* more CI solver caching debugging for s2n

* another attempt at enabling solver caching for s2n tests on CI

* add debugging back to s2n CI tests

* even more debugging for s2n CI solver caching

* tweak debugging for s2n CI solver caching

* the tweaks to s2n CI solver caching just keep coming...

* point the CI solver cache restore/save to the right place for s2n tests

* remove github.ref from cache keys, try to fix s2n cache permissions

* give read permissions to newly created s2n caches

* a different strategy for getting permissions for s2n solver cache

* add `-p` to mkdir in s2n solver caching

* fix typo preventing s2n solver caches from getting restored on CI

* set solver cache timeout to 2s, add print_solver_cache_stats to s2n tests

* change debugging method for solver caching on CI

* remove timeout in solver caching for debugging purposes

* add --clean-solver-cache CLI opt, clean up CI debugging

* update manual with --clean-solver-cache

* use RME-specific hash for solver versioning

* add docs to CACHE_VERSION env vars, add CABAL_ to original for clarity

* add "mismatched_versions" to "clean_solver_cache" command name

* rename cleanSolverCache, cleanCacheOpt to mention mismatched versions

.github/workflows/ci.yml

@@ -16,7 +16,16 @@ on:
   workflow_dispatch:
 
 env:
-  CACHE_VERSION: 1
+  # The CABAL_CACHE_VERSION and SOLVER_CACHE_VERSION environment variables
+  # can be updated to force the use of a new cabal or solver cache if the
+  # respective current cache contents become corrupted/invalid.  This can
+  # sometimes happen when (for example) the OS version is changed but
+  # older .so files are cached, which can have various effects
+  # (e.g. cabal complains it can't find a valid version of the "happy"
+  # tool).
+  CABAL_CACHE_VERSION: 1
+  SOLVER_CACHE_VERSION: 1
+
   DISABLED_TESTS: "test0000 test_FNV_a1_rev test0010_jss_cnf_exp test0039_rust test_boilerplate test_external_abc"
 
   # Solver package snapshot date - also update in the following locations:
@@ -119,9 +128,9 @@ jobs:
           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 }}
+          key: ${{ env.CABAL_CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-${{ github.sha }}
           restore-keys: |
-            ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-
+            ${{ env.CABAL_CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-
 
       - if: needs.config.outputs.release == 'true'
         shell: bash
@@ -211,8 +220,7 @@ jobs:
           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)) }}-
+          key: ${{ env.CABAL_CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-${{ github.sha }}
 
   mr-solver-tests:
     needs: [build]
@@ -421,13 +429,36 @@ jobs:
           java-package: jdk
           architecture: x64
 
+      - uses: actions/cache/restore@v3
+        name: Restore SMT solver result cache
+        if: "matrix.suite == 'integration_tests'"
+        with:
+          path: ${{ matrix.suite }}.cache
+          key: ${{ env.SOLVER_CACHE_VERSION }}-solver-${{ matrix.suite }}-${{ matrix.os }}-${{ github.sha }}
+          restore-keys: |
+            ${{ env.SOLVER_CACHE_VERSION }}-solver-${{ matrix.suite }}-${{ matrix.os }}-
+
+      - shell: bash
+        name: Enable solver caching
+        if: "matrix.suite == 'integration_tests'"
+        run: |
+          echo "SAW_SOLVER_CACHE_PATH=$(pwd)/${{ matrix.suite }}.cache" >> "$GITHUB_ENV"
+          dist/bin/saw --clean-mismatched-versions-solver-cache=$(pwd)/${{ matrix.suite }}.cache
+
       - name: ${{ matrix.suite }}
         continue-on-error: ${{ matrix.continue-on-error }}
         shell: bash
         run: |
           export PATH="$PWD/bin:$PWD/dist/bin:$PATH"
           dist-tests/${{ matrix.suite }}
 
+      - uses: actions/cache/save@v3
+        name: Save SMT solver result cache
+        if: "matrix.suite == 'integration_tests'"
+        with:
+          path: ${{ matrix.suite }}.cache
+          key: ${{ env.SOLVER_CACHE_VERSION }}-solver-${{ matrix.suite }}-${{ matrix.os }}-${{ github.sha }}
+
   build-push-image:
     runs-on: ubuntu-22.04
     needs: [config]
@@ -567,13 +598,30 @@ jobs:
         working-directory: s2nTests
         run: docker-compose build s2n
 
+      - uses: actions/cache/restore@v3
+        name: Restore SMT solver result cache
+        with:
+          path: s2nTests/cache
+          key: ${{ env.SOLVER_CACHE_VERSION }}-solver-s2n-${{ matrix.s2n-target }}-${{ matrix.ghc }}-${{ github.sha }}
+          restore-keys:
+            ${{ env.SOLVER_CACHE_VERSION }}-solver-s2n-${{ matrix.s2n-target }}-${{ matrix.ghc }}-
+
       - shell: bash
         name: "s2n tests: ${{ matrix.s2n-target }}"
         working-directory: s2nTests
         run: |
           chmod +x bin/*
+          mkdir -p cache && touch cache/data.mdb cache/lock.mdb
+          chmod -R +rw cache
           make ${{ matrix.s2n-target }}
 
+      - uses: actions/cache/save@v3
+        name: Save SMT solver result cache
+        if: always()
+        with:
+          path: s2nTests/cache
+          key: ${{ env.SOLVER_CACHE_VERSION }}-solver-s2n-${{ matrix.s2n-target }}-${{ matrix.ghc }}-${{ github.sha }}
+
   exercises:
     name: "Test SAW exercises"
     needs: build

Setup.hs

@@ -31,6 +31,11 @@ myBuild pd lbi uh flags = do
   aig_desc <- gitdescribe "deps/aig" (Just . init) Nothing Nothing
   w4_desc  <- gitdescribe "deps/what4" (Just . init) Nothing Nothing
 
+  rme_desc <- case hasGit of
+    Just exe -> (Just <$> readProcess "git" ["log", "--max-count=1", "--pretty=format:%h", "--", "rme"] "")
+                `catch` gitfailure Nothing
+    Nothing -> return Nothing
+
   writeFile (dir </> "GitRev.hs") $ unlines
     [ "module GitRev where"
     , "-- | String describing the HEAD of saw-script at compile-time"
@@ -42,6 +47,10 @@ myBuild pd lbi uh flags = do
     , "-- | String describing the HEAD of the deps/what4 submodule at compile-time"
     , "what4Hash :: Maybe String"
     , "what4Hash = " ++ show w4_desc
+    , "-- | String describing the most recent commit which modified the rme directory"
+    , "-- at compile-time"
+    , "rmeHash :: Maybe String"
+    , "rmeHash = " ++ show rme_desc
     ]
 
   unless (null $ allBuildInfo pd) $

doc/manual/manual.md

@@ -86,6 +86,15 @@ command-line options:
 
   ~ Set the verbosity level of the SAWScript interpreter.
 
+`--clean-mismatched-versions-solver-cache[=path]`
+
+  ~ Run the `clean_mismatched_versions_solver_cache` command on the solver
+  cache at the given path, or if no path is given, the solver cache at the
+  value of the `SAW_SOLVER_CACHE_PATH` environment variable, then exit. See
+  the section **Caching Solver Results** for a description of the
+  `clean_mismatched_versions_solver_cache` command and the solver caching
+  feature in general.
+
 SAW also uses several environment variables for configuration:
 
 `CRYPTOLPATH`
@@ -1297,10 +1306,12 @@ There are also a number of SAW commands related to solver caching.
   then all entries in the cache already in use will be copied to the new cache
   being opened.
 
-* `clean_solver_cache` will remove all entries in the solver result cache
-  which were created using solver backend versions which do not match the
-  versions in the current environment. This can be run after an update to
-  clear out any old, unusable entries from the solver cache.
+* `clean_mismatched_versions_solver_cache` will remove all entries in the
+  solver result cache which were created using solver backend versions which do
+  not match the versions in the current environment. This can be run after an
+  update to clear out any old, unusable entries from the solver cache. This
+  command can also be run directly from the command line through the
+  `--clean-mismatched-versions-solver-cache` command-line option.
 
 * `print_solver_cache` prints to the console all entries in the cache whose
   SHA256 hash keys start with the given hex string. Providing an empty string

intTests/IntegrationTest.hs

@@ -89,6 +89,7 @@ envVarAssocList = map envVarAssoc
 --     - JAVA_HOME = path to java installation
 --     - TESTBASE = path to intTests directory
 --     - SAW_JDK_JAR = path to rt.jar
+--     - SAW_SOLVER_CACHE_PATH = optional path to solver result cache
 --
 --  These environment variables may already be set to supply default
 --  locations for these components.
@@ -132,7 +133,8 @@ testParams intTestBase verbose = do
       addEnvVar evs e = do v <- lookupEnv e
                            return $ updEnvVars e (fromMaybe "" v) evs
   -- override eVars0 with any environment variables set in this process
-  e1 <- foldM addEnvVar eVars0 [ "SAW", "PATH", "JAVAC", "JAVA_HOME", "SAW_JDK_JAR" ]
+  e1 <- foldM addEnvVar eVars0 [ "SAW", "PATH", "SAW_SOLVER_CACHE_PATH",
+                                 "JAVAC", "JAVA_HOME", "SAW_JDK_JAR" ]
 
   -- Create a pathlist of jars for invoking saw
   let jarsDir = absTestBase </> "jars"

intTests/test_solver_cache/test.sh

@@ -6,8 +6,9 @@ SAW_SOLVER_CACHE_PATH="test_solver_cache.cache" $SAW test_basics.saw
 # Testing the `set_solver_cache_path` command as well as re-using a cache file
 $SAW test_path_and_reuse.saw
 
-# Testing the `clean_solver_cache` command by manually altering the version
-# string of all SBV entries in the database, then running `clean_solver_cache`
+# Testing the `clean_mismatched_versions_solver_cache` command by manually
+# altering the version string of all SBV entries in the database, then running
+# `clean_mismatched_versions_solver_cache`
 pip install cbor2 lmdb
 python3 -m lmdb -e test_solver_cache.cache shell << END
 import cbor2

intTests/test_solver_cache/test_clean.saw

@@ -6,7 +6,7 @@ set_solver_cache_path "test_solver_cache.cache";
 test_solver_cache_stats 6 0 0 0 0;
 
 // After cleaning, all SBV entries should be removed (see test.sh)
-clean_solver_cache;
+clean_mismatched_versions_solver_cache;
 test_solver_cache_stats 4 0 0 0 0;
 
 // After running test_ops, we should have all the original entries back,

s2nTests/docker-compose.yml

@@ -16,6 +16,7 @@ services:
     image: s2n
     volumes:
       - ${PWD:-.}/bin:/saw-bin:rw
+      - ${PWD:-.}/cache:/saw-cache:rw
 
   awslc:
     build:
@@ -24,6 +25,7 @@ services:
     image: awslc
     volumes:
       - ${PWD:-.}/bin:/saw-bin:rw
+      - ${PWD:-.}/cache:/saw-cache:rw
 
   blst:
     build:
@@ -32,3 +34,4 @@ services:
     image: blst
     volumes:
       - ${PWD:-.}/bin:/saw-bin:rw
+      - ${PWD:-.}/cache:/saw-cache:rw

s2nTests/scripts/awslc-entrypoint.sh

@@ -13,6 +13,8 @@ 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
+export SAW_SOLVER_CACHE_PATH=/saw-cache
+saw --clean-mismatched-versions-solver-cache
 
 ./scripts/entrypoint_check.sh
 

s2nTests/scripts/blst-entrypoint.sh

@@ -13,6 +13,8 @@ cp /saw-bin/z3-4.8.8 bin/z3
 
 export PATH=/workdir/bin:$PATH
 export CRYPTOLPATH=/workdir/cryptol-specs:/workdir/spec
+export SAW_SOLVER_CACHE_PATH=/saw-cache
+saw --clean-mismatched-versions-solver-cache
 
 abc -h || true
 z3 --version

s2nTests/scripts/s2n-entrypoint.sh

@@ -16,4 +16,6 @@ cp /saw-bin/abc "$SAW_INSTALL_DIR"/bin/abc
 export CFLAGS=-Wno-error=array-parameter
 export CLANG=clang
 export LLVMLINK=llvm-link
+export SAW_SOLVER_CACHE_PATH=/saw-cache
+"$SAW_INSTALL_DIR"/bin/saw --clean-mismatched-versions-solver-cache
 exec codebuild/bin/s2n_codebuild.sh

saw/Main.hs

@@ -25,6 +25,8 @@ import qualified SAWScript.REPL.Haskeline as REPL
 import qualified SAWScript.REPL.Monad as REPL
 import SAWScript.Version (shortVersionText)
 import SAWScript.Value (AIGProxy(..))
+import SAWScript.SolverCache
+import SAWScript.SolverVersions
 import qualified Data.AIG.CompactGraph as AIG
 
 main :: IO ()
@@ -40,6 +42,7 @@ main = do
       case files of
         _ | showVersion opts'' -> hPutStrLn stderr shortVersionText
         _ | showHelp opts'' -> err opts'' (usageInfo header options)
+        _ | Just path <- cleanMisVsCache opts'' -> doCleanMisVsCache opts'' path
         [] -> checkZ3 opts'' *> REPL.run opts''
         _ | runInteractively opts'' -> checkZ3 opts'' *> REPL.run opts''
         [file] -> checkZ3 opts'' *>
@@ -59,4 +62,10 @@ main = do
           when (verbLevel opts >= Error)
             (hPutStrLn stderr msg)
           exitProofUnknown
+        doCleanMisVsCache opts path | not (null path) = do
+          cache <- lazyOpenSolverCache path
+          vs <- getSolverBackendVersions allBackends
+          fst <$> solverCacheOp (cleanMismatchedVersionsSolverCache vs) opts cache
+        doCleanMisVsCache opts _ =
+          err opts "Error: either --clean-mismatched-versions-solver-cache must be given an argument or SAW_SOLVER_CACHE_PATH must be set"
 

src/SAWScript/Interpreter.hs

@@ -656,10 +656,10 @@ set_solver_cache_path path = do
     Nothing -> do cache <- io $ openSolverCache path
                   putTopLevelRW rw { rwSolverCache = Just cache }
 
-clean_solver_cache :: TopLevel ()
-clean_solver_cache = do
+clean_mismatched_versions_solver_cache :: TopLevel ()
+clean_mismatched_versions_solver_cache = do
   vs <- io $ getSolverBackendVersions allBackends
-  onSolverCache (cleanSolverCache vs)
+  onSolverCache (cleanMismatchedVersionsSolverCache vs)
 
 test_solver_cache_stats :: Integer -> Integer -> Integer -> Integer ->
                            Integer -> TopLevel ()
@@ -1097,8 +1097,8 @@ primitives = Map.fromList
     , "variable is ignored."
     ]
 
-  , prim "clean_solver_cache" "TopLevel ()"
-    (pureVal clean_solver_cache)
+  , prim "clean_mismatched_versions_solver_cache" "TopLevel ()"
+    (pureVal clean_mismatched_versions_solver_cache)
     Current
     [ "Remove all entries in the solver result cache which were created"
     , "using solver backend versions which do not match the versions"

src/SAWScript/Options.hs

@@ -13,6 +13,7 @@ module SAWScript.Options where
 
 import Data.Char (toLower)
 import Data.List (partition)
+import Data.Maybe (fromMaybe)
 import Data.Time
 import System.Console.GetOpt
 import System.Environment
@@ -39,6 +40,7 @@ data Options = Options
   , showVersion      :: Bool
   , printShowPos     :: Bool
   , useColor         :: Bool
+  , cleanMisVsCache  :: Maybe FilePath
   , printOutFn       :: Verbosity -> String -> IO ()
   , summaryFile      :: Maybe FilePath
   , summaryFormat    :: SummaryFormat
@@ -77,6 +79,7 @@ defaultOptions
     , showHelp = False
     , showVersion = False
     , useColor = True
+    , cleanMisVsCache = Nothing
     , summaryFile = Nothing
     , summaryFormat = Pretty
     }
@@ -156,6 +159,14 @@ options =
   , Option [] ["no-color"]
     (NoArg (\opts -> return opts { useColor = False }))
     "Disable ANSI color and Unicode output"
+  , Option [] ["clean-mismatched-versions-solver-cache"]
+    (OptArg
+     (\mb_path opts -> do
+        mb_env_path <- lookupEnv "SAW_SOLVER_CACHE_PATH"
+        let path = fromMaybe (fromMaybe "" mb_env_path) mb_path
+        return opts { cleanMisVsCache = Just path })
+     "path")
+    "Run clean_mismatched_versions_solver_cache with the cache given, or else the value of SAW_SOLVER_CACHE_PATH, then exit"
   , Option "s" ["summary"]
     (ReqArg
      (\file opts -> return opts { summaryFile = Just file })