Skip to content

fix(rt): align transparent pointer casts #811

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
automergerpr-permission-manager merged 8 commits into from
Nov 14, 2025
Merged

fix(rt): align transparent pointer casts #811

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
16daa94
fix(rt): align transparent pointer casts
Stevengre Nov 7, 2025
2596f5a
fix(rt): Clarify struct offsets and add pointer tests
Stevengre Nov 7, 2025
3083f4b
test: update expected outputs for interior mutation tests
Stevengre Nov 10, 2025
0f93087
fix: udpate expected output
Stevengre Nov 10, 2025
fdb314c
Update kmir/src/kmir/kdist/mir-semantics/rt/data.md
Stevengre Nov 10, 2025
2f30c37
doc: apply pr suggestion from jost
Stevengre Nov 11, 2025
d55c2e7
add a test to show case
Stevengre Nov 13, 2025
b7eac02
fix
Stevengre Nov 14, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
65 changes: 64 additions & 1 deletion kmir/src/kmir/kdist/mir-semantics/rt/data.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1265,15 +1265,78 @@ the `Value` sort.
Conversion is especially possible for the case of _Slices_ (of dynamic length) and _Arrays_ (of static length),
which have the same representation `Value::Range`.

When the cast crosses transparent wrappers (newtypes that just forward field `0` e.g. `struct Wrapper<T>(T)`), the pointer's
`Place` must be realigned. `#alignTransparentPlace` rewrites the projection list until the source and target
expose the same inner value:
- if the source unwraps more than the target, append an explicit `field(0)` so the target still sees that field;
- if the target unwraps more, strip any redundant tail projections with `#popTransparentTailTo`, leaving the
canonical prefix shared by both sides.

```k
rule <k> #cast(PtrLocal(OFFSET, PLACE, MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET)
=>
PtrLocal(OFFSET, PLACE, MUT, #convertMetadata(META, lookupTy(TY_TARGET)))
PtrLocal(
OFFSET,
#alignTransparentPlace(
PLACE,
#lookupMaybeTy(pointeeTy(lookupTy(TY_SOURCE))),
#lookupMaybeTy(pointeeTy(lookupTy(TY_TARGET)))
),
MUT,
#convertMetadata(META, lookupTy(TY_TARGET))
)
...
</k>
requires #typesCompatible(lookupTy(TY_SOURCE), lookupTy(TY_TARGET))
[preserves-definedness] // valid map lookups checked

syntax Place ::= #alignTransparentPlace ( Place , TypeInfo , TypeInfo ) [function, total]
syntax ProjectionElems ::= #popTransparentTailTo ( ProjectionElems , TypeInfo ) [function, total]

rule #alignTransparentPlace(place(LOCAL, PROJS), typeInfoStructType(_, _, FIELD_TY .Tys, LAYOUT) #as SOURCE, TARGET)
=> #alignTransparentPlace(
place(
LOCAL,
appendP(PROJS, projectionElemField(fieldIdx(0), FIELD_TY) .ProjectionElems)
),
lookupTy(FIELD_TY),
TARGET
)
requires #transparentDepth(SOURCE) >Int #transparentDepth(TARGET)
andBool #zeroFieldOffset(LAYOUT)

rule #alignTransparentPlace(
place(LOCAL, PROJS),
SOURCE,
typeInfoStructType(_, _, FIELD_TY .Tys, LAYOUT) #as TARGET
)
=> #alignTransparentPlace(
place(LOCAL, #popTransparentTailTo(PROJS, lookupTy(FIELD_TY))),
SOURCE,
lookupTy(FIELD_TY)
)
requires #transparentDepth(SOURCE) <Int #transparentDepth(TARGET)
andBool #zeroFieldOffset(LAYOUT)
andBool PROJS =/=K #popTransparentTailTo(PROJS, lookupTy(FIELD_TY))

rule #alignTransparentPlace(PLACE, _, _) => PLACE [owise]

rule #popTransparentTailTo(
projectionElemField(fieldIdx(0), FIELD_TY) .ProjectionElems,
TARGET
)
=> .ProjectionElems
requires lookupTy(FIELD_TY) ==K TARGET

rule #popTransparentTailTo(
X:ProjectionElem REST:ProjectionElems,
TARGET
)
=> X #popTransparentTailTo(REST, TARGET)
requires REST =/=K .ProjectionElems

rule #popTransparentTailTo(PROJS, _) => PROJS [owise]

syntax Metadata ::= #convertMetadata ( Metadata , TypeInfo ) [function, total]
// -------------------------------------------------------------------------------------
```
Expand Down
6 changes: 0 additions & 6 deletions kmir/src/kmir/kdist/mir-semantics/rt/decoding.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,12 +111,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 ::= #layoutOffsets ( MaybeLayoutShape ) [function, total]
rule #layoutOffsets(someLayoutShape(layoutShape(fieldsShapeArbitrary(mk(OFFSETS)), _, _, _, _))) => OFFSETS
rule #layoutOffsets(noLayoutShape) => .MachineSizes
rule #layoutOffsets(_) => .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
Expand Down
45 changes: 45 additions & 0 deletions kmir/src/kmir/kdist/mir-semantics/rt/types.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,33 @@ Pointers to arrays/slices are compatible with pointers to the element type
rule #isArrayOf( _ , _ ) => false [owise]
```

Pointers to structs with a single zero-offset field are compatible with pointers to that field's type
```k
rule #typesCompatible(SRC, OTHER) => true
requires #zeroSizedType(SRC) orBool #zeroSizedType(OTHER)
Comment on lines +66 to +67
Copy link
Member

