reduced slice sizes to avoid object-bits error

Author: AlexLB99

library/core/src/slice/mod.rs

@@ -4146,45 +4146,6 @@ impl<T> [T] {
         }
     }
 
-    //We need the following wrapper because it is not currently possible to write
-    //contracts for functions that return mut refs to input arguments
-    //see https://github.com/model-checking/kani/issues/3764
-    //----------------------------
-    //Checks if the part that will be transmuted from type T to U is valid for type U
-    //reuses most function logic up to use of from_raw_parts,
-    //where the potentially unsafe transmute occurs
-    #[requires(
-        U::IS_ZST || T::IS_ZST || {
-            let ptr = self.as_ptr();
-            let offset = crate::ptr::align_offset(ptr, align_of::<U>());
-            offset > self.len() || {
-                let (_, rest) = self.split_at(offset);
-                let (us_len, _) = rest.align_to_offsets::<U>();
-                let middle = crate::ptr::slice_from_raw_parts(rest.as_ptr() as *const U, us_len
-);
-                ub_checks::can_dereference(middle)
-            }
-        }
-    )]
-    //The following two ensures clauses guarantee that middle is of maximum size within self
-    #[ensures(|(prefix, _, _): &(*const [T], *const [U], *const [T])| prefix.len() * size_of::<T>() < align_of::<U>())]
-    #[ensures(|(_, _, suffix): &(*const [T], *const [U], *const [T])| suffix.len() * size_of::<T>() < size_of::<U>())]
-    //Either align_to just returns self in the prefix, or the 3 returned slices
-    //should be sequential, contiguous, and have same total length as self
-    #[ensures(|(prefix, middle, suffix): &(*const [T], *const [U], *const [T])|
-        prefix.as_ptr() == self.as_ptr() &&
-        (prefix.len() == self.len() ||  (
-            ((prefix.as_ptr()).add(prefix.len()) as *const u8 == middle.as_ptr() as *const u8)
-&&
-            ((middle.as_ptr()).add(middle.len()) as *const u8 == suffix.as_ptr() as *const u8) &&
-            ((suffix.as_ptr()).add(suffix.len()) == (self.as_ptr()).add(self.len())) )
-        )
-    )]
-    unsafe fn align_to_mut_wrapper<U>(&mut self) -> (*const [T], *const [U], *const [T]) {
-        let (prefix_mut, mid_mut, suffix_mut) = self.align_to_mut::<U>();
-        (prefix_mut as *const [T], mid_mut as *const [U], suffix_mut as *const [T])
-    }
-
     /// Splits a slice into a prefix, a middle of aligned SIMD types, and a suffix.
     ///
     /// This is a safe wrapper around [`slice::align_to`], so inherits the same
@@ -5370,9 +5331,9 @@ mod verify {
 
     macro_rules! proof_of_contract_for_align_to {
         ($harness:ident, $src:ty, $dst:ty) => {
-            #[kani::proof_for_contract(<[$dst]>::align_to)]
+            #[kani::proof_for_contract(<[$src]>::align_to)]
             fn $harness() {
-                const ARR_SIZE: usize = 1000;
+                const ARR_SIZE: usize = 100;
                 let src_arr: [$src; ARR_SIZE] = kani::any();
                 let src_slice = kani::slice::any_slice_of_array(&src_arr);
                 let dst_slice = unsafe { src_slice.align_to::<$dst>() };
@@ -5438,11 +5399,56 @@ mod verify {
     gen_align_to_harnesses!(align_to_from_char, char);
     gen_align_to_harnesses!(align_to_from_unit, ());
 
+    trait wrap_align_to_mut<T> {
+        unsafe fn align_to_mut_wrapper<U>(&mut self) -> (*const [T], *const [U], *const [T]);
+    }
+
+    //We write this as an impl so that we can refer to "self"
+    impl<T> wrap_align_to_mut<T> for [T] {
+		//We need the following wrapper because it is not currently possible to write
+		//contracts for functions that return mut refs to input arguments
+		//see https://github.com/model-checking/kani/issues/3764
+		//----------------------------
+		//Checks if the part that will be transmuted from type T to U is valid for type U
+		//reuses most function logic up to use of from_raw_parts,
+		//where the potentially unsafe transmute occurs
+		#[requires(
+			U::IS_ZST || T::IS_ZST || {
+				let ptr = self.as_ptr();
+				let offset = crate::ptr::align_offset(ptr, align_of::<U>());
+				offset > self.len() || {
+					let (_, rest) = self.split_at(offset);
+					let (us_len, _) = rest.align_to_offsets::<U>();
+					let middle = crate::ptr::slice_from_raw_parts(rest.as_ptr() as *const U, us_len
+	);
+					ub_checks::can_dereference(middle)
+				}
+			}
+		)]
+		//The following two ensures clauses guarantee that middle is of maximum size within self
+		#[ensures(|(prefix, _, _): &(*const [T], *const [U], *const [T])| prefix.len() * size_of::<T>() < align_of::<U>())]
+		#[ensures(|(_, _, suffix): &(*const [T], *const [U], *const [T])| suffix.len() * size_of::<T>() < size_of::<U>())]
+		//Either align_to just returns self in the prefix, or the 3 returned slices
+		//should be sequential, contiguous, and have same total length as self
+		#[ensures(|(prefix, middle, suffix): &(*const [T], *const [U], *const [T])|
+			prefix.as_ptr() == self.as_ptr() &&
+			(prefix.len() == self.len() ||  (
+				((prefix.as_ptr()).add(prefix.len()) as *const u8 == middle.as_ptr() as *const u8) &&
+				((middle.as_ptr()).add(middle.len()) as *const u8 == suffix.as_ptr() as *const u8) &&
+				((suffix.as_ptr()).add(suffix.len()) == (self.as_ptr()).add(self.len())) )
+			)
+		)]
+		unsafe fn align_to_mut_wrapper<U>(&mut self) -> (*const [T], *const [U], *const [T]) {
+            let (prefix_mut, mid_mut, suffix_mut) = self.align_to_mut::<U>();
+            (prefix_mut as *const [T], mid_mut as *const [U], suffix_mut as *const [T])
+        }
+    }
+
     macro_rules! proof_of_contract_for_align_to_mut {
         ($harness:ident, $src:ty, $dst:ty) => {
-            #[kani::proof_for_contract(<[$dst]>::align_to_mut_wrapper)]
+            #[kani::proof_for_contract(<[$src]>::align_to_mut_wrapper)]
             fn $harness() {
-                const ARR_SIZE: usize = 1000;
+                const ARR_SIZE: usize = 100;
                 let mut src_arr: [$src; ARR_SIZE] = kani::any();
                 let src_slice = kani::slice::any_slice_of_array_mut(&mut src_arr);
                 let dst_slice = unsafe { src_slice.align_to_mut_wrapper::<$dst>() };