diff --git a/kmir/src/kmir/decoding.py b/kmir/src/kmir/decoding.py index 66a23e891..8171e0ea9 100644 --- a/kmir/src/kmir/decoding.py +++ b/kmir/src/kmir/decoding.py @@ -24,6 +24,7 @@ Single, StrT, StructT, + TupleT, UintT, WrappingRange, ) @@ -190,6 +191,8 @@ def decode_value(data: bytes, type_info: TypeMetadata, types: Mapping[Ty, TypeMe return _decode_array(data, elem_ty, length, types) case StructT(fields=fields, layout=layout): return _decode_struct(data=data, fields=fields, layout=layout, types=types) + case TupleT(components=components): + return _decode_tuple(data=data, component_tys=components, types=types) case EnumT( discriminants=discriminants, fields=fields, @@ -282,6 +285,20 @@ def _decode_struct( return AggregateValue(0, field_values) +def _decode_tuple( + *, + data: bytes, + component_tys: list[Ty], + types: Mapping[Ty, TypeMetadata], +) -> Value: + if not component_tys: + if data: + raise ValueError(f'Zero-sized tuple expected empty data, got: {data!r}') + return AggregateValue(0, []) + + raise ValueError('Tuple decoding with components is not implemented yet') + + def _decode_enum( *, data: bytes, diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 087af074d..8cbe5f2c0 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -172,7 +172,7 @@ A variant `#forceSetLocal` is provided for setting the local value without check ```k syntax KItem ::= #setLocalValue( Place, Evaluation ) [strict(2)] - | #forceSetLocal ( Local , Value ) + | #forceSetLocal ( Local , Evaluation ) [strict(2)] rule #setLocalValue(place(local(I), .ProjectionElems), VAL) => .K ... @@ -203,7 +203,7 @@ A variant `#forceSetLocal` is provided for setting the local value without check andBool isTypedValue(LOCALS[I]) [preserves-definedness] // valid list indexing and sort checked - rule #forceSetLocal(local(I), MBVAL) => .K ... + rule #forceSetLocal(local(I), MBVAL:Value) => .K ... LOCALS => LOCALS[I <- typedValue(MBVAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityOf(getLocal(LOCALS, I)))] requires 0 <=Int I andBool I #projectionsFor(CTXS, projectionElemSubslice(OFFSET, ORIGIN_LENGTH, false) PROJS) rule #projectionsFor(CtxPointerOffset( _, OFFSET, ORIGIN_LENGTH) CTXS, PROJS) => #projectionsFor(CTXS, PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS) + // Borrowing a zero-sized local that is still `NewLocal`: initialise it, then reuse the regular rule. + rule rvalueRef(REGION, KIND, place(local(I), PROJS)) + => #forceSetLocal( + local(I), + #decodeConstant( + constantKindZeroSized, + tyOfLocal(getLocal(LOCALS, I)), + lookupTy(tyOfLocal(getLocal(LOCALS, I))) + ) + ) + ~> rvalueRef(REGION, KIND, place(local(I), PROJS)) + ... + + LOCALS + requires 0 <=Int I andBool I rvalueRef(_REGION, KIND, place(local(I), PROJS)) => #traverseProjection(toLocal(I), getValue(LOCALS, I), PROJS, .Contexts) ~> #forRef(#mutabilityOf(KIND), metadata(#metadataSize(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS), 0, noMetadataSize)) // TODO: Sus on this rule diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/types.md b/kmir/src/kmir/kdist/mir-semantics/rt/types.md index b46ce90ff..5f6e92561 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/types.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/types.md @@ -143,6 +143,21 @@ Slices, `str`s and dynamic types require it, and any `Ty` that `is_sized` does [preserves-definedness] ``` +## Zero-sized types + +```k + syntax Bool ::= #zeroSizedType ( TypeInfo ) [function, total] + + rule #zeroSizedType(typeInfoTupleType(.Tys)) => true + rule #zeroSizedType(typeInfoStructType(_, _, .Tys, _)) => true + rule #zeroSizedType(typeInfoVoidType) => true + // FIXME: Only unit tuples, empty structs, and void are recognized here; other + // zero-sized types (e.g. single-variant enums, function or closure items, + // newtype wrappers around ZSTs) still fall through because we do not consult + // the layout metadata yet. Update once we rely on machineSize(0). + rule #zeroSizedType(_) => false [owise] +``` + ```k endmodule ``` diff --git a/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state b/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state index 9c598b715..db13358c2 100644 --- a/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state +++ b/kmir/src/tests/integration/data/exec-smir/call-with-args/closure-call.state @@ -32,15 +32,15 @@ ListItem ( typedValue ( Integer ( 32 , 32 , false ) , ty ( 25 ) , mutabilityNot ) ) ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) ) ) , ty ( 26 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 32 , 32 , false ) , ty ( 25 ) , mutabilityNot ) ) - ListItem ( newLocal ( ty ( 30 ) , mutabilityNot ) ) + ListItem ( typedValue ( thunk ( #decodeConstant ( constantKindZeroSized , ty ( 30 ) , typeInfoVoidType ) ) , ty ( 30 ) , mutabilityNot ) ) ListItem ( typedValue ( Integer ( 32 , 32 , false ) , ty ( 25 ) , mutabilityNot ) ) - ListItem ( typedValue ( thunk ( rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 4 ) , projection: .ProjectionElems ) ) ) , ty ( 31 ) , mutabilityMut ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 4 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 31 ) , mutabilityMut ) ) ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) ) ) , ty ( 26 ) , mutabilityMut ) ) ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) ) ListItem ( Integer ( 32 , 32 , false ) ) ) , ty ( 32 ) , mutabilityNot ) ) - ListItem ( newLocal ( ty ( 33 ) , mutabilityNot ) ) + ListItem ( typedValue ( thunk ( #decodeConstant ( constantKindZeroSized , ty ( 33 ) , typeInfoVoidType ) ) , ty ( 33 ) , mutabilityNot ) ) ListItem ( newLocal ( ty ( 1 ) , mutabilityNot ) ) - ListItem ( typedValue ( thunk ( rvalueRef ( region (... kind: regionKindReErased ) , borrowKindShared , place (... local: local ( 9 ) , projection: .ProjectionElems ) ) ) , ty ( 34 ) , mutabilityMut ) ) + ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 9 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 34 ) , mutabilityMut ) ) ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 32 , false ) ) ListItem ( Integer ( 32 , 32 , false ) ) ) , ty ( 32 ) , mutabilityMut ) ) diff --git a/kmir/src/tests/integration/data/prove-rs/const-empty.rs b/kmir/src/tests/integration/data/prove-rs/const-empty.rs new file mode 100644 index 000000000..97d09683e --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/const-empty.rs @@ -0,0 +1,6 @@ +const EMPTY: () = (); + +fn main() { + let e = (); + assert!(e == EMPTY); +} diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct.main.expected deleted file mode 100644 index 4777def47..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct.main.expected +++ /dev/null @@ -1,17 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (311 steps) -├─ 3 (terminal) -│ #EndProgram ~> .K -│ function: main -│ -┊ constraint: true -┊ subst: ... -└─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - - diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 2347ddc63..ae02d189d 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -50,7 +50,6 @@ 'checked_arithmetic-fail', 'offset-u8-fail', 'pointer-cast-length-test-fail', - 'closure_access_struct', 'niche-enum', 'assume-cheatcode-conflict-fail', ]