Conversation
| ┃ │ (99 steps) | ||
| ┃ └─ 10 (stuck, leaf) | ||
| ┃ #ProgramError ( #UBErrorPtrOffsetDiff ( PtrLocal ( 1 , place ( ... local: local |
There was a problem hiding this comment.
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); |
There was a problem hiding this comment.
This operation should pass but fails because of the problem with ConstantIndex vs PointerOffset
There was a problem hiding this comment.
Others are passing all good? I see some other stuck branches in the proof tree above
There was a problem hiding this comment.
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).
| 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); |
There was a problem hiding this comment.
Others are passing all good? I see some other stuck branches in the proof tree above
`ptr_offset_from` intrinsics (#885)
Implements the
ptr_offset_from[_unsigned]intrinsics for pointers with offset, basic case only.