Use of PointerGenerator to mimic array

[QinyuanWu]

From the PR feedback, I was trying to use PointerGenerator instead of initializing an actual array:

    #[kani::proof_for_contract(NonNull::read)]
    pub fn non_null_check_read() {
        const ARR_LEN: usize = 100;
        let mut generator = kani::PointerGenerator::<ARR_LEN>::new();
        let raw_ptr: *mut i8 = generator.any_in_bounds().ptr;
        let offset = kani::any_where(|x| * x < ARR_LEN);
        let nonnull_ptr = unsafe { NonNull::new(raw_ptr).unwrap()};
        unsafe {
            let result = nonnull_ptr.add(offset).read();
            kani::assert( *nonnull_ptr.as_ptr().add(offset) == result, "read returns the correct value");            
        }
    }

Function contract:

    #[requires(ub_checks::can_dereference(self.pointer))]
    pub const unsafe fn read(self) -> T
    where
        T: Sized,
    {
        // SAFETY: the caller must uphold the safety contract for `read`.
        unsafe { ptr::read(self.pointer) }
    }

However, I encounter this failed check:

Check 54: kani::mem::is_inbounds::<(), i8>.assertion.1
	 - Status: FAILURE
	 - Description: "Kani does not support reasoning about pointer to unallocated memory"
	 - Location: library/core/src/lib.rs:421:1 in function kani::mem::is_inbounds::<(), i8>

Is there any step that I missed in using the PointerGenerator? I found that if I don't call nonnull_ptr.add(offset) then the failure is resolved. Thanks! @zhassan-aws

[zhassan-aws]

Hi @QinyuanWu. The PointerGenerator takes care of generating a pointer whose location within the buffer is non-deterministic. So, there is no need for adding a non-deterministic offset before calling read.