improve test_solver_cache_stats args, clean up debugging code, add docs

intTests/test_solver_cache/test_basics.saw

@@ -4,38 +4,38 @@ enable_experimental;
 enable_solver_cache;
 
 // The solver cache starts out empty
-test_solver_cache_stats [0, 0, 0, 0, 0];
+test_solver_cache_stats 0 false 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];
+test_solver_cache_stats 1 false 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];
+test_solver_cache_stats 1 false 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];
+test_solver_cache_stats 2 false 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];
+test_solver_cache_stats 3 false 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];
+test_solver_cache_stats 4 false 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];
+test_solver_cache_stats 4 false 2 0 4 0;
 
 fails (prove_print w4 {{ \(x:[64])(y:[64]) -> x == y }});
-test_solver_cache_stats [5, 2, 0, 5, 0];
+test_solver_cache_stats 5 false 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];
+test_solver_cache_stats 6 false 2 0 6 0;

intTests/test_solver_cache/test_clean.saw

@@ -4,14 +4,14 @@ enable_experimental;
 set_solver_cache_path "test.cache";
 
 // The cache still has entries from prior runs
-test_solver_cache_stats [6, 0, 0, 0, 0];
+test_solver_cache_stats 6 true 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];
+test_solver_cache_stats 4 true 0 0 0 0;
 
 // After running test_path_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_path_ops.saw";
-test_solver_cache_stats [6, 6, 0, 2, 0];
+test_solver_cache_stats 6 true 6 0 2 0;

intTests/test_solver_cache/test_env_var.saw

@@ -4,7 +4,7 @@ enable_experimental;
 
 // The same as test_path_second.saw
 
-test_solver_cache_stats [6, 0, 0, 0, 0];
+test_solver_cache_stats 6 true 0 0 0 0;
 
 include "test_path_ops.saw";
-test_solver_cache_stats [6, 8, 0, 0, 0];
+test_solver_cache_stats 6 true 8 0 0 0;

intTests/test_solver_cache/test_path_first.saw

@@ -4,9 +4,9 @@ enable_experimental;
 set_solver_cache_path "test.cache";
 
 // The solver cache starts out empty
-test_solver_cache_stats [0, 0, 0, 0, 0];
+test_solver_cache_stats 0 true 0 0 0 0;
 
 // After running test_path_ops, we should have as many insertions as we have
 // entries in the cache, as well as a couple usages
 include "test_path_ops.saw";
-test_solver_cache_stats [6, 2, 0, 6, 0];
+test_solver_cache_stats 6 true 2 0 6 0;

intTests/test_solver_cache/test_path_second.saw

@@ -4,10 +4,10 @@ enable_experimental;
 set_solver_cache_path "test.cache";
 
 // The cache still has entries from the last run
-test_solver_cache_stats [6, 0, 0, 0, 0];
+test_solver_cache_stats 6 true 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_path_ops.saw";
-test_solver_cache_stats [6, 8, 0, 0, 0];
+test_solver_cache_stats 6 true 8 0 0 0;

src/SAWScript/Interpreter.hs

@@ -665,6 +665,11 @@ clean_solver_cache = do
   vs <- io $ getSolverBackendVersions allBackends
   onSolverCache (cleanSolverCache vs)
 
+test_solver_cache_stats :: Integer -> Bool -> Integer -> Integer -> Integer ->
+                           Integer -> TopLevel ()
+test_solver_cache_stats sz p ls ls_f is is_f =
+  onSolverCache (testSolverCacheStats sz p ls ls_f is is_f)
+
 enable_debug_intrinsics :: TopLevel ()
 enable_debug_intrinsics = do
   rw <- getTopLevelRW
@@ -1088,48 +1093,57 @@ primitives = Map.fromList
   , prim "enable_solver_cache" "TopLevel ()"
     (pureVal enable_solver_cache)
     Experimental
