Skip to content

Commit c1198df

Browse files
authored
Merge in latest master (#973)
- fix(rt): handle fun-type closure env refs in callee setup [956](#956) - fix(decode): accept signed enum tag scalars in _extract_tag [954](#954) - Added check for `FunType` in `setupCalleeClosure [969](#969)
2 parents c17566d + 7258cfb commit c1198df

13 files changed

Lines changed: 162 additions & 53 deletions

kmir/src/kmir/decoding.py

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -445,10 +445,12 @@ def _extract_tag(*, data: bytes, tag_offset: MachineSize, tag: Scalar) -> tuple[
445445
case Initialized(
446446
value=PrimitiveInt(
447447
length=length,
448-
signed=False,
448+
signed=_,
449449
),
450450
valid_range=_,
451451
):
452+
# Stable MIR enum discriminants are represented against the raw tag bits.
453+
# Use unsigned decoding even when the scalar metadata marks the tag as signed.
452454
tag_data = data[tag_offset.in_bytes : tag_offset.in_bytes + length.value]
453455
tag_value = int.from_bytes(tag_data, byteorder='little', signed=False)
454456
return tag_value, length

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

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -551,8 +551,10 @@ Therefore a heuristics is used here:
551551
andBool isTypedValue(LOCALS[TUPLE])
552552
andBool isTupleType(lookupTy(tyOfLocal({LOCALS[TUPLE]}:>TypedLocal)))
553553
andBool isTypedLocal(LOCALS[CLOSURE])
554-
andBool typeInfoVoidType ==K lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))
555-
// either the closure ref type is missing from type table
554+
andBool (
555+
typeInfoVoidType ==K lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))
556+
orBool isFunType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))
557+
)
556558
[priority(40), preserves-definedness]
557559
558560
rule [setupCalleeClosure2]: <k> #setUpCalleeData(
@@ -584,16 +586,22 @@ Therefore a heuristics is used here:
584586
// or the closure ref type pointee is missing from the type table
585587
andBool isRefType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))
586588
andBool isTy(pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))))
587-
andBool lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType
589+
andBool (
590+
lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType
591+
orBool isFunType(lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty))
592+
)
588593
[priority(45), preserves-definedness]
589594
590595
syntax Bool ::= isTupleType ( TypeInfo ) [function, total]
591596
| isRefType ( TypeInfo ) [function, total]
597+
| isFunType ( TypeInfo ) [function, total]
592598
// -------------------------------------------------------
593599
rule isTupleType(typeInfoTupleType(_, _)) => true
594600
rule isTupleType( _ ) => false [owise]
595601
rule isRefType(typeInfoRefType(_)) => true
596602
rule isRefType( _ ) => false [owise]
603+
rule isFunType(typeInfoFunType(_)) => true
604+
rule isFunType( _ ) => false [owise]
597605
598606
syntax KItem ::= #setTupleArgs ( Int , Value )
599607
| #setTupleArgs ( Int , List )

kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
┌─ 1 (root, init)
33
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
44
5-
│ (740 steps)
5+
│ (737 steps)
66
├─ 3 (terminal)
77
│ #EndProgram ~> .K
88
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Aggregate ( variantIdx ( 1 ) , .List )
Lines changed: 138 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,138 @@
1+
{
2+
"bytes": [
3+
0
4+
],
5+
"types": [],
6+
"typeInfo": {
7+
"EnumType": {
8+
"name": "OrderingLike",
9+
"adt_def": 72,
10+
"discriminants": [
11+
255,
12+
0,
13+
1
14+
],
15+
"fields": [
16+
[],
17+
[],
18+
[]
19+
],
20+
"layout": {
21+
"fields": {
22+
"Arbitrary": {
23+
"offsets": [
24+
{
25+
"num_bits": 0
26+
}
27+
]
28+
}
29+
},
30+
"variants": {
31+
"Multiple": {
32+
"tag": {
33+
"Initialized": {
34+
"value": {
35+
"Int": {
36+
"length": "I8",
37+
"signed": true
38+
}
39+
},
40+
"valid_range": {
41+
"start": 255,
42+
"end": 1
43+
}
44+
}
45+
},
46+
"tag_encoding": "Direct",
47+
"tag_field": 0,
48+
"variants": [
49+
{
50+
"fields": {
51+
"Arbitrary": {
52+
"offsets": []
53+
}
54+
},
55+
"variants": {
56+
"Single": {
57+
"index": 0
58+
}
59+
},
60+
"abi": {
61+
"Aggregate": {
62+
"sized": true
63+
}
64+
},
65+
"abi_align": 1,
66+
"size": {
67+
"num_bits": 8
68+
}
69+
},
70+
{
71+
"fields": {
72+
"Arbitrary": {
73+
"offsets": []
74+
}
75+
},
76+
"variants": {
77+
"Single": {
78+
"index": 1
79+
}
80+
},
81+
"abi": {
82+
"Aggregate": {
83+
"sized": true
84+
}
85+
},
86+
"abi_align": 1,
87+
"size": {
88+
"num_bits": 8
89+
}
90+
},
91+
{
92+
"fields": {
93+
"Arbitrary": {
94+
"offsets": []
95+
}
96+
},
97+
"variants": {
98+
"Single": {
99+
"index": 2
100+
}
101+
},
102+
"abi": {
103+
"Aggregate": {
104+
"sized": true
105+
}
106+
},
107+
"abi_align": 1,
108+
"size": {
109+
"num_bits": 8
110+
}
111+
}
112+
]
113+
}
114+
},
115+
"abi": {
116+
"Scalar": {
117+
"Initialized": {
118+
"value": {
119+
"Int": {
120+
"length": "I8",
121+
"signed": true
122+
}
123+
},
124+
"valid_range": {
125+
"start": 255,
126+
"end": 1
127+
}
128+
}
129+
}
130+
},
131+
"abi_align": 1,
132+
"size": {
133+
"num_bits": 8
134+
}
135+
}
136+
}
137+
}
138+
}

kmir/src/tests/integration/data/prove-rs/and_then_closure-fail.rs renamed to kmir/src/tests/integration/data/prove-rs/and_then_closure.rs

File renamed without changes.

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.
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
fn apply<F: FnOnce(u8, u8) -> u8>(f: F, a: u8, b: u8) -> u8 {
2+
f(a, b)
3+
}
4+
5+
fn main() {
6+
let result = apply(|x, y| x + y, 10, 32);
7+
assert_eq!(result, 42);
8+
}

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

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

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

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

0 commit comments

Comments
 (0)