Skip to content

Commit 2266b60

Browse files
Stevengreautomergerpr-permission-manager[bot]
Stevengre
and
automergerpr-permission-manager[bot]
authored
feat: tuple decoding with components (#826)
- Solve #822 --------- Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>
1 parent 9222a76 commit 2266b60

File tree

18 files changed

+323
-29
lines changed

18 files changed

+323
-29
lines changed

‎kmir/src/kmir/decoding.py‎

Lines changed: 16 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -191,8 +191,8 @@ def decode_value(data: bytes, type_info: TypeMetadata, types: Mapping[Ty, TypeMe
191191
return _decode_array(data, elem_ty, length, types)
192192
case StructT(fields=fields, layout=layout):
193193
return _decode_struct(data=data, fields=fields, layout=layout, types=types)
194-
case TupleT(components=components):
195-
return _decode_tuple(data=data, component_tys=components, types=types)
194+
case TupleT(components=components, layout=layout):
195+
return _decode_tuple(data=data, component_tys=components, layout=layout, types=types)
196196
case EnumT(
197197
discriminants=discriminants,
198198
fields=fields,
@@ -289,14 +289,27 @@ def _decode_tuple(
289289
*,
290290
data: bytes,
291291
component_tys: list[Ty],
292+
layout: LayoutShape | None,
292293
types: Mapping[Ty, TypeMetadata],
293294
) -> Value:
294295
if not component_tys:
295296
if data:
296297
raise ValueError(f'Zero-sized tuple expected empty data, got: {data!r}')
297298
return AggregateValue(0, [])
298299

299-
raise ValueError('Tuple decoding with components is not implemented yet')
300+
if not layout:
301+
raise ValueError('Tuple layout not provided')
302+
303+
offsets = _extract_offsets(layout.fields)
304+
305+
match layout.variants:
306+
case Single(index=0):
307+
pass
308+
case _:
309+
raise ValueError(f'Unexpected layout variants in tuple: {layout.variants}')
310+
311+
field_values = _decode_fields(data=data, tys=component_tys, offsets=offsets, types=types)
312+
return AggregateValue(0, field_values)
300313

301314

302315
def _decode_enum(

‎kmir/src/kmir/kast.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -428,7 +428,7 @@ def _symbolic_value(self, ty: Ty, mutable: bool) -> tuple[KInner, Iterable[KInne
428428
),
429429
)
430430

431-
case TupleT(components):
431+
case TupleT(components=components):
432432
elem_vars = []
433433
elem_constraints = []
434434
for _ty in components:

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -489,8 +489,8 @@ Therefore a heuristics is used here:
489489
syntax Bool ::= isTupleType ( TypeInfo ) [function, total]
490490
| isRefType ( TypeInfo ) [function, total]
491491
// -------------------------------------------------------
492-
rule isTupleType(typeInfoTupleType(_)) => true
493-
rule isTupleType( _ ) => false [owise]
492+
rule isTupleType(typeInfoTupleType(_, _)) => true
493+
rule isTupleType( _ ) => false [owise]
494494
rule isRefType(typeInfoRefType(_)) => true
495495
rule isRefType( _ ) => false [owise]
496496

‎kmir/src/kmir/kdist/mir-semantics/rt/data.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1554,7 +1554,7 @@ Zero-sized types can be decoded trivially into their respective representation.
15541554
rule <k> #decodeConstant(constantKindZeroSized, _TY, typeInfoStructType(_, _, _, _))
15551555
=> Aggregate(variantIdx(0), .List) ... </k>
15561556
// zero-sized tuple
1557-
rule <k> #decodeConstant(constantKindZeroSized, _TY, typeInfoTupleType(_))
1557+
rule <k> #decodeConstant(constantKindZeroSized, _TY, typeInfoTupleType(_, _))
15581558
=> Aggregate(variantIdx(0), .List) ... </k>
15591559
// zero-sized array
15601560
rule <k> #decodeConstant(constantKindZeroSized, _TY, typeInfoArrayType(_, _))

‎kmir/src/kmir/kdist/mir-semantics/rt/decoding.md‎

Lines changed: 28 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -86,10 +86,21 @@ When using layout offsets we always return fields in declaration order within th
8686
// ---------------------------------------------------------------------------
8787
// Use the offsets when they are provided and the input length is sufficient.
8888
rule #decodeValue(BYTES, typeInfoStructType(_, _, TYS, LAYOUT))
89-
=> Aggregate(variantIdx(0), #decodeStructFieldsWithOffsets(BYTES, TYS, #structOffsets(LAYOUT)))
90-
requires #structOffsets(LAYOUT) =/=K .MachineSizes
91-
andBool 0 <=Int #neededBytesForOffsets(TYS, #structOffsets(LAYOUT))
92-
andBool lengthBytes(BYTES) >=Int #neededBytesForOffsets(TYS, #structOffsets(LAYOUT))
89+
=> Aggregate(variantIdx(0), #decodeFieldsWithOffsets(BYTES, TYS, #layoutOffsets(LAYOUT)))
90+
requires #layoutOffsets(LAYOUT) =/=K .MachineSizes
91+
andBool 0 <=Int #neededBytesForOffsets(TYS, #layoutOffsets(LAYOUT))
92+
andBool lengthBytes(BYTES) >=Int #neededBytesForOffsets(TYS, #layoutOffsets(LAYOUT))
93+
[preserves-definedness]
94+
95+
rule #decodeValue(BYTES, typeInfoTupleType(.Tys, _))
96+
=> Aggregate(variantIdx(0), .List)
97+
requires lengthBytes(BYTES) ==Int 0
98+
99+
rule #decodeValue(BYTES, typeInfoTupleType(TYS, LAYOUT))
100+
=> Aggregate(variantIdx(0), #decodeFieldsWithOffsets(BYTES, TYS, #layoutOffsets(LAYOUT)))
101+
requires #layoutOffsets(LAYOUT) =/=K .MachineSizes
102+
andBool 0 <=Int #neededBytesForOffsets(TYS, #layoutOffsets(LAYOUT))
103+
andBool lengthBytes(BYTES) >=Int #neededBytesForOffsets(TYS, #layoutOffsets(LAYOUT))
93104
[preserves-definedness]
94105
95106
// ---------------------------------------------------------------------------
@@ -101,10 +112,10 @@ rule #msBytes(machineSize(mirInt(NBITS))) => NBITS /Int 8 [preserves-definedness
101112
rule #msBytes(machineSize(NBITS)) => NBITS /Int 8 [owise, preserves-definedness]
102113
103114
// Extract field offsets from the struct layout when available (Arbitrary only).
104-
syntax MachineSizes ::= #structOffsets ( MaybeLayoutShape ) [function, total]
105-
rule #structOffsets(someLayoutShape(layoutShape(fieldsShapeArbitrary(mk(OFFSETS)), _, _, _, _))) => OFFSETS
106-
rule #structOffsets(noLayoutShape) => .MachineSizes
107-
rule #structOffsets(_) => .MachineSizes [owise]
115+
syntax MachineSizes ::= #layoutOffsets ( MaybeLayoutShape ) [function, total]
116+
rule #layoutOffsets(someLayoutShape(layoutShape(fieldsShapeArbitrary(mk(OFFSETS)), _, _, _, _))) => OFFSETS
117+
rule #layoutOffsets(noLayoutShape) => .MachineSizes
118+
rule #layoutOffsets(_) => .MachineSizes [owise]
108119
109120
// Minimum number of input bytes required to decode all fields by the chosen offsets.
110121
// Uses builtin maxInt to compute max(offset + size). The lists of types and
@@ -118,17 +129,17 @@ rule #neededBytesForOffsets(TY TYS, OFFSET OFFSETS)
118129
rule #neededBytesForOffsets(_, _) => -1 [owise]
119130
120131
// Decode each field at its byte offset and return values in declaration order.
121-
syntax List ::= #decodeStructFieldsWithOffsets ( Bytes , Tys , MachineSizes ) [function, total]
122-
rule #decodeStructFieldsWithOffsets(_, .Tys, _OFFSETS) => .List
123-
rule #decodeStructFieldsWithOffsets(_, _TYS, .MachineSizes) => .List [owise]
124-
rule #decodeStructFieldsWithOffsets(BYTES, TY TYS, OFFSET OFFSETS)
132+
syntax List ::= #decodeFieldsWithOffsets ( Bytes , Tys , MachineSizes ) [function, total]
133+
rule #decodeFieldsWithOffsets(_, .Tys, _OFFSETS) => .List
134+
rule #decodeFieldsWithOffsets(_, _TYS, .MachineSizes) => .List [owise]
135+
rule #decodeFieldsWithOffsets(BYTES, TY TYS, OFFSET OFFSETS)
125136
=> ListItem(
126137
#decodeValue(
127138
substrBytes(BYTES, #msBytes(OFFSET), #msBytes(OFFSET) +Int #elemSize(lookupTy(TY))),
128139
lookupTy(TY)
129140
)
130141
)
131-
#decodeStructFieldsWithOffsets(BYTES, TYS, OFFSETS)
142+
#decodeFieldsWithOffsets(BYTES, TYS, OFFSETS)
132143
requires lengthBytes(BYTES) >=Int (#msBytes(OFFSET) +Int #elemSize(lookupTy(TY)))
133144
[preserves-definedness]
134145
```
@@ -182,10 +193,10 @@ Known element sizes for common types:
182193
[owise]
183194
184195
// ---- Tuples ----
185-
// Without layout, approximate as sum of element sizes (ignores padding).
186-
rule #elemSize(typeInfoTupleType(.Tys)) => 0
187-
rule #elemSize(typeInfoTupleType(TY TYS))
188-
=> #elemSize(lookupTy(TY)) +Int #elemSize(typeInfoTupleType(TYS))
196+
rule #elemSize(typeInfoTupleType(_TYS, someLayoutShape(layoutShape(_, _, _, _, SIZE)))) => #msBytes(SIZE)
197+
rule #elemSize(typeInfoTupleType(.Tys, noLayoutShape)) => 0
198+
rule #elemSize(typeInfoTupleType(TY TYS, noLayoutShape))
199+
=> #elemSize(lookupTy(TY)) +Int #elemSize(typeInfoTupleType(TYS, noLayoutShape))
189200
190201
// ---- Structs and Enums with layout ----
191202
rule #elemSize(typeInfoStructType(_, _, _, someLayoutShape(layoutShape(_, _, _, _, SIZE)))) => #msBytes(SIZE)

‎kmir/src/kmir/kdist/mir-semantics/rt/types.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -148,7 +148,7 @@ Slices, `str`s and dynamic types require it, and any `Ty` that `is_sized` does
148148
```k
149149
syntax Bool ::= #zeroSizedType ( TypeInfo ) [function, total]
150150
151-
rule #zeroSizedType(typeInfoTupleType(.Tys)) => true
151+
rule #zeroSizedType(typeInfoTupleType(.Tys, _)) => true
152152
rule #zeroSizedType(typeInfoStructType(_, _, .Tys, _)) => true
153153
rule #zeroSizedType(typeInfoVoidType) => true
154154
// FIXME: Only unit tuples, empty structs, and void are recognized here; other

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -274,7 +274,8 @@ syntax ExistentialPredicateBinders ::= List {ExistentialPredicateBinder, ""}
274274
| typeInfoArrayType(Ty, MaybeTyConst) [symbol(TypeInfo::ArrayType) , group(mir-enum---elem-type--size)]
275275
| typeInfoPtrType(Ty) [symbol(TypeInfo::PtrType) , group(mir-enum---pointee-type)]
276276
| typeInfoRefType(Ty) [symbol(TypeInfo::RefType) , group(mir-enum---pointee-type)]
277-
| typeInfoTupleType(Tys) [symbol(TypeInfo::TupleType) , group(mir-enum---types)]
277+
| typeInfoTupleType(types: Tys, layout: MaybeLayoutShape)
278+
[symbol(TypeInfo::TupleType) , group(mir-enum---types--layout)]
278279
| typeInfoFunType(MIRString) [symbol(TypeInfo::FunType) , group(mir-enum)]
279280
| "typeInfoVoidType" [symbol(TypeInfo::VoidType) , group(mir-enum)]
280281

‎kmir/src/kmir/ty.py‎

Lines changed: 29 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -620,19 +620,47 @@ def from_raw(data: Any) -> RefT:
620620
@dataclass
621621
class TupleT(TypeMetadata):
622622
components: list[Ty]
623+
layout: LayoutShape | None
623624

624625
@staticmethod
625626
def from_raw(data: Any) -> TupleT:
626627
match data:
628+
case {
629+
'TupleType': {
630+
'types': types,
631+
'layout': layout,
632+
}
633+
}:
634+
return TupleT(
635+
components=list(types),
636+
layout=LayoutShape.from_raw(layout) if layout is not None else None,
637+
)
627638
case {
628639
'TupleType': {
629640
'types': types,
630641
}
631642
}:
632-
return TupleT(list(types))
643+
return TupleT(
644+
components=list(types),
645+
layout=None,
646+
)
633647
case _:
634648
raise _cannot_parse_as('TupleT', data)
635649

650+
def nbytes(self, types: Mapping[Ty, TypeMetadata]) -> int:
651+
match self.layout:
652+
case None:
653+
total = 0
654+
for component in self.components:
655+
try:
656+
component_info = types[component]
657+
except KeyError as err:
658+
raise ValueError(f'Unknown tuple component type: {component}') from err
659+
total += component_info.nbytes(types)
660+
return total
661+
case LayoutShape(size=size):
662+
return size.in_bytes
663+
636664

637665
@dataclass
638666
class FunT(TypeMetadata):

‎kmir/src/tests/integration/data/decode-value/tuple-bool-u32.expected‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
Aggregate ( variantIdx ( 0 ) , ListItem ( BoolVal ( true ) )
2+
ListItem ( Integer ( 305419896 , 32 , false ) ) )

‎kmir/src/tests/integration/data/decode-value/tuple-bool-u32.json‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
{
2+
"bytes": [
3+
1,
4+
0,
5+
0,
6+
0,
7+
120,
8+
86,
9+
52,
10+
18
11+
],
12+
"types": [
13+
[
14+
1,
15+
{
16+
"PrimitiveType": "Bool"
17+
}
18+
],
19+
[
20+
4,
21+
{
22+
"PrimitiveType": {
23+
"Uint": "U32"
24+
}
25+
}
26+
]
27+
],
28+
"typeInfo": {
29+
"TupleType": {
30+
"types": [
31+
1,
32+
4
33+
],
34+
"layout": {
35+
"fields": {
36+
"Arbitrary": {
37+
"offsets": [
38+
{
39+
"num_bits": 0
40+
},
41+
{
42+
"num_bits": 32
43+
}
44+
]
45+
}
46+
},
47+
"variants": {
48+
"Single": {
49+
"index": 0
50+
}
51+
},
52+
"abi": {
53+
"Aggregate": {
54+
"sized": true
55+
}
56+
},
57+
"abi_align": 4,
58+
"size": {
59+
"num_bits": 64
60+
}
61+
}
62+
}
63+
}
64+
}

0 commit comments

Comments
 (0)