From 5bcca0a1f6c4024369f48a94327c7506c43d7cb2 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 6 Mar 2026 22:09:40 +0800 Subject: [PATCH 1/3] test(integration): add iter-eq repro with red show snapshot --- .../iter-eq-copied-take-dereftruncate-fail.rs | 32 +++++++++++++++++++ ...ied-take-dereftruncate-fail.repro.expected | 15 +++++++++ .../src/tests/integration/test_integration.py | 2 ++ 3 files changed, 49 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/iter-eq-copied-take-dereftruncate-fail.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate-fail.repro.expected diff --git a/kmir/src/tests/integration/data/prove-rs/iter-eq-copied-take-dereftruncate-fail.rs b/kmir/src/tests/integration/data/prove-rs/iter-eq-copied-take-dereftruncate-fail.rs new file mode 100644 index 000000000..75e7c1b9e --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/iter-eq-copied-take-dereftruncate-fail.rs @@ -0,0 +1,32 @@ +fn main() { + let _keep: fn() -> bool = repro; +} + +#[inline(never)] +#[no_mangle] +pub fn repro() -> bool { + let k0 = Pubkey([1; 32]); + let k1 = Pubkey([2; 32]); + let k2 = Pubkey([3; 32]); + let n = 2usize; + + let accounts = [ + AccountInfo { key: &k0 }, + AccountInfo { key: &k1 }, + AccountInfo { key: &k2 }, + ]; + let signers = [k1, k2, k0]; + + accounts[1..] + .iter() + .map(|signer| *signer.key) + .eq(signers.iter().take(n).copied()) +} + +#[derive(Clone)] +struct AccountInfo<'a> { + key: &'a Pubkey, +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +struct Pubkey([u8; 32]); diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate-fail.repro.expected b/kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate-fail.repro.expected new file mode 100644 index 000000000..f2b4fc230 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate-fail.repro.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (1947 steps) +└─ 3 (stuck, leaf) + #traverseProjection ( toLocal ( 1 ) , thunk ( operandCopy ( place ( ... local: l + span: 30 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 3014e4b04..294669ad0 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -38,6 +38,7 @@ 'assume-cheatcode-conflict-fail': ['check_assume_conflict'], 'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'], 'test_offset_from-fail': ['testing'], + 'iter-eq-copied-take-dereftruncate-fail': ['repro'], } PROVE_RS_SHOW_SPECS = [ 'local-raw-fail', @@ -63,6 +64,7 @@ 'test_offset_from-fail', 'ref-ptr-cast-elem-fail', 'ref-ptr-cast-elem-offset-fail', + 'iter-eq-copied-take-dereftruncate-fail', ] From 3a973eab7aaa674eb8089ed2505142baa3f60ec9 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 9 Mar 2026 15:32:55 +0800 Subject: [PATCH 2/3] fix(rt): initialize closure env in setupCalleeClosure2 --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 3 ++- ...l.rs => iter-eq-copied-take-dereftruncate.rs} | 0 ...copied-take-dereftruncate-fail.repro.expected | 15 --------------- ...r-eq-copied-take-dereftruncate.repro.expected | 16 ++++++++++++++++ kmir/src/tests/integration/test_integration.py | 4 ++-- 5 files changed, 20 insertions(+), 18 deletions(-) rename kmir/src/tests/integration/data/prove-rs/{iter-eq-copied-take-dereftruncate-fail.rs => iter-eq-copied-take-dereftruncate.rs} (100%) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate-fail.repro.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate.repro.expected diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index b85ee0002..ea3d2e418 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -562,7 +562,8 @@ Therefore a heuristics is used here: _SPAN ) => - #setTupleArgs(2, getValue(LOCALS, TUPLE)) ~> #execBlock(FIRST) + #setLocalValue(place(local(1), .ProjectionElems), #incrementRef(getValue(LOCALS, CLOSURE))) + ~> #setTupleArgs(2, getValue(LOCALS, TUPLE)) ~> #execBlock(FIRST) // arguments are tuple components, stored as _2 .. _n ... diff --git a/kmir/src/tests/integration/data/prove-rs/iter-eq-copied-take-dereftruncate-fail.rs b/kmir/src/tests/integration/data/prove-rs/iter-eq-copied-take-dereftruncate.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/iter-eq-copied-take-dereftruncate-fail.rs rename to kmir/src/tests/integration/data/prove-rs/iter-eq-copied-take-dereftruncate.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate-fail.repro.expected b/kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate-fail.repro.expected deleted file mode 100644 index f2b4fc230..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate-fail.repro.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (1947 steps) -└─ 3 (stuck, leaf) - #traverseProjection ( toLocal ( 1 ) , thunk ( operandCopy ( place ( ... local: l - span: 30 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate.repro.expected b/kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate.repro.expected new file mode 100644 index 000000000..7d670625d --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate.repro.expected @@ -0,0 +1,16 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (5601 steps) +├─ 3 (terminal) +│ #EndProgram ~> .K +│ +┊ constraint: true +┊ subst: ... +└─ 2 (leaf, target, terminal) + #EndProgram ~> .K + + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 294669ad0..13439a488 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -38,7 +38,7 @@ 'assume-cheatcode-conflict-fail': ['check_assume_conflict'], 'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'], 'test_offset_from-fail': ['testing'], - 'iter-eq-copied-take-dereftruncate-fail': ['repro'], + 'iter-eq-copied-take-dereftruncate': ['repro'], } PROVE_RS_SHOW_SPECS = [ 'local-raw-fail', @@ -64,7 +64,7 @@ 'test_offset_from-fail', 'ref-ptr-cast-elem-fail', 'ref-ptr-cast-elem-offset-fail', - 'iter-eq-copied-take-dereftruncate-fail', + 'iter-eq-copied-take-dereftruncate', ] From 1da95522d52a4a79736f3dc2ade96b62dcd7b215 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 9 Mar 2026 15:33:07 +0800 Subject: [PATCH 3/3] test(integration): remove iter-eq from show list --- ...r-eq-copied-take-dereftruncate.repro.expected | 16 ---------------- kmir/src/tests/integration/test_integration.py | 1 - 2 files changed, 17 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate.repro.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate.repro.expected b/kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate.repro.expected deleted file mode 100644 index 7d670625d..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/iter-eq-copied-take-dereftruncate.repro.expected +++ /dev/null @@ -1,16 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (5601 steps) -├─ 3 (terminal) -│ #EndProgram ~> .K -│ -┊ constraint: true -┊ subst: ... -└─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - - diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 13439a488..945002873 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -64,7 +64,6 @@ 'test_offset_from-fail', 'ref-ptr-cast-elem-fail', 'ref-ptr-cast-elem-offset-fail', - 'iter-eq-copied-take-dereftruncate', ]