diff --git a/cryptol-saw-core/cryptol-saw-core.cabal b/cryptol-saw-core/cryptol-saw-core.cabal index 12d571515b..a0d14d15f3 100644 --- a/cryptol-saw-core/cryptol-saw-core.cabal +++ b/cryptol-saw-core/cryptol-saw-core.cabal @@ -67,7 +67,7 @@ executable css hs-source-dirs : css main-is : Main.hs - GHC-options: -Wall -O2 -rtsopts -pgmlc++ + GHC-options: -Wall -O2 -threaded -rtsopts -pgmlc++ extra-libraries: stdc++ test-suite cryptol-saw-core-tc-test @@ -85,3 +85,5 @@ test-suite cryptol-saw-core-tc-test cryptol-saw-core, heredoc >= 0.2, saw-core + + GHC-options: -threaded diff --git a/saw-remote-api/python/poetry.lock b/saw-remote-api/python/poetry.lock index dc13cebedf..950520dfec 100644 --- a/saw-remote-api/python/poetry.lock +++ b/saw-remote-api/python/poetry.lock @@ -1,6 +1,6 @@ [[package]] name = "argo-client" -version = "0.0.4" +version = "0.0.6" description = "A JSON RPC client library." category = "main" optional = false @@ -27,24 +27,27 @@ 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.4" +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 = "cryptol" -version = "2.11.0" +version = "2.11.4" description = "Cryptol client for the Cryptol 2.11 RPC server" category = "main" optional = false -python-versions = "^3.8" +python-versions = ">=3.7.0" develop = true [package.dependencies] -argo-client = "0.0.4" +argo-client = "0.0.6" BitVector = "^3.4.9" requests = "^2.25.1" @@ -54,11 +57,11 @@ url = "../../deps/cryptol/cryptol-remote-api/python" [[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" @@ -86,21 +89,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" @@ -120,7 +123,7 @@ python-versions = "*" [[package]] name = "urllib3" -version = "1.26.5" +version = "1.26.6" description = "HTTP library with thread-safe connection pooling, file post, and more." category = "main" optional = false @@ -134,12 +137,12 @@ socks = ["PySocks (>=1.5.6,!=1.5.7,<2.0)"] [metadata] lock-version = "1.1" python-versions = "^3.8" -content-hash = "79b15e02ed7ee4db325425fa4eaa19d27c640e08bf75fdc9596bb9ea4a2ac506" +content-hash = "d1ec6c507e7a1f0f935f625feec468b2291974cc537e2891f1f0bbfcc70416bb" [metadata.files] argo-client = [ - {file = "argo-client-0.0.4.tar.gz", hash = "sha256:1ce6af1cbc738d08348dcb62d573968da58e2382cb4ea753cc061aa16d45ff6a"}, - {file = "argo_client-0.0.4-py2-none-any.whl", hash = "sha256:74c13e9f3bf5a48eeda847af343bdaf54a950c100496ed3c342a51f5406cf568"}, + {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"}, @@ -148,14 +151,14 @@ 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.4.tar.gz", hash = "sha256:f23667ebe1084be45f6ae0538e4a5a865206544097e4e8bbcacf42cd02a348f3"}, + {file = "charset_normalizer-2.0.4-py3-none-any.whl", hash = "sha256:0c8911edd15d19223366a194a513099a302055a962bca2cec0f54b8b63175d8b"}, ] cryptol = [] 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"}, @@ -186,8 +189,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"}, @@ -227,6 +230,6 @@ typing-extensions = [ {file = "typing_extensions-3.10.0.0.tar.gz", hash = "sha256:50b6f157849174217d0656f99dc82fe932884fb250826c18350e159ec6cdf342"}, ] urllib3 = [ - {file = "urllib3-1.26.5-py2.py3-none-any.whl", hash = "sha256:753a0374df26658f99d826cfe40394a686d05985786d946fbe4165b5148f5a7c"}, - {file = "urllib3-1.26.5.tar.gz", hash = "sha256:a7acd0977125325f516bda9735fa7142b909a8d01e8b2e4c8108d0984e6e0098"}, + {file = "urllib3-1.26.6-py2.py3-none-any.whl", hash = "sha256:39fb8672126159acb139a7718dd10806104dec1e2f0f6c88aab05d17df10c8d4"}, + {file = "urllib3-1.26.6.tar.gz", hash = "sha256:f57b4c16c62fa2760b7e3d97c35b255512fb6b59a259730f36ba32ce9f8e342f"}, ] diff --git a/saw-remote-api/python/pyproject.toml b/saw-remote-api/python/pyproject.toml index dec371a779..472e1d6a3c 100644 --- a/saw-remote-api/python/pyproject.toml +++ b/saw-remote-api/python/pyproject.toml @@ -15,7 +15,7 @@ python = "^3.8" requests = "^2.25.1" BitVector = "^3.4.9" cryptol = { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true } -argo-client = "0.0.4" +argo-client = "~0.0.6" [tool.poetry.dev-dependencies] mypy = "^0.812" diff --git a/saw-remote-api/python/saw_client/__init__.py b/saw-remote-api/python/saw_client/__init__.py index 746b3d4f26..b8fe7628c2 100644 --- a/saw-remote-api/python/saw_client/__init__.py +++ b/saw-remote-api/python/saw_client/__init__.py @@ -1,6 +1,6 @@ from abc import ABCMeta, abstractmethod from dataclasses import dataclass -from typing import List, Optional, Set, Union, Tuple, Any, IO +from typing import List, Optional, Set, Union, Tuple, Any, IO, TextIO import uuid import sys import time @@ -145,7 +145,9 @@ def connect(command: Union[str, ServerConnection, None] = None, cryptol_path: Optional[str] = None, persist: bool = False, url : Optional[str] = None, - reset_server : bool = False) -> None: + reset_server : bool = False, + verify : Union[bool, str] = True, + log_dest : Optional[TextIO] = None) -> None: """ Connect to a (possibly new) Saw server process. @@ -182,7 +184,9 @@ def connect(command: Union[str, ServerConnection, None] = None, command=command, cryptol_path=cryptol_path, persist=persist, - url=url) + url=url, + verify=verify, + log_dest=log_dest) elif reset_server: __designated_connection.reset_server() else: @@ -231,6 +235,13 @@ def disconnect() -> None: __designated_connection = None +def logging(on : bool, *, dest : TextIO = sys.stderr) -> None: + """Whether to log received and transmitted JSON.""" + global __designated_connection + if __designated_connection is not None: + __designated_connection.logging(on=on,dest=dest) + + class View: """An instance of View describes how to (potentially interactively) view or log the results of a verification script, in real-time.""" diff --git a/saw-remote-api/python/saw_client/connection.py b/saw-remote-api/python/saw_client/connection.py index cabfba9022..78e8a75895 100644 --- a/saw-remote-api/python/saw_client/connection.py +++ b/saw-remote-api/python/saw_client/connection.py @@ -1,11 +1,12 @@ from __future__ import annotations import os import signal +import sys from distutils.spawn import find_executable from argo_client.connection import ServerConnection, DynamicSocketProcess, HttpProcess, ManagedProcess from argo_client.interaction import Interaction, Command from .commands import * -from typing import Optional, Union, Any, List +from typing import Optional, Union, Any, List, TextIO # FIXME cryptol_path isn't always used...? def connect(command: Union[str, ServerConnection, None] = None, @@ -13,7 +14,9 @@ def connect(command: Union[str, ServerConnection, None] = None, cryptol_path: Optional[str] = None, persist: bool = False, url : Optional[str] = None, - reset_server : bool = False) -> SAWConnection: + reset_server : bool = False, + verify : Union[bool, str] = True, + log_dest : Optional[TextIO] = None) -> SAWConnection: """ Connect to a (possibly new) Saw server process. @@ -45,15 +48,15 @@ def connect(command: Union[str, ServerConnection, None] = None, if command is not None: if url is not None: raise ValueError("A SAW server URL cannot be specified with a command currently.") - c = SAWConnection(command) + c = SAWConnection(command, log_dest=log_dest) elif url is not None: - c = SAWConnection(ServerConnection(HttpProcess(url))) + c = SAWConnection(ServerConnection(HttpProcess(url, verify=verify)), log_dest=log_dest) elif (command := os.getenv('SAW_SERVER')) is not None and (command := find_executable(command)) is not None: - c = SAWConnection(command+" socket") # SAWConnection(ServerConnection(StdIOProcess(command+" stdio"))) + c = SAWConnection(command+" socket", log_dest=log_dest) # SAWConnection(ServerConnection(StdIOProcess(command+" stdio"))) elif (url := os.getenv('SAW_SERVER_URL')) is not None: - c = SAWConnection(ServerConnection(HttpProcess(url))) + c = SAWConnection(ServerConnection(HttpProcess(url, verify=verify)), log_dest=log_dest) elif (command := find_executable('saw-remote-api')) is not None: - c = SAWConnection(command+" socket") + c = SAWConnection(command+" socket", log_dest=log_dest) else: raise ValueError( """saw.connection.connect requires one of the following:", @@ -75,7 +78,9 @@ class SAWConnection: def __init__(self, command_or_connection: Union[str, ServerConnection], - *, persist: bool = False) -> None: + *, + persist: bool = False, + log_dest : Optional[TextIO] = None) -> None: self.proc = None self.most_recent_result = None self.persist = persist @@ -85,6 +90,9 @@ def __init__(self, else: self.server_connection = command_or_connection + if log_dest: + self.logging(on=True,dest=log_dest) + def reset(self) -> None: """Resets the connection, causing its unique state on the server to be freed (if applicable). @@ -106,11 +114,12 @@ def disconnect(self) -> None: os.kill(pgid, signal.SIGKILL) self.proc = 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) def __del__(self) -> None: # when being deleted, ensure we don't have a lingering state on the server - if self.most_recent_result is not None: - SAWReset(self) if not self.persist: if self.proc and (pid := self.proc.pid()): os.killpg(os.getpgid(pid), signal.SIGKILL) diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal index 16448f6d2f..c8eee5c99f 100644 --- a/saw-remote-api/saw-remote-api.cabal +++ b/saw-remote-api/saw-remote-api.cabal @@ -16,6 +16,11 @@ maintainer: kwf@galois.com category: Network extra-source-files: CHANGELOG.md +common general + ghc-options: + -O2 + -threaded + common warnings ghc-options: -Wall @@ -86,7 +91,7 @@ library SAWServer.VerifyCommon executable saw-remote-api - import: deps, warnings, errors + import: general, deps, warnings, errors main-is: Main.hs build-depends: saw-remote-api -- other-modules: diff --git a/saw-remote-api/scripts/run_rpc_tests.sh b/saw-remote-api/scripts/run_rpc_tests.sh index fab3445afc..e48a2b3824 100755 --- a/saw-remote-api/scripts/run_rpc_tests.sh +++ b/saw-remote-api/scripts/run_rpc_tests.sh @@ -1,5 +1,7 @@ #!/bin/bash +set -euo pipefail + DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" pushd $DIR/../python @@ -11,6 +13,7 @@ function run_test { } echo "Setting up python environment for remote server clients..." +poetry update poetry install echo "Typechecking code with mypy..."