Solver result caching

.gitmodules

@@ -46,3 +46,6 @@
 [submodule "deps/language-sally"]
 	path = deps/language-sally
 	url = https://github.com/GaloisInc/language-sally
+[submodule "deps/lmdb"]
+	path = deps/lmdb
+	url = https://github.com/GaloisInc/lmdb.git

Setup.hs

@@ -1,11 +1,12 @@
 import Control.Exception
 import Control.Monad (unless)
+import Data.List (find)
 import Distribution.Simple
 import Distribution.Simple.BuildPaths (autogenPackageModulesDir)
 import Distribution.PackageDescription (emptyHookedBuildInfo, allBuildInfo)
-import System.Directory (createDirectoryIfMissing, findExecutable)
+import System.Directory
 import System.FilePath ((</>))
-import System.Process (readProcess)
+import System.Process (readProcess, callProcess)
 import System.Exit
 
 main = defaultMainWithHooks myHooks
@@ -17,20 +18,31 @@ myBuild pd lbi uh flags = do
 
   hasGit <- findExecutable "git"
 
-  let gitfailure :: SomeException -> IO String
-      gitfailure _e = return "<non-dev-build> "
+  let gitfailure :: a -> SomeException -> IO a
+      gitfailure a _e = return a
 
-  desc <- case hasGit of
-            Just git -> readProcess "git" ["describe", "--always", "--dirty"] ""
-                        `catch` gitfailure
-            Nothing -> return "<VCS-less build> "
+  let gitdescribe dir m on_no_exe on_fail = case hasGit of
+        Just exe -> withCurrentDirectory dir (m <$>
+                      readProcess "git" ["describe", "--always", "--dirty"] "")
+                    `catch` gitfailure on_fail
+        Nothing -> return on_no_exe
+
+  desc     <- gitdescribe "." init "<VCS-less build>" "<non-dev-build>"
+  aig_desc <- gitdescribe "deps/aig" (Just . init) Nothing Nothing
+  w4_desc  <- gitdescribe "deps/what4" (Just . init) Nothing Nothing
 
   writeFile (dir </> "GitRev.hs") $ unlines
     [ "module GitRev where"
+    , "-- | String describing the HEAD of saw-script at compile-time"
     , "hash :: String"
-    , "hash = " ++ show (init desc)
+    , "hash = " ++ show desc
+    , "-- | String describing the HEAD of the deps/aig submodule at compile-time"
+    , "aigHash :: Maybe String"
+    , "aigHash = " ++ show aig_desc
+    , "-- | String describing the HEAD of the deps/what4 submodule at compile-time"
+    , "what4Hash :: Maybe String"
+    , "what4Hash = " ++ show w4_desc
     ]
 
   unless (null $ allBuildInfo pd) $
     (buildHook simpleUserHooks) pd lbi uh flags
-

cabal.project

@@ -32,6 +32,8 @@ packages:
     deps/parameterized-utils
     deps/flexdis86
     deps/flexdis86/binary-symbols
+    deps/lmdb/lmdb
+    deps/lmdb/lmdb-simple
     deps/macaw/base
     deps/macaw/symbolic
     deps/macaw/x86

doc/manual/manual.md

@@ -109,6 +109,13 @@ SAW also uses several environment variables for configuration:
   or the `PATH` environment variable is used, as SAW can use this information
   to determine the location of the core Java libraries' `.jar` file.
 
+`SAW_SOLVER_CACHE_PATH`
+
+  ~ Specify a path at which to keep a cache of solver results obtained during
+  calls to certain tactics. A cache is not created at this path until it is
+  needed. See the section **Caching Solver Results** for more detail about this
+  feature.
+
 On Windows, semicolon-delimited lists are used instead of colon-delimited
 lists.
 
@@ -1244,6 +1251,100 @@ differences in how each library represents certain SMT queries. There are also
 some experimental features that are only supported with What4 at the moment,
 such as `enable_lax_loads_and_stores`.
 
