Bug report sequence storage changes (#4509)

Changes bug reports in the case of KoreServer proofs to indicate the sequence of requests not through the `commands` directory, as this wasn't being used, but through a simpler `sequence` directory, which contains files `0`, `1`, `2`, etc. which just contain the name of the request/response file in that position. --------- Co-authored-by: Jost Berthold <[email protected]>
runtimeverification · Jul 10, 2024 · 32dbd20 · 32dbd20
1 parent f6d64e9
commit 32dbd20
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 10 deletions.
diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py
@@ -71,7 +71,7 @@ def request(self, req: str, request_id: int, method_name: str) -> str:
         if self._bug_report:
             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._command(req_name, bug_report_request))
+            self._bug_report.add_request(f'{req_name}_request.json')
 
         server_addr = self._description()
         _LOGGER.info(f'Sending request to {server_addr}: {request_id} - {method_name}')
@@ -83,15 +83,7 @@ def request(self, req: str, request_id: int, method_name: str) -> str:
         if self._bug_report:
             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'{req_name}_actual.json',
-                    f'{req_name}_response.json',
-                ]
-            )
+            self._bug_report.add_request(f'{req_name}_response.json')
         return resp
 
     @abstractmethod

diff --git a/pyk/src/pyk/utils.py b/pyk/src/pyk/utils.py
@@ -688,6 +688,10 @@ def add_file_contents(self, input: str, arcname: Path) -> None:
             ntf.flush()
             self.add_file(Path(ntf.name), arcname)
 
+    def add_request(self, req_name: str) -> None:
+        self.add_file_contents(req_name, Path(f'sequence/{self._command_id:03}'))
+        self._command_id += 1
+
     def add_command(self, args: Iterable[str]) -> None:
         def _remap_arg(_a: str) -> str:
             if _a in self._file_remap: