From 84f5da3cbe2af5a4e9780d22801996b4a3aac155 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Fri, 6 May 2022 14:01:11 -0400 Subject: [PATCH 1/8] Add an `eval_int` command to the remote API and Python interface --- saw-remote-api/python/poetry.lock | 41 +++++----- saw-remote-api/python/saw_client/__init__.py | 7 ++ saw-remote-api/python/saw_client/commands.py | 12 +++ .../python/saw_client/connection.py | 9 +++ saw-remote-api/python/tests/saw/test_eval.py | 23 ++++++ saw-remote-api/saw-remote-api.cabal | 1 + saw-remote-api/saw-remote-api/Main.hs | 7 ++ saw-remote-api/src/SAWServer/Eval.hs | 77 +++++++++++++++++++ 8 files changed, 157 insertions(+), 20 deletions(-) create mode 100644 saw-remote-api/python/tests/saw/test_eval.py create mode 100644 saw-remote-api/src/SAWServer/Eval.hs 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..80c35876d3 100644 --- a/saw-remote-api/python/saw_client/__init__.py +++ b/saw-remote-api/python/saw_client/__init__.py @@ -648,6 +648,13 @@ 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() + return res['value'] + 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..44289372f1 100644 --- a/saw-remote-api/python/saw_client/commands.py +++ b/saw-remote-api/python/saw_client/commands.py @@ -184,6 +184,18 @@ 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 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..4f446ba477 100644 --- a/saw-remote-api/python/saw_client/connection.py +++ b/saw-remote-api/python/saw_client/connection.py @@ -239,6 +239,15 @@ 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 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..3e87188dd3 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_eval.py @@ -0,0 +1,23 @@ +from cryptol import cryptoltypes +import saw_client as saw + +import unittest +from pathlib import Path + + +def cry(exp): + return cryptoltypes.CryptolLiteral(exp) + +class ProverTest(unittest.TestCase): + + def test_provers(self): + saw.connect(reset_server=True) + + if __name__ == "__main__": saw.view(saw.LogResults()) + + expr = cry('(6 : [8]) * 7') + self.assertEqual(saw.eval_int(expr), 42) + + +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..45ea1d7df5 100644 --- a/saw-remote-api/saw-remote-api/Main.hs +++ b/saw-remote-api/saw-remote-api/Main.hs @@ -17,6 +17,9 @@ import SAWServer.CryptolSetup cryptolLoadFileDescr, cryptolLoadFile ) import SAWServer.Data.JVMType() +import SAWServer.Eval + ( evalIntDescr, + evalInt ) import SAWServer.Ghost ( createGhostVariableDescr, createGhostVariable ) @@ -117,6 +120,10 @@ sawMethods = "SAW/prove" proveDescr prove + , Argo.command + "SAW/eval int" + evalIntDescr + evalInt , 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..3d20e989e4 --- /dev/null +++ b/saw-remote-api/src/SAWServer/Eval.hs @@ -0,0 +1,77 @@ +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +module SAWServer.Eval + ( evalInt + , evalIntDescr + ) 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 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 ) + +data EvalIntParams cryptolExpr = + EvalIntParams + { evalIntExpr :: cryptolExpr + } + +instance (FromJSON cryptolExpr) => FromJSON (EvalIntParams cryptolExpr) where + parseJSON = + withObject "SAW/eval int params" $ \o -> + EvalIntParams <$> o .: "expr" + +data EvalIntResult = + EvalIntResult + { evalIntValue :: Integer + } + +instance ToJSON EvalIntResult where + toJSON r = object [ "value" .= evalIntValue r ] + +evalIntDescr :: Doc.Block +evalIntDescr = + Doc.Paragraph [ Doc.Text "Attempt to evaluate the given term to a concrete integer." ] + +instance Doc.DescribedMethod (EvalIntParams cryptolExpr) EvalIntResult where + parameterFieldDescription = + [ ("expr", + Doc.Paragraph [Doc.Text "The Cryptol expression to evaluate."]) + ] + resultFieldDescription = + [ ("value", + Doc.Paragraph [Doc.Text "The integer value of the expresssion."]) + ] + +evalInt :: EvalIntParams Expression -> Argo.Command SAWState EvalIntResult +evalInt params = do + state <- Argo.getState + fileReader <- Argo.getFileReader + let cenv = SV.rwCryptol (view sawTopLevelRW state) + bic = view sawBIC state + cexp <- getCryptolExpr $ evalIntExpr 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 $ SB.eval_int t + pure $ EvalIntResult i From 27bd3b76016c48337ee9c625503b8f13fe0a4cc0 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Fri, 6 May 2022 14:23:24 -0400 Subject: [PATCH 2/8] Add `eval_bool` --- saw-remote-api/python/saw_client/__init__.py | 7 +++ saw-remote-api/python/saw_client/commands.py | 12 +++++ .../python/saw_client/connection.py | 9 ++++ saw-remote-api/python/tests/saw/test_eval.py | 7 ++- saw-remote-api/saw-remote-api/Main.hs | 8 +++- saw-remote-api/src/SAWServer/Eval.hs | 48 +++++++++++++++++++ 6 files changed, 88 insertions(+), 3 deletions(-) diff --git a/saw-remote-api/python/saw_client/__init__.py b/saw-remote-api/python/saw_client/__init__.py index 80c35876d3..e48d4d457d 100644 --- a/saw-remote-api/python/saw_client/__init__.py +++ b/saw-remote-api/python/saw_client/__init__.py @@ -655,6 +655,13 @@ def eval_int(expr: cryptoltypes.CryptolJSON) -> int: res = conn.eval_int(expr).result() return res['value'] +def eval_bool(expr: cryptoltypes.CryptolJSON) -> int: + """Atempts to evaluate the given expression as a concrete boolean. + """ + conn = __get_designated_connection() + res = conn.eval_bool(expr).result() + return res['value'] + 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 44289372f1..a763c4fa82 100644 --- a/saw-remote-api/python/saw_client/commands.py +++ b/saw-remote-api/python/saw_client/commands.py @@ -196,6 +196,18 @@ def __init__( 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 4f446ba477..a90b20a01e 100644 --- a/saw-remote-api/python/saw_client/connection.py +++ b/saw-remote-api/python/saw_client/connection.py @@ -248,6 +248,15 @@ def eval_int(self, 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_int` 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 index 3e87188dd3..64edf87ed0 100644 --- a/saw-remote-api/python/tests/saw/test_eval.py +++ b/saw-remote-api/python/tests/saw/test_eval.py @@ -15,8 +15,11 @@ def test_provers(self): if __name__ == "__main__": saw.view(saw.LogResults()) - expr = cry('(6 : [8]) * 7') - self.assertEqual(saw.eval_int(expr), 42) + expr1 = cry('(6 : [8]) * 7') + self.assertEqual(saw.eval_int(expr1), 42) + + expr2 = cry('(1 < 2) : Bit') + self.assertTrue(saw.eval_bool(expr2)) if __name__ == "__main__": diff --git a/saw-remote-api/saw-remote-api/Main.hs b/saw-remote-api/saw-remote-api/Main.hs index 45ea1d7df5..4fedadf5da 100644 --- a/saw-remote-api/saw-remote-api/Main.hs +++ b/saw-remote-api/saw-remote-api/Main.hs @@ -19,7 +19,9 @@ import SAWServer.CryptolSetup import SAWServer.Data.JVMType() import SAWServer.Eval ( evalIntDescr, - evalInt ) + evalInt, + evalBoolDescr, + evalBool ) import SAWServer.Ghost ( createGhostVariableDescr, createGhostVariable ) @@ -124,6 +126,10 @@ sawMethods = "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 index 3d20e989e4..a915d71fbf 100644 --- a/saw-remote-api/src/SAWServer/Eval.hs +++ b/saw-remote-api/src/SAWServer/Eval.hs @@ -5,6 +5,8 @@ module SAWServer.Eval ( evalInt , evalIntDescr + , evalBool + , evalBoolDescr ) where import Control.Exception ( throw ) @@ -75,3 +77,49 @@ evalInt params = do Left err -> throw $ CryptolModuleException err warnings i <- tl $ SB.eval_int t pure $ EvalIntResult i + +data EvalBoolParams cryptolExpr = + EvalBoolParams + { evalBoolExpr :: cryptolExpr + } + +instance (FromJSON cryptolExpr) => FromJSON (EvalBoolParams cryptolExpr) where + parseJSON = + withObject "SAW/eval bool params" $ \o -> + EvalBoolParams <$> o .: "expr" + +data EvalBoolResult = + EvalBoolResult + { evalBoolValue :: Bool + } + +instance ToJSON EvalBoolResult where + toJSON r = object [ "value" .= evalBoolValue r ] + +evalBoolDescr :: Doc.Block +evalBoolDescr = + Doc.Paragraph [ Doc.Text "Attempt to evaluate the given term to a concrete boolean." ] + +instance Doc.DescribedMethod (EvalBoolParams cryptolExpr) EvalBoolResult where + parameterFieldDescription = + [ ("expr", + Doc.Paragraph [Doc.Text "The Cryptol expression to evaluate."]) + ] + resultFieldDescription = + [ ("value", + Doc.Paragraph [Doc.Text "The boolean value of the expresssion."]) + ] + +evalBool :: EvalBoolParams Expression -> Argo.Command SAWState EvalBoolResult +evalBool params = do + state <- Argo.getState + fileReader <- Argo.getFileReader + let cenv = SV.rwCryptol (view sawTopLevelRW state) + bic = view sawBIC state + cexp <- getCryptolExpr $ evalBoolExpr 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 + b <- tl $ SB.eval_bool t + pure $ EvalBoolResult b From 99c61d94d9bbf034c79f448489d0281e4df8798e Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Fri, 6 May 2022 15:31:13 -0400 Subject: [PATCH 3/8] Fix type error --- saw-remote-api/python/saw_client/__init__.py | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/saw-remote-api/python/saw_client/__init__.py b/saw-remote-api/python/saw_client/__init__.py index e48d4d457d..33aa5a799a 100644 --- a/saw-remote-api/python/saw_client/__init__.py +++ b/saw-remote-api/python/saw_client/__init__.py @@ -653,14 +653,20 @@ def eval_int(expr: cryptoltypes.CryptolJSON) -> int: """ conn = __get_designated_connection() res = conn.eval_int(expr).result() - return res['value'] + v = res['value'] + if not isinstance(v, int): + raise ValueError(str(v) + " is not an integer") + return v def eval_bool(expr: cryptoltypes.CryptolJSON) -> int: """Atempts to evaluate the given expression as a concrete boolean. """ conn = __get_designated_connection() res = conn.eval_bool(expr).result() - return res['value'] + 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.""" From 1fd1882d26bd5a77f8f66eb94c3256311c99425a Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Fri, 6 May 2022 16:21:53 -0400 Subject: [PATCH 4/8] Update SAW.rst --- saw-remote-api/docs/SAW.rst | 48 +++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) 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) ~~~~~~~~~~~~~~~~~~~~~~~~ From 24276e38860fdc5d4e52d6c60eea9946989317c2 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Sun, 8 May 2022 19:36:57 -0400 Subject: [PATCH 5/8] Refactor a bit --- saw-remote-api/src/SAWServer/Eval.hs | 90 ++++++++++------------------ 1 file changed, 33 insertions(+), 57 deletions(-) diff --git a/saw-remote-api/src/SAWServer/Eval.hs b/saw-remote-api/src/SAWServer/Eval.hs index a915d71fbf..984b3e4578 100644 --- a/saw-remote-api/src/SAWServer/Eval.hs +++ b/saw-remote-api/src/SAWServer/Eval.hs @@ -1,4 +1,5 @@ {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} @@ -23,6 +24,7 @@ import Data.Aeson 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 @@ -32,29 +34,25 @@ import SAWServer import SAWServer.CryptolExpression ( CryptolModuleException(..), getTypedTermOfCExp ) import SAWServer.TopLevel ( tl ) -data EvalIntParams cryptolExpr = - EvalIntParams +data EvalParams a cryptolExpr = + EvalParams { evalIntExpr :: cryptolExpr } -instance (FromJSON cryptolExpr) => FromJSON (EvalIntParams cryptolExpr) where +instance (FromJSON cryptolExpr) => FromJSON (EvalParams a cryptolExpr) where parseJSON = - withObject "SAW/eval int params" $ \o -> - EvalIntParams <$> o .: "expr" + withObject "SAW/eval params" $ \o -> + EvalParams <$> o .: "expr" -data EvalIntResult = - EvalIntResult - { evalIntValue :: Integer +data EvalResult a = + EvalResult + { evalValue :: a } -instance ToJSON EvalIntResult where - toJSON r = object [ "value" .= evalIntValue r ] +instance ToJSON a => ToJSON (EvalResult a) where + toJSON r = object [ "value" .= evalValue r ] -evalIntDescr :: Doc.Block -evalIntDescr = - Doc.Paragraph [ Doc.Text "Attempt to evaluate the given term to a concrete integer." ] - -instance Doc.DescribedMethod (EvalIntParams cryptolExpr) EvalIntResult where +instance Doc.DescribedMethod (EvalParams Integer cryptolExpr) (EvalResult Integer) where parameterFieldDescription = [ ("expr", Doc.Paragraph [Doc.Text "The Cryptol expression to evaluate."]) @@ -64,43 +62,7 @@ instance Doc.DescribedMethod (EvalIntParams cryptolExpr) EvalIntResult where Doc.Paragraph [Doc.Text "The integer value of the expresssion."]) ] -evalInt :: EvalIntParams Expression -> Argo.Command SAWState EvalIntResult -evalInt params = do - state <- Argo.getState - fileReader <- Argo.getFileReader - let cenv = SV.rwCryptol (view sawTopLevelRW state) - bic = view sawBIC state - cexp <- getCryptolExpr $ evalIntExpr 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 $ SB.eval_int t - pure $ EvalIntResult i - -data EvalBoolParams cryptolExpr = - EvalBoolParams - { evalBoolExpr :: cryptolExpr - } - -instance (FromJSON cryptolExpr) => FromJSON (EvalBoolParams cryptolExpr) where - parseJSON = - withObject "SAW/eval bool params" $ \o -> - EvalBoolParams <$> o .: "expr" - -data EvalBoolResult = - EvalBoolResult - { evalBoolValue :: Bool - } - -instance ToJSON EvalBoolResult where - toJSON r = object [ "value" .= evalBoolValue r ] - -evalBoolDescr :: Doc.Block -evalBoolDescr = - Doc.Paragraph [ Doc.Text "Attempt to evaluate the given term to a concrete boolean." ] - -instance Doc.DescribedMethod (EvalBoolParams cryptolExpr) EvalBoolResult where +instance Doc.DescribedMethod (EvalParams Bool cryptolExpr) (EvalResult Bool) where parameterFieldDescription = [ ("expr", Doc.Paragraph [Doc.Text "The Cryptol expression to evaluate."]) @@ -110,16 +72,30 @@ instance Doc.DescribedMethod (EvalBoolParams cryptolExpr) EvalBoolResult where Doc.Paragraph [Doc.Text "The boolean value of the expresssion."]) ] -evalBool :: EvalBoolParams Expression -> Argo.Command SAWState EvalBoolResult -evalBool params = do +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 $ evalBoolExpr params + cexp <- getCryptolExpr $ evalIntExpr 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 - b <- tl $ SB.eval_bool t - pure $ EvalBoolResult b + 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 From 0e4013777a9167307ac459cb28cac9798480847c Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Mon, 9 May 2022 12:21:20 -0400 Subject: [PATCH 6/8] Address review comments --- saw-remote-api/CHANGELOG.md | 6 +++++- saw-remote-api/python/CHANGELOG.md | 7 ++++++- saw-remote-api/python/pyproject.toml | 2 +- saw-remote-api/python/saw_client/__init__.py | 2 +- saw-remote-api/python/saw_client/connection.py | 2 +- saw-remote-api/python/tests/saw/test_eval.py | 10 +++------- saw-remote-api/saw-remote-api.cabal | 2 +- saw-remote-api/src/SAWServer/Eval.hs | 13 ++++++++----- 8 files changed, 26 insertions(+), 18 deletions(-) diff --git a/saw-remote-api/CHANGELOG.md b/saw-remote-api/CHANGELOG.md index 519e62d56e..ad964f69ce 100644 --- a/saw-remote-api/CHANGELOG.md +++ b/saw-remote-api/CHANGELOG.md @@ -1,7 +1,11 @@ # Revision history for saw-remote-api +## 0.9.2 -- 2022-05-09 -## 0.9.1 -- YYYY-MM-DD +* Introduced new methods `SAW/eval int` and `SAW/eval bool` that allow the + evaluation of Cryptol expressions into Python values. + +## 0.9.1 -- 2021-12-21 * `SAW/set option`'s `"option"` parameter is now allowed to be `"What4 eval"`, which controls whether to enable or disable What4 translation for SAWCore diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md index 7c4cb19f3f..1a7b5521e4 100644 --- a/saw-remote-api/python/CHANGELOG.md +++ b/saw-remote-api/python/CHANGELOG.md @@ -1,6 +1,11 @@ # Revision history for saw-client -## 0.9.1 -- YYYY-MM-DD +## 0.9.2 -- 2022-05-09 + +* Added two new commands, `eval_int` and `eval_bool`, that evaluate Cryptol + expressions to Python integers or booleans. + +## 0.9.1 -- 2021-12-21 * Add a `set_option` command to `saw_client` that allows enabling and disabling global SAW options. For example, SAWScript's `enable_lax_pointer_ordering` is diff --git a/saw-remote-api/python/pyproject.toml b/saw-remote-api/python/pyproject.toml index c7f25d3fd6..a727529b6f 100644 --- a/saw-remote-api/python/pyproject.toml +++ b/saw-remote-api/python/pyproject.toml @@ -1,6 +1,6 @@ [tool.poetry] name = "saw-client" -version = "0.9.1" +version = "0.9.2" readme = "README.md" description = "SAW client for the SAW 0.9 RPC server" authors = ["Galois, Inc. "] diff --git a/saw-remote-api/python/saw_client/__init__.py b/saw-remote-api/python/saw_client/__init__.py index 33aa5a799a..af4b54b61a 100644 --- a/saw-remote-api/python/saw_client/__init__.py +++ b/saw-remote-api/python/saw_client/__init__.py @@ -658,7 +658,7 @@ def eval_int(expr: cryptoltypes.CryptolJSON) -> int: raise ValueError(str(v) + " is not an integer") return v -def eval_bool(expr: cryptoltypes.CryptolJSON) -> int: +def eval_bool(expr: cryptoltypes.CryptolJSON) -> bool: """Atempts to evaluate the given expression as a concrete boolean. """ conn = __get_designated_connection() diff --git a/saw-remote-api/python/saw_client/connection.py b/saw-remote-api/python/saw_client/connection.py index a90b20a01e..0a45321815 100644 --- a/saw-remote-api/python/saw_client/connection.py +++ b/saw-remote-api/python/saw_client/connection.py @@ -252,7 +252,7 @@ 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_int` function. + 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 diff --git a/saw-remote-api/python/tests/saw/test_eval.py b/saw-remote-api/python/tests/saw/test_eval.py index 64edf87ed0..d756e7f60f 100644 --- a/saw-remote-api/python/tests/saw/test_eval.py +++ b/saw-remote-api/python/tests/saw/test_eval.py @@ -1,13 +1,9 @@ -from cryptol import cryptoltypes +import cryptol import saw_client as saw import unittest from pathlib import Path - -def cry(exp): - return cryptoltypes.CryptolLiteral(exp) - class ProverTest(unittest.TestCase): def test_provers(self): @@ -15,10 +11,10 @@ def test_provers(self): if __name__ == "__main__": saw.view(saw.LogResults()) - expr1 = cry('(6 : [8]) * 7') + expr1 = cryptol.cry_f('(6 : [8]) * 7') self.assertEqual(saw.eval_int(expr1), 42) - expr2 = cry('(1 < 2) : Bit') + expr2 = cryptol.cry_f('(1 < 2) : Bit') self.assertTrue(saw.eval_bool(expr2)) diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal index efdefc63a6..8122d1525c 100644 --- a/saw-remote-api/saw-remote-api.cabal +++ b/saw-remote-api/saw-remote-api.cabal @@ -4,7 +4,7 @@ cabal-version: 2.4 -- http://haskell.org/cabal/users-guide/ name: saw-remote-api -version: 0.9.1 +version: 0.9.2 -- synopsis: -- description: -- bug-reports: diff --git a/saw-remote-api/src/SAWServer/Eval.hs b/saw-remote-api/src/SAWServer/Eval.hs index 984b3e4578..0ede8389f9 100644 --- a/saw-remote-api/src/SAWServer/Eval.hs +++ b/saw-remote-api/src/SAWServer/Eval.hs @@ -34,9 +34,12 @@ import SAWServer import SAWServer.CryptolExpression ( CryptolModuleException(..), getTypedTermOfCExp ) import SAWServer.TopLevel ( tl ) -data EvalParams a cryptolExpr = +-- 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 +data EvalParams evalty cryptolExpr = EvalParams - { evalIntExpr :: cryptolExpr + { evalExpr :: cryptolExpr } instance (FromJSON cryptolExpr) => FromJSON (EvalParams a cryptolExpr) where @@ -44,9 +47,9 @@ instance (FromJSON cryptolExpr) => FromJSON (EvalParams a cryptolExpr) where withObject "SAW/eval params" $ \o -> EvalParams <$> o .: "expr" -data EvalResult a = +data EvalResult evalty = EvalResult - { evalValue :: a + { evalValue :: evalty } instance ToJSON a => ToJSON (EvalResult a) where @@ -78,7 +81,7 @@ eval f params = do fileReader <- Argo.getFileReader let cenv = SV.rwCryptol (view sawTopLevelRW state) bic = view sawBIC state - cexp <- getCryptolExpr $ evalIntExpr params + 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 From b374194be5119a66b5df28b8985490b48d08cdb2 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Mon, 9 May 2022 13:02:51 -0400 Subject: [PATCH 7/8] Update changelogs --- saw-remote-api/CHANGELOG.md | 10 +++------- saw-remote-api/python/CHANGELOG.md | 9 +++------ saw-remote-api/python/pyproject.toml | 2 +- saw-remote-api/saw-remote-api.cabal | 2 +- 4 files changed, 8 insertions(+), 15 deletions(-) diff --git a/saw-remote-api/CHANGELOG.md b/saw-remote-api/CHANGELOG.md index ad964f69ce..afd6b58e91 100644 --- a/saw-remote-api/CHANGELOG.md +++ b/saw-remote-api/CHANGELOG.md @@ -1,11 +1,6 @@ # Revision history for saw-remote-api -## 0.9.2 -- 2022-05-09 - -* Introduced new methods `SAW/eval int` and `SAW/eval bool` that allow the - evaluation of Cryptol expressions into Python values. - -## 0.9.1 -- 2021-12-21 +## 0.9.1 -- YYYY-MM-DD * `SAW/set option`'s `"option"` parameter is now allowed to be `"What4 eval"`, which controls whether to enable or disable What4 translation for SAWCore @@ -20,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/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md index 1a7b5521e4..4246522d1f 100644 --- a/saw-remote-api/python/CHANGELOG.md +++ b/saw-remote-api/python/CHANGELOG.md @@ -1,11 +1,6 @@ # Revision history for saw-client -## 0.9.2 -- 2022-05-09 - -* Added two new commands, `eval_int` and `eval_bool`, that evaluate Cryptol - expressions to Python integers or booleans. - -## 0.9.1 -- 2021-12-21 +## 0.9.1 -- YYYY-MM-DD * Add a `set_option` command to `saw_client` that allows enabling and disabling global SAW options. For example, SAWScript's `enable_lax_pointer_ordering` is @@ -18,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/pyproject.toml b/saw-remote-api/python/pyproject.toml index a727529b6f..c7f25d3fd6 100644 --- a/saw-remote-api/python/pyproject.toml +++ b/saw-remote-api/python/pyproject.toml @@ -1,6 +1,6 @@ [tool.poetry] name = "saw-client" -version = "0.9.2" +version = "0.9.1" readme = "README.md" description = "SAW client for the SAW 0.9 RPC server" authors = ["Galois, Inc. "] diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal index 8122d1525c..efdefc63a6 100644 --- a/saw-remote-api/saw-remote-api.cabal +++ b/saw-remote-api/saw-remote-api.cabal @@ -4,7 +4,7 @@ cabal-version: 2.4 -- http://haskell.org/cabal/users-guide/ name: saw-remote-api -version: 0.9.2 +version: 0.9.1 -- synopsis: -- description: -- bug-reports: From 6b38fcd7c67ddf8e1903ced6e1a9f51a585fd26d Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Mon, 9 May 2022 13:03:25 -0400 Subject: [PATCH 8/8] data -> newtype --- saw-remote-api/src/SAWServer/Eval.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/saw-remote-api/src/SAWServer/Eval.hs b/saw-remote-api/src/SAWServer/Eval.hs index 0ede8389f9..7e783f32f2 100644 --- a/saw-remote-api/src/SAWServer/Eval.hs +++ b/saw-remote-api/src/SAWServer/Eval.hs @@ -37,7 +37,7 @@ 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 -data EvalParams evalty cryptolExpr = +newtype EvalParams evalty cryptolExpr = EvalParams { evalExpr :: cryptolExpr } @@ -47,7 +47,7 @@ instance (FromJSON cryptolExpr) => FromJSON (EvalParams a cryptolExpr) where withObject "SAW/eval params" $ \o -> EvalParams <$> o .: "expr" -data EvalResult evalty = +newtype EvalResult evalty = EvalResult { evalValue :: evalty }