From faa4e7850452e37b3e3f724672edef9d7bd8a026 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 9 Dec 2021 14:04:15 -0800 Subject: [PATCH 1/5] clean up interface for converting to JSON in cryptoltypes --- .../python/cryptol/connection.py | 2 +- .../python/cryptol/cryptoltypes.py | 135 +++++++----------- 2 files changed, 53 insertions(+), 84 deletions(-) diff --git a/cryptol-remote-api/python/cryptol/connection.py b/cryptol-remote-api/python/cryptol/connection.py index e78904327..51d565e48 100644 --- a/cryptol-remote-api/python/cryptol/connection.py +++ b/cryptol-remote-api/python/cryptol/connection.py @@ -469,7 +469,7 @@ def __init__(self, command: str, *, # current_expr = self.name # found_args = [] # while len(arg_types) > 0 and len(remaining_args) > 0: -# found_args.append(arg_types[0].from_python(remaining_args[0])) +# found_args.append(to_cryptol(remaining_args[0])) # current_expr = {'expression': 'call', 'function': self.name, 'arguments': found_args} # ty = self.connection.check_type(current_expr).result() # current_type = cryptoltypes.to_schema(ty) diff --git a/cryptol-remote-api/python/cryptol/cryptoltypes.py b/cryptol-remote-api/python/cryptol/cryptoltypes.py index 18bf88230..cba3b1868 100644 --- a/cryptol-remote-api/python/cryptol/cryptoltypes.py +++ b/cryptol-remote-api/python/cryptol/cryptoltypes.py @@ -54,7 +54,7 @@ def parenthesize(s : str) -> str: JSON = Union[bool, int, float, str, Dict, typing.Tuple, List] class CryptolJSON(Protocol): - def __to_cryptol__(self, ty : CryptolType) -> JSON: ... + def __to_cryptol__(self) -> JSON: ... def __to_cryptol_str__(self) -> str: ... class CryptolCode(metaclass=ABCMeta): @@ -65,7 +65,7 @@ def __call__(self, *others : CryptolJSON) -> CryptolCode: raise ValueError("Argument to __call__ on CryptolCode is not CryptolJSON") @abstractmethod - def __to_cryptol__(self, ty : CryptolType) -> JSON: ... + def __to_cryptol__(self) -> JSON: ... @abstractmethod def __to_cryptol_str__(self) -> str: ... @@ -77,7 +77,7 @@ class CryptolLiteral(CryptolCode): def __init__(self, code : str) -> None: self._code = code - def __to_cryptol__(self, ty : CryptolType) -> JSON: + def __to_cryptol__(self) -> JSON: return self._code def __to_cryptol_str__(self) -> str: @@ -94,7 +94,7 @@ def __init__(self, rator : CryptolJSON, *rands : CryptolJSON) -> None: self._rator = rator self._rands = rands - def __to_cryptol__(self, ty : CryptolType) -> JSON: + def __to_cryptol__(self) -> JSON: return {'expression': 'call', 'function': to_cryptol(self._rator), 'arguments': [to_cryptol(arg) for arg in self._rands]} @@ -163,11 +163,54 @@ def __repr__(self) -> str: return f"Logic({self.subject!r})" -def to_cryptol(val : Any, cryptol_type : Optional[CryptolType] = None) -> JSON: - if cryptol_type is not None: - return cryptol_type.from_python(val) +def to_cryptol(val : Any) -> JSON: + if isinstance(val, bool): + return val + elif isinstance(val, tuple) and val == (): + return {'expression': 'unit'} + elif isinstance(val, tuple): + return {'expression': 'tuple', + 'data': [to_cryptol(x) for x in val]} + elif isinstance(val, dict): + return {'expression': 'record', + 'data': {k : to_cryptol(val[k]) + if isinstance(k, str) + else fail_with (TypeError("Record keys must be strings")) + for k in val}} + elif isinstance(val, int): + return val + elif isinstance(val, list): + return {'expression': 'sequence', + 'data': [to_cryptol(v) for v in val]} + elif isinstance(val, bytes) or isinstance(val, bytearray): + return {'expression': 'bits', + 'encoding': 'base64', + 'width': 8 * len(val), + 'data': base64.b64encode(val).decode('ascii')} + elif isinstance(val, BitVector.BitVector): + n = int(val) + byte_width = ceil(n.bit_length()/8) + return {'expression': 'bits', + 'encoding': 'base64', + 'width': val.length(), # N.B. original length, not padded + 'data': base64.b64encode(n.to_bytes(byte_width,'big')).decode('ascii')} + elif isinstance(val, BV): + return {'expression': 'bits', + 'encoding': 'hex', + 'width': val.size(), # N.B. original length, not padded + 'data': val.hex()[2:]} + elif isinstance(val, OpaqueValue): + return {'expression': 'variable', + 'identifier': val.identifier} + elif hasattr(val, '__to_cryptol__'): + code = val.__to_cryptol__() + if is_plausible_json(code): + # the call to is_plausible_json ensures this cast is OK + return cast(JSON, code) + else: + raise ValueError(f"Improbable JSON from __to_cryptol__: {val!r} gave {code!r}") else: - return CryptolType().from_python(val) + raise TypeError("Unsupported value: " + str(val)) def fail_with(exn : Exception) -> NoReturn: raise exn @@ -185,62 +228,7 @@ def is_plausible_json(val : Any) -> bool: return False class CryptolType: - def from_python(self, val : Any) -> JSON: - if hasattr(val, '__to_cryptol__'): - code = val.__to_cryptol__(self) - if is_plausible_json(code): - # the call to is_plausible_json ensures this cast is OK - return cast(JSON, code) - else: - raise ValueError(f"Improbable JSON from __to_cryptol__: {val!r} gave {code!r}") - # if isinstance(code, CryptolCode): - # return self.convert(code) - # else: - # raise ValueError(f"Expected Cryptol code from __to_cryptol__ on {val!r}, but got {code!r}.") - else: - return self.convert(val) - - def convert(self, val : Any) -> JSON: - if isinstance(val, bool): - return val - elif isinstance(val, tuple) and val == (): - return {'expression': 'unit'} - elif isinstance(val, tuple): - return {'expression': 'tuple', - 'data': [to_cryptol(x) for x in val]} - elif isinstance(val, dict): - return {'expression': 'record', - 'data': {k : to_cryptol(val[k]) - if isinstance(k, str) - else fail_with (TypeError("Record keys must be strings")) - for k in val}} - elif isinstance(val, int): - return val - elif isinstance(val, list): - return {'expression': 'sequence', - 'data': [to_cryptol(v) for v in val]} - elif isinstance(val, bytes) or isinstance(val, bytearray): - return {'expression': 'bits', - 'encoding': 'base64', - 'width': 8 * len(val), - 'data': base64.b64encode(val).decode('ascii')} - elif isinstance(val, BitVector.BitVector): - n = int(val) - byte_width = ceil(n.bit_length()/8) - return {'expression': 'bits', - 'encoding': 'base64', - 'width': val.length(), # N.B. original length, not padded - 'data': base64.b64encode(n.to_bytes(byte_width,'big')).decode('ascii')} - elif isinstance(val, BV): - return {'expression': 'bits', - 'encoding': 'hex', - 'width': val.size(), # N.B. original length, not padded - 'data': val.hex()[2:]} - elif isinstance(val, OpaqueValue): - return {'expression': 'variable', - 'identifier': val.identifier} - else: - raise TypeError("Unsupported value: " + str(val)) + pass class Var(CryptolType): def __init__(self, name : str, kind : CryptolKind) -> None: @@ -267,25 +255,6 @@ def __init__(self, width : CryptolType) -> None: def __repr__(self) -> str: return f"Bitvector({self.width!r})" - def convert(self, val : Any) -> Any: - # XXX figure out what to do when width is not evenly divisible by 8 - if isinstance(val, int): - w = eval_numeric(self.width, None) - if w is not None: - return self.convert(int.to_bytes(val, int(w / 8), 'big', signed=True)) - else: - raise ValueError(f"Insufficent type information to serialize int as bitvector") - elif isinstance(val, bytearray) or isinstance(val, bytes): - return {'expression': 'bits', - 'encoding': 'base64', - 'width': eval_numeric(self.width, 8 * len(val)), - 'data': base64.b64encode(val).decode('ascii')} - elif isinstance(val, BitVector.BitVector): - return CryptolType.convert(self, val) - elif isinstance(val, BV): - return CryptolType.convert(self, val) - else: - raise ValueError(f"Not supported as bitvector: {val!r}") def eval_numeric(t : Any, default : A) -> Union[int, A]: if isinstance(t, Num): From 780c5728581c47fb0226cb689f0d7172c98a03ce Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Thu, 9 Dec 2021 14:29:38 -0800 Subject: [PATCH 2/5] allow bytearrays in BV.from_bytes --- cryptol-remote-api/python/cryptol/bitvector.py | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/cryptol-remote-api/python/cryptol/bitvector.py b/cryptol-remote-api/python/cryptol/bitvector.py index 424645ab6..ec9e3111b 100644 --- a/cryptol-remote-api/python/cryptol/bitvector.py +++ b/cryptol-remote-api/python/cryptol/bitvector.py @@ -1,8 +1,11 @@ from functools import reduce from typing import Any, List, Union, Optional, overload +from typing_extensions import Literal from BitVector import BitVector #type: ignore +ByteOrder = Union[Literal['little'], Literal['big']] + class BV: """A class representing a cryptol bit vector (i.e., a sequence of bits). @@ -211,7 +214,7 @@ def popcount(self) -> int: return bin(self).count("1") @staticmethod - def from_bytes(bs : bytes, *, size : Optional[int] =None, byteorder : str ='big') -> 'BV': + def from_bytes(bs : Union[bytes,bytearray], *, size : Optional[int] = None, byteorder : ByteOrder = 'big') -> 'BV': """Convert the given bytes ``bs`` into a ``BV``. :param bs: Bytes to convert to a ``BV``. @@ -221,11 +224,13 @@ def from_bytes(bs : bytes, *, size : Optional[int] =None, byteorder : str ='big' ``'big'``, ``little`` being the other acceptable value. Equivalent to the ``byteorder`` parameter from Python's ``int.from_bytes``.""" - if not isinstance(bs, bytes): - raise ValueError("from_bytes given not bytes value: {bs!r}") + if isinstance(bs, bytearray): + bs = bytes(bs) + elif not isinstance(bs, bytes): + raise ValueError(f"from_bytes given not a bytearray or bytes value: {bs!r}") if not byteorder == 'little' and not byteorder == 'big': - raise ValueError("from_bytes given not bytes value: {bs!r}") + raise ValueError("byteorder must be either 'little' or 'big'") if size == None: return BV(len(bs) * 8, int.from_bytes(bs, byteorder=byteorder)) From 565a48a2c7adfd56e238f9676b10e287556f74dc Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Fri, 10 Dec 2021 14:41:21 -0800 Subject: [PATCH 3/5] add deprecation errors to CryptolType.from_python and .convert --- cryptol-remote-api/python/cryptol/cryptoltypes.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/cryptol-remote-api/python/cryptol/cryptoltypes.py b/cryptol-remote-api/python/cryptol/cryptoltypes.py index cba3b1868..cba680022 100644 --- a/cryptol-remote-api/python/cryptol/cryptoltypes.py +++ b/cryptol-remote-api/python/cryptol/cryptoltypes.py @@ -228,7 +228,11 @@ def is_plausible_json(val : Any) -> bool: return False class CryptolType: - pass + def from_python(self, val : Any) -> NoReturn: + raise Exception("CryptolType.from_python is deprecated, use to_cryptol") + + def convert(self, val : Any) -> NoReturn: + raise Exception("CryptolType.convert is deprecated, use to_cryptol") class Var(CryptolType): def __init__(self, name : str, kind : CryptolKind) -> None: From 554f53124db118ec319dea2bacaa540b9c369bed Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Fri, 10 Dec 2021 14:45:36 -0800 Subject: [PATCH 4/5] add docstring to to_cryptol, remove eval_numeric --- cryptol-remote-api/python/cryptol/cryptoltypes.py | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/cryptol-remote-api/python/cryptol/cryptoltypes.py b/cryptol-remote-api/python/cryptol/cryptoltypes.py index cba680022..70a5294af 100644 --- a/cryptol-remote-api/python/cryptol/cryptoltypes.py +++ b/cryptol-remote-api/python/cryptol/cryptoltypes.py @@ -164,6 +164,8 @@ def __repr__(self) -> str: def to_cryptol(val : Any) -> JSON: + """Convert a ``CryptolJSON`` value, a Python value representing a Cryptol + term, or any combination of the two to Cryptol JSON.""" if isinstance(val, bool): return val elif isinstance(val, tuple) and val == (): @@ -260,13 +262,6 @@ def __repr__(self) -> str: return f"Bitvector({self.width!r})" -def eval_numeric(t : Any, default : A) -> Union[int, A]: - if isinstance(t, Num): - return t.number - else: - return default - - class Num(CryptolType): def __init__(self, number : int) -> None: self.number = number From 6628bcd36d69d7cfa155c0099ddb837d3fcee483 Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Fri, 10 Dec 2021 14:57:06 -0800 Subject: [PATCH 5/5] update CHANGELOG --- cryptol-remote-api/python/CHANGELOG.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/cryptol-remote-api/python/CHANGELOG.md b/cryptol-remote-api/python/CHANGELOG.md index ad7978fc1..dcc499499 100644 --- a/cryptol-remote-api/python/CHANGELOG.md +++ b/cryptol-remote-api/python/CHANGELOG.md @@ -4,8 +4,9 @@ * Add an interface for Cryptol quasiquotation using an f-string-like syntax, see `tests/cryptol/test_quoting` for some examples. - -* Fixed a bug with the client's `W4_ABC` solver, added a `W4_ANY` solver. +* Fix a bug with the client's `W4_ABC` solver, add a `W4_ANY` solver. +* Deprecate `CryptolType.from_python` and `CryptolType.convert` +* Remove `CryptolType` arguments to `to_cryptol` and `__to_cryptol__` ## 2.12.0 -- 2021-11-19