diff --git a/saw-remote-api/CHANGELOG.md b/saw-remote-api/CHANGELOG.md index 519e62d56e..afd6b58e91 100644 --- a/saw-remote-api/CHANGELOG.md +++ b/saw-remote-api/CHANGELOG.md @@ -1,6 +1,5 @@ # Revision history for saw-remote-api - ## 0.9.1 -- YYYY-MM-DD * `SAW/set option`'s `"option"` parameter is now allowed to be `"What4 eval"`, @@ -16,7 +15,8 @@ verification, so JVM specifications must leave these lists empty. Attempting to provide a non-empty list for either of these fields in a JVM specification will result in an error. - +* Introduced new methods `SAW/eval int` and `SAW/eval bool` that allow the + evaluation of Cryptol expressions into Python values. ## 0.9.0 -- 2021-11-19 diff --git a/saw-remote-api/docs/SAW.rst b/saw-remote-api/docs/SAW.rst index 34acd08a71..8570eb6340 100644 --- a/saw-remote-api/docs/SAW.rst +++ b/saw-remote-api/docs/SAW.rst @@ -505,6 +505,54 @@ Return fields +SAW/eval int (command) +~~~~~~~~~~~~~~~~~~~~~~ + +Attempt to evaluate the given term to a concrete integer. + +Parameter fields +++++++++++++++++ + + +``expr`` + The Cryptol expression to evaluate. + + + +Return fields ++++++++++++++ + + +``value`` + The integer value of the expresssion. + + + + +SAW/eval bool (command) +~~~~~~~~~~~~~~~~~~~~~~~ + +Attempt to evaluate the given term to a concrete boolean. + +Parameter fields +++++++++++++++++ + + +``expr`` + The Cryptol expression to evaluate. + + + +Return fields ++++++++++++++ + + +``value`` + The boolean value of the expresssion. + + + + SAW/set option (command) ~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md index 7c4cb19f3f..4246522d1f 100644 --- a/saw-remote-api/python/CHANGELOG.md +++ b/saw-remote-api/python/CHANGELOG.md @@ -13,6 +13,8 @@ `set_option(LaxLoadsAndStores(), True)` in order for `points_to_bitfield` to work as expected. `points_to_bitfield` is only supported for LLVM (and not JVM) verification. +* Added two new commands, `eval_int` and `eval_bool`, that evaluate Cryptol + expressions to Python integers or booleans. ## 0.9.0 -- 2021-11-19 diff --git a/saw-remote-api/python/poetry.lock b/saw-remote-api/python/poetry.lock index c10a5a223e..8cf80c74fb 100644 --- a/saw-remote-api/python/poetry.lock +++ b/saw-remote-api/python/poetry.lock @@ -28,7 +28,7 @@ python-versions = "*" [[package]] name = "charset-normalizer" -version = "2.0.9" +version = "2.0.12" description = "The Real First Universal Charset Detector. Open, modern and actively maintained alternative to Chardet." category = "main" optional = false @@ -39,7 +39,7 @@ unicode_backport = ["unicodedata2"] [[package]] name = "cryptol" -version = "2.12.2" +version = "2.12.4" description = "Cryptol client for the Cryptol 2.12 RPC server" category = "main" optional = false @@ -49,6 +49,7 @@ python-versions = ">=3.7.0,<4" argo-client = "0.0.10" BitVector = ">=3.4.9,<4.0.0" requests = ">=2.25.1,<3.0.0" +typing-extensions = ">=4.1.1,<5.0.0" [[package]] name = "idna" @@ -84,7 +85,7 @@ python-versions = "*" [[package]] name = "requests" -version = "2.26.0" +version = "2.27.1" description = "Python HTTP for Humans." category = "main" optional = false @@ -110,29 +111,29 @@ python-versions = "*" [[package]] name = "typing-extensions" -version = "4.0.1" -description = "Backported and Experimental Type Hints for Python 3.6+" -category = "dev" +version = "4.2.0" +description = "Backported and Experimental Type Hints for Python 3.7+" +category = "main" optional = false -python-versions = ">=3.6" +python-versions = ">=3.7" [[package]] name = "urllib3" -version = "1.26.7" +version = "1.26.9" description = "HTTP library with thread-safe connection pooling, file post, and more." category = "main" optional = false python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*, <4" [package.extras] -brotli = ["brotlipy (>=0.6.0)"] +brotli = ["brotlicffi (>=0.8.0)", "brotli (>=1.0.9)", "brotlipy (>=0.6.0)"] secure = ["pyOpenSSL (>=0.14)", "cryptography (>=1.3.4)", "idna (>=2.0.0)", "certifi", "ipaddress"] socks = ["PySocks (>=1.5.6,!=1.5.7,<2.0)"] [metadata] lock-version = "1.1" python-versions = "^3.8" -content-hash = "ffca6578b36152988e9e38f2f828a6807ae038cf3ff2722610a03af90f4b7586" +content-hash = "49c7188786f994fbfb2eb67d447ba052aee0e090da5952eda39db840283e7e15" [metadata.files] argo-client = [ @@ -147,12 +148,12 @@ certifi = [ {file = "certifi-2021.10.8.tar.gz", hash = "sha256:78884e7c1d4b00ce3cea67b44566851c4343c120abd683433ce934a68ea58872"}, ] charset-normalizer = [ - {file = "charset-normalizer-2.0.9.tar.gz", hash = "sha256:b0b883e8e874edfdece9c28f314e3dd5badf067342e42fb162203335ae61aa2c"}, - {file = "charset_normalizer-2.0.9-py3-none-any.whl", hash = "sha256:1eecaa09422db5be9e29d7fc65664e6c33bd06f9ced7838578ba40d58bdf3721"}, + {file = "charset-normalizer-2.0.12.tar.gz", hash = "sha256:2857e29ff0d34db842cd7ca3230549d1a697f96ee6d3fb071cfa6c7393832597"}, + {file = "charset_normalizer-2.0.12-py3-none-any.whl", hash = "sha256:6881edbebdb17b39b4eaaa821b438bf6eddffb4468cf344f09f89def34a8b1df"}, ] cryptol = [ - {file = "cryptol-2.12.2-py3-none-any.whl", hash = "sha256:d543f2a92b0000f869576c89eeee2fa19ddeb064193a13ce8e55f1e6a388a60b"}, - {file = "cryptol-2.12.2.tar.gz", hash = "sha256:ca2d84557354387b8f856902e18333fb1b6792cbf0e10173e1b64854af085ec7"}, + {file = "cryptol-2.12.4-py3-none-any.whl", hash = "sha256:7b87d3128c683f234618509600a0fc4c0fd2899a493cdd0ca389198128e785a7"}, + {file = "cryptol-2.12.4.tar.gz", hash = "sha256:588ada535994b52ac4b237edc230c7bb05822f6a0544f1dcf5aff60c800ebf1b"}, ] idna = [ {file = "idna-3.3-py3-none-any.whl", hash = "sha256:84d9dd047ffa80596e0f246e2eab0b391788b0503584e8945f2368256d2735ff"}, @@ -187,8 +188,8 @@ mypy-extensions = [ {file = "mypy_extensions-0.4.3.tar.gz", hash = "sha256:2d82818f5bb3e369420cb3c4060a7970edba416647068eb4c5343488a6c604a8"}, ] requests = [ - {file = "requests-2.26.0-py2.py3-none-any.whl", hash = "sha256:6c1246513ecd5ecd4528a0906f910e8f0f9c6b8ec72030dc9fd154dc1a6efd24"}, - {file = "requests-2.26.0.tar.gz", hash = "sha256:b8aa58f8cf793ffd8782d3d8cb19e66ef36f7aba4353eec859e74678b01b07a7"}, + {file = "requests-2.27.1-py2.py3-none-any.whl", hash = "sha256:f22fa1e554c9ddfd16e6e41ac79759e17be9e492b3587efa038054674760e72d"}, + {file = "requests-2.27.1.tar.gz", hash = "sha256:68d7c56fd5a8999887728ef304a6d12edc7be74f1cfa47714fc8b414525c9a61"}, ] typed-ast = [ {file = "typed_ast-1.4.3-cp35-cp35m-manylinux1_i686.whl", hash = "sha256:2068531575a125b87a41802130fa7e29f26c09a2833fea68d9a40cf33902eba6"}, @@ -223,10 +224,10 @@ typed-ast = [ {file = "typed_ast-1.4.3.tar.gz", hash = "sha256:fb1bbeac803adea29cedd70781399c99138358c26d05fcbd23c13016b7f5ec65"}, ] typing-extensions = [ - {file = "typing_extensions-4.0.1-py3-none-any.whl", hash = "sha256:7f001e5ac290a0c0401508864c7ec868be4e701886d5b573a9528ed3973d9d3b"}, - {file = "typing_extensions-4.0.1.tar.gz", hash = "sha256:4ca091dea149f945ec56afb48dae714f21e8692ef22a395223bcd328961b6a0e"}, + {file = "typing_extensions-4.2.0-py3-none-any.whl", hash = "sha256:6657594ee297170d19f67d55c05852a874e7eb634f4f753dbd667855e07c1708"}, + {file = "typing_extensions-4.2.0.tar.gz", hash = "sha256:f1c24655a0da0d1b67f07e17a5e6b2a105894e6824b92096378bb3668ef02376"}, ] urllib3 = [ - {file = "urllib3-1.26.7-py2.py3-none-any.whl", hash = "sha256:c4fdf4019605b6e5423637e01bc9fe4daef873709a7973e195ceba0a62bbc844"}, - {file = "urllib3-1.26.7.tar.gz", hash = "sha256:4987c65554f7a2dbf30c18fd48778ef124af6fab771a377103da0585e2336ece"}, + {file = "urllib3-1.26.9-py2.py3-none-any.whl", hash = "sha256:44ece4d53fb1706f667c9bd1c648f5469a2ec925fcf3a776667042d645472c14"}, + {file = "urllib3-1.26.9.tar.gz", hash = "sha256:aabaf16477806a5e1dd19aa41f8c2b7950dd3c746362d7e3223dbe6de6ac448e"}, ] diff --git a/saw-remote-api/python/saw_client/__init__.py b/saw-remote-api/python/saw_client/__init__.py index 4a2a412368..af4b54b61a 100644 --- a/saw-remote-api/python/saw_client/__init__.py +++ b/saw-remote-api/python/saw_client/__init__.py @@ -648,6 +648,26 @@ def prove(goal: cryptoltypes.CryptolJSON, pr.counterexample = None return pr +def eval_int(expr: cryptoltypes.CryptolJSON) -> int: + """Atempts to evaluate the given expression as a concrete integer. + """ + conn = __get_designated_connection() + res = conn.eval_int(expr).result() + v = res['value'] + if not isinstance(v, int): + raise ValueError(str(v) + " is not an integer") + return v + +def eval_bool(expr: cryptoltypes.CryptolJSON) -> bool: + """Atempts to evaluate the given expression as a concrete boolean. + """ + conn = __get_designated_connection() + res = conn.eval_bool(expr).result() + v = res['value'] + if not isinstance(v, bool): + raise ValueError(str(v) + " is not a boolean") + return v + def set_option(option : option.SAWOption, value : bool) -> None: """Set a boolean-valued SAW option.""" global __designated_connection diff --git a/saw-remote-api/python/saw_client/commands.py b/saw-remote-api/python/saw_client/commands.py index d6d0263cac..a763c4fa82 100644 --- a/saw-remote-api/python/saw_client/commands.py +++ b/saw-remote-api/python/saw_client/commands.py @@ -184,6 +184,30 @@ def __init__( def process_result(self, res : Any) -> Any: return res +class EvalInt(SAWCommand): + def __init__( + self, + connection : argo.HasProtocolState, + expr : cryptoltypes.CryptolJSON, + timeout : Optional[float]) -> None: + params = {'expr': cryptoltypes.to_cryptol(expr)} + super(EvalInt, self).__init__('SAW/eval int', params, connection, timeout=timeout) + + def process_result(self, res : Any) -> Any: + return res + +class EvalBool(SAWCommand): + def __init__( + self, + connection : argo.HasProtocolState, + expr : cryptoltypes.CryptolJSON, + timeout : Optional[float]) -> None: + params = {'expr': cryptoltypes.to_cryptol(expr)} + super(EvalBool, self).__init__('SAW/eval bool', params, connection, timeout=timeout) + + def process_result(self, res : Any) -> Any: + return res + class SAWReset(argo.Notification): def __init__(self, connection : argo.HasProtocolState) -> None: super(SAWReset, self).__init__( diff --git a/saw-remote-api/python/saw_client/connection.py b/saw-remote-api/python/saw_client/connection.py index 0004f09db4..0a45321815 100644 --- a/saw-remote-api/python/saw_client/connection.py +++ b/saw-remote-api/python/saw_client/connection.py @@ -239,6 +239,24 @@ def prove(self, self.most_recent_result = Prove(self, goal, proof_script, timeout) return self.most_recent_result + def eval_int(self, + expr: cryptoltypes.CryptolJSON, + timeout : Optional[float] = None) -> Command: + """Create an instance of the `EvalInt` command. Documentation on the purpose and + use of this command is associated with the top-level `eval_int` function. + """ + self.most_recent_result = EvalInt(self, expr, timeout) + return self.most_recent_result + + def eval_bool(self, + expr: cryptoltypes.CryptolJSON, + timeout : Optional[float] = None) -> Command: + """Create an instance of the `EvalBool` command. Documentation on the purpose and + use of this command is associated with the top-level `eval_bool` function. + """ + self.most_recent_result = EvalBool(self, expr, timeout) + return self.most_recent_result + def set_option(self, option : SAWOption, value : bool, diff --git a/saw-remote-api/python/tests/saw/test_eval.py b/saw-remote-api/python/tests/saw/test_eval.py new file mode 100644 index 0000000000..d756e7f60f --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_eval.py @@ -0,0 +1,22 @@ +import cryptol +import saw_client as saw + +import unittest +from pathlib import Path + +class ProverTest(unittest.TestCase): + + def test_provers(self): + saw.connect(reset_server=True) + + if __name__ == "__main__": saw.view(saw.LogResults()) + + expr1 = cryptol.cry_f('(6 : [8]) * 7') + self.assertEqual(saw.eval_int(expr1), 42) + + expr2 = cryptol.cry_f('(1 < 2) : Bit') + self.assertTrue(saw.eval_bool(expr2)) + + +if __name__ == "__main__": + unittest.main() diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal index 539fbe4ec6..efdefc63a6 100644 --- a/saw-remote-api/saw-remote-api.cabal +++ b/saw-remote-api/saw-remote-api.cabal @@ -74,6 +74,7 @@ library SAWServer.Data.JVMType, SAWServer.Data.LLVMType, SAWServer.Data.SetupValue, + SAWServer.Eval, SAWServer.Exceptions, SAWServer.Ghost, SAWServer.JVMCrucibleSetup, diff --git a/saw-remote-api/saw-remote-api/Main.hs b/saw-remote-api/saw-remote-api/Main.hs index 0b926e07d4..4fedadf5da 100644 --- a/saw-remote-api/saw-remote-api/Main.hs +++ b/saw-remote-api/saw-remote-api/Main.hs @@ -17,6 +17,11 @@ import SAWServer.CryptolSetup cryptolLoadFileDescr, cryptolLoadFile ) import SAWServer.Data.JVMType() +import SAWServer.Eval + ( evalIntDescr, + evalInt, + evalBoolDescr, + evalBool ) import SAWServer.Ghost ( createGhostVariableDescr, createGhostVariable ) @@ -117,6 +122,14 @@ sawMethods = "SAW/prove" proveDescr prove + , Argo.command + "SAW/eval int" + evalIntDescr + evalInt + , Argo.command + "SAW/eval bool" + evalBoolDescr + evalBool , Argo.command "SAW/set option" setOptionDescr diff --git a/saw-remote-api/src/SAWServer/Eval.hs b/saw-remote-api/src/SAWServer/Eval.hs new file mode 100644 index 0000000000..7e783f32f2 --- /dev/null +++ b/saw-remote-api/src/SAWServer/Eval.hs @@ -0,0 +1,104 @@ +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +module SAWServer.Eval + ( evalInt + , evalIntDescr + , evalBool + , evalBoolDescr + ) where + +import Control.Exception ( throw ) +import Control.Lens ( view ) +import Control.Monad.IO.Class ( MonadIO(liftIO) ) +import Data.Aeson + ( (.:), + withObject, + object, + FromJSON(parseJSON), + KeyValue((.=)), + ToJSON(toJSON) ) + +import qualified Argo +import qualified Argo.Doc as Doc +import CryptolServer.Data.Expression ( Expression(..), getCryptolExpr ) +import Verifier.SAW.TypedTerm (TypedTerm) +import qualified SAWScript.Builtins as SB +import qualified SAWScript.Value as SV +import SAWServer + ( SAWState, + sawBIC, + sawTopLevelRW) +import SAWServer.CryptolExpression ( CryptolModuleException(..), getTypedTermOfCExp ) +import SAWServer.TopLevel ( tl ) + +-- The phantom type here is used to prevent a functional dependency conflict when +-- writing instances of Doc.DescribedMethod, and should match the type parameter +-- of EvalResult +newtype EvalParams evalty cryptolExpr = + EvalParams + { evalExpr :: cryptolExpr + } + +instance (FromJSON cryptolExpr) => FromJSON (EvalParams a cryptolExpr) where + parseJSON = + withObject "SAW/eval params" $ \o -> + EvalParams <$> o .: "expr" + +newtype EvalResult evalty = + EvalResult + { evalValue :: evalty + } + +instance ToJSON a => ToJSON (EvalResult a) where + toJSON r = object [ "value" .= evalValue r ] + +instance Doc.DescribedMethod (EvalParams Integer cryptolExpr) (EvalResult Integer) where + parameterFieldDescription = + [ ("expr", + Doc.Paragraph [Doc.Text "The Cryptol expression to evaluate."]) + ] + resultFieldDescription = + [ ("value", + Doc.Paragraph [Doc.Text "The integer value of the expresssion."]) + ] + +instance Doc.DescribedMethod (EvalParams Bool cryptolExpr) (EvalResult Bool) where + parameterFieldDescription = + [ ("expr", + Doc.Paragraph [Doc.Text "The Cryptol expression to evaluate."]) + ] + resultFieldDescription = + [ ("value", + Doc.Paragraph [Doc.Text "The boolean value of the expresssion."]) + ] + +eval :: (TypedTerm -> SV.TopLevel a) -> EvalParams a Expression -> Argo.Command SAWState (EvalResult a) +eval f params = do + state <- Argo.getState + fileReader <- Argo.getFileReader + let cenv = SV.rwCryptol (view sawTopLevelRW state) + bic = view sawBIC state + cexp <- getCryptolExpr $ evalExpr params + (eterm, warnings) <- liftIO $ getTypedTermOfCExp fileReader (SV.biSharedContext bic) cenv cexp + t <- case eterm of + Right (t, _) -> return t -- TODO: report warnings + Left err -> throw $ CryptolModuleException err warnings + i <- tl $ f t + pure $ EvalResult i + +evalIntDescr :: Doc.Block +evalIntDescr = + Doc.Paragraph [ Doc.Text "Attempt to evaluate the given term to a concrete integer." ] + +evalInt :: EvalParams Integer Expression -> Argo.Command SAWState (EvalResult Integer) +evalInt = eval SB.eval_int + +evalBoolDescr :: Doc.Block +evalBoolDescr = + Doc.Paragraph [ Doc.Text "Attempt to evaluate the given term to a concrete boolean." ] + +evalBool :: EvalParams Bool Expression -> Argo.Command SAWState (EvalResult Bool) +evalBool = eval SB.eval_bool