Merge branch 'develop' into _update-deps/runtimeverification/llvm-bac…

…kend

pyk/src/pyk/kllvm/runtime.py

@@ -6,7 +6,7 @@
     from types import ModuleType
     from typing import Any
 
-    from .ast import Pattern, Sort
+    from .ast import CompositePattern, Pattern, Sort
 
 
 class Runtime:
@@ -43,6 +43,11 @@ def simplify_bool(self, pattern: Pattern) -> bool:
         self._module.free_all_gc_memory()
         return res
 
+    def evaluate(self, pattern: CompositePattern) -> Pattern:
+        res = self._module.evaluate_function(pattern)
+        self._module.free_all_gc_memory()
+        return res
+
 
 class Term:
     _block: Any  # module.InternalTerm

pyk/src/pyk/kore/rpc.py

@@ -622,6 +622,7 @@ def to_dict(self) -> dict[str, Any]:
 class LogOrigin(str, Enum):
     KORE_RPC = 'kore-rpc'
     BOOSTER = 'booster'
+    PROXY = 'proxy'
     LLVM = 'llvm'
 
 

pyk/src/pyk/ktool/krun.py

@@ -339,4 +339,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_2(args, input=kore)
+    return run_process_2(args, input=kore, logger=_LOGGER, loglevel=logging.DEBUG)

pyk/src/pyk/utils.py

@@ -464,6 +464,7 @@ def run_process_2(
     cwd: str | Path | None = None,
     env: Mapping[str, str] | None = None,
     logger: Logger | None = None,
+    loglevel: int | None = None,
     check: bool = True,
 ) -> CompletedProcess:
     if type(args) is str:
@@ -478,6 +479,9 @@ def run_process_2(
     if not logger:
         logger = _LOGGER
 
+    if loglevel is None:
+        loglevel = logging.INFO
+
     res = _subprocess_run(
         args,
         input=input,
@@ -486,6 +490,7 @@ def run_process_2(
         cwd=cwd,
         env=env,
         logger=logger,
+        loglevel=loglevel,
     )
 
     if check:
@@ -503,6 +508,7 @@ def _subprocess_run(
     env: Mapping[str, str] | None,
     cwd: Path | None,
     logger: Logger,
+    loglevel: int,
 ) -> CompletedProcess:
     with Popen(
         args,
@@ -517,26 +523,27 @@ def _subprocess_run(
 
         command = shlex.join(args)
         for line in command.split('\n'):
-            logger.info(f'{log_prefix}[exec] {line}')
+            logger.log(loglevel, f'{log_prefix}[exec] {line}')
 
         start_time = time.time()
 
         try:
             returncode, stdout, stderr = _subprocess_communicate(
                 popen,
                 input=input,
-                logger=logger,
                 write_stdout=write_stdout,
                 write_stderr=write_stderr,
+                logger=logger,
+                loglevel=loglevel,
             )
         except BaseException:
             popen.kill()
             delta_time = time.time() - start_time
-            logger.info(f'{log_prefix}[fail] time={delta_time:.3f}s')
+            logger.log(loglevel, f'{log_prefix}[fail] time={delta_time:.3f}s')
             raise
 
     delta_time = time.time() - start_time
-    logger.info(f'{log_prefix}[done] status={returncode} time={delta_time:.3f}s')
+    logger.log(loglevel, f'{log_prefix}[done] status={returncode} time={delta_time:.3f}s')
 
     return CompletedProcess(popen.args, returncode, stdout, stderr)
 
@@ -548,6 +555,7 @@ def _subprocess_communicate(
     write_stdout: bool,
     write_stderr: bool,
     logger: Logger,
+    loglevel: int,
 ) -> tuple[int, str, str]:
     assert popen.stdout is not None
     assert popen.stderr is not None
@@ -562,7 +570,7 @@ def readerthread(
     ) -> None:
         for line in input_fh:
             buffer.append(line)
-            logger.info(f'{log_prefix}{stream_prefix} {line.rstrip()}')
+            logger.log(loglevel, f'{log_prefix}{stream_prefix} {line.rstrip()}')
             if output_fh:
                 output_fh.write(line)
                 output_fh.flush()
@@ -585,7 +593,7 @@ def readerthread(
     if input is not None:
         assert popen.stdin is not None
         for line in input.split('\n'):
-            logger.info(f'{log_prefix}[stdi] {line}')
+            logger.log(loglevel, f'{log_prefix}[stdi] {line}')
         # Note: popen.stdin.write does not work for llvm_interpret_raw
         popen._stdin_write(input)  # type: ignore [attr-defined]
 
@@ -649,11 +657,6 @@ def ensure_dir_path(path: str | Path) -> Path:
     return path
 
 
-# Implementation because of outdated Python versions: https://github.com/python/cpython/blob/1de4395f62bb140563761ef5cbdf46accef3c550/Lib/pathlib.py#L554
-def is_relative_to(_self: Path, other: Path) -> bool:
-    return _self == other or other in _self.parents
-
-
 def abs_or_rel_to(path: Path, base: Path) -> Path:
     if path.is_absolute():
         return path
@@ -699,7 +702,7 @@ def _remap_arg(_a: str) -> str:
             _a_path = Path(_a)
             for _f in self._file_remap:
                 _f_path = Path(_f)
-                if is_relative_to(_a_path, _f_path):
+                if _a_path.is_relative_to(_f_path):
                     return str(Path(self._file_remap[_f]) / _a_path.relative_to(_f_path))
             return _a
 

pyk/src/tests/integration/kllvm/test_evaluate.py

@@ -0,0 +1,49 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
+import pytest
+
+import pyk.kllvm.load  # noqa: F401
+from pyk.kllvm import parser
+from pyk.testing import RuntimeTest
+
+from ..utils import K_FILES
+
+if TYPE_CHECKING:
+    from pyk.kllvm.runtime import Runtime
+
+
+EVALUATE_TEST_DATA = (
+    ('1 + 2', r"""Lbl'UndsPlus'Int'Unds'{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))""", r'\dv{SortInt{}}("3")'),
+    ('1 * 2', r"""Lbl'UndsStar'Int'Unds'{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))""", r'\dv{SortInt{}}("2")'),
+    (
+        '1 + (2 * 3)',
+        r"""
+        Lbl'UndsPlus'Int'Unds'{}(
+            \dv{SortInt{}}("1"),
+            Lbl'UndsStar'Int'Unds'{}(\dv{SortInt{}}("2"), \dv{SortInt{}}("3"))
+        )
+        """,
+        r'\dv{SortInt{}}("7")',
+    ),
+)
+
+
+class TestEvaluate(RuntimeTest):
+    KOMPILE_MAIN_FILE = K_FILES / 'imp.k'
+
+    @pytest.mark.parametrize(
+        'test_id,pattern_text,expected',
+        EVALUATE_TEST_DATA,
+        ids=[test_id for test_id, *_ in EVALUATE_TEST_DATA],
+    )
+    def test_simplify(self, runtime: Runtime, test_id: str, pattern_text: str, expected: str) -> None:
+        # Given
+        pattern = parser.parse_pattern(pattern_text)
+
+        # When
+        actual = runtime.evaluate(pattern)
+
+        # Then
+        assert str(actual) == expected