diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index 841597f02d..5950146bb3 100644 --- a/deps/llvm-backend_release +++ b/deps/llvm-backend_release @@ -1 +1 @@ -0.1.119 +0.1.103 diff --git a/flake.lock b/flake.lock index 8eea337491..fce466c75c 100644 --- a/flake.lock +++ b/flake.lock @@ -112,16 +112,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1734123780, - "narHash": "sha256-cR/a2NpIyRL6kb4zA0JCbufLITCRfyHpcdzWcnhDTe8=", + "lastModified": 1730229432, + "narHash": "sha256-2Y4U7TCmSf9NAZCBmvXiHLOXrHxpiRgIpw5ERYDdNSM=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "1cd3319755df0c53d437313aea0d71b6cfdd9de5", + "rev": "d5eab4b0f0e610bc60843ebb482f79c043b92702", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.119", + "ref": "v0.1.103", "repo": "llvm-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index 71b5bd4fc5..2a664a969e 100644 --- a/flake.nix +++ b/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"; diff --git a/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out b/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out index ef03e1e235..4706f33c25 100644 Binary files a/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out and b/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out differ diff --git a/k-distribution/tests/regression-new/proof-instrumentation/input.test.out b/k-distribution/tests/regression-new/proof-instrumentation/input.test.out index 24aac4eacc..46c83b90bc 100644 Binary files a/k-distribution/tests/regression-new/proof-instrumentation/input.test.out and b/k-distribution/tests/regression-new/proof-instrumentation/input.test.out differ diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index 1cd3319755..d5eab4b0f0 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit 1cd3319755df0c53d437313aea0d71b6cfdd9de5 +Subproject commit d5eab4b0f0e610bc60843ebb482f79c043b92702 diff --git a/pyk/src/pyk/kllvm/hints/prooftrace.py b/pyk/src/pyk/kllvm/hints/prooftrace.py index 36028cd99f..fabe1d2f64 100644 --- a/pyk/src/pyk/kllvm/hints/prooftrace.py +++ b/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): diff --git a/pyk/src/tests/integration/kllvm/test_prooftrace.py b/pyk/src/tests/integration/kllvm/test_prooftrace.py index ee54383fd7..8ef5cb9495 100644 --- a/pyk/src/tests/integration/kllvm/test_prooftrace.py +++ b/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,14 +321,8 @@ 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' @@ -336,28 +330,16 @@ def test_parse_proof_hint_reverse_no_ints( 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 diff --git a/pyk/src/tests/integration/test_krun_proof_hints.py b/pyk/src/tests/integration/test_krun_proof_hints.py index fa9ca09b0b..008f6fd64f 100644 --- a/pyk/src/tests/integration/test_krun_proof_hints.py +++ b/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