Merge remote-tracking branch 'origin/develop'

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.108";
       inputs.rv-utils.follows = "llvm-backend/rv-utils";

flake.nix

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

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

@@ -103,7 +103,7 @@ def test_streaming_parser_iter(self, header: prooftrace.KoreHeader, hints_file:
         list_of_events = list(it)
 
         # Test length of the list
-        assert len(list_of_events) == 13
+        assert len(list_of_events) == 17
 
         # Test the type of the events
         for event in list_of_events:
@@ -190,7 +190,7 @@ def test_parse_proof_hint_single_rewrite(
         assert pt is not None
 
         # 10 initialization events
-        assert len(pt.pre_trace) == 10
+        assert len(pt.pre_trace) == 14
 
         # 2 post-initial-configuration events
         assert len(pt.trace) == 2
@@ -260,10 +260,10 @@ def test_parse_proof_hint_reverse_no_ints(
         assert pt is not None
 
         # 10 initialization events
-        assert len(pt.pre_trace) == 10
+        assert len(pt.pre_trace) == 14
 
         # 9 post-initial-configuration events
-        assert len(pt.trace) == 9
+        assert len(pt.trace) == 12
 
         # Contents of the k cell in the initial configuration
         kore_pattern = llvm_to_pattern(pt.initial_config.kore_pattern)
@@ -321,25 +321,43 @@ def test_parse_proof_hint_reverse_no_ints(
         assert axiom == axiom_expected
         assert len(rule_event.substitution) == 1
 
+        # Function exit event (no tail)
+        function_exit_event = pt.trace[6].step_event
+        assert isinstance(function_exit_event, prooftrace.LLVMFunctionExitEvent)
+        assert function_exit_event.rule_ordinal == 158
+        assert function_exit_event.is_tail == False
+
         # Function event
-        rule_event = pt.trace[6].step_event
+        rule_event = pt.trace[7].step_event
         assert isinstance(rule_event, prooftrace.LLVMFunctionEvent)
         assert rule_event.name == "Lblreverse'LParUndsRParUnds'TREE-REVERSE-SYNTAX'Unds'Tree'Unds'Tree{}"
         assert rule_event.relative_position == '1'
         # Fun events should not have Kore args unless called with a special flag
         assert len(rule_event.args) == 0
 
         # Simplification rule
-        rule_event = pt.trace[7].step_event
+        rule_event = pt.trace[8].step_event
         assert isinstance(rule_event, prooftrace.LLVMRuleEvent)
         axiom = repr(definition.get_axiom_by_ordinal(rule_event.rule_ordinal))
         axiom_expected = get_pattern_from_ordinal(definition_text, rule_event.rule_ordinal)
         assert axiom == axiom_expected
         assert len(rule_event.substitution) == 1
 
+        # Function exit event (no tail)
+        function_exit_event = pt.trace[9].step_event
+        assert isinstance(function_exit_event, prooftrace.LLVMFunctionExitEvent)
+        assert function_exit_event.rule_ordinal == 157
+        assert function_exit_event.is_tail == False
+
+        # Function exit event (no tail)
+        function_exit_event = pt.trace[10].step_event
+        assert isinstance(function_exit_event, prooftrace.LLVMFunctionExitEvent)
+        assert function_exit_event.rule_ordinal == 160
+        assert function_exit_event.is_tail == False
+
         # Then pattern
-        assert pt.trace[8].is_kore_pattern()
-        kore_pattern = llvm_to_pattern(pt.trace[8].kore_pattern)
+        assert pt.trace[11].is_kore_pattern()
+        kore_pattern = llvm_to_pattern(pt.trace[11].kore_pattern)
         k_cell = kore_pattern.patterns[0].dict['args'][0]
         assert k_cell['name'] == 'kseq'
         assert (
@@ -385,10 +403,10 @@ def test_parse_proof_hint_non_rec_function(
         assert pt is not None
 
         # 10 initialization events
-        assert len(pt.pre_trace) == 10
+        assert len(pt.pre_trace) == 14
 
         # 6 post-initial-configuration events
-        assert len(pt.trace) == 6
+        assert len(pt.trace) == 8
 
         # Contents of the k cell in the initial configuration
         kore_pattern = llvm_to_pattern(pt.initial_config.kore_pattern)
@@ -415,24 +433,36 @@ def test_parse_proof_hint_non_rec_function(
         inner_rule_event = pt.trace[2].step_event
         assert isinstance(inner_rule_event, prooftrace.LLVMRuleEvent)
 
+        # Function exit event (no tail)
+        function_exit_event = pt.trace[3].step_event
+        assert isinstance(function_exit_event, prooftrace.LLVMFunctionExitEvent)
+        assert function_exit_event.rule_ordinal == 103
+        assert function_exit_event.is_tail == False
+
         # Functional event
-        fun_event = pt.trace[3].step_event
+        fun_event = pt.trace[4].step_event
         assert isinstance(fun_event, prooftrace.LLVMFunctionEvent)
         assert fun_event.name == "Lblid'LParUndsRParUnds'NON-REC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo{}"
         assert fun_event.relative_position == '0:0:0'
         assert len(fun_event.args) == 0
 
         # Then rule
-        rule_event = pt.trace[4].step_event
+        rule_event = pt.trace[5].step_event
         assert isinstance(rule_event, prooftrace.LLVMRuleEvent)
         axiom = repr(definition.get_axiom_by_ordinal(rule_event.rule_ordinal))
         axiom_expected = get_pattern_from_ordinal(definition_text, rule_event.rule_ordinal)
         assert axiom == axiom_expected
         assert len(rule_event.substitution) == 1
 
+        # Function exit event (no tail)
+        function_exit_event = pt.trace[6].step_event
+        assert isinstance(function_exit_event, prooftrace.LLVMFunctionExitEvent)
+        assert function_exit_event.rule_ordinal == 103
+        assert function_exit_event.is_tail == False
+
         # Then pattern
-        assert pt.trace[5].is_kore_pattern()
-        kore_pattern = llvm_to_pattern(pt.trace[5].kore_pattern)
+        assert pt.trace[7].is_kore_pattern()
+        kore_pattern = llvm_to_pattern(pt.trace[7].kore_pattern)
         k_cell = kore_pattern.patterns[0].dict['args'][0]
         assert k_cell['name'] == 'kseq'
         assert (
@@ -468,7 +498,7 @@ def test_parse_proof_hint_dv(self, hints: bytes, header: prooftrace.KoreHeader,
         assert pt is not None
 
         # 10 initialization events
-        assert len(pt.pre_trace) == 10
+        assert len(pt.pre_trace) == 14
 
         # 3 post-initial-configuration events
         assert len(pt.trace) == 3
@@ -549,7 +579,7 @@ def test_parse_concurrent_counters(self, hints: bytes, header: prooftrace.KoreHe
         assert pt is not None
 
         # 10 initialization events
-        assert len(pt.pre_trace) == 10
+        assert len(pt.pre_trace) == 14
 
         # 37 post-initial-configuration events
         assert len(pt.trace) == 37
@@ -709,7 +739,7 @@ def test_parse_proof_hint_0_decrement(self, hints: bytes, header: prooftrace.Kor
         assert pt is not None
 
         # 10 initialization events
-        assert len(pt.pre_trace) == 10
+        assert len(pt.pre_trace) == 14
 
         # 1 post-initial-configuration event
         assert len(pt.trace) == 1
@@ -738,7 +768,7 @@ def test_parse_proof_hint_1_decrement(self, hints: bytes, header: prooftrace.Kor
         assert pt is not None
 
         # 10 initialization events
-        assert len(pt.pre_trace) == 10
+        assert len(pt.pre_trace) == 14
 
         # 2 post-initial-configuration events
         assert len(pt.trace) == 2
@@ -767,7 +797,7 @@ def test_parse_proof_hint_2_decrement(self, hints: bytes, header: prooftrace.Kor
         assert pt is not None
 
         # 10 initialization events
-        assert len(pt.pre_trace) == 10
+        assert len(pt.pre_trace) == 14
 
         # 3 post-initial-configuration events
         assert len(pt.trace) == 3
@@ -806,14 +836,14 @@ def test_parse_proof_hint_peano(self, hints: bytes, header: prooftrace.KoreHeade
         assert pt is not None
 
         # 10 initialization events
-        assert len(pt.pre_trace) == 10
+        assert len(pt.pre_trace) == 14
 
         # 776 post-initial-configuration events
-        assert len(pt.trace) == 776
+        assert len(pt.trace) == 916
 
         # Assert that we have a pattern matching failure as the 135th event
-        assert pt.trace[135].is_step_event() and isinstance(
-            pt.trace[135].step_event, prooftrace.LLVMPatternMatchingFailureEvent
+        assert pt.trace[160].is_step_event() and isinstance(
+            pt.trace[160].step_event, prooftrace.LLVMPatternMatchingFailureEvent
         )
 
 
@@ -915,7 +945,7 @@ def test_parse_proof_hint_imp5(self, hints: bytes, header: prooftrace.KoreHeader
         assert pt is not None
 
         # 14 initialization events
-        assert len(pt.pre_trace) == 14
+        assert len(pt.pre_trace) == 20
 
         # 2 post-initial-configuration events
         assert len(pt.trace) == 2
@@ -954,7 +984,7 @@ def test_parse_proof_hint_builtin_hook_events(
         assert pt is not None
 
         # 10 initialization events
-        assert len(pt.pre_trace) == 10
+        assert len(pt.pre_trace) == 14
 
         # 4 post-initial-configuration events
         assert len(pt.trace) == 4

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

@@ -48,8 +48,12 @@ class Test0Decrement(KRunTest, ProofTraceTest):
 function: Lblproject'Coln'KItem{} (0:0)
 rule: 139 1
   VarK = kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()]
+function exit: 139 notail
+function exit: 100 notail
 function: LblinitGeneratedCounterCell{} (1)
 rule: 98 0
+function exit: 98 notail
+function exit: 99 notail
 config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}(),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\\dv{SortInt{}}("0")))]
 config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}(),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\\dv{SortInt{}}("0")))]
 """
@@ -68,7 +72,7 @@ def test_parse_proof_hint_0_decrement(self, krun: KRun, header: prooftrace.KoreH
         assert pt is not None
 
         # 10 initialization events
-        assert len(pt.pre_trace) == 10
+        assert len(pt.pre_trace) == 14
 
         # 1 post-initial-configuration event
         assert len(pt.trace) == 1