Proper use of ub_checks::can_write to check pointer bounds

[QinyuanWu]

For the add function in NonNull we have the following contract:

    #[requires(count.checked_mul(core::mem::size_of::<T>()).is_some())] // Prevent offset overflow
    #[requires(count * core::mem::size_of::<T>() <= isize::MAX as usize)] // SAFETY: count * size_of::<T>() does not overflow isize
    #[requires(ub_checks::can_write(self.as_ptr().offset(count as isize)))]// Check operation is within allocated memory
    #[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,
    {
        // 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) } }
    }

The third requires clause is intend to check whether the shifted pointer will be within the boundary of the allocated memory since count is initialized to kani::any(). However, I got the following error:

SUMMARY:
 ** 3 of 1829 failed
Failed Checks: offset: attempt to compute number in bytes which would overflow
 File: "core/src/ptr/mut_ptr.rs", line 413, in ptr::mut_ptr::<impl *mut i8>::offset
Failed Checks: attempt to compute offset which would overflow
 File: "core/src/ptr/mut_ptr.rs", line 413, in ptr::mut_ptr::<impl *mut i8>::offset
Failed Checks: Kani does not support reasoning about pointer to unallocated memory
 File: "core/src/lib.rs", line 426, in kani::mem::is_inbounds::<(), i8>

I have the following harness:

    #[kani::proof_for_contract(NonNull::add)]
    pub fn non_null_check_add() {
        const SIZE: usize = 100000;
        // Randomiz pointer offset within array bound
        let offset = kani::any_where(|x| *x < SIZE);
        // 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.add(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);
        }

Am I using can_write correctly or is there something I'm missing? Thanks. @zhassan-aws @celinval

[zhassan-aws]

Hi @QinyuanWu. This is an issue with the order of the requires clauses: a requires clause does not seem to take the previous requires clauses into account. You can see a minimal reproducer in model-checking/kani#3575.

The workaround is to combine dependent requires clauses into a single one, e.g. if you have

#[requires(A)]
#[requires(B)]

where B needs to assume A, they should be rewritten as:

#[requires(A && B)]

In your case, the following requires clause:

#[requires(ub_checks::can_write(self.as_ptr().offset(count as isize)))]

relies on this other one:

#[requires(count.checked_mul(core::mem::size_of::<T>()).is_some())] // Prevent offset overflow

to prevent an overflow in offset. Thus, combining them into a single requires clause should resolve the issue.

[QinyuanWu]

@zhassan-aws I combined all three clauses into one but got the same error:

    #[requires(count.checked_mul(core::mem::size_of::<T>()).is_some() 
        && count * core::mem::size_of::<T>() <= isize::MAX as usize
        && ub_checks::can_write(self.as_ptr().offset(count as isize)))] // Prevent offset overflow

[zhassan-aws]

Thanks for checking @QinyuanWu. The failure is due to a bug in Kani. I filed this as model-checking/kani#3582.

[QinyuanWu]

After discussion with @zhassan-aws we will hold off from using ub_checks::can_write in the contract to check the pointer boundary as the kani team is working on a new API that does this job(given a pointer, check whether it is pointing to an address within the allocated memory). The current workaround is to use assume inside the harness to constrain count to avoid pointer out of bound.