diff --git a/cryptol-remote-api/python/CHANGELOG.md b/cryptol-remote-api/python/CHANGELOG.md index e9edeb884..4c304229b 100644 --- a/cryptol-remote-api/python/CHANGELOG.md +++ b/cryptol-remote-api/python/CHANGELOG.md @@ -1,5 +1,10 @@ # Revision history for `cryptol` Python package +## 2.11.4 -- 2021-07-22 + +* Add client logging option. See the `log_dest` keyword argument on + `cryptol.connect` or the `logging` method on a `CryptolConnection` object. + ## 2.11.3 -- 2021-07-20 * Removed automatic reset from `CryptolConnection.__del__`. diff --git a/cryptol-remote-api/python/cryptol/connection.py b/cryptol-remote-api/python/cryptol/connection.py index f0fef54e6..13342221a 100644 --- a/cryptol-remote-api/python/cryptol/connection.py +++ b/cryptol-remote-api/python/cryptol/connection.py @@ -2,15 +2,16 @@ from __future__ import annotations import os +import sys from distutils.spawn import find_executable -from typing import Any, List, Optional, Union +from typing import Any, List, Optional, Union, TextIO from typing_extensions import Literal import argo_client.interaction as argo from argo_client.connection import DynamicSocketProcess, ServerConnection, ServerProcess, StdIOProcess, HttpProcess from . import cryptoltypes from . import solver -from .commands import * +from .commands import * def connect(command : Optional[str]=None, @@ -18,7 +19,8 @@ def connect(command : Optional[str]=None, cryptol_path : Optional[str] = None, url : Optional[str] = None, reset_server : bool = False, - verify : Union[bool, str] = True) -> CryptolConnection: + verify : Union[bool, str] = True, + log_dest : Optional[TextIO] = None) -> CryptolConnection: """ Connect to a (possibly new) Cryptol server process. @@ -39,6 +41,9 @@ def connect(command : Optional[str]=None, only has an affect when ``connect`` is called with a ``url`` parameter or when the ``CRYPTOL_SERVER_URL`` environment variable is set. + :param log_dest: A destination to log JSON requests/responses to, e.g. ``log_dest=sys.stderr`` + will print traffic to ``stderr``, ``log_dest=open('foo.log', 'w')`` will log to ``foo.log``, + etc. If no ``command`` or ``url`` parameters are provided, the following are attempted in order: @@ -56,27 +61,27 @@ def connect(command : Optional[str]=None, if command is not None: if url is not None: raise ValueError("A Cryptol server URL cannot be specified with a command currently.") - c = CryptolConnection(command, cryptol_path) + c = CryptolConnection(command, cryptol_path, log_dest=log_dest) # User-passed url? if c is None and url is not None: - c = CryptolConnection(ServerConnection(HttpProcess(url, verify=verify)), cryptol_path) + c = CryptolConnection(ServerConnection(HttpProcess(url, verify=verify)), cryptol_path, log_dest=log_dest) # 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) + c = CryptolConnection(command+" socket", cryptol_path=cryptol_path, log_dest=log_dest) # 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,verify=verify)), cryptol_path) + c = CryptolConnection(ServerConnection(HttpProcess(url,verify=verify)), cryptol_path, log_dest=log_dest) # 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) + c = CryptolConnection(command+" socket", cryptol_path=cryptol_path, log_dest=log_dest) # Raise an error if still no connection identified yet if c is not None: if reset_server: @@ -92,7 +97,9 @@ def connect(command : Optional[str]=None, -def connect_stdio(command : str, cryptol_path : Optional[str] = None) -> CryptolConnection: +def connect_stdio(command : str, + cryptol_path : Optional[str] = None, + log_dest : Optional[TextIO] = None) -> CryptolConnection: """Start a new connection to a new Cryptol server process. :param command: The command to launch the Cryptol server. @@ -103,7 +110,7 @@ def connect_stdio(command : str, cryptol_path : Optional[str] = None) -> Cryptol """ conn = CryptolStdIOProcess(command, cryptol_path=cryptol_path) - return CryptolConnection(conn) + return CryptolConnection(conn, log_dest=log_dest) class CryptolConnection: @@ -120,21 +127,23 @@ class CryptolConnection: sequential state dependencies between commands. """ most_recent_result : Optional[argo.Interaction] - proc: ServerProcess def __init__(self, command_or_connection : Union[str, ServerConnection, ServerProcess], - cryptol_path : Optional[str] = None) -> None: + cryptol_path : Optional[str] = None, + *, + log_dest : Optional[TextIO] = None) -> None: self.most_recent_result = None if isinstance(command_or_connection, ServerProcess): - self.proc = command_or_connection - self.server_connection = ServerConnection(self.proc) + self.server_connection = ServerConnection(command_or_connection) elif isinstance(command_or_connection, str): - self.proc = CryptolDynamicSocketProcess(command_or_connection, cryptol_path=cryptol_path) - self.server_connection = ServerConnection(self.proc) + self.server_connection = ServerConnection(CryptolDynamicSocketProcess(command_or_connection, cryptol_path=cryptol_path)) else: self.server_connection = command_or_connection + if log_dest: + self.logging(on=True,dest=log_dest) + # Currently disabled in (overly?) conservative effort to not accidentally # duplicate and share mutable state. @@ -258,6 +267,10 @@ def reset_server(self) -> None: CryptolResetServer(self) self.most_recent_result = None + def logging(self, on : bool, *, dest : TextIO = sys.stderr) -> None: + """Whether to log received and transmitted JSON.""" + self.server_connection.logging(on=on,dest=dest) + class CryptolDynamicSocketProcess(DynamicSocketProcess): def __init__(self, command: str, *, diff --git a/cryptol-remote-api/python/poetry.lock b/cryptol-remote-api/python/poetry.lock index 26ae178e2..5b7a23131 100644 --- a/cryptol-remote-api/python/poetry.lock +++ b/cryptol-remote-api/python/poetry.lock @@ -1,6 +1,6 @@ [[package]] name = "argo-client" -version = "0.0.5" +version = "0.0.6" description = "A JSON RPC client library." category = "main" optional = false @@ -27,20 +27,23 @@ optional = false python-versions = "*" [[package]] -name = "chardet" -version = "4.0.0" -description = "Universal encoding detector for Python 2 and 3" +name = "charset-normalizer" +version = "2.0.3" +description = "The Real First Universal Charset Detector. Open, modern and actively maintained alternative to Chardet." category = "main" optional = false -python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*" +python-versions = ">=3.5.0" + +[package.extras] +unicode_backport = ["unicodedata2"] [[package]] name = "idna" -version = "2.10" +version = "3.2" description = "Internationalized Domain Names in Applications (IDNA)" category = "main" optional = false -python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*" +python-versions = ">=3.5" [[package]] name = "mypy" @@ -68,21 +71,21 @@ python-versions = "*" [[package]] name = "requests" -version = "2.25.1" +version = "2.26.0" description = "Python HTTP for Humans." category = "main" optional = false -python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*" +python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*, !=3.5.*" [package.dependencies] certifi = ">=2017.4.17" -chardet = ">=3.0.2,<5" -idna = ">=2.5,<3" +charset-normalizer = {version = ">=2.0.0,<2.1.0", markers = "python_version >= \"3\""} +idna = {version = ">=2.5,<4", markers = "python_version >= \"3\""} urllib3 = ">=1.21.1,<1.27" [package.extras] -security = ["pyOpenSSL (>=0.14)", "cryptography (>=1.3.4)"] socks = ["PySocks (>=1.5.6,!=1.5.7)", "win-inet-pton"] +use_chardet_on_py3 = ["chardet (>=3.0.2,<5)"] [[package]] name = "typed-ast" @@ -115,12 +118,12 @@ socks = ["PySocks (>=1.5.6,!=1.5.7,<2.0)"] [metadata] lock-version = "1.1" python-versions = ">=3.7.0" -content-hash = "4fec48a3684b15cd29af1c2f3db5a9033d34a1605ad11aec7babafd2f6bcb1b1" +content-hash = "3234824238003496eaa03c804047b17dd8d7702f178675d1af61587264e55331" [metadata.files] argo-client = [ - {file = "argo-client-0.0.5.tar.gz", hash = "sha256:9b2157f3ea953df812948c27eb762dbe8401bb9d0dc74f49310b6636320a0347"}, - {file = "argo_client-0.0.5-py3-none-any.whl", hash = "sha256:745239a231a0d891088ca2aedebd7ec075faf0f19c2f6b0ceafd252e3eed616d"}, + {file = "argo-client-0.0.6.tar.gz", hash = "sha256:02fe34502eae62ae331e4ce92c290892ea62222eee0e9b79a41de9f795247186"}, + {file = "argo_client-0.0.6-py2-none-any.whl", hash = "sha256:6a153ba3be43573e680c54afeeba86c10b5d060afe2588e4dcac25abdba83ca5"}, ] bitvector = [ {file = "BitVector-3.5.0.tar.gz", hash = "sha256:cac2fbccf11e325115827ed7be03e5fd62615227b0bbf3fa5a18a842a221839c"}, @@ -129,13 +132,13 @@ certifi = [ {file = "certifi-2021.5.30-py2.py3-none-any.whl", hash = "sha256:50b1e4f8446b06f41be7dd6338db18e0990601dce795c2b1686458aa7e8fa7d8"}, {file = "certifi-2021.5.30.tar.gz", hash = "sha256:2bbf76fd432960138b3ef6dda3dde0544f27cbf8546c458e60baf371917ba9ee"}, ] -chardet = [ - {file = "chardet-4.0.0-py2.py3-none-any.whl", hash = "sha256:f864054d66fd9118f2e67044ac8981a54775ec5b67aed0441892edb553d21da5"}, - {file = "chardet-4.0.0.tar.gz", hash = "sha256:0d6f53a15db4120f2b08c94f11e7d93d2c911ee118b6b30a04ec3ee8310179fa"}, +charset-normalizer = [ + {file = "charset-normalizer-2.0.3.tar.gz", hash = "sha256:c46c3ace2d744cfbdebceaa3c19ae691f53ae621b39fd7570f59d14fb7f2fd12"}, + {file = "charset_normalizer-2.0.3-py3-none-any.whl", hash = "sha256:88fce3fa5b1a84fdcb3f603d889f723d1dd89b26059d0123ca435570e848d5e1"}, ] idna = [ - {file = "idna-2.10-py2.py3-none-any.whl", hash = "sha256:b97d804b1e9b523befed77c48dacec60e6dcb0b5391d57af6a65a312a90648c0"}, - {file = "idna-2.10.tar.gz", hash = "sha256:b307872f855b18632ce0c21c5e45be78c0ea7ae4c15c828c20788b26921eb3f6"}, + {file = "idna-3.2-py3-none-any.whl", hash = "sha256:14475042e284991034cb48e06f6851428fb14c4dc953acd9be9a5e95c7b6dd7a"}, + {file = "idna-3.2.tar.gz", hash = "sha256:467fbad99067910785144ce333826c71fb0e63a425657295239737f7ecd125f3"}, ] mypy = [ {file = "mypy-0.812-cp35-cp35m-macosx_10_9_x86_64.whl", hash = "sha256:a26f8ec704e5a7423c8824d425086705e381b4f1dfdef6e3a1edab7ba174ec49"}, @@ -166,8 +169,8 @@ mypy-extensions = [ {file = "mypy_extensions-0.4.3.tar.gz", hash = "sha256:2d82818f5bb3e369420cb3c4060a7970edba416647068eb4c5343488a6c604a8"}, ] requests = [ - {file = "requests-2.25.1-py2.py3-none-any.whl", hash = "sha256:c210084e36a42ae6b9219e00e48287def368a26d03a048ddad7bfee44f75871e"}, - {file = "requests-2.25.1.tar.gz", hash = "sha256:27973dd4a904a4f13b263a19c866c13b92a39ed1c964655f025f3f8d3d75b804"}, + {file = "requests-2.26.0-py2.py3-none-any.whl", hash = "sha256:6c1246513ecd5ecd4528a0906f910e8f0f9c6b8ec72030dc9fd154dc1a6efd24"}, + {file = "requests-2.26.0.tar.gz", hash = "sha256:b8aa58f8cf793ffd8782d3d8cb19e66ef36f7aba4353eec859e74678b01b07a7"}, ] typed-ast = [ {file = "typed_ast-1.4.3-cp35-cp35m-manylinux1_i686.whl", hash = "sha256:2068531575a125b87a41802130fa7e29f26c09a2833fea68d9a40cf33902eba6"}, diff --git a/cryptol-remote-api/python/pyproject.toml b/cryptol-remote-api/python/pyproject.toml index 432db26c8..9d3cccb38 100644 --- a/cryptol-remote-api/python/pyproject.toml +++ b/cryptol-remote-api/python/pyproject.toml @@ -1,6 +1,6 @@ [tool.poetry] name = "cryptol" -version = "2.11.3" +version = "2.11.4" readme = "README.md" keywords = ["cryptography", "verification"] description = "Cryptol client for the Cryptol 2.11 RPC server" @@ -15,7 +15,7 @@ include = [ python = ">=3.7.0" requests = "^2.25.1" BitVector = "^3.4.9" -argo-client = "0.0.5" +argo-client = "0.0.6" [tool.poetry.dev-dependencies] mypy = "^0.812" diff --git a/cryptol-remote-api/python/tests/cryptol/test_basics.py b/cryptol-remote-api/python/tests/cryptol/test_basics.py index f95c050bc..e93a94214 100644 --- a/cryptol-remote-api/python/tests/cryptol/test_basics.py +++ b/cryptol-remote-api/python/tests/cryptol/test_basics.py @@ -1,16 +1,9 @@ import unittest from pathlib import Path -import os -from pathlib import Path -import subprocess -import time import unittest -import signal -from distutils.spawn import find_executable +import io import cryptol -import argo_client.connection as argo import cryptol.cryptoltypes -from cryptol import solver from cryptol.bitvector import BV from BitVector import * #type: ignore @@ -36,10 +29,49 @@ def test_extend_search_path(self): c = self.c c.extend_search_path(str(Path('tests','cryptol','test-files', 'test-subdir'))) - c.load_module('Bar') + c.load_module('Bar').result() ans1 = c.evaluate_expression("theAnswer").result() ans2 = c.evaluate_expression("id theAnswer").result() self.assertEqual(ans1, ans2) + def test_logging(self): + c = self.c + c.extend_search_path(str(Path('tests','cryptol','test-files', 'test-subdir'))) + c.load_module('Bar').result() + + log_buffer = io.StringIO() + c.logging(on=True, dest=log_buffer) + _ = c.evaluate_expression("theAnswer").result() + contents = log_buffer.getvalue() + print(f'CONTENTS: {contents}', file=sys.stderr) + + self.assertEqual(len(contents.strip().splitlines()), 2) + + _ = c.evaluate_expression("theAnswer").result() + + +class BasicLoggingServerTests(unittest.TestCase): + # Connection to cryptol + c = None + log_buffer = None + + @classmethod + def setUpClass(self): + self.log_buffer = io.StringIO() + self.c = cryptol.connect(verify=False, log_dest = self.log_buffer) + + @classmethod + def tearDownClass(self): + if self.c: + self.c.reset() + + def test_logging(self): + c = self.c + c.extend_search_path(str(Path('tests','cryptol','test-files', 'test-subdir'))) + c.load_module('Bar') + _ = c.evaluate_expression("theAnswer").result() + + self.assertEqual(len(self.log_buffer.getvalue().splitlines()), 6) + if __name__ == "__main__": unittest.main() diff --git a/cryptol-remote-api/run_rpc_tests.sh b/cryptol-remote-api/run_rpc_tests.sh index df46cbbfb..e9e24b057 100755 --- a/cryptol-remote-api/run_rpc_tests.sh +++ b/cryptol-remote-api/run_rpc_tests.sh @@ -23,6 +23,7 @@ get_server() { } echo "Setting up python environment for remote server clients..." +poetry update poetry install echo "Typechecking code with mypy..." diff --git a/deps/argo b/deps/argo index 2481c4250..05cbaf7e8 160000 --- a/deps/argo +++ b/deps/argo @@ -1 +1 @@ -Subproject commit 2481c42506c46be8b6562ab9dcef99fe85a54e5f +Subproject commit 05cbaf7e82f6b4b9badd637e424871697b860844