From 410a5310935903f7788b6afa61053582a10838c0 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 6 Mar 2026 12:42:11 +0800 Subject: [PATCH 1/5] test(prove-rs): add closure staged red case with show snapshot --- .../integration/data/prove-rs/closure-staged.rs | 11 +++++++++++ .../prove-rs/show/closure-staged.main.expected | 16 ++++++++++++++++ kmir/src/tests/integration/test_integration.py | 1 + 3 files changed, 28 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/closure-staged.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/closure-staged.rs b/kmir/src/tests/integration/data/prove-rs/closure-staged.rs new file mode 100644 index 000000000..98e256256 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/closure-staged.rs @@ -0,0 +1,11 @@ +fn apply u8>(f: F, v: u8) -> u8 { + f(v) +} + +fn main() { + let delta: u8 = 1u8; + let _captured = |x: u8| x + delta; + + let f = |x: u8| x + 1u8; + assert_eq!(apply(f, 41u8), 42u8); +} diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected new file mode 100644 index 000000000..681632508 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected @@ -0,0 +1,16 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (33 steps) +└─ 3 (stuck, leaf) + ListItem ( Reference ( 0 , place ( ... local: local ( 1 ) , projection: .Project + function: main + span: 97 + + +┌─ 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 5f36b155d..e6a92d2ad 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -56,6 +56,7 @@ 'transmute-u8-to-enum-fail', 'assert-inhabited-fail', 'iterator-simple', + 'closure-staged', 'unions-fail', 'transmute-maybe-uninit-fail', 'ptr-through-wrapper-fail', From f7fc5bbc6a37fbbed54f35b6f6e915826de1b8b3 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 6 Mar 2026 12:53:25 +0800 Subject: [PATCH 2/5] fix(rt): reduce aggregateKindClosure in mkAggregate --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 6 ++++++ .../data/prove-rs/show/closure-staged.main.expected | 8 ++++---- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 840ae6095..bcce7438b 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1051,6 +1051,12 @@ Literal arrays are also built using this RValue. ... + rule ARGS:List ~> #mkAggregate(aggregateKindClosure(_DEF, _TY_ARGS)) + => + Aggregate(variantIdx(0), ARGS) + ... + + // #readOperands accumulates a list of `TypedLocal` values from operands syntax KItem ::= #readOperands ( Operands ) diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected index 681632508..a8dc1d9d8 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected @@ -3,11 +3,11 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (33 steps) +│ (94 steps) └─ 3 (stuck, leaf) - ListItem ( Reference ( 0 , place ( ... local: local ( 1 ) , projection: .Project - function: main - span: 97 + #setTupleArgs ( 2 , Integer ( 41 , 8 , false ) ) +~> #execBlock ( basicBlock ( .. + span: 121 ┌─ 2 (root, leaf, target, terminal) From 0acd83912e95ab475d3e2c2e6dfe5397626f12e6 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 6 Mar 2026 12:57:26 +0800 Subject: [PATCH 3/5] fix(rt): add initial value fallback for setTupleArgs --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 5 ++ .../show/closure-staged.main.expected | 70 ++++++++++++++++--- 2 files changed, 67 insertions(+), 8 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 5a2b48c65..b141b0386 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -606,6 +606,11 @@ Therefore a heuristics is used here: // unpack tuple and set arguments individually rule #setTupleArgs(IDX, Aggregate(variantIdx(0), ARGS)) => #setTupleArgs(IDX, ARGS) ... + rule #setTupleArgs(IDX, VAL:Value) + => #setTupleArgs(IDX, ListItem(VAL)) + ... + + rule #setTupleArgs(_, .List ) => .K ... rule #setTupleArgs(IDX, ListItem(VAL) REST:List) diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected index a8dc1d9d8..8be60e4c0 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected @@ -3,14 +3,68 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (94 steps) -└─ 3 (stuck, leaf) - #setTupleArgs ( 2 , Integer ( 41 , 8 , false ) ) -~> #execBlock ( basicBlock ( .. - span: 121 +│ (72 steps) +├─ 3 +│ #setTupleArgs ( 2 , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 41 , 8 , +│ span: 73 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ #setTupleArgs ( 2 , ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer +┃ │ span: 73 +┃ │ +┃ │ (21 steps) +┃ ├─ 6 +┃ │ #setTupleArgs ( 2 , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 41 , 8 , +┃ │ span: 121 +┃ ┃ +┃ ┃ (1 step) +┃ ┣━━┓ +┃ ┃ │ +┃ ┃ ├─ 8 +┃ ┃ │ #setTupleArgs ( 2 , ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer +┃ ┃ │ span: 121 +┃ ┃ │ +┃ ┃ │ (23 steps) +┃ ┃ └─ 10 (stuck, leaf) +┃ ┃ #traverseProjection ( toLocal ( 3 ) , thunk ( #applyBinOp ( binOpAdd , Aggregate +┃ ┃ span: 121 +┃ ┃ +┃ ┗━━┓ +┃ │ +┃ ├─ 9 +┃ │ #setTupleArgs ( 2 , ListItem ( Integer ( 41 , 8 , false ) ) ) +~> #execBlock ( ba +┃ │ span: 121 +┃ │ +┃ │ (169 steps) +┃ ├─ 11 (terminal) +┃ │ #EndProgram ~> .K +┃ │ function: main +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + ├─ 5 + │ #setTupleArgs ( 2 , ListItem ( Integer ( 41 , 8 , false ) ) ) +~> #execBlock ( ba + │ span: 73 + │ + │ (191 steps) + ├─ 7 (terminal) + │ #EndProgram ~> .K + │ function: main + │ + ┊ constraint: true + ┊ subst: ... + └─ 2 (leaf, target, terminal) + #EndProgram ~> .K -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - From 491659c72eb71fec4bc9fb98a6f927f740cbd227 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 6 Mar 2026 13:01:30 +0800 Subject: [PATCH 4/5] fix(rt): finalize value fallback for setTupleArgs --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 2 +- .../show/closure-staged.main.expected | 71 +++---------------- 2 files changed, 10 insertions(+), 63 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index b141b0386..b85ee0002 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -609,7 +609,7 @@ Therefore a heuristics is used here: rule #setTupleArgs(IDX, VAL:Value) => #setTupleArgs(IDX, ListItem(VAL)) ... - + [owise] rule #setTupleArgs(_, .List ) => .K ... diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected index 8be60e4c0..2b759968f 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected @@ -3,68 +3,15 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (72 steps) -├─ 3 -│ #setTupleArgs ( 2 , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 41 , 8 , -│ span: 73 -┃ -┃ (1 step) -┣━━┓ -┃ │ -┃ ├─ 4 -┃ │ #setTupleArgs ( 2 , ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer -┃ │ span: 73 -┃ │ -┃ │ (21 steps) -┃ ├─ 6 -┃ │ #setTupleArgs ( 2 , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 41 , 8 , -┃ │ span: 121 -┃ ┃ -┃ ┃ (1 step) -┃ ┣━━┓ -┃ ┃ │ -┃ ┃ ├─ 8 -┃ ┃ │ #setTupleArgs ( 2 , ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer -┃ ┃ │ span: 121 -┃ ┃ │ -┃ ┃ │ (23 steps) -┃ ┃ └─ 10 (stuck, leaf) -┃ ┃ #traverseProjection ( toLocal ( 3 ) , thunk ( #applyBinOp ( binOpAdd , Aggregate -┃ ┃ span: 121 -┃ ┃ -┃ ┗━━┓ -┃ │ -┃ ├─ 9 -┃ │ #setTupleArgs ( 2 , ListItem ( Integer ( 41 , 8 , false ) ) ) -~> #execBlock ( ba -┃ │ span: 121 -┃ │ -┃ │ (169 steps) -┃ ├─ 11 (terminal) -┃ │ #EndProgram ~> .K -┃ │ function: main -┃ │ -┃ ┊ constraint: true -┃ ┊ subst: ... -┃ └─ 2 (leaf, target, terminal) -┃ #EndProgram ~> .K -┃ -┗━━┓ - │ - ├─ 5 - │ #setTupleArgs ( 2 , ListItem ( Integer ( 41 , 8 , false ) ) ) -~> #execBlock ( ba - │ span: 73 - │ - │ (191 steps) - ├─ 7 (terminal) - │ #EndProgram ~> .K - │ function: main - │ - ┊ constraint: true - ┊ subst: ... - └─ 2 (leaf, target, terminal) - #EndProgram ~> .K +│ (264 steps) +├─ 3 (terminal) +│ #EndProgram ~> .K +│ function: main +│ +┊ constraint: true +┊ subst: ... +└─ 2 (leaf, target, terminal) + #EndProgram ~> .K From a167b02ed8ffd7e6cee19d98bec8bf7b8c9bc39d Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 6 Mar 2026 13:02:59 +0800 Subject: [PATCH 5/5] test(integration): remove temporary closure show artifacts --- .../prove-rs/show/closure-staged.main.expected | 17 ----------------- kmir/src/tests/integration/test_integration.py | 1 - 2 files changed, 18 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected deleted file mode 100644 index 2b759968f..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/closure-staged.main.expected +++ /dev/null @@ -1,17 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (264 steps) -├─ 3 (terminal) -│ #EndProgram ~> .K -│ function: main -│ -┊ 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 e6a92d2ad..5f36b155d 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -56,7 +56,6 @@ 'transmute-u8-to-enum-fail', 'assert-inhabited-fail', 'iterator-simple', - 'closure-staged', 'unions-fail', 'transmute-maybe-uninit-fail', 'ptr-through-wrapper-fail',