+## Caching Solver Results
+
+SAW has the capability to cache the results of tactics which call out to
+automated provers. This can save a considerable amount of time in cases such as
+proof development and CI, where the same proof scripts are often run repeatedly
+without changes.
+
+This caching is available for all tactics which call out to automated provers
+at runtime: `abc`, `boolector`, `cvc4`, `cvc5`, `mathsat`, `yices`, `z3`,
+`rme`, and the family of `unint` tactics described in the previous section.
+
+When solver caching is enabled and one of the tactics mentioned above is
+encountered, if there is already an entry in the cache corresponding to the
+call then the cached result is used, otherwise the appropriate solver is
+queried, and the result saved to the cache. Entries are indexed by a SHA256
+hash of the exact query to the solver (ignoring variable names), any options
+passed to the solver, and the names and full version strings of all the solver
+backends involved (e.g. ABC and SBV for the `abc` tactic). This ensures cached
+results are only used when they would be identical to the result of actually
+running the tactic.
+
+The simplest way to enable solver caching is to set the environment variable
+`SAW_SOLVER_CACHE_PATH`. With this environment variable set, `saw` and
+`saw-remote-api` will automatically keep an [LMDB](http://www.lmdb.tech/doc/)
+database at the given path containing the solver result cache. Setting this
+environment variable globally therefore creates a global, concurrency-safe
+solver result cache used by all newly created `saw` or `saw-remote-api`
+processes. Note that when this environment variable is set, SAW does not create
+a cache at the specified path until it is actually needed.
+
+There are also a number of SAW commands related to solver caching.
+
+* `set_solver_cache_path` is like setting `SAW_SOLVER_CACHE_PATH` for the
+  remainder of the current session, but opens an LMDB database at the specified
+  path immediately. If a cache is already in use in the current session
+  (i.e. through a prior call to `set_solver_cache_path` or through
+  `SAW_SOLVER_CACHE_PATH` being set and the cache being used at least once)
+  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.
+
+* `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
+  results in all entries in the cache being printed.
+
+* `print_solver_cache_stats` prints to the console statistics including the
+  size of the solver cache, where on disk it is stored, and some counts of how
+  often it has been used during the current session.
+
+For performing more complicated database operations on the set of cached
+results, the file `solver_cache.py` is provided with the Python bindings of the
+SAW Remote API. This file implements a general-purpose Python interface for
+interacting with the LMDB databases kept by SAW for solver caching.
+
+Below is an example of using solver caching with `saw -v Debug`. Only the
+relevant output is shown, the rest abbreviated with "...".
+
+~~~~
+sawscript> set_solver_cache_path "example.cache"
+sawscript> prove_print z3 {{ \(x:[8]) -> x+x == x*2 }}
+[22:13:00.832] Caching result: d1f5a76e7a0b7c01 (SBV 9.2, Z3 4.8.7 - 64 bit)
+...
+sawscript> prove_print z3 {{ \(new:[8]) -> new+new == new*2 }}
+[22:13:04.122] Using cached result: d1f5a76e7a0b7c01 (SBV 9.2, Z3 4.8.7 - 64 bit)
+...
+sawscript> prove_print (w4_unint_z3_using "qfnia" []) \
+                                  {{ \(x:[8]) -> x+x == x*2 }}
+[22:13:09.484] Caching result: 4ee451f8429c2dfe (What4 v1.3-29-g6c462cd using qfnia, Z3 4.8.7 - 64 bit)
+...
+sawscript> print_solver_cache "d1f5a76e7a0b7c01"
+[22:13:13.250] SHA: d1f5a76e7a0b7c01bdfe7d0e1be82b4f233a805ae85a287d45933ed12a54d3eb
+[22:13:13.250] - Result: unsat
+[22:13:13.250] - Solver: "SBV->Z3"
+[22:13:13.250] - Versions: SBV 9.2, Z3 4.8.7 - 64 bit
+[22:13:13.250] - Last used: 2023-07-25 22:13:04.120351 UTC
+
+sawscript> print_solver_cache "4ee451f8429c2dfe"
+[22:13:16.727] SHA: 4ee451f8429c2dfefecb6216162bd33cf053f8e66a3b41833193529449ef5752
+[22:13:16.727] - Result: unsat
+[22:13:16.727] - Solver: "W4 ->z3"
+[22:13:16.727] - Versions: What4 v1.3-29-g6c462cd using qfnia, Z3 4.8.7 - 64 bit
+[22:13:16.727] - Last used: 2023-07-25 22:13:09.484464 UTC
+
+sawscript> print_solver_cache_stats
+[22:13:20.585] == Solver result cache statistics ==
+[22:13:20.585] - 2 results cached in example.cache
+[22:13:20.585] - 2 insertions into the cache so far this run (0 failed attempts)
+[22:13:20.585] - 1 usage of cached results so far this run (0 failed attempts)
+~~~~
+
 ## Other External Provers
 
 In addition to the built-in automated provers already discussed, SAW

intTests/test_solver_cache/test.sh

@@ -0,0 +1,34 @@
+set -e
+
+# Testing the basic features of the solver cache
+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`
+pip install cbor2 lmdb
+python3 -m lmdb -e test_solver_cache.cache shell << END
+import cbor2
+with ENV.begin(write=True) as txn:
+  for k_enc, v_enc in txn.cursor():
+    k, v = cbor2.loads(k_enc), cbor2.loads(v_enc)
+    if 'vs' in v and 'SBV' in v['vs']:
+      v['vs']['SBV'] = '[OLD VERSION]'
+      txn.put(k_enc, cbor2.dumps(v))
+      print(f'Altered {k.hex()} {v}')
+    else:
+      print(f'Keeping {k.hex()} {v}')
+
+END
+$SAW test_clean.saw
+
+# Testing that the envionment variable only creates the cache file when needed
+rm -rf test_solver_cache.cache
+SAW_SOLVER_CACHE_PATH="test_solver_cache.cache" $SAW test_env_var.saw
+if [ -d "test_solver_cache.cache" ]; then
+  echo "FAILURE: Cache file created from SAW_SOLVER_CACHE_PATH when not used"; exit 1
+else
+  echo "SUCCESS: Cache file not created from SAW_SOLVER_CACHE_PATH when not used"
+fi

intTests/test_solver_cache/test_basics.saw

@@ -0,0 +1,38 @@
+// Testing the basic features of solver result caching
+
+// The solver cache starts out empty
+test_solver_cache_stats 0 0 0 0 0;
+
+// The cache should now have one entry and one insertion
+prove_print z3 {{ \(x:[64]) -> x == x }};
+test_solver_cache_stats 1 0 0 1 0;
+
+// Testing that cached results do not depend on variable names - thus, the
+// cache should now have one more usage, but not a new entry or insertion
+prove_print z3 {{ \(new_name:[64]) -> new_name == new_name }};
+test_solver_cache_stats 1 1 0 1 0;
+
+// Testing that cached results depend on the backend used - thus, the cache
+// should now have one more entry and one more insertion, but not a new usage
+prove_print (w4_unint_z3 []) {{ \(x:[64]) -> x == x }};
+test_solver_cache_stats 2 1 0 2 0;
+
+// Testing that cached results depend on the options passed to the given
+// backend - thus, the cache should now have one more entry and one more
+// insertion, but not a new usage
+prove_print (w4_unint_z3_using "qfnia" []) {{ \(x:[64]) -> x == x }};
+test_solver_cache_stats 3 1 0 3 0;
+
+// Same as the above but for sat results
+
+fails (prove_print z3 {{ \(x:[64])(y:[64]) -> x == y }});
+test_solver_cache_stats 4 1 0 4 0;
+
+fails (prove_print z3 {{ \(new_name_1:[64])(new_name_2:[64]) -> new_name_1 == new_name_2 }});
+test_solver_cache_stats 4 2 0 4 0;
+
+fails (prove_print w4 {{ \(x:[64])(y:[64]) -> x == y }});
+test_solver_cache_stats 5 2 0 5 0;
+
+fails (prove_print (w4_unint_z3_using "qfnia" []) {{ \(x:[64])(y:[64]) -> x == y }});
+test_solver_cache_stats 6 2 0 6 0;

intTests/test_solver_cache/test_clean.saw

@@ -0,0 +1,16 @@
+// Testing cleaning the solver cache
+
+set_solver_cache_path "test_solver_cache.cache";
+
+// The cache still has entries from prior runs
+test_solver_cache_stats 6 0 0 0 0;
+
+// After cleaning, all SBV entries should be removed (see test.sh)
+clean_solver_cache;
+test_solver_cache_stats 4 0 0 0 0;
+
+// After running test_ops, we should have all the original entries back,
+// as many insertions as there were SBV entries, and as many usages as there
+// were in test_path_second less the number of SBV entries
+include "test_ops.saw";
+test_solver_cache_stats 6 6 0 2 0;

intTests/test_solver_cache/test_env_var.saw

@@ -0,0 +1,3 @@
+// Testing setting the solver cache path through an envionment variable
+
+prove_print assume_valid {{ \(x:[64]) -> x == x }};

intTests/test_solver_cache/test_ops.saw

@@ -0,0 +1,8 @@
+prove_print z3 {{ \(x:[64]) -> x == x }};
+prove_print z3 {{ \(new_name:[64]) -> new_name == new_name }};
+prove_print (w4_unint_z3 []) {{ \(x:[64]) -> x == x }};
+prove_print (w4_unint_z3_using "qfnia" []) {{ \(x:[64]) -> x == x }};
+fails (prove_print z3 {{ \(x:[64])(y:[64]) -> x == y }});
+fails (prove_print z3 {{ \(new_name_1:[64])(new_name_2:[64]) -> new_name_1 == new_name_2 }});
+fails (prove_print w4 {{ \(x:[64])(y:[64]) -> x == y }});
+fails (prove_print (w4_unint_z3_using "qfnia" []) {{ \(x:[64])(y:[64]) -> x == y }});

intTests/test_solver_cache/test_path_and_reuse.saw

@@ -0,0 +1,12 @@
+// Testing the `set_solver_cache_path` command as well as re-using a cache file
+
+set_solver_cache_path "test_solver_cache.cache";
+
+// The cache still has entries from the last run
+test_solver_cache_stats 6 0 0 0 0;
+
+// After running test_path_ops, we should have the same number of entries, but
+// no insertions and and as many usages as there were insertions plus usages
+// the first time
+include "test_ops.saw";
+test_solver_cache_stats 6 8 0 0 0;

saw-core/saw-core.cabal

@@ -25,6 +25,7 @@ library
 
   build-depends:
     base >= 4.8,
+    aeson >= 2.0 && < 2.2,
     array,
     bytestring,
     containers,