diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index 07a1ccc00011f..96312ab46a995 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -387,7 +387,9 @@ impl [T] { #[stable(feature = "slice_first_last_chunk", since = "1.77.0")] #[rustc_const_stable(feature = "slice_first_last_chunk", since = "1.77.0")] pub const fn split_first_chunk(&self) -> Option<(&[T; N], &[T])> { - let Some((first, tail)) = self.split_at_checked(N) else { return None }; + let Some((first, tail)) = self.split_at_checked(N) else { + return None; + }; // SAFETY: We explicitly check for the correct number of elements, // and do not let the references outlive the slice. @@ -419,7 +421,9 @@ impl [T] { pub const fn split_first_chunk_mut( &mut self, ) -> Option<(&mut [T; N], &mut [T])> { - let Some((first, tail)) = self.split_at_mut_checked(N) else { return None }; + let Some((first, tail)) = self.split_at_mut_checked(N) else { + return None; + }; // SAFETY: We explicitly check for the correct number of elements, // do not let the reference outlive the slice, @@ -447,7 +451,9 @@ impl [T] { #[stable(feature = "slice_first_last_chunk", since = "1.77.0")] #[rustc_const_stable(feature = "slice_first_last_chunk", since = "1.77.0")] pub const fn split_last_chunk(&self) -> Option<(&[T], &[T; N])> { - let Some(index) = self.len().checked_sub(N) else { return None }; + let Some(index) = self.len().checked_sub(N) else { + return None; + }; let (init, last) = self.split_at(index); // SAFETY: We explicitly check for the correct number of elements, @@ -480,7 +486,9 @@ impl [T] { pub const fn split_last_chunk_mut( &mut self, ) -> Option<(&mut [T], &mut [T; N])> { - let Some(index) = self.len().checked_sub(N) else { return None }; + let Some(index) = self.len().checked_sub(N) else { + return None; + }; let (init, last) = self.split_at_mut(index); // SAFETY: We explicitly check for the correct number of elements, @@ -510,7 +518,9 @@ impl [T] { #[rustc_const_stable(feature = "const_slice_last_chunk", since = "1.80.0")] pub const fn last_chunk(&self) -> Option<&[T; N]> { // FIXME(const-hack): Without const traits, we need this instead of `get`. - let Some(index) = self.len().checked_sub(N) else { return None }; + let Some(index) = self.len().checked_sub(N) else { + return None; + }; let (_, last) = self.split_at(index); // SAFETY: We explicitly check for the correct number of elements, @@ -540,7 +550,9 @@ impl [T] { #[rustc_const_stable(feature = "const_slice_first_last_chunk", since = "1.83.0")] pub const fn last_chunk_mut(&mut self) -> Option<&mut [T; N]> { // FIXME(const-hack): Without const traits, we need this instead of `get`. - let Some(index) = self.len().checked_sub(N) else { return None }; + let Some(index) = self.len().checked_sub(N) else { + return None; + }; let (_, last) = self.split_at_mut(index); // SAFETY: We explicitly check for the correct number of elements, @@ -945,6 +957,7 @@ impl [T] { /// [undefined behavior]: https://doc.rust-lang.org/reference/behavior-considered-undefined.html #[unstable(feature = "slice_swap_unchecked", issue = "88539")] #[track_caller] + #[requires(a < self.len() && b < self.len())] pub const unsafe fn swap_unchecked(&mut self, a: usize, b: usize) { assert_unsafe_precondition!( check_library_ub, @@ -1342,6 +1355,7 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[requires(N != 0 && self.len() % N == 0)] pub const unsafe fn as_chunks_unchecked(&self) -> &[[T; N]] { assert_unsafe_precondition!( check_language_ub, @@ -1502,6 +1516,7 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[requires(N != 0 && self.len() % N == 0)] pub const unsafe fn as_chunks_unchecked_mut(&mut self) -> &mut [[T; N]] { assert_unsafe_precondition!( check_language_ub, @@ -2040,6 +2055,7 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[requires(mid <= self.len())] pub const unsafe fn split_at_unchecked(&self, mid: usize) -> (&[T], &[T]) { // FIXME(const-hack): the const function `from_raw_parts` is used to make this // function const; previously the implementation used @@ -2094,6 +2110,7 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[requires(mid <= self.len())] pub const unsafe fn split_at_mut_unchecked(&mut self, mid: usize) -> (&mut [T], &mut [T]) { let len = self.len(); let ptr = self.as_mut_ptr(); @@ -4645,7 +4662,9 @@ impl [T] { #[rustc_const_unstable(feature = "const_split_off_first_last", issue = "138539")] pub const fn split_off_first<'a>(self: &mut &'a Self) -> Option<&'a T> { // FIXME(const-hack): Use `?` when available in const instead of `let-else`. - let Some((first, rem)) = self.split_first() else { return None }; + let Some((first, rem)) = self.split_first() else { + return None; + }; *self = rem; Some(first) } @@ -4671,7 +4690,9 @@ impl [T] { pub const fn split_off_first_mut<'a>(self: &mut &'a mut Self) -> Option<&'a mut T> { // FIXME(const-hack): Use `mem::take` and `?` when available in const. // Original: `mem::take(self).split_first_mut()?` - let Some((first, rem)) = mem::replace(self, &mut []).split_first_mut() else { return None }; + let Some((first, rem)) = mem::replace(self, &mut []).split_first_mut() else { + return None; + }; *self = rem; Some(first) } @@ -4695,7 +4716,9 @@ impl [T] { #[rustc_const_unstable(feature = "const_split_off_first_last", issue = "138539")] pub const fn split_off_last<'a>(self: &mut &'a Self) -> Option<&'a T> { // FIXME(const-hack): Use `?` when available in const instead of `let-else`. - let Some((last, rem)) = self.split_last() else { return None }; + let Some((last, rem)) = self.split_last() else { + return None; + }; *self = rem; Some(last) } @@ -4721,7 +4744,9 @@ impl [T] { pub const fn split_off_last_mut<'a>(self: &mut &'a mut Self) -> Option<&'a mut T> { // FIXME(const-hack): Use `mem::take` and `?` when available in const. // Original: `mem::take(self).split_last_mut()?` - let Some((last, rem)) = mem::replace(self, &mut []).split_last_mut() else { return None }; + let Some((last, rem)) = mem::replace(self, &mut []).split_last_mut() else { + return None; + }; *self = rem; Some(last) } @@ -5508,4 +5533,353 @@ mod verify { let mut a: [u8; 100] = kani::any(); a.reverse(); } + + // ---- Tier 1: Simple safe wrappers ---- + + #[kani::proof] + fn check_first_chunk() { + let a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array(&a); + let _ = s.first_chunk::<4>(); + } + + #[kani::proof] + fn check_first_chunk_mut() { + let mut a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let _ = s.first_chunk_mut::<4>(); + } + + #[kani::proof] + fn check_split_first_chunk() { + let a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array(&a); + let _ = s.split_first_chunk::<4>(); + } + + #[kani::proof] + fn check_split_first_chunk_mut() { + let mut a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let _ = s.split_first_chunk_mut::<4>(); + } + + #[kani::proof] + fn check_split_last_chunk() { + let a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array(&a); + let _ = s.split_last_chunk::<4>(); + } + + #[kani::proof] + fn check_split_last_chunk_mut() { + let mut a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let _ = s.split_last_chunk_mut::<4>(); + } + + #[kani::proof] + fn check_last_chunk() { + let a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array(&a); + let _ = s.last_chunk::<4>(); + } + + #[kani::proof] + fn check_last_chunk_mut() { + let mut a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let _ = s.last_chunk_mut::<4>(); + } + + #[kani::proof] + fn check_as_chunks() { + let a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array(&a); + let _ = s.as_chunks::<4>(); + } + + #[kani::proof] + fn check_as_chunks_mut() { + let mut a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let _ = s.as_chunks_mut::<4>(); + } + + #[kani::proof] + fn check_as_rchunks() { + let a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array(&a); + let _ = s.as_rchunks::<4>(); + } + + #[kani::proof] + fn check_as_rchunks_mut() { + let mut a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let _ = s.as_rchunks_mut::<4>(); + } + + #[kani::proof] + fn check_as_flattened() { + let a: [[u8; 4]; 25] = kani::any(); + let s = kani::slice::any_slice_of_array(&a); + let _ = s.as_flattened(); + } + + #[kani::proof] + fn check_as_flattened_mut() { + let mut a: [[u8; 4]; 25] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let _ = s.as_flattened_mut(); + } + + // ---- Tier 2: Unsafe functions with contracts ---- + + #[kani::proof] + fn check_swap_unchecked() { + const ARR_SIZE: usize = 100; + let mut a: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let len = s.len(); + let a_idx: usize = kani::any(); + let b_idx: usize = kani::any(); + kani::assume(a_idx < len); + kani::assume(b_idx < len); + unsafe { s.swap_unchecked(a_idx, b_idx) }; + } + + #[kani::proof_for_contract(<[u8]>::as_chunks_unchecked)] + fn check_as_chunks_unchecked() { + const ARR_SIZE: usize = 100; + let a: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array(&a); + kani::assume(s.len() % 4 == 0); + let _ = unsafe { s.as_chunks_unchecked::<4>() }; + } + + #[kani::proof_for_contract(<[u8]>::as_chunks_unchecked_mut)] + fn check_as_chunks_unchecked_mut() { + const ARR_SIZE: usize = 100; + let mut a: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + kani::assume(s.len() % 4 == 0); + let _ = unsafe { s.as_chunks_unchecked_mut::<4>() }; + } + + #[kani::proof_for_contract(<[u8]>::split_at_unchecked)] + fn check_split_at_unchecked() { + const ARR_SIZE: usize = 100; + let a: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array(&a); + let mid: usize = kani::any(); + kani::assume(mid <= s.len()); + let _ = unsafe { s.split_at_unchecked(mid) }; + } + + #[kani::proof_for_contract(<[u8]>::split_at_mut_unchecked)] + fn check_split_at_mut_unchecked() { + const ARR_SIZE: usize = 100; + let mut a: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let mid: usize = kani::any(); + kani::assume(mid <= s.len()); + let _ = unsafe { s.split_at_mut_unchecked(mid) }; + } + + #[kani::proof] + fn check_get_unchecked_usize() { + const ARR_SIZE: usize = 100; + let a: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array(&a); + let idx: usize = kani::any(); + kani::assume(idx < s.len()); + let _ = unsafe { s.get_unchecked(idx) }; + } + + #[kani::proof] + fn check_get_unchecked_mut_usize() { + const ARR_SIZE: usize = 100; + let mut a: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let idx: usize = kani::any(); + kani::assume(idx < s.len()); + let _ = unsafe { s.get_unchecked_mut(idx) }; + } + + #[kani::proof] + fn check_get_unchecked_range() { + const ARR_SIZE: usize = 100; + let a: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array(&a); + let start: usize = kani::any(); + let end: usize = kani::any(); + kani::assume(start <= end); + kani::assume(end <= s.len()); + let _ = unsafe { s.get_unchecked(start..end) }; + } + + #[kani::proof] + fn check_get_unchecked_mut_range() { + const ARR_SIZE: usize = 100; + let mut a: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let start: usize = kani::any(); + let end: usize = kani::any(); + kani::assume(start <= end); + kani::assume(end <= s.len()); + let _ = unsafe { s.get_unchecked_mut(start..end) }; + } + + #[kani::proof] + fn check_get_disjoint_unchecked_mut() { + const ARR_SIZE: usize = 100; + let mut a: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let i: usize = kani::any(); + let j: usize = kani::any(); + kani::assume(i < s.len()); + kani::assume(j < s.len()); + kani::assume(i != j); + let _ = unsafe { s.get_disjoint_unchecked_mut([i, j]) }; + } + + // ---- Tier 3: Safe functions with pointer ops ---- + + #[kani::proof] + fn check_split_at_checked() { + const ARR_SIZE: usize = 100; + let a: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array(&a); + let mid: usize = kani::any(); + let _ = s.split_at_checked(mid); + } + + #[kani::proof] + fn check_split_at_mut_checked() { + const ARR_SIZE: usize = 100; + let mut a: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let mid: usize = kani::any(); + let _ = s.split_at_mut_checked(mid); + } + + #[kani::proof] + fn check_copy_from_slice() { + const ARR_SIZE: usize = 100; + let src_arr: [u8; ARR_SIZE] = kani::any(); + let src = kani::slice::any_slice_of_array(&src_arr); + let mut dst_arr: [u8; ARR_SIZE] = kani::any(); + let dst = kani::slice::any_slice_of_array_mut(&mut dst_arr); + kani::assume(src.len() == dst.len()); + dst.copy_from_slice(src); + } + + #[kani::proof] + #[kani::stub(crate::ptr::swap_nonoverlapping, swap_nonoverlapping_stub)] + fn check_swap_with_slice() { + const ARR_SIZE: usize = 100; + let mut a: [u8; ARR_SIZE] = kani::any(); + let mut b: [u8; ARR_SIZE] = kani::any(); + let s1 = kani::slice::any_slice_of_array_mut(&mut a); + let s2 = kani::slice::any_slice_of_array_mut(&mut b); + kani::assume(s1.len() == s2.len()); + s1.swap_with_slice(s2); + } + + #[kani::proof] + fn check_copy_within() { + const ARR_SIZE: usize = 100; + let mut a: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let len = s.len(); + let start: usize = kani::any(); + let end: usize = kani::any(); + let dest: usize = kani::any(); + kani::assume(start <= end); + kani::assume(end <= len); + let count = end - start; + kani::assume(dest <= len - count); + s.copy_within(start..end, dest); + } + + #[kani::proof] + fn check_get_disjoint_mut() { + const ARR_SIZE: usize = 100; + let mut a: [u8; ARR_SIZE] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let i: usize = kani::any(); + let j: usize = kani::any(); + let _ = s.get_disjoint_mut([i, j]); + } + + #[kani::proof] + fn check_get_disjoint_check_valid() { + const ARR_SIZE: usize = 100; + let len: usize = kani::any(); + kani::assume(len <= ARR_SIZE); + let i: usize = kani::any(); + let j: usize = kani::any(); + let _ = get_disjoint_check_valid(&[i, j], len); + } + + // ---- Tier 4: Complex functions ---- + + // Stub for ptr_rotate that avoids the 256-byte BufType stack allocation + // which makes CBMC intractable. The stub verifies that rotate_left/rotate_right + // correctly compute and pass arguments to ptr_rotate. + unsafe fn ptr_rotate_stub(_left: usize, _mid: *mut T, _right: usize) {} + + unsafe fn swap_nonoverlapping_stub(_x: *mut T, _y: *mut T, _count: usize) {} + + #[kani::proof] + #[kani::stub(rotate::ptr_rotate, ptr_rotate_stub)] + fn check_rotate_left() { + let mut a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let mid: usize = kani::any(); + kani::assume(mid <= s.len()); + s.rotate_left(mid); + } + + #[kani::proof] + #[kani::stub(rotate::ptr_rotate, ptr_rotate_stub)] + fn check_rotate_right() { + let mut a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let k: usize = kani::any(); + kani::assume(k <= s.len()); + s.rotate_right(k); + } + + #[kani::proof] + #[kani::unwind(8)] + fn check_binary_search_by() { + let a: [u8; 7] = kani::any(); + let s = kani::slice::any_slice_of_array(&a); + let target: u8 = kani::any(); + let _ = s.binary_search_by(|x| x.cmp(&target)); + } + + #[kani::proof] + #[kani::unwind(8)] + fn check_partition_dedup_by() { + let mut a: [u8; 7] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let _ = s.partition_dedup_by(|a, b| *a == *b); + } + + #[kani::proof] + fn check_as_simd() { + let a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array(&a); + let _ = s.as_simd::<4>(); + } + + #[kani::proof] + fn check_as_simd_mut() { + let mut a: [u8; 100] = kani::any(); + let s = kani::slice::any_slice_of_array_mut(&mut a); + let _ = s.as_simd_mut::<4>(); + } }