diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index e8a52eafbf9..c0e787030f4 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -19,7 +19,7 @@ from psutil import Process -from ..utils import FrozenDict, check_dir_path, check_file_path, filter_none, hash_str, run_process +from ..utils import FrozenDict, check_dir_path, check_file_path, filter_none, run_process from . import manip from .prelude import SORT_GENERATED_TOP_CELL from .syntax import And, Equals, EVar, kore_term @@ -69,7 +69,7 @@ def __exit__(self, *args: Any) -> None: def close(self) -> None: ... @abstractmethod - def command(self, bug_report_id: str, uid: str, bug_report_request: str) -> list[str]: ... + def command(self, req_name: str, bug_report_request: str) -> list[str]: ... @abstractmethod def description(self) -> str: ... @@ -117,7 +117,7 @@ def close(self) -> None: self._file.close() self._sock.close() - def command(self, bug_report_id: str, uid: str, bug_report_request: str) -> list[str]: + def command(self, req_name: str, bug_report_request: str) -> list[str]: return [ 'cat', bug_report_request, @@ -127,7 +127,7 @@ def command(self, bug_report_id: str, uid: str, bug_report_request: str) -> list self._host, str(self._port), '>', - f'rpc_{bug_report_id}/{uid:03}_actual.json', + f'{req_name}_actual.json', ] def request(self, req: str) -> str: @@ -154,7 +154,7 @@ def __init__(self, host: str, port: int, *, timeout: int | None = None): def close(self) -> None: pass - def command(self, bug_report_id: str, uid: str, bug_report_request: str) -> list[str]: + def command(self, req_name: str, bug_report_request: str) -> list[str]: return [ 'curl', '-X', @@ -165,7 +165,7 @@ def command(self, bug_report_id: str, uid: str, bug_report_request: str) -> list '@' + bug_report_request, 'http://' + self._host + ':' + str(self._port), '>', - f'rpc_{bug_report_id}/{uid:03}_actual.json', + f'{req_name}_actual.json', ] def request(self, req: str) -> str: @@ -259,7 +259,7 @@ class JsonRpcClient(ContextManager['JsonRpcClient']): _transport: Transport _req_id: int _bug_report: BugReport | None - _bug_report_id: str + _bug_report_id: str | None def __init__( self, @@ -279,7 +279,15 @@ def __init__( raise AssertionError() self._req_id = 1 self._bug_report = bug_report - self._bug_report_id = bug_report_id if bug_report_id is not None else str(id(self)) + self._bug_report_id = bug_report_id + from traceback import format_stack + + print(self.client_id) + print('\n'.join(format_stack())) + + @property + def client_id(self) -> str: + return str(id(self)) def __enter__(self) -> JsonRpcClient: return self @@ -291,24 +299,25 @@ def close(self) -> None: self._transport.close() def request(self, method: str, **params: Any) -> dict[str, Any]: - # Generate unique ID regardless of different clients, repeated requests from the same client, etc. - uid = hash_str((id(self), self._req_id)) + old_id = self._req_id self._req_id += 1 payload = { 'jsonrpc': self._JSON_RPC_VERSION, - 'id': uid, + 'id': old_id, 'method': method, 'params': params, } server_addr = self._transport.description() - _LOGGER.info(f'Sending request to {server_addr}: {uid} - {method}') + _LOGGER.info(f'Sending request to {server_addr}: {old_id} - {method}') req = json.dumps(payload) + base_name = self._bug_report_id if self._bug_report_id is not None else 'kore_rpc' + req_name = f'{base_name}/{self.client_id}/{old_id:03}' if self._bug_report: - bug_report_request = f'rpc_{self._bug_report_id}/{uid:03}_request.json' + bug_report_request = f'{req_name}_request.json' self._bug_report.add_file_contents(req, Path(bug_report_request)) - self._bug_report.add_command(self._transport.command(self._bug_report_id, uid, bug_report_request)) + self._bug_report.add_command(self._transport.command(req_name, bug_report_request)) _LOGGER.debug(f'Sending request to {server_addr}: {req}') resp = self._transport.request(req) @@ -317,23 +326,23 @@ def request(self, method: str, **params: Any) -> dict[str, Any]: _LOGGER.debug(f'Received response from {server_addr}: {resp}') if self._bug_report: - bug_report_response = f'rpc_{self._bug_report_id}/{uid:03}_response.json' + bug_report_response = f'{req_name}_response.json' self._bug_report.add_file_contents(resp, Path(bug_report_response)) self._bug_report.add_command( [ 'diff', '-b', '-s', - f'rpc_{self._bug_report_id}/{uid:03}_actual.json', - f'rpc_{self._bug_report_id}/{uid:03}_response.json', + f'{req_name}_actual.json', + f'{req_name}_response.json', ] ) data = json.loads(resp) self._check(data) - assert data['id'] == uid + assert data['id'] == old_id - _LOGGER.info(f'Received response from {server_addr}: {uid} - {method}') + _LOGGER.info(f'Received response from {server_addr}: {old_id} - {method}') return data['result'] @staticmethod