Fix bug report request IDs being reset when using multiple KoreClients
#4480
Conversation
…ate ID of request
pyk/src/pyk/kore/rpc.py
Outdated
| @@ -291,23 +291,24 @@ def close(self) -> None: | |||
| self._transport.close() | |||
|
|
|||
| def request(self, method: str, **params: Any) -> dict[str, Any]: | |||
| old_id = self._req_id | |||
| # Generate unique ID regardless of different clients, repeated requests from the same client, etc. | |||
| uid = hash_str((id(self), self._req_id)) | |||
There was a problem hiding this comment.
Does this mean that the requests will no longer be linear? If they are not, is there any way of establishing the correct order in the bug reports?
There was a problem hiding this comment.
My understanding is that the order is determined by the ordering of the commands files, which are bash scripts that refer to the request files, and those are still named using a counter. This would only be changing the names of the request files (and the IDs of the requests referred to in the requests themselves)
See:
Line 541 in 0cfdcda
pyk/src/pyk/kore/rpc.py
Outdated
| self._bug_report.add_file_contents(req, Path(bug_report_request)) | ||
| self._bug_report.add_command(self._transport.command(self._bug_report_id, old_id, bug_report_request)) | ||
| self._bug_report.add_command(self._transport.command(req_name, bug_report_request)) |
There was a problem hiding this comment.
I wonder, is it possible to pull all this logic into Transport (and its subclasses)? Then command and client_id can become private on Transport.
pyk/src/pyk/kore/rpc.py
Outdated
| def __init__(self, bug_report_id: str | None = None, bug_report: BugReport | None = None) -> None: | ||
| self._bug_report_id = bug_report_id | ||
| self._bug_report = bug_report |
There was a problem hiding this comment.
| def __init__(self, bug_report_id: str | None = None, bug_report: BugReport | None = None) -> None: | |
| self._bug_report_id = bug_report_id | |
| self._bug_report = bug_report | |
| def __init__(self, bug_report: BugReport | None = None, bug_report_id: str | None = None) -> None: | |
| self._bug_report = bug_report | |
| self._bug_report_id = bug_report_id |
There was a problem hiding this comment.
Is it valid to have a bug_report_id but not a bug_report? If it isn't, ValueError should be raised when it happens.
pyk/src/pyk/kore/rpc.py
Outdated
| @@ -87,7 +123,8 @@ class SingleSocketTransport(Transport): | |||
| _sock: socket.socket | |||
| _file: TextIO | |||
|
|
|||
| def __init__(self, host: str, port: int, *, timeout: int | None = None): | |||
| def __init__(self, host: str, port: int, *, timeout: int | None = None, **kwargs: Any): | |||
| super().__init__(**kwargs) | |||
There was a problem hiding this comment.
Consider just explicitly listing kwargs here.
Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
…ithout bug report, etc.
…ication/k into noah/bug-report-fix
Fixes #4478.
We were generating response json files for bug reports in a non-unique way so that when we have multiple
JsonRpcClients they will overwrite each other's response files. This change ensures that each client will have a unique ID associated which will be included in the path of the response files generated by that client so there are no more name conflicts.Tested generating bug reports for
kontrol proveandkevm prove.