Skip to content

Commit

Permalink
feat(rpc): make python client compat with python 3.7
Browse files Browse the repository at this point in the history
  • Loading branch information
Andrew Kent committed May 7, 2021
1 parent ac4500a commit 9d319f3
Show file tree
Hide file tree
Showing 11 changed files with 144 additions and 239 deletions.
16 changes: 10 additions & 6 deletions cryptol-remote-api/python/cryptol/bitvector.py
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ def widen(self, n : int) -> 'BV':
Args:
n (int): How many bits wider the returned ``BV`` should be than ``self`` (must be nonnegative).
"""
if not isinstance(n, int) or n < 0:
if not isinstance(n, int) or n < 0: # type: ignore
raise ValueError(f'``widen`` expects a nonnegative integer, but got {n!r}')
else:
return BV(self.__size + n, self.__value)
Expand All @@ -124,7 +124,7 @@ def concat(self, *others : 'BV') -> 'BV':
``others`` in order on the right.
"""
return reduce(lambda acc, b: acc.__concat_single(b), others, self)

@staticmethod
def join(*bs : 'BV') -> 'BV':
"""Concatenate the given ``BV``s in order.
Expand Down Expand Up @@ -178,6 +178,10 @@ def __index__(self) -> int:
"""Equivalent to ``self.value()``."""
return self.__value

def __int__(self) -> int:
"""Equivalent to ``self.value()``."""
return self.__value

def __len__(self) -> int:
"""Equivalent to ``self.size()``."""
return self.__size
Expand All @@ -190,10 +194,10 @@ def __bytes__(self) -> bytes:

def split(self, size : int) -> List['BV']:
"""Split ``self`` into a list of ``BV``s of length ``size``.
:param size: Size of segments to partition ``self`` into (must evently divide ``self.size()``).
"""
if not isinstance(size, int) or size <= 0:
if not isinstance(size, int) or size <= 0: # type: ignore
raise ValueError(f'`size` argument to splits must be a positive integer, got {size!r}')
if not self.size() % size == 0:
raise ValueError(f'{self!r} is not divisible into equal parts of size {size!r}')
Expand All @@ -209,7 +213,7 @@ def popcount(self) -> int:
@staticmethod
def from_bytes(bs : bytes, *, size : Optional[int] =None, byteorder : str ='big') -> 'BV':
"""Convert the given bytes ``bs`` into a ``BV``.
:param bs: Bytes to convert to a ``BV``.
:param size, optional: Desired ``BV``'s size (must be large enough to represent ``bs``). The
default (i.e., ``None``) will result in a ``BV`` of size ``len(bs) * 8``.
Expand Down Expand Up @@ -246,7 +250,7 @@ def with_bit(self, index : int, set_bit : bool) -> 'BV':
def with_bits(self, low : int, bits : 'BV') -> 'BV':
"""Return a ``BV`` identical to ``self`` but with the bits from ``low`` to
``low + bits.size() - 1`` replaced by the bits from ``bits``."""
if not isinstance(low, int) or low < 0 or low >= self.__size:
if not isinstance(low, int) or low < 0 or low >= self.__size: # type: ignore
raise ValueError(f'{low!r} is not a valid low bit index for {self!r}')
elif not isinstance(bits, BV):
raise ValueError(f'Expected a BV but got {bits!r}')
Expand Down
37 changes: 26 additions & 11 deletions cryptol-remote-api/python/cryptol/connection.py
Original file line number Diff line number Diff line change
Expand Up @@ -51,24 +51,39 @@ def connect(command : Optional[str]=None,
if url is not None:
raise ValueError("A Cryptol server URL cannot be specified with a command currently.")
c = CryptolConnection(command, cryptol_path)
elif url is not None:
# User-passed url?
if c is None and url is not None:
c = CryptolConnection(ServerConnection(HttpProcess(url)), cryptol_path)
elif (command := os.getenv('CRYPTOL_SERVER')) is not None and (command := find_executable(command)) is not None:
c = CryptolConnection(command+" socket", cryptol_path=cryptol_path)
elif (url := os.getenv('CRYPTOL_SERVER_URL')) is not None:
c = CryptolConnection(ServerConnection(HttpProcess(url)), cryptol_path)
elif (command := find_executable('cryptol-remote-api')) is not None:
c = CryptolConnection(command+" socket", cryptol_path=cryptol_path)
# Check `CRYPTOL_SERVER` env var if no connection identified yet
if c is None:
command = os.getenv('CRYPTOL_SERVER')
if command is not None:
command = find_executable(command)
if command is not None:
c = CryptolConnection(command+" socket", cryptol_path=cryptol_path)
# Check `CRYPTOL_SERVER_URL` env var if no connection identified yet
if c is None:
url = os.getenv('CRYPTOL_SERVER_URL')
if url is not None:
c = CryptolConnection(ServerConnection(HttpProcess(url)), cryptol_path)
# Check if `cryptol-remote-api` is in the PATH if no connection identified yet
if c is None:
command = find_executable('cryptol-remote-api')
if command is not None:
c = CryptolConnection(command+" socket", cryptol_path=cryptol_path)
# Raise an error if still no connection identified yet
if c is not None:
if reset_server:
CryptolResetServer(c)
return c
else:
raise ValueError(
"""cryptol.connect requires one of the following:",
1) a command to launch a cryptol server is the first positional argument,
2) a URL to connect to a running cryptol server is provided via the `url` keyword argument,
3) the environment variable `CRYPTOL_SERVER` must refer to a valid server executable, or
4) the environment variable `CRYPTOL_SERVER_URL` must refer to the URL of a running cryptol server.""")
if reset_server:
CryptolResetServer(c)
return c



def connect_stdio(command : str, cryptol_path : Optional[str] = None) -> CryptolConnection:
Expand Down Expand Up @@ -102,7 +117,7 @@ class CryptolConnection:
proc: ServerProcess

def __init__(self,
command_or_connection : Union[str, ServerConnection, ServerProcess],
command_or_connection : Union[str, ServerConnection, ServerProcess],
cryptol_path : Optional[str] = None) -> None:
self.most_recent_result = None
if isinstance(command_or_connection, ServerProcess):
Expand Down
83 changes: 41 additions & 42 deletions cryptol-remote-api/python/poetry.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions cryptol-remote-api/python/pyproject.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[tool.poetry]
name = "cryptol"
version = "2.11.0"
version = "2.11.1"
readme = "README.md"
keywords = ["cryptography", "verification"]
description = "Cryptol client for the Cryptol 2.11 RPC server"
Expand All @@ -12,7 +12,7 @@ include = [
]

[tool.poetry.dependencies]
python = "^3.8"
python = ">=3.7.0"
requests = "^2.25.1"
BitVector = "^3.4.9"
argo-client = "0.0.4"
Expand Down
Loading

0 comments on commit 9d319f3

Please sign in to comment.