Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update dependency: deps/llvm-backend_release #4648

Merged
merged 6 commits into from
Sep 25, 2024
Merged

Update dependency: deps/llvm-backend_release #4648

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
8bc2bd0
deps/llvm-backend_release: Set Version 0.1.95
Sep 23, 2024
6605db8
flake.nix, llvm-backend/src/main/native/llvm-backend: update to versi…
Sep 23, 2024
5e64411
flake.lock: update
Sep 23, 2024
758135a
Merge branch 'develop' into _update-deps/runtimeverification/llvm-bac…
theo25 Sep 25, 2024
de613df
fixing K tests
theo25 Sep 25, 2024
bd02511
fixes for pyk tests
theo25 Sep 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion deps/llvm-backend_release
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.94
0.1.95
8 changes: 4 additions & 4 deletions flake.lock
View file
Open in desktop

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
Open in desktop
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.94";
llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.95";
haskell-backend = {
url = "github:runtimeverification/haskell-backend/v0.1.76";
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
Open in desktop
Binary file not shown.
Binary file modified k-distribution/tests/regression-new/proof-instrumentation/input.test.out
View file
Open in desktop
Binary file not shown.
2 changes: 1 addition & 1 deletion llvm-backend/src/main/native/llvm-backend
Open in desktop
Submodule llvm-backend updated 106 files
46 changes: 23 additions & 23 deletions pyk/src/tests/integration/kllvm/test_prooftrace.py
View file
Open in desktop
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) == 14
assert len(list_of_events) == 13

# Test the type of the events
for event in list_of_events:
Expand Down Expand Up @@ -189,8 +189,8 @@ def test_parse_proof_hint_single_rewrite(
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 2 post-initial-configuration events
assert len(pt.trace) == 2
Expand Down Expand Up @@ -259,8 +259,8 @@ def test_parse_proof_hint_reverse_no_ints(
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 9 post-initial-configuration events
assert len(pt.trace) == 9
Expand Down Expand Up @@ -384,8 +384,8 @@ def test_parse_proof_hint_non_rec_function(
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 6 post-initial-configuration events
assert len(pt.trace) == 6
Expand Down Expand Up @@ -467,8 +467,8 @@ def test_parse_proof_hint_dv(self, hints: bytes, header: prooftrace.KoreHeader,
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 3 post-initial-configuration events
assert len(pt.trace) == 3
Expand Down Expand Up @@ -548,8 +548,8 @@ def test_parse_concurrent_counters(self, hints: bytes, header: prooftrace.KoreHe
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 37 post-initial-configuration events
assert len(pt.trace) == 37
Expand Down Expand Up @@ -708,8 +708,8 @@ def test_parse_proof_hint_0_decrement(self, hints: bytes, header: prooftrace.Kor
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 1 post-initial-configuration event
assert len(pt.trace) == 1
Expand Down Expand Up @@ -737,8 +737,8 @@ def test_parse_proof_hint_1_decrement(self, hints: bytes, header: prooftrace.Kor
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 2 post-initial-configuration events
assert len(pt.trace) == 2
Expand Down Expand Up @@ -766,8 +766,8 @@ def test_parse_proof_hint_2_decrement(self, hints: bytes, header: prooftrace.Kor
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 3 post-initial-configuration events
assert len(pt.trace) == 3
Expand Down Expand Up @@ -805,8 +805,8 @@ def test_parse_proof_hint_peano(self, hints: bytes, header: prooftrace.KoreHeade
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 776 post-initial-configuration events
assert len(pt.trace) == 776
Expand Down Expand Up @@ -914,8 +914,8 @@ def test_parse_proof_hint_imp5(self, hints: bytes, header: prooftrace.KoreHeader
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 16 initialization events
assert len(pt.pre_trace) == 16
# 14 initialization events
assert len(pt.pre_trace) == 14

# 2 post-initial-configuration events
assert len(pt.trace) == 2
Expand Down Expand Up @@ -953,8 +953,8 @@ def test_parse_proof_hint_builtin_hook_events(
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 4 post-initial-configuration events
assert len(pt.trace) == 4
Expand Down
10 changes: 2 additions & 8 deletions pyk/src/tests/integration/test_krun_proof_hints.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,12 +31,6 @@ class Test0Decrement(KRunTest, ProofTraceTest):
"""

HINTS_OUTPUT = """version: 13
hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
arg: kore[\\dv{SortKConfigVar{}}("$PGM")]
arg: kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()]
hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
hook: MAP.unit Lbl'Stop'Map{} ()
hook result: kore[Lbl'Stop'Map{}()]
hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
arg: kore[Lbl'Stop'Map{}()]
arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
Expand Down Expand Up @@ -73,8 +67,8 @@ def test_parse_proof_hint_0_decrement(self, krun: KRun, header: prooftrace.KoreH
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 1 post-initial-configuration event
assert len(pt.trace) == 1
Expand Down
Loading