Skip to content

Commit 1642b91

Browse files
StevengreStevengre
committed
feat: support roundtrip pointer <> int cast
1 parent 470f857 commit 1642b91

File tree

2 files changed

+365
-23
lines changed

2 files changed

+365
-23
lines changed

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

Lines changed: 351 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -1456,28 +1456,6 @@ What can be supported without additional layout consideration is trivial casts b
14561456
requires lookupTy(TY_SOURCE) ==K lookupTy(TY_TARGET)
14571457
```
14581458

1459-
Transmuting a pointer to an integer discards provenance and reinterprets the pointer’s offset as a value of the target integer type.
1460-
1461-
```k
1462-
// `prove-rs/interior-mut3.rs` needs this
1463-
// TODO: check its correctness, I assume the pointer offset is the address here and we can use it to recover the PtrLocal
1464-
rule <k> #cast(
1465-
PtrLocal(_, _, _, metadata(_, PTR_OFFSET, _)),
1466-
castKindTransmute,
1467-
_TY_SOURCE,
1468-
TY_TARGET
1469-
)
1470-
=>
1471-
#intAsType(
1472-
PTR_OFFSET,
1473-
#bitWidth(#numTypeOf(lookupTy(TY_TARGET))),
1474-
#numTypeOf(lookupTy(TY_TARGET))
1475-
)
1476-
...
1477-
</k>
1478-
requires #isIntType(lookupTy(TY_TARGET))
1479-
```
1480-
14811459
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.
14821460
The first cast is reified as a `thunk`, the second one resolves it and eliminates the `thunk`:
14831461

@@ -1582,6 +1560,50 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes.
15821560
rule #staticArrayLenBits(_OTHER) => 0 [owise]
15831561
```
15841562

