Merge branch 'develop' into _update-deps/runtimeverification/haskell-…

…backend

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)

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

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
 
@@ -71,7 +72,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 +84,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
@@ -123,7 +116,7 @@ class SingleSocketTransport(Transport):
     _host: str
     _port: int
     _sock: socket.socket
-    _file: TextIO
+    _file: IO[str]
 
     def __init__(
         self,
@@ -1137,6 +1130,8 @@ class KoreServerInfo(NamedTuple):
 
 class KoreServer(ContextManager['KoreServer']):
     _proc: Popen
+    _stdout_reader: Thread
+    _stderr_reader: Thread
     _info: KoreServerInfo
 
     _kompiled_dir: Path
@@ -1216,21 +1211,41 @@ 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:
             assert port == self._port
         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:
             self._proc.send_signal(SIGINT)
         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:

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])

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:

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]'),
 )