@jberthold jberthold Nov 11, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A bit puzzled by the orBool here... I would accept it immediately with andBool (one zero-sized thing is as good as another) but what happens if we cast a pointer to non-zero-sized to a zero-sized one and back, should that be allowed? Or which side is not allowed? (zero to non-zero I would guess)

Copy link
Contributor Author

@Stevengre Stevengre Nov 11, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm investigating this with a new test, but it encounters other ndbranches.

Copy link
Contributor Author

@Stevengre Stevengre Nov 11, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It needs a cast from pointer to integer. here: #812

Copy link
Contributor Author

@Stevengre Stevengre Nov 13, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I provided pointer-cast-zst.rs to cover this scenario: it casts a *const Wrapper to *const () (ZST) and back, then asserts the roundtrip preserves the value. Since this test passes, the semantics currently allow non‑zero → zero → non‑zero pointer casts, so we shoud use this orBool to allow this situation.


rule #typesCompatible(typeInfoStructType(_, _, FIELD .Tys, LAYOUT), OTHER)
=> #typesCompatible(lookupTy(FIELD), OTHER)
requires #zeroFieldOffset(LAYOUT)

rule #typesCompatible(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT))
=> #typesCompatible(OTHER, lookupTy(FIELD))
requires #zeroFieldOffset(LAYOUT)

syntax Bool ::= #zeroFieldOffset ( MaybeLayoutShape ) [function, total]

rule #zeroFieldOffset(LAYOUT)
=> #layoutOffsets(LAYOUT) ==K .MachineSizes
orBool #layoutOffsets(LAYOUT) ==K machineSize(mirInt(0)) .MachineSizes
orBool #layoutOffsets(LAYOUT) ==K machineSize(0) .MachineSizes

