Skip to content

Commit e653715

Browse files
committed
fix(rt): recognize closure env refs in tuple-arg setup
1 parent 682df6b commit e653715

2 files changed

Lines changed: 16 additions & 8 deletions

File tree

kmir/src/kmir/kdist/mir-semantics/kmir.md

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -581,16 +581,22 @@ Therefore a heuristics is used here:
581581
// or the closure ref type pointee is missing from the type table
582582
andBool isRefType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))
583583
andBool isTy(pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))))
584-
andBool lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType
584+
andBool (
585+
lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType
586+
orBool isFunType(lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty))
587+
)
585588
[priority(45), preserves-definedness]
586589
587590
syntax Bool ::= isTupleType ( TypeInfo ) [function, total]
588591
| isRefType ( TypeInfo ) [function, total]
592+
| isFunType ( TypeInfo ) [function, total]
589593
// -------------------------------------------------------
590594
rule isTupleType(typeInfoTupleType(_, _)) => true
591595
rule isTupleType( _ ) => false [owise]
592596
rule isRefType(typeInfoRefType(_)) => true
593597
rule isRefType( _ ) => false [owise]
598+
rule isFunType(typeInfoFunType(_)) => true
599+
rule isFunType( _ ) => false [owise]
594600
595601
syntax KItem ::= #setTupleArgs ( Int , Value )
596602
| #setTupleArgs ( Int , List )

kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,15 @@
33
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
44
│ span: 0
55
6-
│ (196 steps)
7-
└─ 3 (stuck, leaf)
8-
#traverseProjection ( toLocal ( 2 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
9-
span: 125
10-
11-
12-
┌─ 2 (root, leaf, target, terminal)
6+
│ (313 steps)
7+
├─ 3 (terminal)
138
│ #EndProgram ~> .K
9+
│ function: main
10+
11+
┊ constraint: true
12+
┊ subst: ...
13+
└─ 2 (leaf, target, terminal)
14+
#EndProgram ~> .K
15+
1416

1517

0 commit comments

Comments
 (0)