From 32dbd20e8e986e4abe04858ccc7202fb220067f3 Mon Sep 17 00:00:00 2001 From: Noah Watson <107630091+nwatson22@users.noreply.github.com> Date: Tue, 9 Jul 2024 21:00:33 -0500 Subject: [PATCH 1/3] 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 --- pyk/src/pyk/kore/rpc.py | 12 ++---------- pyk/src/pyk/utils.py | 4 ++++ 2 files changed, 6 insertions(+), 10 deletions(-) diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index 24cfde7a76e..647e6e4fcb9 100644 --- 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 index 15d4c9665ec..03550dcafc6 100644 --- 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: From 981f5e6293a1fc38cdc8040a857cf9c7a28fa5c6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 10 Jul 2024 12:02:27 +0200 Subject: [PATCH 2/3] Remove `Atts.KLABEL` (#4506) Related: * #4045 * runtimeverification/kontrol#679 Changes: * Remove `Atts.KLABEL` * Make `Atts.SYMBOL` unary --- pyk/src/pyk/kast/att.py | 3 +-- pyk/src/pyk/kast/pretty.py | 6 ++---- pyk/src/pyk/kore_exec_covr/__main__.py | 4 ++-- pyk/src/tests/unit/kast/test_att.py | 6 +++--- 4 files changed, 8 insertions(+), 11 deletions(-) diff --git a/pyk/src/pyk/kast/att.py b/pyk/src/pyk/kast/att.py index b9f4f4bc2cb..d730bbd67de 100644 --- a/pyk/src/pyk/kast/att.py +++ b/pyk/src/pyk/kast/att.py @@ -319,7 +319,6 @@ class Atts: INDEX: Final = AttKey('index', type=_INT) INITIALIZER: Final = AttKey('initializer', type=_NONE) INJECTIVE: Final = AttKey('injective', type=_NONE) - KLABEL: Final = AttKey('klabel', type=_ANY) LABEL: Final = AttKey('label', type=_ANY) LEFT: Final = AttKey('left', type=_ANY) # LEFT and LEFT_INTERNAL on the Frontend LOCATION: Final = AttKey('org.kframework.attributes.Location', type=_LOCATION) @@ -341,7 +340,7 @@ class Atts: SORT: Final = AttKey('org.kframework.kore.Sort', type=_ANY) SOURCE: Final = AttKey('org.kframework.attributes.Source', type=_PATH) STRICT: Final = AttKey('strict', type=_ANY) - SYMBOL: Final = AttKey('symbol', type=OptionalType(_STR)) + SYMBOL: Final = AttKey('symbol', type=_STR) SYNTAX_MODULE: Final = AttKey('syntaxModule', type=_STR) TERMINALS: Final = AttKey('terminals', type=_STR) TOKEN: Final = AttKey('token', type=_NONE) diff --git a/pyk/src/pyk/kast/pretty.py b/pyk/src/pyk/kast/pretty.py index 7ff0e17c017..6a30d41e94e 100644 --- a/pyk/src/pyk/kast/pretty.py +++ b/pyk/src/pyk/kast/pretty.py @@ -217,8 +217,6 @@ def _print_knonterminal(self, knonterminal: KNonTerminal) -> str: return self.print(knonterminal.sort) def _print_kproduction(self, kproduction: KProduction) -> str: - if Atts.KLABEL not in kproduction.att and kproduction.klabel: - kproduction = kproduction.update_atts([Atts.KLABEL(kproduction.klabel.name)]) syntax_str = 'syntax ' + self.print(kproduction.sort) if kproduction.items: syntax_str += ' ::= ' + ' '.join([self._print_kouter(pi) for pi in kproduction.items]) @@ -378,8 +376,8 @@ def build_symbol_table( unparser = unparser_for_production(prod) symbol_table[label] = unparser - if Atts.SYMBOL in prod.att and Atts.KLABEL in prod.att: - symbol_table[prod.att[Atts.KLABEL]] = unparser + if Atts.SYMBOL in prod.att: + symbol_table[prod.att[Atts.SYMBOL]] = unparser if opinionated: symbol_table['#And'] = lambda c1, c2: c1 + '\n#And ' + c2 diff --git a/pyk/src/pyk/kore_exec_covr/__main__.py b/pyk/src/pyk/kore_exec_covr/__main__.py index cf6d692d84f..d0957da33a1 100644 --- a/pyk/src/pyk/kore_exec_covr/__main__.py +++ b/pyk/src/pyk/kore_exec_covr/__main__.py @@ -66,8 +66,8 @@ def do_analyze(definition_dir: Path, input_file: Path) -> None: print('=================================') for location_str, hits in applied_simplifications.items(): rule_label_str = '' - if location_str in rule_dict and Atts.KLABEL in rule_dict[location_str].att: - rule_label_str = f'[{rule_dict[location_str].att[Atts.LABEL]}]' + if location_str in rule_dict and Atts.SYMBOL in rule_dict[location_str].att: + rule_label_str = f'[{rule_dict[location_str].att[Atts.SYMBOL]}]' if hits > 0: print(f' {hits} applications of rule {rule_label_str} defined at {location_str}') total_simplifications = sum([v for v in applied_simplifications.values() if v > 0]) diff --git a/pyk/src/tests/unit/kast/test_att.py b/pyk/src/tests/unit/kast/test_att.py index a3df205aea2..cab5c4975c5 100644 --- a/pyk/src/tests/unit/kast/test_att.py +++ b/pyk/src/tests/unit/kast/test_att.py @@ -17,9 +17,9 @@ ('empty', (), ''), ('nullary', (Atts.FUNCTION(None),), '[function]'), ('two-nullaries', (Atts.FUNCTION(None), Atts.TOTAL(None)), '[function, total]'), - ('opt-none', (Atts.SYMBOL(None),), '[symbol]'), - ('opt-some-empty-str', (Atts.SYMBOL(''),), '[symbol("")]'), - ('opt-some-nonempty-str', (Atts.SYMBOL('foo'),), '[symbol("foo")]'), + ('opt-none', (Atts.CONCRETE(None),), '[concrete]'), + ('opt-some-empty-str', (Atts.CONCRETE(''),), '[concrete("")]'), + ('opt-some-nonempty-str', (Atts.CONCRETE('foo'),), '[concrete("foo")]'), ('multiple', (Atts.SYMBOL('foo'), Atts.FUNCTION(None), Atts.TOTAL(None)), '[symbol("foo"), function, total]'), ) From 8093153e8ecf1c87dcbdf1fc22293fa7222d35bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 10 Jul 2024 13:48:41 +0200 Subject: [PATCH 3/3] Log `KoreServer` output (#4501) Stream output from `kore-rpc` and `kore-rpc-booster` into a `Logger`, instead of the standard output / error stream of the parent. --- pyk/src/pyk/kore/rpc.py | 31 +++++++++++++++++++++++++++---- 1 file changed, 27 insertions(+), 4 deletions(-) diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index 647e6e4fcb9..3bbfdb68620 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -12,7 +12,8 @@ from enum import Enum, auto from pathlib import Path from signal import SIGINT -from subprocess import Popen +from subprocess import DEVNULL, PIPE, Popen +from threading import Thread from time import sleep from typing import ClassVar # noqa: TC003 from typing import TYPE_CHECKING, ContextManager, NamedTuple, TypedDict, final @@ -26,7 +27,7 @@ if TYPE_CHECKING: from collections.abc import Iterable, Mapping - from typing import Any, Final, TextIO, TypeVar + from typing import IO, Any, Final, TypeVar from typing_extensions import Required @@ -115,7 +116,7 @@ class SingleSocketTransport(Transport): _host: str _port: int _sock: socket.socket - _file: TextIO + _file: IO[str] def __init__( self, @@ -1129,6 +1130,8 @@ class KoreServerInfo(NamedTuple): class KoreServer(ContextManager['KoreServer']): _proc: Popen + _stdout_reader: Thread + _stderr_reader: Thread _info: KoreServerInfo _kompiled_dir: Path @@ -1208,7 +1211,7 @@ def start(self) -> None: new_env['GHCRTS'] = f'-N{self._haskell_threads}' _LOGGER.info(f'Starting KoreServer: {" ".join(cli_args)}') - self._proc = Popen(cli_args, env=new_env) + self._proc, self._stdout_reader, self._stderr_reader = self._create_proc(cli_args, new_env) pid = self._proc.pid host, port = self._get_host_and_port(pid) if self._port: @@ -1216,6 +1219,24 @@ def start(self) -> None: self._info = KoreServerInfo(pid=pid, host=host, port=port) _LOGGER.info(f'KoreServer started: {self.host}:{self.port}, pid={self.pid}') + @staticmethod + def _create_proc(args: list[str], env: dict[str, str]) -> tuple[Popen, Thread, Thread]: + popen = Popen(args, env=env, stdin=DEVNULL, stdout=PIPE, stderr=PIPE, text=True) + + def reader(fh: IO[str], prefix: str) -> None: + for line in fh: + _LOGGER.info(f'[PID={popen.pid}][{prefix}] {line.rstrip()}') + + stdout_reader = Thread(target=reader, args=(popen.stdout, 'stdo')) + stdout_reader.daemon = True + stdout_reader.start() + + stderr_reader = Thread(target=reader, args=(popen.stderr, 'stde')) + stderr_reader.daemon = True + stderr_reader.start() + + return popen, stdout_reader, stderr_reader + def close(self) -> None: _LOGGER.info(f'Stopping KoreServer: {self.host}:{self.port}, pid={self.pid}') if '--solver-transcript' in self._command: @@ -1223,6 +1244,8 @@ def close(self) -> None: else: self._proc.terminate() self._proc.wait() + self._stdout_reader.join() + self._stderr_reader.join() _LOGGER.info(f'KoreServer stopped: {self.host}:{self.port}, pid={self.pid}') def _validate(self) -> None: