ub_checks::can_dereference does not support reasoning about pointer to unallocated memory

[QinyuanWu]

@zhassan-aws As part of the attempt to constrain count to be within the allocated memory for functions such as add and to specify this constrain in the contract requires instead of the harness, we tried ub_checks::can_dereference in the following way:

    #[requires(count.checked_mul(core::mem::size_of::<T>()).is_some() 
        && count * core::mem::size_of::<T>() <= isize::MAX as usize
        && ub_checks::can_dereference(self.pointer)
        && ub_checks::can_dereference(self.pointer.wrapping_offset(count as size)))]
    #[ensures(|result: &NonNull<T>| result.as_ptr() == self.as_ptr().offset(count as isize))]
    pub const unsafe fn add(self, count: usize) -> Self
    where
        T: Sized,
    {
        unsafe { NonNull { pointer: intrinsics::offset(self.pointer, count) } }
    }

Harness:

    #[kani::proof_for_contract(NonNull::add)]
    pub fn non_null_check_add() {
        const SIZE: usize = 100000;
        // Randomize pointer offset within array bound
        let offset = kani::any_where(|x| * x <= SIZE as isize);
        kani::assume(offset >= 0);
        // Create a non-deterministic array of size SIZE
        let arr: [i8; SIZE] = kani::any();  
        // Get a raw pointer to the array
        let raw_ptr: *mut i8 = arr.as_ptr() as *mut i8;  
        // NonNUll pointer to the random offset
        let ptr = unsafe { NonNull::new(raw_ptr.offset(offset)).unwrap()};
        // Create a non-deterministic count value
        let count: usize = kani::any();  

        unsafe {
            // Add a positive offset to pointer
            let result = ptr.add(count);
        }
    }

Note count can be any usize value. This causes the following failures:

SUMMARY:
 ** 2 of 251 failed
Failed Checks: Kani does not support reasoning about pointer to unallocated memory
 File: "/Users/owo/Desktop/verify-rust-std/library/core/src/lib.rs", line 426, in kani::mem::is_inbounds::<(), i8>
Failed Checks: attempt to compute offset which would overflow
 File: "/Users/owo/Desktop/verify-rust-std/library/core/src/ptr/const_ptr.rs", line 396, in ptr::const_ptr::<impl *const i8>::offset

Is this expected and is it true that we cannot use can_dereference to check whether a pointer is out of bound? And if so I want to confirm that we will be waiting on a new API(potentially same_objecct or another one?) to achieve this constraint goal in the contract? Thank you!
can_dereference definition:

    /// Checks if a pointer can be dereferenced, ensuring:
    ///   * `src` is valid for reads (see [`crate::ptr`] documentation).
    ///   * `src` is properly aligned (use `read_unaligned` if not).
    ///   * `src` points to a properly initialized value of type `T`.
    ///
    /// [`crate::ptr`]: https://doc.rust-lang.org/std/ptr/index.html
    pub fn can_dereference<T>(src: *const T) -> bool {
        let _ = src;
        true
    }

[zhassan-aws]

Hi @QinyuanWu. Yes, unfortunately, this is currently a limitation with can_dereference. Unless the offset is restricted in the harness (but it shouldn't be), the new pointer can go out-of-bounds, and Kani will fail.

The PR that adds an API to check if two pointers are within the same allocation has been merged: model-checking/kani#3583

Once this is available in this repo, you can start using it.