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

…backend

deps/llvm-backend_release

@@ -1 +1 @@
-0.1.103
+0.1.119

flake.nix

@@ -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.119";
     haskell-backend = {
       url = "github:runtimeverification/haskell-backend/v0.1.105";
       inputs.rv-utils.follows = "llvm-backend/rv-utils";

pyk/src/pyk/kast/att.py

@@ -290,6 +290,7 @@ class Atts:
     ALIAS_REC: Final = AttKey('alias-rec', type=_NONE)
     ANYWHERE: Final = AttKey('anywhere', type=_NONE)
     ASSOC: Final = AttKey('assoc', type=_NONE)
+    AVOID: Final = AttKey('avoid', type=_NONE)
     BRACKET: Final = AttKey('bracket', type=_NONE)
     BRACKET_LABEL: Final = AttKey('bracketLabel', type=_ANY)
     CIRCULARITY: Final = AttKey('circularity', type=_NONE)
@@ -307,6 +308,7 @@ class Atts:
     DEPENDS: Final = AttKey('depends', type=_ANY)
     DIGEST: Final = AttKey('digest', type=_ANY)
     ELEMENT: Final = AttKey('element', type=_ANY)
+    EXIT: Final = AttKey('exit', type=_ANY)
     FORMAT: Final = AttKey('format', type=FormatType())
     FRESH_GENERATOR: Final = AttKey('freshGenerator', type=_NONE)
     FUNCTION: Final = AttKey('function', type=_NONE)
@@ -325,6 +327,8 @@ class Atts:
     MACRO: Final = AttKey('macro', type=_NONE)
     MACRO_REC: Final = AttKey('macro-rec', type=_NONE)
     MAINCELL: Final = AttKey('maincell', type=_NONE)
+    MULTIPLICITY: Final = AttKey('multiplicity', type=_ANY)
+    NO_EVALUATORS: Final = AttKey('no-evaluators', type=_NONE)
     OVERLOAD: Final = AttKey('overload', type=_STR)
     OWISE: Final = AttKey('owise', type=_NONE)
     PREDICATE: Final = AttKey('predicate', type=_ANY)
@@ -335,6 +339,7 @@ class Atts:
     PRODUCTION: Final = AttKey('org.kframework.definition.Production', type=_ANY)
     PROJECTION: Final = AttKey('projection', type=_NONE)
     RIGHT: Final = AttKey('right', type=_ANY)  # RIGHT and RIGHT_INTERNAL on the Frontend
+    RETURNS_UNIT: Final = AttKey('returnsUnit', type=_NONE)
     SIMPLIFICATION: Final = AttKey('simplification', type=_ANY)
     SEQSTRICT: Final = AttKey('seqstrict', type=_ANY)
     SORT: Final = AttKey('org.kframework.kore.Sort', type=_ANY)
@@ -345,9 +350,11 @@ class Atts:
     SYNTAX_MODULE: Final = AttKey('syntaxModule', type=_STR)
     SYMBOLIC: Final = AttKey('symbolic', type=OptionalType(_STR))
     TERMINALS: Final = AttKey('terminals', type=_STR)
+    TERMINATOR_SYMBOL: Final = AttKey('terminator-symbol', type=_ANY)
     TOKEN: Final = AttKey('token', type=_NONE)
     TOTAL: Final = AttKey('total', type=_NONE)
     TRUSTED: Final = AttKey('trusted', type=_NONE)
+    TYPE: Final = AttKey('type', type=_ANY)
     UNIT: Final = AttKey('unit', type=_STR)
     UNIQUE_ID: Final = AttKey('UNIQUE_ID', type=_ANY)
     UNPARSE_AVOID: Final = AttKey('unparseAvoid', type=_NONE)

pyk/src/pyk/kast/inner.py

@@ -877,20 +877,18 @@ def _var_occurence(_term: KInner) -> None:
     return _var_occurrences
 
 
-# TODO replace by method that does not reconstruct the AST
 def collect(callback: Callable[[KInner], None], kinner: KInner) -> None:
-    """Collect information about a given term traversing it bottom-up using a function with side effects.
+    """Collect information about a given term traversing it top-down using a function with side effects.
 
     Args:
         callback: Function with the side effect of collecting desired information at each AST node.
         kinner: The term to traverse.
     """
-
-    def f(kinner: KInner) -> KInner:
-        callback(kinner)
-        return kinner
-
-    bottom_up(f, kinner)
+    subterms = [kinner]
+    while subterms:
+        term = subterms.pop()
+        subterms.extend(reversed(term.terms))
+        callback(term)
 
 
 def build_assoc(unit: KInner, label: str | KLabel, terms: Iterable[KInner]) -> KInner:

pyk/src/pyk/kcfg/kcfg.py

@@ -559,6 +559,8 @@ def extend(
         extend_result: KCFGExtendResult,
         node: KCFG.Node,
         logs: dict[int, tuple[LogEntry, ...]],
+        *,
+        optimize_kcfg: bool,
     ) -> None:
 
         def log(message: str, *, warning: bool = False) -> None:
@@ -584,10 +586,25 @@ def log(message: str, *, warning: bool = False) -> None:
                 log(f'abstraction node: {node.id}')
 
             case Step(cterm, depth, next_node_logs, rule_labels, _):
+                node_id = node.id
                 next_node = self.create_node(cterm)
+                # Optimization for steps consists of on-the-fly merging of consecutive edges and can
+                # be performed only if the current node has a single predecessor connected by an Edge
+                if (
+                    optimize_kcfg
+                    and (len(predecessors := self.predecessors(target_id=node.id)) == 1)
+                    and isinstance(in_edge := predecessors[0], KCFG.Edge)
+                ):
+                    # The existing edge is removed and the step parameters are updated accordingly
+                    self.remove_edge(in_edge.source.id, node.id)
+                    node_id = in_edge.source.id
+                    depth += in_edge.depth
+                    rule_labels = list(in_edge.rules) + rule_labels
+                    next_node_logs = logs[node.id] + next_node_logs if node.id in logs else next_node_logs
+                    self.remove_node(node.id)
+                self.create_edge(node_id, next_node.id, depth, rule_labels)
                 logs[next_node.id] = next_node_logs
-                self.create_edge(node.id, next_node.id, depth, rules=rule_labels)
-                log(f'basic block at depth {depth}: {node.id} --> {next_node.id}')
+                log(f'basic block at depth {depth}: {node_id} --> {next_node.id}')
 
             case Branch(branches, _):
                 branch_node_ids = self.split_on_constraints(node.id, branches)

pyk/src/pyk/kllvm/hints/prooftrace.py

@@ -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):