1563+
Transmuting a raw pointer to an integer (and back) uses a reversible encoding that serialises the pointer provenance,
1564+
its place/projection, mutability and metadata into a natural number. The helpers that implement this encoding are
1565+
documented in the [Pointer/Integer Encoding Helpers](#pointerinteger-encoding-helpers) section at the end of this file.
1566+
The encoding must fit the destination integer width; decoding rehydrates the pointer metadata and reinterprets the
1567+
byte offset for the target pointee type.
1568+
1569+
```k
1570+
rule <k> #cast(
1571+
PtrLocal(_, _, _, _) #as PTR,
1572+
castKindTransmute,
1573+
TY_SOURCE,
1574+
TY_TARGET
1575+
)
1576+
=>
1577+
#ptrIntValue(
1578+
#encodePtrInt(PTR, pointeeTy(lookupTy(TY_SOURCE))),
1579+
#numTypeOf(lookupTy(TY_TARGET))
1580+
)
1581+
...
1582+
</k>
1583+
requires #isIntType(lookupTy(TY_TARGET))
1584+
andBool #isRawPointerType(lookupTy(TY_SOURCE))
1585+
1586+
rule <k> #cast(
1587+
Integer(VAL, WIDTH, SIGNED) #as _INT,
1588+
castKindTransmute,
1589+
TY_SOURCE,
1590+
TY_TARGET
1591+
)
1592+
=>
1593+
#ptrWithOffset(
1594+
#decodePtrBase(#cantorUnpairLeft(#unsignedFromIntValue(VAL, WIDTH, SIGNED))),
1595+
#bytesToPtrOffset(
1596+
#cantorUnpairRight(#unsignedFromIntValue(VAL, WIDTH, SIGNED)),
1597+
pointeeTy(lookupTy(TY_TARGET))
1598+
),
1599+
lookupTy(TY_TARGET)
1600+
)
1601+
...
1602+
</k>
1603+
requires #isIntType(lookupTy(TY_SOURCE))
1604+
andBool #isRawPointerType(lookupTy(TY_TARGET))
1605+
```
1606+
15851607
A transmutation from an integer to an enum is wellformed if:
15861608
- The bit width of the incoming integer is the same as the discriminant type of the enum
15871609
(e.g. `u8 -> i8` fine, `u8 -> u16` not fine) - this is guaranteed by the compiler;
@@ -2197,11 +2219,317 @@ A trivial case where `binOpOffset` applies an offset of `0` is added with higher
21972219
_CHECKED)
21982220
=>
21992221
PtrLocal( STACK_DEPTH , PLACE , MUT, metadata(CURRENT_SIZE, CURRENT_OFFSET +Int OFFSET_VAL, staticSize(ORIGIN_SIZE)) )
2200-
requires OFFSET_VAL >=Int 0
2222+
requires OFFSET_VAL >=Int 0
22012223
andBool CURRENT_OFFSET +Int OFFSET_VAL <=Int ORIGIN_SIZE
22022224
[preserves-definedness]
22032225
```
22042226

2227+
## Pointer/Integer Encoding Helpers
2228+
2229+
The pointer/int transmute rules rely on a reversible encoding that serialises all pointer components into a single
2230+
natural number. The encoding uses Cantor pairing/unpairing to store structured data (stack depth, place/projection,
2231+
mutability, metadata, byte offset). A small helper recognises raw pointer `TypeInfo`s so that these rules do not match
2232+
non-pointer transmutes.
2233+
2234+
```k
2235+
syntax Bool ::= #isRawPointerType ( TypeInfo ) [function, total]
2236+
rule #isRawPointerType(typeInfoPtrType(_)) => true
2237+
rule #isRawPointerType(_) => false [owise]
2238+
2239+
syntax Value ::= #ptrWithOffset ( Value , Int , TypeInfo ) [function, total]
2240+
rule #ptrWithOffset(PtrLocal(STACK, PLACE, MUT, metadata(SIZE, _, ORIGIN)), OFFSET, TYINFO)
2241+
=> PtrLocal(STACK, PLACE, MUT, #convertMetadata(metadata(SIZE, OFFSET, ORIGIN), TYINFO))
2242+
rule #ptrWithOffset(VAL:Value, _, _) => VAL [owise]
2243+
2244+
syntax Int ::= #encodePtrInt ( Value , MaybeTy ) [function, total]
2245+
rule #encodePtrInt(PtrLocal(STACK, PLACE, MUT, metadata(SIZE, PTR_OFFSET, ORIGIN)), TY)
2246+
=> #cantorPair(
2247+
#encodePtrBase(PtrLocal(STACK, PLACE, MUT, metadata(SIZE, PTR_OFFSET, ORIGIN))),
2248+
#ptrOffsetBytes(PTR_OFFSET, TY)
2249+
)
2250+
rule #encodePtrInt(_OTHER:Value, _) => 0 [owise]
2251+
2252+
syntax Value ::= #ptrIntValue ( Int , NumTy ) [function]
2253+
rule #ptrIntValue(ENC, INTTY:IntTy)
2254+
=> Integer(ENC, #bitWidth(INTTY), true)
2255+
rule #ptrIntValue(ENC, UINTTY:UintTy)
2256+
=> Integer(ENC, #bitWidth(UINTTY), false)
2257+
rule #ptrIntValue(_, FLOATTY:FloatTy)
2258+
=> Integer(0, #bitWidth(FLOATTY), false)
2259+
rule #ptrIntValue(_, _) => Integer(0, 0, false) [owise]
2260+
2261+
syntax Int ::= #unsignedFromIntValue ( Int , Int , Bool ) [function, total]
2262+
rule #unsignedFromIntValue(VAL, _WIDTH, _SIGNED) => VAL
2263+
requires VAL >=Int 0
2264+
rule #unsignedFromIntValue(VAL, WIDTH, _SIGNED)
2265+
=> VAL +Int (1 <<Int WIDTH)
2266+
requires VAL <Int 0
2267+
2268+
syntax Int ::= #intToNat ( Int ) [function, total]
2269+
rule #intToNat(VAL) => 2 *Int VAL
2270+
requires VAL >=Int 0
2271+
rule #intToNat(VAL) => 0 -Int (2 *Int VAL) -Int 1
2272+
requires VAL <Int 0
2273+
2274+
syntax Int ::= #natToInt ( Int ) [function, total]
2275+
rule #natToInt(N) => N /Int 2
2276+
requires N >=Int 0
2277+
andBool N modInt 2 ==Int 0
2278+
rule #natToInt(N) => 0 -Int ((N +Int 1) /Int 2)
2279+
requires N >=Int 0
2280+
andBool N modInt 2 ==Int 1
2281+
2282+
syntax Int ::= #tri ( Int ) [function, total]
2283+
rule #tri(T) => (T *Int (T +Int 1)) /Int 2
2284+
2285+
syntax Int ::= #cantorPair ( Int , Int ) [function, total]
2286+
rule #cantorPair(A, B)
2287+
=> ((A +Int B) *Int (A +Int B +Int 1)) /Int 2 +Int B
2288+
requires A >=Int 0
2289+
andBool B >=Int 0
2290+
2291+
syntax Int ::= #cantorUnpairLeft ( Int ) [function, total]
2292+
syntax Int ::= #cantorUnpairRight( Int ) [function, total]
2293+
syntax Int ::= #cantorUnpairLeftAux ( Int , Int ) [function, total]
2294+
syntax Int ::= #cantorUnpairRightAux( Int , Int ) [function, total]
2295+
2296+
rule #cantorUnpairLeft(Z) => #cantorUnpairLeftAux(Z, 0)
2297+
requires Z >=Int 0
2298+
rule #cantorUnpairLeftAux(Z, T)
2299+
=> T -Int (#tri(T) -Int Z)
2300+
requires Z <Int #tri(T)
2301+
rule #cantorUnpairLeftAux(Z, T)
2302+
=> #cantorUnpairLeftAux(Z, T +Int 1)
2303+
requires Z >=Int #tri(T)
2304+
2305+
rule #cantorUnpairRight(Z) => #cantorUnpairRightAux(Z, 0)
2306+
requires Z >=Int 0
2307+
rule #cantorUnpairRightAux(Z, T)
2308+
=> Z -Int #tri(T)
2309+
requires Z <Int #tri(T)
2310+
rule #cantorUnpairRightAux(Z, T)
2311+
=> #cantorUnpairRightAux(Z, T +Int 1)
2312+
requires Z >=Int #tri(T)
2313+
2314+
syntax Int ::= #encodeBool ( Bool ) [function, total]
2315+
syntax Bool ::= #decodeBool ( Int ) [function, total]
2316+
rule #encodeBool(false) => 0
2317+
rule #encodeBool(true) => 1
2318+
rule #decodeBool(0) => false
2319+
rule #decodeBool(1) => true
2320+
rule #decodeBool(_) => false [owise]
2321+
2322+
syntax Int ::= #encodeMIRBool ( MIRBool ) [function, total]
2323+
syntax MIRBool ::= #decodeMIRBool ( Int ) [function, total]
2324+
rule #encodeMIRBool(mirBool(B)) => #encodeBool(B)
2325+
rule #encodeMIRBool(_) => 0 [owise]
2326+
rule #decodeMIRBool(N) => mirBool(#decodeBool(N))
2327+
2328+
syntax Int ::= #encodeMIRInt ( MIRInt ) [function, total]
2329+
syntax MIRInt ::= #decodeMIRInt ( Int ) [function, total]
2330+
rule #encodeMIRInt(mirInt(I)) => #intToNat(I)
2331+
rule #encodeMIRInt(_) => 0 [owise]
2332+
rule #decodeMIRInt(N) => mirInt(#natToInt(N))
2333+
2334+
syntax Int ::= #encodeLocal ( Local ) [function, total]
2335+
syntax Local ::= #decodeLocal ( Int ) [function, total]
2336+
rule #encodeLocal(local(I)) => #intToNat(I)
2337+
rule #decodeLocal(N) => local(#natToInt(N))
2338+
requires N >=Int 0
2339+
2340+
syntax Int ::= #encodeFieldIdx ( FieldIdx ) [function, total]
2341+
syntax FieldIdx ::= #decodeFieldIdx ( Int ) [function, total]
2342+
rule #encodeFieldIdx(fieldIdx(I)) => #intToNat(I)
2343+
rule #decodeFieldIdx(N) => fieldIdx(#natToInt(N))
2344+
requires N >=Int 0
2345+
2346+
syntax Int ::= #encodeVariantIdx ( VariantIdx ) [function, total]
2347+
syntax VariantIdx ::= #decodeVariantIdx ( Int ) [function, total]
2348+
rule #encodeVariantIdx(variantIdx(I)) => #intToNat(I)
2349+
rule #encodeVariantIdx(_) => 0 [owise]
2350+
rule #decodeVariantIdx(N) => variantIdx(#natToInt(N))
2351+
requires N >=Int 0
2352+
2353+
syntax Int ::= #encodeTy ( Ty ) [function, total]
2354+
syntax Ty ::= #decodeTy ( Int ) [function, total]
2355+
rule #encodeTy(ty(I)) => #intToNat(I)
2356+
rule #decodeTy(N) => ty(#natToInt(N))
2357+
requires N >=Int 0
2358+
2359+
syntax Int ::= #encodeMutability ( Mutability ) [function, total]
2360+
syntax Mutability ::= #decodeMutability ( Int ) [function, total]
2361+
rule #encodeMutability(mutabilityNot) => 0
2362+
rule #encodeMutability(mutabilityMut) => 1
2363+
rule #decodeMutability(0) => mutabilityNot
2364+
rule #decodeMutability(1) => mutabilityMut
2365+
rule #decodeMutability(_) => mutabilityNot [owise]
2366+
2367+
syntax Int ::= #encodeMetadataSize ( MetadataSize ) [function, total]
2368+
syntax MetadataSize ::= #decodeMetadataSize ( Int ) [function, total]
2369+
rule #encodeMetadataSize(noMetadataSize) => 0
2370+
rule #encodeMetadataSize(staticSize(SIZE)) => 1 +Int #cantorPair(0, #intToNat(SIZE))
2371+
rule #encodeMetadataSize(dynamicSize(SIZE)) => 1 +Int #cantorPair(1, #intToNat(SIZE))
2372+
rule #decodeMetadataSize(0) => noMetadataSize
2373+
rule #decodeMetadataSize(ENC)
2374+
=> staticSize(#natToInt(#cantorUnpairRight(ENC -Int 1)))
2375+
requires ENC >Int 0
2376+
andBool #cantorUnpairLeft(ENC -Int 1) ==Int 0
2377+
rule #decodeMetadataSize(ENC)
2378+
=> dynamicSize(#natToInt(#cantorUnpairRight(ENC -Int 1)))
2379+
requires ENC >Int 0
2380+
andBool #cantorUnpairLeft(ENC -Int 1) ==Int 1
2381+
2382+
syntax Int ::= #encodeMetadata ( Metadata ) [function, total]
2383+
syntax Metadata ::= #decodeMetadata ( Int ) [function, total]
2384+
rule #encodeMetadata(metadata(SIZE, PTR_OFFSET, ORIGIN))
2385+
=> #cantorPair(
2386+
#encodeMetadataSize(SIZE),
2387+
#cantorPair(#intToNat(PTR_OFFSET), #encodeMetadataSize(ORIGIN))
2388+
)
2389+
rule #decodeMetadata(ENC)
2390+
=> metadata(
2391+
#decodeMetadataSize(#cantorUnpairLeft(ENC)),
2392+
#natToInt(#cantorUnpairLeft(#cantorUnpairRight(ENC))),
2393+
#decodeMetadataSize(#cantorUnpairRight(#cantorUnpairRight(ENC)))
2394+
)
2395+
requires ENC >=Int 0
2396+
2397+
syntax Int ::= #encodeProjectionElem ( ProjectionElem ) [function, total]
2398+
syntax ProjectionElem ::= #decodeProjectionElem ( Int ) [function, total]
2399+
rule #encodeProjectionElem(projectionElemDeref) => 0
2400+
rule #encodeProjectionElem(projectionElemField(FIELD, TY))
2401+
=> 1 +Int #cantorPair(0, #cantorPair(#encodeFieldIdx(FIELD), #encodeTy(TY)))
2402+
rule #encodeProjectionElem(projectionElemIndex(LOCAL))
2403+
=> 1 +Int #cantorPair(1, #encodeLocal(LOCAL))
2404+
rule #encodeProjectionElem(projectionElemConstantIndex(OFFSET, MIN, FROM_END))
2405+
=> 1 +Int #cantorPair(
2406+
2,
2407+
#cantorPair(
2408+
#encodeMIRInt(OFFSET),
2409+
#cantorPair(#encodeMIRInt(MIN), #encodeMIRBool(FROM_END))
2410+
)
2411+
)
2412+
rule #encodeProjectionElem(projectionElemSubslice(FROM, TO, FROM_END))
2413+
=> 1 +Int #cantorPair(
2414+
3,
2415+
#cantorPair(
2416+
#encodeMIRInt(FROM),
2417+
#cantorPair(#encodeMIRInt(TO), #encodeMIRBool(FROM_END))
2418+
)
2419+
)
2420+
rule #encodeProjectionElem(projectionElemDowncast(VARIANT))
2421+
=> 1 +Int #cantorPair(4, #encodeVariantIdx(VARIANT))
2422+
rule #encodeProjectionElem(projectionElemOpaqueCast(TY))
2423+
=> 1 +Int #cantorPair(5, #encodeTy(TY))
2424+
rule #encodeProjectionElem(projectionElemSubtype(TY))
2425+
=> 1 +Int #cantorPair(6, #encodeTy(TY))
2426+
rule #encodeProjectionElem(PointerOffset(OFFSET, LEN))
2427+
=> 1 +Int #cantorPair(7, #cantorPair(#intToNat(OFFSET), #intToNat(LEN)))
2428+
2429+
rule #decodeProjectionElem(0) => projectionElemDeref
2430+
rule #decodeProjectionElem(ENC)
2431+
=> projectionElemField(
2432+
#decodeFieldIdx(#cantorUnpairLeft(#cantorUnpairRight(ENC -Int 1))),
2433+
#decodeTy(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1)))
2434+
)
2435+
requires ENC >Int 0
2436+
andBool #cantorUnpairLeft(ENC -Int 1) ==Int 0
2437+
rule #decodeProjectionElem(ENC)
2438+
=> projectionElemIndex(#decodeLocal(#cantorUnpairRight(ENC -Int 1)))
2439+
requires ENC >Int 0
2440+
andBool #cantorUnpairLeft(ENC -Int 1) ==Int 1
2441+
rule #decodeProjectionElem(ENC)
2442+
=> projectionElemConstantIndex(
2443+
#decodeMIRInt(#cantorUnpairLeft(#cantorUnpairRight(ENC -Int 1))),
2444+
#decodeMIRInt(#cantorUnpairLeft(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1)))),
2445+
#decodeMIRBool(#cantorUnpairRight(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1))))
2446+
)
2447+
requires ENC >Int 0
2448+
andBool #cantorUnpairLeft(ENC -Int 1) ==Int 2
2449+
rule #decodeProjectionElem(ENC)
2450+
=> projectionElemSubslice(
2451+
#decodeMIRInt(#cantorUnpairLeft(#cantorUnpairRight(ENC -Int 1))),
2452+
#decodeMIRInt(#cantorUnpairLeft(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1)))),
2453+
#decodeMIRBool(#cantorUnpairRight(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1))))
2454+
)
2455+
requires ENC >Int 0
2456+
andBool #cantorUnpairLeft(ENC -Int 1) ==Int 3
2457+
rule #decodeProjectionElem(ENC)
2458+
=> projectionElemDowncast(#decodeVariantIdx(#cantorUnpairRight(ENC -Int 1)))
2459+
requires ENC >Int 0
2460+
andBool #cantorUnpairLeft(ENC -Int 1) ==Int 4
2461+
rule #decodeProjectionElem(ENC)
2462+
=> projectionElemOpaqueCast(#decodeTy(#cantorUnpairRight(ENC -Int 1)))
2463+
requires ENC >Int 0
2464+
andBool #cantorUnpairLeft(ENC -Int 1) ==Int 5
2465+
rule #decodeProjectionElem(ENC)
2466+
=> projectionElemSubtype(#decodeTy(#cantorUnpairRight(ENC -Int 1)))
2467+
requires ENC >Int 0
2468+
andBool #cantorUnpairLeft(ENC -Int 1) ==Int 6
2469+
rule #decodeProjectionElem(ENC)
2470+
=> PointerOffset(
2471+
#natToInt(#cantorUnpairLeft(#cantorUnpairRight(ENC -Int 1))),
2472+
#natToInt(#cantorUnpairRight(#cantorUnpairRight(ENC -Int 1)))
2473+
)
2474+
requires ENC >Int 0
2475+
andBool #cantorUnpairLeft(ENC -Int 1) ==Int 7
2476+
2477+
syntax Int ::= #encodeProjectionElems ( ProjectionElems ) [function, total]
2478+
syntax ProjectionElems ::= #decodeProjectionElems ( Int ) [function, total]
2479+
rule #encodeProjectionElems(.ProjectionElems) => 0
2480+
rule #encodeProjectionElems(PROJ PROJS)
2481+
=> 1 +Int #cantorPair(#encodeProjectionElem(PROJ), #encodeProjectionElems(PROJS))
2482+
2483+
rule #decodeProjectionElems(0) => .ProjectionElems
2484+
rule #decodeProjectionElems(ENC)
2485+
=> #decodeProjectionElem(#cantorUnpairLeft(ENC -Int 1))
2486+
#decodeProjectionElems(#cantorUnpairRight(ENC -Int 1))
2487+
requires ENC >Int 0
2488+
2489+
syntax Int ::= #encodePlace ( Place ) [function, total]
2490+
syntax Place ::= #decodePlace ( Int ) [function, total]
2491+
rule #encodePlace(place(LOCAL, PROJS))
2492+
=> #cantorPair(#encodeLocal(LOCAL), #encodeProjectionElems(PROJS))
2493+
rule #decodePlace(ENC)
2494+
=> place(
2495+
#decodeLocal(#cantorUnpairLeft(ENC)),
2496+
#decodeProjectionElems(#cantorUnpairRight(ENC))
2497+
)
2498+
requires ENC >=Int 0
2499+
2500+
syntax Int ::= #encodePtrBase ( Value ) [function, total]
2501+
syntax Value ::= #decodePtrBase ( Int ) [function, total]
2502+
rule #encodePtrBase(PtrLocal(STACK, PLACE, MUT, META))
2503+
=> #cantorPair(
2504+
#intToNat(STACK),
2505+
#cantorPair(
2506+
#encodePlace(PLACE),
2507+
#cantorPair(#encodeMutability(MUT), #encodeMetadata(META))
2508+
)
2509+
)
2510+
rule #encodePtrBase(_OTHER:Value) => 0 [owise]
2511+
2512+
rule #decodePtrBase(ENC)
2513+
=> PtrLocal(
2514+
#natToInt(#cantorUnpairLeft(ENC)),
2515+
#decodePlace(#cantorUnpairLeft(#cantorUnpairRight(ENC))),
2516+
#decodeMutability(#cantorUnpairLeft(#cantorUnpairRight(#cantorUnpairRight(ENC)))),
2517+
#decodeMetadata(#cantorUnpairRight(#cantorUnpairRight(ENC)))
2518+
)
2519+
requires ENC >=Int 0
2520+
2521+
syntax Int ::= #ptrOffsetBytes ( Int , MaybeTy ) [function, total]
2522+
rule #ptrOffsetBytes(PTR_OFFSET, TyUnknown) => PTR_OFFSET
2523+
rule #ptrOffsetBytes(PTR_OFFSET, TY:Ty) => PTR_OFFSET *Int #elemSize(lookupTy(TY))
2524+
2525+
syntax Int ::= #bytesToPtrOffset ( Int , MaybeTy ) [function, total]
2526+
rule #bytesToPtrOffset(BYTES, TyUnknown) => BYTES
2527+
rule #bytesToPtrOffset(BYTES, TY:Ty)
2528+
=> BYTES /Int #elemSize(lookupTy(TY))
2529+
requires #elemSize(lookupTy(TY)) >Int 0
2530+
andBool BYTES modInt #elemSize(lookupTy(TY)) ==Int 0
2531+
```
2532+
22052533
```k
22062534
endmodule
22072535
```

0 commit comments

Comments
 (0)