From 5f79fb3abf43dfd2fd8196b57b8e536267722f71 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Fri, 13 Dec 2024 22:42:59 -0700 Subject: [PATCH] Update dependency: deps/llvm-backend_release (#4711) Co-authored-by: devops Co-authored-by: Roberto Rosmaninho Co-authored-by: Roberto Rosmaninho --- deps/llvm-backend_release | 2 +- flake.lock | 8 +- flake.nix | 2 +- .../input.test.out | Bin 1006 -> 1074 bytes .../proof-instrumentation/input.test.out | Bin 896 -> 964 bytes llvm-backend/src/main/native/llvm-backend | 2 +- pyk/src/pyk/kllvm/hints/prooftrace.py | 40 +++++++++ .../integration/kllvm/test_prooftrace.py | 80 ++++++++++++------ .../integration/test_krun_proof_hints.py | 6 +- 9 files changed, 107 insertions(+), 33 deletions(-) diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index c21e67e653a..841597f02d9 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 34fbc3b7dca..8eea337491b 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 2296c01a4cf..71b5bd4fc58 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 4706f33c2538bbba45acb6c8b35862811b75b653..ef03e1e235d4a03e8c276afb4c5d95ebea3d016d 100644 GIT binary patch delta 74 pcmaFIzKLVQ87BEqDClN@0+>KDm_PX>leZL1C=p#v(qtayM*!kL66F8@ delta 19 bcmdnQ@s54N8K%jxOx%-yGTBa!V7>(aPumB+ 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 46c83b90bc1ad6cd3d33def10d74256b86802860..24aac4eaccee69ebb8c3a6dd0dd66b46d323aaee 100644 GIT binary patch delta 74 pcmZo*Kf=Btj!8Zg3c4Af049(O=1-1h@|J=LC8DcInmmu`5dfU85 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 8ef5cb94956..ee54383fd7a 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 008f6fd64f9..fa9ca09b0b7 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