diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/types.md b/kmir/src/kmir/kdist/mir-semantics/rt/types.md index 3998cb3eb..31ad4f915 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/types.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/types.md @@ -76,29 +76,18 @@ It also implements cancellation of inverse projections (such as casting from one The `#pointeeProjection` function computes, for compatible pointee types, how to project from one pointee to the other. +It uses a **source-first strategy**: always unwrap the source type (struct wrapper or array) before +attempting to unwrap the target type. This eliminates non-deterministic overlap between source-side +and target-side rules, because a type cannot be both a struct and an array simultaneously. +When the source cannot be unwrapped further, target-side unwrapping is handled by `#pointeeProjectionTarget`. + ```k syntax MaybeProjectionElems ::= #pointeeProjection ( TypeInfo , TypeInfo ) [function, total] ``` A short-cut rule for identical types takes preference. -As a default, no projection elements are returned for incompatible types. ```k rule #pointeeProjection(T , T) => .ProjectionElems [priority(40)] - rule #pointeeProjection(_ , _) => NoProjectionElems [owise] -``` - -Pointers to arrays/slices are compatible with pointers to the element type -```k - rule #pointeeProjection(typeInfoArrayType(TY1, _), TY2) - => maybeConcatProj( - projectionElemConstantIndex(0, 0, false), - #pointeeProjection(lookupTy(TY1), TY2) - ) - rule #pointeeProjection(TY1, typeInfoArrayType(TY2, _)) - => maybeConcatProj( - projectionElemSingletonArray, - #pointeeProjection(TY1, lookupTy(TY2)) - ) ``` Pointers to zero-sized types can be converted from and to. No recursion beyond the ZST. @@ -112,9 +101,11 @@ Pointers to zero-sized types can be converted from and to. No recursion beyond t [priority(45)] ``` -Pointers to structs with a single zero-offset field are compatible with pointers to that field's type -```k +Source-side: unwrap structs and arrays from the source type first. +When source is an array and target is a transparent wrapper whose inner type equals the source, +the source should be wrapped rather than unwrapped (e.g., `*const [u8;2] → *const Wrapper([u8;2])`). +```k rule #pointeeProjection(typeInfoStructType(_, _, FIELD .Tys, LAYOUT), OTHER) => maybeConcatProj( projectionElemField(fieldIdx(0), FIELD), @@ -122,12 +113,21 @@ Pointers to structs with a single zero-offset field are compatible with pointers ) requires #zeroFieldOffset(LAYOUT) - rule #pointeeProjection(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT)) + rule #pointeeProjection(SRC:TypeInfo, typeInfoStructType(_NAME, _ADTDEF, FIELD .Tys, LAYOUT)) => maybeConcatProj( projectionElemWrapStruct, - #pointeeProjection(OTHER, lookupTy(FIELD)) + #pointeeProjection(SRC, lookupTy(FIELD)) + ) + requires #isArrayType(SRC) + andBool #zeroFieldOffset(LAYOUT) + andBool lookupTy(FIELD) ==K SRC + [priority(42)] + + rule #pointeeProjection(typeInfoArrayType(TY1, _), TY2) + => maybeConcatProj( + projectionElemConstantIndex(0, 0, false), + #pointeeProjection(lookupTy(TY1), TY2) ) - requires #zeroFieldOffset(LAYOUT) ``` Pointers to `MaybeUninit` can be cast to pointers to `X`. @@ -148,6 +148,34 @@ which is a singleton struct (see above). andBool #lookupMaybeTy(getFieldTy(#lookupMaybeTy(getFieldTy(MAYBEUNINIT_TYINFO, 1)), 0)) ==K ELEM_TYINFO ``` +Fallback: source is not unwrappable, delegate to target-side. +```k + rule #pointeeProjection(SRC, TGT) => #pointeeProjectionTarget(SRC, TGT) [owise] +``` + +Target-side fallback: only reached when source cannot be unwrapped further. +After one step of target unwrapping, recurse back to `#pointeeProjection` to maintain +the source-first strategy. + +```k + syntax MaybeProjectionElems ::= #pointeeProjectionTarget ( TypeInfo , TypeInfo ) [function, total] + + rule #pointeeProjectionTarget(TY1, typeInfoArrayType(TY2, _)) + => maybeConcatProj( + projectionElemSingletonArray, + #pointeeProjection(TY1, lookupTy(TY2)) + ) + + rule #pointeeProjectionTarget(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT)) + => maybeConcatProj( + projectionElemWrapStruct, + #pointeeProjection(OTHER, lookupTy(FIELD)) + ) + requires #zeroFieldOffset(LAYOUT) + + rule #pointeeProjectionTarget(_, _) => NoProjectionElems [owise] +``` + ```k syntax Bool ::= #zeroFieldOffset ( MaybeLayoutShape ) [function, total] // -------------------------------------------------------------------- diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-nested-wrapper-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-nested-wrapper-fail.rs new file mode 100644 index 000000000..9df7ec0f8 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-nested-wrapper-fail.rs @@ -0,0 +1,12 @@ +// [T; N] -> W2(W1([T; N])) - nested struct wrapping on target +#[derive(Clone, Copy, PartialEq, Debug)] +struct Inner([u8; 2]); + +#[derive(Clone, Copy, PartialEq, Debug)] +struct Outer(Inner); + +fn main() { + let arr: [u8; 2] = [11, 22]; + let o: Outer = unsafe { *((&arr) as *const [u8; 2] as *const Outer) }; + assert_eq!(o.0 .0, [11, 22]); +} diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-singleton-wrapped-array-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-singleton-wrapped-array-fail.rs new file mode 100644 index 000000000..1e40d8de2 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-singleton-wrapped-array-fail.rs @@ -0,0 +1,9 @@ +// [T; N] -> W([[T; N]; 1]) - singleton-array wrapping array (in-wrapper) on target +#[derive(Clone, Copy, PartialEq, Debug)] +struct Wrapper([[u8; 2]; 1]); + +fn main() { + let arr: [u8; 2] = [11, 22]; + let w: Wrapper = unsafe { *((&arr) as *const [u8; 2] as *const Wrapper) }; + assert_eq!(w.0, [[11, 22]]); +} diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-wrapper-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-wrapper-fail.rs new file mode 100644 index 000000000..ae40e8d8b --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-wrapper-fail.rs @@ -0,0 +1,8 @@ +#[derive(Clone, Copy, PartialEq, Debug)] +struct Wrapper([u8; 2]); + +fn main() { + let arr: [u8; 2] = [11, 22]; + let w: Wrapper = unsafe { *((&arr) as *const [u8; 2] as *const Wrapper) }; + assert_eq!(w.0, [11, 22]); +} diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-nested-wrapper-to-array.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-nested-wrapper-to-array.rs new file mode 100644 index 000000000..ca931f6cc --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/ptr-cast-nested-wrapper-to-array.rs @@ -0,0 +1,9 @@ +// W2(W1([T; N])) -> [T; N] - nested struct wrapping on source +struct Inner([u8; 2]); +struct Outer(Inner); + +fn main() { + let o = Outer(Inner([11, 22])); + let arr: [u8; 2] = unsafe { *((&o) as *const Outer as *const [u8; 2]) }; + assert_eq!(arr, [11, 22]); +} diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-singleton-wrapped-array-to-array.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-singleton-wrapped-array-to-array.rs new file mode 100644 index 000000000..58aa5f74c --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/ptr-cast-singleton-wrapped-array-to-array.rs @@ -0,0 +1,8 @@ +// W([[T; N]; 1]) -> [T; N] - singleton-array wrapping array (in-wrapper) on source +struct Wrapper([[u8; 2]; 1]); + +fn main() { + let w = Wrapper([[11, 22]]); + let arr: [u8; 2] = unsafe { *((&w) as *const Wrapper as *const [u8; 2]) }; + assert_eq!(arr, [11, 22]); +} diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-wrapper-to-array.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-wrapper-to-array.rs new file mode 100644 index 000000000..dbc4625ac --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/ptr-cast-wrapper-to-array.rs @@ -0,0 +1,7 @@ +struct Wrapper([u8; 2]); + +fn main() { + let w = Wrapper([11, 22]); + let arr: [u8; 2] = unsafe { *((&w) as *const Wrapper as *const [u8; 2]) }; + assert_eq!(arr, [11, 22]); +} diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-nested-wrapper-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-nested-wrapper-fail.main.expected new file mode 100644 index 000000000..7ea5e8b1e --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-nested-wrapper-fail.main.expected @@ -0,0 +1,39 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (128 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 + │ + │ (11 steps) + └─ 7 (stuck, leaf) + #traverseProjection ( toLocal ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( + function: main + span: 282 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-singleton-wrapped-array-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-singleton-wrapped-array-fail.main.expected new file mode 100644 index 000000000..a7bbe1146 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-singleton-wrapped-array-fail.main.expected @@ -0,0 +1,39 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (128 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 + │ + │ (10 steps) + └─ 7 (stuck, leaf) + #traverseProjection ( toLocal ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( + function: main + span: 282 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-fail.main.expected new file mode 100644 index 000000000..2a3653a3e --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-fail.main.expected @@ -0,0 +1,40 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (128 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 + │ + │ (154 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 a0486027b..ba7faccec 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -68,6 +68,9 @@ 'volatile_store_static-fail', 'volatile_load_static-fail', 'box_heap_alloc-fail', + 'ptr-cast-array-to-wrapper-fail', + 'ptr-cast-array-to-nested-wrapper-fail', + 'ptr-cast-array-to-singleton-wrapped-array-fail', ]