From 449726d959107728a5fd076e38c1708fb517ea95 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Wed, 25 Sep 2024 14:02:28 -0600 Subject: [PATCH] Update dependency: deps/llvm-backend_release (#4648) Co-authored-by: devops Co-authored-by: Theodoros Kasampalis --- deps/llvm-backend_release | 2 +- flake.lock | 8 +-- flake.nix | 2 +- .../input.test.out | Bin 1197 -> 1006 bytes .../proof-instrumentation/input.test.out | Bin 1087 -> 896 bytes llvm-backend/src/main/native/llvm-backend | 2 +- .../integration/kllvm/test_prooftrace.py | 46 +++++++++--------- .../integration/test_krun_proof_hints.py | 10 +--- 8 files changed, 32 insertions(+), 38 deletions(-) diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index e9822155054..9c178d3b81d 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 197fe0862bc..0573caa5f2e 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 b5fc3552a6b..75d1243b0ce 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 e37a8e44649c1c7f09ee16b58057bf7dcf951483..4706f33c2538bbba45acb6c8b35862811b75b653 100644 GIT binary patch delta 10 RcmZ3>`Hp>p$i~aJm;o7f1hD`B delta 97 zcmaFIzLs->h*D}!YHn&?34>2kj(TWbN^wADL8`j0x~_YOE{LmMT{~HmNsgu7JIH8a nwC&^zj6BMvd6^LP!6o?x>b{8u)wK)^yP*K2kdbvG>q}+;RjVS3 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 adc5b2451f5703f44daf3cf42b3ecf6e2de2d95f..46c83b90bc1ad6cd3d33def10d74256b86802860 100644 GIT binary patch delta 10 Rcmdnb(ZD`IWaH%=W&jn{1Lgn# delta 102 zcmZo*-_J2YL?bmPH8(Y{guy2%M?Ewzr8pq7AXQygUDrKC7sOSsu4Q1T_YN|e_(p;S mOh?;Ju43d-F3rn?XbLXLFHrYQEC4Co4Fw>DjI0}3tC<1X*CTcS diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index c023bc5eb73..b830daaa639 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 62fa039a55d..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) == 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 5650a12697f..008f6fd64f9 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