From 30a66159af43ee6bb2a115d2a2e5ee423c884de7 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 17 Dec 2024 16:58:26 +0000 Subject: [PATCH 01/15] deps/llvm-backend_release: Set Version 0.1.120 --- deps/llvm-backend_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index 5950146bb3b..27f3bc3e903 100644 --- a/deps/llvm-backend_release +++ b/deps/llvm-backend_release @@ -1 +1 @@ -0.1.103 +0.1.120 From 22a68d6deb8702430a3f9d5de2c684749abc4ada Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Tue, 17 Dec 2024 16:59:32 +0000 Subject: [PATCH 02/15] flake.nix, llvm-backend/src/main/native/llvm-backend: update to version v0.1.120 --- flake.nix | 2 +- llvm-backend/src/main/native/llvm-backend | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/flake.nix b/flake.nix index 2a664a969e2..61e73045e2d 100644 --- a/flake.nix +++ b/flake.nix @@ -1,7 +1,7 @@ { description = "K Framework"; inputs = { - llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.103"; + llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.120"; haskell-backend = { url = "github:runtimeverification/haskell-backend/v0.1.104"; inputs.rv-utils.follows = "llvm-backend/rv-utils"; diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index d5eab4b0f0e..75e29599ed7 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit d5eab4b0f0e610bc60843ebb482f79c043b92702 +Subproject commit 75e29599ed760bb881e3f7dea6416d309a344058 From 83b27b067f5a488e5c40effa5ae935c0113e6e06 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Tue, 17 Dec 2024 16:59:47 +0000 Subject: [PATCH 03/15] flake.lock: update --- flake.lock | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/flake.lock b/flake.lock index fce466c75cd..0d6f3a7f31f 100644 --- a/flake.lock +++ b/flake.lock @@ -112,16 +112,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1730229432, - "narHash": "sha256-2Y4U7TCmSf9NAZCBmvXiHLOXrHxpiRgIpw5ERYDdNSM=", + "lastModified": 1734454030, + "narHash": "sha256-FbqcVNu2SYc9mc79cl8w5iTeQ3qGSM2EM/IP0yH9skw=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "d5eab4b0f0e610bc60843ebb482f79c043b92702", + "rev": "75e29599ed760bb881e3f7dea6416d309a344058", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.103", + "ref": "v0.1.120", "repo": "llvm-backend", "type": "github" } From a31e43ecc9b40f8e85232f9782240d91aba5e0c5 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 19 Dec 2024 17:44:17 +0000 Subject: [PATCH 04/15] deps/llvm-backend_release: Set Version 0.1.121 --- deps/llvm-backend_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index 27f3bc3e903..025c3166600 100644 --- a/deps/llvm-backend_release +++ b/deps/llvm-backend_release @@ -1 +1 @@ -0.1.120 +0.1.121 From 35b9e3493fbe35255c6d8ba8d6a90c44f5539cac Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 19 Dec 2024 17:45:23 +0000 Subject: [PATCH 05/15] flake.nix, llvm-backend/src/main/native/llvm-backend: update to version v0.1.121 --- flake.nix | 2 +- llvm-backend/src/main/native/llvm-backend | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/flake.nix b/flake.nix index 61e73045e2d..a85da28176e 100644 --- a/flake.nix +++ b/flake.nix @@ -1,7 +1,7 @@ { description = "K Framework"; inputs = { - llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.120"; + llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.121"; haskell-backend = { url = "github:runtimeverification/haskell-backend/v0.1.104"; inputs.rv-utils.follows = "llvm-backend/rv-utils"; diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index 75e29599ed7..c23977459e0 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit 75e29599ed760bb881e3f7dea6416d309a344058 +Subproject commit c23977459e01e2b6ef1122642a3c1ebf4d23fb24 From ebef8644acc780d347ce312b2fd97139de667621 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 19 Dec 2024 17:45:38 +0000 Subject: [PATCH 06/15] flake.lock: update --- flake.lock | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/flake.lock b/flake.lock index 0d6f3a7f31f..d8115f4508c 100644 --- a/flake.lock +++ b/flake.lock @@ -112,16 +112,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1734454030, - "narHash": "sha256-FbqcVNu2SYc9mc79cl8w5iTeQ3qGSM2EM/IP0yH9skw=", + "lastModified": 1734629436, + "narHash": "sha256-wugmpfkscDNQL5+ZNYCuZVKQQv3I4/ZwryBVoTV1cMU=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "75e29599ed760bb881e3f7dea6416d309a344058", + "rev": "c23977459e01e2b6ef1122642a3c1ebf4d23fb24", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.120", + "ref": "v0.1.121", "repo": "llvm-backend", "type": "github" } From ed4a1b4843d4a61f9ec232fae88c37569726202a Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 10 Jan 2025 16:14:38 +0000 Subject: [PATCH 07/15] deps/llvm-backend_release: Set Version 0.1.122 --- deps/llvm-backend_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index 025c3166600..aa3e27071d1 100644 --- a/deps/llvm-backend_release +++ b/deps/llvm-backend_release @@ -1 +1 @@ -0.1.121 +0.1.122 From 2e3884a4d1460ea6d4c54d7be9c69b1ea24698c8 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Fri, 10 Jan 2025 16:15:41 +0000 Subject: [PATCH 08/15] flake.nix, llvm-backend/src/main/native/llvm-backend: update to version v0.1.122 --- flake.nix | 2 +- llvm-backend/src/main/native/llvm-backend | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/flake.nix b/flake.nix index 01b740ce0be..6e1521f5dad 100644 --- a/flake.nix +++ b/flake.nix @@ -1,7 +1,7 @@ { description = "K Framework"; inputs = { - llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.121"; + llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.122"; haskell-backend = { url = "github:runtimeverification/haskell-backend/v0.1.108"; inputs.rv-utils.follows = "llvm-backend/rv-utils"; diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index c23977459e0..d910a26d2a4 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit c23977459e01e2b6ef1122642a3c1ebf4d23fb24 +Subproject commit d910a26d2a4c45e1b72eafb35642b76fc0d1faf0 From 6ea2853995687b40bb1a73365f0c6c1e0cefd514 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Fri, 10 Jan 2025 16:15:54 +0000 Subject: [PATCH 09/15] flake.lock: update --- flake.lock | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/flake.lock b/flake.lock index cb3f36b8dfd..5f6e64d4c46 100644 --- a/flake.lock +++ b/flake.lock @@ -112,16 +112,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1734629436, - "narHash": "sha256-wugmpfkscDNQL5+ZNYCuZVKQQv3I4/ZwryBVoTV1cMU=", + "lastModified": 1736524972, + "narHash": "sha256-h9tcey+vDixmOjLFtpdPU+bQJPkzyU8FsyrHWZHEWWk=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "c23977459e01e2b6ef1122642a3c1ebf4d23fb24", + "rev": "d910a26d2a4c45e1b72eafb35642b76fc0d1faf0", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.121", + "ref": "v0.1.122", "repo": "llvm-backend", "type": "github" } From 61c62e248dd983b8d79c1c7f9487b2b8fd5db276 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Fri, 13 Dec 2024 15:46:24 -0300 Subject: [PATCH 10/15] Updating proof binary --- .../proof-instrumentation/input.test.out | Bin 896 -> 964 bytes 1 file changed, 0 insertions(+), 0 deletions(-) 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 Date: Fri, 13 Dec 2024 16:22:53 -0300 Subject: [PATCH 11/15] Fixing proof hints tests --- .../integration/kllvm/test_prooftrace.py | 24 +++++++++---------- .../integration/test_krun_proof_hints.py | 2 +- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/pyk/src/tests/integration/kllvm/test_prooftrace.py b/pyk/src/tests/integration/kllvm/test_prooftrace.py index 8ef5cb94956..5eb84947292 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,7 +260,7 @@ 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 @@ -385,7 +385,7 @@ 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 @@ -468,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) == 10 + assert len(pt.pre_trace) == 14 # 3 post-initial-configuration events assert len(pt.trace) == 3 @@ -549,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) == 10 + assert len(pt.pre_trace) == 14 # 37 post-initial-configuration events assert len(pt.trace) == 37 @@ -709,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) == 10 + assert len(pt.pre_trace) == 14 # 1 post-initial-configuration event assert len(pt.trace) == 1 @@ -738,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) == 10 + assert len(pt.pre_trace) == 14 # 2 post-initial-configuration events assert len(pt.trace) == 2 @@ -767,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) == 10 + assert len(pt.pre_trace) == 14 # 3 post-initial-configuration events assert len(pt.trace) == 3 @@ -806,7 +806,7 @@ 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 @@ -915,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) == 14 + assert len(pt.pre_trace) == 20 # 2 post-initial-configuration events assert len(pt.trace) == 2 @@ -954,7 +954,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..5052b1e5bc6 100644 --- a/pyk/src/tests/integration/test_krun_proof_hints.py +++ b/pyk/src/tests/integration/test_krun_proof_hints.py @@ -68,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) == 10 + assert len(pt.pre_trace) == 14 # 1 post-initial-configuration event assert len(pt.trace) == 1 From d57e365921f986a966a132841b8c98ea95a6ca9d Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Fri, 13 Dec 2024 16:27:23 -0300 Subject: [PATCH 12/15] Updating proof binary debug --- .../input.test.out | Bin 1006 -> 1074 bytes 1 file changed, 0 insertions(+), 0 deletions(-) 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+ From 6bc07b7d0d7b8c974207a8b5d2c6909926d83c98 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Mon, 13 Jan 2025 17:35:04 -0300 Subject: [PATCH 13/15] Introducing `LLVMFunctionExitEvent` to `ProofTrace` python wrapper class --- pyk/src/pyk/kllvm/hints/prooftrace.py | 37 +++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/pyk/src/pyk/kllvm/hints/prooftrace.py b/pyk/src/pyk/kllvm/hints/prooftrace.py index fabe1d2f64d..5f2d6ce26ae 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,40 @@ 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 +365,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): From c203e134eef8c3b606a7aac76df018e27fa8732a Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Mon, 13 Jan 2025 17:38:02 -0300 Subject: [PATCH 14/15] Adapting remaining tests from `LLVMFunctionExitEvent` --- .../integration/kllvm/test_prooftrace.py | 56 ++++++++++++++----- .../integration/test_krun_proof_hints.py | 4 ++ 2 files changed, 47 insertions(+), 13 deletions(-) diff --git a/pyk/src/tests/integration/kllvm/test_prooftrace.py b/pyk/src/tests/integration/kllvm/test_prooftrace.py index 5eb84947292..ee54383fd7a 100644 --- a/pyk/src/tests/integration/kllvm/test_prooftrace.py +++ b/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,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 ( @@ -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 ) diff --git a/pyk/src/tests/integration/test_krun_proof_hints.py b/pyk/src/tests/integration/test_krun_proof_hints.py index 5052b1e5bc6..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")))] """ From b4903bfae0dee11c1c4ed584c7a8a81b6f3f4f8b Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Mon, 13 Jan 2025 17:44:08 -0300 Subject: [PATCH 15/15] Formatting --- pyk/src/pyk/kllvm/hints/prooftrace.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/pyk/src/pyk/kllvm/hints/prooftrace.py b/pyk/src/pyk/kllvm/hints/prooftrace.py index 5f2d6ce26ae..36028cd99f2 100644 --- a/pyk/src/pyk/kllvm/hints/prooftrace.py +++ b/pyk/src/pyk/kllvm/hints/prooftrace.py @@ -249,6 +249,7 @@ def args(self) -> list[LLVMArgument]: @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. """ @@ -257,6 +258,7 @@ class LLVMFunctionExitEvent(LLVMStepEvent): 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. """ @@ -264,6 +266,7 @@ def __init__(self, function_exit_event: llvm_function_exit_event) -> None: def __repr__(self) -> str: """Return a string representation of the object. + Returns: A string representation of the LLVMFunctionExitEvent object using the AST printing method. """