Fix copy* contract to make it untyped

The intrinsics `copy` and `copy_nonoverlapping` are untyped copies,
so they don't respect the validity requirements of `T`. The copy is
also done on `size_of::<T>() * count` bytes which may be different than
`size_of::<[T; count]>`

Author: celinval

library/core/src/intrinsics.rs

@@ -2728,7 +2728,7 @@ pub const fn is_val_statically_known<T: Copy>(_arg: T) -> bool {
 #[requires(ub_checks::can_dereference(x) && ub_checks::can_write(x))]
 #[requires(ub_checks::can_dereference(y) && ub_checks::can_write(y))]
 #[requires(x.addr() != y.addr() || core::mem::size_of::<T>() == 0)]
-#[requires((x.addr() >= y.addr() + core::mem::size_of::<T>()) || (y.addr() >= x.addr() + core::mem::size_of::<T>()))]
+#[requires(ub_checks::is_nonoverlapping(x as *const (), x as *const (), size_of::<T>(), 1))]
 pub const unsafe fn typed_swap<T>(x: *mut T, y: *mut T) {
     // SAFETY: The caller provided single non-overlapping items behind
     // pointers, so swapping them with `count: 1` is fine.
@@ -2943,11 +2943,11 @@ impl<P: ?Sized, T: ptr::Thin> AggregateRawPtr<*mut T> for *mut P {
 #[inline(always)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_diagnostic_item = "ptr_copy_nonoverlapping"]
+// Copy is "untyped".
 #[requires(!count.overflowing_mul(size_of::<T>()).1
-  && ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src, count))
-  && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)))]
-#[requires(src.addr() != dst.addr() || core::mem::size_of::<T>() == 0)]
-#[requires((src.addr() >= dst.addr() + core::mem::size_of::<T>()) || (dst.addr() >= src.addr() + core::mem::size_of::<T>()))]
+  && ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src as *const crate::mem::MaybeUninit<u8>, count * size_of::<T>()))
+  && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst as *mut u8, count * size_of::<T>())))]
+#[requires(ub_checks::is_nonoverlapping(src as *const (), dst as *const (), size_of::<T>(), count))]
 // TODO: Modifies doesn't work with slices today.
 // https://github.com/model-checking/kani/pull/3295
 // #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))]
@@ -3055,8 +3055,8 @@ pub const unsafe fn copy_nonoverlapping<T>(src: *const T, dst: *mut T, count: us
 #[rustc_diagnostic_item = "ptr_copy"]
 // FIXME: How to verify safety for types that do not implement Copy and count > 1??
 #[requires(!count.overflowing_mul(size_of::<T>()).1
-    && ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src, count))
-    && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)))]
+  && ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src as *const crate::mem::MaybeUninit<u8>, count * size_of::<T>()))
+  && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst as *mut u8, count * size_of::<T>())))]
 // TODO: Modifies doesn't work with slices today.
 // https://github.com/model-checking/kani/pull/3295
 // #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))]