diff --git a/.github/ci.sh b/.github/ci.sh index 2ba26e7b7d..e9a549147c 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -75,7 +75,7 @@ install_system_deps() { cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT export PATH="$BIN:$PATH" echo "$BIN" >> "$GITHUB_PATH" - is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" cvc5 && is_exe "$BIN" yices + is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" cvc5 && is_exe "$BIN" yices && is_exe "$BIN" bitwuzla && is_exe "$BIN" boolector } build_cryptol() { @@ -121,6 +121,8 @@ zip_dist_with_solvers() { # should be at least as portable (in terms of dynamic library # dependencies) as the SAW binaries. cp "$BIN/abc" dist/bin/ + cp "$BIN/bitwuzla" dist/bin/ + cp "$BIN/boolector" dist/bin/ cp "$BIN/cvc4" dist/bin/ cp "$BIN/cvc5" dist/bin/ cp "$BIN/yices" dist/bin/ diff --git a/CHANGES.md b/CHANGES.md index 59de003989..759bb1851d 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -2,6 +2,8 @@ ## New Features +* Add a `bitwuzla` family of proof scripts that use the Bitwuzla SMT solver. + * Add a `:tenv` REPL command, which is like `:env` but prints the type environment instead of the variable environment. `:t` is still short for `:type`. diff --git a/deps/crucible b/deps/crucible index 2fb1c26a3c..95b39e3453 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 2fb1c26a3cd4562d90a51956925363a0b40f50ed +Subproject commit 95b39e34537987c00f3dd2da4e837e12151795ff diff --git a/deps/cryptol b/deps/cryptol index b1bdfd0e3f..f959fbe650 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit b1bdfd0e3ff0ff8d16e94fd6e6402a3d1fb497f2 +Subproject commit f959fbe650cb684bbb2fa6c45d56ed500b42051f diff --git a/doc/manual/manual.md b/doc/manual/manual.md index 3cdcf54888..d9a772fe14 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -1154,10 +1154,10 @@ sawscript> sat_print abc {{ \(x:[8]) -> x+x == x*2 }} Sat: [x = 0] ~~~~ -In addition to these, the `boolector`, `cvc4`, `cvc5`, `mathsat`, and `yices` -provers are available. The internal decision procedure `rme`, short for -Reed-Muller Expansion, is an automated prover that works particularly -well on the Galois field operations that show up, for example, in AES. +In addition to these, the `bitwuzla`, `boolector`, `cvc4`, `cvc5`, `mathsat`, +and `yices` provers are available. The internal decision procedure `rme`, short +for Reed-Muller Expansion, is an automated prover that works particularly well +on the Galois field operations that show up, for example, in AES. In more complex cases, some pre-processing can be helpful or necessary before handing the problem off to an automated prover. The @@ -1220,6 +1220,8 @@ provers is to unfold everything before sending a goal to a prover. However, with some provers it is possible to indicate that specific named subterms should be represented as uninterpreted functions. +* `unint_bitwuzla : [String] -> ProofScript ()` + * `unint_cvc4 : [String] -> ProofScript ()` * `unint_cvc5 : [String] -> ProofScript ()` @@ -1241,6 +1243,8 @@ Note that each of the `unint_*` tactics have variants that are prefixed with `sbv_` and `w4_`. The `sbv_`-prefixed tactics make use of the SBV library to represent and solve SMT queries: +* `sbv_unint_bitwuzla : [String] -> ProofScript ()` + * `sbv_unint_cvc4 : [String] -> ProofScript ()` * `sbv_unint_cvc5 : [String] -> ProofScript ()` @@ -1251,6 +1255,8 @@ library to represent and solve SMT queries: The `w4_`-prefixed tactics make use of the What4 library instead of SBV: +* `w4_unint_bitwuzla : [String] -> ProofScript ()` + * `w4_unint_cvc4 : [String] -> ProofScript ()` * `w4_unint_cvc5 : [String] -> ProofScript ()` diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf index e651b1f40d..9e4c44b1f8 100644 Binary files a/doc/manual/manual.pdf and b/doc/manual/manual.pdf differ diff --git a/doc/tutorial/tutorial.md b/doc/tutorial/tutorial.md index 801b4806f6..80ab805ae9 100644 --- a/doc/tutorial/tutorial.md +++ b/doc/tutorial/tutorial.md @@ -295,8 +295,9 @@ this automatically, but for flexibility the `write_smtlib2` primitive passes the given term through unchanged, because it might be used for either satisfiability or validity checking. -The SMT-Lib export capabilities in SAWScript make use of the Haskell -SBV package, and support ABC, Boolector, CVC4, CVC5, MathSAT, Yices, and Z3. +The SMT-Lib export capabilities in SAWScript make use of the Haskell SBV +package, and support ABC, Bitwuzla, Boolector, CVC4, CVC5, MathSAT, Yices, and +Z3. \newpage diff --git a/intTests/test_bitwuzla/test.saw b/intTests/test_bitwuzla/test.saw new file mode 100644 index 0000000000..bdc747b13a --- /dev/null +++ b/intTests/test_bitwuzla/test.saw @@ -0,0 +1,10 @@ +let +{{ +add_mul_lemma : [64] -> [64] -> [64] -> Bit +add_mul_lemma m n p = + m * (n + p) == (m * n) + (m * p) +}}; + +prove bitwuzla {{ add_mul_lemma }}; +prove sbv_bitwuzla {{ add_mul_lemma }}; +prove (w4_unint_bitwuzla []) {{ add_mul_lemma }}; diff --git a/intTests/test_bitwuzla/test.sh b/intTests/test_bitwuzla/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_bitwuzla/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/saw-remote-api/python/saw_client/proofscript.py b/saw-remote-api/python/saw_client/proofscript.py index 853cee7d32..6f1834cfb3 100644 --- a/saw-remote-api/python/saw_client/proofscript.py +++ b/saw-remote-api/python/saw_client/proofscript.py @@ -21,6 +21,14 @@ class ABC_SBV(Prover): def to_json(self) -> Any: return { "name": "sbv-abc" } +class Bitwuzla(Prover): + def to_json(self) -> Any: + return { "name": "bitwuzla" } + +class Bitwuzla_SBV(Prover): + def to_json(self) -> Any: + return { "name": "sbv-bitwuzla" } + class Boolector(Prover): def to_json(self) -> Any: return { "name": "boolector" } @@ -126,6 +134,9 @@ def to_json(self) -> Any: rme = UseProver(RME()) boolector = UseProver(Boolector()) +def bitwuzla(unints : List[str]) -> ProofTactic + return UseProver(Bitwuzla(unints)) + def cvc4(unints : List[str]) -> ProofTactic: return UseProver(CVC4(unints)) diff --git a/saw-remote-api/python/saw_client/solver_cache.py b/saw-remote-api/python/saw_client/solver_cache.py index 520f19e08a..907bdb1405 100644 --- a/saw-remote-api/python/saw_client/solver_cache.py +++ b/saw-remote-api/python/saw_client/solver_cache.py @@ -17,7 +17,7 @@ # External solvers supported by SBV (adapted from SBV.Solver) Literal["ABC"], Literal["Boolector"], - Literal["Bitwuzla"], # NOTE: Not currently supported by SAW + Literal["Bitwuzla"], Literal["CVC4"], Literal["CVC5"], Literal["DReal"], # NOTE: Not currently supported by SAW @@ -52,7 +52,7 @@ def __post_init__(self): def load_solver_cache_entry(enc): obj = cbor2.loads(enc) - opts = obj['opts'] if 'opts' in obj else [] + 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) @@ -88,7 +88,7 @@ def __init__(self, path : Optional[str] = None): 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") @@ -96,7 +96,7 @@ def __getitem__(self, k : bytes): 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") @@ -104,19 +104,19 @@ def __setitem__(self, k : bytes, 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) diff --git a/saw-remote-api/src/SAWServer/ProofScript.hs b/saw-remote-api/src/SAWServer/ProofScript.hs index 78755d861c..494dd119f5 100644 --- a/saw-remote-api/src/SAWServer/ProofScript.hs +++ b/saw-remote-api/src/SAWServer/ProofScript.hs @@ -55,6 +55,7 @@ import Verifier.SAW.TermNet (merge) data Prover = RME | SBV_ABC_SMTLib + | SBV_Bitwuzla [String] | SBV_Boolector [String] | SBV_CVC4 [String] | SBV_CVC5 [String] @@ -63,6 +64,7 @@ data Prover | SBV_Z3 [String] | W4_ABC_SMTLib | W4_ABC_Verilog + | W4_Bitwuzla [String] | W4_Boolector [String] | W4_CVC4 [String] | W4_CVC5 [String] @@ -87,12 +89,14 @@ instance FromJSON Prover where let unints = fromMaybe [] <$> o .:? "uninterpreted functions" case name of "abc" -> pure W4_ABC_SMTLib + "bitwuzla" -> SBV_Bitwuzla <$> unints "boolector" -> SBV_Boolector <$> unints "cvc4" -> SBV_CVC4 <$> unints "cvc5" -> SBV_CVC5 <$> unints "mathsat" -> SBV_MathSAT <$> unints "rme" -> pure RME "sbv-abc" -> pure SBV_ABC_SMTLib + "sbv-bitwuzla" -> SBV_Bitwuzla <$> unints "sbv-boolector" -> SBV_Boolector <$> unints "sbv-cvc4" -> SBV_CVC4 <$> unints "sbv-cvc5" -> SBV_CVC5 <$> unints @@ -101,6 +105,7 @@ instance FromJSON Prover where "sbv-z3" -> SBV_Z3 <$> unints "w4-abc-smtlib" -> pure W4_ABC_SMTLib "w4-abc-verilog" -> pure W4_ABC_Verilog + "w4-bitwuzla" -> W4_Bitwuzla <$> unints "w4-boolector" -> W4_Boolector <$> unints "w4-cvc4" -> W4_CVC4 <$> unints "w4-cvc5" -> W4_CVC5 <$> unints @@ -277,6 +282,7 @@ interpretProofScript (ProofScript ts) = go ts case p of RME -> return $ SB.proveRME SBV_ABC_SMTLib -> return $ SB.proveABC_SBV + SBV_Bitwuzla unints -> return $ SB.proveUnintBitwuzla unints SBV_Boolector unints -> return $ SB.proveUnintBoolector unints SBV_CVC4 unints -> return $ SB.proveUnintCVC4 unints SBV_CVC5 unints -> return $ SB.proveUnintCVC5 unints @@ -285,6 +291,7 @@ interpretProofScript (ProofScript ts) = go ts SBV_Z3 unints -> return $ SB.proveUnintZ3 unints W4_ABC_SMTLib -> return $ SB.w4_abc_smtlib2 W4_ABC_Verilog -> return $ SB.w4_abc_verilog + W4_Bitwuzla unints -> return $ SB.w4_unint_bitwuzla unints W4_Boolector unints -> return $ SB.w4_unint_boolector unints W4_CVC4 unints -> return $ SB.w4_unint_cvc4 unints W4_CVC5 unints -> return $ SB.w4_unint_cvc5 unints diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 2da41fcf22..8ca8cf1795 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -1051,6 +1051,9 @@ wrapW4ProveExporter f unints path ext = do proveABC_SBV :: ProofScript () proveABC_SBV = proveSBV SBV.abc +proveBitwuzla :: ProofScript () +proveBitwuzla = proveSBV SBV.bitwuzla + proveBoolector :: ProofScript () proveBoolector = proveSBV SBV.boolector @@ -1069,6 +1072,9 @@ proveMathSAT = proveSBV SBV.mathSAT proveYices :: ProofScript () proveYices = proveSBV SBV.yices +proveUnintBitwuzla :: [String] -> ProofScript () +proveUnintBitwuzla = proveUnintSBV SBV.bitwuzla + proveUnintBoolector :: [String] -> ProofScript () proveUnintBoolector = proveUnintSBV SBV.boolector @@ -1092,6 +1098,9 @@ proveUnintYices = proveUnintSBV SBV.yices w4_abc_smtlib2 :: ProofScript () w4_abc_smtlib2 = wrapW4Prover ABC [W4_SMTLib2] Prover.proveWhat4_abc [] +w4_bitwuzla :: ProofScript () +w4_bitwuzla = wrapW4Prover Bitwuzla [] Prover.proveWhat4_bitwuzla [] + w4_boolector :: ProofScript () w4_boolector = wrapW4Prover Boolector [] Prover.proveWhat4_boolector [] @@ -1107,6 +1116,9 @@ w4_cvc5 = wrapW4Prover CVC5 [] Prover.proveWhat4_cvc5 [] w4_yices :: ProofScript () w4_yices = wrapW4Prover Yices [] Prover.proveWhat4_yices [] +w4_unint_bitwuzla :: [String] -> ProofScript () +w4_unint_bitwuzla = wrapW4Prover Bitwuzla [] Prover.proveWhat4_bitwuzla + w4_unint_boolector :: [String] -> ProofScript () w4_unint_boolector = wrapW4Prover Boolector [] Prover.proveWhat4_boolector @@ -1125,6 +1137,10 @@ w4_unint_cvc5 = wrapW4Prover CVC5 [] Prover.proveWhat4_cvc5 w4_unint_yices :: [String] -> ProofScript () w4_unint_yices = wrapW4Prover Yices [] Prover.proveWhat4_yices +offline_w4_unint_bitwuzla :: [String] -> String -> ProofScript () +offline_w4_unint_bitwuzla unints path = + wrapW4ProveExporter Prover.proveExportWhat4_bitwuzla unints path ".smt2" + offline_w4_unint_z3 :: [String] -> String -> ProofScript () offline_w4_unint_z3 unints path = wrapW4ProveExporter Prover.proveExportWhat4_z3 unints path ".smt2" diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 71669da99c..e7367009c4 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -2184,6 +2184,11 @@ primitives = Map.fromList Current [ "Use the ABC theorem prover to prove the current goal." ] + , prim "bitwuzla" "ProofScript ()" + (pureVal proveBitwuzla) + Current + [ "Use the Bitwuzla theorem prover to prove the current goal." ] + , prim "boolector" "ProofScript ()" (pureVal proveBoolector) Current @@ -2214,6 +2219,13 @@ primitives = Map.fromList Current [ "Use the Yices theorem prover to prove the current goal." ] + , prim "unint_bitwuzla" "[String] -> ProofScript ()" + (pureVal proveUnintBitwuzla) + Current + [ "Use the Bitwuzla theorem prover to prove the current goal. Leave the" + , "given list of names as uninterpreted." + ] + , prim "unint_z3" "[String] -> ProofScript ()" (pureVal proveUnintZ3) Current @@ -2242,6 +2254,11 @@ primitives = Map.fromList , "given list of names as uninterpreted." ] + , prim "sbv_bitwuzla" "ProofScript ()" + (pureVal proveBitwuzla) + Current + [ "Use the Bitwuzla theorem prover to prove the current goal." ] + , prim "sbv_boolector" "ProofScript ()" (pureVal proveBoolector) Current @@ -2272,6 +2289,13 @@ primitives = Map.fromList Current [ "Use the Yices theorem prover to prove the current goal." ] + , prim "sbv_unint_bitwuzla" "[String] -> ProofScript ()" + (pureVal proveUnintBitwuzla) + Current + [ "Use the Bitwuzla theorem prover to prove the current goal. Leave the" + , "given list of names as uninterpreted." + ] + , prim "sbv_unint_z3" "[String] -> ProofScript ()" (pureVal proveUnintZ3) Current @@ -2388,6 +2412,13 @@ primitives = Map.fromList Current [ "Prove the current goal using What4 (Z3 backend)." ] + , prim "w4_unint_bitwuzla" "[String] -> ProofScript ()" + (pureVal w4_unint_bitwuzla) + Current + [ "Prove the current goal using What4 (Bitwuzla backend). Leave the" + , "given list of names as uninterpreted." + ] + , prim "w4_unint_z3" "[String] -> ProofScript ()" (pureVal w4_unint_z3) Current @@ -2447,6 +2478,13 @@ primitives = Map.fromList , "using the What4 backend." ] + , prim "offline_w4_unint_bitwuzla" "[String] -> String -> ProofScript ()" + (pureVal offline_w4_unint_bitwuzla) + Current + [ "Write the current goal to the given file using What4 (Bitwuzla backend)" + , " in SMT-Lib2 format. Leave the given list of names as uninterpreted." + ] + , prim "offline_w4_unint_z3" "[String] -> String -> ProofScript ()" (pureVal offline_w4_unint_z3) Current diff --git a/src/SAWScript/Prover/SBV.hs b/src/SAWScript/Prover/SBV.hs index 45f214070d..ffea9b0c1c 100644 --- a/src/SAWScript/Prover/SBV.hs +++ b/src/SAWScript/Prover/SBV.hs @@ -2,7 +2,7 @@ module SAWScript.Prover.SBV ( proveUnintSBV , proveUnintSBVIO , SBV.SMTConfig - , SBV.z3, SBV.cvc4, SBV.cvc5, SBV.yices, SBV.mathSAT, SBV.boolector + , SBV.z3, SBV.cvc4, SBV.cvc5, SBV.yices, SBV.mathSAT, SBV.boolector, SBV.bitwuzla ) where import System.Directory diff --git a/src/SAWScript/Prover/What4.hs b/src/SAWScript/Prover/What4.hs index 69f289d6c8..e41c22bd0a 100644 --- a/src/SAWScript/Prover/What4.hs +++ b/src/SAWScript/Prover/What4.hs @@ -122,7 +122,8 @@ proveExportWhat4_sym solver hashConsing outFilePath satq = do -- Assume unsat return (Nothing, solver_name) -proveWhat4_z3, proveWhat4_boolector, +proveWhat4_z3, + proveWhat4_bitwuzla, proveWhat4_boolector, proveWhat4_cvc4, proveWhat4_cvc5, proveWhat4_dreal, proveWhat4_stp, proveWhat4_yices, proveWhat4_abc :: @@ -131,6 +132,7 @@ proveWhat4_z3, proveWhat4_boolector, TopLevel (Maybe CEX, String) proveWhat4_z3 = proveWhat4_sym z3Adapter +proveWhat4_bitwuzla = proveWhat4_sym bitwuzlaAdapter proveWhat4_boolector = proveWhat4_sym boolectorAdapter proveWhat4_cvc4 = proveWhat4_sym cvc4Adapter proveWhat4_cvc5 = proveWhat4_sym cvc5Adapter @@ -154,7 +156,8 @@ proveWhat4_z3_using tactic hashConsing satq = do _ <- setOpt z3TacticSetting $ Text.pack tactic return () -proveExportWhat4_z3, proveExportWhat4_boolector, +proveExportWhat4_z3, + proveExportWhat4_bitwuzla, proveExportWhat4_boolector, proveExportWhat4_cvc4, proveExportWhat4_cvc5, proveExportWhat4_dreal, proveExportWhat4_stp, proveExportWhat4_yices :: Bool {- ^ Hash-consing of ExportWhat4 terms -}-> @@ -163,6 +166,7 @@ proveExportWhat4_z3, proveExportWhat4_boolector, TopLevel (Maybe CEX, String) proveExportWhat4_z3 = proveExportWhat4_sym z3Adapter +proveExportWhat4_bitwuzla = proveExportWhat4_sym bitwuzlaAdapter proveExportWhat4_boolector = proveExportWhat4_sym boolectorAdapter proveExportWhat4_cvc4 = proveExportWhat4_sym cvc4Adapter proveExportWhat4_cvc5 = proveExportWhat4_sym cvc5Adapter diff --git a/src/SAWScript/SolverCache.hs b/src/SAWScript/SolverCache.hs index 402b8cd3f9..fa9387c168 100644 --- a/src/SAWScript/SolverCache.hs +++ b/src/SAWScript/SolverCache.hs @@ -162,7 +162,7 @@ data SolverBackend = What4 -- External solvers supported by SBV (copied from SBV.Solver) | ABC | Boolector - | Bitwuzla -- NOTE: Not currently supported by SAW + | Bitwuzla | CVC4 | CVC5 | DReal -- NOTE: Not currently supported by SAW diff --git a/src/SAWScript/SolverVersions.hs b/src/SAWScript/SolverVersions.hs index 039cc642d0..8228035075 100644 --- a/src/SAWScript/SolverVersions.hs +++ b/src/SAWScript/SolverVersions.hs @@ -59,8 +59,8 @@ getSolverBackendVersion backend = case backend of -- 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 + Boolector -> getSolverVersion SBV.Boolector CVC4 -> getSolverVersion SBV.CVC4 CVC5 -> getSolverVersion SBV.CVC5 DReal -> getSolverVersion SBV.DReal