Roll back to pre mmap in llvm backend (0.1.103)

deps/llvm-backend_release

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

flake.nix

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

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

@@ -9,7 +9,6 @@
     kore_header,
     llvm_rewrite_event,
     llvm_function_event,
-    llvm_function_exit_event,
     llvm_hook_event,
     llvm_rewrite_trace,
     llvm_rule_event,
@@ -246,43 +245,6 @@ 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.
@@ -368,8 +330,6 @@ 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):

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

@@ -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) == 17
+        assert len(list_of_events) == 13
 
         # 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) == 14
+        assert len(pt.pre_trace) == 10
 
         # 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) == 14
+        assert len(pt.pre_trace) == 10
 
         # 9 post-initial-configuration events
-        assert len(pt.trace) == 12
+        assert len(pt.trace) == 9
 
         # Contents of the k cell in the initial configuration
         kore_pattern = llvm_to_pattern(pt.initial_config.kore_pattern)
@@ -321,43 +321,25 @@ 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[7].step_event
+        rule_event = pt.trace[6].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[8].step_event
+        rule_event = pt.trace[7].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[11].is_kore_pattern()
-        kore_pattern = llvm_to_pattern(pt.trace[11].kore_pattern)
+        assert pt.trace[8].is_kore_pattern()
+        kore_pattern = llvm_to_pattern(pt.trace[8].kore_pattern)
         k_cell = kore_pattern.patterns[0].dict['args'][0]
         assert k_cell['name'] == 'kseq'
         assert (
@@ -403,10 +385,10 @@ def test_parse_proof_hint_non_rec_function(
         assert pt is not None
 
         # 10 initialization events
-        assert len(pt.pre_trace) == 14
+        assert len(pt.pre_trace) == 10
 
         # 6 post-initial-configuration events
-        assert len(pt.trace) == 8
+        assert len(pt.trace) == 6
 
         # Contents of the k cell in the initial configuration
         kore_pattern = llvm_to_pattern(pt.initial_config.kore_pattern)
@@ -433,36 +415,24 @@ 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[4].step_event
+        fun_event = pt.trace[3].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[5].step_event
+        rule_event = pt.trace[4].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[7].is_kore_pattern()
-        kore_pattern = llvm_to_pattern(pt.trace[7].kore_pattern)
+        assert pt.trace[5].is_kore_pattern()
+        kore_pattern = llvm_to_pattern(pt.trace[5].kore_pattern)
         k_cell = kore_pattern.patterns[0].dict['args'][0]
         assert k_cell['name'] == 'kseq'
         assert (
@@ -498,7 +468,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) == 14
+        assert len(pt.pre_trace) == 10
 
         # 3 post-initial-configuration events
         assert len(pt.trace) == 3
@@ -579,7 +549,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) == 14
+        assert len(pt.pre_trace) == 10
 
         # 37 post-initial-configuration events
         assert len(pt.trace) == 37
@@ -739,7 +709,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) == 14
+        assert len(pt.pre_trace) == 10
 
         # 1 post-initial-configuration event
         assert len(pt.trace) == 1
@@ -768,7 +738,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) == 14
+        assert len(pt.pre_trace) == 10
 
         # 2 post-initial-configuration events
         assert len(pt.trace) == 2
@@ -797,7 +767,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) == 14
+        assert len(pt.pre_trace) == 10
 
         # 3 post-initial-configuration events
         assert len(pt.trace) == 3
@@ -836,14 +806,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) == 14
+        assert len(pt.pre_trace) == 10
 
         # 776 post-initial-configuration events
-        assert len(pt.trace) == 916
+        assert len(pt.trace) == 776
 
         # Assert that we have a pattern matching failure as the 135th event
-        assert pt.trace[160].is_step_event() and isinstance(
-            pt.trace[160].step_event, prooftrace.LLVMPatternMatchingFailureEvent
+        assert pt.trace[135].is_step_event() and isinstance(
+            pt.trace[135].step_event, prooftrace.LLVMPatternMatchingFailureEvent
         )
 
 
@@ -945,7 +915,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) == 20
+        assert len(pt.pre_trace) == 14
 
         # 2 post-initial-configuration events
         assert len(pt.trace) == 2
@@ -984,7 +954,7 @@ def test_parse_proof_hint_builtin_hook_events(
         assert pt is not None
 
         # 10 initialization events
-        assert len(pt.pre_trace) == 14
+        assert len(pt.pre_trace) == 10
 
         # 4 post-initial-configuration events
         assert len(pt.trace) == 4

pyk/src/tests/integration/test_krun_proof_hints.py

@@ -48,12 +48,8 @@ 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")))]
 """
@@ -72,7 +68,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) == 14
+        assert len(pt.pre_trace) == 10
 
         # 1 post-initial-configuration event
         assert len(pt.trace) == 1