Contract and harness for copy_to, copy_to_nonoverlapping, copy_from, and copy_from_nonoverlapping

[Dhvani-Kapadia]

Description

This PR includes contracts and proof harnesses for the four APIs copy_to, copy_to_nonoverlapping, copy_from, and copy_from_nonoverlapping which are part of the NonNull library in Rust.

Changes Overview:

Covered APIs:
NonNull::copy_to
NonNull::copy_to_nonoverlapping
NonNull::copy_from
NonNull::opy_from_nonoverlapping

Proof harness:
non_null_check_copy_to
non_null_check_copy_to_nonoverlapping
non_null_check_copy_from
non_null_check_copy_from_nonoverlapping,

Revalidation

To revalidate the verification results, run path_to/kani/scripts/kani verify-std -Z unstable-options "path/to/library" -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify. This will run all four harnesses in the module. All default checks should pass:

SUMMARY:
** 0 of 141 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.62114185s

Complete - 6 successfully verified harnesses, 0 failures, 6 total.

Towards issue #53

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[celinval]

Thanks!

[Dhvani-Kapadia]

This is my contract and harness for fn copy_to,I run into these two failed checks.could you please help me understand where I am going wrong?

#[requires(
        count.checked_mul(core::mem::size_of::<T>()).map_or(false, |size| size <= isize::MAX as usize) &&        
ub_checks::can_dereference(self.as_ptr()) &&
       (count == 0 || ub_checks::can_dereference(self.as_ptr().wrapping_add(count - 1))) &&  
       ub_checks::can_write(dest.as_ptr()) &&

        (count == 0 || ub_checks::can_write(dest.as_ptr().wrapping_add(count - 1))) &&

        kani::mem::same_allocation(self.as_ptr(), self.as_ptr().wrapping_add(count - 1)) &&

        kani::mem::same_allocation(dest.as_ptr(), dest.as_ptr().wrapping_add(count - 1))
    )]
    #[ensures(|_: &()| 
        ub_checks::can_dereference(self.as_ptr()) &&
        ub_checks::can_dereference(dest.as_ptr()))]
    #[kani::modifies(self.as_ptr(), dest.as_ptr())]
    pub const unsafe fn copy_to(self, dest: NonNull<T>, count: usize)
    where
        T: Sized,
    {
        // SAFETY: the caller must uphold the safety contract for `copy`.
        unsafe { ptr::copy(self.pointer, dest.as_ptr(), count) }
    }
 

#[kani::proof_for_contract(NonNull::<T>::copy_to)]
    pub fn non_null_check_copy_to() {
        // Generate arbitrary raw pointers for src and dest
        const SIZE: usize = mem::size_of::<i32>() * 100;
        let mut generator = PointerGenerator::<SIZE>::new();  
        let src_ptr: *mut i32 =  generator.any_in_bounds().ptr as *mut i32;
        let dest_ptr: *mut i32 =  generator.any_in_bounds().ptr as *mut i32;
        let src_nonnull = NonNull::new(src_ptr).unwrap();
        let dest_nonnull = NonNull::new(dest_ptr).unwrap();
        let max_count = SIZE / mem::size_of::<i32>();
        let count: usize = kani::any_where(|&x| x > 0 && x <= max_count);
        unsafe { src_nonnull.copy_to(dest_nonnull, count); }
            }
        }

check 39: memmove.assigns.2
	 - Status: FAILURE
	 - Description: "Check that array_replace((const void *)(char *)dest, ...) is allowed by the assigns clause"
	 - Location: <builtin-library-memmove>:34 in function memmove //ADD modifies clause

     Check 28: kani::mem::is_inbounds::<(), i32>.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::<(), i32> ,

[zhassan-aws]

@Dhvani-Kapadia the modifies clause:

#[kani::modifies(dest.as_ptr())]

states that only the element that dest points to is modified. However, the function modifies count elements starting at dest. To fix this, the modifies clause needs to be in terms of the entire slice, e.g.

#[kani::modifies(NonNull::slice_from_raw_parts(dest, count).as_ptr()]

[zhassan-aws]

The same thing applies to the can_write and can_dereference conditions: both of them need to refer to the entire slice, i.e.:

ub_checks::can_dereference(NonNull::slice_from_raw_parts(self, count).as_ptr())

ub_checks::can_write(NonNull::slice_from_raw_parts(dest, count).as_ptr())

[QinyuanWu]

@zhassan-aws Thank you for the suggestion! I've applied the changes and the two failed checks for copy_to are resolved.

[Dhvani-Kapadia]

Thanks @zhassan-aws, @celinval and @qinheping ,
with Olivias help the two failed checks passed.Could you please review it?

[Dhvani-Kapadia]

Thanks @celinval , I resolved the conversations.