diff --git a/kmir/src/kmir/kast.py b/kmir/src/kmir/kast.py index ed6b128f0..22b7360b7 100644 --- a/kmir/src/kmir/kast.py +++ b/kmir/src/kmir/kast.py @@ -36,8 +36,6 @@ from pyk.kast.outer import KDefinition from .smir import SMIRInfo - from .ty import TypeMetadata - from .value import MetadataSize, Value _LOGGER: Final = logging.getLogger(__name__) diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 36ced69cf..f3c60d776 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -443,13 +443,162 @@ This does not sacrifice unsoundness as we would not eliminate any assertion fail Other terminators that matter at the MIR level "Runtime" are `Drop` and `Unreachable`. Drops are elaborated to Noops but still define the continuing control flow. Unreachable terminators lead to a program error. +#### Drop Terminator + +The `Drop` terminator traverses the target place, materialises its value and type information, and then resumes execution at the successor block once the type-directed drop handler has run. + +#### Borrow-Aware Drops + +Our runtime model tracks RefCell borrow counts for smart-pointer types. Dropping `RefMut` releases the unique borrow by incrementing the cell, while dropping `Ref` decrements the shared borrow count. The helper rules below normalise pointer shapes and apply those updates across the stack. + +- Detect `RefMut` / `Ref` via `#isRefMutTy` and `#isRefTy`, which presently match the canonical names that contain `"RefMut<"` or `"Ref<"`. +- Extract projection data so that borrow cells can be reached regardless of pointer shape or stack depth. +- Update the borrow cell using `#incCellBorrow` for mutable borrows and `#decCellBorrow` for shared borrows; the cell is represented as a signed 64-bit integer (`rt/data.md`). +- The model does not assert that the borrow cell currently equals `-1`; repeated drops therefore leave the configuration unchanged. + ```k - rule [termDrop]: #execTerminator(terminator(terminatorKindDrop(_PLACE, TARGET, _UNWIND), _SPAN)) + // TODO: support general drops (not specifically Ref/RefMut) + rule [termDrop]: + #execTerminator(terminator(terminatorKindDrop(place(local(I), PROJS), TARGET, _UNWIND), _SPAN)) => - #execBlockIdx(TARGET) + #applyDrop( + operandMove(place(local(I), PROJS)), + getTyOf(tyOfLocal(getLocal(LOCALS, I)), PROJS) + ) ~> #execBlockIdx(TARGET) ... + LOCALS + requires 0 <=Int I + andBool I #applyDrop(Aggregate(_, ARGS), MTY) + => #releaseBorrowRef(getValue(ARGS, 1), #isRefMutTy(#lookupMaybeTy(MTY))) + ... + + requires 1 #applyDrop(_:Value, MTY) => .K ... + requires notBool #isRefMutTy(#lookupMaybeTy(MTY)) + andBool notBool #isRefTy(#lookupMaybeTy(MTY)) + + syntax Bool ::= #isRefMutTy ( TypeInfo ) [function, total] + rule #isRefMutTy(typeInfoStructType(NAME:String, _, _, _)) + => findString(NAME, "RefMut<", 0) =/=Int -1 + rule #isRefMutTy(_) => false [owise] + + syntax Bool ::= #isRefTy ( TypeInfo ) [function, total] + rule #isRefTy(typeInfoStructType(NAME:String, _, _, _)) + => findString(NAME, "Ref<", 0) =/=Int -1 + andBool findString(NAME, "RefMut<", 0) ==Int -1 + rule #isRefTy(_) => false [owise] + + // Helper to release borrow reference; Bool indicates mutability + syntax KItem ::= #releaseBorrowRef(Value, Bool) + + // Strip tuple/struct wrappers so the borrow cell pointer can be normalised. + rule #releaseBorrowRef(Aggregate(_, ListItem(PTR) _), IS_MUT) + => #releaseBorrowRef(PTR, IS_MUT) + + // Turn References into PtrLocal so projection traversal can reach the borrow cell. + rule #releaseBorrowRef(Reference(OFFSET, PLACE, MUT, META), IS_MUT) + => #releaseBorrowRef(PtrLocal(OFFSET, PLACE, MUT, META), IS_MUT) + + // Stack height 0: borrow cell lives in the current frame, adjust projections (respecting pointer metadata). + rule #releaseBorrowRef(PtrLocal(0, place(local(J), PROJS), _, metadata(_SIZE, PTR_OFFSET, ORIGIN_SIZE)), IS_MUT) + => + #traverseProjection( + toLocal(J), + getValue(LOCALS, J), + #withPointerOffset(PROJS, PTR_OFFSET, ORIGIN_SIZE), + .Contexts + ) + ~> #readProjection(false) + ~> #applyBorrowCellLocal(J, #withPointerOffset(PROJS, PTR_OFFSET, ORIGIN_SIZE), IS_MUT) + ... + + LOCALS + requires 0 <=Int J + andBool J #releaseBorrowRef(PtrLocal(OFFSET, place(local(J), PROJS), _, metadata(_SIZE, PTR_OFFSET, ORIGIN_SIZE)), IS_MUT) + => + #traverseProjection( + toStack(OFFSET, local(J)), + #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(J), OFFSET), + #withPointerOffset(PROJS, PTR_OFFSET, ORIGIN_SIZE), + .Contexts + ) + ~> #readProjection(false) + ~> #applyBorrowCellStack(OFFSET, J, #withPointerOffset(PROJS, PTR_OFFSET, ORIGIN_SIZE), IS_MUT) + ... + + STACK + requires 0 .K [owise] + + syntax ProjectionElems ::= #withPointerOffset(ProjectionElems, Int, MetadataSize) [function, total] + rule #withPointerOffset(PROJS, PTR_OFFSET, ORIGIN_SIZE) + => appendP(PROJS, PointerOffset(PTR_OFFSET, originSize(ORIGIN_SIZE))) + requires PTR_OFFSET =/=Int 0 + rule #withPointerOffset(PROJS, _PTR_OFFSET, _ORIGIN_SIZE) => PROJS [owise] + + syntax KItem ::= #applyBorrowCellLocal(Int, ProjectionElems, Bool) + | #applyBorrowCellStack(Int, Int, ProjectionElems, Bool) + + // Write the adjusted borrow count back into the current frame's cell. + rule CELL:Value ~> #applyBorrowCellLocal(J, PROJS, IS_MUT) + => + #setLocalValue( + place(local(J), PROJS), + #if IS_MUT + #then #incCellBorrow(CELL) + #else #decCellBorrow(CELL) + #fi + ) + ... + + rule #applyBorrowCellLocal(_, _, _) => .K [owise] + // Same as above, but for borrow cells located in ancestor stack frames. + rule CELL:Value ~> #applyBorrowCellStack(OFFSET, J, PROJS, IS_MUT) + => + #traverseProjection( + toStack(OFFSET, local(J)), + #localFromFrame({STACK[OFFSET -Int 1]}:>StackFrame, local(J), OFFSET), + PROJS, + .Contexts + ) + ~> #writeProjection( + #if IS_MUT + #then #incCellBorrow(CELL) + #else #decCellBorrow(CELL) + #fi + ) + ... + + STACK + requires 0 .K [owise] +``` + +#### Unreachable Terminator + +```k syntax MIRError ::= "ReachedUnreachable" rule [termUnreachable]: #execTerminator(terminator(terminatorKindUnreachable, _SPAN)) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 7adc8dd0f..073c8873c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -346,6 +346,28 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr andBool isTypedLocal(LOCALS[I]) [preserves-definedness] // valid list indexing and sort checked + // Borrow cell increment (interior mutability model) for shared Ref borrows. + syntax Value ::= #incCellBorrow ( Value ) [function, total] + rule #incCellBorrow(Integer(VAL, WIDTH, true)) + => Integer(VAL +Int 1, WIDTH, true) + requires WIDTH ==Int 64 + [preserves-definedness] + rule #incCellBorrow(Aggregate(IDX, ListItem(FIRST) REST)) + => Aggregate(IDX, ListItem(#incCellBorrow(FIRST)) REST) + [preserves-definedness] + rule #incCellBorrow(OTHER) => OTHER [owise] + + // Borrow cell decrement for releasing shared Ref borrows. + syntax Value ::= #decCellBorrow ( Value ) [function, total] + rule #decCellBorrow(Integer(VAL, WIDTH, true)) + => Integer(VAL -Int 1, WIDTH, true) + requires WIDTH ==Int 64 + [preserves-definedness] + rule #decCellBorrow(Aggregate(IDX, ListItem(FIRST) REST)) + => Aggregate(IDX, ListItem(#decCellBorrow(FIRST)) REST) + [preserves-definedness] + rule #decCellBorrow(OTHER) => OTHER [owise] + syntax ProjectionElems ::= appendP ( ProjectionElems , ProjectionElems ) [function, total] rule appendP(.ProjectionElems, TAIL) => TAIL rule appendP(X:ProjectionElem REST:ProjectionElems, TAIL) => X appendP(REST, TAIL) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md index 77cc5bbd5..c98f56a9a 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md @@ -100,12 +100,6 @@ syntax Int ::= #msBytes ( MachineSize ) [function, total] rule #msBytes(machineSize(mirInt(NBITS))) => NBITS /Int 8 [preserves-definedness] rule #msBytes(machineSize(NBITS)) => NBITS /Int 8 [owise, preserves-definedness] -// Extract field offsets from the struct layout when available (Arbitrary only). -syntax MachineSizes ::= #structOffsets ( MaybeLayoutShape ) [function, total] -rule #structOffsets(someLayoutShape(layoutShape(fieldsShapeArbitrary(mk(OFFSETS)), _, _, _, _))) => OFFSETS -rule #structOffsets(noLayoutShape) => .MachineSizes -rule #structOffsets(_) => .MachineSizes [owise] - // Minimum number of input bytes required to decode all fields by the chosen offsets. // Uses builtin maxInt to compute max(offset + size). The lists of types and // offsets must have the same length; if not, this function returns -1 to signal diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md b/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md index 7c9f43f38..9a56ecd11 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/numbers.md @@ -148,6 +148,7 @@ This truncation function is instrumental in the implementation of Integer arithm ```k // FIXME: Alignment is platform specific +// TODO: Extend #alignOf to be total by handling aggregate layouts (structs, arrays, unions). syntax Int ::= #alignOf( TypeInfo ) [function] rule #alignOf( typeInfoPrimitiveType(primTypeBool) ) => 1 rule #alignOf( typeInfoPrimitiveType(primTypeChar) ) => 4 @@ -167,6 +168,7 @@ rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF16)) ) => 2 rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF32)) ) => 4 rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF64)) ) => 8 rule #alignOf( typeInfoPrimitiveType(primTypeFloat(floatTyF128)) ) => 16 +rule #alignOf( typeInfoStructType(_,_,_,someLayoutShape(layoutShape(_, _, _, align(ALIGN), _)))) => ALIGN ``` ```k diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected index 224160f42..f162c21ea 100644 --- a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected +++ b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (730 steps) +│ (751 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected index 9c905f5d3..56ffc4c40 100644 --- a/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected +++ b/kmir/src/tests/integration/data/crate-tests/two-crate-dylib/crate2::test_crate1_with.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (212 steps) +│ (219 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ diff --git a/kmir/src/tests/integration/data/prove-rs/interior-mut-refcell.rs b/kmir/src/tests/integration/data/prove-rs/interior-mut-refcell.rs new file mode 100644 index 000000000..dc6f51ddd --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/interior-mut-refcell.rs @@ -0,0 +1,134 @@ +//! Minimal dual-AccountInfo harness for MIR semantics tests. + +use std::cell::{Ref, RefCell, RefMut}; + +trait MiniPack: Copy { + const LEN: usize; + fn pack_into_slice(self, dst: &mut [u8]); + fn unpack_unchecked(src: &[u8]) -> Self + where + Self: Sized; +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +struct MiniMint { + decimals: u8, + supply: u64, +} + +impl MiniPack for MiniMint { + const LEN: usize = 9; + + fn pack_into_slice(self, dst: &mut [u8]) { + assert_eq!(dst.len(), Self::LEN); + dst[0] = self.decimals; + dst[1..].copy_from_slice(&self.supply.to_le_bytes()); + } + + fn unpack_unchecked(src: &[u8]) -> Self { + let mut supply = [0_u8; 8]; + supply.copy_from_slice(&src[1..]); + Self { + decimals: src[0], + supply: u64::from_le_bytes(supply), + } + } +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +struct MiniTokenAccount { + owner: [u8; 8], + amount: u64, + status: u8, +} + +impl MiniPack for MiniTokenAccount { + const LEN: usize = 17; + + fn pack_into_slice(self, dst: &mut [u8]) { + assert_eq!(dst.len(), Self::LEN); + dst[0..8].copy_from_slice(&self.owner); + dst[8..16].copy_from_slice(&self.amount.to_le_bytes()); + dst[16] = self.status; + } + + fn unpack_unchecked(src: &[u8]) -> Self { + let mut owner = [0_u8; 8]; + owner.copy_from_slice(&src[0..8]); + let mut amount = [0_u8; 8]; + amount.copy_from_slice(&src[8..16]); + Self { + owner, + amount: u64::from_le_bytes(amount), + status: src[16], + } + } +} + +pub struct AccountInfo<'a> { + data: RefCell<&'a mut [u8]>, +} + +impl<'a> AccountInfo<'a> { + pub fn new(data: &'a mut [u8]) -> Self { + Self { + data: RefCell::new(data), + } + } + + pub fn borrow_data(&self) -> Ref<'_, [u8]> { + Ref::map(self.data.borrow(), |slice| &**slice) + } + + pub fn borrow_mut_data(&self) -> RefMut<'_, [u8]> { + RefMut::map(self.data.borrow_mut(), |slice| &mut **slice) + } +} + +#[no_mangle] +pub fn dual_account_demo(account_info: &AccountInfo, mint_info: &AccountInfo) -> bool { + let account_read = account_info.borrow_data(); + let mint_read = mint_info.borrow_data(); + let _ = MiniTokenAccount::unpack_unchecked(&account_read); + let _ = MiniMint::unpack_unchecked(&mint_read); + drop(account_read); + drop(mint_read); + + let mut account_write = account_info.borrow_mut_data(); + let mut mint_write = mint_info.borrow_mut_data(); + let expected_account = MiniTokenAccount { + owner: *b"demoacct", + amount: 123, + status: 1, + }; + let expected_mint = MiniMint { + decimals: 9, + supply: 500, + }; + expected_account.pack_into_slice(&mut account_write); + expected_mint.pack_into_slice(&mut mint_write); + drop(account_write); + drop(mint_write); + + let account_read_after = account_info.borrow_data(); + let mint_read_after = mint_info.borrow_data(); + assert_eq!( + MiniTokenAccount::unpack_unchecked(&account_read_after), + expected_account + ); + assert_eq!( + MiniMint::unpack_unchecked(&mint_read_after), + expected_mint + ); + + true +} + +fn main() { + let mut account_bytes = [0_u8; MiniTokenAccount::LEN]; + let mut mint_bytes = [0_u8; MiniMint::LEN]; + let account = AccountInfo::new(&mut account_bytes); + let mint = AccountInfo::new(&mut mint_bytes); + let result = dual_account_demo(&account, &mint); + assert!(result); +} diff --git a/kmir/src/tests/integration/data/prove-rs/interior-mut-fail.rs b/kmir/src/tests/integration/data/prove-rs/interior-mut.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/interior-mut-fail.rs rename to kmir/src/tests/integration/data/prove-rs/interior-mut.rs diff --git a/kmir/src/tests/integration/data/prove-rs/interior-mut2-fail.rs b/kmir/src/tests/integration/data/prove-rs/interior-mut2.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/interior-mut2-fail.rs rename to kmir/src/tests/integration/data/prove-rs/interior-mut2.rs 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/pointer-cast-struct-field-fail.rs b/kmir/src/tests/integration/data/prove-rs/pointer-cast-struct-field-fail.rs new file mode 100644 index 000000000..cca13da87 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/pointer-cast-struct-field-fail.rs @@ -0,0 +1,13 @@ +struct Pair { + head: i64, + tail: i8, +} + +fn read_via_cast(pair: &Pair) -> i64 { + unsafe { *(pair as *const Pair as *const i64) } +} + +fn main() { + let pair = Pair { head: 7, tail: 1 }; + assert!(read_via_cast(&pair) == 7); +} diff --git a/kmir/src/tests/integration/data/prove-rs/pointer-cast-transparent-wrapper.rs b/kmir/src/tests/integration/data/prove-rs/pointer-cast-transparent-wrapper.rs new file mode 100644 index 000000000..b47544474 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/pointer-cast-transparent-wrapper.rs @@ -0,0 +1,21 @@ +#[repr(transparent)] +#[derive(Clone, Copy)] +struct Wrapper(u32); + +fn main() { + let w = Wrapper(13); + let round_tripped = round_trip(&w); + // If the cast alignment is wrong, dereferencing `round_tripped` + // will read the inner `u32` instead of the whole `Wrapper`, + // so destructuring as `Wrapper` fails. + let Wrapper(v) = unsafe { *round_tripped }; + assert!(v == 13); +} + +fn round_trip(wrapper: &Wrapper) -> *const Wrapper { + unsafe { + let p0: *const Wrapper = wrapper; + let p1: *const u32 = p0 as *const u32; + p1 as *const Wrapper + } +} diff --git a/kmir/src/tests/integration/data/prove-rs/pointer-cast-unsafe-cell.rs b/kmir/src/tests/integration/data/prove-rs/pointer-cast-unsafe-cell.rs new file mode 100644 index 000000000..a78147886 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/pointer-cast-unsafe-cell.rs @@ -0,0 +1,14 @@ +use std::cell::UnsafeCell; + +fn read(cell: &UnsafeCell) -> i64 { + unsafe { + let raw: *const UnsafeCell = cell; + let inner: *const i64 = raw as *const i64; + *inner + } +} + +fn main() { + let cell = UnsafeCell::new(41); + assert!(read(&cell) == 41); +} diff --git a/kmir/src/tests/integration/data/prove-rs/reference-zero-sized.rs b/kmir/src/tests/integration/data/prove-rs/reference-zero-sized.rs new file mode 100644 index 000000000..87b00103a --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/reference-zero-sized.rs @@ -0,0 +1,7 @@ +struct Marker; + +fn main() { + let m = Marker; + let r = &m; + std::mem::drop::<&Marker>(r); +} 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 0459ee731..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 -│ -│ (315 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/interior-mut-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected deleted file mode 100644 index 7cb6831b6..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (198 steps) -└─ 3 (stuck, leaf) - #traverseProjection ( toLocal ( 11 ) , thunk ( #cast ( PtrLocal ( 3 , place ( .. - span: 91 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected deleted file mode 100644 index 6ef3112a7..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (185 steps) -└─ 3 (stuck, leaf) - #traverseProjection ( toLocal ( 2 ) , thunk ( #cast ( PtrLocal ( 3 , place ( ... - span: 53 - - -┌─ 2 (root, 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 a99c05167..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 -│ -│ (105 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/pointer-cast-length-test-fail.array_cast_test.expected b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected index ff6808691..2688fd0d2 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected @@ -41,7 +41,7 @@ ┃ │ ┃ │ (6 steps) ┃ ├─ 10 - ┃ │ #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( #mapOffset ( range ( + ┃ │ #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( #mapOffset ( #mapOff ┃ │ span: 87 ┃ ┃ ┃ ┃ (1 step) @@ -59,7 +59,7 @@ ┃ ┗━━┓ ┃ │ ┃ └─ 12 (stuck, leaf) - ┃ #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( #mapOffset ( range ( + ┃ #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( #mapOffset ( #mapOff ┃ span: 87 ┃ ┗━━┓ 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/pointer-cast-struct-field-fail.main.expected similarity index 77% rename from kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected rename to kmir/src/tests/integration/data/prove-rs/show/pointer-cast-struct-field-fail.main.expected index d4b0127e7..92eca15d1 100644 --- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected +++ b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-struct-field-fail.main.expected @@ -3,34 +3,29 @@ │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ span: 0 │ -│ (151 steps) +│ (135 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 + │ #execBlockIdx ( basicBlockIdx ( 1 ) ) ~> .K │ - │ (8 steps) + │ (7 steps) └─ 7 (stuck, leaf) #traverseProjection ( toLocal ( 2 ) , thunk ( #cast ( PtrLocal ( 1 , place ( ... - function: main - span: 80 + span: 53 ┌─ 2 (root, leaf, target, terminal) diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index a42265cc9..a29051443 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -38,10 +38,6 @@ 'assume-cheatcode-conflict-fail': ['check_assume_conflict'], } PROVE_RS_SHOW_SPECS = [ - 'local-raw-fail', - 'interior-mut-fail', - 'interior-mut2-fail', - 'interior-mut3-fail', 'assert_eq_exp', 'bitwise-not-shift', 'symbolic-args-fail', @@ -49,7 +45,7 @@ 'checked_arithmetic-fail', 'offset-u8-fail', 'pointer-cast-length-test-fail', - 'closure_access_struct', + 'pointer-cast-struct-field-fail', 'niche-enum', 'assume-cheatcode-conflict-fail', ]