Contract and harness for copy_to, copy_to_nonoverlapping, copy_from, and copy_from_nonoverlapping #149
Conversation
| @@ -934,6 +934,12 @@ impl<T: ?Sized> NonNull<T> { | |||
| #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces | |||
| #[stable(feature = "non_null_convenience", since = "1.80.0")] | |||
| #[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")] | |||
| #[kani::requires(count * core::mem::size_of::<T>() <= isize::MAX as usize)] | |||
There was a problem hiding this comment.
This operation can overflow. Consider using checked_mul or overflowing_mul instead
| @@ -934,6 +934,12 @@ impl<T: ?Sized> NonNull<T> { | |||
| #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces | |||
| #[stable(feature = "non_null_convenience", since = "1.80.0")] | |||
| #[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")] | |||
| #[kani::requires(count * core::mem::size_of::<T>() <= isize::MAX as usize)] | |||
| #[requires(ub_checks::can_dereference(self.as_ptr()))] //The pointer is valid | |||
| #[requires(ub_checks::can_dereference(dest.as_ptr()))] | |||
There was a problem hiding this comment.
I don't think you need to be able to dereference the destination. You should check if you can write to it for the given count.
| @@ -934,6 +934,12 @@ impl<T: ?Sized> NonNull<T> { | |||
| #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces | |||
| #[stable(feature = "non_null_convenience", since = "1.80.0")] | |||
| #[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")] | |||
| #[kani::requires(count * core::mem::size_of::<T>() <= isize::MAX as usize)] | |||
| #[requires(ub_checks::can_dereference(self.as_ptr()))] //The pointer is valid | |||
There was a problem hiding this comment.
I don't think pointer requires a valid value of type T. I.e., I think you need to cast this to *const MaybeUninit<T>.
| #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr() as *const T))] | ||
| #[ensures(|result: &()| ub_checks::can_dereference(dest.as_ptr() as *const T))] |
There was a problem hiding this comment.
This is also not necessarily true since the copy is untyped.
| #[kani::requires(count * core::mem::size_of::<T>() <= isize::MAX as usize)] | ||
| #[requires(ub_checks::can_dereference(self.as_ptr()))] | ||
| #[requires(ub_checks::can_dereference(dest.as_ptr()))] | ||
| #[requires((self.as_ptr() as usize).abs_diff(dest.as_ptr() as usize) >= count * core::mem::size_of::<T>())] | ||
| #[ensures(|result: &()| ub_checks::can_dereference(self.as_ptr()))] | ||
| #[ensures(|result: &()| ub_checks::can_dereference(dest.as_ptr()))] |
There was a problem hiding this comment.
Can you create a function to allow you to reuse the requires and ensures clauses of all these predicates. Also, the ub_checks module contains a function is_nonoverlapping that you can use
| kani::assume(kani::mem::can_dereference(src_u8)); | ||
| kani::assume(kani::mem::can_dereference( | ||
| src_u8.add(core::mem::size_of::<i32>() - 1), | ||
| )); | ||
| kani::assume(kani::mem::can_dereference(dest_u8)); | ||
| kani::assume(kani::mem::can_dereference( | ||
| dest_u8.add(core::mem::size_of::<i32>() - 1), | ||
| )); |
There was a problem hiding this comment.
Please remove these assumptions. As a rule of thumb, you should minimize assumptions in the harnesses themselves.
| let src = NonNull::new(&mut src_value as *mut i32).unwrap(); | ||
| let dest = NonNull::new(&mut dest_value as *mut i32).unwrap(); |
There was a problem hiding this comment.
Can you please try to create a few more combinations of pointers? You can try using the PointerGenerator or some other code.
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.
Resolves #53
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.