Adapting remaining tests from LLVMFunctionExitEvent

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

@@ -263,7 +263,7 @@ def test_parse_proof_hint_reverse_no_ints(
         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 (
@@ -388,7 +406,7 @@ def test_parse_proof_hint_non_rec_function(
         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 (
@@ -809,11 +839,11 @@ def test_parse_proof_hint_peano(self, hints: bytes, header: prooftrace.KoreHeade
         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
         )
 
 

pyk/src/tests/integration/test_krun_proof_hints.py

@@ -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")))]
 """