Merge remote-tracking branch 'origin/develop' into _update-deps/runtimeverification/haskell-backend

Author: rv-auditor

deps/llvm-backend_release

@@ -1 +1 @@
-0.1.103
+0.1.122

flake.lock

@@ -1,7 +1,7 @@
 {
   description = "K Framework";
   inputs = {
-    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.103";
+    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.122";
     haskell-backend = {
       url = "github:runtimeverification/haskell-backend/v0.1.109";
       inputs.rv-utils.follows = "llvm-backend/rv-utils";

flake.nix

@@ -0,0 +1 @@
+from .k2lean4 import K2Lean4

k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out

@@ -1,18 +1,27 @@
 from __future__ import annotations
 
+import re
 from dataclasses import dataclass
 from typing import TYPE_CHECKING
 
+from ..konvert import unmunge
 from ..kore.internal import CollectionKind
 from ..kore.syntax import SortApp
 from ..utils import check_type
 from .model import Abbrev, Ctor, ExplBinder, Inductive, Module, Signature, Term
 
 if TYPE_CHECKING:
+    from typing import Final
+
     from ..kore.internal import KoreDefn
     from .model import Command
 
 
+_VALID_LEAN_IDENT: Final = re.compile(
+    "_[a-zA-Z0-9_?!']+|[a-zA-Z][a-zA-Z0-9_?!']*"
+)  # Simplified to characters permitted in KORE in the first place
+
+
 @dataclass(frozen=True)
 class K2Lean4:
     defn: KoreDefn
@@ -46,10 +55,19 @@ def _symbol_ctor(self, sort: str, symbol: str) -> Ctor:
         param_sorts = (
             check_type(sort, SortApp).name for sort in self.defn.symbols[symbol].param_sorts
         )  # TODO eliminate check_type
+        symbol = self._symbol_ident(symbol)
         binders = tuple(ExplBinder((f'x{i}',), Term(sort)) for i, sort in enumerate(param_sorts))
-        symbol = symbol.replace('-', '_')
         return Ctor(symbol, Signature(binders, Term(sort)))
 
+    @staticmethod
+    def _symbol_ident(symbol: str) -> str:
+        if symbol.startswith('Lbl'):
+            symbol = symbol[3:]
+        symbol = unmunge(symbol)
+        if not _VALID_LEAN_IDENT.fullmatch(symbol):
+            symbol = f'«{symbol}»'
+        return symbol
+
     def _collections(self) -> list[Command]:
         return [self._collection(sort) for sort in sorted(self.defn.collections)]
 

k-distribution/tests/regression-new/proof-instrumentation/input.test.out

@@ -73,7 +73,7 @@ def __init__(
     def __str__(self) -> str:
         modifiers = f'{self.modifiers} ' if self.modifiers else ''
         signature = f' {self.signature}' if self.signature else ''
-        return f'{modifiers} abbrev {self.ident}{signature} := {self.val}'
+        return f'{modifiers}abbrev {self.ident}{signature} := {self.val}'
 
 
 @final

llvm-backend/src/main/native/llvm-backend

@@ -9,6 +9,7 @@
     kore_header,
     llvm_rewrite_event,
     llvm_function_event,
+    llvm_function_exit_event,
     llvm_hook_event,
     llvm_rewrite_trace,
     llvm_rule_event,
@@ -245,6 +246,43 @@ def args(self) -> list[LLVMArgument]:
         return [LLVMArgument(arg) for arg in self._function_event.args]
 
 
+@final
+class LLVMFunctionExitEvent(LLVMStepEvent):
+    """Represent an LLVM function exit event in a proof trace.
+
+    Attributes:
+        _function_exit_event (llvm_function_exit_event): The underlying LLVM function exit event object.
+    """
+
+    _function_exit_event: llvm_function_exit_event
+
+    def __init__(self, function_exit_event: llvm_function_exit_event) -> None:
+        """Initialize a new instance of the LLVMFunctionExitEvent class.
+
+        Args:
+            function_exit_event (llvm_function_exit_event): The LLVM function exit event object.
+        """
+        self._function_exit_event = function_exit_event
+
+    def __repr__(self) -> str:
+        """Return a string representation of the object.
+
+        Returns:
+            A string representation of the LLVMFunctionExitEvent object using the AST printing method.
+        """
+        return self._function_exit_event.__repr__()
+
+    @property
+    def rule_ordinal(self) -> int:
+        """Return the axiom ordinal number associated with the function exit event."""
+        return self._function_exit_event.rule_ordinal
+
+    @property
+    def is_tail(self) -> bool:
+        """Return True if the function exit event is a tail call."""
+        return self._function_exit_event.is_tail
+
+
 @final
 class LLVMHookEvent(LLVMStepEvent):
     """Represents a hook event in LLVM execution.
@@ -330,6 +368,8 @@ def step_event(self) -> LLVMStepEvent:
             return LLVMSideConditionEventExit(self._argument.step_event)
         elif isinstance(self._argument.step_event, llvm_function_event):
             return LLVMFunctionEvent(self._argument.step_event)
+        elif isinstance(self._argument.step_event, llvm_function_exit_event):
+            return LLVMFunctionExitEvent(self._argument.step_event)
         elif isinstance(self._argument.step_event, llvm_hook_event):
             return LLVMHookEvent(self._argument.step_event)
         elif isinstance(self._argument.step_event, llvm_pattern_matching_failure_event):