From 547551113a673b6a28a0ee4dbc3042ab1881f7ab Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 6 Mar 2026 07:48:05 +0800 Subject: [PATCH 1/2] fix(rt-data): handle singleton-array projection traversal --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 15 +++++++++++++++ .../prove-rs/singleton-array-pointer-cast-fail.rs | 9 +++++++++ 2 files changed, 24 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/singleton-array-pointer-cast-fail.rs diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index bcce7438b..0ed80bfed 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -330,6 +330,7 @@ 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) | "CtxWrapStruct" // special context adding a singleton Aggregate(0, _) around a value + | "CtxWrapSingletonArray" // special context adding a singleton Range(ListItem(_)) around a value syntax ProjectionElem ::= PointerOffset( Int, Int ) // Same as subslice but coming from BinopOffset injected by us @@ -368,6 +369,10 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr rule #buildUpdate(Aggregate(variantIdx(0), ListItem(VALUE) .List), CtxWrapStruct CTXS) => #buildUpdate(VALUE, CTXS) + // removing a singleton-array wrapper added by a SingletonArray projection + rule #buildUpdate(Range(ListItem(VALUE) .List), CtxWrapSingletonArray CTXS) + => #buildUpdate(VALUE, CTXS) + syntax StackFrame ::= #updateStackLocal ( StackFrame, Int, Value ) [function] @@ -501,6 +506,15 @@ The situation typically arises when the stored value is a pointer (`NonNull`) bu ) => #traverseProjection(DEST, Aggregate(variantIdx(0), ListItem(VALUE)), PROJS, CtxWrapStruct CTXTS) ... [preserves-definedness, priority(100)] + + rule #traverseProjection( + DEST, + VALUE, + projectionElemSingletonArray PROJS, + CTXTS + ) + => #traverseProjection(DEST, Range(ListItem(VALUE)), PROJS, CtxWrapSingletonArray CTXTS) ... + [preserves-definedness, priority(100)] ``` A somewhat dual case to this rule can occur when a pointer into an array of data elements has been offset and is then dereferenced. @@ -1235,6 +1249,7 @@ This eliminates any `Deref` projections from the place, and also resolves `Index rule #projectionsFor(CtxPointerOffset( _, OFFSET, ORIGIN_LENGTH) CTXS, PROJS) => #projectionsFor(CTXS, PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS) rule #projectionsFor(CtxFieldUnion(F_IDX, _, TY) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemField(F_IDX, TY) PROJS) rule #projectionsFor( CtxWrapStruct CTXS, PROJS) => #projectionsFor(CTXS, projectionElemWrapStruct PROJS) + rule #projectionsFor(CtxWrapSingletonArray CTXS, PROJS) => #projectionsFor(CTXS, projectionElemSingletonArray PROJS) // Borrowing a zero-sized local that is still `NewLocal`: initialise it, then reuse the regular rule. rule rvalueRef(REGION, KIND, place(local(I), PROJS)) diff --git a/kmir/src/tests/integration/data/prove-rs/singleton-array-pointer-cast-fail.rs b/kmir/src/tests/integration/data/prove-rs/singleton-array-pointer-cast-fail.rs new file mode 100644 index 000000000..44bf4b544 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/singleton-array-pointer-cast-fail.rs @@ -0,0 +1,9 @@ +fn main() { + let mut x: u8 = 1; + unsafe { + let p: *mut u8 = &mut x; + let q: *mut [u8; 1] = p as *mut [u8; 1]; + std::ptr::write(q, [2]); + } + assert!(x == 2); +} From 6c2fa5bed7e7416268f0b8bd8fbb8aa6ed7cce5d Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 6 Mar 2026 14:35:15 +0800 Subject: [PATCH 2/2] test(prove-rs): rename singleton-array fixture to passing case --- ...array-pointer-cast-fail.rs => singleton-array-pointer-cast.rs} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename kmir/src/tests/integration/data/prove-rs/{singleton-array-pointer-cast-fail.rs => singleton-array-pointer-cast.rs} (100%) diff --git a/kmir/src/tests/integration/data/prove-rs/singleton-array-pointer-cast-fail.rs b/kmir/src/tests/integration/data/prove-rs/singleton-array-pointer-cast.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/singleton-array-pointer-cast-fail.rs rename to kmir/src/tests/integration/data/prove-rs/singleton-array-pointer-cast.rs