-    [ "Enable solver result caching. Unless set_solver_cache_path is"
-    , " later called, the cache will not persist between sessions."
+    [ "Enable solver result caching, if it is not already enabled. Unless"
+    , "set_solver_cache_path is later called, the cache will not persist"
+    , "between sessions. Requires Python 3 to be installed."
     ]
 
   , prim "set_solver_cache_path" "String -> TopLevel ()"
     (pureVal set_solver_cache_path)
     Experimental
-    [ "Enable solver result caching if it is not already enabled, set a"
-    , " path to use for loading and saving cached results, and save to"
-    , " that path any results cached so far from the current session."
+    [ "Enable solver result caching if it is not already enabled, open an"
+    , "LMDB database at the given path, save to that database all results in"
+    , "the current cache, then use that database as the cache going forward."
+    , "Requires Python 3 and the Python lmdb library to be installed."
     ]
 
   , prim "clean_solver_cache" "TopLevel ()"
     (pureVal clean_solver_cache)
     Experimental
     [ "Remove all entries in the solver result cache which were created"
-    , " using solver backend version(s) which do not match the version(s)"
-    , " in the current environment."
+    , "using solver backend versions which do not match the versions"
+    , "in the current environment."
     ]
 
   , prim "print_solver_cache" "String -> TopLevel ()"
     (pureVal (onSolverCache . printSolverCacheByHex))
     Experimental
     [ "Print all entries in the solver result cache whose SHA256 hash"
-    , " keys start with the given string. Thus, given an empty string,"
-    , " all entries in the cache will be printed."
+    , "keys start with the given string. Providing an empty string results"
+    , "in all entries in the cache being printed."
     ]
 
   , prim "print_solver_cache_stats" "TopLevel ()"
     (pureVal (onSolverCache printSolverCacheStats))
     Experimental
-    [ "Print out statistics about how the solver cache was used, namely"
-    , " how many entries are in the cache, how many insertions into the"
-    , " cache have been made so far this session, and how many times"
-    , " cached results have been used so far this session." ]
-
-  , prim "test_solver_cache_stats" "[Int] -> TopLevel ()"
-    (pureVal (onSolverCache . testSolverCacheStats))
-    Experimental
-    [ "Check whether the values of the statistics printed out by"
-    , " print_solver_cache_stats are equal to those given, failing if"
-    , " this does not hold. Used for testing." ]
+    [ "Print out statistics about how the solver cache has been used, namely"
+    , "how many entries are in the cache, whether the cache is being stored"
+    , "in memory or on disk, how many insertions into the cache have been made"
+    , "so far this session, how many failed insertion attempts have been made"
+    , "so far this session, how times cached results have been used so far this"
+    , "session, and with how many failed attempted usages have occurred so far"
+    , "this session." ]
+
+  , prim "test_solver_cache_stats" "Int -> Bool -> Int -> Int -> Int -> Int -> TopLevel ()"
+    (pureVal test_solver_cache_stats)
+    Experimental
+    [ "Test whether the values of the statistics printed out by"
+    , "print_solver_cache_stats are equal to those given, failing if"
+    , "this does not hold. Specifically, the arguments represent how many"
+    , "entries are in the cache, whether the cache is being stored on disk,"
+    , "how many insertions into the cache have been made, how many failed"
+    , "insertion attempts have been made, how times cached results have"
+    , "been used, and how many failed attempted usages have occurred." ]
 
   , prim "enable_debug_intrinsics" "TopLevel ()"
     (pureVal enable_debug_intrinsics)

src/SAWScript/SolverCache.hs

@@ -74,7 +74,7 @@ import GHC.Generics (Generic)
 import Data.IORef (IORef, newIORef, modifyIORef, readIORef)
 import Data.Tuple.Extra (first, firstM, both)
 import Data.List (isPrefixOf, elemIndex, intercalate)
-import Data.Maybe (fromMaybe)
+import Data.Maybe (fromMaybe, isJust)
 import Data.Functor ((<&>))
 
 import Data.Map.Strict (Map)
@@ -144,20 +144,25 @@ tryWithTimeout t_ms m = try (timeout (t_ms * 1000) m) <&> \case
 
 -- Solver Backends -------------------------------------------------------------
 
--- | A datatype representing one of the solver backends available in SAW. Note
--- that for 'SBV' and 'W4', multiple backends will be used (e.g. 'SBV' with
+-- | A datatype including all solver backends currently supported by SAW. This
+-- type is most often used in a list (@[SolverBackend]@), since at least one
+-- other backend is always used along with 'What4' or 'SBV' (e.g. 'SBV' with
 -- 'Z3' or 'W4' with 'AIG' and 'ABC').
+-- NOTE: This definition includes all backends supported by SBV, even though not
+-- all of them are currently supported by SAW (namely, 'Bitwuzla' and 'DReal').
+-- This is to ensure the system for keeping track of solver backend versions
+-- is not silently broken if support for these backends is ever added to SAW.
 data SolverBackend = What4
                    | SBV
                    | AIG
                    | RME
-                   -- External solvers (copied from SBV.Solver)
+                   -- External solvers supported by SBV (copied from SBV.Solver)
                    | ABC
                    | Boolector
-                   | Bitwuzla
+                   | Bitwuzla -- NOTE: Not currently supported by SAW
                    | CVC4
                    | CVC5
-                   | DReal
+                   | DReal -- NOTE: Not currently supported by SAW
                    | MathSAT
                    | Yices
                    | Z3
@@ -347,8 +352,11 @@ fromSolverCacheValue satq (SolverCacheValue _ _ solver_name cexs) =
 
 -- The Solver Cache ------------------------------------------------------------
 
--- | A 'SolverCacheDB' of cached solver results as well as counters for how
--- many cache hits and how many new entry creations have occurred
+-- | A 'SolverCacheDB' of cached solver results, a timeout in milliseconds to
+-- use for all lookups and insertions into the DB, as well as counters for how
+-- many lookups, failed lookups, insertions, and failed insertions have been
+-- made (see 'SolverCacheStat'). The latter are represented as an 'IORef' to
+-- make sure failures are counted correctly.
 data SolverCache =
   SolverCache
   { solverCacheDB      :: LMDBOptDatabase SolverCacheValue
@@ -378,7 +386,7 @@ lookupInSolverCache k = (Just Nothing,) $ \opts SolverCache{..} ->
                  (LMDBOpt.lookup (solverCacheKeyHash k)
                                  solverCacheDB) >>= \case
     Right (Just v) -> do
-      printOutLn opts Info ("Using cached result: " ++ show k)
+      printOutLn opts Debug ("Using cached result: " ++ show k)
       modifyIORef solverCacheStats $ M.adjust (+1) Lookups
       return (Just v)
     Left err -> do
@@ -391,7 +399,7 @@ lookupInSolverCache k = (Just Nothing,) $ \opts SolverCache{..} ->
 -- | Add a 'SolverCacheValue' to the solver result cache
 insertInSolverCache :: SolverCacheKey -> SolverCacheValue -> SolverCacheOp ()
 insertInSolverCache k v = (Just (),) $ \opts SolverCache{..} ->
-  printOutLn opts Info ("Caching result: " ++ show k) >>
+  printOutLn opts Debug ("Caching result: " ++ show k) >>
   tryWithTimeout solverCacheTimeout
                  (LMDBOpt.insert (solverCacheKeyHash k) v
                                  solverCacheDB) >>= \case
@@ -472,17 +480,21 @@ printSolverCacheStats = (Nothing,) $ \opts SolverCache{..} -> do
 -- | Check whether the values of the statistics printed out by
 -- 'printSolverCacheStats' are equal to those given, failing if this does not
 -- hold
-testSolverCacheStats :: [Integer] -> SolverCacheOp ()
-testSolverCacheStats ex = (Nothing,) $ \opts SolverCache{..} -> do
-  sz <- fromIntegral <$> LMDBOpt.size solverCacheDB
-  test sz 0 "Size of"
+testSolverCacheStats :: Integer -> Bool -> Integer -> Integer -> Integer ->
+                        Integer -> SolverCacheOp ()
+testSolverCacheStats sz p ls ls_f is is_f = (Nothing,) $ \opts SolverCache{..} -> do
+  sz_actual <- fromIntegral <$> LMDBOpt.size solverCacheDB
+  test sz sz_actual "Size of solver cache"
+  p_actual <- isJust <$> LMDBOpt.getPath solverCacheDB
+  test p p_actual "Whether solver cache saved to disk"
   stats <- readIORef solverCacheStats
-  test (stats M.! Lookups) 1 "Number of usages of"
-  test (stats M.! FailedLookups) 2 "Number of failed usages of"
-  test (stats M.! Inserts) 3 "Number of insertions into"
-  test (stats M.! FailedInserts) 4 "Number of failed insertions into"
-  printOutLn opts Info $ "Solver cache stats matched expected (" ++
-                         intercalate ", " (show <$> ex) ++ ")"
-  where test v i str = when (length ex > i && v /= ex !! i) $ fail $
-          str ++ " solver cache (" ++ show v ++ ") did not match expected" ++
-                              " (" ++ show (ex !! i) ++ ")"
+  test ls (stats M.! Lookups) "Number of usages of solver cache"
+  test ls_f (stats M.! FailedLookups) "Number of failed usages of solver cache"
+  test is (stats M.! Inserts) "Number of insertions into solver cache"
+  test is_f (stats M.! FailedInserts) "Number of failed insertions into solver cache"
+  printOutLn opts Info $ "Solver cache stats matched expected (" ++ show sz ++
+                         (if p then " true " else " false ") ++ show ls ++ " " ++
+                         show ls_f ++ " " ++ show is ++ " " ++ show is_f ++ ")"
+  where test v v_actual str = when (v /= v_actual) $ fail $
+          str ++ " (" ++ show v_actual ++ ")"
+              ++ " did not match expected (" ++ show v ++ ")"

src/SAWScript/SolverCache/lmdb_opt_database.py

@@ -161,33 +161,31 @@ def pHex(v):
   """Print the given value as a hex string, if it is a ``bytes`` object"""
   if isinstance(v, bytes): print(v.hex())
 
-def pJSONHex(obj, pretty = False):
+def pJSONHex(obj):
   """Serialize the given object as JSON to get a ``bytes`` object then print
      the result as a hex string"""
   print(bytes(json.dumps(obj), 'utf-8').hex())
 
-def pHexPair(v1, v2, pretty = False):
+def pHexPair(v1, v2):
   """Print the given pair of values as a hex strings, if both are ``bytes``
-     objects. For the second element, if ``pretty`` is ``True``, deserialise it
-     as JSON and print that instead."""
+     objects."""
   if isinstance(v1, bytes) and isinstance(v2, bytes):
-    print(v1.hex(), json.loads(v2) if pretty else v2.hex())
+    print(v1.hex(), v2.hex())
 
-def pHexJSONPair(v1, obj2, pretty = False):
-  """Print the given pair of values as a hex strings, if the first element is a
-     ``bytes`` object. For the second element, if ``pretty`` is ``True``, print
-     it directly, otherwise serialize it as JSON to get a ``bytes`` object and
-     use that to print its hex string."""
+def pHexJSONPair(v1, obj2):
+  """Print the given pair of values as a hex strings, if the first element is
+     a ``bytes`` object. For the second element, serialize it as JSON to get a
+     ``bytes`` object and use that to print its hex string."""
   if isinstance(v1, bytes):
-    print(v1.hex(), obj2 if pretty else bytes(json.dumps(obj2), 'utf-8').hex())
+    print(v1.hex(), bytes(json.dumps(obj2), 'utf-8').hex())
 
-def pHexPairs(vprs, pretty = False):
+def pHexPairs(vprs):
   """Print each pair in a given iterable using ``pHexPair``"""
-  for v1, v2 in vprs: pHexPair(v1, v2, pretty)
+  for v1, v2 in vprs: pHexPair(v1, v2)
 
-def pHexJSONPairs(vobjprs, pretty = False):
+def pHexJSONPairs(vobjprs):
   """Print each pair in a given iterable using ``pHexJSONPair``"""
-  for v1, obj2 in vobjprs: pHexJSONPair(v1, obj2, pretty)
+  for v1, obj2 in vobjprs: pHexJSONPair(v1, obj2)
 
 # ------------------------------------------------------------------------------
 # Interactive Shell Interface