From 29aedd725e4d797393b8f090f775a9fff2183012 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 17 Dec 2024 15:44:44 +1100 Subject: [PATCH] Roll back to pre mmap in llvm backend (0.1.103) (#4713) This rolls back the LLVM backend dependency to 0.1.105, to work around problems with the new thread-local `mmap` memory management. It also rolls back a change that introduced the new `LLVMFunctionExitEvent` in pyk (to cater for its addition in LLVM backend), which is in the first commit of this branch (tag `added-llvm-function-exit`, to retain the commit for later re-addition). --------- Co-authored-by: rv-jenkins --- deps/llvm-backend_release | 2 +- flake.lock | 8 +- flake.nix | 2 +- .../input.test.out | Bin 1074 -> 1006 bytes .../proof-instrumentation/input.test.out | Bin 964 -> 896 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, 33 insertions(+), 107 deletions(-) diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index 841597f02d9..5950146bb3b 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 8eea337491b..fce466c75cd 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 71b5bd4fc58..2a664a969e2 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 ef03e1e235d4a03e8c276afb4c5d95ebea3d016d..4706f33c2538bbba45acb6c8b35862811b75b653 100644 GIT binary patch delta 19 bcmdnQ@s54N8K%jxOx%-yGTBa!V7>(aPumB+ delta 74 pcmaFIzKLVQ87BEqDClN@0+>KDm_PX>leZL1C=p#v(qtayM*!kL66F8@ 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 24aac4eaccee69ebb8c3a6dd0dd66b46d323aaee..46c83b90bc1ad6cd3d33def10d74256b86802860 100644 GIT binary patch delta 18 acmX@Y-oU;gj%nfyiODmV3?{!~x&;71-v?R% 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. @@ -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 ee54383fd7a..8ef5cb94956 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 fa9ca09b0b7..008f6fd64f9 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