Skip to content

Commit ca11f30

Browse files
StevengreStevengre
authored
Merge branch 'master' into jh/align-transparent-place
2 parents 699f5dd + 2266b60 commit ca11f30

File tree

20 files changed

+361
-34
lines changed

20 files changed

+361
-34
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/lemmas/kmir-lemmas.md‎

Lines changed: 23 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -118,18 +118,39 @@ power of two but the semantics will always operate with these particular ones.
118118
rule VAL &Int bitmask128 => VAL requires 0 <=Int VAL andBool VAL <=Int bitmask128 [simplification, preserves-definedness, smt-lemma]
119119
```
120120

121+
Support for `transmute` between byte arrays and numbers (and vice-versa) uses computations involving bit masks with 255 and 8-bit shifts.
122+
To support simplifying round-trip conversion, the following simplifications are essential.
123+
121124
```k
122-
rule (VAL +Int 256 *Int REST) %Int 256 => VAL
125+
rule (VAL +Int 256 *Int REST) &Int 255 => VAL
123126
requires 0 <=Int VAL
124127
andBool VAL <=Int 255
125128
andBool 0 <=Int REST
126129
[simplification, preserves-definedness]
127130
128-
rule (VAL +Int 256 *Int REST) /Int 256 => REST
131+
rule (VAL +Int 256 *Int REST) >>Int 8 => REST
129132
requires 0 <=Int VAL
130133
andBool VAL <=Int 255
131134
andBool 0 <=Int REST
132135
[simplification, preserves-definedness]
136+
137+
rule (_ &Int 255) <=Int 255 => true
138+
[simplification, preserves-definedness]
139+
rule 0 <=Int (_ &Int 255) => true
140+
[simplification, preserves-definedness]
141+
142+
rule [simplify-u64-bytes-u64]:
143+
(VAL &Int 255) +Int (256 *Int (
144+
((VAL >>Int 8) &Int 255) +Int (256 *Int (
145+
((VAL >>Int 8 >>Int 8) &Int 255) +Int (256 *Int (
146+
((VAL >>Int 8 >>Int 8 >>Int 8) &Int 255) +Int (256 *Int (
147+
((VAL >>Int 8 >>Int 8 >>Int 8 >>Int 8) &Int 255) +Int (256 *Int (
148+
((VAL >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8) &Int 255) +Int (256 *Int (
149+
((VAL >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8) &Int 255) +Int (256 *Int (
150+
((VAL >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8) &Int 255)))))))))))))))
151+
=> VAL
152+
requires 0 <=Int VAL andBool VAL <=Int bitmask64
153+
[simplification, preserves-definedness, symbolic(VAL)]
133154
```
134155

135156

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1522,16 +1522,16 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes.
15221522
...
15231523
</k>
15241524
requires #isStaticU8Array(lookupTy(TY_TARGET))
1525-
andBool WIDTH >=Int 0
1526-
andBool WIDTH %Int 8 ==Int 0
15271525
andBool WIDTH ==Int #staticArrayLenBits(lookupTy(TY_TARGET))
1526+
// andBool WIDTH >=Int 0 ensured by the above
1527+
// andBool WIDTH % 8 == 0 ensured by the above
15281528
[preserves-definedness] // ensures element type/length are well-formed
15291529
15301530
syntax List ::= #littleEndianBytesFromInt ( Int, Int ) [function]
15311531
// -------------------------------------------------------------
15321532
rule #littleEndianBytesFromInt(VAL, WIDTH)
1533-
=> #littleEndianBytes(truncate(VAL, WIDTH, Unsigned), WIDTH /Int 8)
1534-
requires WIDTH %Int 8 ==Int 0
1533+
=> #littleEndianBytes(truncate(VAL, WIDTH, Unsigned), WIDTH >>Int 3)
1534+
requires WIDTH &Int 7 ==Int 0 // WIDTH % 8 == 0
15351535
andBool WIDTH >=Int 0
15361536
[preserves-definedness]
15371537
@@ -1542,7 +1542,7 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes.
15421542
requires COUNT <=Int 0
15431543
15441544
rule #littleEndianBytes(VAL, COUNT)
1545-
=> ListItem(Integer(VAL %Int 256, 8, false)) #littleEndianBytes(VAL /Int 256, COUNT -Int 1)
1545+
=> ListItem(Integer(VAL &Int 255, 8, false)) #littleEndianBytes(VAL >>Int 8, COUNT -Int 1)
15461546
requires COUNT >Int 0
15471547
[preserves-definedness]
15481548
@@ -1617,7 +1617,7 @@ Zero-sized types can be decoded trivially into their respective representation.
16171617
rule <k> #decodeConstant(constantKindZeroSized, _TY, typeInfoStructType(_, _, _, _))
16181618
=> Aggregate(variantIdx(0), .List) ... </k>
16191619
// zero-sized tuple
1620-
rule <k> #decodeConstant(constantKindZeroSized, _TY, typeInfoTupleType(_))
1620+
rule <k> #decodeConstant(constantKindZeroSized, _TY, typeInfoTupleType(_, _))
16211621
=> Aggregate(variantIdx(0), .List) ... </k>
16221622
// zero-sized array
16231623
rule <k> #decodeConstant(constantKindZeroSized, _TY, typeInfoArrayType(_, _))

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

Lines changed: 30 additions & 13 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
// ---------------------------------------------------------------------------
@@ -100,6 +111,12 @@ syntax Int ::= #msBytes ( MachineSize ) [function, total]
100111
rule #msBytes(machineSize(mirInt(NBITS))) => NBITS /Int 8 [preserves-definedness]
101112
rule #msBytes(machineSize(NBITS)) => NBITS /Int 8 [owise, preserves-definedness]
102113
114+
// Extract field offsets from the struct layout when available (Arbitrary only).
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]
119+
103120
// Minimum number of input bytes required to decode all fields by the chosen offsets.
104121
// Uses builtin maxInt to compute max(offset + size). The lists of types and
105122
// offsets must have the same length; if not, this function returns -1 to signal
@@ -112,17 +129,17 @@ rule #neededBytesForOffsets(TY TYS, OFFSET OFFSETS)
112129
rule #neededBytesForOffsets(_, _) => -1 [owise]
113130
114131
// Decode each field at its byte offset and return values in declaration order.
115-
syntax List ::= #decodeStructFieldsWithOffsets ( Bytes , Tys , MachineSizes ) [function, total]
116-
rule #decodeStructFieldsWithOffsets(_, .Tys, _OFFSETS) => .List
117-
rule #decodeStructFieldsWithOffsets(_, _TYS, .MachineSizes) => .List [owise]
118-
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)
119136
=> ListItem(
120137
#decodeValue(
121138
substrBytes(BYTES, #msBytes(OFFSET), #msBytes(OFFSET) +Int #elemSize(lookupTy(TY))),
122139
lookupTy(TY)
123140
)
124141
)
125-
#decodeStructFieldsWithOffsets(BYTES, TYS, OFFSETS)
142+
#decodeFieldsWithOffsets(BYTES, TYS, OFFSETS)
126143
requires lengthBytes(BYTES) >=Int (#msBytes(OFFSET) +Int #elemSize(lookupTy(TY)))
127144
[preserves-definedness]
128145
```
@@ -176,10 +193,10 @@ Known element sizes for common types:
176193
[owise]
177194
178195
// ---- Tuples ----
179-
// Without layout, approximate as sum of element sizes (ignores padding).
180-
rule #elemSize(typeInfoTupleType(.Tys)) => 0
181-
rule #elemSize(typeInfoTupleType(TY TYS))
182-
=> #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))
183200
184201
// ---- Structs and Enums with layout ----
185202
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
@@ -192,7 +192,7 @@ Slices, `str`s and dynamic types require it, and any `Ty` that `is_sized` does
192192
```k
193193
syntax Bool ::= #zeroSizedType ( TypeInfo ) [function, total]
194194
195-
rule #zeroSizedType(typeInfoTupleType(.Tys)) => true
195+
rule #zeroSizedType(typeInfoTupleType(.Tys, _)) => true
196196
rule #zeroSizedType(typeInfoStructType(_, _, .Tys, _)) => true
197197
rule #zeroSizedType(typeInfoVoidType) => true
198198
// 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 ) ) )

0 commit comments

Comments
 (0)