From ee885521bbfaba05ff693c15999e12b6b6ee55ca Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 16 Jul 2024 11:25:50 -0700
Subject: [PATCH] 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`.
---
 library/core/src/intrinsics.rs | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/library/core/src/intrinsics.rs b/library/core/src/intrinsics.rs
index 396226d44143..1588a979146e 100644
--- a/library/core/src/intrinsics.rs
+++ b/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_dereference(core::ptr::slice_from_raw_parts(src as *const crate::mem::MaybeUninit<T>, 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>()))]
+#[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<T>, count))
+  && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, 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)))]