mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
feat(rpc): logging for server and client (#1251)
* feat(rpc): logging for server and client * fix: CryptolConnection dflt val for proc * fix: activate logging on connection, not process * chore: remove unnecessary proc field
This commit is contained in:
parent
e6f80ed50a
commit
8e7e04726c
@ -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__`.
|
||||
|
@ -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 @@ class CryptolConnection:
|
||||
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, *,
|
||||
|
47
cryptol-remote-api/python/poetry.lock
generated
47
cryptol-remote-api/python/poetry.lock
generated
@ -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"},
|
||||
|
@ -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"
|
||||
|
@ -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 @@ class BasicServerTests(unittest.TestCase):
|
||||
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()
|
||||
|
@ -23,6 +23,7 @@ get_server() {
|
||||
}
|
||||
|
||||
echo "Setting up python environment for remote server clients..."
|
||||
poetry update
|
||||
poetry install
|
||||
|
||||
echo "Typechecking code with mypy..."
|
||||
|
2
deps/argo
vendored
2
deps/argo
vendored
@ -1 +1 @@
|
||||
Subproject commit 2481c42506c46be8b6562ab9dcef99fe85a54e5f
|
||||
Subproject commit 05cbaf7e82f6b4b9badd637e424871697b860844
|
Loading…
Reference in New Issue
Block a user