Some fixes + trying to clean up the metadata stuff

Author: celinval

library/core/src/intrinsics.rs

@@ -3323,7 +3323,7 @@ pub const fn ptr_metadata<P: ptr::Pointee<Metadata = M> + ?Sized, M>(_ptr: *cons
   && 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))
   && ub_checks::is_nonoverlapping(src as *const (), dst as *const (), size_of::<T>(), count))]
-#[ensures(|_| { check_copy_untyped(src, dst, count)}) ]
+#[ensures(|_| { check_copy_untyped(src, dst, count)})]
 #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))]
 pub const unsafe fn copy_nonoverlapping<T>(src: *const T, dst: *mut T, count: usize) {
     extern "rust-intrinsic" {
@@ -3427,7 +3427,6 @@ pub const unsafe fn copy_nonoverlapping<T>(src: *const T, dst: *mut T, count: us
 #[inline(always)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_diagnostic_item = "ptr_copy"]
-// FIXME(kani): 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 as *const crate::mem::MaybeUninit<T>, count))
   && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)))]
@@ -3543,10 +3542,14 @@ pub const unsafe fn write_bytes<T>(dst: *mut T, val: u8, count: usize) {
     }
 }
 
-// Ensures the initialization state is preserved.
-// This is used for contracts only.
+/// Return whether the initialization state is preserved.
+///
+/// This is used for contracts only.
+/// FIXME: Change this once we add support to quantifiers.
 #[allow(dead_code)]
+#[allow(unused_variables)]
 fn check_copy_untyped<T>(src: *const T, dst: *mut T, count: usize) -> bool {
+    #[cfg(kani)]
     if count > 0 {
         let byte = kani::any_where(| sz: &usize | *sz < size_of::< T >());
         let elem = kani::any_where(| val: &usize | *val < count);
@@ -3557,6 +3560,8 @@ fn check_copy_untyped<T>(src: *const T, dst: *mut T, count: usize) -> bool {
     } else {
         true
     }
+    #[cfg(not(kani))]
+    false
 }
 
 /// Inform Miri that a given pointer definitely has a certain alignment.
@@ -3706,7 +3711,7 @@ mod verify {
         let mut generator = PointerGenerator::<char, 10>::new();
         let src = generator.generate_ptr();
         let dst = if kani::any() {
-            generator.generate_ptr();
+            generator.generate_ptr()
         } else {
             PointerGenerator::<char, 10>::new().generate_ptr()
         };
@@ -3720,9 +3725,9 @@ mod verify {
     fn check_copy_nonoverlapping() {
         let mut generator = PointerGenerator::<char, 10>::new();
         let src = generator.generate_ptr();
-        // Destination may or may not have the same precedence as src.
+        // Destination may or may not have the same provenance as src.
         let dst = if kani::any() {
-            generator.generate_ptr();
+            generator.generate_ptr()
         } else {
             PointerGenerator::<char, 10>::new().generate_ptr()
         };

library/core/src/ub_checks.rs

@@ -164,9 +164,10 @@ pub(crate) const fn is_nonoverlapping(
 
 pub use predicates::*;
 
-pub trait MetadataPredicates<T> where T: ?Sized {
+/// Trait that allow us to inspect metadata independently on the type `T`.
+pub trait MetadataExt<T, M> where T: core::ptr::Pointee<Metadata=M> + ?Sized {
     /// If the metadata is the length of a slice or str, run the map function.
-    fn map_len<U, F>(metadata: *const Self, map: F) -> Option<U>
+    unsafe fn map_len<U, F>(ptr: *const T, map: F) -> Option<U>
     where
         F: Fn(*const usize) -> U;
 
@@ -176,61 +177,62 @@ pub trait MetadataPredicates<T> where T: ?Sized {
         F: Fn(*const crate::ptr::DynMetadata<T>) -> U;
 }
 
-impl<T> MetadataPredicates<T> for () {
+/// Sized types will have a metadata of type `()`.
+impl<T> MetadataExt<T> for () {
     /// Return None.
-    fn map_len<U, F>(_metadata: *const Self, _map: F) -> Option<U>
+    fn map_len<U, F>(&self, map: F) -> Option<U>
     where
         F: Fn(*const usize) -> U,
     {
         None
     }
 
     /// Return None.
-    fn map_dyn<U, F>(_metadata: *const Self, _map: F) -> Option<U>
+    fn map_dyn<U, F>(&self, map: F) -> Option<U>
     where
         F: Fn(*const crate::ptr::DynMetadata<T>) -> U,
     {
         None
     }
 }
 
-impl<T> MetadataPredicates<T> for usize
-where
-    T: ?Sized
+/// Slices and string slices will have metadata of type `usize`.
+impl<T> MetadataExt<T> for usize
 {
     /// Return the result of the map function.
-    fn map_len<U, F>(metadata: *const Self, map: F) -> Option<U>
+    fn map_len<U, F>(&self, map: F) -> Option<U>
     where
-        F: Fn(*const usize) -> U,
+        F: Fn(usize) -> U,
     {
         Some(map(metadata))
     }
 
     /// This is not a DynMetadata. Return `None`.
-    fn map_dyn<U, F>(_metadata: *const Self, _map: F) -> Option<U>
+    fn map_dyn<U, F>(&self, map: F) -> Option<U>
     where
-        F: Fn(*const crate::ptr::DynMetadata<T>) -> U
+        F: Fn(crate::ptr::DynMetadata<T>) -> U,
     {
         None
     }
 }
 
-impl<T> MetadataPredicates<T> for crate::ptr::DynMetadata<T>
+#[cfg(kani)]
+impl<T> MetadataExt<T> for crate::ptr::DynMetadata<T>
 where
     T: ?Sized
 {
     /// Not a length. Return None.
-    fn map_len<U, F>(_metadata: *const Self, _map: F) -> Option<U>
+    fn map_len<U, F>(&self, map: F) -> Option<U>
     where
-        F: Fn(*const usize) -> U,
+        F: Fn(usize) -> U,
     {
         None
     }
 
     /// Return the result of the map function.
-    fn map_dyn<U, F>(metadata: *const Self, map: F) -> Option<U>
+    fn map_dyn<U, F>(&self, map: F) -> Option<U>
     where
-        F: Fn(*const crate::ptr::DynMetadata<T>) -> U,
+        F: Fn(crate::ptr::DynMetadata<T>) -> U,
     {
         Some(map(metadata))
     }