Merge branch 'develop' into log-kore-server

llvm-backend/src/main/scripts/bin/llvm-kompile-matching

@@ -45,10 +45,10 @@ then
 elif [ $# -lt 4 ];
 then
     fail "ERROR: Not enough arguments!"
-elif [ ! -f $1 ];
+elif [ ! -f "$1" ];
 then
     fail "ERROR: <definition.kore> not a file!"
-elif [ ! -d $3 ];
+elif ! mkdir -p "$3";
 then
     fail "ERROR: <output dir> not a directory!"
 fi

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/kbuild/utils.py

@@ -7,7 +7,7 @@
 from typing import TYPE_CHECKING, final
 
 from ..cli.utils import check_dir_path, check_file_path
-from ..utils import run_process
+from ..utils import run_process_2
 
 if TYPE_CHECKING:
     from collections.abc import Iterable
@@ -71,7 +71,7 @@ def text(self) -> str:
 
 def k_version() -> KVersion:
     try:
-        proc_res = run_process(['kompile', '--version'], pipe_stderr=True)
+        proc_res = run_process_2(['kompile', '--version'])
     except FileNotFoundError as err:
         raise RuntimeError('K is not installed') from err
 

pyk/src/pyk/kllvm/compiler.py

@@ -7,7 +7,7 @@
 from typing import TYPE_CHECKING
 
 from ..cli.utils import check_dir_path, check_file_path
-from ..utils import run_process
+from ..utils import run_process_2
 
 if TYPE_CHECKING:
     from collections.abc import Iterable
@@ -37,7 +37,7 @@ def compile_kllvm(target_dir: str | Path, *, verbose: bool = False) -> Path:
         args += ['--verbose']
 
     _LOGGER.info(f'Compiling pythonast extension: {module_file.name}')
-    run_process(args, logger=_LOGGER)
+    run_process_2(args, logger=_LOGGER)
 
     assert module_file.is_file()
     return module_file
@@ -87,7 +87,7 @@ def compile_runtime(
         args += ccopts
 
     _LOGGER.info(f'Compiling python extension: {module_file.name}')
-    run_process(args, logger=_LOGGER)
+    run_process_2(args, logger=_LOGGER)
 
     assert module_file.is_file()
     return module_file
@@ -123,7 +123,7 @@ def generate_hints(
 
     args = [str(interpreter), str(input_kore_file), '-1', str(hints_file), '--proof-output']
     _LOGGER.info(f'Generating hints: {hints_file.name}')
-    run_process(args, logger=_LOGGER)
+    run_process_2(args, logger=_LOGGER)
 
     assert hints_file.is_file()
 

pyk/src/pyk/kllvm/load_static.py

@@ -3,7 +3,7 @@
 from pathlib import Path
 from typing import TYPE_CHECKING
 
-from ..utils import run_process
+from ..utils import run_process_2
 from .importer import import_kllvm
 
 if TYPE_CHECKING:
@@ -12,7 +12,7 @@
 
 def get_kllvm() -> Path:
     args = ['llvm-kompile', '--bindings-path']
-    proc = run_process(args, pipe_stdout=True)
+    proc = run_process_2(args)
     bindings_dir = Path(proc.stdout.rstrip()).resolve()
     kllvm_dir = bindings_dir / 'kllvm'
     return kllvm_dir

pyk/src/pyk/kore/rpc.py

@@ -20,7 +20,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, run_process_2
 from . import manip
 from .prelude import SORT_GENERATED_TOP_CELL
 from .syntax import And, Equals, EVar, kore_term
@@ -72,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}')
@@ -84,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
@@ -1304,7 +1296,7 @@ def _extra_args(self) -> list[str]:
     def _populate_bug_report(self, bug_report: BugReport) -> None:
         prog_name = self._command[0]
         bug_report.add_file(self._definition_file, Path('definition.kore'))
-        version_info = run_process((prog_name, '--version'), pipe_stderr=True, logger=_LOGGER).stdout.strip()
+        version_info = run_process_2((prog_name, '--version'), logger=_LOGGER).stdout.strip()
         bug_report.add_file_contents(version_info, Path('server_version.txt'))
         server_instance = {
             'exe': prog_name,
@@ -1410,7 +1402,7 @@ def _extra_args(self) -> list[str]:
     def _populate_bug_report(self, bug_report: BugReport) -> None:
         super()._populate_bug_report(bug_report)
         bug_report.add_file(self._llvm_definition, Path('llvm_definition/definition.kore'))
-        llvm_version = run_process('llvm-backend-version', pipe_stderr=True, logger=_LOGGER).stdout.strip()
+        llvm_version = run_process_2('llvm-backend-version', logger=_LOGGER).stdout.strip()
         bug_report.add_file_contents(llvm_version, Path('llvm_version.txt'))
 
 

pyk/src/pyk/kore/tools.py

@@ -5,7 +5,7 @@
 from typing import TYPE_CHECKING
 
 from ..cli.utils import check_dir_path, check_file_path
-from ..utils import run_process
+from ..utils import run_process_2
 
 if TYPE_CHECKING:
     from .syntax import Pattern
@@ -79,5 +79,5 @@ def _kore_print(
     if color is not None:
         args += ['--color', 'on' if color else 'off']
 
-    run_res = run_process(args, input=input)
+    run_res = run_process_2(args, input=input)
     return run_res.stdout.strip()

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/ktool/kompile.py

@@ -15,7 +15,7 @@
 from subprocess import CalledProcessError
 from typing import TYPE_CHECKING, final
 
-from ..utils import abs_or_rel_to, check_dir_path, check_file_path, run_process, single
+from ..utils import abs_or_rel_to, check_dir_path, check_file_path, run_process_2, single
 from . import TypeInferenceMode
 
 if TYPE_CHECKING:
@@ -332,7 +332,7 @@ def __call__(
             args += ['-Wno', ','.join(ignore_warnings)]
 
         try:
-            proc_res = run_process(args, logger=_LOGGER, cwd=cwd, check=check)
+            proc_res = run_process_2(args, write_stderr=True, logger=_LOGGER, cwd=cwd, check=check)
         except CalledProcessError as err:
             raise RuntimeError(
                 f'Command kompile exited with code {err.returncode} for: {self.base_args.main_file}',

pyk/src/pyk/ktool/kprint.py

@@ -19,7 +19,7 @@
 from ..kore.parser import KoreParser
 from ..kore.syntax import App, SortApp
 from ..kore.tools import PrintOutput, kore_print
-from ..utils import run_process
+from ..utils import run_process_2
 from .kompile import DefinitionInfo
 
 if TYPE_CHECKING:
@@ -108,7 +108,7 @@ def _kast(
     )
 
     try:
-        return run_process(args, logger=_LOGGER, check=check)
+        return run_process_2(args, write_stderr=True, logger=_LOGGER, check=check)
     except CalledProcessError as err:
         raise RuntimeError(
             f'Command kast exited with code {err.returncode} for: {file}', err.stdout, err.stderr

pyk/src/pyk/ktool/kprove.py

@@ -19,7 +19,7 @@
 from ..kast.outer import KDefinition, KFlatModule, KFlatModuleList, KImport, KRequire
 from ..kore.rpc import KoreExecLogFormat
 from ..prelude.ml import is_top
-from ..utils import gen_file_timestamp, run_process
+from ..utils import gen_file_timestamp, run_process_2
 from . import TypeInferenceMode
 from .claim_index import ClaimIndex
 from .kprint import KPrint
@@ -98,7 +98,7 @@ def _kprove(
 
     try:
         run_args = tuple(chain(command, [str(spec_file)], typed_args, args))
-        return run_process(run_args, logger=_LOGGER, env=env, check=check)
+        return run_process_2(run_args, write_stderr=True, logger=_LOGGER, env=env, check=check)
     except CalledProcessError as err:
         raise RuntimeError(
             f'Command kprove exited with code {err.returncode} for: {spec_file}', err.stdout, err.stderr, err

pyk/src/pyk/ktool/krun.py

@@ -9,7 +9,7 @@
 from ..cli.utils import check_dir_path, check_file_path
 from ..kore.parser import KoreParser
 from ..kore.tools import PrintOutput, kore_print
-from ..utils import run_process
+from ..utils import run_process, run_process_2
 from .kprint import KPrint
 
 if TYPE_CHECKING:
@@ -344,4 +344,4 @@ def llvm_interpret_raw(definition_dir: str | Path, kore: str, depth: int | None
     depth = depth if depth is not None else -1
     args = [str(interpreter_file), '/dev/stdin', str(depth), '/dev/stdout']
 
-    return run_process(args, input=kore, pipe_stderr=True)
+    return run_process_2(args, input=kore)