Skip to content

Commit

Permalink
Roll back to pre mmap in llvm backend (0.1.103) (#4713)
Browse files Browse the repository at this point in the history 
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 <[email protected]>
  • Loading branch information
@jberthold
jberthold and rv-jenkins authored Dec 17, 2024
1 parent 5f79fb3 commit 29aedd7
Show file tree
Hide file tree
Showing 9 changed files with 33 additions and 107 deletions.
2 changes: 1 addition & 1 deletion deps/llvm-backend_release
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.119
0.1.103
8 changes: 4 additions & 4 deletions flake.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion flake.nix
View file
Original file line number Diff line number Diff line change
@@ -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";
Expand Down
Binary file modified k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out
View file
Binary file not shown.
Binary file modified k-distribution/tests/regression-new/proof-instrumentation/input.test.out
View file
Binary file not shown.
2 changes: 1 addition & 1 deletion llvm-backend/src/main/native/llvm-backend
Submodule llvm-backend updated 158 files
40 changes: 0 additions & 40 deletions pyk/src/pyk/kllvm/hints/prooftrace.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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):
Expand Down
80 changes: 25 additions & 55 deletions pyk/src/tests/integration/kllvm/test_prooftrace.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -321,43 +321,25 @@ 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'
# Fun events should not have Kore args unless called with a special flag
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 (
Expand Down Expand Up @@ -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)
Expand All @@ -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 (
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
)


Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
6 changes: 1 addition & 5 deletions pyk/src/tests/integration/test_krun_proof_hints.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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")))]
"""
Expand All @@ -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
Expand Down

0 comments on commit 29aedd7

Please sign in to comment.