Skip to content

Commit 697e68a

Browse files
authored
fix(rt): handle fun-type closure env refs in callee setup (#956)
- Extend closure callee setup (`setupCalleeClosure2`) to accept closure-env references whose pointee resolves to `typeInfoFunType` (in addition to `typeInfoVoidType`). - Add `isFunType(TypeInfo)` helper predicate used by that guard. - In the fix commit, refresh `closure_access_struct-fail.main.expected` to show the behavior change from stuck frontier to terminal `#EndProgram`. - Cleanup after fix: - rename `closure_access_struct-fail.rs` -> `closure_access_struct.rs` - remove `show/closure_access_struct-fail.main.expected` - remove this case from `PROVE_RS_SHOW_SPECS`
1 parent 682df6b commit 697e68a

4 files changed

Lines changed: 7 additions & 17 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/closure_access_struct-fail.rs renamed to kmir/src/tests/integration/data/prove-rs/closure_access_struct.rs

File renamed without changes.

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

Lines changed: 0 additions & 15 deletions
This file was deleted.

kmir/src/tests/integration/test_integration.py

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,6 @@
6464
'ref-ptr-cast-elem-fail',
6565
'ref-ptr-cast-elem-offset-fail',
6666
'and_then_closure-fail',
67-
'closure_access_struct-fail',
6867
]
6968

7069

0 commit comments

Comments
 (0)