Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

rpc dep tweaks #1429

Merged
merged 3 commits into from
Aug 24, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion cryptol-saw-core/cryptol-saw-core.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -85,3 +85,5 @@ test-suite cryptol-saw-core-tc-test
cryptol-saw-core,
heredoc >= 0.2,
saw-core

GHC-options: -threaded
59 changes: 31 additions & 28 deletions saw-remote-api/python/poetry.lock

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

2 changes: 1 addition & 1 deletion saw-remote-api/python/pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
17 changes: 14 additions & 3 deletions saw-remote-api/python/saw_client/__init__.py
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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."""
Expand Down
29 changes: 19 additions & 10 deletions saw-remote-api/python/saw_client/connection.py
Original file line number Diff line number Diff line change
@@ -1,19 +1,22 @@
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,
*,
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.

Expand Down Expand Up @@ -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:",
Expand All @@ -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
Expand All @@ -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).

Expand All @@ -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)
Expand Down
7 changes: 6 additions & 1 deletion saw-remote-api/saw-remote-api.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,11 @@ maintainer: [email protected]
category: Network
extra-source-files: CHANGELOG.md

common general
ghc-options:
-O2
-threaded

common warnings
ghc-options:
-Wall
Expand Down Expand Up @@ -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:
Expand Down
3 changes: 3 additions & 0 deletions saw-remote-api/scripts/run_rpc_tests.sh
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
#!/bin/bash

set -euo pipefail

DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"

pushd $DIR/../python
Expand All @@ -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..."
Expand Down