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.

Sign up for GitHub

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

Fix bug report request IDs being reset when using multiple KoreClients #4480

Merged
merged 18 commits into from
Jun 27, 2024
Merged

Fix bug report request IDs being reset when using multiple KoreClients #4480

Changes from 3 commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
b582f14
Use hash of request contents, _req_id counter, and client ID to gener…
nwatson22 Jun 25, 2024
6eedcbc
Remove unneeded components from uid calculation
nwatson22 Jun 25, 2024
3699701
Merge branch 'develop' into noah/bug-report-fix
nwatson22 Jun 25, 2024
c4f5058
Change file structure of bug report, don't use hashing
nwatson22 Jun 26, 2024
d88c70e
Merge branch 'noah/bug-report-fix' of https://github.com/runtimeverif…
nwatson22 Jun 26, 2024
1a136a6
Remove debug code
nwatson22 Jun 26, 2024
bb8ef9f
Merge branch 'develop' into noah/bug-report-fix
nwatson22 Jun 26, 2024
1d6a8ed
Merge branch 'develop' into noah/bug-report-fix
nwatson22 Jun 27, 2024
25398bb
Move bug report generation to the Transport level
nwatson22 Jun 27, 2024
cc401c9
Fix test
nwatson22 Jun 27, 2024
6c16110
Rename methods
nwatson22 Jun 27, 2024
067319b
Make description private
nwatson22 Jun 27, 2024
f64c1fd
Merge branch 'develop' into noah/bug-report-fix
nwatson22 Jun 27, 2024
ab53d2e
Merge branch 'develop' into noah/bug-report-fix
rv-jenkins Jun 27, 2024
e00a875
Update pyk/src/pyk/kore/rpc.py
nwatson22 Jun 27, 2024
8e3dd95
explicitly list args for Transport, warn when passing bug report ID w…
nwatson22 Jun 27, 2024
6a3bc38
Merge branch 'noah/bug-report-fix' of https://github.com/runtimeverif…
nwatson22 Jun 27, 2024
fb6baf7
Merge branch 'develop' into noah/bug-report-fix
nwatson22 Jun 27, 2024
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
33 changes: 17 additions & 16 deletions pyk/src/pyk/kore/rpc.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@

from psutil import Process

from ..utils import FrozenDict, check_dir_path, check_file_path, filter_none, run_process
from ..utils import FrozenDict, check_dir_path, check_file_path, filter_none, hash_str, run_process
from . import manip
from .prelude import SORT_GENERATED_TOP_CELL
from .syntax import And, Equals, EVar, kore_term
Expand Down Expand Up @@ -69,7 +69,7 @@ def __exit__(self, *args: Any) -> None:
def close(self) -> None: ...

@abstractmethod
def command(self, bug_report_id: str, old_id: int, bug_report_request: str) -> list[str]: ...
def command(self, bug_report_id: str, uid: str, bug_report_request: str) -> list[str]: ...

@abstractmethod
def description(self) -> str: ...
Expand Down Expand Up @@ -117,7 +117,7 @@ def close(self) -> None:
self._file.close()
self._sock.close()

def command(self, bug_report_id: str, old_id: int, bug_report_request: str) -> list[str]:
def command(self, bug_report_id: str, uid: str, bug_report_request: str) -> list[str]:
return [
'cat',
bug_report_request,
Expand All @@ -127,7 +127,7 @@ def command(self, bug_report_id: str, old_id: int, bug_report_request: str) -> l
self._host,
str(self._port),
'>',
f'rpc_{bug_report_id}/{old_id:03}_actual.json',
f'rpc_{bug_report_id}/{uid:03}_actual.json',
]

def request(self, req: str) -> str:
Expand All @@ -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, old_id: int, bug_report_request: str) -> list[str]:
def command(self, bug_report_id: str, uid: str, bug_report_request: str) -> list[str]:
return [
'curl',
'-X',
Expand All @@ -165,7 +165,7 @@ def command(self, bug_report_id: str, old_id: int, bug_report_request: str) -> l
'@' + bug_report_request,
'http://' + self._host + ':' + str(self._port),
'>',
f'rpc_{bug_report_id}/{old_id:03}_actual.json',
f'rpc_{bug_report_id}/{uid:03}_actual.json',
]

def request(self, req: str) -> str:
Expand Down Expand Up @@ -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))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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:

k/pyk/src/pyk/utils.py

Line 541 in 0cfdcda

def add_command(self, args: Iterable[str]) -> None:

tothtamas28 marked this conversation as resolved.
Show resolved Hide resolved
self._req_id += 1

payload = {
'jsonrpc': self._JSON_RPC_VERSION,
'id': old_id,
'id': uid,
'method': method,
'params': params,
}

server_addr = self._transport.description()
_LOGGER.info(f'Sending request to {server_addr}: {old_id} - {method}')
_LOGGER.info(f'Sending request to {server_addr}: {uid} - {method}')
req = json.dumps(payload)
if self._bug_report:
bug_report_request = f'rpc_{self._bug_report_id}/{old_id:03}_request.json'
bug_report_request = f'rpc_{self._bug_report_id}/{uid:03}_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, old_id, bug_report_request))
self._bug_report.add_command(self._transport.command(self._bug_report_id, uid, bug_report_request))

_LOGGER.debug(f'Sending request to {server_addr}: {req}')
resp = self._transport.request(req)
Expand All @@ -316,23 +317,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}/{old_id:03}_response.json'
bug_report_response = f'rpc_{self._bug_report_id}/{uid:03}_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}/{old_id:03}_actual.json',
f'rpc_{self._bug_report_id}/{old_id:03}_response.json',
f'rpc_{self._bug_report_id}/{uid:03}_actual.json',
f'rpc_{self._bug_report_id}/{uid:03}_response.json',
]
)

data = json.loads(resp)
self._check(data)
assert data['id'] == old_id
assert data['id'] == uid

_LOGGER.info(f'Received response from {server_addr}: {old_id} - {method}')
_LOGGER.info(f'Received response from {server_addr}: {uid} - {method}')
return data['result']

@staticmethod
Expand Down
Loading