Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[RPC] Clean up to_cryptol interface in cryptoltypes.py #1312

Merged
merged 5 commits into from
Dec 11, 2021
Merged
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 9 additions & 4 deletions cryptol-remote-api/python/cryptol/bitvector.py
Original file line number Diff line number Diff line change
@@ -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).
Expand Down Expand Up @@ -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``.
Expand All @@ -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))
Expand Down
2 changes: 1 addition & 1 deletion cryptol-remote-api/python/cryptol/connection.py
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
135 changes: 52 additions & 83 deletions cryptol-remote-api/python/cryptol/cryptoltypes.py
Original file line number Diff line number Diff line change
Expand Up @@ -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):
Expand All @@ -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: ...
Expand All @@ -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:
Expand All @@ -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]}
Expand Down Expand Up @@ -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
Expand All @@ -185,62 +228,7 @@ def is_plausible_json(val : Any) -> bool:
return False

class CryptolType:
def from_python(self, val : Any) -> JSON:
m-yac marked this conversation as resolved.
Show resolved Hide resolved
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:
Expand All @@ -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):
Expand Down