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

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__`.

cryptol-remote-api/python/cryptol/connection.py

@@ -2,23 +2,25 @@
 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,
             *,
             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, *,

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"

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()

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..."