Casting pointer to usize and back have unexpected behavior

[celinval]

I tried this code:

//! This module contains a dummy implementation of a slice iterator.
//!
//! It shows how computing pointer offset by using integer arithmetic + casting does not yield
//! the same result as operating on pointer directly.

#![feature(core_intrinsics)]

use std::marker::PhantomData;

#[kani::proof]
fn check_addr_offset() {
    let array = [0, 1, 2];
    let slice = &array;
    let mut iter = MyIter::new(slice);
    let first = iter.next().unwrap();
    let second = iter.next().unwrap();
    let third = iter.next().unwrap();
    assert!(iter.next().is_none());
    assert_eq!(*first, 0);
    assert_eq!(*second, 1);
    assert_eq!(*third, 2);
}

#[kani::proof]
#[kani::stub(addr_offset, ptr_offset)]
fn check_ptr_offset() {
    check_addr_offset();
}

pub struct MyIter<'a> {
    ptr: *const i8,
    end: *const i8,
    phantom_data: PhantomData<&'a i8>,
}

impl<'a> MyIter<'a> {
    pub fn new(slice: &[i8]) -> Self {
        MyIter { ptr: slice.as_ptr(), end: addr_offset(slice.as_ptr(), slice.len()),
        phantom_data: PhantomData
        }
    }

    pub fn next(&mut self) -> Option<&'a i8> {
        if self.ptr == self.end {
            None
        } else {
            let result = unsafe { &*self.ptr };
            self.ptr = addr_offset(self.ptr, 1);
            Some(result)
        }
    }
}

/// Version of offset that converts pointer to usize, performs the offset, then cast the result.
fn addr_offset(ptr: *const i8, byte_offset: usize) -> *const i8 {
    std::intrinsics::wrapping_add(ptr as usize, byte_offset) as *const i8
}

/// Version that does a pointer offset directly via intrinsic.
fn ptr_offset(ptr: *const i8, byte_offset: usize) -> *const i8 {
    unsafe { std::intrinsics::arith_offset(ptr, byte_offset as isize) }
}

using the following command line invocation:

kani dummy_iter.rs

with Kani version: 0.56.0

I expected to see this happen: Verification to succeed.

Instead, this happened: The harness where we compute offset using the pointer address fails, while the one doing the offset in the pointer directly succeeds.

Note that for some reason, the second element is set to a non-deterministic value, while the third element is correct. I enabled -Z uninit-checks as well as --extra-pointer-checks, and none of them detected any other issue.

This issue is a blocker for #90.

[celinval]

@remi-delmas-3000 @tautschnig, I could really use your help to understand what's going on.