GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-22 11:46:03 +03:00
Code Issues Projects Releases Wiki Activity

feat: initial co-located python client

Browse Source
This commit is contained in:
Andrew Kent 2021-03-01 14:29:57 -08:00
parent 27b8718891
commit 307c18f1f4
12 changed files with 203 additions and 212 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
.gitmodules vendored
View File

@ -4,6 +4,3 @@
[submodule "deps/argo"] [submodule "deps/argo"]
path = deps/argo path = deps/argo
url = https://github.com/galoisinc/argo url = https://github.com/galoisinc/argo
[submodule "cryptol-remote-api/test/galois-py-toolkit"]
path = cryptol-remote-api/test/galois-py-toolkit
url = https://github.com/GaloisInc/galois-py-toolkit.git

5
cry
View File

@ -87,10 +87,7 @@ case $COMMAND in
rpc-test) rpc-test)
echo Running RPC server tests echo Running RPC server tests
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
if [ ! -d "$DIR/cryptol-remote-api/test/galois-py-toolkit/tests" ]; then $DIR/cryptol-remote-api/run_rpc_tests.sh
git submodule update --init $DIR/cryptol-remote-api
fi
$DIR/cryptol-remote-api/test/run_rpc_tests.sh
;; ;;

19
cryptol-remote-api/cryptol-remote-api.cabal
View File

@ -93,22 +93,3 @@ executable cryptol-eval-server
sbv < 8.10 sbv < 8.10
test-suite test-cryptol-remote-api
import: deps, warnings, errors
type: exitcode-stdio-1.0
hs-source-dirs: test
main-is: Test.hs
other-modules: Paths_cryptol_remote_api
ghc-options:
-Wno-orphans
build-tool-depends:
cryptol-remote-api:cryptol-remote-api,
cryptol-remote-api:cryptol-eval-server
build-depends:
argo-python,
cryptol-remote-api,
quickcheck-instances ^>= 0.3.19,
tasty >= 1.2.1,
tasty-quickcheck ^>= 0.10,
tasty-hunit,
tasty-script-exitcode

0
cryptol-remote-api/python/README.md Normal file
View File

28
cryptol-remote-api/python/cryptol/__init__.py
View File

