From 470f8578f43c86c6b47464c89dd2396e39552d4f Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 7 Nov 2025 11:19:34 +0800 Subject: [PATCH 1/4] docs(rt): Document pointer transmute behavior --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 22 ++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 9fd89c6a9..967d98c90 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1456,6 +1456,28 @@ What can be supported without additional layout consideration is trivial casts b requires lookupTy(TY_SOURCE) ==K lookupTy(TY_TARGET) ``` +Transmuting a pointer to an integer discards provenance and reinterprets the pointer’s offset as a value of the target integer type. + +```k + // `prove-rs/interior-mut3.rs` needs this + // TODO: check its correctness, I assume the pointer offset is the address here and we can use it to recover the PtrLocal + rule #cast( + PtrLocal(_, _, _, metadata(_, PTR_OFFSET, _)), + castKindTransmute, + _TY_SOURCE, + TY_TARGET + ) + => + #intAsType( + PTR_OFFSET, + #bitWidth(#numTypeOf(lookupTy(TY_TARGET))), + #numTypeOf(lookupTy(TY_TARGET)) + ) + ... + + requires #isIntType(lookupTy(TY_TARGET)) +``` + Other `Transmute` casts that can be resolved are round-trip casts from type A to type B and then directly back from B to A. The first cast is reified as a `thunk`, the second one resolves it and eliminates the `thunk`: From 04c66a60df67a75a88bd925efb4954521af582db Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 12 Nov 2025 18:07:50 +0800 Subject: [PATCH 2/4] feat: support roundtrip pointer <> int cast --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 78 +++-- .../kdist/mir-semantics/rt/pointer-int.md | 323 ++++++++++++++++++ .../data/prove-rs/ptr-int-transmute.rs | 14 + 3 files changed, 390 insertions(+), 25 deletions(-) create mode 100644 kmir/src/kmir/kdist/mir-semantics/rt/pointer-int.md create mode 100644 kmir/src/tests/integration/data/prove-rs/ptr-int-transmute.rs diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 967d98c90..bd705b9ed 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -10,6 +10,7 @@ requires "./types.md" requires "./value.md" requires "./numbers.md" requires "./decoding.md" +requires "./pointer-int.md" // pointer/int encoding helpers live separately for readability module RT-DATA imports INT @@ -27,6 +28,7 @@ module RT-DATA imports RT-NUMBERS imports RT-DECODING imports RT-TYPES + imports RT-POINTER-INT // shared pointer/int encoding + decoding helpers imports KMIR-CONFIGURATION ``` @@ -316,8 +318,6 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr | CtxSubslice( List , Int , Int ) // start and end always counted from beginning | CtxPointerOffset( List, Int, Int ) // pointer offset for accessing elements with an offset (Offset, Origin Length) - syntax ProjectionElem ::= PointerOffset( Int, Int ) // Same as subslice but coming from BinopOffset injected by us - syntax Contexts ::= List{Context, ""} syntax Value ::= #buildUpdate ( Value , Contexts ) [function] @@ -1456,28 +1456,6 @@ What can be supported without additional layout consideration is trivial casts b requires lookupTy(TY_SOURCE) ==K lookupTy(TY_TARGET) ``` -Transmuting a pointer to an integer discards provenance and reinterprets the pointer’s offset as a value of the target integer type. - -```k - // `prove-rs/interior-mut3.rs` needs this - // TODO: check its correctness, I assume the pointer offset is the address here and we can use it to recover the PtrLocal - rule #cast( - PtrLocal(_, _, _, metadata(_, PTR_OFFSET, _)), - castKindTransmute, - _TY_SOURCE, - TY_TARGET - ) - => - #intAsType( - PTR_OFFSET, - #bitWidth(#numTypeOf(lookupTy(TY_TARGET))), - #numTypeOf(lookupTy(TY_TARGET)) - ) - ... - - requires #isIntType(lookupTy(TY_TARGET)) -``` - Other `Transmute` casts that can be resolved are round-trip casts from type A to type B and then directly back from B to A. The first cast is reified as a `thunk`, the second one resolves it and eliminates the `thunk`: @@ -1582,6 +1560,56 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes. rule #staticArrayLenBits(_OTHER) => 0 [owise] ``` +Transmuting a raw pointer to an integer (and back) uses the reversible encoding defined in `RT-POINTER-INT`. +Keeping these helpers in a dedicated module keeps this file focused on semantics while still reusing the canonical encoding. +The encoding serialises the pointer provenance, its place/projection, mutability and metadata into a natural number; +decoding rehydrates the pointer metadata and reinterprets the byte offset for the target pointee type. + +```k + syntax Value ::= #ptrWithOffset ( Value , Int , TypeInfo ) [function, total] + rule #ptrWithOffset(PtrLocal(STACK, PLACE, MUT, metadata(SIZE, _, ORIGIN)), OFFSET, TYINFO) + => PtrLocal(STACK, PLACE, MUT, #convertMetadata(metadata(SIZE, OFFSET, ORIGIN), TYINFO)) + rule #ptrWithOffset(VAL:Value, _, _) => VAL [owise] +``` + +```k + rule #cast( + PtrLocal(_, _, _, _) #as PTR, + castKindTransmute, + TY_SOURCE, + TY_TARGET + ) + => + #ptrIntValue( + #encodePtrInt(PTR, pointeeTy(lookupTy(TY_SOURCE))), // full Cantor encoding + #numTypeOf(lookupTy(TY_TARGET)) // signedness + width + ) + ... + + requires #isIntType(lookupTy(TY_TARGET)) + andBool pointeeTy(lookupTy(TY_SOURCE)) =/=K TyUnknown + + rule #cast( + Integer(VAL, WIDTH, SIGNED) #as _INT, + castKindTransmute, + TY_SOURCE, + TY_TARGET + ) + => + #ptrWithOffset( + #decodePtrBase(#cantorUnpairLeft(#unsignedFromIntValue(VAL, WIDTH, SIGNED))), + #bytesToPtrOffset( + #cantorUnpairRight(#unsignedFromIntValue(VAL, WIDTH, SIGNED)), + pointeeTy(lookupTy(TY_TARGET)) + ), + lookupTy(TY_TARGET) + ) + ... + + requires #isIntType(lookupTy(TY_SOURCE)) + andBool pointeeTy(lookupTy(TY_TARGET)) =/=K TyUnknown +``` + A transmutation from an integer to an enum is wellformed if: - The bit width of the incoming integer is the same as the discriminant type of the enum (e.g. `u8 -> i8` fine, `u8 -> u16` not fine) - this is guaranteed by the compiler; @@ -2197,7 +2225,7 @@ A trivial case where `binOpOffset` applies an offset of `0` is added with higher _CHECKED) => PtrLocal( STACK_DEPTH , PLACE , MUT, metadata(CURRENT_SIZE, CURRENT_OFFSET +Int OFFSET_VAL, staticSize(ORIGIN_SIZE)) ) - requires OFFSET_VAL >=Int 0 + requires OFFSET_VAL >=Int 0 andBool CURRENT_OFFSET +Int OFFSET_VAL <=Int ORIGIN_SIZE [preserves-definedness] ``` diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/pointer-int.md b/kmir/src/kmir/kdist/mir-semantics/rt/pointer-int.md new file mode 100644 index 000000000..1808a01dc --- /dev/null +++ b/kmir/src/kmir/kdist/mir-semantics/rt/pointer-int.md @@ -0,0 +1,323 @@ +# Pointer/Integer Encoding Helpers + +This module defines the reversible encoding used for pointer/int transmutes. +We keep these helpers isolated from `RT-DATA` so GitHub reviews stay focused +on the semantics while still reusing exactly the same encoding/decoding logic. +The encoding works by flattening every pointer component into a single natural +number, using Cantor pairing to store the following pieces in order: + +1. Stack depth (`PtrLocal` provenance) +2. Place + projection list (locals, fields, etc.) +3. Mutability flag +4. Metadata triple (`MetadataSize`, pointer offset, original metadata) +5. Logical pointer offset converted into bytes when a pointee `Ty` is known + +Decoding simply applies the inverse Cantor functions to rebuild the original +`PtrLocal`, metadata, and projection structure before reinterpreting offsets. + +```k +requires "../body.md" +requires "./value.md" +requires "./types.md" +requires "./decoding.md" + +module RT-POINTER-INT + imports BOOL + imports INT + imports BODY + imports RT-VALUE-SYNTAX + imports RT-TYPES + imports RT-DECODING + + syntax ProjectionElem ::= PointerOffset( Int , Int ) + + syntax Int ::= #intToNat ( Int ) [function, total] + rule #intToNat(VAL) => 2 *Int VAL + requires VAL >=Int 0 + rule #intToNat(VAL) => 0 -Int (2 *Int VAL) -Int 1 + requires VAL N /Int 2 + requires N >=Int 0 + andBool N modInt 2 ==Int 0 + rule #natToInt(N) => 0 -Int ((N +Int 1) /Int 2) + requires N >=Int 0 + andBool N modInt 2 ==Int 1 + + syntax Int ::= #tri ( Int ) [function, total] + rule #tri(T) => (T *Int (T +Int 1)) /Int 2 + + syntax Int ::= #cantorPair ( Int , Int ) [function, total] + rule #cantorPair(A, B) + => ((A +Int B) *Int (A +Int B +Int 1)) /Int 2 +Int B + requires A >=Int 0 + andBool B >=Int 0 + + syntax Int ::= #cantorUnpairLeft ( Int ) [function, total] + syntax Int ::= #cantorUnpairRight( Int ) [function, total] + syntax Int ::= #cantorUnpairLeftAux ( Int , Int ) [function, total] + syntax Int ::= #cantorUnpairRightAux( Int , Int ) [function, total] + + rule #cantorUnpairLeft(Z) => #cantorUnpairLeftAux(Z, 0) + requires Z >=Int 0 + rule #cantorUnpairLeftAux(Z, T) + => T -Int (#tri(T) -Int Z) + requires Z #cantorUnpairLeftAux(Z, T +Int 1) + requires Z >=Int #tri(T) + + rule #cantorUnpairRight(Z) => #cantorUnpairRightAux(Z, 0) + requires Z >=Int 0 + rule #cantorUnpairRightAux(Z, T) + => Z -Int #tri(T) + requires Z #cantorUnpairRightAux(Z, T +Int 1) + requires Z >=Int #tri(T) + + syntax Int ::= #encodeBool ( Bool ) [function, total] + syntax Bool ::= #decodeBool ( Int ) [function, total] + rule #encodeBool(false) => 0 + rule #encodeBool(true) => 1 + rule #decodeBool(0) => false + rule #decodeBool(1) => true + rule #decodeBool(_) => false [owise] + + syntax Int ::= #encodeMIRBool ( MIRBool ) [function, total] + syntax MIRBool ::= #decodeMIRBool ( Int ) [function, total] + rule #encodeMIRBool(mirBool(B)) => #encodeBool(B) + rule #encodeMIRBool(_) => 0 [owise] + rule #decodeMIRBool(N) => mirBool(#decodeBool(N)) + + syntax Int ::= #encodeMIRInt ( MIRInt ) [function, total] + syntax MIRInt ::= #decodeMIRInt ( Int ) [function, total] + rule #encodeMIRInt(mirInt(I)) => #intToNat(I) + rule #encodeMIRInt(_) => 0 [owise] + rule #decodeMIRInt(N) => mirInt(#natToInt(N)) + + syntax Int ::= #encodeLocal ( Local ) [function, total] + syntax Local ::= #decodeLocal ( Int ) [function, total] + rule #encodeLocal(local(I)) => #intToNat(I) + rule #decodeLocal(N) => local(#natToInt(N)) + requires N >=Int 0 + + syntax Int ::= #encodeFieldIdx ( FieldIdx ) [function, total] + syntax FieldIdx ::= #decodeFieldIdx ( Int ) [function, total] + rule #encodeFieldIdx(fieldIdx(I)) => #intToNat(I) + rule #decodeFieldIdx(N) => fieldIdx(#natToInt(N)) + requires N >=Int 0 + + syntax Int ::= #encodeVariantIdx ( VariantIdx ) [function, total] + syntax VariantIdx ::= #decodeVariantIdx ( Int ) [function, total] + rule #encodeVariantIdx(variantIdx(I)) => #intToNat(I) + rule #encodeVariantIdx(_) => 0 [owise] + rule #decodeVariantIdx(N) => variantIdx(#natToInt(N)) + requires N >=Int 0 + + syntax Int ::= #encodeTy ( Ty ) [function, total] + syntax Ty ::= #decodeTy ( Int ) [function, total] + rule #encodeTy(ty(I)) => #intToNat(I) + rule #decodeTy(N) => ty(#natToInt(N)) + requires N >=Int 0 + + syntax Int ::= #encodeMutability ( Mutability ) [function, total] + syntax Mutability ::= #decodeMutability ( Int ) [function, total] + rule #encodeMutability(mutabilityNot) => 0 + rule #encodeMutability(mutabilityMut) => 1 + rule #decodeMutability(0) => mutabilityNot + rule #decodeMutability(1) => mutabilityMut + rule #decodeMutability(_) => mutabilityNot [owise] + + syntax Int ::= #encodeMetadataSize ( MetadataSize ) [function, total] + syntax MetadataSize ::= #decodeMetadataSize ( Int ) [function, total] + rule #encodeMetadataSize(noMetadataSize) => 0 + rule #encodeMetadataSize(staticSize(SIZE)) => 1 +Int #cantorPair(0, #intToNat(SIZE)) + rule #encodeMetadataSize(dynamicSize(SIZE)) => 1 +Int #cantorPair(1, #intToNat(SIZE)) + rule #decodeMetadataSize(0) => noMetadataSize + rule #decodeMetadataSize(ENC) + => staticSize(#natToInt(#cantorUnpairRight(ENC -Int 1))) + requires ENC >Int 0 + andBool #cantorUnpairLeft(ENC -Int 1) ==Int 0 + rule #decodeMetadataSize(ENC) + => dynamicSize(#natToInt(#cantorUnpairRight(ENC -Int 1))) + requires ENC >Int 0 + andBool #cantorUnpairLeft(ENC -Int 1) ==Int 1 + + syntax Int ::= #encodeMetadata ( Metadata ) [function, total] + syntax Metadata ::= #decodeMetadata ( Int ) [function, total] + rule #encodeMetadata(metadata(SIZE, PTR_OFFSET, ORIGIN)) + => #cantorPair( + #encodeMetadataSize(SIZE), + #cantorPair(#intToNat(PTR_OFFSET), #encodeMetadataSize(ORIGIN)) + ) + rule #decodeMetadata(ENC) + => metadata( + #decodeMetadataSize(#cantorUnpairLeft(ENC)), + #natToInt(#cantorUnpairLeft(#cantorUnpairRight(ENC))), + #decodeMetadataSize(#cantorUnpairRight(#cantorUnpairRight(ENC))) + ) + requires ENC >=Int 0 + + syntax Int ::= #encodeProjectionElem ( ProjectionElem ) [function, total] + syntax ProjectionElem ::= #decodeProjectionElem ( Int ) [function, total] + rule #encodeProjectionElem(projectionElemDeref) => 0 + rule #encodeProjectionElem(projectionElemField(FIELD, TY)) + => 1 +Int #cantorPair(0, #cantorPair(#encodeFieldIdx(FIELD), #encodeTy(TY))) + rule #encodeProjectionElem(projectionElemIndex(LOCAL)) + => 1 +Int #cantorPair(1, #encodeLocal(LOCAL)) + rule #encodeProjectionElem(projectionElemConstantIndex(OFFSET, MIN, FROM_END)) + => 1 +Int #cantorPair( + 2, + #cantorPair( + #encodeMIRInt(OFFSET), + #cantorPair(#encodeMIRInt(MIN), #encodeMIRBool(FROM_END)) + ) + ) + rule #encodeProjectionElem(projectionElemSubslice(FROM, TO, FROM_END)) + => 1 +Int #cantorPair( + 3, + #cantorPair( + #encodeMIRInt(FROM), + #cantorPair(#encodeMIRInt(TO), #encodeMIRBool(FROM_END)) + ) + ) + rule #encodeProjectionElem(projectionElemDowncast(VARIANT)) + => 1 +Int #cantorPair(4, #encodeVariantIdx(VARIANT)) + rule #encodeProjectionElem(projectionElemOpaqueCast(TY)) + => 1 +Int #cantorPair(5, #encodeTy(TY)) + rule #encodeProjectionElem(projectionElemSubtype(TY)) + => 1 +Int #cantorPair(6, #encodeTy(TY)) + rule #encodeProjectionElem(PointerOffset(OFFSET, LEN)) + => 1 +Int #cantorPair(7, #cantorPair(#intToNat(OFFSET), #intToNat(LEN))) + + rule #decodeProjectionElem(0) => projectionElemDeref + rule #decodeProjectionElem(ENC) + => projectionElemField( + #decodeFieldIdx(#cantorUnpairLeft(#cantorUnpairRight(ENC -Int 1))), + #decodeTy(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1))) + ) + requires ENC >Int 0 + andBool #cantorUnpairLeft(ENC -Int 1) ==Int 0 + rule #decodeProjectionElem(ENC) + => projectionElemIndex(#decodeLocal(#cantorUnpairRight(ENC -Int 1))) + requires ENC >Int 0 + andBool #cantorUnpairLeft(ENC -Int 1) ==Int 1 + rule #decodeProjectionElem(ENC) + => projectionElemConstantIndex( + #decodeMIRInt(#cantorUnpairLeft(#cantorUnpairRight(ENC -Int 1))), + #decodeMIRInt(#cantorUnpairLeft(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1)))), + #decodeMIRBool(#cantorUnpairRight(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1)))) + ) + requires ENC >Int 0 + andBool #cantorUnpairLeft(ENC -Int 1) ==Int 2 + rule #decodeProjectionElem(ENC) + => projectionElemSubslice( + #decodeMIRInt(#cantorUnpairLeft(#cantorUnpairRight(ENC -Int 1))), + #decodeMIRInt(#cantorUnpairLeft(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1)))), + #decodeMIRBool(#cantorUnpairRight(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1)))) + ) + requires ENC >Int 0 + andBool #cantorUnpairLeft(ENC -Int 1) ==Int 3 + rule #decodeProjectionElem(ENC) + => projectionElemDowncast(#decodeVariantIdx(#cantorUnpairRight(ENC -Int 1))) + requires ENC >Int 0 + andBool #cantorUnpairLeft(ENC -Int 1) ==Int 4 + rule #decodeProjectionElem(ENC) + => projectionElemOpaqueCast(#decodeTy(#cantorUnpairRight(ENC -Int 1))) + requires ENC >Int 0 + andBool #cantorUnpairLeft(ENC -Int 1) ==Int 5 + rule #decodeProjectionElem(ENC) + => projectionElemSubtype(#decodeTy(#cantorUnpairRight(ENC -Int 1))) + requires ENC >Int 0 + andBool #cantorUnpairLeft(ENC -Int 1) ==Int 6 + rule #decodeProjectionElem(ENC) + => PointerOffset( + #natToInt(#cantorUnpairLeft(#cantorUnpairRight(ENC -Int 1))), + #natToInt(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1))) + ) + requires ENC >Int 0 + + syntax Int ::= #encodeProjectionElems ( ProjectionElems ) [function, total] + syntax ProjectionElems ::= #decodeProjectionElems ( Int ) [function, total] + rule #encodeProjectionElems(.ProjectionElems) => 0 + rule #encodeProjectionElems(PROJ PROJS) + => 1 +Int #cantorPair(#encodeProjectionElem(PROJ), #encodeProjectionElems(PROJS)) + + rule #decodeProjectionElems(0) => .ProjectionElems + rule #decodeProjectionElems(ENC) + => #decodeProjectionElem(#cantorUnpairLeft(ENC -Int 1)) + #decodeProjectionElems(#cantorUnpairRight(ENC -Int 1)) + requires ENC >Int 0 + + syntax Int ::= #encodePlace ( Place ) [function, total] + syntax Place ::= #decodePlace ( Int ) [function, total] + rule #encodePlace(place(LOCAL, PROJS)) + => #cantorPair(#encodeLocal(LOCAL), #encodeProjectionElems(PROJS)) + rule #decodePlace(ENC) + => place( + #decodeLocal(#cantorUnpairLeft(ENC)), + #decodeProjectionElems(#cantorUnpairRight(ENC)) + ) + requires ENC >=Int 0 + + syntax Int ::= #encodePtrBase ( Value ) [function, total] + syntax Value ::= #decodePtrBase ( Int ) [function, total] + rule #encodePtrBase(PtrLocal(STACK, PLACE, MUT, META)) + => #cantorPair( + #intToNat(STACK), + #cantorPair( + #encodePlace(PLACE), + #cantorPair(#encodeMutability(MUT), #encodeMetadata(META)) + ) + ) + rule #encodePtrBase(_OTHER:Value) => 0 [owise] + + rule #decodePtrBase(ENC) + => PtrLocal( + #natToInt(#cantorUnpairLeft(ENC)), + #decodePlace(#cantorUnpairLeft(#cantorUnpairRight(ENC))), + #decodeMutability(#cantorUnpairLeft(#cantorUnpairRight(#cantorUnpairRight(ENC)))), + #decodeMetadata(#cantorUnpairRight(#cantorUnpairRight(ENC))) + ) + requires ENC >=Int 0 + + syntax Int ::= #ptrOffsetBytes ( Int , MaybeTy ) [function, total] + rule #ptrOffsetBytes(PTR_OFFSET, TyUnknown) => PTR_OFFSET + rule #ptrOffsetBytes(PTR_OFFSET, TY:Ty) => PTR_OFFSET *Int #elemSize(lookupTy(TY)) + + syntax Int ::= #bytesToPtrOffset ( Int , MaybeTy ) [function, total] + rule #bytesToPtrOffset(BYTES, TyUnknown) => BYTES + rule #bytesToPtrOffset(BYTES, TY:Ty) + => BYTES /Int #elemSize(lookupTy(TY)) + requires #elemSize(lookupTy(TY)) >Int 0 + andBool BYTES modInt #elemSize(lookupTy(TY)) ==Int 0 + + syntax Int ::= #encodePtrInt ( Value , MaybeTy ) [function, total] + rule #encodePtrInt(PtrLocal(STACK, PLACE, MUT, metadata(SIZE, PTR_OFFSET, ORIGIN)), TY) + => #cantorPair( + #encodePtrBase(PtrLocal(STACK, PLACE, MUT, metadata(SIZE, PTR_OFFSET, ORIGIN))), + #ptrOffsetBytes(PTR_OFFSET, TY) + ) + rule #encodePtrInt(_OTHER:Value, _) => 0 [owise] + + // Helper to materialise the Cantor-encoded pointer into either a signed or unsigned Integer. + syntax Value ::= #ptrIntValue ( Int , NumTy ) [function, total] + rule #ptrIntValue(ENC, INTTY:IntTy) + => Integer(ENC, #bitWidth(INTTY), true) + rule #ptrIntValue(ENC, UINTTY:UintTy) + => Integer(ENC, #bitWidth(UINTTY), false) + rule #ptrIntValue(_, FLOATTY:FloatTy) + => Integer(0, #bitWidth(FLOATTY), false) + rule #ptrIntValue(_, _) => Integer(0, 0, false) [owise] + + syntax Int ::= #unsignedFromIntValue ( Int , Int , Bool ) [function, total] + rule #unsignedFromIntValue(VAL, _WIDTH, _SIGNED) => VAL + requires VAL >=Int 0 + rule #unsignedFromIntValue(VAL, WIDTH, _SIGNED) + => VAL +Int (1 <(ptr) }; + + // Turn it back into a pointer, assuming round-trip soundness. + let restored_ptr = unsafe { transmute::(leaked_addr) }; + + assert_eq!(ptr, restored_ptr); +} From 27434bd8df9e5d36f2d6de1d8665e1f8250d78b9 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 17 Nov 2025 17:31:21 +0800 Subject: [PATCH 3/4] feat: don't want to make it complex --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 95 +++--- .../kdist/mir-semantics/rt/pointer-int.md | 323 ------------------ .../data/prove-rs/ptr-int-transmute.rs | 14 - .../show/interior-mut3-fail.main.expected | 56 +-- 4 files changed, 47 insertions(+), 441 deletions(-) delete mode 100644 kmir/src/kmir/kdist/mir-semantics/rt/pointer-int.md delete mode 100644 kmir/src/tests/integration/data/prove-rs/ptr-int-transmute.rs diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index bd705b9ed..2d7d6dea0 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -10,7 +10,6 @@ requires "./types.md" requires "./value.md" requires "./numbers.md" requires "./decoding.md" -requires "./pointer-int.md" // pointer/int encoding helpers live separately for readability module RT-DATA imports INT @@ -28,7 +27,6 @@ module RT-DATA imports RT-NUMBERS imports RT-DECODING imports RT-TYPES - imports RT-POINTER-INT // shared pointer/int encoding + decoding helpers imports KMIR-CONFIGURATION ``` @@ -318,6 +316,8 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr | CtxSubslice( List , Int , Int ) // start and end always counted from beginning | CtxPointerOffset( List, Int, Int ) // pointer offset for accessing elements with an offset (Offset, Origin Length) + syntax ProjectionElem ::= PointerOffset( Int, Int ) // Same as subslice but coming from BinopOffset injected by us + syntax Contexts ::= List{Context, ""} syntax Value ::= #buildUpdate ( Value , Contexts ) [function] @@ -1456,6 +1456,45 @@ What can be supported without additional layout consideration is trivial casts b requires lookupTy(TY_SOURCE) ==K lookupTy(TY_TARGET) ``` +Transmuting a pointer to an integer discards provenance and reinterprets the pointer’s offset as a value of the target integer type. + +```k + syntax Int ::= #ptrOffsetBytes ( Int , MaybeTy ) [function, total] + rule #ptrOffsetBytes(PTR_OFFSET, _TY:Ty) => 0 + requires PTR_OFFSET ==Int 0 + rule #ptrOffsetBytes(PTR_OFFSET, TY:Ty) + => PTR_OFFSET *Int #elemSize(#lookupMaybeTy(elemTy(lookupTy(TY)))) + requires PTR_OFFSET =/=Int 0 + andBool #isUnsizedArrayType(lookupTy(TY)) + rule #ptrOffsetBytes(_, _) => -1 [owise] // should not happen + + syntax Bool ::= #isUnsizedArrayType ( TypeInfo ) [function, total] + rule #isUnsizedArrayType(typeInfoArrayType(_, noTyConst)) => true + rule #isUnsizedArrayType(_) => false [owise] +``` + +```k + rule #cast( + PtrLocal(_, _, _, metadata(_, PTR_OFFSET, _)), + castKindTransmute, + TY_SOURCE, + TY_TARGET + ) + => + #intAsType( + #ptrOffsetBytes( + PTR_OFFSET, + pointeeTy(#lookupMaybeTy(TY_SOURCE)) + ), + #bitWidth(#numTypeOf(lookupTy(TY_TARGET))), + #numTypeOf(lookupTy(TY_TARGET)) + ) + ... + + requires #isIntType(lookupTy(TY_TARGET)) + andBool 0 <=Int #ptrOffsetBytes(PTR_OFFSET,pointeeTy(#lookupMaybeTy(TY_SOURCE))) +``` + Other `Transmute` casts that can be resolved are round-trip casts from type A to type B and then directly back from B to A. The first cast is reified as a `thunk`, the second one resolves it and eliminates the `thunk`: @@ -1560,56 +1599,6 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes. rule #staticArrayLenBits(_OTHER) => 0 [owise] ``` -Transmuting a raw pointer to an integer (and back) uses the reversible encoding defined in `RT-POINTER-INT`. -Keeping these helpers in a dedicated module keeps this file focused on semantics while still reusing the canonical encoding. -The encoding serialises the pointer provenance, its place/projection, mutability and metadata into a natural number; -decoding rehydrates the pointer metadata and reinterprets the byte offset for the target pointee type. - -```k - syntax Value ::= #ptrWithOffset ( Value , Int , TypeInfo ) [function, total] - rule #ptrWithOffset(PtrLocal(STACK, PLACE, MUT, metadata(SIZE, _, ORIGIN)), OFFSET, TYINFO) - => PtrLocal(STACK, PLACE, MUT, #convertMetadata(metadata(SIZE, OFFSET, ORIGIN), TYINFO)) - rule #ptrWithOffset(VAL:Value, _, _) => VAL [owise] -``` - -```k - rule #cast( - PtrLocal(_, _, _, _) #as PTR, - castKindTransmute, - TY_SOURCE, - TY_TARGET - ) - => - #ptrIntValue( - #encodePtrInt(PTR, pointeeTy(lookupTy(TY_SOURCE))), // full Cantor encoding - #numTypeOf(lookupTy(TY_TARGET)) // signedness + width - ) - ... - - requires #isIntType(lookupTy(TY_TARGET)) - andBool pointeeTy(lookupTy(TY_SOURCE)) =/=K TyUnknown - - rule #cast( - Integer(VAL, WIDTH, SIGNED) #as _INT, - castKindTransmute, - TY_SOURCE, - TY_TARGET - ) - => - #ptrWithOffset( - #decodePtrBase(#cantorUnpairLeft(#unsignedFromIntValue(VAL, WIDTH, SIGNED))), - #bytesToPtrOffset( - #cantorUnpairRight(#unsignedFromIntValue(VAL, WIDTH, SIGNED)), - pointeeTy(lookupTy(TY_TARGET)) - ), - lookupTy(TY_TARGET) - ) - ... - - requires #isIntType(lookupTy(TY_SOURCE)) - andBool pointeeTy(lookupTy(TY_TARGET)) =/=K TyUnknown -``` - A transmutation from an integer to an enum is wellformed if: - The bit width of the incoming integer is the same as the discriminant type of the enum (e.g. `u8 -> i8` fine, `u8 -> u16` not fine) - this is guaranteed by the compiler; @@ -2225,7 +2214,7 @@ A trivial case where `binOpOffset` applies an offset of `0` is added with higher _CHECKED) => PtrLocal( STACK_DEPTH , PLACE , MUT, metadata(CURRENT_SIZE, CURRENT_OFFSET +Int OFFSET_VAL, staticSize(ORIGIN_SIZE)) ) - requires OFFSET_VAL >=Int 0 + requires OFFSET_VAL >=Int 0 andBool CURRENT_OFFSET +Int OFFSET_VAL <=Int ORIGIN_SIZE [preserves-definedness] ``` diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/pointer-int.md b/kmir/src/kmir/kdist/mir-semantics/rt/pointer-int.md deleted file mode 100644 index 1808a01dc..000000000 --- a/kmir/src/kmir/kdist/mir-semantics/rt/pointer-int.md +++ /dev/null @@ -1,323 +0,0 @@ -# Pointer/Integer Encoding Helpers - -This module defines the reversible encoding used for pointer/int transmutes. -We keep these helpers isolated from `RT-DATA` so GitHub reviews stay focused -on the semantics while still reusing exactly the same encoding/decoding logic. -The encoding works by flattening every pointer component into a single natural -number, using Cantor pairing to store the following pieces in order: - -1. Stack depth (`PtrLocal` provenance) -2. Place + projection list (locals, fields, etc.) -3. Mutability flag -4. Metadata triple (`MetadataSize`, pointer offset, original metadata) -5. Logical pointer offset converted into bytes when a pointee `Ty` is known - -Decoding simply applies the inverse Cantor functions to rebuild the original -`PtrLocal`, metadata, and projection structure before reinterpreting offsets. - -```k -requires "../body.md" -requires "./value.md" -requires "./types.md" -requires "./decoding.md" - -module RT-POINTER-INT - imports BOOL - imports INT - imports BODY - imports RT-VALUE-SYNTAX - imports RT-TYPES - imports RT-DECODING - - syntax ProjectionElem ::= PointerOffset( Int , Int ) - - syntax Int ::= #intToNat ( Int ) [function, total] - rule #intToNat(VAL) => 2 *Int VAL - requires VAL >=Int 0 - rule #intToNat(VAL) => 0 -Int (2 *Int VAL) -Int 1 - requires VAL N /Int 2 - requires N >=Int 0 - andBool N modInt 2 ==Int 0 - rule #natToInt(N) => 0 -Int ((N +Int 1) /Int 2) - requires N >=Int 0 - andBool N modInt 2 ==Int 1 - - syntax Int ::= #tri ( Int ) [function, total] - rule #tri(T) => (T *Int (T +Int 1)) /Int 2 - - syntax Int ::= #cantorPair ( Int , Int ) [function, total] - rule #cantorPair(A, B) - => ((A +Int B) *Int (A +Int B +Int 1)) /Int 2 +Int B - requires A >=Int 0 - andBool B >=Int 0 - - syntax Int ::= #cantorUnpairLeft ( Int ) [function, total] - syntax Int ::= #cantorUnpairRight( Int ) [function, total] - syntax Int ::= #cantorUnpairLeftAux ( Int , Int ) [function, total] - syntax Int ::= #cantorUnpairRightAux( Int , Int ) [function, total] - - rule #cantorUnpairLeft(Z) => #cantorUnpairLeftAux(Z, 0) - requires Z >=Int 0 - rule #cantorUnpairLeftAux(Z, T) - => T -Int (#tri(T) -Int Z) - requires Z #cantorUnpairLeftAux(Z, T +Int 1) - requires Z >=Int #tri(T) - - rule #cantorUnpairRight(Z) => #cantorUnpairRightAux(Z, 0) - requires Z >=Int 0 - rule #cantorUnpairRightAux(Z, T) - => Z -Int #tri(T) - requires Z #cantorUnpairRightAux(Z, T +Int 1) - requires Z >=Int #tri(T) - - syntax Int ::= #encodeBool ( Bool ) [function, total] - syntax Bool ::= #decodeBool ( Int ) [function, total] - rule #encodeBool(false) => 0 - rule #encodeBool(true) => 1 - rule #decodeBool(0) => false - rule #decodeBool(1) => true - rule #decodeBool(_) => false [owise] - - syntax Int ::= #encodeMIRBool ( MIRBool ) [function, total] - syntax MIRBool ::= #decodeMIRBool ( Int ) [function, total] - rule #encodeMIRBool(mirBool(B)) => #encodeBool(B) - rule #encodeMIRBool(_) => 0 [owise] - rule #decodeMIRBool(N) => mirBool(#decodeBool(N)) - - syntax Int ::= #encodeMIRInt ( MIRInt ) [function, total] - syntax MIRInt ::= #decodeMIRInt ( Int ) [function, total] - rule #encodeMIRInt(mirInt(I)) => #intToNat(I) - rule #encodeMIRInt(_) => 0 [owise] - rule #decodeMIRInt(N) => mirInt(#natToInt(N)) - - syntax Int ::= #encodeLocal ( Local ) [function, total] - syntax Local ::= #decodeLocal ( Int ) [function, total] - rule #encodeLocal(local(I)) => #intToNat(I) - rule #decodeLocal(N) => local(#natToInt(N)) - requires N >=Int 0 - - syntax Int ::= #encodeFieldIdx ( FieldIdx ) [function, total] - syntax FieldIdx ::= #decodeFieldIdx ( Int ) [function, total] - rule #encodeFieldIdx(fieldIdx(I)) => #intToNat(I) - rule #decodeFieldIdx(N) => fieldIdx(#natToInt(N)) - requires N >=Int 0 - - syntax Int ::= #encodeVariantIdx ( VariantIdx ) [function, total] - syntax VariantIdx ::= #decodeVariantIdx ( Int ) [function, total] - rule #encodeVariantIdx(variantIdx(I)) => #intToNat(I) - rule #encodeVariantIdx(_) => 0 [owise] - rule #decodeVariantIdx(N) => variantIdx(#natToInt(N)) - requires N >=Int 0 - - syntax Int ::= #encodeTy ( Ty ) [function, total] - syntax Ty ::= #decodeTy ( Int ) [function, total] - rule #encodeTy(ty(I)) => #intToNat(I) - rule #decodeTy(N) => ty(#natToInt(N)) - requires N >=Int 0 - - syntax Int ::= #encodeMutability ( Mutability ) [function, total] - syntax Mutability ::= #decodeMutability ( Int ) [function, total] - rule #encodeMutability(mutabilityNot) => 0 - rule #encodeMutability(mutabilityMut) => 1 - rule #decodeMutability(0) => mutabilityNot - rule #decodeMutability(1) => mutabilityMut - rule #decodeMutability(_) => mutabilityNot [owise] - - syntax Int ::= #encodeMetadataSize ( MetadataSize ) [function, total] - syntax MetadataSize ::= #decodeMetadataSize ( Int ) [function, total] - rule #encodeMetadataSize(noMetadataSize) => 0 - rule #encodeMetadataSize(staticSize(SIZE)) => 1 +Int #cantorPair(0, #intToNat(SIZE)) - rule #encodeMetadataSize(dynamicSize(SIZE)) => 1 +Int #cantorPair(1, #intToNat(SIZE)) - rule #decodeMetadataSize(0) => noMetadataSize - rule #decodeMetadataSize(ENC) - => staticSize(#natToInt(#cantorUnpairRight(ENC -Int 1))) - requires ENC >Int 0 - andBool #cantorUnpairLeft(ENC -Int 1) ==Int 0 - rule #decodeMetadataSize(ENC) - => dynamicSize(#natToInt(#cantorUnpairRight(ENC -Int 1))) - requires ENC >Int 0 - andBool #cantorUnpairLeft(ENC -Int 1) ==Int 1 - - syntax Int ::= #encodeMetadata ( Metadata ) [function, total] - syntax Metadata ::= #decodeMetadata ( Int ) [function, total] - rule #encodeMetadata(metadata(SIZE, PTR_OFFSET, ORIGIN)) - => #cantorPair( - #encodeMetadataSize(SIZE), - #cantorPair(#intToNat(PTR_OFFSET), #encodeMetadataSize(ORIGIN)) - ) - rule #decodeMetadata(ENC) - => metadata( - #decodeMetadataSize(#cantorUnpairLeft(ENC)), - #natToInt(#cantorUnpairLeft(#cantorUnpairRight(ENC))), - #decodeMetadataSize(#cantorUnpairRight(#cantorUnpairRight(ENC))) - ) - requires ENC >=Int 0 - - syntax Int ::= #encodeProjectionElem ( ProjectionElem ) [function, total] - syntax ProjectionElem ::= #decodeProjectionElem ( Int ) [function, total] - rule #encodeProjectionElem(projectionElemDeref) => 0 - rule #encodeProjectionElem(projectionElemField(FIELD, TY)) - => 1 +Int #cantorPair(0, #cantorPair(#encodeFieldIdx(FIELD), #encodeTy(TY))) - rule #encodeProjectionElem(projectionElemIndex(LOCAL)) - => 1 +Int #cantorPair(1, #encodeLocal(LOCAL)) - rule #encodeProjectionElem(projectionElemConstantIndex(OFFSET, MIN, FROM_END)) - => 1 +Int #cantorPair( - 2, - #cantorPair( - #encodeMIRInt(OFFSET), - #cantorPair(#encodeMIRInt(MIN), #encodeMIRBool(FROM_END)) - ) - ) - rule #encodeProjectionElem(projectionElemSubslice(FROM, TO, FROM_END)) - => 1 +Int #cantorPair( - 3, - #cantorPair( - #encodeMIRInt(FROM), - #cantorPair(#encodeMIRInt(TO), #encodeMIRBool(FROM_END)) - ) - ) - rule #encodeProjectionElem(projectionElemDowncast(VARIANT)) - => 1 +Int #cantorPair(4, #encodeVariantIdx(VARIANT)) - rule #encodeProjectionElem(projectionElemOpaqueCast(TY)) - => 1 +Int #cantorPair(5, #encodeTy(TY)) - rule #encodeProjectionElem(projectionElemSubtype(TY)) - => 1 +Int #cantorPair(6, #encodeTy(TY)) - rule #encodeProjectionElem(PointerOffset(OFFSET, LEN)) - => 1 +Int #cantorPair(7, #cantorPair(#intToNat(OFFSET), #intToNat(LEN))) - - rule #decodeProjectionElem(0) => projectionElemDeref - rule #decodeProjectionElem(ENC) - => projectionElemField( - #decodeFieldIdx(#cantorUnpairLeft(#cantorUnpairRight(ENC -Int 1))), - #decodeTy(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1))) - ) - requires ENC >Int 0 - andBool #cantorUnpairLeft(ENC -Int 1) ==Int 0 - rule #decodeProjectionElem(ENC) - => projectionElemIndex(#decodeLocal(#cantorUnpairRight(ENC -Int 1))) - requires ENC >Int 0 - andBool #cantorUnpairLeft(ENC -Int 1) ==Int 1 - rule #decodeProjectionElem(ENC) - => projectionElemConstantIndex( - #decodeMIRInt(#cantorUnpairLeft(#cantorUnpairRight(ENC -Int 1))), - #decodeMIRInt(#cantorUnpairLeft(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1)))), - #decodeMIRBool(#cantorUnpairRight(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1)))) - ) - requires ENC >Int 0 - andBool #cantorUnpairLeft(ENC -Int 1) ==Int 2 - rule #decodeProjectionElem(ENC) - => projectionElemSubslice( - #decodeMIRInt(#cantorUnpairLeft(#cantorUnpairRight(ENC -Int 1))), - #decodeMIRInt(#cantorUnpairLeft(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1)))), - #decodeMIRBool(#cantorUnpairRight(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1)))) - ) - requires ENC >Int 0 - andBool #cantorUnpairLeft(ENC -Int 1) ==Int 3 - rule #decodeProjectionElem(ENC) - => projectionElemDowncast(#decodeVariantIdx(#cantorUnpairRight(ENC -Int 1))) - requires ENC >Int 0 - andBool #cantorUnpairLeft(ENC -Int 1) ==Int 4 - rule #decodeProjectionElem(ENC) - => projectionElemOpaqueCast(#decodeTy(#cantorUnpairRight(ENC -Int 1))) - requires ENC >Int 0 - andBool #cantorUnpairLeft(ENC -Int 1) ==Int 5 - rule #decodeProjectionElem(ENC) - => projectionElemSubtype(#decodeTy(#cantorUnpairRight(ENC -Int 1))) - requires ENC >Int 0 - andBool #cantorUnpairLeft(ENC -Int 1) ==Int 6 - rule #decodeProjectionElem(ENC) - => PointerOffset( - #natToInt(#cantorUnpairLeft(#cantorUnpairRight(ENC -Int 1))), - #natToInt(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1))) - ) - requires ENC >Int 0 - - syntax Int ::= #encodeProjectionElems ( ProjectionElems ) [function, total] - syntax ProjectionElems ::= #decodeProjectionElems ( Int ) [function, total] - rule #encodeProjectionElems(.ProjectionElems) => 0 - rule #encodeProjectionElems(PROJ PROJS) - => 1 +Int #cantorPair(#encodeProjectionElem(PROJ), #encodeProjectionElems(PROJS)) - - rule #decodeProjectionElems(0) => .ProjectionElems - rule #decodeProjectionElems(ENC) - => #decodeProjectionElem(#cantorUnpairLeft(ENC -Int 1)) - #decodeProjectionElems(#cantorUnpairRight(ENC -Int 1)) - requires ENC >Int 0 - - syntax Int ::= #encodePlace ( Place ) [function, total] - syntax Place ::= #decodePlace ( Int ) [function, total] - rule #encodePlace(place(LOCAL, PROJS)) - => #cantorPair(#encodeLocal(LOCAL), #encodeProjectionElems(PROJS)) - rule #decodePlace(ENC) - => place( - #decodeLocal(#cantorUnpairLeft(ENC)), - #decodeProjectionElems(#cantorUnpairRight(ENC)) - ) - requires ENC >=Int 0 - - syntax Int ::= #encodePtrBase ( Value ) [function, total] - syntax Value ::= #decodePtrBase ( Int ) [function, total] - rule #encodePtrBase(PtrLocal(STACK, PLACE, MUT, META)) - => #cantorPair( - #intToNat(STACK), - #cantorPair( - #encodePlace(PLACE), - #cantorPair(#encodeMutability(MUT), #encodeMetadata(META)) - ) - ) - rule #encodePtrBase(_OTHER:Value) => 0 [owise] - - rule #decodePtrBase(ENC) - => PtrLocal( - #natToInt(#cantorUnpairLeft(ENC)), - #decodePlace(#cantorUnpairLeft(#cantorUnpairRight(ENC))), - #decodeMutability(#cantorUnpairLeft(#cantorUnpairRight(#cantorUnpairRight(ENC)))), - #decodeMetadata(#cantorUnpairRight(#cantorUnpairRight(ENC))) - ) - requires ENC >=Int 0 - - syntax Int ::= #ptrOffsetBytes ( Int , MaybeTy ) [function, total] - rule #ptrOffsetBytes(PTR_OFFSET, TyUnknown) => PTR_OFFSET - rule #ptrOffsetBytes(PTR_OFFSET, TY:Ty) => PTR_OFFSET *Int #elemSize(lookupTy(TY)) - - syntax Int ::= #bytesToPtrOffset ( Int , MaybeTy ) [function, total] - rule #bytesToPtrOffset(BYTES, TyUnknown) => BYTES - rule #bytesToPtrOffset(BYTES, TY:Ty) - => BYTES /Int #elemSize(lookupTy(TY)) - requires #elemSize(lookupTy(TY)) >Int 0 - andBool BYTES modInt #elemSize(lookupTy(TY)) ==Int 0 - - syntax Int ::= #encodePtrInt ( Value , MaybeTy ) [function, total] - rule #encodePtrInt(PtrLocal(STACK, PLACE, MUT, metadata(SIZE, PTR_OFFSET, ORIGIN)), TY) - => #cantorPair( - #encodePtrBase(PtrLocal(STACK, PLACE, MUT, metadata(SIZE, PTR_OFFSET, ORIGIN))), - #ptrOffsetBytes(PTR_OFFSET, TY) - ) - rule #encodePtrInt(_OTHER:Value, _) => 0 [owise] - - // Helper to materialise the Cantor-encoded pointer into either a signed or unsigned Integer. - syntax Value ::= #ptrIntValue ( Int , NumTy ) [function, total] - rule #ptrIntValue(ENC, INTTY:IntTy) - => Integer(ENC, #bitWidth(INTTY), true) - rule #ptrIntValue(ENC, UINTTY:UintTy) - => Integer(ENC, #bitWidth(UINTTY), false) - rule #ptrIntValue(_, FLOATTY:FloatTy) - => Integer(0, #bitWidth(FLOATTY), false) - rule #ptrIntValue(_, _) => Integer(0, 0, false) [owise] - - syntax Int ::= #unsignedFromIntValue ( Int , Int , Bool ) [function, total] - rule #unsignedFromIntValue(VAL, _WIDTH, _SIGNED) => VAL - requires VAL >=Int 0 - rule #unsignedFromIntValue(VAL, WIDTH, _SIGNED) - => VAL +Int (1 <(ptr) }; - - // Turn it back into a pointer, assuming round-trip soundness. - let restored_ptr = unsafe { transmute::(leaked_addr) }; - - assert_eq!(ptr, restored_ptr); -} diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected index 5d1bd2ecc..80793fa28 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected @@ -3,57 +3,11 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (151 steps) -├─ 3 -│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th -│ function: main -┃ -┃ (1 step) -┣━━┓ -┃ │ -┃ ├─ 4 -┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC -┃ │ function: main -┃ │ -┃ │ (1 step) -┃ └─ 6 (stuck, leaf) -┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re -┃ function: main -┃ -┗━━┓ - │ - ├─ 5 - │ #execBlockIdx ( basicBlockIdx ( 8 ) ) ~> .K - │ function: main - │ - │ (111 steps) - ├─ 7 - │ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th - │ function: main - ┃ - ┃ (1 step) - ┣━━┓ - ┃ │ - ┃ ├─ 8 - ┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC - ┃ │ function: main - ┃ │ - ┃ │ (1 step) - ┃ └─ 10 (stuck, leaf) - ┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re - ┃ function: main - ┃ - ┗━━┓ - │ - ├─ 9 - │ #execBlockIdx ( basicBlockIdx ( 7 ) ) ~> .K - │ function: main - │ - │ (17 steps) - └─ 11 (stuck, leaf) - #setLocalValue ( place ( ... local: local ( 1 ) , projection: .ProjectionElems ) - function: main - span: 79 +│ (281 steps) +└─ 3 (stuck, leaf) + #setLocalValue ( place ( ... local: local ( 1 ) , projection: .ProjectionElems ) + function: main + span: 79 ┌─ 2 (root, leaf, target, terminal) From 236c2691b1bcba4a4146477b4ee5e1cd7fa2c1c9 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 17 Nov 2025 17:47:03 +0800 Subject: [PATCH 4/4] fix: update array type checks for pointer offset calculations --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 2d7d6dea0..ed9194065 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1465,12 +1465,12 @@ Transmuting a pointer to an integer discards provenance and reinterprets the poi rule #ptrOffsetBytes(PTR_OFFSET, TY:Ty) => PTR_OFFSET *Int #elemSize(#lookupMaybeTy(elemTy(lookupTy(TY)))) requires PTR_OFFSET =/=Int 0 - andBool #isUnsizedArrayType(lookupTy(TY)) + andBool #isArrayType(lookupTy(TY)) rule #ptrOffsetBytes(_, _) => -1 [owise] // should not happen - syntax Bool ::= #isUnsizedArrayType ( TypeInfo ) [function, total] - rule #isUnsizedArrayType(typeInfoArrayType(_, noTyConst)) => true - rule #isUnsizedArrayType(_) => false [owise] + syntax Bool ::= #isArrayType ( TypeInfo ) [function, total] + rule #isArrayType(typeInfoArrayType(_, _)) => true + rule #isArrayType(_) => false [owise] ``` ```k