feat(rt): handle zero-sized locals (#809)

Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com>

Author: Stevengre

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,

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 <k> #setLocalValue(place(local(I), .ProjectionElems), VAL) => .K ... </k>
        <locals>
@@ -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 <k> #forceSetLocal(local(I), MBVAL) => .K ... </k>
+  rule <k> #forceSetLocal(local(I), MBVAL:Value) => .K ... </k>
        <locals> LOCALS => LOCALS[I <- typedValue(MBVAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityOf(getLocal(LOCALS, I)))] </locals>
     requires 0 <=Int I andBool I <Int size(LOCALS)
      andBool isTypedLocal(LOCALS[I])
@@ -1064,6 +1064,25 @@ This eliminates any `Deref` projections from the place, and also resolves `Index
   // rule #projectionsFor(CtxPointerOffset(OFFSET, ORIGIN_LENGTH) CTXS, PROJS) => #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 <k> 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))
+       ...
+       </k>
+       <locals> LOCALS </locals>
+    requires 0 <=Int I andBool I <Int size(LOCALS)
+     andBool isNewLocal(LOCALS[I])
+     andBool #zeroSizedType(lookupTy(tyOfLocal(getLocal(LOCALS, I))))
+    [preserves-definedness] // valid list indexing checked, zero-sized locals materialise trivially
+
   rule <k> 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

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
 ```

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 ) )
     </locals>

kmir/src/tests/integration/data/prove-rs/const-empty.rs

@@ -0,0 +1,6 @@
+const EMPTY: () = ();
+
+fn main() {
+    let e = ();
+    assert!(e == EMPTY);
+}

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

@@ -50,7 +50,6 @@
     'checked_arithmetic-fail',
     'offset-u8-fail',
     'pointer-cast-length-test-fail',
-    'closure_access_struct',
     'niche-enum',
     'assume-cheatcode-conflict-fail',
 ]