diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index 7268cf755..cdc86c4b3 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -215,8 +215,11 @@ def _make_symbolic_call_config( types: Mapping[Ty, TypeMetadata], ) -> tuple[KInner, list[KInner]]: locals, constraints = _symbolic_locals(fn_data.args, types) + init_config = definition.init_config(KSort('GeneratedTopCell')) + _, init_subst = split_config_from(init_config) subst = Subst( { + **init_subst, 'K_CELL': fn_data.call_terminator, 'STACK_CELL': list_empty(), # FIXME see #560, problems matching a symbolic stack 'LOCALS_CELL': list_of(locals), diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 82c28b3f0..da66849fb 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -225,6 +225,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f _ => CALLER // + _ => FRAMEID _ => #getBlocks(CALLER) CALLER => NEWCALLER DEST => NEWDEST @@ -233,7 +234,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f ListItem(typedValue(VAL:Value, _, _)) _ => NEWLOCALS // // remaining call stack (without top frame) - ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK + ListItem(StackFrame(FRAMEID, NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK // no value to return, skip writing rule [termReturnNone]: #execTerminator(terminator(terminatorKindReturn, _SPAN)) ~> _ @@ -242,6 +243,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f _ => CALLER // + _ => FRAMEID _ => #getBlocks(CALLER) CALLER => NEWCALLER _ => NEWDEST @@ -250,7 +252,7 @@ If the local `_0` does not have a value (i.e., it remained uninitialised), the f ListItem(_:NewLocal) _ => NEWLOCALS // // remaining call stack (without top frame) - ListItem(StackFrame(NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK + ListItem(StackFrame(FRAMEID, NEWCALLER, NEWDEST, NEWTARGET, UNWIND, NEWLOCALS)) STACK => STACK syntax List ::= #getBlocks( Ty ) [function, total] | #getBlocksAux( MonoItemKind ) [function, total] @@ -356,6 +358,7 @@ where the returned result should go. CALLER => FTY + OLDFRAMEID => NEWFRAMEID _ OLDCALLER => CALLER OLDDEST => DEST @@ -363,7 +366,8 @@ where the returned result should go. OLDUNWIND => UNWIND LOCALS - STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK + STACK => ListItem(StackFrame(OLDFRAMEID, OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK + NEWFRAMEID => NEWFRAMEID +Int 1 requires notBool isIntrinsicFunction(FUNC) andBool notBool #functionNameMatchesEnv(getFunctionName(FUNC)) @@ -374,6 +378,7 @@ where the returned result should go. CALLER => FTY + OLDFRAMEID => NEWFRAMEID _ OLDCALLER => CALLER OLDDEST => DEST @@ -381,7 +386,8 @@ where the returned result should go. OLDUNWIND => UNWIND LOCALS - STACK => ListItem(StackFrame(OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK + STACK => ListItem(StackFrame(OLDFRAMEID, OLDCALLER, OLDDEST, OLDTARGET, OLDUNWIND, LOCALS)) STACK + NEWFRAMEID => NEWFRAMEID +Int 1 requires notBool isIntrinsicFunction(FUNC) andBool #functionNameMatchesEnv(getFunctionName(FUNC)) @@ -498,7 +504,7 @@ An operand may be a `Reference` (the only way a function could access another fu #setLocalValue(place(local(IDX), .ProjectionElems), #incrementRef(getValue(CALLERLOCALS, I))) ... - ListItem(StackFrame(_, _, _, _, CALLERLOCALS)) _:List + ListItem(StackFrame(_, _, _, _, _, CALLERLOCALS)) _:List requires 0 <=Int I andBool I - (ListItem(StackFrame(_, _, _, _, CALLERLOCALS) #as CALLERFRAME => #updateStackLocal(CALLERFRAME, I, Moved))) _:List + (ListItem(StackFrame(_, _, _, _, _, CALLERLOCALS) #as CALLERFRAME => #updateStackLocal(CALLERFRAME, I, Moved))) _:List requires 0 <=Int I andBool I ty(-1) // to retrieve caller // unpacking the top frame to avoid frequent stack read/write operations + 0 .List ty(-1) place(local(-1), .ProjectionElems) @@ -45,6 +49,11 @@ module KMIR-CONFIGURATION // remaining call stack (without top frame) .List + 1 + // address allocation model for pointer-to-integer casts + .Map + 4096 + .Set ``` diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 5839521b4..7360aa4ca 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -18,6 +18,7 @@ module RT-DATA imports BYTES imports LIST imports MAP + imports SET imports K-EQUAL imports BODY @@ -362,13 +363,105 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr syntax StackFrame ::= #updateStackLocal ( StackFrame, Int, Value ) [function] - rule #updateStackLocal(StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS), I, VAL) - => StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS[I <- typedValue(VAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityMut)]) + rule #updateStackLocal(StackFrame(FRAMEID, CALLER, DEST, TARGET, UNWIND, LOCALS), I, VAL) + => StackFrame(FRAMEID, CALLER, DEST, TARGET, UNWIND, LOCALS[I <- typedValue(VAL, tyOfLocal(getLocal(LOCALS, I)), mutabilityMut)]) requires 0 <=Int I andBool I FRAMEID + + syntax Int ::= #stackFrameId ( Int , Int , List ) [function, total] + // ---------------------------------------------------------------- + rule #stackFrameId(0, CURRENT_FRAME_ID, _STACK) => CURRENT_FRAME_ID + rule #stackFrameId(OFFSET, _CURRENT_FRAME_ID, STACK) + => #frameIdOf({STACK[OFFSET -Int 1]}:>StackFrame) + requires 0 -1 [owise] + + syntax AllocKey ::= #stackAllocKey ( Int , Local , Int , List ) [function, total] + // --------------------------------------------------------------------------- + rule #stackAllocKey(STACK_DEPTH, LOCAL, CURRENT_FRAME_ID, STACK) + => allocKey(#stackFrameId(STACK_DEPTH, CURRENT_FRAME_ID, STACK), LOCAL) + + syntax ProjectionElems ::= #addressProjs ( ProjectionElems ) [function, total] + // ----------------------------------------------------------------------- + rule #addressProjs(.ProjectionElems) => .ProjectionElems + rule #addressProjs(projectionElemToZST REST) => #addressProjs(REST) + rule #addressProjs(projectionElemFromZST REST) => #addressProjs(REST) + rule #addressProjs(projectionElemWrapStruct REST) => #addressProjs(REST) + rule #addressProjs(PROJ REST) => PROJ #addressProjs(REST) [owise] + + syntax MaybeTy ::= #stackAllocTy ( Int , Local , List , List ) [function, total] + | #stackAllocTyInStack ( Int , Local , List ) [function, total] + | #ptrBaseElemTy ( Int , Local , ProjectionElems , List , List ) [function, total] + | #ptrBaseElemTyInStack ( Int , Local , ProjectionElems , List ) [function, total] + // ---------------------------------------------------------------------------------------------------------------- + rule #stackAllocTy(0, local(I:Int), LOCALS, _STACK) + => tyOfLocal({LOCALS[I]}:>TypedLocal) + requires 0 <=Int I + andBool I #stackAllocTyInStack(OFFSET, LOCAL, STACK) + requires 0 tyOfLocal({FRAMELOCALS[I]}:>TypedLocal) + requires 0 <=Int I + andBool I #stackAllocTyInStack(OFFSET -Int 1, LOCAL, REST) + requires 1 TyUnknown [owise] + rule #stackAllocTyInStack(_, _, _) => TyUnknown [owise] + + rule #ptrBaseElemTy(0, local(I:Int), PROJS, LOCALS, _STACK) + => getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), #addressProjs(PROJS)) + requires 0 <=Int I + andBool I #ptrBaseElemTyInStack(OFFSET, LOCAL, PROJS, STACK) + requires 0 getTyOf(tyOfLocal({FRAMELOCALS[I]}:>TypedLocal), #addressProjs(PROJS)) + requires 0 <=Int I + andBool I #ptrBaseElemTyInStack(OFFSET -Int 1, LOCAL, PROJS, REST) + requires 1 TyUnknown [owise] + rule #ptrBaseElemTyInStack(_, _, _, _) => TyUnknown [owise] + + syntax Int ::= #ptrByteStep ( Ty , Int , Local , ProjectionElems , List , List ) [function, total] + // -------------------------------------------------------------------------------------------- + rule #ptrByteStep(TY_SOURCE, _STACK_DEPTH, _LOCAL, _PROJS, _LOCALS, _STACK) + => #sizeOf(#lookupMaybeTy({pointeeTy(#lookupMaybeTy(TY_SOURCE))}:>Ty)) + requires isTy(pointeeTy(#lookupMaybeTy(TY_SOURCE))) + andBool #sizeOf(#lookupMaybeTy({pointeeTy(#lookupMaybeTy(TY_SOURCE))}:>Ty)) >Int 0 + [preserves-definedness] + rule #ptrByteStep(_TY_SOURCE, STACK_DEPTH, LOCAL, PROJS, LOCALS, STACK) + => #ptrElemSize(#lookupMaybeTy({#ptrBaseElemTy(STACK_DEPTH, LOCAL, PROJS, LOCALS, STACK)}:>Ty)) + requires isTy(#ptrBaseElemTy(STACK_DEPTH, LOCAL, PROJS, LOCALS, STACK)) + [preserves-definedness] + rule #ptrByteStep(_, _, _, _, _, _) => 1 [owise] + syntax ProjectionElems ::= appendP ( ProjectionElems , ProjectionElems ) [function, total] syntax ProjectionElems ::= appendP ( ProjectionElems , ProjectionElems ) [function, total] | consP ( ProjectionElem , ProjectionElems ) [function, total] @@ -1615,6 +1708,128 @@ 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 +address as a value of the target integer type. +The address is computed from a lazily-assigned base address for the allocation plus the +pointer offset within that allocation. + +A stack allocation key uses a stable frame id together with the local index, so the +same stack slot keeps the same abstract address even when deeper calls change relative +stack depths. + +```k + syntax AllocKey ::= allocKey ( Int , Local ) [symbol(allocKey)] + syntax AddrEntry ::= addrEntry ( Int , Int ) [symbol(addrEntry)] + + syntax Int ::= #alignUp ( Int , Int ) [function, total] + rule #alignUp(ADDR, ALIGN) => ((ADDR +Int ALIGN -Int 1) /Int ALIGN) *Int ALIGN + requires ALIGN >Int 0 + [preserves-definedness] + rule #alignUp(ADDR, _) => ADDR [owise] + + syntax Int ::= #addrEntryBase ( AddrEntry ) [function, total] + rule #addrEntryBase(addrEntry(BASE, _)) => BASE + + syntax Int ::= #ptrElemSize ( TypeInfo ) [function, total] + rule #ptrElemSize(TY_INFO) => #sizeOf(TY_INFO) requires #sizeOf(TY_INFO) >Int 0 + rule #ptrElemSize(TY_INFO) => 1 requires #sizeOf(TY_INFO) ==Int 0 // ZST + rule #ptrElemSize(_) => 1 [owise] + + syntax KItem ::= #allocAddressFor ( Int , Local , Int , Int ) + // #allocAddressFor(STACK_DEPTH, LOCAL, SIZE, ALIGN) + // Lazily assigns an aligned base address for the allocation at (frame id of STACK_DEPTH, LOCAL). + rule #allocAddressFor(STACK_DEPTH, LOCAL, SIZE, ALIGN) + => .K + ... + + CURRENT_FRAME_ID ... + STACK + + MAP => MAP[#stackAllocKey(STACK_DEPTH, LOCAL, CURRENT_FRAME_ID, STACK) <- addrEntry(#alignUp(NEXT, ALIGN), SIZE)] + + + NEXT => #alignUp(NEXT, ALIGN) +Int maxInt(SIZE, 1) + + requires 0 <=Int #stackFrameId(STACK_DEPTH, CURRENT_FRAME_ID, STACK) + andBool notBool #stackAllocKey(STACK_DEPTH, LOCAL, CURRENT_FRAME_ID, STACK) in_keys(MAP) + + // Already allocated: no-op + rule #allocAddressFor(STACK_DEPTH, LOCAL, _, _) => .K ... + CURRENT_FRAME_ID ... + STACK + MAP + requires 0 <=Int #stackFrameId(STACK_DEPTH, CURRENT_FRAME_ID, STACK) + andBool #stackAllocKey(STACK_DEPTH, LOCAL, CURRENT_FRAME_ID, STACK) in_keys(MAP) +``` + +Transmuting a `PtrLocal` to an integer type: look up or lazily assign the base address, +then compute `base + byte_offset` where byte_offset comes from the pointer's metadata. + +```k + // Case 1: address already assigned — compute base + offset + rule #cast( + PtrLocal(STACK_DEPTH, place(LOCAL, PROJS), _MUT, metadata(_SIZE, PTR_OFFSET, _ORIGIN)), + castKindTransmute, + TY_SOURCE, + TY_TARGET + ) + => + #intAsType( + #addrEntryBase({MAP[#stackAllocKey(STACK_DEPTH, LOCAL, CURRENT_FRAME_ID, STACK)]}:>AddrEntry) + +Int PTR_OFFSET *Int #ptrByteStep(TY_SOURCE, STACK_DEPTH, LOCAL, PROJS, LOCALS, STACK), + 64, + #numTypeOf(lookupTy(TY_TARGET)) + ) + ... + + + CURRENT_FRAME_ID + LOCALS + ... + + STACK + MAP + requires #isIntType(lookupTy(TY_TARGET)) + andBool 0 <=Int #stackFrameId(STACK_DEPTH, CURRENT_FRAME_ID, STACK) + andBool #stackAllocKey(STACK_DEPTH, LOCAL, CURRENT_FRAME_ID, STACK) in_keys(MAP) + [preserves-definedness] + + // Case 2: address not yet assigned — allocate first, original #cast stays on + rule #cast( + PtrLocal(STACK_DEPTH, place(LOCAL, PROJS), MUT, META), + castKindTransmute, + TY_SOURCE, + TY_TARGET + ) + => + #allocAddressFor( + STACK_DEPTH, + LOCAL, + #sizeOf(#lookupMaybeTy({#stackAllocTy(STACK_DEPTH, LOCAL, LOCALS, STACK)}:>Ty)), + #alignOf(#lookupMaybeTy({#stackAllocTy(STACK_DEPTH, LOCAL, LOCALS, STACK)}:>Ty)) + ) + ~> #cast( + PtrLocal(STACK_DEPTH, place(LOCAL, PROJS), MUT, META), + castKindTransmute, + TY_SOURCE, + TY_TARGET + ) + ... + + + CURRENT_FRAME_ID + LOCALS + ... + + STACK + MAP + requires #isIntType(lookupTy(TY_TARGET)) + andBool 0 <=Int #stackFrameId(STACK_DEPTH, CURRENT_FRAME_ID, STACK) + andBool isTy(#stackAllocTy(STACK_DEPTH, LOCAL, LOCALS, STACK)) + andBool notBool #stackAllocKey(STACK_DEPTH, LOCAL, CURRENT_FRAME_ID, STACK) in_keys(MAP) + [preserves-definedness] +``` + 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`: @@ -1879,12 +2094,151 @@ the safety of this cast. The logic of the semantics and saftey of this cast for ``` +### Pointer provenance casts + +`PointerExposeAddress` converts a pointer to an integer (like `ptr as usize`), exposing +the pointer's provenance so that a future `PointerWithExposedProvenance` cast can recover it. + +```k + // PointerExposeAddress for PtrLocal: compute address and expose provenance + rule #cast( + PtrLocal(STACK_DEPTH, place(LOCAL, PROJS), _MUT, metadata(_SIZE, PTR_OFFSET, _ORIGIN)), + castKindPointerExposeAddress, + TY_SOURCE, + TY_TARGET + ) + => + #intAsType( + #addrEntryBase({MAP[#stackAllocKey(STACK_DEPTH, LOCAL, CURRENT_FRAME_ID, STACK)]}:>AddrEntry) + +Int PTR_OFFSET *Int #ptrByteStep(TY_SOURCE, STACK_DEPTH, LOCAL, PROJS, LOCALS, STACK), + 64, + #numTypeOf(lookupTy(TY_TARGET)) + ) + ... + + + CURRENT_FRAME_ID + LOCALS + ... + + STACK + MAP + EXPOSED => EXPOSED |Set SetItem(#stackAllocKey(STACK_DEPTH, LOCAL, CURRENT_FRAME_ID, STACK)) + requires #isIntType(lookupTy(TY_TARGET)) + andBool 0 <=Int #stackFrameId(STACK_DEPTH, CURRENT_FRAME_ID, STACK) + andBool #stackAllocKey(STACK_DEPTH, LOCAL, CURRENT_FRAME_ID, STACK) in_keys(MAP) + [preserves-definedness] + + rule #cast( + PtrLocal(STACK_DEPTH, place(LOCAL, PROJS), MUT, META), + castKindPointerExposeAddress, + TY_SOURCE, + TY_TARGET + ) + => + #allocAddressFor( + STACK_DEPTH, + LOCAL, + #sizeOf(#lookupMaybeTy({#stackAllocTy(STACK_DEPTH, LOCAL, LOCALS, STACK)}:>Ty)), + #alignOf(#lookupMaybeTy({#stackAllocTy(STACK_DEPTH, LOCAL, LOCALS, STACK)}:>Ty)) + ) + ~> #cast( + PtrLocal(STACK_DEPTH, place(LOCAL, PROJS), MUT, META), + castKindPointerExposeAddress, + TY_SOURCE, + TY_TARGET + ) + ... + + + CURRENT_FRAME_ID + LOCALS + ... + + STACK + MAP + requires #isIntType(lookupTy(TY_TARGET)) + andBool 0 <=Int #stackFrameId(STACK_DEPTH, CURRENT_FRAME_ID, STACK) + andBool isTy(#stackAllocTy(STACK_DEPTH, LOCAL, LOCALS, STACK)) + andBool notBool #stackAllocKey(STACK_DEPTH, LOCAL, CURRENT_FRAME_ID, STACK) in_keys(MAP) + [preserves-definedness] + + // PointerExposeAddress for Reference + rule #cast( + Reference(STACK_DEPTH, place(LOCAL, PROJS), _MUT, metadata(_SIZE, PTR_OFFSET, _ORIGIN)), + castKindPointerExposeAddress, + TY_SOURCE, + TY_TARGET + ) + => + #intAsType( + #addrEntryBase({MAP[#stackAllocKey(STACK_DEPTH, LOCAL, CURRENT_FRAME_ID, STACK)]}:>AddrEntry) + +Int PTR_OFFSET *Int #ptrByteStep(TY_SOURCE, STACK_DEPTH, LOCAL, PROJS, LOCALS, STACK), + 64, + #numTypeOf(lookupTy(TY_TARGET)) + ) + ... + + + CURRENT_FRAME_ID + LOCALS + ... + + STACK + MAP + EXPOSED => EXPOSED |Set SetItem(#stackAllocKey(STACK_DEPTH, LOCAL, CURRENT_FRAME_ID, STACK)) + requires #isIntType(lookupTy(TY_TARGET)) + andBool 0 <=Int #stackFrameId(STACK_DEPTH, CURRENT_FRAME_ID, STACK) + andBool #stackAllocKey(STACK_DEPTH, LOCAL, CURRENT_FRAME_ID, STACK) in_keys(MAP) + [preserves-definedness] + + rule #cast( + Reference(STACK_DEPTH, place(LOCAL, PROJS), MUT, META), + castKindPointerExposeAddress, + TY_SOURCE, + TY_TARGET + ) + => + #allocAddressFor( + STACK_DEPTH, + LOCAL, + #sizeOf(#lookupMaybeTy({#stackAllocTy(STACK_DEPTH, LOCAL, LOCALS, STACK)}:>Ty)), + #alignOf(#lookupMaybeTy({#stackAllocTy(STACK_DEPTH, LOCAL, LOCALS, STACK)}:>Ty)) + ) + ~> #cast( + Reference(STACK_DEPTH, place(LOCAL, PROJS), MUT, META), + castKindPointerExposeAddress, + TY_SOURCE, + TY_TARGET + ) + ... + + + CURRENT_FRAME_ID + LOCALS + ... + + STACK + MAP + requires #isIntType(lookupTy(TY_TARGET)) + andBool 0 <=Int #stackFrameId(STACK_DEPTH, CURRENT_FRAME_ID, STACK) + andBool isTy(#stackAllocTy(STACK_DEPTH, LOCAL, LOCALS, STACK)) + andBool notBool #stackAllocKey(STACK_DEPTH, LOCAL, CURRENT_FRAME_ID, STACK) in_keys(MAP) + [preserves-definedness] +``` + +`PointerWithExposedProvenance` converts an integer to a pointer (`ptr::with_exposed_provenance`), +recovering the provenance that was previously exposed. + +```k + // TODO: PointerWithExposedProvenance requires searching the address map and exposed set + // to recover the original allocation. This is left for future implementation. +``` + ### Other casts involving pointers | CastKind | Description | |------------------------------|-------------| -| PointerExposeAddress | | -| PointerWithExposedProvenance | | | FnPtrToPtr | | ## Decoding constants from their bytes representation to values diff --git a/kmir/src/tests/integration/data/prove-rs/alignment-check.rs b/kmir/src/tests/integration/data/prove-rs/alignment-check.rs new file mode 100644 index 000000000..0ef832c69 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/alignment-check.rs @@ -0,0 +1,14 @@ +// Test for issue #638: alignment check in raw pointer dereference. +// The compiler inserts an alignment check that transmutes a pointer to usize. +// Verifies that the transmute cast evaluates concretely. + +struct Thing { payload: i16 } + +fn main() { + let a = [Thing { payload: 1 }, Thing { payload: 2 }, Thing { payload: 3 }]; + let p = &a as *const Thing; + let p1 = unsafe { p.add(1) }; + + let two = unsafe { (*p1).payload }; + assert!(two == 2); +} diff --git a/kmir/src/tests/integration/data/prove-rs/interior-mut3-fail.rs b/kmir/src/tests/integration/data/prove-rs/interior-mut3.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/interior-mut3-fail.rs rename to kmir/src/tests/integration/data/prove-rs/interior-mut3.rs diff --git a/kmir/src/tests/integration/data/prove-rs/local-raw-fail.rs b/kmir/src/tests/integration/data/prove-rs/local-raw.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/local-raw-fail.rs rename to kmir/src/tests/integration/data/prove-rs/local-raw.rs diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-cross-frame-eq.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-cross-frame-eq.rs new file mode 100644 index 000000000..c68cdb626 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/ptr-cast-cross-frame-eq.rs @@ -0,0 +1,13 @@ +fn addr_of(ptr: *const i32) -> usize { + ptr as usize +} + +fn main() { + let x = 7; + let ptr = &x as *const i32; + + let caller_addr = ptr as usize; + let callee_addr = addr_of(ptr); + + assert_eq!(caller_addr, callee_addr); +} diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper-fail.rs rename to kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper.rs diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-transmute-nonzero.rs b/kmir/src/tests/integration/data/prove-rs/ptr-transmute-nonzero.rs new file mode 100644 index 000000000..252a4bd0a --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/ptr-transmute-nonzero.rs @@ -0,0 +1,11 @@ +/// Test that a stack pointer transmuted to usize is non-zero. +use std::mem::transmute; + +fn main() { + let x: u32 = 42; + let ptr: *const u32 = &x; + unsafe { + let addr: usize = transmute(ptr); + assert!(addr != 0); + } +} diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-transmute-two-locals.rs b/kmir/src/tests/integration/data/prove-rs/ptr-transmute-two-locals.rs new file mode 100644 index 000000000..aceabc703 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/ptr-transmute-two-locals.rs @@ -0,0 +1,14 @@ +/// Test that two different local pointers transmute to different addresses. +use std::mem::transmute; + +fn main() { + let a: u32 = 42; + let b: u32 = 99; + let pa: *const u32 = &a; + let pb: *const u32 = &b; + unsafe { + let addr_a: usize = transmute(pa); + let addr_b: usize = transmute(pb); + assert!(addr_a != addr_b); + } +} diff --git a/kmir/src/tests/integration/data/prove-rs/ptr_offset.rs b/kmir/src/tests/integration/data/prove-rs/ptr_offset.rs new file mode 100644 index 000000000..e14cb1ebc --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/ptr_offset.rs @@ -0,0 +1,11 @@ +struct Thing {payload: i16} + +fn main() { + + let a = [Thing{payload: 1}, Thing{payload: 2}, Thing{payload:3}]; + let p = &a as *const Thing; + let p1 = unsafe { p.add(1) }; + + let two = unsafe { (*p1).payload }; + assert!(two == 2); +} diff --git a/kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-fail.rs b/kmir/src/tests/integration/data/prove-rs/raw-ptr-cast.rs similarity index 69% rename from kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-fail.rs rename to kmir/src/tests/integration/data/prove-rs/raw-ptr-cast.rs index cf098c9c3..bf425e202 100644 --- a/kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-fail.rs +++ b/kmir/src/tests/integration/data/prove-rs/raw-ptr-cast.rs @@ -5,6 +5,6 @@ fn main() { let ptr_mut = &mut data as *mut i32; unsafe { (*ptr_mut) = 44; - assert_eq!(44, *ptr); // FIXME: fails due to thunks on casts + assert_eq!(44, *ptr); } } diff --git a/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset-fail.rs b/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset-fail.rs rename to kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset.rs diff --git a/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-fail.rs b/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-fail.rs rename to kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem.rs 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 deleted file mode 100644 index 32338a571..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected +++ /dev/null @@ -1,63 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (154 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 - │ - │ (66 steps) - ├─ 11 (terminal) - │ #EndProgram ~> .K - │ function: main - │ - ┊ constraint: true - ┊ subst: ... - └─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected deleted file mode 100644 index a9a6646e9..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected +++ /dev/null @@ -1,40 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (106 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 ( 1 ) ) ~> .K - │ function: main - │ - │ (16 steps) - ├─ 7 (terminal) - │ #EndProgram ~> .K - │ function: main - │ - ┊ constraint: true - ┊ subst: ... - └─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-cross-frame-eq.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-cross-frame-eq.main.expected new file mode 100644 index 000000000..d3690d8ab --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-cross-frame-eq.main.expected @@ -0,0 +1,18 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ function: main +│ span: 0 +│ +│ (173 steps) +├─ 3 (terminal) +│ #EndProgram ~> .K +│ function: main +│ +┊ constraint: true +┊ subst: ... +└─ 2 (leaf, target, terminal) + #EndProgram ~> .K + + + diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper-fail.main.expected deleted file mode 100644 index 6c000e5b0..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper-fail.main.expected +++ /dev/null @@ -1,109 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (106 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 ( 12 ) ) ~> .K - │ function: main - │ - │ (113 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 ( 11 ) ) ~> .K - │ function: main - │ - │ (115 steps) - ├─ 11 - │ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th - │ function: main - ┃ - ┃ (1 step) - ┣━━┓ - ┃ │ - ┃ ├─ 12 - ┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC - ┃ │ function: main - ┃ │ - ┃ │ (1 step) - ┃ └─ 14 (stuck, leaf) - ┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re - ┃ function: main - ┃ - ┗━━┓ - │ - ├─ 13 - │ #execBlockIdx ( basicBlockIdx ( 10 ) ) ~> .K - │ function: main - │ - │ (117 steps) - ├─ 15 - │ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th - │ function: main - ┃ - ┃ (1 step) - ┣━━┓ - ┃ │ - ┃ ├─ 16 - ┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC - ┃ │ function: main - ┃ │ - ┃ │ (1 step) - ┃ └─ 18 (stuck, leaf) - ┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re - ┃ function: main - ┃ - ┗━━┓ - │ - ├─ 17 - │ #execBlockIdx ( basicBlockIdx ( 9 ) ) ~> .K - │ function: main - │ - │ (25 steps) - ├─ 19 (terminal) - │ #EndProgram ~> .K - │ function: main - │ - ┊ constraint: true - ┊ subst: ... - └─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected deleted file mode 100644 index 7be3f4dd4..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/raw-ptr-cast-fail.main.expected +++ /dev/null @@ -1,40 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (120 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 ( 3 ) ) ~> .K - │ function: main - │ - │ (124 steps) - ├─ 7 (terminal) - │ #EndProgram ~> .K - │ function: main - │ - ┊ constraint: true - ┊ subst: ... - └─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-fail.main.expected deleted file mode 100644 index e6f0eec24..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-fail.main.expected +++ /dev/null @@ -1,40 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (124 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 ( 3 ) ) ~> .K - │ function: main - │ - │ (26 steps) - ├─ 7 (terminal) - │ #EndProgram ~> .K - │ function: main - │ - ┊ constraint: true - ┊ subst: ... - └─ 2 (leaf, target, terminal) - #EndProgram ~> .K - - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-offset-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-offset-fail.main.expected deleted file mode 100644 index 2d1468486..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-offset-fail.main.expected +++ /dev/null @@ -1,40 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (185 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 ( 4 ) ) ~> .K - │ function: main - │ - │ (26 steps) - ├─ 7 (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 a731e4880..f445fbe9a 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -45,9 +45,7 @@ 'closure-staged', ] PROVE_SHOW_SPECS = [ - 'local-raw-fail', 'interior-mut-fail', - 'interior-mut3-fail', 'iter_next_3', 'assert_eq_exp', 'bitwise-not-shift', @@ -58,19 +56,16 @@ 'pointer-cast-length-test-fail', 'niche-enum', 'assume-cheatcode-conflict-fail', - 'raw-ptr-cast-fail', 'transmute-u8-to-enum-fail', 'assert-inhabited-fail', 'iterator-simple', 'unions-fail', 'transmute-maybe-uninit-fail', - 'ptr-through-wrapper-fail', 'test_offset_from-fail', - 'ref-ptr-cast-elem-fail', - 'ref-ptr-cast-elem-offset-fail', 'volatile_store_static-fail', 'volatile_load_static-fail', 'box_heap_alloc-fail', + 'ptr-cast-cross-frame-eq', 'ptr-cast-array-to-wrapper-fail', 'ptr-cast-array-to-nested-wrapper-fail', 'ptr-cast-array-to-singleton-wrapped-array-fail',