// Extract field offsets from the struct layout when available (Arbitrary only).
syntax MachineSizes ::= #layoutOffsets ( MaybeLayoutShape ) [function, total]
rule #layoutOffsets(someLayoutShape(layoutShape(fieldsShapeArbitrary(mk(OFFSETS)), _, _, _, _))) => OFFSETS
rule #layoutOffsets(noLayoutShape) => .MachineSizes
rule #layoutOffsets(_) => .MachineSizes [owise]
```

## Determining types of places with projection

A helper function `getTyOf` traverses type metadata (using the type metadata map `Ty -> TypeInfo`) along the applied projections to determine the `Ty` of the projected place.
Expand All @@ -70,6 +97,24 @@ To make this function total, an optional `MaybeTy` is used.
syntax MaybeTy ::= Ty
| "TyUnknown"

syntax MaybeTy ::= #transparentFieldTy ( TypeInfo ) [function, total]

rule #transparentFieldTy(typeInfoStructType(_, _, FIELD .Tys, LAYOUT)) => FIELD
requires #zeroFieldOffset(LAYOUT)
rule #transparentFieldTy(_) => TyUnknown [owise]

syntax Int ::= #transparentDepth ( TypeInfo ) [function, total]

rule #transparentDepth(typeInfoStructType(_, _, FIELD .Tys, LAYOUT))
=> 1 +Int #transparentDepth(lookupTy(FIELD))
requires #zeroFieldOffset(LAYOUT)
rule #transparentDepth(_) => 0 [owise]

syntax TypeInfo ::= #lookupMaybeTy ( MaybeTy ) [function, total]

rule #lookupMaybeTy(TY:Ty) => lookupTy(TY)
rule #lookupMaybeTy(TyUnknown) => typeInfoVoidType

syntax MaybeTy ::= getTyOf( MaybeTy , ProjectionElems ) [function, total]
// -----------------------------------------------------------
rule getTyOf(TyUnknown, _ ) => TyUnknown
Expand Down
14 changes: 14 additions & 0 deletions kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
struct Wrapper(u32);

fn roundtrip(ptr: *const Wrapper) -> u32 {
unsafe {
let erased = ptr as *const ();
let restored = erased as *const Wrapper;
(*restored).0
}
}

fn main() {
let value = Wrapper(0xCAFE_BABE);
assert!(roundtrip(&value) == 0xCAFE_BABE);
}
1 change: 1 addition & 0 deletions kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.smir.json
View file
Open in desktop

Large diffs are not rendered by default.

50 changes: 50 additions & 0 deletions kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
<kmir>
<k>
PtrLocal ( 1 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 29 ) ) .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindAssign (... place: place (... local: local ( 3 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , ty ( 26 ) ) ) , span: span ( 52 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , ty ( 25 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindTransmute , operandCopy ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) , ty ( 27 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueNullaryOp ( nullOpAlignOf , ty ( 28 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 7 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpSub , operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x01\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 9 ) ) ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 8 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpBitAnd , operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) , operandCopy ( place (... local: local ( 7 ) , projection: .ProjectionElems ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 9 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpEq , operandCopy ( place (... local: local ( 8 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 50 ) ) .Statements ) ~> #execTerminator ( terminator (... kind: assert (... cond: operandCopy ( place (... local: local ( 9 ) , projection: .ProjectionElems ) ) , expected: true , msg: assertMessageMisalignedPointerDereference (... required: operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , found: operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) ) , target: basicBlockIdx ( 1 ) , unwind: unwindActionUnreachable ) , span: span ( 50 ) ) ) ~> .K
</k>
<retVal>
noReturn
</retVal>
<currentFunc>
ty ( 31 )
</currentFunc>
<currentFrame>
<currentBody>
ListItem ( basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 2 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , ty ( 25 ) ) ) , span: span ( 51 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 3 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , ty ( 26 ) ) ) , span: span ( 52 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , ty ( 25 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindTransmute , operandCopy ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) , ty ( 27 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueNullaryOp ( nullOpAlignOf , ty ( 28 ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 7 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpSub , operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x01\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 9 ) ) ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 8 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpBitAnd , operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) , operandCopy ( place (... local: local ( 7 ) , projection: .ProjectionElems ) ) ) ) , span: span ( 50 ) ) statement (... kind: statementKindAssign (... place: place (... local: local ( 9 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpEq , operandCopy ( place (... local: local ( 8 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 50 ) ) .Statements , terminator: terminator (... kind: assert (... cond: operandCopy ( place (... local: local ( 9 ) , projection: .ProjectionElems ) ) , expected: true , msg: assertMessageMisalignedPointerDereference (... required: operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , found: operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) ) , target: basicBlockIdx ( 1 ) , unwind: unwindActionUnreachable ) , span: span ( 50 ) ) ) )
ListItem ( basicBlock (... statements: statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueUse ( operandCopy ( place (... local: local ( 3 ) , projection: projectionElemDeref projectionElemField ( fieldIdx ( 0 ) , ty ( 29 ) ) .ProjectionElems ) ) ) ) , span: span ( 50 ) ) .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 53 ) ) ) )
</currentBody>
<caller>
ty ( -1 )
</caller>
<dest>
place (... local: local ( 2 ) , projection: .ProjectionElems )
</dest>
<target>
someBasicBlockIdx ( basicBlockIdx ( 1 ) )
</target>
<unwind>
unwindActionContinue
</unwind>
<locals>
ListItem ( newLocal ( ty ( 29 ) , mutabilityMut ) )
ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 26 ) , mutabilityNot ) )
ListItem ( newLocal ( ty ( 25 ) , mutabilityNot ) )
ListItem ( newLocal ( ty ( 26 ) , mutabilityNot ) )
ListItem ( newLocal ( ty ( 25 ) , mutabilityMut ) )
ListItem ( newLocal ( ty ( 27 ) , mutabilityMut ) )
ListItem ( newLocal ( ty ( 27 ) , mutabilityMut ) )
ListItem ( newLocal ( ty ( 27 ) , mutabilityMut ) )
ListItem ( newLocal ( ty ( 27 ) , mutabilityMut ) )
ListItem ( newLocal ( ty ( 30 ) , mutabilityMut ) )
</locals>
</currentFrame>
<stack>
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( 0 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionContinue , ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 3405691582 , 32 , false ) ) ) , ty ( 28 ) , mutabilityNot ) )
ListItem ( newLocal ( ty ( 29 ) , mutabilityMut ) )
ListItem ( typedValue ( Moved , ty ( 26 ) , mutabilityMut ) )
ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 34 ) , mutabilityNot ) )
ListItem ( newLocal ( ty ( 35 ) , mutabilityMut ) ) ) )
ListItem ( StackFrame ( ty ( -1 ) , place (... local: local ( -1 ) , projection: .ProjectionElems ) , noBasicBlockIdx , unwindActionUnreachable , .List ) )
</stack>
</kmir>
0 ...ation/data/prove-rs/interior-mut2-fail.rs → ...ntegration/data/prove-rs/interior-mut2.rs
View file
Open in desktop
File renamed without changes.
6 changes: 3 additions & 3 deletions kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,10 @@
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
│ span: 0
│
│ (198 steps)
│ (866 steps)
└─ 3 (stuck, leaf)
#traverseProjection ( toLocal ( 11 ) , thunk ( #cast ( PtrLocal ( 3 , place ( ..
span: 91
#setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
span: 32


┌─ 2 (root, leaf, target, terminal)
Expand Down
15 changes: 0 additions & 15 deletions kmir/src/tests/integration/data/prove-rs/show/interior-mut2-fail.main.expected
View file
Open in desktop

This file was deleted.

33 changes: 28 additions & 5 deletions kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,11 +26,34 @@
│ #execBlockIdx ( basicBlockIdx ( 8 ) ) ~> .K
│ function: main
│
│ (8 steps)
└─ 7 (stuck, leaf)
#traverseProjection ( toLocal ( 2 ) , thunk ( #cast ( PtrLocal ( 1 , place ( ...
function: main
span: 80
│ (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
│
│ (17 steps)
└─ 11 (stuck, leaf)
#setLocalValue ( place ( ... local: local ( 1 ) , projection: .ProjectionElems )
function: main
Comment on lines +29 to +55
Copy link
Member

@jberthold jberthold Nov 11, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FYI This now hits a non-deterministic branch on what looks like a pointer alignment check .

Copy link
Collaborator

@dkcumming dkcumming Nov 11, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@jberthold I saw this last night in a previous proof, it comes when the pointer cast is thunked, and then the pointer is branches. I am worried it is happening because it needs to get the address but I haven't looked with details yet. If it needs the address I am not sure what we do

Copy link
Contributor Author

@Stevengre Stevengre Nov 11, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think I solved it before in the big pr. Could I introduce an issue for this and solve it later in another pr?

Copy link
Member

@jberthold jberthold Nov 11, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, we can solve this one later, it should not block this PR

span: 79


┌─ 2 (root, leaf, target, terminal)
Expand Down
7 changes: 6 additions & 1 deletion kmir/src/tests/integration/test_integration.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,6 @@
PROVE_RS_SHOW_SPECS = [
'local-raw-fail',
'interior-mut-fail',
'interior-mut2-fail',
'interior-mut3-fail',
'assert_eq_exp',
'bitwise-not-shift',
Expand Down Expand Up @@ -263,6 +262,12 @@ def test_crate_examples(main_crate: Path, kmir: KMIR, update_expected_output: bo
EXEC_DATA_DIR / 'pointers' / 'pointer-cast-length-test-fail.state',
1000,
),
(
'pointer-cast-zst',
EXEC_DATA_DIR / 'pointers' / 'pointer-cast-zst.smir.json',
EXEC_DATA_DIR / 'pointers' / 'pointer-cast-zst.state',
48,
),
(
'ref-ptr-cases',
EXEC_DATA_DIR / 'pointers' / 'ref_ptr_cases.smir.json',
Expand Down