diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index e982215505..9c178d3b81 100644 --- a/deps/llvm-backend_release +++ b/deps/llvm-backend_release @@ -1 +1 @@ -0.1.94 +0.1.95 diff --git a/flake.lock b/flake.lock index 197fe0862b..0573caa5f2 100644 --- a/flake.lock +++ b/flake.lock @@ -112,16 +112,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1726776150, - "narHash": "sha256-A4OX0ZV4/AS+tztmLG52v/ayMV43WscbF6lLKOaoPrw=", + "lastModified": 1727116141, + "narHash": "sha256-htGQy05VRhuAWdMkUzCf67gkKRGSHfJUeXU5bc2Z27Q=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "c023bc5eb734c1718243d66613044e895e8fcf7e", + "rev": "b830daaa6392ff256e62970cab89deeaaf7aab95", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.94", + "ref": "v0.1.95", "repo": "llvm-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index b5fc3552a6..75d1243b0c 100644 --- a/flake.nix +++ b/flake.nix @@ -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"; 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 e37a8e4464..4706f33c25 100644 Binary files a/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out and b/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out differ 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 adc5b2451f..46c83b90bc 100644 Binary files a/k-distribution/tests/regression-new/proof-instrumentation/input.test.out and b/k-distribution/tests/regression-new/proof-instrumentation/input.test.out differ diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index c023bc5eb7..b830daaa63 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit c023bc5eb734c1718243d66613044e895e8fcf7e +Subproject commit b830daaa6392ff256e62970cab89deeaaf7aab95 diff --git a/pyk/src/tests/integration/kllvm/test_prooftrace.py b/pyk/src/tests/integration/kllvm/test_prooftrace.py index 62fa039a55..8ef5cb9495 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) == 14 + assert len(list_of_events) == 13 # Test the type of the events for event in list_of_events: @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 diff --git a/pyk/src/tests/integration/test_krun_proof_hints.py b/pyk/src/tests/integration/test_krun_proof_hints.py index 5650a12697..008f6fd64f 100644 --- a/pyk/src/tests/integration/test_krun_proof_hints.py +++ b/pyk/src/tests/integration/test_krun_proof_hints.py @@ -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{}())] @@ -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