Skip to content

Conversation

@jberthold
Copy link
Member

Implements the ptr_offset_from[_unsigned] intrinsics for pointers with offset, basic case only.

Comment on lines +46 to +48
┃ │ (99 steps)
┃ └─ 10 (stuck, leaf)
┃ #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 1 , place ( ... local: local
Copy link
Member Author

Choose a reason for hiding this comment

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

The test program uncovered a problem caused by making a pointer from a reference with offset:

let a = [1,2,3];
let a1_p: *const i32 = &a[1];

yields a pointer without size information nor offset in the metadata.

PtrLocal ( 
    0 ,
    place ( ... 
        local: local ( 2 ) ,
        projection: projectionElemConstantIndex ( ... offset: 1 , minLength: 0 , fromEnd: false )  .ProjectionElems ) ,
    mutabilityNot ,
    metadata ( noMetadataSize , 0 , noMetadataSize ) )

One would instead expect a pointer where the ConstantIndex projection is replaced by an offset, and the metadata indicates the original size of the array.
The test program fails here because the two pointers have different projection instead of different offsets. It would be possible to add a rule to the intrinsic for this case but the problem lies deeper.

This should be addressed when working on #784 .

assert_eq!(ptr_offset_from_unsigned(a1_p, a_p), 1);
},
1 => unsafe { // correct and expected operation on addresses within arrays
assert_eq!(a3.offset_from(a1), 2);
Copy link
Member Author

Choose a reason for hiding this comment

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

This operation should pass but fails because of the problem with ConstantIndex vs PointerOffset

Copy link
Collaborator

Choose a reason for hiding this comment

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

Others are passing all good? I see some other stuck branches in the proof tree above

Copy link
Member Author

Choose a reason for hiding this comment

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

Cases 2..4 are intended to become stuck because they are undefined behaviour (although the rustc compiled program executes the function calls in 2 and 3 - the random addresses are of course unlikely to produce 0xdeadbeef).

@jberthold jberthold marked this pull request as ready for review December 9, 2025 09:56
assert_eq!(ptr_offset_from_unsigned(a1_p, a_p), 1);
},
1 => unsafe { // correct and expected operation on addresses within arrays
assert_eq!(a3.offset_from(a1), 2);
Copy link
Collaborator

Choose a reason for hiding this comment

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

Others are passing all good? I see some other stuck branches in the proof tree above

@jberthold jberthold merged commit e42fd70 into master Dec 9, 2025
7 checks passed
@jberthold jberthold deleted the offset_from-intrinsics branch December 9, 2025 22:31
@jberthold jberthold mentioned this pull request Dec 9, 2025
Stevengre added a commit that referenced this pull request Dec 10, 2025
`ptr_offset_from` intrinsics (#885)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants