Simpler approach to verify add, sub, offset for integer types

[QinyuanWu]

For NonNull::add we currently have the following harness:

       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);
        }

This is technically creating a slice out of the original array and calling add to shift the pointer.
Since we want to cover more integer types and also be efficient, would it be appropriate to verify this way(take u8 as example):

        let ptr_u8: *mut u8 = &mut kani::any();
        let nonnull_ptr_u8 = NonNull::new(ptr_u8).unwrap();
        let count: usize = kani::any();  

        unsafe {
            let result = nonnull_ptr_u8.add(count);
        }

In this case, the only valid value for count would be 1(will be restricted by the contract), which will move the pointer to point to the end of the integer. I tried it and all verification checks passed for this example. @zhassan-aws

[celinval]

Are you able to use the PointerGenerator instead?

[QinyuanWu]

According to the documentation, PointerGenerator may not be the best choice for the pointer arithmetic APIs since we want to verify pointer allocation and cover all possible address spaces and include pointer wrapping scenarios:

NonNull::add contract:

    #[requires(count.checked_mul(core::mem::size_of::<T>()).is_some() 
        && count * core::mem::size_of::<T>() <= isize::MAX as usize
        && (self.pointer as isize).checked_add(count as isize * core::mem::size_of::<T>() as isize).is_some() // check wrapping add
        && kani::mem::same_allocation(self.pointer, self.pointer.wrapping_offset(count as isize)))]
    #[ensures(|result: &NonNull<T>| result.as_ptr() == self.as_ptr().offset(count as isize)
        && kani::mem::same_allocation(result.pointer, self.pointer))]
    pub const unsafe fn add(self, count: usize) -> Self
    where
        T: Sized,
    {
        // SAFETY: the caller must uphold the safety contract for `offset`.
        // Additionally safety contract of `offset` guarantees that the resulting pointer is
        // pointing to an allocation, there can't be an allocation at null, thus it's safe to
        // construct `NonNull`.
        unsafe { NonNull { pointer: intrinsics::offset(self.pointer, count) } }
    }

[celinval]

Yes, you are correct that it is not ideal. However, Kani does have a limitation today that it cannot reason about the allocation of all possible adresses. Thus, if your harness is manipulating a pointer and it needs to be able to be aware of the allocation, the generator is a good stop gap.