diff --git a/.gitmodules b/.gitmodules index 926212c99c..90b2fb191d 100644 --- a/.gitmodules +++ b/.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 diff --git a/Setup.hs b/Setup.hs index 10e9dc83a7..0722b80ccb 100644 --- a/Setup.hs +++ b/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 " " + 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 " " + 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 "" "" + 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 - diff --git a/cabal.project b/cabal.project index 7ed7119a69..4b3dc8753f 100644 --- a/cabal.project +++ b/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 diff --git a/deps/lmdb b/deps/lmdb new file mode 160000 index 0000000000..d454c81385 --- /dev/null +++ b/deps/lmdb @@ -0,0 +1 @@ +Subproject commit d454c8138587aa762bc19a8cb1b101f3379f8f3c diff --git a/doc/manual/manual.md b/doc/manual/manual.md index ff3555b46a..8b6c06eab6 100644 --- a/doc/manual/manual.md +++ b/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 diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf index 47e865b0ce..cd2df09cb7 100644 Binary files a/doc/manual/manual.pdf and b/doc/manual/manual.pdf differ diff --git a/intTests/test_solver_cache/test.sh b/intTests/test_solver_cache/test.sh new file mode 100644 index 0000000000..6364ddfc0f --- /dev/null +++ b/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 diff --git a/intTests/test_solver_cache/test_basics.saw b/intTests/test_solver_cache/test_basics.saw new file mode 100644 index 0000000000..436d54b759 --- /dev/null +++ b/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; diff --git a/intTests/test_solver_cache/test_clean.saw b/intTests/test_solver_cache/test_clean.saw new file mode 100644 index 0000000000..ff2a1bf47e --- /dev/null +++ b/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; diff --git a/intTests/test_solver_cache/test_env_var.saw b/intTests/test_solver_cache/test_env_var.saw new file mode 100644 index 0000000000..7b7a4f4e85 --- /dev/null +++ b/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 }}; diff --git a/intTests/test_solver_cache/test_ops.saw b/intTests/test_solver_cache/test_ops.saw new file mode 100644 index 0000000000..f7fa6b2930 --- /dev/null +++ b/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 }}); \ No newline at end of file diff --git a/intTests/test_solver_cache/test_path_and_reuse.saw b/intTests/test_solver_cache/test_path_and_reuse.saw new file mode 100644 index 0000000000..5efce48a0a --- /dev/null +++ b/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; diff --git a/saw-core/saw-core.cabal b/saw-core/saw-core.cabal index 9e6d9d77d9..f5be965b28 100644 --- a/saw-core/saw-core.cabal +++ b/saw-core/saw-core.cabal @@ -25,6 +25,7 @@ library build-depends: base >= 4.8, + aeson >= 2.0 && < 2.2, array, bytestring, containers, diff --git a/saw-core/src/Verifier/SAW/FiniteValue.hs b/saw-core/src/Verifier/SAW/FiniteValue.hs index 7a0c9c85dc..3f7db224a0 100644 --- a/saw-core/src/Verifier/SAW/FiniteValue.hs +++ b/saw-core/src/Verifier/SAW/FiniteValue.hs @@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveGeneric #-} {- | Module : Verifier.SAW.FiniteValue @@ -15,6 +16,7 @@ import Control.Applicative import Data.Traversable #endif +import GHC.Generics (Generic) import Control.Monad (mzero) import Control.Monad.Trans (lift) import Control.Monad.Trans.Maybe @@ -27,6 +29,9 @@ import Numeric.Natural (Natural) import Prettyprinter hiding (Doc) +import Data.Aeson ( FromJSON(..), ToJSON(..) ) +import qualified Data.Aeson as JSON + import qualified Verifier.SAW.Recognizer as R import Verifier.SAW.SharedTerm import Verifier.SAW.TypedAST @@ -50,6 +55,9 @@ data FiniteValue deriving Eq -- | First-order types that can be encoded in an SMT solver. +-- NB: The JSON encoding of this type, used for saw-script solver result caching, +-- assumes constructor names and argument orders will not change (though the +-- order and number of constructors may change) - see 'firstOrderJSONOptions' data FirstOrderType = FOTBit | FOTInt @@ -58,9 +66,12 @@ data FirstOrderType | FOTArray FirstOrderType FirstOrderType | FOTTuple [FirstOrderType] | FOTRec (Map FieldName FirstOrderType) - deriving (Eq, Show) + deriving (Eq, Show, Generic) -- | Values inhabiting those first-order types. +-- NB: The JSON encoding of this type, used for saw-script solver result caching, +-- assumes constructor names and argument orders will not change (though the +-- order and number of constructors may change) - see 'firstOrderJSONOptions' data FirstOrderValue = FOVBit Bool | FOVInt Integer @@ -70,7 +81,7 @@ data FirstOrderValue | FOVArray FirstOrderType FirstOrderType | FOVTuple [FirstOrderValue] | FOVRec (Map FieldName FirstOrderValue) - deriving Eq + deriving (Eq, Generic) toFirstOrderType :: FiniteType -> FirstOrderType toFirstOrderType ft = @@ -136,6 +147,30 @@ ppFirstOrderValue opts = loop FOVRec xs -> braces (sep (punctuate comma (map ppField (Map.toList xs)))) where ppField (f,x) = pretty f <+> pretty '=' <+> loop x +-- | The options for JSON-serializing 'FirstOrderType's and 'FirstOrderValue's: +-- remove the @FOT@/@FOV@ prefixes and encode the different constructors as +-- two-element arrays. Thus, this encoding assumes constructor names and +-- argument orders will not change (though the order and number of constructors +-- may change). +firstOrderJSONOptions :: JSON.Options +firstOrderJSONOptions = + JSON.defaultOptions { JSON.sumEncoding = JSON.TwoElemArray + , JSON.constructorTagModifier = dropFO } + where dropFO ('F':'O':tv:cs) | tv `elem` ['T', 'V'] = cs + dropFO cs = cs + +instance FromJSON FirstOrderType where + parseJSON = JSON.genericParseJSON firstOrderJSONOptions +instance FromJSON FirstOrderValue where + parseJSON = JSON.genericParseJSON firstOrderJSONOptions + +instance ToJSON FirstOrderType where + toJSON = JSON.genericToJSON firstOrderJSONOptions + toEncoding = JSON.genericToEncoding firstOrderJSONOptions +instance ToJSON FirstOrderValue where + toJSON = JSON.genericToJSON firstOrderJSONOptions + toEncoding = JSON.genericToEncoding firstOrderJSONOptions + -- | Smart constructor fvVec :: FiniteType -> [FiniteValue] -> FiniteValue diff --git a/saw-core/src/Verifier/SAW/SATQuery.hs b/saw-core/src/Verifier/SAW/SATQuery.hs index 1ddc69a843..650738659c 100644 --- a/saw-core/src/Verifier/SAW/SATQuery.hs +++ b/saw-core/src/Verifier/SAW/SATQuery.hs @@ -3,10 +3,12 @@ module Verifier.SAW.SATQuery , SATResult(..) , SATAssert(..) , satQueryAsTerm +, satQueryAsPropTerm ) where import Data.Map (Map) import Data.Set (Set) +import Data.Foldable (foldrM) import Verifier.SAW.Name import Verifier.SAW.FiniteValue @@ -87,3 +89,13 @@ satQueryAsTerm sc satq = do x' <- scAnd sc x y loop x' xs loop _ (UniversalAssert{} : _) = univFail + +-- | Compute the conjunction of all the assertions +-- in this SAT query as a single term of type Prop. +satQueryAsPropTerm :: SharedContext -> SATQuery -> IO Term +satQueryAsPropTerm sc satq = + scTupleType sc =<< mapM assertAsPropTerm (satAsserts satq) + where assertAsPropTerm (BoolAssert b) = scEqTrue sc b + assertAsPropTerm (UniversalAssert ecs hs g) = + scGeneralizeExts sc (map fst ecs) =<< + scEqTrue sc =<< foldrM (scImplies sc) g hs diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md index cf6d59216e..3966a2b05f 100644 --- a/saw-remote-api/python/CHANGELOG.md +++ b/saw-remote-api/python/CHANGELOG.md @@ -1,5 +1,10 @@ # Revision history for saw-client +## 1.0.1 -- YYYY-MM-DD + +* Add `solver_cache.py` implementing an interface for interacting with SAW + solver cache databases. + ## 1.0.0 -- 2023-06-26 * The v1.0.0 release is made in tandem with the SAW 1.0 release. See the diff --git a/saw-remote-api/python/poetry.lock b/saw-remote-api/python/poetry.lock index a73e6b7303..0e385103c9 100644 --- a/saw-remote-api/python/poetry.lock +++ b/saw-remote-api/python/poetry.lock @@ -25,6 +25,55 @@ files = [ {file = "BitVector-3.5.0.tar.gz", hash = "sha256:cac2fbccf11e325115827ed7be03e5fd62615227b0bbf3fa5a18a842a221839c"}, ] +[[package]] +name = "cbor2" +version = "5.4.6" +description = "CBOR (de)serializer with extensive tag support" +optional = false +python-versions = ">=3.7" +files = [ + {file = "cbor2-5.4.6-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:309fffbb7f561d67f02095d4b9657b73c9220558701c997e9bfcfbca2696e927"}, + {file = "cbor2-5.4.6-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:ff95b33e5482313a74648ca3620c9328e9f30ecfa034df040b828e476597d352"}, + {file = "cbor2-5.4.6-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:db9eb582fce972f0fa429d8159b7891ff8deccb7affc4995090afc61ce0d328a"}, + {file = "cbor2-5.4.6-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:3950be57a1698086cf26d8710b4e5a637b65133c5b1f9eec23967d4089d8cfed"}, + {file = "cbor2-5.4.6-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:78304df140b9e13b93bcbb2aecee64c9aaa9f1cadbd45f043b5e7b93cc2f21a2"}, + {file = "cbor2-5.4.6-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:e73ca40dd3c7210ff776acff9869ddc9ff67bae7c425b58e5715dcf55275163f"}, + {file = "cbor2-5.4.6-cp310-cp310-win_amd64.whl", hash = "sha256:0b956f19e93ba3180c336282cd1b6665631f2d3a196a9c19b29a833bf979e7a4"}, + {file = "cbor2-5.4.6-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:1c12c0ab78f5bc290b08a79152a8621822415836a86f8f4b50dadba371736fda"}, + {file = "cbor2-5.4.6-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:3545b16f9f0d5f34d4c99052829c3726020a07be34c99c250d0df87418f02954"}, + {file = "cbor2-5.4.6-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:24144822f8d2b0156f4cda9427f071f969c18683ffed39663dc86bc0a75ae4dd"}, + {file = "cbor2-5.4.6-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:1835536e76ea16e88c934aac5e369ba9f93d495b01e5fa2d93f0b4986b89146d"}, + {file = "cbor2-5.4.6-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:39452c799453f5bf33281ffc0752c620b8bfa0b7c13070b87d370257a1311976"}, + {file = "cbor2-5.4.6-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:3316f09a77af85e7772ecfdd693b0f450678a60b1aee641bac319289757e3fa0"}, + {file = "cbor2-5.4.6-cp311-cp311-win_amd64.whl", hash = "sha256:456cdff668a50a52fdb8aa6d0742511e43ed46d6a5b463dba80a5a720fa0d320"}, + {file = "cbor2-5.4.6-cp37-cp37m-macosx_10_9_x86_64.whl", hash = "sha256:9394ca49ecdf0957924e45d09a4026482d184a465a047f60c4044eb464c43de9"}, + {file = "cbor2-5.4.6-cp37-cp37m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:56dfa030cd3d67e5b6701d3067923f2f61536a8ffb1b45be14775d1e866b59ae"}, + {file = "cbor2-5.4.6-cp37-cp37m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:e5094562dfe3e5583202b93ef7ca5082c2ba5571accb2c4412d27b7d0ba8a563"}, + {file = "cbor2-5.4.6-cp37-cp37m-musllinux_1_1_aarch64.whl", hash = "sha256:94f844d0e232aca061a86dd6ff191e47ba0389ddd34acb784ad9a41594dc99a4"}, + {file = "cbor2-5.4.6-cp37-cp37m-musllinux_1_1_x86_64.whl", hash = "sha256:7bbd3470eb685325398023e335be896b74f61b014896604ed45049a7b7b6d8ac"}, + {file = "cbor2-5.4.6-cp37-cp37m-win_amd64.whl", hash = "sha256:0bd12c54a48949d11f5ffc2fa27f5df1b4754111f5207453e5fae3512ebb3cab"}, + {file = "cbor2-5.4.6-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:d2984a488f350aee1d54fa9cb8c6a3c1f1f5b268abbc91161e47185de4d829f3"}, + {file = "cbor2-5.4.6-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:c285a2cb2c04004bfead93df89d92a0cef1874ad337d0cb5ea53c2c31e97bfdb"}, + {file = "cbor2-5.4.6-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:6709d97695205cd08255363b54afa035306d5302b7b5e38308c8ff5a47e60f2a"}, + {file = "cbor2-5.4.6-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:96087fa5336ebfc94465c0768cd5de0fcf9af3840d2cf0ce32f5767855f1a293"}, + {file = "cbor2-5.4.6-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:0d2b926b024d3a1549b819bc82fdc387062bbd977b0299dd5fa5e0ea3267b98b"}, + {file = "cbor2-5.4.6-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:6e1b5aee920b6a2f737aa12e2b54de3826b09f885a7ce402db84216343368140"}, + {file = "cbor2-5.4.6-cp38-cp38-win_amd64.whl", hash = "sha256:79e048e623846d60d735bb350263e8fdd36cb6195d7f1a2b57eacd573d9c0b33"}, + {file = "cbor2-5.4.6-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:80ac8ba450c7a41c5afe5f7e503d3092442ed75393e1de162b0bf0d97edf7c7f"}, + {file = "cbor2-5.4.6-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:4ce1a2c272ba8523a55ea2f1d66e3464e89fa0e37c9a3d786a919fe64e68dbd7"}, + {file = "cbor2-5.4.6-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:1618d16e310f7ffed141762b0ff5d8bb6b53ad449406115cc465bf04213cefcf"}, + {file = "cbor2-5.4.6-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:4bbbdb2e3ef274865dc3f279aae109b5d94f4654aea3c72c479fb37e4a1e7ed7"}, + {file = "cbor2-5.4.6-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:6f9c702bee2954fffdfa3de95a5af1a6b1c5f155e39490353d5654d83bb05bb9"}, + {file = "cbor2-5.4.6-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:4b9f3924da0e460a93b3674c7e71020dd6c9e9f17400a34e52a88c0af2dcd2aa"}, + {file = "cbor2-5.4.6-cp39-cp39-win_amd64.whl", hash = "sha256:d54bd840b4fe34f097b8665fc0692c7dd175349e53976be6c5de4433b970daa4"}, + {file = "cbor2-5.4.6-py3-none-any.whl", hash = "sha256:181ac494091d1f9c5bb373cd85514ce1eb967a8cf3ec298e8dfa8878aa823956"}, + {file = "cbor2-5.4.6.tar.gz", hash = "sha256:b893500db0fe033e570c3adc956af6eefc57e280026bd2d86fd53da9f1e594d7"}, +] + +[package.extras] +doc = ["sphinx-autodoc-typehints (>=1.2.0)", "sphinx-rtd-theme"] +test = ["pytest", "pytest-cov"] + [[package]] name = "certifi" version = "2023.7.22" @@ -38,99 +87,86 @@ files = [ [[package]] name = "charset-normalizer" -version = "3.0.1" +version = "3.2.0" description = "The Real First Universal Charset Detector. Open, modern and actively maintained alternative to Chardet." optional = false -python-versions = "*" +python-versions = ">=3.7.0" files = [ - {file = "charset-normalizer-3.0.1.tar.gz", hash = "sha256:ebea339af930f8ca5d7a699b921106c6e29c617fe9606fa7baa043c1cdae326f"}, - {file = "charset_normalizer-3.0.1-cp310-cp310-macosx_10_9_universal2.whl", hash = "sha256:88600c72ef7587fe1708fd242b385b6ed4b8904976d5da0893e31df8b3480cb6"}, - {file = "charset_normalizer-3.0.1-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:c75ffc45f25324e68ab238cb4b5c0a38cd1c3d7f1fb1f72b5541de469e2247db"}, - {file = "charset_normalizer-3.0.1-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:db72b07027db150f468fbada4d85b3b2729a3db39178abf5c543b784c1254539"}, - {file = "charset_normalizer-3.0.1-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:62595ab75873d50d57323a91dd03e6966eb79c41fa834b7a1661ed043b2d404d"}, - {file = "charset_normalizer-3.0.1-cp310-cp310-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:ff6f3db31555657f3163b15a6b7c6938d08df7adbfc9dd13d9d19edad678f1e8"}, - {file = "charset_normalizer-3.0.1-cp310-cp310-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:772b87914ff1152b92a197ef4ea40efe27a378606c39446ded52c8f80f79702e"}, - {file = "charset_normalizer-3.0.1-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:70990b9c51340e4044cfc394a81f614f3f90d41397104d226f21e66de668730d"}, - {file = "charset_normalizer-3.0.1-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:292d5e8ba896bbfd6334b096e34bffb56161c81408d6d036a7dfa6929cff8783"}, - {file = "charset_normalizer-3.0.1-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:2edb64ee7bf1ed524a1da60cdcd2e1f6e2b4f66ef7c077680739f1641f62f555"}, - {file = "charset_normalizer-3.0.1-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:31a9ddf4718d10ae04d9b18801bd776693487cbb57d74cc3458a7673f6f34639"}, - {file = "charset_normalizer-3.0.1-cp310-cp310-musllinux_1_1_ppc64le.whl", hash = "sha256:44ba614de5361b3e5278e1241fda3dc1838deed864b50a10d7ce92983797fa76"}, - {file = "charset_normalizer-3.0.1-cp310-cp310-musllinux_1_1_s390x.whl", hash = "sha256:12db3b2c533c23ab812c2b25934f60383361f8a376ae272665f8e48b88e8e1c6"}, - {file = "charset_normalizer-3.0.1-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:c512accbd6ff0270939b9ac214b84fb5ada5f0409c44298361b2f5e13f9aed9e"}, - {file = "charset_normalizer-3.0.1-cp310-cp310-win32.whl", hash = "sha256:502218f52498a36d6bf5ea77081844017bf7982cdbe521ad85e64cabee1b608b"}, - {file = "charset_normalizer-3.0.1-cp310-cp310-win_amd64.whl", hash = "sha256:601f36512f9e28f029d9481bdaf8e89e5148ac5d89cffd3b05cd533eeb423b59"}, - {file = "charset_normalizer-3.0.1-cp311-cp311-macosx_10_9_universal2.whl", hash = "sha256:0298eafff88c99982a4cf66ba2efa1128e4ddaca0b05eec4c456bbc7db691d8d"}, - {file = "charset_normalizer-3.0.1-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:a8d0fc946c784ff7f7c3742310cc8a57c5c6dc31631269876a88b809dbeff3d3"}, - {file = "charset_normalizer-3.0.1-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:87701167f2a5c930b403e9756fab1d31d4d4da52856143b609e30a1ce7160f3c"}, - {file = "charset_normalizer-3.0.1-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:14e76c0f23218b8f46c4d87018ca2e441535aed3632ca134b10239dfb6dadd6b"}, - {file = "charset_normalizer-3.0.1-cp311-cp311-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:0c0a590235ccd933d9892c627dec5bc7511ce6ad6c1011fdf5b11363022746c1"}, - {file = "charset_normalizer-3.0.1-cp311-cp311-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:8c7fe7afa480e3e82eed58e0ca89f751cd14d767638e2550c77a92a9e749c317"}, - {file = "charset_normalizer-3.0.1-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:79909e27e8e4fcc9db4addea88aa63f6423ebb171db091fb4373e3312cb6d603"}, - {file = "charset_normalizer-3.0.1-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:8ac7b6a045b814cf0c47f3623d21ebd88b3e8cf216a14790b455ea7ff0135d18"}, - {file = "charset_normalizer-3.0.1-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:72966d1b297c741541ca8cf1223ff262a6febe52481af742036a0b296e35fa5a"}, - {file = "charset_normalizer-3.0.1-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:f9d0c5c045a3ca9bedfc35dca8526798eb91a07aa7a2c0fee134c6c6f321cbd7"}, - {file = "charset_normalizer-3.0.1-cp311-cp311-musllinux_1_1_ppc64le.whl", hash = "sha256:5995f0164fa7df59db4746112fec3f49c461dd6b31b841873443bdb077c13cfc"}, - {file = "charset_normalizer-3.0.1-cp311-cp311-musllinux_1_1_s390x.whl", hash = "sha256:4a8fcf28c05c1f6d7e177a9a46a1c52798bfe2ad80681d275b10dcf317deaf0b"}, - {file = "charset_normalizer-3.0.1-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:761e8904c07ad053d285670f36dd94e1b6ab7f16ce62b9805c475b7aa1cffde6"}, - {file = "charset_normalizer-3.0.1-cp311-cp311-win32.whl", hash = "sha256:71140351489970dfe5e60fc621ada3e0f41104a5eddaca47a7acb3c1b851d6d3"}, - {file = "charset_normalizer-3.0.1-cp311-cp311-win_amd64.whl", hash = "sha256:9ab77acb98eba3fd2a85cd160851816bfce6871d944d885febf012713f06659c"}, - {file = "charset_normalizer-3.0.1-cp36-cp36m-macosx_10_9_x86_64.whl", hash = "sha256:84c3990934bae40ea69a82034912ffe5a62c60bbf6ec5bc9691419641d7d5c9a"}, - {file = "charset_normalizer-3.0.1-cp36-cp36m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:74292fc76c905c0ef095fe11e188a32ebd03bc38f3f3e9bcb85e4e6db177b7ea"}, - {file = "charset_normalizer-3.0.1-cp36-cp36m-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:c95a03c79bbe30eec3ec2b7f076074f4281526724c8685a42872974ef4d36b72"}, - {file = "charset_normalizer-3.0.1-cp36-cp36m-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:f4c39b0e3eac288fedc2b43055cfc2ca7a60362d0e5e87a637beac5d801ef478"}, - {file = "charset_normalizer-3.0.1-cp36-cp36m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:df2c707231459e8a4028eabcd3cfc827befd635b3ef72eada84ab13b52e1574d"}, - {file = "charset_normalizer-3.0.1-cp36-cp36m-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:93ad6d87ac18e2a90b0fe89df7c65263b9a99a0eb98f0a3d2e079f12a0735837"}, - {file = "charset_normalizer-3.0.1-cp36-cp36m-musllinux_1_1_aarch64.whl", hash = "sha256:59e5686dd847347e55dffcc191a96622f016bc0ad89105e24c14e0d6305acbc6"}, - {file = "charset_normalizer-3.0.1-cp36-cp36m-musllinux_1_1_i686.whl", hash = "sha256:cd6056167405314a4dc3c173943f11249fa0f1b204f8b51ed4bde1a9cd1834dc"}, - {file = "charset_normalizer-3.0.1-cp36-cp36m-musllinux_1_1_ppc64le.whl", hash = "sha256:083c8d17153ecb403e5e1eb76a7ef4babfc2c48d58899c98fcaa04833e7a2f9a"}, - {file = "charset_normalizer-3.0.1-cp36-cp36m-musllinux_1_1_s390x.whl", hash = "sha256:f5057856d21e7586765171eac8b9fc3f7d44ef39425f85dbcccb13b3ebea806c"}, - {file = "charset_normalizer-3.0.1-cp36-cp36m-musllinux_1_1_x86_64.whl", hash = "sha256:7eb33a30d75562222b64f569c642ff3dc6689e09adda43a082208397f016c39a"}, - {file = "charset_normalizer-3.0.1-cp36-cp36m-win32.whl", hash = "sha256:95dea361dd73757c6f1c0a1480ac499952c16ac83f7f5f4f84f0658a01b8ef41"}, - {file = "charset_normalizer-3.0.1-cp36-cp36m-win_amd64.whl", hash = "sha256:eaa379fcd227ca235d04152ca6704c7cb55564116f8bc52545ff357628e10602"}, - {file = "charset_normalizer-3.0.1-cp37-cp37m-macosx_10_9_x86_64.whl", hash = "sha256:3e45867f1f2ab0711d60c6c71746ac53537f1684baa699f4f668d4c6f6ce8e14"}, - {file = "charset_normalizer-3.0.1-cp37-cp37m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:cadaeaba78750d58d3cc6ac4d1fd867da6fc73c88156b7a3212a3cd4819d679d"}, - {file = "charset_normalizer-3.0.1-cp37-cp37m-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:911d8a40b2bef5b8bbae2e36a0b103f142ac53557ab421dc16ac4aafee6f53dc"}, - {file = "charset_normalizer-3.0.1-cp37-cp37m-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:503e65837c71b875ecdd733877d852adbc465bd82c768a067badd953bf1bc5a3"}, - {file = "charset_normalizer-3.0.1-cp37-cp37m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:a60332922359f920193b1d4826953c507a877b523b2395ad7bc716ddd386d866"}, - {file = "charset_normalizer-3.0.1-cp37-cp37m-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:16a8663d6e281208d78806dbe14ee9903715361cf81f6d4309944e4d1e59ac5b"}, - {file = "charset_normalizer-3.0.1-cp37-cp37m-musllinux_1_1_aarch64.whl", hash = "sha256:a16418ecf1329f71df119e8a65f3aa68004a3f9383821edcb20f0702934d8087"}, - {file = "charset_normalizer-3.0.1-cp37-cp37m-musllinux_1_1_i686.whl", hash = "sha256:9d9153257a3f70d5f69edf2325357251ed20f772b12e593f3b3377b5f78e7ef8"}, - {file = "charset_normalizer-3.0.1-cp37-cp37m-musllinux_1_1_ppc64le.whl", hash = "sha256:02a51034802cbf38db3f89c66fb5d2ec57e6fe7ef2f4a44d070a593c3688667b"}, - {file = "charset_normalizer-3.0.1-cp37-cp37m-musllinux_1_1_s390x.whl", hash = "sha256:2e396d70bc4ef5325b72b593a72c8979999aa52fb8bcf03f701c1b03e1166918"}, - {file = "charset_normalizer-3.0.1-cp37-cp37m-musllinux_1_1_x86_64.whl", hash = "sha256:11b53acf2411c3b09e6af37e4b9005cba376c872503c8f28218c7243582df45d"}, - {file = "charset_normalizer-3.0.1-cp37-cp37m-win32.whl", hash = "sha256:0bf2dae5291758b6f84cf923bfaa285632816007db0330002fa1de38bfcb7154"}, - {file = "charset_normalizer-3.0.1-cp37-cp37m-win_amd64.whl", hash = "sha256:2c03cc56021a4bd59be889c2b9257dae13bf55041a3372d3295416f86b295fb5"}, - {file = "charset_normalizer-3.0.1-cp38-cp38-macosx_10_9_universal2.whl", hash = "sha256:024e606be3ed92216e2b6952ed859d86b4cfa52cd5bc5f050e7dc28f9b43ec42"}, - {file = "charset_normalizer-3.0.1-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:4b0d02d7102dd0f997580b51edc4cebcf2ab6397a7edf89f1c73b586c614272c"}, - {file = "charset_normalizer-3.0.1-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:358a7c4cb8ba9b46c453b1dd8d9e431452d5249072e4f56cfda3149f6ab1405e"}, - {file = "charset_normalizer-3.0.1-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:81d6741ab457d14fdedc215516665050f3822d3e56508921cc7239f8c8e66a58"}, - {file = "charset_normalizer-3.0.1-cp38-cp38-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:8b8af03d2e37866d023ad0ddea594edefc31e827fee64f8de5611a1dbc373174"}, - {file = "charset_normalizer-3.0.1-cp38-cp38-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:9cf4e8ad252f7c38dd1f676b46514f92dc0ebeb0db5552f5f403509705e24753"}, - {file = "charset_normalizer-3.0.1-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:e696f0dd336161fca9adbb846875d40752e6eba585843c768935ba5c9960722b"}, - {file = "charset_normalizer-3.0.1-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:c22d3fe05ce11d3671297dc8973267daa0f938b93ec716e12e0f6dee81591dc1"}, - {file = "charset_normalizer-3.0.1-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:109487860ef6a328f3eec66f2bf78b0b72400280d8f8ea05f69c51644ba6521a"}, - {file = "charset_normalizer-3.0.1-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:37f8febc8ec50c14f3ec9637505f28e58d4f66752207ea177c1d67df25da5aed"}, - {file = "charset_normalizer-3.0.1-cp38-cp38-musllinux_1_1_ppc64le.whl", hash = "sha256:f97e83fa6c25693c7a35de154681fcc257c1c41b38beb0304b9c4d2d9e164479"}, - {file = "charset_normalizer-3.0.1-cp38-cp38-musllinux_1_1_s390x.whl", hash = "sha256:a152f5f33d64a6be73f1d30c9cc82dfc73cec6477ec268e7c6e4c7d23c2d2291"}, - {file = "charset_normalizer-3.0.1-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:39049da0ffb96c8cbb65cbf5c5f3ca3168990adf3551bd1dee10c48fce8ae820"}, - {file = "charset_normalizer-3.0.1-cp38-cp38-win32.whl", hash = "sha256:4457ea6774b5611f4bed5eaa5df55f70abde42364d498c5134b7ef4c6958e20e"}, - {file = "charset_normalizer-3.0.1-cp38-cp38-win_amd64.whl", hash = "sha256:e62164b50f84e20601c1ff8eb55620d2ad25fb81b59e3cd776a1902527a788af"}, - {file = "charset_normalizer-3.0.1-cp39-cp39-macosx_10_9_universal2.whl", hash = "sha256:8eade758719add78ec36dc13201483f8e9b5d940329285edcd5f70c0a9edbd7f"}, - {file = "charset_normalizer-3.0.1-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:8499ca8f4502af841f68135133d8258f7b32a53a1d594aa98cc52013fff55678"}, - {file = "charset_normalizer-3.0.1-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:3fc1c4a2ffd64890aebdb3f97e1278b0cc72579a08ca4de8cd2c04799a3a22be"}, - {file = "charset_normalizer-3.0.1-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:00d3ffdaafe92a5dc603cb9bd5111aaa36dfa187c8285c543be562e61b755f6b"}, - {file = "charset_normalizer-3.0.1-cp39-cp39-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:c2ac1b08635a8cd4e0cbeaf6f5e922085908d48eb05d44c5ae9eabab148512ca"}, - {file = "charset_normalizer-3.0.1-cp39-cp39-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:f6f45710b4459401609ebebdbcfb34515da4fc2aa886f95107f556ac69a9147e"}, - {file = "charset_normalizer-3.0.1-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:3ae1de54a77dc0d6d5fcf623290af4266412a7c4be0b1ff7444394f03f5c54e3"}, - {file = "charset_normalizer-3.0.1-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:3b590df687e3c5ee0deef9fc8c547d81986d9a1b56073d82de008744452d6541"}, - {file = "charset_normalizer-3.0.1-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:ab5de034a886f616a5668aa5d098af2b5385ed70142090e2a31bcbd0af0fdb3d"}, - {file = "charset_normalizer-3.0.1-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:9cb3032517f1627cc012dbc80a8ec976ae76d93ea2b5feaa9d2a5b8882597579"}, - {file = "charset_normalizer-3.0.1-cp39-cp39-musllinux_1_1_ppc64le.whl", hash = "sha256:608862a7bf6957f2333fc54ab4399e405baad0163dc9f8d99cb236816db169d4"}, - {file = "charset_normalizer-3.0.1-cp39-cp39-musllinux_1_1_s390x.whl", hash = "sha256:0f438ae3532723fb6ead77e7c604be7c8374094ef4ee2c5e03a3a17f1fca256c"}, - {file = "charset_normalizer-3.0.1-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:356541bf4381fa35856dafa6a965916e54bed415ad8a24ee6de6e37deccf2786"}, - {file = "charset_normalizer-3.0.1-cp39-cp39-win32.whl", hash = "sha256:39cf9ed17fe3b1bc81f33c9ceb6ce67683ee7526e65fde1447c772afc54a1bb8"}, - {file = "charset_normalizer-3.0.1-cp39-cp39-win_amd64.whl", hash = "sha256:0a11e971ed097d24c534c037d298ad32c6ce81a45736d31e0ff0ad37ab437d59"}, - {file = "charset_normalizer-3.0.1-py3-none-any.whl", hash = "sha256:7e189e2e1d3ed2f4aebabd2d5b0f931e883676e51c7624826e0a4e5fe8a0bf24"}, + {file = "charset-normalizer-3.2.0.tar.gz", hash = "sha256:3bb3d25a8e6c0aedd251753a79ae98a093c7e7b471faa3aa9a93a81431987ace"}, + {file = "charset_normalizer-3.2.0-cp310-cp310-macosx_10_9_universal2.whl", hash = "sha256:0b87549028f680ca955556e3bd57013ab47474c3124dc069faa0b6545b6c9710"}, + {file = "charset_normalizer-3.2.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:7c70087bfee18a42b4040bb9ec1ca15a08242cf5867c58726530bdf3945672ed"}, + {file = "charset_normalizer-3.2.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:a103b3a7069b62f5d4890ae1b8f0597618f628b286b03d4bc9195230b154bfa9"}, + {file = "charset_normalizer-3.2.0-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:94aea8eff76ee6d1cdacb07dd2123a68283cb5569e0250feab1240058f53b623"}, + {file = "charset_normalizer-3.2.0-cp310-cp310-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:db901e2ac34c931d73054d9797383d0f8009991e723dab15109740a63e7f902a"}, + {file = "charset_normalizer-3.2.0-cp310-cp310-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:b0dac0ff919ba34d4df1b6131f59ce95b08b9065233446be7e459f95554c0dc8"}, + {file = "charset_normalizer-3.2.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:193cbc708ea3aca45e7221ae58f0fd63f933753a9bfb498a3b474878f12caaad"}, + {file = "charset_normalizer-3.2.0-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:09393e1b2a9461950b1c9a45d5fd251dc7c6f228acab64da1c9c0165d9c7765c"}, + {file = "charset_normalizer-3.2.0-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:baacc6aee0b2ef6f3d308e197b5d7a81c0e70b06beae1f1fcacffdbd124fe0e3"}, + {file = "charset_normalizer-3.2.0-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:bf420121d4c8dce6b889f0e8e4ec0ca34b7f40186203f06a946fa0276ba54029"}, + {file = "charset_normalizer-3.2.0-cp310-cp310-musllinux_1_1_ppc64le.whl", hash = "sha256:c04a46716adde8d927adb9457bbe39cf473e1e2c2f5d0a16ceb837e5d841ad4f"}, + {file = "charset_normalizer-3.2.0-cp310-cp310-musllinux_1_1_s390x.whl", hash = "sha256:aaf63899c94de41fe3cf934601b0f7ccb6b428c6e4eeb80da72c58eab077b19a"}, + {file = "charset_normalizer-3.2.0-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:d62e51710986674142526ab9f78663ca2b0726066ae26b78b22e0f5e571238dd"}, + {file = "charset_normalizer-3.2.0-cp310-cp310-win32.whl", hash = "sha256:04e57ab9fbf9607b77f7d057974694b4f6b142da9ed4a199859d9d4d5c63fe96"}, + {file = "charset_normalizer-3.2.0-cp310-cp310-win_amd64.whl", hash = "sha256:48021783bdf96e3d6de03a6e39a1171ed5bd7e8bb93fc84cc649d11490f87cea"}, + {file = "charset_normalizer-3.2.0-cp311-cp311-macosx_10_9_universal2.whl", hash = "sha256:4957669ef390f0e6719db3613ab3a7631e68424604a7b448f079bee145da6e09"}, + {file = "charset_normalizer-3.2.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:46fb8c61d794b78ec7134a715a3e564aafc8f6b5e338417cb19fe9f57a5a9bf2"}, + {file = "charset_normalizer-3.2.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:f779d3ad205f108d14e99bb3859aa7dd8e9c68874617c72354d7ecaec2a054ac"}, + {file = "charset_normalizer-3.2.0-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:f25c229a6ba38a35ae6e25ca1264621cc25d4d38dca2942a7fce0b67a4efe918"}, + {file = "charset_normalizer-3.2.0-cp311-cp311-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:2efb1bd13885392adfda4614c33d3b68dee4921fd0ac1d3988f8cbb7d589e72a"}, + {file = "charset_normalizer-3.2.0-cp311-cp311-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:1f30b48dd7fa1474554b0b0f3fdfdd4c13b5c737a3c6284d3cdc424ec0ffff3a"}, + {file = "charset_normalizer-3.2.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:246de67b99b6851627d945db38147d1b209a899311b1305dd84916f2b88526c6"}, + {file = "charset_normalizer-3.2.0-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:9bd9b3b31adcb054116447ea22caa61a285d92e94d710aa5ec97992ff5eb7cf3"}, + {file = "charset_normalizer-3.2.0-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:8c2f5e83493748286002f9369f3e6607c565a6a90425a3a1fef5ae32a36d749d"}, + {file = "charset_normalizer-3.2.0-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:3170c9399da12c9dc66366e9d14da8bf7147e1e9d9ea566067bbce7bb74bd9c2"}, + {file = "charset_normalizer-3.2.0-cp311-cp311-musllinux_1_1_ppc64le.whl", hash = "sha256:7a4826ad2bd6b07ca615c74ab91f32f6c96d08f6fcc3902ceeedaec8cdc3bcd6"}, + {file = "charset_normalizer-3.2.0-cp311-cp311-musllinux_1_1_s390x.whl", hash = "sha256:3b1613dd5aee995ec6d4c69f00378bbd07614702a315a2cf6c1d21461fe17c23"}, + {file = "charset_normalizer-3.2.0-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:9e608aafdb55eb9f255034709e20d5a83b6d60c054df0802fa9c9883d0a937aa"}, + {file = "charset_normalizer-3.2.0-cp311-cp311-win32.whl", hash = "sha256:f2a1d0fd4242bd8643ce6f98927cf9c04540af6efa92323e9d3124f57727bfc1"}, + {file = "charset_normalizer-3.2.0-cp311-cp311-win_amd64.whl", hash = "sha256:681eb3d7e02e3c3655d1b16059fbfb605ac464c834a0c629048a30fad2b27489"}, + {file = "charset_normalizer-3.2.0-cp37-cp37m-macosx_10_9_x86_64.whl", hash = "sha256:c57921cda3a80d0f2b8aec7e25c8aa14479ea92b5b51b6876d975d925a2ea346"}, + {file = "charset_normalizer-3.2.0-cp37-cp37m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:41b25eaa7d15909cf3ac4c96088c1f266a9a93ec44f87f1d13d4a0e86c81b982"}, + {file = "charset_normalizer-3.2.0-cp37-cp37m-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:f058f6963fd82eb143c692cecdc89e075fa0828db2e5b291070485390b2f1c9c"}, + {file = "charset_normalizer-3.2.0-cp37-cp37m-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:a7647ebdfb9682b7bb97e2a5e7cb6ae735b1c25008a70b906aecca294ee96cf4"}, + {file = "charset_normalizer-3.2.0-cp37-cp37m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:eef9df1eefada2c09a5e7a40991b9fc6ac6ef20b1372abd48d2794a316dc0449"}, + {file = "charset_normalizer-3.2.0-cp37-cp37m-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:e03b8895a6990c9ab2cdcd0f2fe44088ca1c65ae592b8f795c3294af00a461c3"}, + {file = "charset_normalizer-3.2.0-cp37-cp37m-musllinux_1_1_aarch64.whl", hash = "sha256:ee4006268ed33370957f55bf2e6f4d263eaf4dc3cfc473d1d90baff6ed36ce4a"}, + {file = "charset_normalizer-3.2.0-cp37-cp37m-musllinux_1_1_i686.whl", hash = "sha256:c4983bf937209c57240cff65906b18bb35e64ae872da6a0db937d7b4af845dd7"}, + {file = "charset_normalizer-3.2.0-cp37-cp37m-musllinux_1_1_ppc64le.whl", hash = "sha256:3bb7fda7260735efe66d5107fb7e6af6a7c04c7fce9b2514e04b7a74b06bf5dd"}, + {file = "charset_normalizer-3.2.0-cp37-cp37m-musllinux_1_1_s390x.whl", hash = "sha256:72814c01533f51d68702802d74f77ea026b5ec52793c791e2da806a3844a46c3"}, + {file = "charset_normalizer-3.2.0-cp37-cp37m-musllinux_1_1_x86_64.whl", hash = "sha256:70c610f6cbe4b9fce272c407dd9d07e33e6bf7b4aa1b7ffb6f6ded8e634e3592"}, + {file = "charset_normalizer-3.2.0-cp37-cp37m-win32.whl", hash = "sha256:a401b4598e5d3f4a9a811f3daf42ee2291790c7f9d74b18d75d6e21dda98a1a1"}, + {file = "charset_normalizer-3.2.0-cp37-cp37m-win_amd64.whl", hash = "sha256:c0b21078a4b56965e2b12f247467b234734491897e99c1d51cee628da9786959"}, + {file = "charset_normalizer-3.2.0-cp38-cp38-macosx_10_9_universal2.whl", hash = "sha256:95eb302ff792e12aba9a8b8f8474ab229a83c103d74a750ec0bd1c1eea32e669"}, + {file = "charset_normalizer-3.2.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:1a100c6d595a7f316f1b6f01d20815d916e75ff98c27a01ae817439ea7726329"}, + {file = "charset_normalizer-3.2.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:6339d047dab2780cc6220f46306628e04d9750f02f983ddb37439ca47ced7149"}, + {file = "charset_normalizer-3.2.0-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:e4b749b9cc6ee664a3300bb3a273c1ca8068c46be705b6c31cf5d276f8628a94"}, + {file = "charset_normalizer-3.2.0-cp38-cp38-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:a38856a971c602f98472050165cea2cdc97709240373041b69030be15047691f"}, + {file = "charset_normalizer-3.2.0-cp38-cp38-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:f87f746ee241d30d6ed93969de31e5ffd09a2961a051e60ae6bddde9ec3583aa"}, + {file = "charset_normalizer-3.2.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:89f1b185a01fe560bc8ae5f619e924407efca2191b56ce749ec84982fc59a32a"}, + {file = "charset_normalizer-3.2.0-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:e1c8a2f4c69e08e89632defbfabec2feb8a8d99edc9f89ce33c4b9e36ab63037"}, + {file = "charset_normalizer-3.2.0-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:2f4ac36d8e2b4cc1aa71df3dd84ff8efbe3bfb97ac41242fbcfc053c67434f46"}, + {file = "charset_normalizer-3.2.0-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:a386ebe437176aab38c041de1260cd3ea459c6ce5263594399880bbc398225b2"}, + {file = "charset_normalizer-3.2.0-cp38-cp38-musllinux_1_1_ppc64le.whl", hash = "sha256:ccd16eb18a849fd8dcb23e23380e2f0a354e8daa0c984b8a732d9cfaba3a776d"}, + {file = "charset_normalizer-3.2.0-cp38-cp38-musllinux_1_1_s390x.whl", hash = "sha256:e6a5bf2cba5ae1bb80b154ed68a3cfa2fa00fde979a7f50d6598d3e17d9ac20c"}, + {file = "charset_normalizer-3.2.0-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:45de3f87179c1823e6d9e32156fb14c1927fcc9aba21433f088fdfb555b77c10"}, + {file = "charset_normalizer-3.2.0-cp38-cp38-win32.whl", hash = "sha256:1000fba1057b92a65daec275aec30586c3de2401ccdcd41f8a5c1e2c87078706"}, + {file = "charset_normalizer-3.2.0-cp38-cp38-win_amd64.whl", hash = "sha256:8b2c760cfc7042b27ebdb4a43a4453bd829a5742503599144d54a032c5dc7e9e"}, + {file = "charset_normalizer-3.2.0-cp39-cp39-macosx_10_9_universal2.whl", hash = "sha256:855eafa5d5a2034b4621c74925d89c5efef61418570e5ef9b37717d9c796419c"}, + {file = "charset_normalizer-3.2.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:203f0c8871d5a7987be20c72442488a0b8cfd0f43b7973771640fc593f56321f"}, + {file = "charset_normalizer-3.2.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:e857a2232ba53ae940d3456f7533ce6ca98b81917d47adc3c7fd55dad8fab858"}, + {file = "charset_normalizer-3.2.0-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:5e86d77b090dbddbe78867a0275cb4df08ea195e660f1f7f13435a4649e954e5"}, + {file = "charset_normalizer-3.2.0-cp39-cp39-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:c4fb39a81950ec280984b3a44f5bd12819953dc5fa3a7e6fa7a80db5ee853952"}, + {file = "charset_normalizer-3.2.0-cp39-cp39-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:2dee8e57f052ef5353cf608e0b4c871aee320dd1b87d351c28764fc0ca55f9f4"}, + {file = "charset_normalizer-3.2.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:8700f06d0ce6f128de3ccdbc1acaea1ee264d2caa9ca05daaf492fde7c2a7200"}, + {file = "charset_normalizer-3.2.0-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:1920d4ff15ce893210c1f0c0e9d19bfbecb7983c76b33f046c13a8ffbd570252"}, + {file = "charset_normalizer-3.2.0-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:c1c76a1743432b4b60ab3358c937a3fe1341c828ae6194108a94c69028247f22"}, + {file = "charset_normalizer-3.2.0-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:f7560358a6811e52e9c4d142d497f1a6e10103d3a6881f18d04dbce3729c0e2c"}, + {file = "charset_normalizer-3.2.0-cp39-cp39-musllinux_1_1_ppc64le.whl", hash = "sha256:c8063cf17b19661471ecbdb3df1c84f24ad2e389e326ccaf89e3fb2484d8dd7e"}, + {file = "charset_normalizer-3.2.0-cp39-cp39-musllinux_1_1_s390x.whl", hash = "sha256:cd6dbe0238f7743d0efe563ab46294f54f9bc8f4b9bcf57c3c666cc5bc9d1299"}, + {file = "charset_normalizer-3.2.0-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:1249cbbf3d3b04902ff081ffbb33ce3377fa6e4c7356f759f3cd076cc138d020"}, + {file = "charset_normalizer-3.2.0-cp39-cp39-win32.whl", hash = "sha256:6c409c0deba34f147f77efaa67b8e4bb83d2f11c8806405f76397ae5b8c0d1c9"}, + {file = "charset_normalizer-3.2.0-cp39-cp39-win_amd64.whl", hash = "sha256:7095f6fbfaa55defb6b733cfeb14efaae7a29f0b59d8cf213be4e7ca0b857b80"}, + {file = "charset_normalizer-3.2.0-py3-none-any.whl", hash = "sha256:8e098148dd37b4ce3baca71fb394c81dc5d9c7728c95df695d2dca218edf40e6"}, ] [[package]] @@ -161,6 +197,45 @@ files = [ {file = "idna-3.4.tar.gz", hash = "sha256:814f528e8dead7d329833b91c5faa87d60bf71824cd12a7530b5526063d02cb4"}, ] +[[package]] +name = "lmdb" +version = "1.4.1" +description = "Universal Python binding for the LMDB 'Lightning' Database" +optional = false +python-versions = "*" +files = [ + {file = "lmdb-1.4.1-cp27-cp27m-macosx_10_14_x86_64.whl", hash = "sha256:dcdbe27f75da9b8f58815c6ac9a1f8fa2d7a8d42abc22abb664e089002d5ffa4"}, + {file = "lmdb-1.4.1-cp310-cp310-macosx_11_0_x86_64.whl", hash = "sha256:032ce6f490caedbec642fc0a79114475e8520d1bf1e1465c6a12b8e5fe39022f"}, + {file = "lmdb-1.4.1-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:13c5c8504d419039d6617cee24941e420d648a5b15c4b21e6491821400e5750f"}, + {file = "lmdb-1.4.1-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:6f8018a947608c4be0dc885c90f477a600be1b71285059a9c68280d36b3fb29b"}, + {file = "lmdb-1.4.1-cp310-cp310-win_amd64.whl", hash = "sha256:360ac42a8772f571fdd01156e0466d6be52eea1140556a138281b7c887916ae2"}, + {file = "lmdb-1.4.1-cp311-cp311-macosx_10_9_universal2.whl", hash = "sha256:f683f3d9a1771f21a7788a9be98fae9f3ce13cb8d549d6074d0402f284572458"}, + {file = "lmdb-1.4.1-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:73332a830c72d76d57744cd2b29eca2c258bc406273ca4ee07dc9e48ae84d712"}, + {file = "lmdb-1.4.1-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:0c178c5134e942256a830b0bca7bb052d3d7c645b4b8759d720ab49ec36b3aae"}, + {file = "lmdb-1.4.1-cp311-cp311-win_amd64.whl", hash = "sha256:12047c239ab6ccbbc9db99277aabcfe1c15b1cfc9ea33b92ab30ddd6f0823a10"}, + {file = "lmdb-1.4.1-cp35-cp35m-macosx_10_14_x86_64.whl", hash = "sha256:91930a2a7eb9acc4d687f9067d6f9ec83c9673bbee55823badbbee2f9a3e9970"}, + {file = "lmdb-1.4.1-cp36-cp36m-macosx_10_14_x86_64.whl", hash = "sha256:1b106eb7a23b6a224bc7dfe2bd5a34c84973dda039965ae99106e10d22833dd9"}, + {file = "lmdb-1.4.1-cp36-cp36m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:9d7779ccfacd5f4c62f28485dd2427b54d19dd7016000e6237816a3750287a82"}, + {file = "lmdb-1.4.1-cp36-cp36m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:0c1f1eff7ae8d8d534309f05e274fd646dd1d4abf5157c59db59a54a55463371"}, + {file = "lmdb-1.4.1-cp36-cp36m-win_amd64.whl", hash = "sha256:b6354df94d241e8c0158f716902224109a5f3f7ed9a24447a25f968427f61d77"}, + {file = "lmdb-1.4.1-cp37-cp37m-macosx_10_15_x86_64.whl", hash = "sha256:64cf7470edfc45ff0369956e40a0784b5225097569299b91f893bd50fa336f52"}, + {file = "lmdb-1.4.1-cp37-cp37m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:a3c15d344731507fcfddb911a86d325e867c5574751af28591e82ecf21aad1e5"}, + {file = "lmdb-1.4.1-cp37-cp37m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:342550b86bb6275bfb89dbde9e48385da51d57124433bd464cd7681d0702f566"}, + {file = "lmdb-1.4.1-cp37-cp37m-win_amd64.whl", hash = "sha256:3a99a3859427fbc273ae1e932b3e7da946089757e74a05a24a19f5c4a1aba933"}, + {file = "lmdb-1.4.1-cp38-cp38-macosx_10_15_x86_64.whl", hash = "sha256:f71da9bd33fd17c9cdbe2bd4ce87f4b36b8f044927df4220bec4b03f209c78a2"}, + {file = "lmdb-1.4.1-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:4e9ff50ad20d890bc63524230237a61b6eb3be96ad6a6ac475e8ba1a1f2c751f"}, + {file = "lmdb-1.4.1-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:81abf9475a62b7ced1ac0352967106b7ed1ac5d1c1a0d23ed24abe55a28f9884"}, + {file = "lmdb-1.4.1-cp38-cp38-win_amd64.whl", hash = "sha256:c9fa31743b447a3fbbbdaefc858de1c761568d855155dec54d5ad490f88856b6"}, + {file = "lmdb-1.4.1-cp39-cp39-macosx_11_0_x86_64.whl", hash = "sha256:26ef8fa7bd34a64f78f5e16fa9bcce0fe2ad682dd26ef078f95a8847dacb1171"}, + {file = "lmdb-1.4.1-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:9f5dc8a335f7925fd667d62a5e43bed3aa35959b32b233fe0112a6ef02e07877"}, + {file = "lmdb-1.4.1-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:7ba5d78b0ff130b38a56b7161ceb7e27ba4364d827d2bbb251c24b06c28c64cd"}, + {file = "lmdb-1.4.1-cp39-cp39-win_amd64.whl", hash = "sha256:3b84f6a349ed1bd3fa4e6c3c6b711d0389cc8d9206733cb92feffaf102998e0c"}, + {file = "lmdb-1.4.1-pp27-pypy_73-macosx_10_7_x86_64.whl", hash = "sha256:a428e6b0e298290b91b7d0ce409f595c2c9027d7f2076c39ba006290b90d14cc"}, + {file = "lmdb-1.4.1-pp27-pypy_73-win_amd64.whl", hash = "sha256:885d3f3bf51b9167d368e37b1f1277eabf595dceefd69a489bd81c1ffd3d8ffd"}, + {file = "lmdb-1.4.1-pp39-pypy39_pp73-win_amd64.whl", hash = "sha256:4bd8e49d5209c652b2caa18a3a4c30524025d7868d34b7bb249c42f7997da240"}, + {file = "lmdb-1.4.1.tar.gz", hash = "sha256:1f4c76af24e907593487c904ef5eba1993beb38ed385af82adb25a858f2d658d"}, +] + [[package]] name = "mypy" version = "0.991" @@ -213,15 +288,29 @@ reports = ["lxml"] [[package]] name = "mypy-extensions" -version = "0.4.3" -description = "Experimental type system extensions for programs checked with the mypy typechecker." +version = "1.0.0" +description = "Type system extensions for programs checked with the mypy type checker." optional = false -python-versions = "*" +python-versions = ">=3.5" files = [ - {file = "mypy_extensions-0.4.3-py2.py3-none-any.whl", hash = "sha256:090fedd75945a69ae91ce1303b5824f428daf5a028d2f6ab8a299250a846f15d"}, - {file = "mypy_extensions-0.4.3.tar.gz", hash = "sha256:2d82818f5bb3e369420cb3c4060a7970edba416647068eb4c5343488a6c604a8"}, + {file = "mypy_extensions-1.0.0-py3-none-any.whl", hash = "sha256:4392f6c0eb8a5668a69e23d168ffa70f0be9ccfd32b5cc2d26a34ae5b844552d"}, + {file = "mypy_extensions-1.0.0.tar.gz", hash = "sha256:75dbf8955dc00442a438fc4d0666508a9a97b6bd41aa2f0ffe9d2f2725af0782"}, ] +[[package]] +name = "python-dateutil" +version = "2.8.2" +description = "Extensions to the standard Python datetime module" +optional = false +python-versions = "!=3.0.*,!=3.1.*,!=3.2.*,>=2.7" +files = [ + {file = "python-dateutil-2.8.2.tar.gz", hash = "sha256:0123cacc1627ae19ddf3c27a5de5bd67ee4586fbdd6440d9748f8abb483d3e86"}, + {file = "python_dateutil-2.8.2-py2.py3-none-any.whl", hash = "sha256:961d03dc3453ebbc59dbdea9e4e11c5651520a876d0f4db161e8674aae935da9"}, +] + +[package.dependencies] +six = ">=1.5" + [[package]] name = "requests" version = "2.31.0" @@ -243,6 +332,17 @@ urllib3 = ">=1.21.1,<3" socks = ["PySocks (>=1.5.6,!=1.5.7)"] use-chardet-on-py3 = ["chardet (>=3.0.2,<6)"] +[[package]] +name = "six" +version = "1.16.0" +description = "Python 2 and 3 compatibility utilities" +optional = false +python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*" +files = [ + {file = "six-1.16.0-py2.py3-none-any.whl", hash = "sha256:8abb2f1d86890a2dfb989f9a77cfcfd3e47c2a354b01111771326f8aa26e0254"}, + {file = "six-1.16.0.tar.gz", hash = "sha256:1e61c37477a1626458e36f7b1d82aa5c9b094fa4802892072e49de9c60c4c926"}, +] + [[package]] name = "tomli" version = "2.0.1" @@ -256,32 +356,33 @@ files = [ [[package]] name = "typing-extensions" -version = "4.4.0" +version = "4.7.1" description = "Backported and Experimental Type Hints for Python 3.7+" optional = false python-versions = ">=3.7" files = [ - {file = "typing_extensions-4.4.0-py3-none-any.whl", hash = "sha256:16fa4864408f655d35ec496218b85f79b3437c829e93320c7c9215ccfd92489e"}, - {file = "typing_extensions-4.4.0.tar.gz", hash = "sha256:1511434bb92bf8dd198c12b1cc812e800d4181cfcb867674e0f8279cc93087aa"}, + {file = "typing_extensions-4.7.1-py3-none-any.whl", hash = "sha256:440d5dd3af93b060174bf433bccd69b0babc3b15b1a8dca43789fd7f61514b36"}, + {file = "typing_extensions-4.7.1.tar.gz", hash = "sha256:b75ddc264f0ba5615db7ba217daeb99701ad295353c45f9e95963337ceeeffb2"}, ] [[package]] name = "urllib3" -version = "1.26.14" +version = "2.0.4" description = "HTTP library with thread-safe connection pooling, file post, and more." optional = false -python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*, !=3.5.*" +python-versions = ">=3.7" files = [ - {file = "urllib3-1.26.14-py2.py3-none-any.whl", hash = "sha256:75edcdc2f7d85b137124a6c3c9fc3933cdeaa12ecb9a6a959f22797a0feca7e1"}, - {file = "urllib3-1.26.14.tar.gz", hash = "sha256:076907bf8fd355cde77728471316625a4d2f7e713c125f51953bb5b3eecf4f72"}, + {file = "urllib3-2.0.4-py3-none-any.whl", hash = "sha256:de7df1803967d2c2a98e4b11bb7d6bd9210474c46e8a0401514e3a42a75ebde4"}, + {file = "urllib3-2.0.4.tar.gz", hash = "sha256:8d22f86aae8ef5e410d4f539fde9ce6b2113a001bb4d189e0aed70642d602b11"}, ] [package.extras] -brotli = ["brotli (>=1.0.9)", "brotlicffi (>=0.8.0)", "brotlipy (>=0.6.0)"] -secure = ["certifi", "cryptography (>=1.3.4)", "idna (>=2.0.0)", "ipaddress", "pyOpenSSL (>=0.14)", "urllib3-secure-extra"] -socks = ["PySocks (>=1.5.6,!=1.5.7,<2.0)"] +brotli = ["brotli (>=1.0.9)", "brotlicffi (>=0.8.0)"] +secure = ["certifi", "cryptography (>=1.9)", "idna (>=2.0.0)", "pyopenssl (>=17.1.0)", "urllib3-secure-extra"] +socks = ["pysocks (>=1.5.6,!=1.5.7,<2.0)"] +zstd = ["zstandard (>=0.18.0)"] [metadata] lock-version = "2.0" python-versions = "^3.8" -content-hash = "e71c605ccdce9858ca305335b89ecee016b5e93f9cad94d1ffd81c4335a58b61" +content-hash = "10ff740f6f3d75ad166908c0eb46e73ed65a13af67879ff507c95089ed103e0c" diff --git a/saw-remote-api/python/pyproject.toml b/saw-remote-api/python/pyproject.toml index 2a425480c8..7677b432bd 100644 --- a/saw-remote-api/python/pyproject.toml +++ b/saw-remote-api/python/pyproject.toml @@ -16,6 +16,9 @@ requests = "^2.25.1" BitVector = "^3.4.9" cryptol = "3.0.0" # { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true } argo-client = "0.0.11" +lmdb = "^1.4.1" +cbor2 = "^5.4.6" +python-dateutil = "^2.8.2" [tool.poetry.dev-dependencies] mypy = "^0.991" diff --git a/saw-remote-api/python/saw_client/solver_cache.py b/saw-remote-api/python/saw_client/solver_cache.py new file mode 100644 index 0000000000..12f66e61fe --- /dev/null +++ b/saw-remote-api/python/saw_client/solver_cache.py @@ -0,0 +1,123 @@ +import cbor2 # type: ignore +from collections.abc import MutableMapping +from dataclasses import dataclass +from datetime import datetime, timezone +import dateutil.parser +import lmdb # type: ignore +import os +from typing import Dict, List, Optional, Tuple, Union +from typing_extensions import Literal + +# Adapted from src/SAWScript/SolverCache.hs +SolverBackend = Union[ + Literal["What4"], + Literal["SBV"], + Literal["AIG"], + Literal["RME"], + # External solvers supported by SBV (adapted from SBV.Solver) + Literal["ABC"], + Literal["Boolector"], + Literal["Bitwuzla"], # NOTE: Not currently supported by SAW + Literal["CVC4"], + Literal["CVC5"], + Literal["DReal"], # NOTE: Not currently supported by SAW + Literal["MathSAT"], + Literal["Yices"], + Literal["Z3"]] + +@dataclass +class SolverCacheEntry: + counterexamples : Optional[List[List]] + solver_name : str + solver_versions : Dict[SolverBackend, str] + solver_options : List[List] + timestamp : datetime + + def __post_init__(self): + if self.counterexamples is not None: + if not isinstance(self.counterexamples, list) or \ + any(not isinstance(cex, list) for cex in self.counterexamples): + raise ValueError('`counterexamples` must be a list of lists') + if not isinstance(self.solver_name, str): + raise ValueError('`solver_name` must be a string') + if not isinstance(self.solver_versions, dict) or \ + any(not isinstance(k, str) or not isinstance(v, str) for k,v in self.solver_versions.items()): + raise ValueError('`solver_versions` must be a `dict` with `str` keys and values') + if self.solver_options is not None: + if not isinstance(self.solver_options, list) or \ + any(not isinstance(opt, list) for opt in self.solver_options): + raise ValueError('`solver_options` must be a list of lists') + if not isinstance(self.timestamp, datetime): + raise ValueError('`timestamp` must be a `datetime` object') + +def load_solver_cache_entry(enc): + obj = cbor2.loads(enc) + opts = obj['opts'] if 'opts' in obj else [] + t = dateutil.parser.isoparse(obj['t']) + return SolverCacheEntry(obj.get('cexs'), obj['nm'], obj['vs'], opts, t) + +def solver_cache_entry_encoder(encoder, entry): + if not isinstance(entry, SolverCacheEntry): + raise Exception('cannot serialize type %s' % entry.__class__) + entry.__post_init__() # re-validate everything just to be sure + obj = {} # this dict should be created in alphabetical order to match the Haskell + if entry.counterexamples is not None: obj['cexs'] = entry.counterexamples + obj['nm'] = entry.solver_name + if len(entry.solver_options) > 0: obj['opts'] = entry.solver_options + obj['t'] = entry.timestamp.astimezone(timezone.utc).isoformat('T').replace('+00:00', 'Z') + obj['vs'] = entry.solver_versions + return encoder.encode(obj) + +class SolverCache(MutableMapping): + """An interface for interacting with a SAW solver cache. This is implemented + as a `MutableMapping` from a 256-bit `bytes` keys to `SolverCacheEntry` + values, with LMDB as the backend.""" + + def __init__(self, path : Optional[str] = None): + """Immediately open a solver cache at the given path, or if no path is + given, at the path specified by the current value of the + `SAW_SOLVER_CACHE_PATH` environment variable. If neither the former is + given nor the latter is set, a `ValueError` is raised.""" + if path is None: + if 'SAW_SOLVER_CACHE_PATH' not in os.environ or os.environ['SAW_SOLVER_CACHE_PATH'] == '': + raise ValueError("no path given to SolverCache and SAW_SOLVER_CACHE_PATH not set") + path = os.environ['SAW_SOLVER_CACHE_PATH'] + self.env = lmdb.Environment(path, map_size = 4 * 1073741824) # 4 GiB + self.path = path + + def __len__(self): + with self.env.begin() as txn: + return txn.stat()['entries'] + + def __getitem__(self, k : bytes): + if not isinstance(k, bytes) or len(k) != 32: + raise ValueError("solver cache key must be a 256-bit `bytes` value") + with self.env.begin() as txn: + v = txn.get(cbor2.dumps(k)) + if v is None: raise KeyError + return load_solver_cache_entry(v) + + def __setitem__(self, k : bytes, v : SolverCacheEntry): + if not isinstance(k, bytes) or len(k) != 32: + raise ValueError("solver cache key must be a 256-bit `bytes` value") + if not isinstance(v, SolverCacheEntry): + raise ValueError("solver cache value must be a `SolverCacheEntry` object") + with self.env.begin(write = True) as txn: + txn.put(cbor2.dumps(k), cbor2.dumps(v, default=solver_cache_entry_encoder), overwrite=True) + + def __delitem__(self, k : bytes): + if not isinstance(k, bytes) or len(k) != 32: + raise ValueError("solver cache key must be a 256-bit `bytes` value") + with self.env.begin(write = True) as txn: + txn.delete(cbor2.dumps(k)) + + def _iter(self, keys, values, fn): + with self.env.begin() as txn: + with txn.cursor() as curs: + for v in curs.iternext(keys, values): + yield fn(v) + + def __iter__(self): yield from self._iter(True, False, cbor2.loads) + def keys (self): yield from self._iter(True, False, cbor2.loads) + def values (self): yield from self._iter(False, True, load_solver_cache_entry) + def items (self): yield from self._iter(True, True, lambda kv: (cbor2.loads(kv[0]), load_solver_cache_entry(kv[1]))) diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index 016c01c853..5ec7c5882c 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -6,6 +6,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeApplications #-} module SAWServer @@ -26,6 +27,7 @@ import qualified Data.Text as T import qualified Crypto.Hash as Hash --import qualified Crypto.Hash.Conduit as Hash import System.Directory (getCurrentDirectory) +import System.Environment (lookupEnv) import System.IO.Silently (silence) import qualified Cryptol.Parser.AST as P @@ -63,6 +65,7 @@ import Verifier.SAW.CryptolEnv (initCryptolEnv, bindTypedTerm) import qualified Cryptol.Utils.Ident as Cryptol import Verifier.SAW.Cryptol.Monadify (defaultMonEnv) import SAWScript.Prover.MRSolver (emptyMREnv) +import SAWScript.SolverCache (lazyOpenSolverCache) import qualified Argo --import qualified CryptolServer (validateServerState, ServerState(..)) @@ -207,6 +210,9 @@ initialState readFileFn = halloc <- Crucible.newHandleAllocator jvmTrans <- CJ.mkInitialJVMContext halloc cwd <- getCurrentDirectory + mb_cache <- lookupEnv "SAW_SOLVER_CACHE_PATH" >>= \case + Just path | not (null path) -> Just <$> lazyOpenSolverCache path + _ -> return Nothing let ro = TopLevelRO { roJavaCodebase = jcb , roOptions = opts @@ -233,6 +239,7 @@ initialState readFileFn = , rwMonadify = defaultMonEnv , rwMRSolverEnv = emptyMREnv , rwPPOpts = defaultPPOpts + , rwSolverCache = mb_cache , rwTheoremDB = emptyTheoremDB , rwSharedContext = sc , rwJVMTrans = jvmTrans diff --git a/saw-script.cabal b/saw-script.cabal index 8e42049f28..41534fcd4a 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -30,8 +30,10 @@ library , bimap , bytestring , bv-sized >= 1.0 && < 1.1 + , cborg-json , containers , constraints >= 0.6 + , cryptohash-sha256 >= 0.11.102.1 , cryptol , cryptol-saw-core , crucible >= 0.4 @@ -59,6 +61,7 @@ library , lens , llvm-pretty >= 0.8 , llvm-pretty-bc-parser >= 0.1.3.1 + , lmdb-simple , macaw-base , macaw-x86 , macaw-symbolic @@ -82,6 +85,7 @@ library , saw-core-sbv , saw-core-what4 , sbv >= 9.1 && < 9.3 + , serialise , split , temporary , template-haskell @@ -126,6 +130,8 @@ library SAWScript.Position SAWScript.SBVParser SAWScript.SBVModel + SAWScript.SolverCache + SAWScript.SolverVersions SAWScript.Token SAWScript.TopLevel SAWScript.MGU @@ -188,6 +194,11 @@ library SAWScript.Yosys.TransitionSystem SAWScript.Yosys.Utils + other-modules: + GitRev + autogen-modules: + GitRev + GHC-options: -O2 -Wall -fno-ignore-asserts -fno-spec-constr-count if impl(ghc == 8.0.1) ghc-options: -Wno-redundant-constraints diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 5130051d5f..f732a1e67b 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -125,6 +125,8 @@ import SAWScript.Crucible.Common (PathSatSolver(..)) import SAWScript.TopLevel import qualified SAWScript.Value as SV import SAWScript.Value (ProofScript, printOutLnTop, AIGNetwork) +import SAWScript.SolverCache +import SAWScript.SolverVersions import SAWScript.Crucible.Common.MethodSpec (ppTypedTermType) import SAWScript.Prover.Util(checkBooleanSchema) @@ -922,7 +924,7 @@ goal_num_ite n s1 s2 = proveABC :: ProofScript () proveABC = do SV.AIGProxy proxy <- SV.scriptTopLevel SV.getProxy - wrapProver (Prover.proveABC proxy) + wrapProver [AIG] [] (Prover.proveABC proxy) Set.empty satExternal :: Bool -> String -> [String] -> ProofScript () satExternal doCNF execName args = @@ -947,7 +949,7 @@ writeSAIGComputedPrim = Prover.writeSAIG -- | Bit-blast a proposition check its validity using the RME library. proveRME :: ProofScript () -proveRME = wrapProver Prover.proveRME +proveRME = wrapProver [RME] [] Prover.proveRME Set.empty codegenSBV :: SharedContext -> FilePath -> [String] -> String -> TypedTerm -> TopLevel () codegenSBV sc path unints fname (TypedTerm _schema t) = @@ -967,35 +969,57 @@ proveUnintSBV :: SBV.SMTConfig -> [String] -> ProofScript () proveUnintSBV conf unints = do timeout <- psTimeout <$> get unintSet <- SV.scriptTopLevel (resolveNames unints) - wrapProver (Prover.proveUnintSBV conf unintSet timeout) - -applyProverToGoal :: (Sequent -> TopLevel (Maybe CEX, SolverStats)) + wrapProver (sbvBackends conf) [] + (Prover.proveUnintSBV conf timeout) unintSet + +-- | Given a continuation which calls a prover, call the continuation on the +-- 'goalSequent' of the given 'ProofGoal' and return a 'SolveResult'. If there +-- is a 'SolverCache', do not call the continuation if the goal has an already +-- cached result, and otherwise save the result of the call to the cache. +applyProverToGoal :: [SolverBackend] -> [SolverBackendOption] + -> (SATQuery -> TopLevel (Maybe CEX, String)) + -> Set VarIndex -> ProofGoal -> TopLevel (SolverStats, SolveResult) -applyProverToGoal f g = do - (mb, stats) <- f (goalSequent g) +applyProverToGoal backends opts f unintSet g = do + sc <- getSharedContext + let opt_backends = concatMap optionBackends opts + vs <- io $ getSolverBackendVersions (backends ++ opt_backends) + satq <- io $ sequentToSATQuery sc unintSet (goalSequent g) + k <- io $ mkSolverCacheKey sc vs opts satq + (mb, solver_name) <- SV.onSolverCache (lookupInSolverCache k) >>= \case + -- Use a cached result if one exists (and it's valid w.r.t our query) + Just v -> return $ fromSolverCacheValue satq v + -- Otherwise try to cache the result of the call + _ -> f satq >>= \res -> io (toSolverCacheValue vs opts satq res) >>= \case + Just v -> SV.onSolverCache (insertInSolverCache k v) >> + return res + Nothing -> return res + let stats = solverStats solver_name (sequentSharedSize (goalSequent g)) case mb of Nothing -> return (stats, SolveSuccess (SolverEvidence stats (goalSequent g))) Just a -> return (stats, SolveCounterexample a) wrapProver :: - (Sequent -> TopLevel (Maybe CEX, SolverStats)) -> + [SolverBackend] -> [SolverBackendOption] -> + (SATQuery -> TopLevel (Maybe CEX, String)) -> + Set VarIndex -> ProofScript () -wrapProver f = execTactic $ tacticSolve $ applyProverToGoal f +wrapProver backends opts f = + execTactic . tacticSolve . applyProverToGoal backends opts f wrapW4Prover :: - ( Set VarIndex -> Bool -> - Sequent -> TopLevel (Maybe CEX, SolverStats)) -> + SolverBackend -> [SolverBackendOption] -> + ( Bool -> SATQuery -> TopLevel (Maybe CEX, String) ) -> [String] -> ProofScript () -wrapW4Prover f unints = do +wrapW4Prover backend opts f unints = do hashConsing <- SV.scriptTopLevel $ gets SV.rwWhat4HashConsing unintSet <- SV.scriptTopLevel $ resolveNames unints - wrapProver $ f unintSet hashConsing + wrapProver [What4, backend] opts (f hashConsing) unintSet wrapW4ProveExporter :: - ( Set VarIndex -> Bool -> FilePath -> - Sequent -> TopLevel (Maybe CEX, SolverStats)) -> + ( Bool -> FilePath -> SATQuery -> TopLevel (Maybe CEX, String) ) -> [String] -> String -> String -> @@ -1005,7 +1029,11 @@ wrapW4ProveExporter f unints path ext = do unintSet <- SV.scriptTopLevel $ resolveNames unints execTactic $ tacticSolve $ \g -> do let file = path ++ "." ++ goalType g ++ show (goalNum g) ++ ext - applyProverToGoal (f unintSet hashConsing file) g + sc <- getSharedContext + satq <- io $ sequentToSATQuery sc unintSet (goalSequent g) + (_, solver_name) <- f hashConsing file satq + let stats = solverStats solver_name (sequentSharedSize (goalSequent g)) + return (stats, SolveSuccess (SolverEvidence stats (goalSequent g))) -------------------------------------------------- proveABC_SBV :: ProofScript () @@ -1050,40 +1078,40 @@ proveUnintYices = proveUnintSBV SBV.yices -------------------------------------------------- w4_abc_smtlib2 :: ProofScript () -w4_abc_smtlib2 = wrapW4Prover Prover.proveWhat4_abc [] +w4_abc_smtlib2 = wrapW4Prover ABC [W4_SMTLib2] Prover.proveWhat4_abc [] w4_boolector :: ProofScript () -w4_boolector = wrapW4Prover Prover.proveWhat4_boolector [] +w4_boolector = wrapW4Prover Boolector [] Prover.proveWhat4_boolector [] w4_z3 :: ProofScript () -w4_z3 = wrapW4Prover Prover.proveWhat4_z3 [] +w4_z3 = wrapW4Prover Z3 [] Prover.proveWhat4_z3 [] w4_cvc4 :: ProofScript () -w4_cvc4 = wrapW4Prover Prover.proveWhat4_cvc4 [] +w4_cvc4 = wrapW4Prover CVC4 [] Prover.proveWhat4_cvc4 [] w4_cvc5 :: ProofScript () -w4_cvc5 = wrapW4Prover Prover.proveWhat4_cvc5 [] +w4_cvc5 = wrapW4Prover CVC5 [] Prover.proveWhat4_cvc5 [] w4_yices :: ProofScript () -w4_yices = wrapW4Prover Prover.proveWhat4_yices [] +w4_yices = wrapW4Prover Yices [] Prover.proveWhat4_yices [] w4_unint_boolector :: [String] -> ProofScript () -w4_unint_boolector = wrapW4Prover Prover.proveWhat4_boolector +w4_unint_boolector = wrapW4Prover Boolector [] Prover.proveWhat4_boolector w4_unint_z3 :: [String] -> ProofScript () -w4_unint_z3 = wrapW4Prover Prover.proveWhat4_z3 +w4_unint_z3 = wrapW4Prover Z3 [] Prover.proveWhat4_z3 w4_unint_z3_using :: String -> [String] -> ProofScript () -w4_unint_z3_using tactic = wrapW4Prover (Prover.proveWhat4_z3_using tactic) +w4_unint_z3_using tactic = wrapW4Prover Z3 [W4_Tactic tactic] (Prover.proveWhat4_z3_using tactic) w4_unint_cvc4 :: [String] -> ProofScript () -w4_unint_cvc4 = wrapW4Prover Prover.proveWhat4_cvc4 +w4_unint_cvc4 = wrapW4Prover CVC4 [] Prover.proveWhat4_cvc4 w4_unint_cvc5 :: [String] -> ProofScript () -w4_unint_cvc5 = wrapW4Prover Prover.proveWhat4_cvc5 +w4_unint_cvc5 = wrapW4Prover CVC5 [] Prover.proveWhat4_cvc5 w4_unint_yices :: [String] -> ProofScript () -w4_unint_yices = wrapW4Prover Prover.proveWhat4_yices +w4_unint_yices = wrapW4Prover Yices [] Prover.proveWhat4_yices offline_w4_unint_z3 :: [String] -> String -> ProofScript () offline_w4_unint_z3 unints path = @@ -1166,10 +1194,10 @@ offline_verilog path = proveWithSATExporter Prover.writeVerilogSAT mempty path "." ".v" w4_abc_aiger :: ProofScript () -w4_abc_aiger = wrapW4Prover Prover.w4AbcAIGER [] +w4_abc_aiger = wrapW4Prover ABC [W4_AIGER] Prover.w4AbcAIGER [] w4_abc_verilog :: ProofScript () -w4_abc_verilog = wrapW4Prover Prover.w4AbcVerilog [] +w4_abc_verilog = wrapW4Prover ABC [W4_Verilog] Prover.w4AbcVerilog [] set_timeout :: Integer -> ProofScript () set_timeout to = modify (setProofTimeout to) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 8fd5bd5c16..1e25925687 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -10,6 +10,7 @@ Stability : provisional {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} #if !MIN_VERSION_base(4,8,0) {-# LANGUAGE OverlappingInstances #-} @@ -49,6 +50,7 @@ import Data.Set ( Set ) import qualified Data.Text as Text import System.Directory (getCurrentDirectory, setCurrentDirectory, canonicalizePath) import System.FilePath (takeDirectory) +import System.Environment (lookupEnv) import System.Process (readProcess) import qualified SAWScript.AST as SS @@ -67,6 +69,8 @@ import SAWScript.Parser (parseSchema) import SAWScript.TopLevel import SAWScript.Utils import SAWScript.Value +import SAWScript.SolverCache +import SAWScript.SolverVersions import SAWScript.Proof (emptyTheoremDB) import SAWScript.Prover.Rewrite(basic_ss) import SAWScript.Prover.Exporter @@ -453,6 +457,9 @@ buildTopLevelEnv proxy opts = ss <- basic_ss sc jcb <- JCB.loadCodebase (jarList opts) (classPath opts) (javaBinDirs opts) currDir <- getCurrentDirectory + mb_cache <- lookupEnv "SAW_SOLVER_CACHE_PATH" >>= \case + Just path | not (null path) -> Just <$> lazyOpenSolverCache path + _ -> return Nothing Crucible.withHandleAllocator $ \halloc -> do let ro0 = TopLevelRO { roJavaCodebase = jcb @@ -487,6 +494,7 @@ buildTopLevelEnv proxy opts = , rwProofs = [] , rwPPOpts = SAWScript.Value.defaultPPOpts , rwSharedContext = sc + , rwSolverCache = mb_cache , rwTheoremDB = emptyTheoremDB , rwJVMTrans = jvmTrans , rwPrimsAvail = primsAvail @@ -637,6 +645,24 @@ disable_lax_loads_and_stores = do rw <- getTopLevelRW putTopLevelRW rw { rwLaxLoadsAndStores = False } +set_solver_cache_path :: FilePath -> TopLevel () +set_solver_cache_path path = do + rw <- getTopLevelRW + case rwSolverCache rw of + Just _ -> onSolverCache (setSolverCachePath path) + Nothing -> do cache <- io $ openSolverCache path + putTopLevelRW rw { rwSolverCache = Just cache } + +clean_solver_cache :: TopLevel () +clean_solver_cache = do + vs <- io $ getSolverBackendVersions allBackends + onSolverCache (cleanSolverCache vs) + +test_solver_cache_stats :: Integer -> Integer -> Integer -> Integer -> + Integer -> TopLevel () +test_solver_cache_stats sz ls ls_f is is_f = + onSolverCache (testSolverCacheStats sz ls ls_f is is_f) + enable_debug_intrinsics :: TopLevel () enable_debug_intrinsics = do rw <- getTopLevelRW @@ -1057,6 +1083,55 @@ primitives = Map.fromList , "currently are 'z3' and 'yices'." ] + , prim "set_solver_cache_path" "String -> TopLevel ()" + (pureVal set_solver_cache_path) + Current + [ "Create a solver result cache at the given path, add to that cache all results" + , "in the currently used solver result cache, if there is one, then use the newly" + , "created cache as the solver result cache going forward. Note that if the" + , "SAW_SOLVER_CACHE_PATH environment variable was set at startup but solver" + , "caching has yet to actually be used, then the value of the environment" + , "variable is ignored." + ] + + , prim "clean_solver_cache" "TopLevel ()" + (pureVal clean_solver_cache) + Current + [ "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." + ] + + , prim "print_solver_cache" "String -> TopLevel ()" + (pureVal (onSolverCache . printSolverCacheByHex)) + Current + [ "Print all entries in the solver result cache whose SHA256 hash" + , "keys start with the given hex string. Providing an empty string" + , "results in all entries in the cache being printed." + ] + + , prim "print_solver_cache_stats" "TopLevel ()" + (pureVal (onSolverCache printSolverCacheStats)) + Current + [ "Print out statistics about how the solver cache has been used, namely:" + , "1. How many entries are in the cache (and where the cache is stored)" + , "2. How many insertions into the cache have been made so far this session" + , "3. How many failed insertion attempts have been made so far this session" + , "4. How times cached results have been used so far this session" + , "5. How many failed attempted usages have occurred so far this session." ] + + , prim "test_solver_cache_stats" "Int -> Int -> Int -> Int -> Int -> TopLevel ()" + (pureVal test_solver_cache_stats) + Current + [ "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:" + , "1. How many entries are in the cache" + , "2. How many insertions into the cache have been made so far this session" + , "3. How many failed insertion attempts have been made so far this session" + , "4. How times cached results have been used so far this session" + , "5. How many failed attempted usages have occurred so far this session" ] + , prim "enable_debug_intrinsics" "TopLevel ()" (pureVal enable_debug_intrinsics) Current diff --git a/src/SAWScript/Prover/ABC.hs b/src/SAWScript/Prover/ABC.hs index d1e4c79814..7fda525b56 100644 --- a/src/SAWScript/Prover/ABC.hs +++ b/src/SAWScript/Prover/ABC.hs @@ -12,7 +12,6 @@ import Data.Char (isSpace) import Data.List (isPrefixOf) import qualified Data.Map as Map import Data.Maybe -import Data.Set (Set) import qualified Data.Text as Text import Text.Read (readMaybe) @@ -32,7 +31,7 @@ import qualified Verifier.SAW.Simulator.BitBlast as BBSim import SAWScript.Proof ( sequentToSATQuery, goalSequent, ProofGoal , goalType, goalNum, CEX - , Sequent, sequentSharedSize + , sequentSharedSize ) import SAWScript.Prover.SolverStats (SolverStats, solverStats) import qualified SAWScript.Prover.Exporter as Exporter @@ -48,15 +47,13 @@ import Lang.JVM.ProcessUtils (readProcessExitIfFailure) proveABC :: (AIG.IsAIG l g) => AIG.Proxy l g -> - Sequent -> - TopLevel (Maybe CEX, SolverStats) -proveABC proxy goal = getSharedContext >>= \sc -> liftIO $ - do satq <- sequentToSATQuery sc mempty goal - BBSim.withBitBlastedSATQuery proxy sc mempty satq $ \be lit shapes -> - do let (ecs,fts) = unzip shapes - res <- getModel ecs fts =<< AIG.checkSat be lit - let stats = solverStats "ABC" (sequentSharedSize goal) - return (res, stats) + SATQuery -> + TopLevel (Maybe CEX, String) +proveABC proxy satq = getSharedContext >>= \sc -> liftIO $ + BBSim.withBitBlastedSATQuery proxy sc mempty satq $ \be lit shapes -> + do let (ecs,fts) = unzip shapes + res <- getModel ecs fts =<< AIG.checkSat be lit + return (res, "ABC") getModel :: @@ -85,20 +82,18 @@ getModel argNames shapes satRes = w4AbcVerilog :: - Set VarIndex -> Bool -> - Sequent -> - TopLevel (Maybe CEX, SolverStats) + SATQuery -> + TopLevel (Maybe CEX, String) w4AbcVerilog = w4AbcExternal Exporter.writeVerilogSAT cmd where cmd tmp tmpCex = "%read " ++ tmp ++ "; %blast; &sweep -C 5000; &syn4; &cec -m; write_aiger_cex " ++ tmpCex w4AbcAIGER :: - Set VarIndex -> Bool -> - Sequent -> - TopLevel (Maybe CEX, SolverStats) + SATQuery -> + TopLevel (Maybe CEX, String) w4AbcAIGER = do w4AbcExternal Exporter.writeAIG_SAT cmd where cmd tmp tmpCex = "read_aiger " ++ tmp ++ "; sat; write_cex " ++ tmpCex @@ -106,19 +101,16 @@ w4AbcAIGER = w4AbcExternal :: (FilePath -> SATQuery -> TopLevel [(ExtCns Term, FiniteType)]) -> (String -> String -> String) -> - Set VarIndex -> Bool -> - Sequent -> - TopLevel (Maybe CEX, SolverStats) -w4AbcExternal exporter argFn unints _hashcons goal = + SATQuery -> + TopLevel (Maybe CEX, String) +w4AbcExternal exporter argFn _hashcons satq = -- Create temporary files do let tpl = "abc_verilog.v" tplCex = "abc_verilog.cex" - sc <- getSharedContext tmp <- liftIO $ emptySystemTempFile tpl tmpCex <- liftIO $ emptySystemTempFile tplCex - satq <- liftIO $ sequentToSATQuery sc unints goal (argNames, argTys) <- unzip <$> exporter tmp satq -- Run ABC and remove temporaries @@ -130,7 +122,6 @@ w4AbcExternal exporter argFn unints _hashcons goal = liftIO $ removeFile tmpCex -- Parse and report results - let stats = solverStats "abc_verilog" (sequentSharedSize goal) res <- if all isSpace cexText then return Nothing else do cex <- liftIO $ parseAigerCex cexText argTys @@ -138,7 +129,7 @@ w4AbcExternal exporter argFn unints _hashcons goal = Left parseErr -> fail parseErr Right vs -> return $ Just model where model = zip argNames (map toFirstOrderValue vs) - return (res, stats) + return (res, "abc_verilog") parseAigerCex :: String -> [FiniteType] -> IO (Either String [FiniteValue]) parseAigerCex text tys = diff --git a/src/SAWScript/Prover/MRSolver/SMT.hs b/src/SAWScript/Prover/MRSolver/SMT.hs index f5f8be763f..369f4a26b2 100644 --- a/src/SAWScript/Prover/MRSolver/SMT.hs +++ b/src/SAWScript/Prover/MRSolver/SMT.hs @@ -49,7 +49,7 @@ import Verifier.SAW.Module import Verifier.SAW.Prelude.Constants import Verifier.SAW.FiniteValue -import SAWScript.Proof (termToProp, propToTerm, prettyProp, propToSequent) +import SAWScript.Proof (termToProp, propToTerm, prettyProp, propToSequent, sequentToSATQuery) import What4.Solver import SAWScript.Prover.What4 @@ -388,12 +388,13 @@ mrProvableRaw prop_term = nenv <- liftIO (scGetNamingEnv sc) debugPrint 2 ("Calling SMT solver with proposition: " ++ prettyProp defaultPPOpts nenv prop) + satq <- liftIO $ sequentToSATQuery sc unints (propToSequent prop) sym <- liftIO $ setupWhat4_sym True -- If there are any saw-core `error`s in the term, this will throw a -- Haskell error - in this case we want to just return False, not stop -- execution smt_res <- liftIO $ - (Right <$> proveWhat4_solver z3Adapter sym unints sc (propToSequent prop) (return ())) + (Right <$> proveWhat4_solver z3Adapter sym sc satq (return ())) `X.catch` \case UserError msg -> return $ Left msg e -> X.throw e diff --git a/src/SAWScript/Prover/RME.hs b/src/SAWScript/Prover/RME.hs index 3f4c9b7fd4..d21db63491 100644 --- a/src/SAWScript/Prover/RME.hs +++ b/src/SAWScript/Prover/RME.hs @@ -8,31 +8,29 @@ import qualified Data.RME as RME import Verifier.SAW.FiniteValue import qualified Verifier.SAW.Simulator.RME as RME +import Verifier.SAW.SATQuery (SATQuery(..)) -import SAWScript.Proof(Sequent, sequentToSATQuery, sequentSharedSize, CEX) -import SAWScript.Prover.SolverStats +import SAWScript.Proof (CEX) import SAWScript.Prover.Util import SAWScript.Value -- | Bit-blast a proposition and check its validity using RME. proveRME :: - Sequent {- ^ A proposition to be proved -} -> - TopLevel (Maybe CEX, SolverStats) -proveRME goal = getSharedContext >>= \sc -> liftIO $ - do satq <- sequentToSATQuery sc mempty goal - RME.withBitBlastedSATQuery sc Map.empty satq $ \lit shapes -> - let stats = solverStats "RME" (sequentSharedSize goal) - in case RME.sat lit of - Nothing -> return (Nothing, stats) - Just cex -> do - let m = Map.fromList cex - let n = sum (map (sizeFiniteType . snd) shapes) - let bs = map (maybe False id . flip Map.lookup m) $ take n [0..] - let r = liftCexBB (map snd shapes) bs - case r of - Left err -> fail $ "Can't parse counterexample: " ++ err - Right vs - | length shapes == length vs -> do - let model = zip (map fst shapes) (map toFirstOrderValue vs) - return (Just model, stats) - | otherwise -> fail $ unwords ["RME SAT results do not match expected arguments", show shapes, show vs] + SATQuery {- ^ The query to be proved -} -> + TopLevel (Maybe CEX, String) +proveRME satq = getSharedContext >>= \sc -> liftIO $ + RME.withBitBlastedSATQuery sc Map.empty satq $ \lit shapes -> + case RME.sat lit of + Nothing -> return (Nothing, "RME") + Just cex -> do + let m = Map.fromList cex + let n = sum (map (sizeFiniteType . snd) shapes) + let bs = map (maybe False id . flip Map.lookup m) $ take n [0..] + let r = liftCexBB (map snd shapes) bs + case r of + Left err -> fail $ "Can't parse counterexample: " ++ err + Right vs + | length shapes == length vs -> do + let model = zip (map fst shapes) (map toFirstOrderValue vs) + return (Just model, "RME") + | otherwise -> fail $ unwords ["RME SAT results do not match expected arguments", show shapes, show vs] diff --git a/src/SAWScript/Prover/SBV.hs b/src/SAWScript/Prover/SBV.hs index 3e4d6114ba..45f214070d 100644 --- a/src/SAWScript/Prover/SBV.hs +++ b/src/SAWScript/Prover/SBV.hs @@ -3,13 +3,11 @@ module SAWScript.Prover.SBV , proveUnintSBVIO , SBV.SMTConfig , SBV.z3, SBV.cvc4, SBV.cvc5, SBV.yices, SBV.mathSAT, SBV.boolector - , prepNegatedSBV ) where import System.Directory import Data.Maybe -import Data.Set ( Set ) import Control.Monad import qualified Data.SBV.Dynamic as SBV @@ -18,9 +16,9 @@ import qualified Data.SBV.Internals as SBV import qualified Verifier.SAW.Simulator.SBV as SBVSim import Verifier.SAW.SharedTerm +import Verifier.SAW.SATQuery (SATQuery(..)) -import SAWScript.Proof(Sequent, sequentSharedSize, sequentToSATQuery, CEX) -import SAWScript.Prover.SolverStats +import SAWScript.Proof (CEX) import SAWScript.Value -- | Bit-blast a proposition and check its validity using SBV. @@ -28,24 +26,22 @@ import SAWScript.Value -- functions. proveUnintSBV :: SBV.SMTConfig {- ^ SBV configuration -} -> - Set VarIndex {- ^ Uninterpreted functions -} -> Maybe Integer {- ^ Timeout in milliseconds -} -> - Sequent {- ^ A proposition to be proved -} -> - TopLevel (Maybe CEX, SolverStats) + SATQuery {- ^ A query to be proved -} -> + TopLevel (Maybe CEX, String) -- ^ (example/counter-example, solver statistics) -proveUnintSBV conf unintSet timeout goal = +proveUnintSBV conf timeout satq = do sc <- getSharedContext - io $ proveUnintSBVIO sc conf unintSet timeout goal + io $ proveUnintSBVIO sc conf timeout satq proveUnintSBVIO :: SharedContext -> SBV.SMTConfig {- ^ SBV configuration -} -> - Set VarIndex {- ^ Uninterpreted functions -} -> Maybe Integer {- ^ Timeout in milliseconds -} -> - Sequent {- ^ A proposition to be proved -} -> - IO (Maybe CEX, SolverStats) + SATQuery {- ^ A query to be proved -} -> + IO (Maybe CEX, String) -- ^ (example/counter-example, solver statistics) -proveUnintSBVIO sc conf unintSet timeout goal = +proveUnintSBVIO sc conf timeout satq = do p <- findExecutable . SBV.executable $ SBV.solver conf unless (isJust p) . fail $ mconcat [ "Unable to locate the executable \"" @@ -54,21 +50,21 @@ proveUnintSBVIO sc conf unintSet timeout goal = , show . SBV.name $ SBV.solver conf ] - (labels, argNames, lit) <- prepNegatedSBV sc unintSet goal + (labels, argNames, lit) <- SBVSim.sbvSATQuery sc mempty satq let script = maybe (return ()) SBV.setTimeOut timeout >> lit SBV.SatResult r <- SBV.satWith conf script - let stats = solverStats ("SBV->" ++ show (SBV.name (SBV.solver conf))) - (sequentSharedSize goal) + let solver_name = "SBV->" ++ show (SBV.name (SBV.solver conf)) + case r of - SBV.Unsatisfiable {} -> return (Nothing, stats) + SBV.Unsatisfiable {} -> return (Nothing, solver_name) SBV.Satisfiable {} -> do let dict = SBV.getModelDictionary r r' = SBVSim.getLabels labels dict argNames - return (r', stats) + return (r', solver_name) SBV.DeltaSat{} -> fail "Prover returned an unexpected DeltaSat result" @@ -77,18 +73,3 @@ proveUnintSBVIO sc conf unintSet timeout goal = SBV.Unknown {} -> fail "Prover returned Unknown" SBV.ProofError _ ls _ -> fail . unlines $ "Prover returned error: " : ls - - --- | Convert a saw-core proposition to a logically-negated SBV --- symbolic boolean formula with existentially quantified variables. --- The returned formula is suitable for checking satisfiability. The --- specified function names are left uninterpreted. - -prepNegatedSBV :: - SharedContext -> - Set VarIndex {- ^ Uninterpreted function names -} -> - Sequent {- ^ Proposition to prove -} -> - IO ([SBVSim.Labeler], [ExtCns Term], SBV.Symbolic SBV.SVal) -prepNegatedSBV sc unintSet goal = - do satq <- sequentToSATQuery sc unintSet goal - SBVSim.sbvSATQuery sc mempty satq diff --git a/src/SAWScript/Prover/What4.hs b/src/SAWScript/Prover/What4.hs index 969a61f74a..52de3e941e 100644 --- a/src/SAWScript/Prover/What4.hs +++ b/src/SAWScript/Prover/What4.hs @@ -19,8 +19,7 @@ import Verifier.SAW.SharedTerm import Verifier.SAW.FiniteValue import Verifier.SAW.SATQuery (SATQuery(..)) -import SAWScript.Proof(Sequent, sequentToSATQuery, sequentSharedSize, CEX) -import SAWScript.Prover.SolverStats +import SAWScript.Proof(Sequent, sequentToSATQuery, CEX) import SAWScript.Value (TopLevel, io, getSharedContext) import Data.Parameterized.Nonce @@ -84,42 +83,39 @@ evalTheories pf = [ nm | (nm,f) <- xs, hasProblemFeature pf f ] proveWhat4_sym :: SolverAdapter St -> - Set VarIndex -> Bool -> - Sequent -> - TopLevel (Maybe CEX, SolverStats) -proveWhat4_sym solver un hashConsing t = + SATQuery -> + TopLevel (Maybe CEX, String) +proveWhat4_sym solver hashConsing satq = getSharedContext >>= \sc -> io $ do sym <- setupWhat4_sym hashConsing - proveWhat4_solver solver sym un sc t (return ()) + proveWhat4_solver solver sym sc satq (return ()) proveExportWhat4_sym :: SolverAdapter St -> - Set VarIndex -> Bool -> FilePath -> - Sequent-> - TopLevel (Maybe CEX, SolverStats) -proveExportWhat4_sym solver un hashConsing outFilePath t = + SATQuery -> + TopLevel (Maybe CEX, String) +proveExportWhat4_sym solver hashConsing outFilePath satq = getSharedContext >>= \sc -> io $ do sym <- setupWhat4_sym hashConsing -- Write smt out - (_, _, lits, stats) <- setupWhat4_solver solver sym un sc t + (_, _, lits, solver_name) <- setupWhat4_solver solver sym sc satq withFile outFilePath WriteMode $ \handle -> solver_adapter_write_smt2 solver sym handle lits -- Assume unsat - return (Nothing, stats) + return (Nothing, solver_name) proveWhat4_z3, proveWhat4_boolector, proveWhat4_cvc4, proveWhat4_cvc5, proveWhat4_dreal, proveWhat4_stp, proveWhat4_yices, proveWhat4_abc :: - Set VarIndex {- ^ Uninterpreted functions -} -> Bool {- ^ Hash-consing of What4 terms -}-> - Sequent {- ^ A proposition to be proved -} -> - TopLevel (Maybe CEX, SolverStats) + SATQuery {- ^ The query to be proved -} -> + TopLevel (Maybe CEX, String) proveWhat4_z3 = proveWhat4_sym z3Adapter proveWhat4_boolector = proveWhat4_sym boolectorAdapter @@ -132,14 +128,13 @@ proveWhat4_abc = proveWhat4_sym externalABCAdapter proveWhat4_z3_using :: String {- ^ Solver tactic -} -> - Set VarIndex {- ^ Uninterpreted functions -} -> Bool {- ^ Hash-consing of What4 terms -}-> - Sequent {- ^ A proposition to be proved -} -> - TopLevel (Maybe CEX, SolverStats) -proveWhat4_z3_using tactic un hashConsing t = + SATQuery {- ^ The query to be proved -} -> + TopLevel (Maybe CEX, String) +proveWhat4_z3_using tactic hashConsing satq = getSharedContext >>= \sc -> io $ do sym <- setupWhat4_sym hashConsing - proveWhat4_solver z3Adapter sym un sc t $ + proveWhat4_solver z3Adapter sym sc satq $ do z3TacticSetting <- getOptionSetting z3Tactic $ getConfiguration sym _ <- setOpt z3TacticSetting $ Text.pack tactic return () @@ -147,11 +142,10 @@ proveWhat4_z3_using tactic un hashConsing t = proveExportWhat4_z3, proveExportWhat4_boolector, proveExportWhat4_cvc4, proveExportWhat4_cvc5, proveExportWhat4_dreal, proveExportWhat4_stp, proveExportWhat4_yices :: - Set VarIndex {- ^ Uninterpreted functions -} -> Bool {- ^ Hash-consing of ExportWhat4 terms -}-> FilePath {- ^ Path of file to write SMT to -}-> - Sequent {- ^ A proposition to be proved -} -> - TopLevel (Maybe CEX, SolverStats) + SATQuery {- ^ The query to be proved -} -> + TopLevel (Maybe CEX, String) proveExportWhat4_z3 = proveExportWhat4_sym z3Adapter proveExportWhat4_boolector = proveExportWhat4_sym boolectorAdapter @@ -165,17 +159,15 @@ proveExportWhat4_yices = proveExportWhat4_sym yicesAdapter setupWhat4_solver :: forall st t ff. SolverAdapter st {- ^ Which solver to use -} -> B.ExprBuilder t st ff {- ^ The glorious sym -} -> - Set VarIndex {- ^ Uninterpreted functions -} -> SharedContext {- ^ Context for working with terms -} -> - Sequent {- ^ A proposition to be proved/checked. -} -> + SATQuery {- ^ The query to be proved/checked. -} -> IO ( [ExtCns Term] , [W.Labeler (B.ExprBuilder t st ff)] , [Pred (B.ExprBuilder t st ff)] - , SolverStats) -setupWhat4_solver solver sym unintSet sc goal = + , String) +setupWhat4_solver solver sym sc satq = do -- symbolically evaluate - satq <- sequentToSATQuery sc unintSet goal let varList = Map.toList (satVariables satq) let argNames = map fst varList (varMap, lits) <- W.w4Solve sym sc satq @@ -184,25 +176,23 @@ setupWhat4_solver solver sym unintSet sc goal = extendConfig (solver_adapter_config_options solver) (getConfiguration sym) - let stats = solverStats ("W4 ->" ++ solver_adapter_name solver) - (sequentSharedSize goal) + let solver_name = "W4 ->" ++ solver_adapter_name solver - return (argNames, bvs, lits, stats) + return (argNames, bvs, lits, solver_name) -- | Check the validity of a proposition using What4. proveWhat4_solver :: forall st t ff. SolverAdapter st {- ^ Which solver to use -} -> B.ExprBuilder t st ff {- ^ The glorious sym -} -> - Set VarIndex {- ^ Uninterpreted functions -} -> SharedContext {- ^ Context for working with terms -} -> - Sequent {- ^ A proposition to be proved/checked. -} -> + SATQuery {- ^ The query to be proved/checked. -} -> IO () {- ^ Extra setup actions -} -> - IO (Maybe CEX, SolverStats) + IO (Maybe CEX, String) -- ^ (example/counter-example, solver statistics) -proveWhat4_solver solver sym unintSet sc goal extraSetup = +proveWhat4_solver solver sym sc satq extraSetup = do - (argNames, bvs, lits, stats) <- setupWhat4_solver solver sym unintSet sc goal + (argNames, bvs, lits, solver_name) <- setupWhat4_solver solver sym sc satq extraSetup -- log to stdout @@ -215,9 +205,9 @@ proveWhat4_solver solver sym unintSet sc goal extraSetup = Sat (gndEvalFcn,_) -> do mvals <- mapM (getValues @(B.ExprBuilder t st ff) gndEvalFcn) (zip bvs argNames) - return (Just mvals, stats) where + return (Just mvals, solver_name) where - Unsat _ -> return (Nothing, stats) + Unsat _ -> return (Nothing, solver_name) Unknown -> fail "Prover returned Unknown" diff --git a/src/SAWScript/SolverCache.hs b/src/SAWScript/SolverCache.hs new file mode 100644 index 0000000000..bf1310b450 --- /dev/null +++ b/src/SAWScript/SolverCache.hs @@ -0,0 +1,618 @@ +{- | +Module : SAWScript.SolverCache +Description : Caching SMT solver results for SAWScript +License : BSD3 +Maintainer : m-yac +Stability : provisional + +This file defines an interface for caching SMT/SAT solver results using an LMDB +database. The interface, as used in 'applyProverToGoal', works as follows: + +1. An 'SMTQuery' is converted into a string using 'scWriteExternal', and + along with any relevant 'SolverBackendVersion's (obtained using + 'getSolverBackendVersions' from @SAWScript.SolverVersions@), is then hashed + using SHA256 ('mkSolverCacheKey'). +2. The core of the 'SolverCache' is an LMDB database mapping these hashes to + previously obtained results ('solverCacheEnv', 'solverCacheDB'). If this is + the first time solver caching is being used and the `SAW_SOLVER_CACHE_PATH` + environment variable was set at startup, then open an LMDB database at the + specified path and use this database for all subsequent uses of the solver + cache. Note that this only occurs if there have been no prior calls to the + `set_solver_cache_path` command, which immediately opens an LMDB database at + specified path when called. +3. If the hash corresponding to the 'SATQuery' and 'SolverBackendVersion's + can be found in the database ('lookupInSolverCache'), then the corresponding + result is used. +4. Otherwise, the 'SATQuery' is dispatched to the requested backend and a + result is obtained. This result is then added to the database using the + aforementioned hash as the key ('insertInSolverCache'). + +A interesting detail is how results are represented. For all of the backends +which use 'applyProverToGoal', the type of a result is: +@Maybe [(ExtCns Term, FirstOrderValue)]@, where 'Nothing' represents a result +of "unsat," and 'Just' represents a result of "sat" along with a list of +counterexamples. Since 'ExtCns' contains execution-specific 'VarIndex'es, we +don't want to save these results directly. Instead, we represent each 'ExtCns' +as its index in the 'satVariables' field of 'SATQuery' (which is where they +were obtained by the backends in the first place). +-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE GeneralisedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE ViewPatterns #-} + +module SAWScript.SolverCache + ( SolverBackend(..) + , allBackends + , sbvBackends + , SolverBackendOption(..) + , optionBackends + , SolverBackendVersions + , SolverCacheKey(..) + , mkSolverCacheKey + , SolverCacheValue(..) + , toSolverCacheValue + , fromSolverCacheValue + , SolverCache(..) + , lazyOpenSolverCache + , openSolverCache + , SolverCacheOp + , solverCacheOp + , solverCacheOpDefault + , lookupInSolverCache + , insertInSolverCache + , setSolverCachePath + , printSolverCacheByHex + , cleanSolverCache + , printSolverCacheStats + , testSolverCacheStats + ) where + +import System.Directory (createDirectoryIfMissing) +import Control.Exception (try, SomeException) +import Control.Monad (when, forM_) +import System.Timeout (timeout) + +import GHC.Generics (Generic) +import Data.IORef (IORef, newIORef, modifyIORef, readIORef) +import Data.Time.Clock (UTCTime, getCurrentTime) +import Data.Tuple.Extra (first, firstM) +import Data.List (elemIndex, intercalate, isPrefixOf) +import Data.Maybe (fromMaybe, isJust) +import Data.Functor ((<&>)) +import Numeric (readHex) + +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as M + +import qualified Data.Text as T +import Data.Text.Encoding (encodeUtf8) +import Text.Printf (printf) + +import Data.ByteString (ByteString) +import qualified Data.ByteString as BS + +import qualified Crypto.Hash.SHA256 as SHA256 + +import Data.Aeson ( FromJSON(..), ToJSON(..), FromJSONKey(..), ToJSONKey(..) + , (.:), (.:?), (.=), fromJSON ) +import qualified Data.Aeson as JSON +import Codec.CBOR.JSON (encodeValue, decodeValue) +import Codec.Serialise (Serialise(..)) + +import qualified Database.LMDB.Simple as LMDB +import qualified Database.LMDB.Simple.Extra as LMDB + +import qualified Data.SBV.Dynamic as SBV + +import Verifier.SAW.FiniteValue +import Verifier.SAW.SATQuery +import Verifier.SAW.ExternalFormat +import Verifier.SAW.SharedTerm + +import SAWScript.Options +import SAWScript.Proof + + +-- Helper Functions ------------------------------------------------------------ + +-- | Run the given IO action, but if the given 'timeout' (in microseconds) is +-- reached or the action encounters any 'SomeException', 'Left' is returned +tryWithTimeout :: Int -> IO a -> IO (Either String a) +tryWithTimeout t_us m = try (timeout t_us m) <&> \case + Right (Just a) -> Right a + Right Nothing -> let t_str | t_us `mod` 1000000 == 0 = show (t_us `div` 1000000) ++ "s" + | t_us `mod` 1000 == 0 = show (t_us `div` 1000) ++ "ms" + | otherwise = show t_us ++ "us" + in Left $ "Operation timed out (" ++ t_str ++ ")" + Left (exn :: SomeException) -> Left $ show exn + +-- | Encode a 'ByteString' as a hex string +encodeHex :: ByteString -> String +encodeHex = concatMap (printf "%02x") . BS.unpack + +-- | Decode a hex string as a 'ByteString' +decodeHex :: String -> Either String ByteString +decodeHex s = BS.pack <$> go s + where go (c0:c1:cs) | [(b,[])] <- readHex [c0,c1] = (b:) <$> go cs + go [] = return [] + go _ = Left $ "Hex decoding failure on: " ++ s + + +-- Solver Backends ------------------------------------------------------------- + +-- | 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 supported by SBV (copied from SBV.Solver) + | ABC + | Boolector + | Bitwuzla -- NOTE: Not currently supported by SAW + | CVC4 + | CVC5 + | DReal -- NOTE: Not currently supported by SAW + | MathSAT + | Yices + | Z3 + deriving (Eq, Ord, Enum, Bounded, Show, Generic) + +instance FromJSON SolverBackend where + parseJSON = JSON.genericParseJSON JSON.defaultOptions +instance ToJSON SolverBackend where + toJSON = JSON.genericToJSON JSON.defaultOptions + toEncoding = JSON.genericToEncoding JSON.defaultOptions +instance FromJSONKey SolverBackend where + fromJSONKey = JSON.genericFromJSONKey JSON.defaultJSONKeyOptions +instance ToJSONKey SolverBackend where + toJSONKey = JSON.genericToJSONKey JSON.defaultJSONKeyOptions + +-- | The list of all available 'SolverBackend's +allBackends :: [SolverBackend] +allBackends = [minBound..] + +-- | Given an 'SBV.SMTConfig', return the list of corresponding 'SolverBackend's +sbvBackends :: SBV.SMTConfig -> [SolverBackend] +sbvBackends conf = [SBV, cvtSolver $ SBV.name $ SBV.solver conf] + where cvtSolver SBV.ABC = ABC + cvtSolver SBV.Boolector = Boolector + cvtSolver SBV.Bitwuzla = Bitwuzla + cvtSolver SBV.CVC4 = CVC4 + cvtSolver SBV.CVC5 = CVC5 + cvtSolver SBV.DReal = DReal + cvtSolver SBV.MathSAT = MathSAT + cvtSolver SBV.Yices = Yices + cvtSolver SBV.Z3 = Z3 + +-- | A datatype representing an option to one of the 'SolverBackend's. +-- Currently, there are only the following options for using 'What4': with a +-- tactic ('W4_Tactic'), by converting to SMTLib2 then calling ABC +-- ('W4_SMTLib2'), by converting to Verilog then calling ABC ('W4_Verilog'), +-- or by converting to AIGER then calling ABC ('W4_AIGER'). Note that certain +-- options may imply that additional 'SolverBackend's were used - see +-- 'optionBackends'. +data SolverBackendOption = W4_Tactic String + | W4_SMTLib2 + | W4_Verilog + | W4_AIGER + deriving (Eq, Ord, Show, Generic) + +instance FromJSON SolverBackendOption where + parseJSON = JSON.genericParseJSON JSON.defaultOptions + { JSON.sumEncoding = JSON.TwoElemArray } +instance ToJSON SolverBackendOption where + toJSON = JSON.genericToJSON JSON.defaultOptions + { JSON.sumEncoding = JSON.TwoElemArray } + toEncoding = JSON.genericToEncoding JSON.defaultOptions + { JSON.sumEncoding = JSON.TwoElemArray } + +-- | Given a 'SolverBackendOption', return the list of additional +-- 'SolverBackend's that are used +optionBackends :: SolverBackendOption -> [SolverBackend] +optionBackends W4_AIGER = [AIG] +optionBackends _ = [] + +-- | A map from 'SolverBackend's to their version 'String's, if one could be +-- obtained +type SolverBackendVersions = Map SolverBackend (Maybe String) + +-- | Pretty-print a 'SolverBackend' with its version 'String' +showSolverBackendVersion :: SolverBackend -> Maybe String -> [String] -> String +showSolverBackendVersion backend (Just v_str) opt_words = + unwords $ show backend : v_str : opt_words +showSolverBackendVersion backend Nothing opt_words = + showSolverBackendVersion backend (Just "[unknown version]") opt_words + +-- | Pretty-print a set of 'SolverBackendVersions' and 'SolverBackendOption's +-- with the given 'String' separator +showBackendVersionsWithOptions :: String -> SolverBackendVersions -> + [SolverBackendOption] -> String +showBackendVersionsWithOptions sep vs opts = + let entries = M.unionWith (<>) (M.map (\v -> (v, [])) vs) + (M.fromList $ optEntry <$> opts) + in intercalate sep $ showEntry <$> M.toList entries + where optEntry (W4_Tactic t) = (What4, (Nothing, ["using", t])) + optEntry W4_SMTLib2 = (What4, (Nothing, ["to", "SMTLib2"])) + optEntry W4_Verilog = (What4, (Nothing, ["to", "Verilog"])) + optEntry W4_AIGER = (What4, (Nothing, ["to", "AIGER"])) + showEntry (backend, (mb_v_str, opt_words)) = + showSolverBackendVersion backend mb_v_str opt_words + + +-- Solver Cache Keys ----------------------------------------------------------- + +-- | The key type for 'SolverCache'. Each is a SHA256 hash of a 'SATQuery' (see +-- 'mkSolverCacheKey') along with optional solver version information used only +-- for pretty-printing. +data SolverCacheKey = + SolverCacheKey + { solverCacheKeyVersions :: SolverBackendVersions + , solverCacheKeyOptions :: [SolverBackendOption] + , solverCacheKeyHash :: ByteString + } + +instance Eq SolverCacheKey where + (SolverCacheKey _ _ bs1) == (SolverCacheKey _ _ bs2) = bs1 == bs2 + +instance Show SolverCacheKey where + show (SolverCacheKey vs opts bs) = encodeHex (BS.take 8 bs) ++ + if M.null vs && null opts then "" + else " (" ++ showBackendVersionsWithOptions ", " vs opts ++ ")" + +-- | Make a 'SolverCacheKey' with no version information +solverCacheKeyFromHash :: ByteString -> SolverCacheKey +solverCacheKeyFromHash = SolverCacheKey M.empty [] + +instance Serialise SolverCacheKey where + encode = encode . solverCacheKeyHash + decode = solverCacheKeyFromHash <$> decode + +-- | Hash using SHA256 a 'String' representation of a 'SATQuery' and a 'Set' of +-- 'SolverBackendVersion's to get a 'SolverCacheKey'. In particular, this +-- 'String' representation contains all the 'SolverBackendVersion's, the +-- number of 'satVariables' in the 'SATQuery', the number of 'satUninterp's in +-- the 'SATQuery, and finally the 'scWriteExternal' representation of the +-- 'satQueryAsPropTerm' of the 'SATQuery' - with two additional things: +-- 1. Before calling 'scWriteExternal', we generalize ('scGeneralizeExts') over +-- all 'satVariables' and 'satUninterp's. This ensures the hash does not +-- depend on any execution-specific 'VarIndex'es. +-- 2. After calling 'scWriteExternal', all 'LocalName's in 'Pi' and 'Lam' +-- constructors are removed. This ensures that two terms which are alpha +-- equivalent are given the same hash. +mkSolverCacheKey :: SharedContext -> SolverBackendVersions -> + [SolverBackendOption] -> SATQuery -> IO SolverCacheKey +mkSolverCacheKey sc vs opts satq = do + body <- satQueryAsPropTerm sc satq + let ecs = M.keys (satVariables satq) ++ + filter (\ec -> ecVarIndex ec `elem` satUninterp satq) + (getAllExts body) + tm <- scGeneralizeExts sc ecs body + let str_prefix = [ showBackendVersionsWithOptions "\n" vs opts + , "satVariables " ++ show (M.size (satVariables satq)) + , "satUninterp " ++ show (length (satUninterp satq)) ] + str_to_hash = unlines str_prefix ++ anonLocalNames (scWriteExternal tm) + return $ SolverCacheKey vs opts $ SHA256.hash $ encodeUtf8 $ T.pack $ str_to_hash + where anonLocalNames = unlines . map (unwords . go . words) . lines + go (x:y:_:xs) | y `elem` ["Pi", "Lam"] = x:y:"_":xs + go xs = xs + + +-- Solver Cache Values --------------------------------------------------------- + +-- | The value type for 'SolverCache': solver version information, the timestamp +-- of when the entry was last used, a 'String' representing the solver used, and +-- an optional list of counterexamples, represented as pairs of indexes into the +-- list of 'satVariables' of an associated 'SATQuery' +data SolverCacheValue = + SolverCacheValue + { solverCacheValueVersions :: SolverBackendVersions + , solverCacheValueOptions :: [SolverBackendOption] + , solverCacheValueSolverName :: String + , solverCacheValueCEXs :: Maybe [(Int, FirstOrderValue)] + , solverCacheValueLastUsed :: UTCTime + } deriving Eq + +instance FromJSON SolverCacheValue where + parseJSON = JSON.withObject "SolverCacheValue" $ \v -> do + vs <- v .: "vs" + opts <- v .:? "opts" + nm <- v .: "nm" + mb_cexs <- v .:? "cexs" + t <- v .: "t" + return $ SolverCacheValue vs (fromMaybe [] opts) nm mb_cexs t + +instance ToJSON SolverCacheValue where + toJSON (SolverCacheValue vs opts nm mb_cexs t) = JSON.object $ + ["vs" .= vs] ++ (if null opts then [] else ["opts" .= opts]) ++ + ["nm" .= nm] ++ maybe [] (\cexs -> ["cexs" .= cexs]) mb_cexs ++ ["t" .= t] + toEncoding (SolverCacheValue vs opts nm mb_cexs t) = JSON.pairs $ + "vs" .= vs <> (if null opts then mempty else "opts" .= opts) <> + "nm" .= nm <> maybe mempty (\cexs -> "cexs" .= cexs) mb_cexs <> "t" .= t + +-- NOTE: We go through JSON because the `aeson` library gives us much nicer and +-- more customizable encodings than the `serialise` library, and because there +-- is a bijection between JSON and CBOR so we can freely pass between the two +instance Serialise SolverCacheValue where + encode = encodeValue . toJSON + decode = do + v <- decodeValue False + case fromJSON v of + JSON.Success x -> return x + JSON.Error e -> fail e + +-- | Convert the result of a solver call on the given 'SATQuery' to a +-- 'SolverCacheValue' +toSolverCacheValue :: SolverBackendVersions -> [SolverBackendOption] -> + SATQuery -> (Maybe CEX, String) -> + IO (Maybe SolverCacheValue) +toSolverCacheValue vs opts satq (cexs, solver_name) = do + getCurrentTime <&> \t -> case firstsMaybeM (`elemIndex` ecs) cexs of + Just cexs' -> Just $ SolverCacheValue vs opts solver_name cexs' t + Nothing -> Nothing + where ecs = M.keys $ satVariables satq + firstsMaybeM :: Monad m => (a -> m b) -> + Maybe [(a, c)] -> m (Maybe [(b, c)]) + firstsMaybeM = mapM . mapM . firstM + +-- | Convert a 'SolverCacheValue' to something which has the same form as the +-- result of a solver call on the given 'SATQuery' +fromSolverCacheValue :: SATQuery -> SolverCacheValue -> (Maybe CEX, String) +fromSolverCacheValue satq (SolverCacheValue _ _ solver_name cexs _) = + (firstsMaybe (ecs !!) cexs, solver_name) + where ecs = M.keys $ satVariables satq + firstsMaybe :: (a -> b) -> Maybe [(a, c)] -> Maybe [(b, c)] + firstsMaybe = fmap . fmap . first + + +-- The Solver Cache ------------------------------------------------------------ + +-- | A 'SolverCache' consists of a 'FilePath' to an LMDB database (which may or +-- may not exist yet), an optional LMDB database at that path (represented as an +-- 'LMDB.Environment' and 'LMDB.Database' once it is created), counters for how +-- many lookups, failed lookups, insertions, and failed insertions have been made +-- (see 'SolverCacheStat'), a map size for the LMDB database, and a timeout to +-- use for database lookups and inserts. Note that the counters are stored in an +-- 'IORef' to make sure failures are counted correctly. +data SolverCache = + SolverCache + { solverCachePath :: FilePath + , solverCacheEnv :: Maybe (LMDB.Environment LMDB.ReadWrite) + , solverCacheDB :: Maybe (LMDB.Database SolverCacheKey SolverCacheValue) + , solverCacheStats :: IORef (Map SolverCacheStat Integer) + , solverCacheMapSize :: Int + , solverCacheTimeout :: Int + } + +-- | A statistic to track in 'solverCacheStats' +data SolverCacheStat = Lookups | FailedLookups | Inserts | FailedInserts + deriving (Eq, Ord, Bounded, Enum) + +-- | Create a 'SolverCache' with the given 'FilePath', but do not yet open an +-- LMDB database at that path (i.e. `solverCacheEnv` and `solverCacheDB` are +-- both set to 'Nothing') +lazyOpenSolverCache :: FilePath -> IO SolverCache +lazyOpenSolverCache path = do + stats <- newIORef $ M.fromList ((,0) <$> [minBound..]) + return SolverCache { solverCachePath = path, + solverCacheEnv = Nothing, + solverCacheDB = Nothing, + solverCacheStats = stats, + solverCacheMapSize = 4 {- GiB -} * 1073741824, + solverCacheTimeout = 1 {- sec -} * 1000000 } + +-- | Create a 'SolverCache' with the given 'FilePath' and open an LMDB database +-- at that path (i.e. `solverCacheEnv` and `solverCacheDB` are both 'Just') +openSolverCache :: FilePath -> IO SolverCache +openSolverCache path = do + (_, _, cache') <- forceSolverCacheOpened =<< lazyOpenSolverCache path + return cache' + +-- | Ensure that the given 'SolverCache' has opened an LMDB database at its set +-- 'FilePath' - returning either the newly created or previously created +-- 'LMDB.Environment' and 'LMDB.Database', as well as an 'SolverCache' +-- containing both of them +forceSolverCacheOpened :: SolverCache -> + IO (LMDB.Environment LMDB.ReadWrite, + LMDB.Database SolverCacheKey SolverCacheValue, + SolverCache) +forceSolverCacheOpened cache@SolverCache{ solverCacheEnv = Just env + , solverCacheDB = Just db } = + return (env, db, cache) +forceSolverCacheOpened cache@SolverCache{..} = do + createDirectoryIfMissing True solverCachePath + let limits = LMDB.defaultLimits { LMDB.mapSize = solverCacheMapSize } + env <- LMDB.openEnvironment solverCachePath limits + db <- LMDB.readOnlyTransaction env (LMDB.getDatabase Nothing) + let cache' = cache { solverCacheEnv = Just env, solverCacheDB = Just db } + return (env, db, cache') + +-- | Try to call 'forceSolverCacheOpened' then try to perform the given +-- 'LMDB.Transaction' on the LMDB database associated to the given +-- 'SolverCache', returning 'Left' if an error or timeout occurred at any point +-- and 'Right' otherwise, as well as the updated 'SolverCache' returned by +-- 'forceSolverCacheOpened' +tryTransaction :: (LMDB.Mode tmode, LMDB.SubMode LMDB.ReadWrite tmode) => + SolverCache -> + (LMDB.Database SolverCacheKey SolverCacheValue -> + LMDB.Transaction tmode a) -> + IO (Either String a, SolverCache) +tryTransaction cache@SolverCache{..} t = + tryWithTimeout solverCacheTimeout (forceSolverCacheOpened cache) >>= \case + Right (env, db, cache') -> + (,cache') <$> tryWithTimeout solverCacheTimeout + (LMDB.transaction env (t db)) + Left err -> + return (Left $ "Failed to open LMDB database: " ++ err, cache) + +-- | An operation on a 'SolverCache', returning a value of the given type as +-- well as an updated 'SolverCache' ('solverCacheOp'). Additionally, in the case +-- of no enabled solver cache, the operation could either fail or return a +-- default value ('solverCacheOpDefault'). +data SolverCacheOp a = SCOpOrFail (Options -> SolverCache -> IO (a, SolverCache)) + | SCOpOrDefault a (Options -> SolverCache -> IO (a, SolverCache)) + +-- | Get the operation associated to a 'SolverCacheOp' +solverCacheOp :: SolverCacheOp a -> Options -> SolverCache -> IO (a, SolverCache) +solverCacheOp (SCOpOrFail f) = f +solverCacheOp (SCOpOrDefault _ f) = f + +-- | Get the default value associated to a 'SolverCacheOp', if any +solverCacheOpDefault :: SolverCacheOp a -> Maybe a +solverCacheOpDefault (SCOpOrFail _) = Nothing +solverCacheOpDefault (SCOpOrDefault a _) = Just a + +-- | Lookup a 'SolverCacheKey' in the solver result cache +lookupInSolverCache :: SolverCacheKey -> SolverCacheOp (Maybe SolverCacheValue) +lookupInSolverCache k = SCOpOrDefault Nothing $ \opts cache@SolverCache{..} -> + getCurrentTime >>= \now -> + let upd _ v = Just v { solverCacheValueLastUsed = now } in + tryTransaction cache (LMDB.updateLookupWithKey upd k) >>= \case + (Right (Just v), cache') -> do + printOutLn opts Debug ("Using cached result: " ++ show k) + modifyIORef solverCacheStats $ M.adjust (+1) Lookups + return (Just v, cache') + (Left err, cache') -> do + printOutLn opts Warn ("Solver cache lookup failed:\n" ++ err) + modifyIORef solverCacheStats $ M.adjust (+1) FailedLookups + return (Nothing, cache') + (Right Nothing, cache') -> do + return (Nothing, cache') + +-- | Add a 'SolverCacheValue' to the solver result cache +insertInSolverCache :: SolverCacheKey -> SolverCacheValue -> SolverCacheOp () +insertInSolverCache k v = SCOpOrDefault () $ \opts cache@SolverCache{..} -> + printOutLn opts Debug ("Caching result: " ++ show k) >> + tryTransaction cache (LMDB.insert k v) >>= \case + (Right (), cache') -> do + modifyIORef solverCacheStats $ M.adjust (+1) Inserts + return ((), cache') + (Left err, cache') -> do + printOutLn opts Warn ("Solver cache insert failed:\n" ++ err) + modifyIORef solverCacheStats $ M.adjust (+1) FailedInserts + return ((), cache') + +-- | Set the 'FilePath' of the solver result cache and save all results cached +-- so far +setSolverCachePath :: FilePath -> SolverCacheOp () +setSolverCachePath path = SCOpOrFail $ \opts cache@SolverCache{..} -> + if path == solverCachePath + then do + (_, _, cache') <- forceSolverCacheOpened cache + return ((), cache') + else do + (new_env, new_db, cache') <- + forceSolverCacheOpened cache { solverCachePath = path + , solverCacheEnv = Nothing + , solverCacheDB = Nothing } + case (solverCacheEnv, solverCacheDB) of + (Just old_env, Just old_db) -> do + kvs <- LMDB.readOnlyTransaction old_env $ LMDB.toList old_db + forM_ kvs $ \(k,v) -> LMDB.transaction new_env $ LMDB.insert k v new_db + printOutLn opts Info ("Saved " ++ show (length kvs) ++ " cached result" ++ + (if length kvs == 1 then "" else "s") ++ " to disk") + return ((), cache') + _ -> return ((), cache') + +-- | Print all entries in the solver result cache whose SHA256 hash keys start +-- with the given string +printSolverCacheByHex :: String -> SolverCacheOp () +printSolverCacheByHex hex_pref = SCOpOrFail $ \opts cache -> do + (env, db, cache') <- forceSolverCacheOpened cache + let flt k v kvs = if hex_pref `isPrefixOf` encodeHex (solverCacheKeyHash k) + then (k,v):kvs else kvs + kvs <- case decodeHex hex_pref of + Right (solverCacheKeyFromHash -> k) -> do + LMDB.readOnlyTransaction env (LMDB.lookup k db) >>= \case + Just v -> return [(k,v)] + Nothing -> LMDB.readOnlyTransaction env $ LMDB.foldrWithKey flt [] db + Left _ -> LMDB.readOnlyTransaction env $ LMDB.foldrWithKey flt [] db + when (length kvs == 0) $ printOutLn opts Info "No keys found" + forM_ kvs $ \(k, SolverCacheValue vs bk_opts nm mb_cexs t) -> do + let vs_str = showBackendVersionsWithOptions ", " vs bk_opts + res_str = maybe "unsat" (("sat " ++) . show) mb_cexs + printOutLn opts Info $ "SHA: " ++ encodeHex (solverCacheKeyHash k) + printOutLn opts Info $ "- Result: " ++ res_str + printOutLn opts Info $ "- Solver: " ++ show nm + printOutLn opts Info $ "- Versions: " ++ vs_str + printOutLn opts Info $ "- Last used: " ++ show t ++ "\n" + return ((), cache') + +-- | Remove all entries in the solver result cache which have version(s) that +-- do not match the current version(s) or are marked as stale +cleanSolverCache :: SolverBackendVersions -> SolverCacheOp () +cleanSolverCache curr_base_vs = SCOpOrFail $ \opts cache -> do + let known_curr_base_vs = M.filter isJust curr_base_vs + mismatched_vs vs = M.mapMaybe id $ M.intersectionWith + (\base_ver v_ver -> if base_ver /= v_ver + then Just (base_ver, v_ver) else Nothing) + known_curr_base_vs vs + flt k v (ks, mvs) = let mvs' = mismatched_vs (solverCacheValueVersions v) + in if M.null mvs' then (ks, mvs) + else (k:ks, M.union mvs mvs') + (env, db, cache') <- forceSolverCacheOpened cache + (ks, mvs) <- LMDB.readOnlyTransaction env $ LMDB.foldrWithKey flt ([], M.empty) db + forM_ ks $ \k -> LMDB.transaction env $ LMDB.delete k db + let s0 = if length ks == 1 then "" else "s" + s1 = if M.size mvs == 0 then "" else ":" + printOutLn opts Info $ + "Removed " ++ show (length ks) ++ + " cached result" ++ s0 ++ " with mismatched version" ++ s0 ++ s1 + forM_ (M.toList mvs) $ \(backend, (v1, v2)) -> + printOutLn opts Info $ + "- " ++ showSolverBackendVersion backend v1 [] ++ + " (Current: " ++ showSolverBackendVersion backend v2 [] ++ ")" + return ((), cache') + +-- | Print out statistics about how the solver cache was used +printSolverCacheStats :: SolverCacheOp () +printSolverCacheStats = SCOpOrFail $ \opts cache@SolverCache{..} -> do + (env, db, cache') <- forceSolverCacheOpened cache + printOutLn opts Info ("== Solver result cache statistics ==") + sz <- LMDB.readOnlyTransaction env $ LMDB.size db + printOutLn opts Info ("- " ++ show sz ++ " result" ++ pl sz + ++ " cached in " ++ solverCachePath) + stats <- readIORef solverCacheStats + let (ls, ls_f) = (stats M.! Lookups, stats M.! FailedLookups) + (is, is_f) = (stats M.! Inserts, stats M.! FailedInserts) + printOutLn opts Info $ "- " ++ show is ++ " insertion" ++ pl is + ++ " into the cache so far this run (" + ++ show is_f ++ " failed attempt" ++ pl is_f ++ ")" + printOutLn opts Info $ "- " ++ show ls ++ " usage" ++ pl ls + ++ " of cached results so far this run (" + ++ show ls_f ++ " failed attempt" ++ pl ls_f ++ ")" + return ((), cache') + where pl i = if i == 1 then "" else "s" + +-- | Check whether the values of the statistics printed out by +-- 'printSolverCacheStats' are equal to those given, failing if this does not +-- hold +testSolverCacheStats :: Integer -> Integer -> Integer -> Integer -> Integer -> + SolverCacheOp () +testSolverCacheStats sz ls ls_f is is_f = SCOpOrFail $ \opts cache@SolverCache{..} -> do + (env, db, cache') <- forceSolverCacheOpened cache + sz_actual <- fromIntegral <$> LMDB.readOnlyTransaction env (LMDB.size db) + test sz sz_actual "Size of solver cache" + stats <- readIORef solverCacheStats + 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 ++ " " ++ + show ls ++ " " ++ show ls_f ++ " " ++ show is ++ " " ++ show is_f ++ ")" + return ((), cache') + where test v v_actual str = when (v /= v_actual) $ fail $ + str ++ " (" ++ show v_actual ++ ")" + ++ " did not match expected (" ++ show v ++ ")" diff --git a/src/SAWScript/SolverVersions.hs b/src/SAWScript/SolverVersions.hs new file mode 100644 index 0000000000..e2d577a373 --- /dev/null +++ b/src/SAWScript/SolverVersions.hs @@ -0,0 +1,73 @@ +{- | +Module : SAWScript.SolverVersions +Description : Determining SMT solver backend versions +License : BSD3 +Maintainer : m-yac +Stability : provisional +-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} + +module SAWScript.SolverVersions where + +import Control.Exception (SomeException, try) +import System.Process (readProcessWithExitCode) +import System.Exit (ExitCode(..)) + +import qualified Data.Map as Map + +import qualified Data.SBV.Dynamic as SBV + +import SAWScript.SolverCache +import GitRev + +-- | Given an 'SBV.Solver' from @SBV@, attempt to query the solver for its +-- version and return the result as a string. +-- Adapted from @what4/test/ProbeSolvers.hs@ +getSolverVersion :: SBV.Solver -> IO (Maybe String) +getSolverVersion s = + let s' = SBV.solver $ SBV.defaultSolverConfig s + (args, pref) = case SBV.name s' of + -- n.b. abc will return a non-zero exit code if asked for command usage. + SBV.ABC -> (["s", "-q", "version;quit"], "UC Berkeley, ABC ") + SBV.Boolector -> (["--version"] , "") + SBV.Bitwuzla -> (["--version"] , "") + SBV.CVC4 -> (["--version"] , "This is CVC4 version ") + SBV.CVC5 -> (["--version"] , "This is cvc5 version ") + SBV.DReal -> (["--version"] , "dReal v") + SBV.MathSAT -> (["-version"] , "MathSAT5 version ") + SBV.Yices -> (["--version"] , "Yices ") + SBV.Z3 -> (["--version"] , "Z3 version ") + in try (readProcessWithExitCode (SBV.executable s') args "") >>= \case + Right (ExitSuccess,o,_) | (l:_) <- lines o -> + return $ Just $ dropPrefix pref l + Right _ -> return Nothing + Left (_ :: SomeException) -> return Nothing + where dropPrefix (x:xs) (y:ys) | x == y = dropPrefix xs ys + dropPrefix _ ys = ys + +-- | Get the 'SolverBackendVersion' of a 'SolverBackend' +getSolverBackendVersion :: SolverBackend -> IO (Maybe String) +getSolverBackendVersion backend = case backend of + What4 -> return what4Hash + SBV -> return (Just VERSION_sbv) + AIG -> return aigHash + RME -> return (Just hash) + -- We use individual cases for the remaining constructors to ensure that if + -- a new backend is added, a warning is generated for this pattern match + ABC -> getSolverVersion SBV.ABC + Boolector -> getSolverVersion SBV.Boolector + Bitwuzla -> getSolverVersion SBV.Bitwuzla + CVC4 -> getSolverVersion SBV.CVC4 + CVC5 -> getSolverVersion SBV.CVC5 + DReal -> getSolverVersion SBV.DReal + MathSAT -> getSolverVersion SBV.MathSAT + Yices -> getSolverVersion SBV.Yices + Z3 -> getSolverVersion SBV.Z3 + +-- | Get the set of 'SolverBackendVersions' of a list of 'SolverBackend's +getSolverBackendVersions :: [SolverBackend] -> IO SolverBackendVersions +getSolverBackendVersions backends = Map.fromList <$> + mapM (\backend -> (backend,) <$> getSolverBackendVersion backend) backends diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 0294d00b02..ee00c5e46a 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -49,6 +49,7 @@ import Control.Monad.Trans.Class (MonadTrans(lift)) import Data.IORef import Data.Foldable(foldrM) import Data.List ( intersperse ) +import Data.List.Extra ( dropEnd ) import qualified Data.Map as M import Data.Map ( Map ) import Data.Set ( Set ) @@ -78,6 +79,7 @@ import SAWScript.Options (Options(printOutFn),printOutLn,Verbosity(..)) import SAWScript.Proof import SAWScript.Prover.SolverStats import SAWScript.Prover.MRSolver.Term as MRSolver +import SAWScript.SolverCache import SAWScript.Crucible.LLVM.Skeleton import SAWScript.X86 (X86Unsupported(..), X86Error(..)) import SAWScript.Yosys.IR @@ -276,7 +278,6 @@ showsProofResult opts r = showMulti _ [] = showString "]" showMulti s (eqn : eqns) = showString s . showEqn eqn . showMulti ", " eqns - showsSatResult :: PPOpts -> SatResult -> ShowS showsSatResult opts r = case r of @@ -520,6 +521,7 @@ data TopLevelRW = , rwProofs :: [Value] {- ^ Values, generated anywhere, that represent proofs. -} , rwPPOpts :: PPOpts , rwSharedContext :: SharedContext + , rwSolverCache :: Maybe SolverCache , rwTheoremDB :: TheoremDB -- , rwCrucibleLLVMCtx :: Crucible.LLVMContext @@ -602,7 +604,7 @@ io f = (TopLevel_ (liftIO f)) handleIO e | IOError.isUserError e = do pos <- getPosition - rethrow (SS.TopLevelException pos (init . drop 12 $ show e)) + rethrow (SS.TopLevelException pos (dropEnd 1 . drop 12 $ show e)) | otherwise = rethrow e handleX86Unsupported (X86Unsupported s) = @@ -742,6 +744,21 @@ recordProof v = do rw <- getTopLevelRW putTopLevelRW rw { rwProofs = toValue v : rwProofs rw } +-- | Perform an operation on the 'SolverCache', returning a default value or +-- failing (depending on the first element of the 'SolverCacheOp') if there +-- is no enabled 'SolverCache' +onSolverCache :: SolverCacheOp a -> TopLevel a +onSolverCache cacheOp = + do opts <- getOptions + rw <- getTopLevelRW + case rwSolverCache rw of + Just cache -> do (a, cache') <- io $ solverCacheOp cacheOp opts cache + putTopLevelRW rw { rwSolverCache = Just cache' } + return a + Nothing -> case solverCacheOpDefault cacheOp of + Just a -> return a + Nothing -> fail "Solver result cache not enabled!" + -- | Access the current state of Java Class translation getJVMTrans :: TopLevel CJ.JVMContext getJVMTrans = gets rwJVMTrans