@ -106,7 +106,7 @@ class CryptolLoadFile(argo.Command):
return res return res
class CryptolEvalExpr(argo.Query): class CryptolEvalExpr(argo.Command):
def __init__(self, connection : HasProtocolState, expr : Any) -> None: def __init__(self, connection : HasProtocolState, expr : Any) -> None:
super(CryptolEvalExpr, self).__init__( super(CryptolEvalExpr, self).__init__(
'evaluate expression', 'evaluate expression',
@ -117,7 +117,7 @@ class CryptolEvalExpr(argo.Query):
def process_result(self, res : Any) -> Any: def process_result(self, res : Any) -> Any:
return res return res
class CryptolCall(argo.Query): class CryptolCall(argo.Command):
def __init__(self, connection : HasProtocolState, fun : str, args : List[Any]) -> None: def __init__(self, connection : HasProtocolState, fun : str, args : List[Any]) -> None:
super(CryptolCall, self).__init__( super(CryptolCall, self).__init__(
'call', 'call',
@ -128,7 +128,7 @@ class CryptolCall(argo.Query):
def process_result(self, res : Any) -> Any: def process_result(self, res : Any) -> Any:
return from_cryptol_arg(res['value']) return from_cryptol_arg(res['value'])
class CryptolCheckType(argo.Query): class CryptolCheckType(argo.Command):
def __init__(self, connection : HasProtocolState, expr : Any) -> None: def __init__(self, connection : HasProtocolState, expr : Any) -> None:
super(CryptolCheckType, self).__init__( super(CryptolCheckType, self).__init__(
'check type', 'check type',
@ -139,7 +139,7 @@ class CryptolCheckType(argo.Query):
def process_result(self, res : Any) -> Any: def process_result(self, res : Any) -> Any:
return res['type schema'] return res['type schema']
class CryptolProveSat(argo.Query): class CryptolProveSat(argo.Command):
def __init__(self, connection : HasProtocolState, qtype : str, expr : Any, solver : solver.Solver, count : Optional[int]) -> None: def __init__(self, connection : HasProtocolState, qtype : str, expr : Any, solver : solver.Solver, count : Optional[int]) -> None:
super(CryptolProveSat, self).__init__( super(CryptolProveSat, self).__init__(
'prove or satisfy', 'prove or satisfy',
@ -177,14 +177,14 @@ class CryptolSat(CryptolProveSat):
def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver, count : int) -> None: def __init__(self, connection : HasProtocolState, expr : Any, solver : solver.Solver, count : int) -> None:
super(CryptolSat, self).__init__(connection, 'sat', expr, solver, count) super(CryptolSat, self).__init__(connection, 'sat', expr, solver, count)
class CryptolNames(argo.Query): class CryptolNames(argo.Command):
def __init__(self, connection : HasProtocolState) -> None: def __init__(self, connection : HasProtocolState) -> None:
super(CryptolNames, self).__init__('visible names', {}, connection) super(CryptolNames, self).__init__('visible names', {}, connection)
def process_result(self, res : Any) -> Any: def process_result(self, res : Any) -> Any:
return res return res
class CryptolFocusedModule(argo.Query): class CryptolFocusedModule(argo.Command):
def __init__(self, connection : HasProtocolState) -> None: def __init__(self, connection : HasProtocolState) -> None:
super(CryptolFocusedModule, self).__init__( super(CryptolFocusedModule, self).__init__(
'focused module', 'focused module',
@ -324,7 +324,7 @@ class CryptolConnection:
self.most_recent_result = CryptolLoadModule(self, module_name) self.most_recent_result = CryptolLoadModule(self, module_name)
return self.most_recent_result return self.most_recent_result
def eval(self, expression : Any) -> argo.Query: def eval(self, expression : Any) -> argo.Command:
"""Evaluate a Cryptol expression, represented according to """Evaluate a Cryptol expression, represented according to
:ref:`cryptol-json-expression`, with Python datatypes standing :ref:`cryptol-json-expression`, with Python datatypes standing
for their JSON equivalents. for their JSON equivalents.
@ -332,17 +332,17 @@ class CryptolConnection:
self.most_recent_result = CryptolEvalExpr(self, expression) self.most_recent_result = CryptolEvalExpr(self, expression)
return self.most_recent_result return self.most_recent_result
def evaluate_expression(self, expression : Any) -> argo.Query: def evaluate_expression(self, expression : Any) -> argo.Command:
"""Synonym for member method ``eval``. """Synonym for member method ``eval``.
""" """
return self.eval(expression) return self.eval(expression)
def call(self, fun : str, *args : List[Any]) -> argo.Query: def call(self, fun : str, *args : List[Any]) -> argo.Command:
encoded_args = [cryptoltypes.CryptolType().from_python(a) for a in args] encoded_args = [cryptoltypes.CryptolType().from_python(a) for a in args]
self.most_recent_result = CryptolCall(self, fun, encoded_args) self.most_recent_result = CryptolCall(self, fun, encoded_args)
return self.most_recent_result return self.most_recent_result
def check_type(self, code : Any) -> argo.Query: def check_type(self, code : Any) -> argo.Command:
"""Check the type of a Cryptol expression, represented according to """Check the type of a Cryptol expression, represented according to
:ref:`cryptol-json-expression`, with Python datatypes standing for :ref:`cryptol-json-expression`, with Python datatypes standing for
their JSON equivalents. their JSON equivalents.
@ -350,7 +350,7 @@ class CryptolConnection:
self.most_recent_result = CryptolCheckType(self, code) self.most_recent_result = CryptolCheckType(self, code)
return self.most_recent_result return self.most_recent_result
def sat(self, expr : Any, solver : solver.Solver = solver.Z3, count : int = 1) -> argo.Query: def sat(self, expr : Any, solver : solver.Solver = solver.Z3, count : int = 1) -> argo.Command:
"""Check the satisfiability of a Cryptol expression, represented according to """Check the satisfiability of a Cryptol expression, represented according to
:ref:`cryptol-json-expression`, with Python datatypes standing for :ref:`cryptol-json-expression`, with Python datatypes standing for
their JSON equivalents. Use the solver named `solver`, and return up to their JSON equivalents. Use the solver named `solver`, and return up to
@ -359,7 +359,7 @@ class CryptolConnection:
self.most_recent_result = CryptolSat(self, expr, solver, count) self.most_recent_result = CryptolSat(self, expr, solver, count)
return self.most_recent_result return self.most_recent_result
def prove(self, expr : Any, solver : solver.Solver = solver.Z3) -> argo.Query: def prove(self, expr : Any, solver : solver.Solver = solver.Z3) -> argo.Command:
"""Check the validity of a Cryptol expression, represented according to """Check the validity of a Cryptol expression, represented according to
:ref:`cryptol-json-expression`, with Python datatypes standing for :ref:`cryptol-json-expression`, with Python datatypes standing for
their JSON equivalents. Use the solver named `solver`. their JSON equivalents. Use the solver named `solver`.
@ -367,12 +367,12 @@ class CryptolConnection:
self.most_recent_result = CryptolProve(self, expr, solver) self.most_recent_result = CryptolProve(self, expr, solver)
return self.most_recent_result return self.most_recent_result
def names(self) -> argo.Query: def names(self) -> argo.Command:
"""Discover the list of names currently in scope in the current context.""" """Discover the list of names currently in scope in the current context."""
self.most_recent_result = CryptolNames(self) self.most_recent_result = CryptolNames(self)
return self.most_recent_result return self.most_recent_result
def focused_module(self) -> argo.Query: def focused_module(self) -> argo.Command:
"""Return the name of the currently-focused module.""" """Return the name of the currently-focused module."""
self.most_recent_result = CryptolFocusedModule(self) self.most_recent_result = CryptolFocusedModule(self)
return self.most_recent_result return self.most_recent_result

7
cryptol-remote-api/python/mypy.ini
View File

@ -11,10 +11,3 @@ warn_unused_ignores = True
[mypy-cryptol.*] [mypy-cryptol.*]
disallow_untyped_defs = True disallow_untyped_defs = True
warn_unreachable = True warn_unreachable = True
[mypy-saw.*]
disallow_untyped_defs = True
[mypy-saw.llvm]
# fails for re match objects right now
warn_unreachable = False

15
cryptol-remote-api/python/setup.py
View File

@ -10,23 +10,22 @@ def get_README():
return content return content
setup( setup(
name="galois-toolkit", name="cryptol",
python_requires=">=3.7", python_requires=">=3.7",
version="0.0.1", version="0.0.1",
url="https://github.com/GaloisInc/galois-py-toolkit", url="https://github.com/GaloisInc/cryptol",
project_urls={ project_urls={
"Changelog": "https://github.com/GaloisInc/galois-py-toolkit/tree/main/CHANGELOG.md", "Source": "https://github.com/GaloisInc/cryptol/tree/master/cryptol-remote-api/pthon",
"Source": "https://github.com/GaloisInc/galois-py-toolkit/tree/main/cryptol", "Bug Tracker": "https://github.com/GaloisInc/cryptol/issues"
"Bug Tracker": "https://github.com/GaloisInc/galois-py-toolkit/issues"
}, },
license="BSD", license="BSD",
description="A scripting library for interacting with the Cryptol and SAW RPC servers.", description="A scripting library for interacting with the Cryptol RPC server.",
long_description=get_README(), long_description=get_README(),
long_description_content_type="text/markdown", long_description_content_type="text/markdown",
author="Galois, Inc.", author="Galois, Inc.",
author_email="andrew@galois.com", author_email="andrew@galois.com",
packages=["cryptol", "saw"], packages=["cryptol"],
package_data={"cryptol": ["py.typed"], "saw": ["py.typed"]}, package_data={"cryptol": ["py.typed"]},
zip_safe=False, zip_safe=False,
install_requires=[ install_requires=[
"BitVector==3.4.9", "BitVector==3.4.9",

30
cryptol-remote-api/python/tests/cryptol/test_cryptol_api.py
View File

@ -26,18 +26,20 @@ class CryptolTests(unittest.TestCase):
self.assertEqual(c.call('add', b'\0', b'\1').result(), BV(8,1)) self.assertEqual(c.call('add', b'\0', b'\1').result(), BV(8,1))
self.assertEqual(c.call('add', bytes.fromhex('ff'), bytes.fromhex('03')).result(), BV(8,2)) self.assertEqual(c.call('add', bytes.fromhex('ff'), bytes.fromhex('03')).result(), BV(8,2))
def test_module_import(self): # AMK: importing cryptol bindings into Python temporarily broken due to linear state usage changes
c = self.c # in argo approx 1 March 2020
cryptol.add_cryptol_module('Foo', c) # def test_module_import(self):
from Foo import add # c = self.c
self.assertEqual(add(b'\2', 2), BV(8,4)) # cryptol.add_cryptol_module('Foo', c)
# from Foo import add
# self.assertEqual(add(b'\2', 2), BV(8,4))
self.assertEqual(add(BitVector( intVal = 0, size = 8 ), BitVector( intVal = 1, size = 8 )), BV(8,1)) # self.assertEqual(add(BitVector( intVal = 0, size = 8 ), BitVector( intVal = 1, size = 8 )), BV(8,1))
self.assertEqual(add(BitVector( intVal = 1, size = 8 ), BitVector( intVal = 2, size = 8 )), BV(8,3)) # self.assertEqual(add(BitVector( intVal = 1, size = 8 ), BitVector( intVal = 2, size = 8 )), BV(8,3))
self.assertEqual(add(BitVector( intVal = 255, size = 8 ), BitVector( intVal = 1, size = 8 )), BV(8,0)) # self.assertEqual(add(BitVector( intVal = 255, size = 8 ), BitVector( intVal = 1, size = 8 )), BV(8,0))
self.assertEqual(add(BV(8,0), BV(8,1)), BV(8,1)) # self.assertEqual(add(BV(8,0), BV(8,1)), BV(8,1))
self.assertEqual(add(BV(8,1), BV(8,2)), BV(8,3)) # self.assertEqual(add(BV(8,1), BV(8,2)), BV(8,3))
self.assertEqual(add(BV(8,255), BV(8,1)), BV(8,0)) # self.assertEqual(add(BV(8,255), BV(8,1)), BV(8,0))
def test_sat(self): def test_sat(self):
c = self.c c = self.c
@ -67,5 +69,11 @@ class CryptolTests(unittest.TestCase):
# check for a valid condition # check for a valid condition
self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]').result()) self.assertTrue(c.prove('\\x -> isSqrtOf9 x ==> elem x [3,131,125,253]').result())
def test_repeat_usages(self):
c = self.c
for i in range(0,100):
x_val = c.evaluate_expression("x").result()
self.assertEqual(c.eval("Id::id x").result(), x_val)
if __name__ == "__main__": if __name__ == "__main__":
unittest.main() unittest.main()

215
cryptol-remote-api/python/tests/cryptol/test_low_level_ops.py
View File

@ -13,21 +13,23 @@ from distutils.spawn import find_executable
# Test empty options # Test empty options
def do_test_options(c, state, options): def do_test_options(c, state, options):
id_opt = c.send_query("evaluate expression", {"state": state, "expression": "four", "options": options}) id_opt = c.send_command("evaluate expression", {"state": state, "expression": "four", "options": options})
reply_opt = c.wait_for_reply_to(id_opt) reply = c.wait_for_reply_to(id_opt)
assert('result' in reply_opt) assert('result' in reply)
assert('answer' in reply_opt['result']) assert('answer' in reply['result'])
assert('value' in reply_opt['result']['answer']) assert('value' in reply['result']['answer'])
assert(reply_opt['result']['answer']['value'] == {'data': '00004', 'width': 17, 'expression': 'bits', 'encoding': 'hex'}) assert(reply['result']['answer']['value'] == {'data': '00004', 'width': 17, 'expression': 'bits', 'encoding': 'hex'})
return reply['result']['state']
def do_test_instantiation(c, state, t, expected=None): def do_test_instantiation(c, state, t, expected=None):
if expected is None: expected = t if expected is None: expected = t
id_t = c.send_query("check type", {"state": state, "expression": {"expression": "instantiate", "generic": "id", "arguments": {"a": t}}}) id_t = c.send_command("check type", {"state": state, "expression": {"expression": "instantiate", "generic": "id", "arguments": {"a": t}}})
reply_t = c.wait_for_reply_to(id_t) reply = c.wait_for_reply_to(id_t)
assert('result' in reply_t) assert('result' in reply)
assert('answer' in reply_t['result']) assert('answer' in reply['result'])
assert('type schema' in reply_t['result']['answer']) assert('type schema' in reply['result']['answer'])
assert(reply_t['result']['answer']['type schema']['type']['domain'] == expected) assert(reply['result']['answer']['type schema']['type']['domain'] == expected)
return reply['result']['state']
class LowLevelCryptolApiTests(unittest.TestCase): class LowLevelCryptolApiTests(unittest.TestCase):
c = None c = None
@ -46,42 +48,45 @@ class LowLevelCryptolApiTests(unittest.TestCase):
def test_low_level_api(self): def test_low_level_api(self):
c = self.c c = self.c
id_1 = c.send_command("load file", {"file": str(Path('tests','cryptol','test-files', 'M.cry')), "state": None}) uid = c.send_command("load file", {"file": str(Path('tests','cryptol','test-files', 'M.cry')), "state": None})
reply_1 = c.wait_for_reply_to(id_1) reply = c.wait_for_reply_to(uid)
self.assertIn('result', reply_1) self.assertIn('result', reply)
self.assertIn('state', reply_1['result']) self.assertIn('state', reply['result'])
self.assertIn('answer', reply_1['result']) self.assertIn('answer', reply['result'])
state_1 = reply_1['result']['state'] state = reply['result']['state']
id_2 = c.send_query("evaluate expression", {"expression": {"expression":"call","function":"f","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": state_1}) uid = c.send_command("evaluate expression", {"expression": {"expression":"call","function":"f","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": state})
reply_2 = c.wait_for_reply_to(id_2) reply = c.wait_for_reply_to(uid)
self.assertIn('result', reply_2) self.assertIn('result', reply)
self.assertIn('answer', reply_2['result']) self.assertIn('answer', reply['result'])
self.assertIn('value', reply_2['result']['answer']) self.assertIn('value', reply['result']['answer'])
self.assertEqual(reply_2['result']['answer']['value'], self.assertEqual(reply['result']['answer']['value'],
{'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}, {'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'},
{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}], {'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}],
'expression': 'sequence'}) 'expression': 'sequence'})
state = reply['result']['state']
id_3 = c.send_query("evaluate expression", {"expression": {"expression":"call","function":"g","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": state_1}) uid = c.send_command("evaluate expression", {"expression": {"expression":"call","function":"g","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": state})
reply_3 = c.wait_for_reply_to(id_3) reply = c.wait_for_reply_to(uid)
self.assertIn('result', reply_3) self.assertIn('result', reply)
self.assertIn('answer', reply_3['result']) self.assertIn('answer', reply['result'])
self.assertIn('value', reply_3['result']['answer']) self.assertIn('value', reply['result']['answer'])
self.assertEqual(reply_3['result']['answer']['value'], self.assertEqual(reply['result']['answer']['value'],
{'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}, {'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'},
{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}], {'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}],
'expression': 'sequence'}) 'expression': 'sequence'})
state = reply['result']['state']
id_4 = c.send_query("evaluate expression", {"expression":{"expression":"call","function":"h","arguments":[{"expression":"sequence","data":[{"expression":"bits","encoding":"hex","data":"ff","width":8},{"expression":"bits","encoding":"hex","data":"ff","width":8}]}]}, "state": state_1}) uid = c.send_command("evaluate expression", {"expression":{"expression":"call","function":"h","arguments":[{"expression":"sequence","data":[{"expression":"bits","encoding":"hex","data":"ff","width":8},{"expression":"bits","encoding":"hex","data":"ff","width":8}]}]}, "state": state})
reply_4 = c.wait_for_reply_to(id_4) reply = c.wait_for_reply_to(uid)
self.assertIn('result', reply_4) self.assertIn('result', reply)
self.assertIn('answer', reply_4['result']) self.assertIn('answer', reply['result'])
self.assertIn('value', reply_4['result']['answer']) self.assertIn('value', reply['result']['answer'])
self.assertEqual(reply_4['result']['answer']['value'], self.assertEqual(reply['result']['answer']['value'],
{'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}, {'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'},
{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}], {'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}],
'expression': 'sequence'}) 'expression': 'sequence'})
state = reply['result']['state']
a_record = {"expression": "record", a_record = {"expression": "record",
"data": {"unit": "()", "data": {"unit": "()",
@ -90,12 +95,12 @@ class LowLevelCryptolApiTests(unittest.TestCase):
"width": 4, "width": 4,
"data": "f"}}} "data": "f"}}}
id_5 = c.send_query("evaluate expression", {"state": state_1, "expression": a_record}) uid = c.send_command("evaluate expression", {"state": state, "expression": a_record})
reply_5 = c.wait_for_reply_to(id_5) reply = c.wait_for_reply_to(uid)
self.assertIn('result', reply_5) self.assertIn('result', reply)
self.assertIn('answer', reply_5['result']) self.assertIn('answer', reply['result'])
self.assertIn('value', reply_5['result']['answer']) self.assertIn('value', reply['result']['answer'])
self.assertEqual(reply_5['result']['answer']['value'], self.assertEqual(reply['result']['answer']['value'],
{'expression': 'record', {'expression': 'record',
'data': {'fifteen': 'data': {'fifteen':
{'data': 'f', {'data': 'f',
@ -104,18 +109,19 @@ class LowLevelCryptolApiTests(unittest.TestCase):
'encoding': 'hex'}, 'encoding': 'hex'},
'unit': 'unit':
{'expression': 'unit'}}}) {'expression': 'unit'}}})
state = reply['result']['state']
id_6 = c.send_query("evaluate expression", uid = c.send_command("evaluate expression",
{"state": state_1, {"state": state,
"expression": {"expression": "let", "expression": {"expression": "let",
"binders": [{"name": "theRecord", "definition": a_record}], "binders": [{"name": "theRecord", "definition": a_record}],
"body": {"expression": "tuple", "body": {"expression": "tuple",
"data": [a_record, "theRecord"]}}}) "data": [a_record, "theRecord"]}}})
reply_6 = c.wait_for_reply_to(id_6) reply = c.wait_for_reply_to(uid)
self.assertIn('result', reply_6) self.assertIn('result', reply)
self.assertIn('answer', reply_6['result']) self.assertIn('answer', reply['result'])
self.assertIn('value', reply_6['result']['answer']) self.assertIn('value', reply['result']['answer'])
self.assertEqual(reply_6['result']['answer']['value'], self.assertEqual(reply['result']['answer']['value'],
{'expression': 'tuple', {'expression': 'tuple',
'data': [{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'}, 'data': [{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'},
'unit': {'expression': 'unit'}}, 'unit': {'expression': 'unit'}},
@ -123,16 +129,17 @@ class LowLevelCryptolApiTests(unittest.TestCase):
{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'}, {'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'},
'unit': {'expression': 'unit'}}, 'unit': {'expression': 'unit'}},
'expression': 'record'}]}) 'expression': 'record'}]})
state = reply['result']['state']
id_7 = c.send_query("evaluate expression", uid = c.send_command("evaluate expression",
{"state": state_1, {"state": state,
"expression": {"expression": "sequence", "expression": {"expression": "sequence",
"data": [a_record, a_record]}}) "data": [a_record, a_record]}})
reply_7 = c.wait_for_reply_to(id_7) reply = c.wait_for_reply_to(uid)
self.assertIn('result', reply_7) self.assertIn('result', reply)
self.assertIn('answer', reply_7['result']) self.assertIn('answer', reply['result'])
self.assertIn('value', reply_7['result']['answer']) self.assertIn('value', reply['result']['answer'])
self.assertEqual(reply_7['result']['answer']['value'], self.assertEqual(reply['result']['answer']['value'],
{'expression': 'sequence', {'expression': 'sequence',
'data': [{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'}, 'data': [{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'},
'unit': {'expression': 'unit'}}, 'unit': {'expression': 'unit'}},
@ -140,78 +147,84 @@ class LowLevelCryptolApiTests(unittest.TestCase):
{'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'}, {'data': {'fifteen': {'data': 'f', 'width': 4, 'expression': 'bits', 'encoding': 'hex'},
'unit': {'expression': 'unit'}}, 'unit': {'expression': 'unit'}},
'expression': 'record'}]}) 'expression': 'record'}]})
state = reply['result']['state']
id_8 = c.send_query("evaluate expression", uid = c.send_command("evaluate expression",
{"state": state_1, {"state": state,
"expression": {"expression": "integer modulo", "expression": {"expression": "integer modulo",
"integer": 14, "integer": 14,
"modulus": 42}}) "modulus": 42}})
reply_8 = c.wait_for_reply_to(id_8) reply = c.wait_for_reply_to(uid)
self.assertIn('result', reply_8) self.assertIn('result', reply)
self.assertIn('answer', reply_8['result']) self.assertIn('answer', reply['result'])
self.assertIn('value', reply_8['result']['answer']) self.assertIn('value', reply['result']['answer'])
self.assertEqual(reply_8['result']['answer']['value'], self.assertEqual(reply['result']['answer']['value'],
{"expression": "integer modulo", {"expression": "integer modulo",
"integer": 14, "integer": 14,
"modulus": 42}) "modulus": 42})
state = reply['result']['state']
id_9 = c.send_query("evaluate expression", uid = c.send_command("evaluate expression",
{"state": state_1, {"state": state,
"expression": "m `{a=60}"}) "expression": "m `{a=60}"})
reply_9 = c.wait_for_reply_to(id_9) reply = c.wait_for_reply_to(uid)
self.assertIn('result', reply_9) self.assertIn('result', reply)
self.assertIn('answer', reply_9['result']) self.assertIn('answer', reply['result'])
self.assertIn('value', reply_9['result']['answer']) self.assertIn('value', reply['result']['answer'])
self.assertEqual(reply_9['result']['answer']['value'], self.assertEqual(reply['result']['answer']['value'],
{"expression": "integer modulo", {"expression": "integer modulo",
"integer": 42, "integer": 42,
"modulus": 60}) "modulus": 60})
state = reply['result']['state']
id_10 = c.send_query("evaluate expression", {"state": state_1, "expression": "two"}) uid = c.send_command("evaluate expression", {"state": state, "expression": "two"})
reply_10 = c.wait_for_reply_to(id_10) reply = c.wait_for_reply_to(uid)
self.assertIn('result', reply_10) self.assertIn('result', reply)
self.assertIn('answer', reply_10['result']) self.assertIn('answer', reply['result'])
self.assertIn('value', reply_10['result']['answer']) self.assertIn('value', reply['result']['answer'])
self.assertEqual(reply_10['result']['answer']['value'], {'data': '0002', 'width': 15, 'expression': 'bits', 'encoding': 'hex'}) self.assertEqual(reply['result']['answer']['value'], {'data': '0002', 'width': 15, 'expression': 'bits', 'encoding': 'hex'})
state = reply['result']['state']
id_11 = c.send_query("evaluate expression", {"state": state_1, "expression": "three"}) uid = c.send_command("evaluate expression", {"state": state, "expression": "three"})
reply_11 = c.wait_for_reply_to(id_11) reply = c.wait_for_reply_to(uid)
self.assertIn('result', reply_11) self.assertIn('result', reply)
self.assertIn('answer', reply_11['result']) self.assertIn('answer', reply['result'])
self.assertIn('value', reply_11['result']['answer']) self.assertIn('value', reply['result']['answer'])
self.assertEqual(reply_11['result']['answer']['value'], {'data': '0003', 'width': 16, 'expression': 'bits', 'encoding': 'hex'}) self.assertEqual(reply['result']['answer']['value'], {'data': '0003', 'width': 16, 'expression': 'bits', 'encoding': 'hex'})
state = reply['result']['state']
id_12 = c.send_query("evaluate expression", {"state": state_1, "expression": "four"}) uid = c.send_command("evaluate expression", {"state": state, "expression": "four"})
reply_12 = c.wait_for_reply_to(id_12) reply = c.wait_for_reply_to(uid)
self.assertIn('result', reply_12) self.assertIn('result', reply)
self.assertIn('answer', reply_12['result']) self.assertIn('answer', reply['result'])
self.assertIn('value', reply_12['result']['answer']) self.assertIn('value', reply['result']['answer'])
self.assertEqual(reply_12['result']['answer']['value'], {'data': '00004', 'width': 17, 'expression': 'bits', 'encoding': 'hex'}) self.assertEqual(reply['result']['answer']['value'], {'data': '00004', 'width': 17, 'expression': 'bits', 'encoding': 'hex'})
state = reply['result']['state']
do_test_options(c, state_1, dict()) state = do_test_options(c, state, dict())
do_test_options(c, state_1, {"call stacks": True}) state = do_test_options(c, state, {"call stacks": True})
do_test_options(c, state_1, {"call stacks": False}) state = do_test_options(c, state, {"call stacks": False})
do_test_options(c, state_1, {"call stacks": False, "output": dict()}) state = do_test_options(c, state, {"call stacks": False, "output": dict()})
do_test_options(c, state_1, {"call stacks": False, "output": {"ASCII": True}}) state = do_test_options(c, state, {"call stacks": False, "output": {"ASCII": True}})
do_test_options(c, state_1, {"call stacks": False, "output": {"base": 16}}) state = do_test_options(c, state, {"call stacks": False, "output": {"base": 16}})
do_test_options(c, state_1, {"call stacks": False, "output": {"prefix of infinite lengths": 3}}) state = do_test_options(c, state, {"call stacks": False, "output": {"prefix of infinite lengths": 3}})
# These test both the type instantiation form and the serialization/deserialization of the types involved # These test both the type instantiation form and the serialization/deserialization of the types involved
do_test_instantiation(c, state_1, {"type": "Integer"}) state = do_test_instantiation(c, state, {"type": "Integer"})
do_test_instantiation(c, state_1, {"type": "record", state = do_test_instantiation(c, state, {"type": "record",
"fields": {'a': {'type': 'Integer'}, "fields": {'a': {'type': 'Integer'},
'b': {'type': 'sequence', 'length': {'type': 'inf'}, 'contents': {'type': 'unit'}}}}) 'b': {'type': 'sequence', 'length': {'type': 'inf'}, 'contents': {'type': 'unit'}}}})
do_test_instantiation(c, state_1, {'type': 'sequence', state = do_test_instantiation(c, state, {'type': 'sequence',
'length': {'type': 'number', 'value': 42}, 'length': {'type': 'number', 'value': 42},
'contents': {'type': 'Rational'}}) 'contents': {'type': 'Rational'}})
do_test_instantiation(c, state_1, {'type': 'bitvector', state = do_test_instantiation(c, state, {'type': 'bitvector',
'width': {'type': 'number', 'value': 432}}) 'width': {'type': 'number', 'value': 432}})
do_test_instantiation(c, state_1, {'type': 'variable', state = do_test_instantiation(c, state, {'type': 'variable',
'name': 'Word8'}, 'name': 'Word8'},
{'type': 'bitvector', {'type': 'bitvector',
'width': {'type': 'number', 'value': 8}}) 'width': {'type': 'number', 'value': 8}})
do_test_instantiation(c, state_1, {'type': 'variable', state = do_test_instantiation(c, state, {'type': 'variable',
'name': 'Twenty', 'name': 'Twenty',
'arguments': [{'type': 'Z', 'modulus': {'type': 'number', 'value': 5}}]}, 'arguments': [{'type': 'Z', 'modulus': {'type': 'number', 'value': 5}}]},
{ 'type': 'sequence', { 'type': 'sequence',

48
cryptol-remote-api/run_rpc_tests.sh Executable file
View File

@ -0,0 +1,48 @@
#!/bin/bash
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
pushd $DIR/python
NUM_FAILS=0
echo "Setting up python environment for remote server clients..."
python3 -m venv virtenv
. virtenv/bin/activate
pip install -r requirements.txt
export CRYPTOL_SERVER=$(cabal v2-exec which cryptol-remote-api)
if [[ -x "$CRYPTOL_SERVER" ]]; then
echo "Running cryptol-remote-api tests..."
echo "Using server $CRYPTOL_SERVER"
python3 -m unittest discover tests/cryptol
if [ $? -ne 0 ]; then
NUM_FAILS=$(($NUM_FAILS+1))
fi
else
echo "could not find the cryptol-remote-api via `cabal v2-exec which`"
NUM_FAILS=$(($NUM_FAILS+1))
fi
export CRYPTOL_SERVER=$(cabal v2-exec which cryptol-eval-server)
if [[ -x "$CRYPTOL_SERVER" ]]; then
echo "Running cryptol-eval-server tests..."
echo "Using server $CRYPTOL_SERVER"
python3 -m unittest discover tests/cryptol_eval
if [ $? -ne 0 ]; then
NUM_FAILS=$(($NUM_FAILS+1))
fi
else
echo "could not find the cryptol-eval-server via `cabal v2-exec which`"
NUM_FAILS=$(($NUM_FAILS+1))
fi
popd
if [ $NUM_FAILS -eq 0 ]
then
echo "All RPC tests passed"
exit 0
else
echo "Some RPC tests failed"
exit 1
fi

1
cryptol-remote-api/test/galois-py-toolkit

@ -1 +0,0 @@
Subproject commit 08413dbd48fb601b45b398de73218b9de2b95985

44
cryptol-remote-api/test/run_rpc_tests.sh
View File

@ -1,44 +0,0 @@
#!/bin/bash
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
if [ ! -d "$DIR/galois-py-toolkit/tests" ]; then
echo "ERROR: could not find the python test directory -- is the galois-py-toolkit submodule initialzed?"
exit 1
fi
pushd $DIR/galois-py-toolkit
NUM_FAILS=0
echo "Setting up python environment for remote server clients..."
python3 -m venv virtenv
. virtenv/bin/activate
pip install -r requirements.txt
export CRYPTOL_SERVER=$(cabal v2-exec which cryptol-remote-api)
echo "Running cryptol-remote-api tests..."
echo "Using server $CRYPTOL_SERVER"
python3 -m unittest discover tests/cryptol
if [ $? -ne 0 ]; then
NUM_FAILS=$(($NUM_FAILS+1))
fi
echo "Running cryptol-eval-server tests..."
export CRYPTOL_SERVER=$(cabal v2-exec which cryptol-eval-server)
echo "Using server $CRYPTOL_SERVER"
python3 -m unittest discover tests/cryptol_eval
if [ $? -ne 0 ]; then
NUM_FAILS=$(($NUM_FAILS+1))
fi
popd
if [ $NUM_FAILS -eq 0 ]
then
echo "All RPC tests passed"
exit 0
else
echo "Some RPC tests failed"
exit 1
fi