From fc12dccd7ff7eb033c07e8cfb35d593279ded3a2 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 6 Nov 2025 20:42:02 +0800 Subject: [PATCH 1/7] feat(rt): support zero-sized constant --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 7adc8dd0f..f9c04e046 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -128,6 +128,13 @@ Constant operands are simply decoded according to their type. ... requires typeInfoVoidType =/=K lookupTy(TY) + + // Fallback for zero-sized constants whose type metadata was not emitted. + rule operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, TY, _))) + => Aggregate(variantIdx(0), .List) + ... + + requires typeInfoVoidType ==K lookupTy(TY) ``` ### Copying and Moving From 389add9b5d0d3b81c4124ec03653f0afc54d8192 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 6 Nov 2025 21:21:01 +0800 Subject: [PATCH 2/7] fix(rt): Handle zero-sized locals on borrow --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 12 ++++++++++++ kmir/src/kmir/kdist/mir-semantics/rt/types.md | 15 +++++++++++++++ 2 files changed, 27 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index f9c04e046..59cd9dc45 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1087,6 +1087,18 @@ 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 rvalueRef(REGION, KIND, place(local(I), PROJS)) + => #forceSetLocal(local(I), Aggregate(variantIdx(0), .List)) + ~> 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 ``` From 94f30cc0b7dc998eb8476cc9558edca50474bb3a Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 10 Nov 2025 12:47:02 +0800 Subject: [PATCH 3/7] fix(rt): remove fallback for zero-sized constants type metadata --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 7 ------- 1 file changed, 7 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 704172261..5aa19f1d3 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -128,13 +128,6 @@ Constant operands are simply decoded according to their type. ... requires typeInfoVoidType =/=K lookupTy(TY) - - // Fallback for zero-sized constants whose type metadata was not emitted. - rule operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, TY, _))) - => Aggregate(variantIdx(0), .List) - ... - - requires typeInfoVoidType ==K lookupTy(TY) ``` ### Copying and Moving From b6736e2bfb68153f784848c10869e4d96d50cdea Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 10 Nov 2025 13:02:28 +0800 Subject: [PATCH 4/7] fix(rt): update #forceSetLocal to accept Evaluation type for local values --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 5aa19f1d3..32a848768 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 rvalueRef(REGION, KIND, place(local(I), PROJS)) - => #forceSetLocal(local(I), Aggregate(variantIdx(0), .List)) + => #forceSetLocal( + local(I), + #decodeConstant( + constantKindZeroSized, + tyOfLocal(getLocal(LOCALS, I)), + lookupTy(tyOfLocal(getLocal(LOCALS, I))) + ) + ) ~> rvalueRef(REGION, KIND, place(local(I), PROJS)) ... From 0e8c30ac560387e417f89dd7b476b0bb3ecde087 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 10 Nov 2025 14:10:24 +0800 Subject: [PATCH 5/7] feat(decoding): add tuple decoding support and implement _decode_tuple function --- kmir/src/kmir/decoding.py | 17 +++++++++++++++++ .../integration/data/prove-rs/const-empty.rs | 6 ++++++ 2 files changed, 23 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/const-empty.rs 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/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); +} From 497f3e76ecbc30e8f4ecc52dc0978139eb1aaafe Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 10 Nov 2025 15:16:40 +0800 Subject: [PATCH 6/7] fix(tests): don't show closure_access_struct test case --- .../show/closure_access_struct.main.expected | 17 ----------------- kmir/src/tests/integration/test_integration.py | 1 - 2 files changed, 18 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/closure_access_struct.main.expected 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', ] From 1c52f87ca81d155cd3176504ed731685b1671846 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 10 Nov 2025 15:20:14 +0800 Subject: [PATCH 7/7] fix: update expected output --- .../data/exec-smir/call-with-args/closure-call.state | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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 ) )