From e653715568ccb899a0ba41d26b945955aeb869d4 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 3 Mar 2026 18:07:13 +0800 Subject: [PATCH 1/2] fix(rt): recognize closure env refs in tuple-arg setup --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 8 +++++++- .../closure_access_struct-fail.main.expected | 16 +++++++++------- 2 files changed, 16 insertions(+), 8 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index ece4c9a3f..05df79d37 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -581,16 +581,22 @@ Therefore a heuristics is used here: // or the closure ref type pointee is missing from the type table andBool isRefType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))) andBool isTy(pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))) - andBool lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType + andBool ( + lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType + orBool isFunType(lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty)) + ) [priority(45), preserves-definedness] syntax Bool ::= isTupleType ( TypeInfo ) [function, total] | isRefType ( TypeInfo ) [function, total] + | isFunType ( TypeInfo ) [function, total] // ------------------------------------------------------- rule isTupleType(typeInfoTupleType(_, _)) => true rule isTupleType( _ ) => false [owise] rule isRefType(typeInfoRefType(_)) => true rule isRefType( _ ) => false [owise] + rule isFunType(typeInfoFunType(_)) => true + rule isFunType( _ ) => false [owise] syntax KItem ::= #setTupleArgs ( Int , Value ) | #setTupleArgs ( Int , List ) diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected index 8a1aff14b..876c733d8 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected @@ -3,13 +3,15 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (196 steps) -└─ 3 (stuck, leaf) - #traverseProjection ( toLocal ( 2 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( - span: 125 - - -┌─ 2 (root, leaf, target, terminal) +│ (313 steps) +├─ 3 (terminal) │ #EndProgram ~> .K +│ function: main +│ +┊ constraint: true +┊ subst: ... +└─ 2 (leaf, target, terminal) + #EndProgram ~> .K + From b46a5fe07410809096520feccc5cff15622705ae Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 4 Mar 2026 11:09:12 +0800 Subject: [PATCH 2/2] test(integration): rename closure_access_struct and remove show --- ..._struct-fail.rs => closure_access_struct.rs} | 0 .../closure_access_struct-fail.main.expected | 17 ----------------- kmir/src/tests/integration/test_integration.py | 1 - 3 files changed, 18 deletions(-) rename kmir/src/tests/integration/data/prove-rs/{closure_access_struct-fail.rs => closure_access_struct.rs} (100%) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/closure_access_struct-fail.rs b/kmir/src/tests/integration/data/prove-rs/closure_access_struct.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/closure_access_struct-fail.rs rename to kmir/src/tests/integration/data/prove-rs/closure_access_struct.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected deleted file mode 100644 index 876c733d8..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected +++ /dev/null @@ -1,17 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (313 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 8b1def7f8..a5f470208 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -64,7 +64,6 @@ 'ref-ptr-cast-elem-fail', 'ref-ptr-cast-elem-offset-fail', 'and_then_closure-fail', - 'closure_access_struct-fail', ]