diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index c21e67e653..841597f02d 100644 --- a/deps/llvm-backend_release +++ b/deps/llvm-backend_release @@ -1 +1 @@ -0.1.113 +0.1.119 diff --git a/flake.lock b/flake.lock index 34fbc3b7dc..8eea337491 100644 --- a/flake.lock +++ b/flake.lock @@ -112,16 +112,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1733763903, - "narHash": "sha256-wvkNjv30PWyswJA2+1XnNSydCX+jXAiaaGovz2z/5Lw=", + "lastModified": 1734123780, + "narHash": "sha256-cR/a2NpIyRL6kb4zA0JCbufLITCRfyHpcdzWcnhDTe8=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "b16e56c905b7dc4db70ac7c0ec00abc18831500d", + "rev": "1cd3319755df0c53d437313aea0d71b6cfdd9de5", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.113", + "ref": "v0.1.119", "repo": "llvm-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index 2296c01a4c..71b5bd4fc5 100644 --- a/flake.nix +++ b/flake.nix @@ -1,7 +1,7 @@ { description = "K Framework"; inputs = { - llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.113"; + llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.119"; 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 4706f33c25..ef03e1e235 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 46c83b90bc..24aac4eacc 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 b16e56c905..1cd3319755 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit b16e56c905b7dc4db70ac7c0ec00abc18831500d +Subproject commit 1cd3319755df0c53d437313aea0d71b6cfdd9de5 diff --git a/pyk/src/pyk/kllvm/hints/prooftrace.py b/pyk/src/pyk/kllvm/hints/prooftrace.py index fabe1d2f64..36028cd99f 100644 --- a/pyk/src/pyk/kllvm/hints/prooftrace.py +++ b/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): diff --git a/pyk/src/tests/integration/kllvm/test_prooftrace.py b/pyk/src/tests/integration/kllvm/test_prooftrace.py index 8ef5cb9495..ee54383fd7 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) == 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,8 +321,14 @@ 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' @@ -330,16 +336,28 @@ def test_parse_proof_hint_reverse_no_ints( 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 diff --git a/pyk/src/tests/integration/test_krun_proof_hints.py b/pyk/src/tests/integration/test_krun_proof_hints.py index 008f6fd64f..fa9ca09b0b 100644 --- a/pyk/src/tests/integration/test_krun_proof_hints.py +++ b/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")))] """ @@ -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