From 271ad64ebb84517efd5af0f5dbb34f02588efcd1 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 17:35:58 +0530 Subject: [PATCH 1/6] Challenge 17: Kani contracts for slice functions Kani contracts and harnesses for verify-rust-std challenge. Fixes #281 --- library/core/src/slice/ascii.rs | 4 +- library/core/src/slice/cmp.rs | 12 +- library/core/src/slice/index.rs | 143 +++- library/core/src/slice/iter.rs | 289 ++++++-- library/core/src/slice/mod.rs | 625 +++++++++++++++++- library/core/src/slice/rotate.rs | 15 + library/core/src/slice/sort/select.rs | 19 +- library/core/src/slice/sort/shared/mod.rs | 5 +- .../core/src/slice/sort/shared/smallsort.rs | 18 +- library/core/src/slice/sort/stable/drift.rs | 9 +- library/core/src/slice/sort/stable/merge.rs | 6 +- library/core/src/slice/sort/stable/mod.rs | 5 +- .../core/src/slice/sort/stable/quicksort.rs | 15 +- .../core/src/slice/sort/unstable/quicksort.rs | 16 +- 14 files changed, 1068 insertions(+), 113 deletions(-) diff --git a/library/core/src/slice/ascii.rs b/library/core/src/slice/ascii.rs index ae438f2fa5ca6..849d6ef5d3b1c 100644 --- a/library/core/src/slice/ascii.rs +++ b/library/core/src/slice/ascii.rs @@ -143,7 +143,9 @@ impl [u8] { without modifying the original"] #[stable(feature = "inherent_ascii_escape", since = "1.60.0")] pub fn escape_ascii(&self) -> EscapeAscii<'_> { - EscapeAscii { inner: self.iter().flat_map(EscapeByte) } + EscapeAscii { + inner: self.iter().flat_map(EscapeByte), + } } /// Returns a byte slice with leading ASCII whitespace bytes removed. diff --git a/library/core/src/slice/cmp.rs b/library/core/src/slice/cmp.rs index fd1ca23fb79c5..ac5e59b5921fc 100644 --- a/library/core/src/slice/cmp.rs +++ b/library/core/src/slice/cmp.rs @@ -149,7 +149,11 @@ where // The two slices have been checked to have the same size above. unsafe { let size = size_of_val(self); - compare_bytes(self.as_ptr() as *const u8, other.as_ptr() as *const u8, size) == 0 + compare_bytes( + self.as_ptr() as *const u8, + other.as_ptr() as *const u8, + size, + ) == 0 } } } @@ -312,7 +316,11 @@ impl const SliceOrd for A { let diff = left.len() as isize - right.len() as isize; // This comparison gets optimized away (on x86_64 and ARM) because the // subtraction updates flags. - let len = if left.len() < right.len() { left.len() } else { right.len() }; + let len = if left.len() < right.len() { + left.len() + } else { + right.len() + }; let left = left.as_ptr().cast(); let right = right.as_ptr().cast(); // SAFETY: `left` and `right` are references and are thus guaranteed to diff --git a/library/core/src/slice/index.rs b/library/core/src/slice/index.rs index d8ed521f44353..a3a2011d18b74 100644 --- a/library/core/src/slice/index.rs +++ b/library/core/src/slice/index.rs @@ -151,7 +151,10 @@ mod private_slice_index { #[rustc_on_unimplemented( on(T = "str", label = "string indices are ranges of `usize`",), on( - all(any(T = "str", T = "&str", T = "alloc::string::String"), Self = "{integer}"), + all( + any(T = "str", T = "&str", T = "alloc::string::String"), + Self = "{integer}" + ), note = "you can use `.chars().nth()` or `.bytes().nth()`\n\ for more information, see chapter 8 in The Book: \ " @@ -206,6 +209,18 @@ pub const unsafe trait SliceIndex: private_slice_index::Sealed { #[unstable(feature = "slice_index_methods", issue = "none")] #[track_caller] fn index_mut(self, slice: &mut T) -> &mut Self::Output; + + /// Borrowed form of the `get_unchecked` safety condition for Kani contracts. + /// + /// `true` iff `self` is a valid index into a `[T]` of length `len`. + /// Override in every `[T]` impl; the default is deliberately `false` so a + /// missing override cannot make `proof_for_contract` succeed vacuously. + #[cfg(kani)] + #[unstable(feature = "kani", issue = "none")] + fn in_bounds(&self, len: usize) -> bool { + let _ = len; + false + } } /// The methods `index` and `index_mut` panic if the index is out of bounds. @@ -277,6 +292,11 @@ unsafe impl const SliceIndex<[T]> for usize { // N.B., use intrinsic indexing &mut (*slice)[self] } + + #[cfg(kani)] + fn in_bounds(&self, len: usize) -> bool { + *self < len + } } /// Because `IndexRange` guarantees `start <= end`, fewer checks are needed here @@ -299,7 +319,13 @@ unsafe impl const SliceIndex<[T]> for ops::IndexRange { fn get_mut(self, slice: &mut [T]) -> Option<&mut [T]> { if self.end() <= slice.len() { // SAFETY: `self` is checked to be valid and in bounds above. - unsafe { Some(&mut *get_offset_len_mut_noubcheck(slice, self.start(), self.len())) } + unsafe { + Some(&mut *get_offset_len_mut_noubcheck( + slice, + self.start(), + self.len(), + )) + } } else { None } @@ -352,6 +378,11 @@ unsafe impl const SliceIndex<[T]> for ops::IndexRange { slice_index_fail(self.start(), self.end(), slice.len()) } } + + #[cfg(kani)] + fn in_bounds(&self, len: usize) -> bool { + self.end() <= len + } } /// The methods `index` and `index_mut` panic if: @@ -381,7 +412,11 @@ unsafe impl const SliceIndex<[T]> for ops::Range { && self.end <= slice.len() { // SAFETY: `self` is checked to be valid and in bounds above. - unsafe { Some(&mut *get_offset_len_mut_noubcheck(slice, self.start, new_len)) } + unsafe { + Some(&mut *get_offset_len_mut_noubcheck( + slice, self.start, new_len, + )) + } } else { None } @@ -456,6 +491,11 @@ unsafe impl const SliceIndex<[T]> for ops::Range { slice_index_fail(self.start, self.end, slice.len()) } } + + #[cfg(kani)] + fn in_bounds(&self, len: usize) -> bool { + self.start <= self.end && self.end <= len + } } #[unstable(feature = "new_range_api", issue = "125687")] @@ -494,6 +534,11 @@ unsafe impl const SliceIndex<[T]> for range::Range { fn index_mut(self, slice: &mut [T]) -> &mut [T] { ops::Range::from(self).index_mut(slice) } + + #[cfg(kani)] + fn in_bounds(&self, len: usize) -> bool { + self.start <= self.end && self.end <= len + } } /// The methods `index` and `index_mut` panic if the end of the range is out of bounds. @@ -533,6 +578,11 @@ unsafe impl const SliceIndex<[T]> for ops::RangeTo { fn index_mut(self, slice: &mut [T]) -> &mut [T] { (0..self.end).index_mut(slice) } + + #[cfg(kani)] + fn in_bounds(&self, len: usize) -> bool { + self.end <= len + } } /// The methods `index` and `index_mut` panic if the start of the range is out of bounds. @@ -586,6 +636,11 @@ unsafe impl const SliceIndex<[T]> for ops::RangeFrom { &mut *get_offset_len_mut_noubcheck(slice, self.start, new_len) } } + + #[cfg(kani)] + fn in_bounds(&self, len: usize) -> bool { + self.start <= len + } } #[unstable(feature = "new_range_api", issue = "125687")] @@ -624,6 +679,11 @@ unsafe impl const SliceIndex<[T]> for range::RangeFrom { fn index_mut(self, slice: &mut [T]) -> &mut [T] { ops::RangeFrom::from(self).index_mut(slice) } + + #[cfg(kani)] + fn in_bounds(&self, len: usize) -> bool { + self.start <= len + } } #[stable(feature = "slice_get_slice_impls", since = "1.15.0")] @@ -660,6 +720,11 @@ unsafe impl const SliceIndex<[T]> for ops::RangeFull { fn index_mut(self, slice: &mut [T]) -> &mut [T] { slice } + + #[cfg(kani)] + fn in_bounds(&self, _len: usize) -> bool { + true + } } /// The methods `index` and `index_mut` panic if: @@ -673,12 +738,20 @@ unsafe impl const SliceIndex<[T]> for ops::RangeInclusive { #[inline] fn get(self, slice: &[T]) -> Option<&[T]> { - if *self.end() == usize::MAX { None } else { self.into_slice_range().get(slice) } + if *self.end() == usize::MAX { + None + } else { + self.into_slice_range().get(slice) + } } #[inline] fn get_mut(self, slice: &mut [T]) -> Option<&mut [T]> { - if *self.end() == usize::MAX { None } else { self.into_slice_range().get_mut(slice) } + if *self.end() == usize::MAX { + None + } else { + self.into_slice_range().get_mut(slice) + } } #[inline] @@ -695,7 +768,11 @@ unsafe impl const SliceIndex<[T]> for ops::RangeInclusive { #[inline] fn index(self, slice: &[T]) -> &[T] { - let Self { mut start, mut end, exhausted } = self; + let Self { + mut start, + mut end, + exhausted, + } = self; let len = slice.len(); if end < len { end = end + 1; @@ -710,7 +787,11 @@ unsafe impl const SliceIndex<[T]> for ops::RangeInclusive { #[inline] fn index_mut(self, slice: &mut [T]) -> &mut [T] { - let Self { mut start, mut end, exhausted } = self; + let Self { + mut start, + mut end, + exhausted, + } = self; let len = slice.len(); if end < len { end = end + 1; @@ -722,6 +803,21 @@ unsafe impl const SliceIndex<[T]> for ops::RangeInclusive { } slice_index_fail(start, end, slice.len()) } + + #[cfg(kani)] + fn in_bounds(&self, len: usize) -> bool { + // `into_slice_range` does `end + 1`; that add is UB at `usize::MAX`. + if self.end == usize::MAX { + return false; + } + let exclusive_end = self.end + 1; + let start = if self.exhausted { + exclusive_end + } else { + self.start + }; + start <= exclusive_end && exclusive_end <= len + } } #[unstable(feature = "new_range_api", issue = "125687")] @@ -760,6 +856,15 @@ unsafe impl const SliceIndex<[T]> for range::RangeInclusive { fn index_mut(self, slice: &mut [T]) -> &mut [T] { ops::RangeInclusive::from(self).index_mut(slice) } + + #[cfg(kani)] + fn in_bounds(&self, len: usize) -> bool { + if self.last == usize::MAX { + return false; + } + let exclusive_end = self.last + 1; + self.start <= exclusive_end && exclusive_end <= len + } } /// The methods `index` and `index_mut` panic if the end of the range is out of bounds. @@ -799,6 +904,11 @@ unsafe impl const SliceIndex<[T]> for ops::RangeToInclusive { fn index_mut(self, slice: &mut [T]) -> &mut [T] { (0..=self.end).index_mut(slice) } + + #[cfg(kani)] + fn in_bounds(&self, len: usize) -> bool { + self.end < len + } } /// The methods `index` and `index_mut` panic if the end of the range is out of bounds. @@ -838,6 +948,11 @@ unsafe impl const SliceIndex<[T]> for range::RangeToInclusive { fn index_mut(self, slice: &mut [T]) -> &mut [T] { (0..=self.last).index_mut(slice) } + + #[cfg(kani)] + fn in_bounds(&self, len: usize) -> bool { + self.last < len + } } /// Performs bounds checking of a range. @@ -985,7 +1100,11 @@ where ops::Bound::Unbounded => len, }; - if start > end || end > len { None } else { Some(ops::Range { start, end }) } + if start > end || end > len { + None + } else { + Some(ops::Range { start, end }) + } } /// Converts a pair of `ops::Bound`s into `ops::Range` without performing any @@ -1100,4 +1219,12 @@ unsafe impl SliceIndex<[T]> for (ops::Bound, ops::Bound) { fn index_mut(self, slice: &mut [T]) -> &mut Self::Output { into_slice_range(slice.len(), self).index_mut(slice) } + + #[cfg(kani)] + fn in_bounds(&self, len: usize) -> bool { + match into_range(len, *self) { + Some(r) => r.start <= r.end && r.end <= len, + None => false, + } + } } diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index b6de37033cc47..21d935cb73bae 100644 --- a/library/core/src/slice/iter.rs +++ b/library/core/src/slice/iter.rs @@ -103,10 +103,17 @@ impl<'a, T> Iter<'a, T> { let ptr: NonNull = NonNull::from_ref(slice).cast(); // SAFETY: Similar to `IterMut::new`. unsafe { - let end_or_len = - if T::IS_ZST { without_provenance(len) } else { ptr.as_ptr().add(len) }; + let end_or_len = if T::IS_ZST { + without_provenance(len) + } else { + ptr.as_ptr().add(len) + }; - Self { ptr, end_or_len, _marker: PhantomData } + Self { + ptr, + end_or_len, + _marker: PhantomData, + } } } @@ -158,7 +165,11 @@ iterator! {struct Iter -> *const T, &'a T, const, {/* no mut */}, as_ref, { impl Clone for Iter<'_, T> { #[inline] fn clone(&self) -> Self { - Iter { ptr: self.ptr, end_or_len: self.end_or_len, _marker: self._marker } + Iter { + ptr: self.ptr, + end_or_len: self.end_or_len, + _marker: self._marker, + } } } @@ -292,10 +303,17 @@ impl<'a, T> IterMut<'a, T> { // See the `next_unchecked!` and `is_empty!` macros as well as the // `post_inc_start` method for more information. unsafe { - let end_or_len = - if T::IS_ZST { without_provenance_mut(len) } else { ptr.as_ptr().add(len) }; + let end_or_len = if T::IS_ZST { + without_provenance_mut(len) + } else { + ptr.as_ptr().add(len) + }; - Self { ptr, end_or_len, _marker: PhantomData } + Self { + ptr, + end_or_len, + _marker: PhantomData, + } } } @@ -466,7 +484,11 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> Split<'a, T, P> { #[inline] pub(super) fn new(slice: &'a [T], pred: P) -> Self { - Self { v: slice, pred, finished: false } + Self { + v: slice, + pred, + finished: false, + } } /// Returns a slice which contains items not yet handled by split. /// # Example @@ -490,7 +512,10 @@ where P: FnMut(&T) -> bool, { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("Split").field("v", &self.v).field("finished", &self.finished).finish() + f.debug_struct("Split") + .field("v", &self.v) + .field("finished", &self.finished) + .finish() } } @@ -501,7 +526,11 @@ where P: Clone + FnMut(&T) -> bool, { fn clone(&self) -> Self { - Split { v: self.v, pred: self.pred.clone(), finished: self.finished } + Split { + v: self.v, + pred: self.pred.clone(), + finished: self.finished, + } } } @@ -621,7 +650,11 @@ impl<'a, T: 'a, P: FnMut(&T) -> bool> SplitInclusive<'a, T, P> { #[inline] pub(super) fn new(slice: &'a [T], pred: P) -> Self { let finished = slice.is_empty(); - Self { v: slice, pred, finished } + Self { + v: slice, + pred, + finished, + } } } @@ -645,7 +678,11 @@ where P: Clone + FnMut(&T) -> bool, { fn clone(&self) -> Self { - SplitInclusive { v: self.v, pred: self.pred.clone(), finished: self.finished } + SplitInclusive { + v: self.v, + pred: self.pred.clone(), + finished: self.finished, + } } } @@ -662,8 +699,12 @@ where return None; } - let idx = - self.v.iter().position(|x| (self.pred)(x)).map(|idx| idx + 1).unwrap_or(self.v.len()); + let idx = self + .v + .iter() + .position(|x| (self.pred)(x)) + .map(|idx| idx + 1) + .unwrap_or(self.v.len()); if idx == self.v.len() { self.finished = true; } @@ -699,8 +740,16 @@ where // The last index of self.v is already checked and found to match // by the last iteration, so we start searching a new match // one index to the left. - let remainder = if self.v.is_empty() { &[] } else { &self.v[..(self.v.len() - 1)] }; - let idx = remainder.iter().rposition(|x| (self.pred)(x)).map(|idx| idx + 1).unwrap_or(0); + let remainder = if self.v.is_empty() { + &[] + } else { + &self.v[..(self.v.len() - 1)] + }; + let idx = remainder + .iter() + .rposition(|x| (self.pred)(x)) + .map(|idx| idx + 1) + .unwrap_or(0); if idx == 0 { self.finished = true; } @@ -741,7 +790,11 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> SplitMut<'a, T, P> { #[inline] pub(super) fn new(slice: &'a mut [T], pred: P) -> Self { - Self { v: slice, pred, finished: false } + Self { + v: slice, + pred, + finished: false, + } } } @@ -751,7 +804,10 @@ where P: FnMut(&T) -> bool, { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("SplitMut").field("v", &self.v).field("finished", &self.finished).finish() + f.debug_struct("SplitMut") + .field("v", &self.v) + .field("finished", &self.finished) + .finish() } } @@ -871,7 +927,11 @@ impl<'a, T: 'a, P: FnMut(&T) -> bool> SplitInclusiveMut<'a, T, P> { #[inline] pub(super) fn new(slice: &'a mut [T], pred: P) -> Self { let finished = slice.is_empty(); - Self { v: slice, pred, finished } + Self { + v: slice, + pred, + finished, + } } } @@ -995,7 +1055,9 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> RSplit<'a, T, P> { #[inline] pub(super) fn new(slice: &'a [T], pred: P) -> Self { - Self { inner: Split::new(slice, pred) } + Self { + inner: Split::new(slice, pred), + } } } @@ -1019,7 +1081,9 @@ where P: Clone + FnMut(&T) -> bool, { fn clone(&self) -> Self { - RSplit { inner: self.inner.clone() } + RSplit { + inner: self.inner.clone(), + } } } @@ -1092,7 +1156,9 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> RSplitMut<'a, T, P> { #[inline] pub(super) fn new(slice: &'a mut [T], pred: P) -> Self { - Self { inner: SplitMut::new(slice, pred) } + Self { + inner: SplitMut::new(slice, pred), + } } } @@ -1218,7 +1284,9 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> SplitN<'a, T, P> { #[inline] pub(super) fn new(s: Split<'a, T, P>, n: usize) -> Self { - Self { inner: GenericSplitN { iter: s, count: n } } + Self { + inner: GenericSplitN { iter: s, count: n }, + } } } @@ -1228,7 +1296,9 @@ where P: FnMut(&T) -> bool, { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("SplitN").field("inner", &self.inner).finish() + f.debug_struct("SplitN") + .field("inner", &self.inner) + .finish() } } @@ -1262,7 +1332,9 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> RSplitN<'a, T, P> { #[inline] pub(super) fn new(s: RSplit<'a, T, P>, n: usize) -> Self { - Self { inner: GenericSplitN { iter: s, count: n } } + Self { + inner: GenericSplitN { iter: s, count: n }, + } } } @@ -1272,7 +1344,9 @@ where P: FnMut(&T) -> bool, { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("RSplitN").field("inner", &self.inner).finish() + f.debug_struct("RSplitN") + .field("inner", &self.inner) + .finish() } } @@ -1302,7 +1376,9 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> SplitNMut<'a, T, P> { #[inline] pub(super) fn new(s: SplitMut<'a, T, P>, n: usize) -> Self { - Self { inner: GenericSplitN { iter: s, count: n } } + Self { + inner: GenericSplitN { iter: s, count: n }, + } } } @@ -1312,7 +1388,9 @@ where P: FnMut(&T) -> bool, { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("SplitNMut").field("inner", &self.inner).finish() + f.debug_struct("SplitNMut") + .field("inner", &self.inner) + .finish() } } @@ -1343,7 +1421,9 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> RSplitNMut<'a, T, P> { #[inline] pub(super) fn new(s: RSplitMut<'a, T, P>, n: usize) -> Self { - Self { inner: GenericSplitN { iter: s, count: n } } + Self { + inner: GenericSplitN { iter: s, count: n }, + } } } @@ -1353,7 +1433,9 @@ where P: FnMut(&T) -> bool, { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("RSplitNMut").field("inner", &self.inner).finish() + f.debug_struct("RSplitNMut") + .field("inner", &self.inner) + .finish() } } @@ -1398,7 +1480,10 @@ impl<'a, T: 'a> Windows<'a, T> { #[stable(feature = "rust1", since = "1.0.0")] impl Clone for Windows<'_, T> { fn clone(&self) -> Self { - Windows { v: self.v, size: self.size } + Windows { + v: self.v, + size: self.size, + } } } @@ -1545,7 +1630,10 @@ pub struct Chunks<'a, T: 'a> { impl<'a, T: 'a> Chunks<'a, T> { #[inline] pub(super) const fn new(slice: &'a [T], size: usize) -> Self { - Self { v: slice, chunk_size: size } + Self { + v: slice, + chunk_size: size, + } } } @@ -1553,7 +1641,10 @@ impl<'a, T: 'a> Chunks<'a, T> { #[stable(feature = "rust1", since = "1.0.0")] impl Clone for Chunks<'_, T> { fn clone(&self) -> Self { - Chunks { v: self.v, chunk_size: self.chunk_size } + Chunks { + v: self.v, + chunk_size: self.chunk_size, + } } } @@ -1640,7 +1731,11 @@ impl<'a, T> DoubleEndedIterator for Chunks<'a, T> { None } else { let remainder = self.v.len() % self.chunk_size; - let chunksz = if remainder != 0 { remainder } else { self.chunk_size }; + let chunksz = if remainder != 0 { + remainder + } else { + self.chunk_size + }; // SAFETY: split_at_unchecked requires the argument be less than or // equal to the length. This is guaranteed, but subtle: `chunksz` // will always either be `self.v.len() % self.chunk_size`, which @@ -1734,7 +1829,11 @@ pub struct ChunksMut<'a, T: 'a> { impl<'a, T: 'a> ChunksMut<'a, T> { #[inline] pub(super) const fn new(slice: &'a mut [T], size: usize) -> Self { - Self { v: slice, chunk_size: size, _marker: PhantomData } + Self { + v: slice, + chunk_size: size, + _marker: PhantomData, + } } } @@ -1829,7 +1928,11 @@ impl<'a, T> DoubleEndedIterator for ChunksMut<'a, T> { None } else { let remainder = self.v.len() % self.chunk_size; - let sz = if remainder != 0 { remainder } else { self.chunk_size }; + let sz = if remainder != 0 { + remainder + } else { + self.chunk_size + }; let len = self.v.len(); // SAFETY: Similar to `Chunks::next_back` let (head, tail) = unsafe { self.v.split_at_mut_unchecked(len - sz) }; @@ -1925,7 +2028,11 @@ impl<'a, T> ChunksExact<'a, T> { let fst_len = slice.len() - rem; // SAFETY: 0 <= fst_len <= slice.len() by construction above let (fst, snd) = unsafe { slice.split_at_unchecked(fst_len) }; - Self { v: fst, rem: snd, chunk_size } + Self { + v: fst, + rem: snd, + chunk_size, + } } /// Returns the remainder of the original slice that is not going to be @@ -1956,7 +2063,11 @@ impl<'a, T> ChunksExact<'a, T> { #[stable(feature = "chunks_exact", since = "1.31.0")] impl Clone for ChunksExact<'_, T> { fn clone(&self) -> Self { - ChunksExact { v: self.v, rem: self.rem, chunk_size: self.chunk_size } + ChunksExact { + v: self.v, + rem: self.rem, + chunk_size: self.chunk_size, + } } } @@ -2106,7 +2217,12 @@ impl<'a, T> ChunksExactMut<'a, T> { let fst_len = slice.len() - rem; // SAFETY: 0 <= fst_len <= slice.len() by construction above let (fst, snd) = unsafe { slice.split_at_mut_unchecked(fst_len) }; - Self { v: fst, rem: snd, chunk_size, _marker: PhantomData } + Self { + v: fst, + rem: snd, + chunk_size, + _marker: PhantomData, + } } /// Returns the remainder of the original slice that is not going to be @@ -2367,7 +2483,10 @@ pub struct RChunks<'a, T: 'a> { impl<'a, T: 'a> RChunks<'a, T> { #[inline] pub(super) const fn new(slice: &'a [T], size: usize) -> Self { - Self { v: slice, chunk_size: size } + Self { + v: slice, + chunk_size: size, + } } } @@ -2375,7 +2494,10 @@ impl<'a, T: 'a> RChunks<'a, T> { #[stable(feature = "rchunks", since = "1.31.0")] impl Clone for RChunks<'_, T> { fn clone(&self) -> Self { - RChunks { v: self.v, chunk_size: self.chunk_size } + RChunks { + v: self.v, + chunk_size: self.chunk_size, + } } } @@ -2468,7 +2590,11 @@ impl<'a, T> DoubleEndedIterator for RChunks<'a, T> { None } else { let remainder = self.v.len() % self.chunk_size; - let chunksz = if remainder != 0 { remainder } else { self.chunk_size }; + let chunksz = if remainder != 0 { + remainder + } else { + self.chunk_size + }; // SAFETY: similar to Chunks::next_back let (fst, snd) = unsafe { self.v.split_at_unchecked(chunksz) }; self.v = snd; @@ -2548,7 +2674,11 @@ pub struct RChunksMut<'a, T: 'a> { impl<'a, T: 'a> RChunksMut<'a, T> { #[inline] pub(super) const fn new(slice: &'a mut [T], size: usize) -> Self { - Self { v: slice, chunk_size: size, _marker: PhantomData } + Self { + v: slice, + chunk_size: size, + _marker: PhantomData, + } } } @@ -2650,7 +2780,11 @@ impl<'a, T> DoubleEndedIterator for RChunksMut<'a, T> { None } else { let remainder = self.v.len() % self.chunk_size; - let sz = if remainder != 0 { remainder } else { self.chunk_size }; + let sz = if remainder != 0 { + remainder + } else { + self.chunk_size + }; // SAFETY: Similar to `Chunks::next_back` let (head, tail) = unsafe { self.v.split_at_mut_unchecked(sz) }; self.v = tail; @@ -2743,7 +2877,11 @@ impl<'a, T> RChunksExact<'a, T> { let rem = slice.len() % chunk_size; // SAFETY: 0 <= rem <= slice.len() by construction above let (fst, snd) = unsafe { slice.split_at_unchecked(rem) }; - Self { v: snd, rem: fst, chunk_size } + Self { + v: snd, + rem: fst, + chunk_size, + } } /// Returns the remainder of the original slice that is not going to be @@ -2775,7 +2913,11 @@ impl<'a, T> RChunksExact<'a, T> { #[stable(feature = "rchunks", since = "1.31.0")] impl<'a, T> Clone for RChunksExact<'a, T> { fn clone(&self) -> RChunksExact<'a, T> { - RChunksExact { v: self.v, rem: self.rem, chunk_size: self.chunk_size } + RChunksExact { + v: self.v, + rem: self.rem, + chunk_size: self.chunk_size, + } } } @@ -2927,7 +3069,11 @@ impl<'a, T> RChunksExactMut<'a, T> { let rem = slice.len() % chunk_size; // SAFETY: 0 <= rem <= slice.len() by construction above let (fst, snd) = unsafe { slice.split_at_mut_unchecked(rem) }; - Self { v: snd, rem: fst, chunk_size } + Self { + v: snd, + rem: fst, + chunk_size, + } } /// Returns the remainder of the original slice that is not going to be @@ -3121,7 +3267,11 @@ where let mut len = 1; let mut iter = self.slice.windows(2); while let Some([l, r]) = iter.next() { - if (self.predicate)(l, r) { len += 1 } else { break } + if (self.predicate)(l, r) { + len += 1 + } else { + break; + } } let (head, tail) = self.slice.split_at(len); self.slice = tail; @@ -3131,7 +3281,11 @@ where #[inline] fn size_hint(&self) -> (usize, Option) { - if self.slice.is_empty() { (0, Some(0)) } else { (1, Some(self.slice.len())) } + if self.slice.is_empty() { + (0, Some(0)) + } else { + (1, Some(self.slice.len())) + } } #[inline] @@ -3153,7 +3307,11 @@ where let mut len = 1; let mut iter = self.slice.windows(2); while let Some([l, r]) = iter.next_back() { - if (self.predicate)(l, r) { len += 1 } else { break } + if (self.predicate)(l, r) { + len += 1 + } else { + break; + } } let (head, tail) = self.slice.split_at(self.slice.len() - len); self.slice = head; @@ -3168,14 +3326,19 @@ impl<'a, T: 'a, P> FusedIterator for ChunkBy<'a, T, P> where P: FnMut(&T, &T) -> #[stable(feature = "slice_group_by_clone", since = "1.89.0")] impl<'a, T: 'a, P: Clone> Clone for ChunkBy<'a, T, P> { fn clone(&self) -> Self { - Self { slice: self.slice, predicate: self.predicate.clone() } + Self { + slice: self.slice, + predicate: self.predicate.clone(), + } } } #[stable(feature = "slice_group_by", since = "1.77.0")] impl<'a, T: 'a + fmt::Debug, P> fmt::Debug for ChunkBy<'a, T, P> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("ChunkBy").field("slice", &self.slice).finish() + f.debug_struct("ChunkBy") + .field("slice", &self.slice) + .finish() } } @@ -3215,7 +3378,11 @@ where let mut len = 1; let mut iter = self.slice.windows(2); while let Some([l, r]) = iter.next() { - if (self.predicate)(l, r) { len += 1 } else { break } + if (self.predicate)(l, r) { + len += 1 + } else { + break; + } } let slice = mem::take(&mut self.slice); let (head, tail) = slice.split_at_mut(len); @@ -3226,7 +3393,11 @@ where #[inline] fn size_hint(&self) -> (usize, Option) { - if self.slice.is_empty() { (0, Some(0)) } else { (1, Some(self.slice.len())) } + if self.slice.is_empty() { + (0, Some(0)) + } else { + (1, Some(self.slice.len())) + } } #[inline] @@ -3248,7 +3419,11 @@ where let mut len = 1; let mut iter = self.slice.windows(2); while let Some([l, r]) = iter.next_back() { - if (self.predicate)(l, r) { len += 1 } else { break } + if (self.predicate)(l, r) { + len += 1 + } else { + break; + } } let slice = mem::take(&mut self.slice); let (head, tail) = slice.split_at_mut(slice.len() - len); @@ -3264,7 +3439,9 @@ impl<'a, T: 'a, P> FusedIterator for ChunkByMut<'a, T, P> where P: FnMut(&T, &T) #[stable(feature = "slice_group_by", since = "1.77.0")] impl<'a, T: 'a + fmt::Debug, P> fmt::Debug for ChunkByMut<'a, T, P> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("ChunkByMut").field("slice", &self.slice).finish() + f.debug_struct("ChunkByMut") + .field("slice", &self.slice) + .finish() } } diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index 8e19bbdca0cd4..fc636f78d3034 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -6,7 +6,7 @@ #![stable(feature = "rust1", since = "1.0.0")] -use safety::{ensures, requires}; +use safety::{ensures, loop_invariant, requires}; use crate::clone::TrivialClone; use crate::cmp::Ordering::{self, Equal, Greater, Less}; @@ -156,7 +156,11 @@ impl [T] { #[inline] #[must_use] pub const fn first(&self) -> Option<&T> { - if let [first, ..] = self { Some(first) } else { None } + if let [first, ..] = self { + Some(first) + } else { + None + } } /// Returns a mutable reference to the first element of the slice, or `None` if it is empty. @@ -179,7 +183,11 @@ impl [T] { #[inline] #[must_use] pub const fn first_mut(&mut self) -> Option<&mut T> { - if let [first, ..] = self { Some(first) } else { None } + if let [first, ..] = self { + Some(first) + } else { + None + } } /// Returns the first and all the rest of the elements of the slice, or `None` if it is empty. @@ -199,7 +207,11 @@ impl [T] { #[inline] #[must_use] pub const fn split_first(&self) -> Option<(&T, &[T])> { - if let [first, tail @ ..] = self { Some((first, tail)) } else { None } + if let [first, tail @ ..] = self { + Some((first, tail)) + } else { + None + } } /// Returns the first and all the rest of the elements of the slice, or `None` if it is empty. @@ -221,7 +233,11 @@ impl [T] { #[inline] #[must_use] pub const fn split_first_mut(&mut self) -> Option<(&mut T, &mut [T])> { - if let [first, tail @ ..] = self { Some((first, tail)) } else { None } + if let [first, tail @ ..] = self { + Some((first, tail)) + } else { + None + } } /// Returns the last and all the rest of the elements of the slice, or `None` if it is empty. @@ -241,7 +257,11 @@ impl [T] { #[inline] #[must_use] pub const fn split_last(&self) -> Option<(&T, &[T])> { - if let [init @ .., last] = self { Some((last, init)) } else { None } + if let [init @ .., last] = self { + Some((last, init)) + } else { + None + } } /// Returns the last and all the rest of the elements of the slice, or `None` if it is empty. @@ -263,7 +283,11 @@ impl [T] { #[inline] #[must_use] pub const fn split_last_mut(&mut self) -> Option<(&mut T, &mut [T])> { - if let [init @ .., last] = self { Some((last, init)) } else { None } + if let [init @ .., last] = self { + Some((last, init)) + } else { + None + } } /// Returns the last element of the slice, or `None` if it is empty. @@ -282,7 +306,11 @@ impl [T] { #[inline] #[must_use] pub const fn last(&self) -> Option<&T> { - if let [.., last] = self { Some(last) } else { None } + if let [.., last] = self { + Some(last) + } else { + None + } } /// Returns a mutable reference to the last item in the slice, or `None` if it is empty. @@ -305,7 +333,11 @@ impl [T] { #[inline] #[must_use] pub const fn last_mut(&mut self) -> Option<&mut T> { - if let [.., last] = self { Some(last) } else { None } + if let [.., last] = self { + Some(last) + } else { + None + } } /// Returns an array reference to the first `N` items in the slice. @@ -388,7 +420,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. @@ -420,7 +454,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, @@ -448,7 +484,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, @@ -481,7 +519,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, @@ -511,7 +551,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, @@ -541,7 +583,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, @@ -639,6 +683,7 @@ impl [T] { #[must_use] #[track_caller] #[rustc_const_unstable(feature = "const_index", issue = "143775")] + #[requires(index.in_bounds(self.len()))] pub const unsafe fn get_unchecked(&self, index: I) -> &I::Output where I: [const] SliceIndex, @@ -684,6 +729,7 @@ impl [T] { #[must_use] #[track_caller] #[rustc_const_unstable(feature = "const_index", issue = "143775")] + #[requires(index.in_bounds(self.len()))] pub const unsafe fn get_unchecked_mut(&mut self, index: I) -> &mut I::Output where I: [const] SliceIndex, @@ -948,6 +994,8 @@ 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())] + #[cfg_attr(kani, kani::modifies(self))] pub const unsafe fn swap_unchecked(&mut self, a: usize, b: usize) { assert_unsafe_precondition!( check_library_ub, @@ -978,6 +1026,7 @@ impl [T] { #[stable(feature = "rust1", since = "1.0.0")] #[rustc_const_stable(feature = "const_slice_reverse", since = "1.90.0")] #[inline] + #[cfg_attr(kani, kani::modifies(self))] pub const fn reverse(&mut self) { let half_len = self.len() / 2; let Range { start, end } = self.as_mut_ptr_range(); @@ -1345,6 +1394,7 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[requires(N != 0 && self.len().is_multiple_of(N))] pub const unsafe fn as_chunks_unchecked(&self) -> &[[T; N]] { assert_unsafe_precondition!( check_language_ub, @@ -1505,6 +1555,7 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[requires(N != 0 && self.len().is_multiple_of(N))] pub const unsafe fn as_chunks_unchecked_mut(&mut self) -> &mut [[T; N]] { assert_unsafe_precondition!( check_language_ub, @@ -2043,6 +2094,13 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[requires(mid <= self.len())] + #[ensures(|(left, right): &(&[T], &[T])| { + left.len() == mid + && right.len() == self.len() - mid + && left.as_ptr() == self.as_ptr() + && right.as_ptr() == self.as_ptr().wrapping_add(mid) + })] 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 @@ -2058,7 +2116,12 @@ impl [T] { ); // SAFETY: Caller has to check that `0 <= mid <= self.len()` - unsafe { (from_raw_parts(ptr, mid), from_raw_parts(ptr.add(mid), unchecked_sub(len, mid))) } + unsafe { + ( + from_raw_parts(ptr, mid), + from_raw_parts(ptr.add(mid), unchecked_sub(len, mid)), + ) + } } /// Divides one mutable slice into two at an index, without doing bounds checking. @@ -2097,6 +2160,13 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[requires(mid <= self.len())] + #[ensures(|(left, right): &(&mut [T], &mut [T])| { + left.len() == mid + && right.len() == old(self.len()) - mid + && left.as_ptr() == old(self.as_ptr()) + && right.as_ptr() == old(self.as_ptr()).wrapping_add(mid) + })] 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(); @@ -2989,6 +3059,7 @@ impl [T] { // returns Equal. We want the number of loop iterations to depend *only* // on the size of the input slice so that the CPU can reliably predict // the loop count. + #[loop_invariant(size >= 1 && base + size <= self.len())] while size > 1 { let half = size / 2; let mid = base + half; @@ -3595,6 +3666,12 @@ impl [T] { // thus `next_read > next_write - 1` is too. unsafe { // Avoid bounds checks by using raw pointers. + #[loop_invariant( + next_read <= len + && next_write >= 1 + && next_write <= next_read + && next_read >= 1 + )] while next_read < len { let ptr_read = ptr.add(next_read); let prev_ptr_write = ptr.add(next_write - 1); @@ -3676,6 +3753,8 @@ impl [T] { /// ``` #[stable(feature = "slice_rotate", since = "1.26.0")] #[rustc_const_stable(feature = "const_slice_rotate", since = "1.92.0")] + #[requires(mid <= self.len())] + #[cfg_attr(kani, kani::modifies(self))] pub const fn rotate_left(&mut self, mid: usize) { assert!(mid <= self.len()); let k = self.len() - mid; @@ -3722,6 +3801,8 @@ impl [T] { /// ``` #[stable(feature = "slice_rotate", since = "1.26.0")] #[rustc_const_stable(feature = "const_slice_rotate", since = "1.92.0")] + #[requires(k <= self.len())] + #[cfg_attr(kani, kani::modifies(self))] pub const fn rotate_right(&mut self, k: usize) { assert!(k <= self.len()); let mid = self.len() - k; @@ -3898,6 +3979,8 @@ impl [T] { #[stable(feature = "copy_from_slice", since = "1.9.0")] #[rustc_const_stable(feature = "const_copy_from_slice", since = "1.87.0")] #[track_caller] + #[requires(self.len() == src.len())] + #[cfg_attr(kani, kani::modifies(self))] pub const fn copy_from_slice(&mut self, src: &[T]) where T: Copy, @@ -3936,7 +4019,10 @@ impl [T] { where T: Copy, { - let Range { start: src_start, end: src_end } = slice::range(src, ..self.len()); + let Range { + start: src_start, + end: src_end, + } = slice::range(src, ..self.len()); let count = src_end - src_start; assert!(dest <= self.len() - count, "dest is out of bounds"); // SAFETY: the conditions for `ptr::copy` have all been checked above, @@ -4000,8 +4086,13 @@ impl [T] { #[stable(feature = "swap_with_slice", since = "1.27.0")] #[rustc_const_unstable(feature = "const_swap_with_slice", issue = "142204")] #[track_caller] + #[requires(self.len() == other.len())] + #[cfg_attr(kani, kani::modifies(self, other))] pub const fn swap_with_slice(&mut self, other: &mut [T]) { - assert!(self.len() == other.len(), "destination and source slices have different lengths"); + assert!( + self.len() == other.len(), + "destination and source slices have different lengths" + ); // SAFETY: `self` is valid for `self.len()` elements by definition, and `src` was // checked to have the same length. The slices cannot overlap because // mutable references are exclusive. @@ -4504,7 +4595,8 @@ impl [T] { where P: FnMut(&T) -> bool, { - self.binary_search_by(|x| if pred(x) { Less } else { Greater }).unwrap_or_else(|i| i) + self.binary_search_by(|x| if pred(x) { Less } else { Greater }) + .unwrap_or_else(|i| i) } /// Removes the subslice corresponding to the given range @@ -4658,7 +4750,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) } @@ -4684,7 +4778,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) } @@ -4708,7 +4804,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) } @@ -4734,7 +4832,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) } @@ -4788,6 +4888,7 @@ impl [T] { #[stable(feature = "get_many_mut", since = "1.86.0")] #[inline] #[track_caller] + #[requires(get_disjoint_check_valid(&indices, self.len()).is_ok())] pub unsafe fn get_disjoint_unchecked_mut( &mut self, indices: [I; N], @@ -4808,7 +4909,10 @@ impl [T] { unsafe { for i in 0..N { let idx = indices.get_unchecked(i).clone(); - arr_ptr.cast::<&mut I::Output>().add(i).write(&mut *slice.get_unchecked_mut(idx)); + arr_ptr + .cast::<&mut I::Output>() + .add(i) + .write(&mut *slice.get_unchecked_mut(idx)); } arr.assume_init() } @@ -4926,7 +5030,11 @@ impl [T] { let offset = byte_offset / size_of::(); - if offset < self.len() { Some(offset) } else { None } + if offset < self.len() { + Some(offset) + } else { + None + } } /// Returns the range of indices that a subslice points to. @@ -4981,7 +5089,11 @@ impl [T] { let start = byte_start / size_of::(); let end = start.wrapping_add(subslice.len()); - if start <= self.len() && end <= self.len() { Some(start..end) } else { None } + if start <= self.len() && end <= self.len() { + Some(start..end) + } else { + None + } } } @@ -5221,7 +5333,10 @@ where { #[track_caller] default fn spec_clone_from(&mut self, src: &[T]) { - assert!(self.len() == src.len(), "destination and source slices have different lengths"); + assert!( + self.len() == src.len(), + "destination and source slices have different lengths" + ); // NOTE: We need to explicitly slice them to the same length // to make it easier for the optimizer to elide bounds checking. // But since it can't be relied on we also have an explicit specialization for T: Copy. @@ -5264,7 +5379,11 @@ impl const Default for &mut [T] { } } -#[unstable(feature = "slice_pattern", reason = "stopgap trait for slice patterns", issue = "56345")] +#[unstable( + feature = "slice_pattern", + reason = "stopgap trait for slice patterns", + issue = "56345" +)] /// Patterns in slices - currently, only used by `strip_prefix` and `strip_suffix`. At a future /// point, we hope to generalise `core::str::Pattern` (which at the time of writing is limited to /// `str`) to slices, and then this trait will be replaced or abolished. @@ -5470,6 +5589,8 @@ unsafe impl GetDisjointMutIndex for range::RangeInclusive { #[unstable(feature = "kani", issue = "none")] mod verify { use super::*; + use crate::ops::Bound; + use crate::range; //generates proof_of_contract harness for align_to given the T (src) and U (dst) types macro_rules! proof_of_contract_for_align_to { @@ -5551,9 +5672,451 @@ mod verify { gen_align_to_mut_harnesses!(align_to_mut_from_char, char); gen_align_to_mut_harnesses!(align_to_mut_from_unit, ()); - #[kani::proof] + // Challenge 17: remaining functions. Contracts are written over generic `[T]`; + // each harness instantiates a layout. Looping methods use loop contracts so + // the argument is inductive in the length, not an unwind bound. + const CAP: usize = 8; + + fn any_ref(arr: &[T; N]) -> &[T] { + kani::slice::any_slice_of_array(arr) + } + + fn any_mut(arr: &mut [T; N]) -> &mut [T] { + kani::slice::any_slice_of_array_mut(arr) + } + + fn any_bound() -> Bound { + match kani::any::() % 3 { + 0 => Bound::Included(kani::any()), + 1 => Bound::Excluded(kani::any()), + _ => Bound::Unbounded, + } + } + + // --- unsafe functions: proof_for_contract --- + + #[kani::proof_for_contract(<[u8]>::get_unchecked)] + fn check_get_unchecked_usize() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let idx = kani::any::(); + let _ = unsafe { slice.get_unchecked(idx) }; + } + + #[kani::proof_for_contract(<[u8]>::get_unchecked)] + fn check_get_unchecked_range() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let idx = kani::any::()..kani::any::(); + let _ = unsafe { slice.get_unchecked(idx) }; + } + + #[kani::proof_for_contract(<[u8]>::get_unchecked)] + fn check_get_unchecked_range_inclusive() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let start = kani::any::(); + let end = kani::any::(); + let _ = unsafe { slice.get_unchecked(start..=end) }; + } + + #[kani::proof_for_contract(<[u8]>::get_unchecked)] + fn check_get_unchecked_range_from() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let idx = kani::any::()..; + let _ = unsafe { slice.get_unchecked(idx) }; + } + + #[kani::proof_for_contract(<[u8]>::get_unchecked)] + fn check_get_unchecked_range_to() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let idx = ..kani::any::(); + let _ = unsafe { slice.get_unchecked(idx) }; + } + + #[kani::proof_for_contract(<[u8]>::get_unchecked)] + fn check_get_unchecked_range_full() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let _ = unsafe { slice.get_unchecked(..) }; + } + + #[kani::proof_for_contract(<[u8]>::get_unchecked)] + fn check_get_unchecked_range_to_inclusive() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let idx = ..=kani::any::(); + let _ = unsafe { slice.get_unchecked(idx) }; + } + + #[kani::proof_for_contract(<[u8]>::get_unchecked)] + fn check_get_unchecked_index_range() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let start = kani::any::(); + let end = kani::any::(); + kani::assume(start <= end); + let idx = unsafe { crate::ops::IndexRange::new_unchecked(start, end) }; + let _ = unsafe { slice.get_unchecked(idx) }; + } + + #[kani::proof_for_contract(<[u8]>::get_unchecked)] + fn check_get_unchecked_core_range() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let idx = range::Range { + start: kani::any(), + end: kani::any(), + }; + let _ = unsafe { slice.get_unchecked(idx) }; + } + + #[kani::proof_for_contract(<[u8]>::get_unchecked)] + fn check_get_unchecked_core_range_inclusive() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let idx = range::RangeInclusive { + start: kani::any(), + last: kani::any(), + }; + let _ = unsafe { slice.get_unchecked(idx) }; + } + + #[kani::proof_for_contract(<[u8]>::get_unchecked)] + fn check_get_unchecked_core_range_from() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let idx = range::RangeFrom { start: kani::any() }; + let _ = unsafe { slice.get_unchecked(idx) }; + } + + #[kani::proof_for_contract(<[u8]>::get_unchecked)] + fn check_get_unchecked_core_range_to_inclusive() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let idx = range::RangeToInclusive { last: kani::any() }; + let _ = unsafe { slice.get_unchecked(idx) }; + } + + #[kani::proof_for_contract(<[u8]>::get_unchecked)] + fn check_get_unchecked_bound_pair() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let idx = (any_bound(), any_bound()); + let _ = unsafe { slice.get_unchecked(idx) }; + } + + #[kani::proof_for_contract(<[u8]>::get_unchecked_mut)] + fn check_get_unchecked_mut_usize() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + let idx = kani::any::(); + let _ = unsafe { slice.get_unchecked_mut(idx) }; + } + + #[kani::proof_for_contract(<[u8]>::get_unchecked_mut)] + fn check_get_unchecked_mut_range() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + let idx = kani::any::()..kani::any::(); + let _ = unsafe { slice.get_unchecked_mut(idx) }; + } + + #[kani::proof_for_contract(<[u8]>::get_unchecked_mut)] + fn check_get_unchecked_mut_range_inclusive() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + let start = kani::any::(); + let end = kani::any::(); + let _ = unsafe { slice.get_unchecked_mut(start..=end) }; + } + + #[kani::proof_for_contract(<[u8]>::swap_unchecked)] + fn check_swap_unchecked() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + let a = kani::any::(); + let b = kani::any::(); + unsafe { slice.swap_unchecked(a, b) }; + } + + #[kani::proof_for_contract(<[u8]>::as_chunks_unchecked)] + fn check_as_chunks_unchecked() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let _ = unsafe { slice.as_chunks_unchecked::<2>() }; + } + + #[kani::proof_for_contract(<[u8]>::as_chunks_unchecked_mut)] + fn check_as_chunks_unchecked_mut() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + let _ = unsafe { slice.as_chunks_unchecked_mut::<2>() }; + } + + #[kani::proof_for_contract(<[u8]>::split_at_unchecked)] + fn check_split_at_unchecked() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let mid = kani::any::(); + let _ = unsafe { slice.split_at_unchecked(mid) }; + } + + #[kani::proof_for_contract(<[()]>::split_at_unchecked)] + fn check_split_at_unchecked_zst() { + let arr: [(); CAP] = [(); CAP]; + let slice = any_ref(&arr); + let mid = kani::any::(); + let _ = unsafe { slice.split_at_unchecked(mid) }; + } + + #[kani::proof_for_contract(<[u8]>::split_at_mut_unchecked)] + fn check_split_at_mut_unchecked() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + let mid = kani::any::(); + let _ = unsafe { slice.split_at_mut_unchecked(mid) }; + } + + #[kani::proof_for_contract(<[u8]>::get_disjoint_unchecked_mut)] + fn check_get_disjoint_unchecked_mut_usize() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + let indices = [kani::any::(), kani::any::()]; + let _ = unsafe { slice.get_disjoint_unchecked_mut(indices) }; + } + + #[kani::proof_for_contract(<[u8]>::get_disjoint_unchecked_mut)] + fn check_get_disjoint_unchecked_mut_range() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + let indices = [ + kani::any::()..kani::any::(), + kani::any::()..kani::any::(), + ]; + let _ = unsafe { slice.get_disjoint_unchecked_mut(indices) }; + } + + #[kani::proof_for_contract(<[u8]>::get_disjoint_unchecked_mut)] + fn check_get_disjoint_unchecked_mut_range_inclusive() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + let a = kani::any::()..=kani::any::(); + let b = kani::any::()..=kani::any::(); + let _ = unsafe { slice.get_disjoint_unchecked_mut([a, b]) }; + } + + // --- safe abstractions --- + + #[kani::proof_for_contract(<[u8]>::reverse)] fn check_reverse() { - let mut a: [u8; 100] = kani::any(); - a.reverse(); + let mut arr: [u8; CAP] = kani::any(); + any_mut(&mut arr).reverse(); + } + + #[kani::proof] + fn check_first_chunk() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let _ = slice.first_chunk::<0>(); + let _ = slice.first_chunk::<2>(); + let _ = slice.first_chunk::<8>(); + } + + #[kani::proof] + fn check_first_chunk_mut() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + let _ = slice.first_chunk_mut::<2>(); + } + + #[kani::proof] + fn check_split_first_chunk() { + let arr: [u8; CAP] = kani::any(); + let _ = any_ref(&arr).split_first_chunk::<2>(); + } + + #[kani::proof] + fn check_split_first_chunk_mut() { + let mut arr: [u8; CAP] = kani::any(); + let _ = any_mut(&mut arr).split_first_chunk_mut::<2>(); + } + + #[kani::proof] + fn check_split_last_chunk() { + let arr: [u8; CAP] = kani::any(); + let _ = any_ref(&arr).split_last_chunk::<2>(); + } + + #[kani::proof] + fn check_split_last_chunk_mut() { + let mut arr: [u8; CAP] = kani::any(); + let _ = any_mut(&mut arr).split_last_chunk_mut::<2>(); + } + + #[kani::proof] + fn check_last_chunk() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let _ = slice.last_chunk::<0>(); + let _ = slice.last_chunk::<2>(); + } + + #[kani::proof] + fn check_last_chunk_mut() { + let mut arr: [u8; CAP] = kani::any(); + let _ = any_mut(&mut arr).last_chunk_mut::<2>(); + } + + #[kani::proof] + fn check_as_chunks() { + let arr: [u8; CAP] = kani::any(); + let _ = any_ref(&arr).as_chunks::<2>(); + } + + #[kani::proof] + fn check_as_chunks_mut() { + let mut arr: [u8; CAP] = kani::any(); + let _ = any_mut(&mut arr).as_chunks_mut::<2>(); + } + + #[kani::proof] + fn check_as_rchunks() { + let arr: [u8; CAP] = kani::any(); + let _ = any_ref(&arr).as_rchunks::<2>(); + } + + #[kani::proof] + fn check_split_at_checked() { + let arr: [u8; CAP] = kani::any(); + let _ = any_ref(&arr).split_at_checked(kani::any()); + } + + #[kani::proof] + fn check_split_at_mut_checked() { + let mut arr: [u8; CAP] = kani::any(); + let _ = any_mut(&mut arr).split_at_mut_checked(kani::any()); + } + + #[kani::proof] + fn check_binary_search_by() { + let arr: [u8; CAP] = kani::any(); + let slice = any_ref(&arr); + let _ = slice.binary_search_by(|_| match kani::any::() % 3 { + 0 => Equal, + 1 => Less, + _ => Greater, + }); + } + + #[kani::proof] + fn check_partition_dedup_by() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + let _ = slice.partition_dedup_by(|a, b| a == b); + } + + #[kani::proof_for_contract(<[u8]>::rotate_left)] + fn check_rotate_left() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + slice.rotate_left(kani::any()); + } + + #[kani::proof_for_contract(<[u8]>::rotate_right)] + fn check_rotate_right() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + slice.rotate_right(kani::any()); + } + + #[kani::proof_for_contract(super::rotate::ptr_rotate)] + fn check_ptr_rotate() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + let mid = kani::any::(); + kani::assume(mid <= slice.len()); + let k = slice.len() - mid; + let p = slice.as_mut_ptr(); + unsafe { super::rotate::ptr_rotate(mid, p.add(mid), k) }; + } + + #[kani::proof_for_contract(<[u8]>::copy_from_slice)] + fn check_copy_from_slice() { + let mut dst: [u8; CAP] = kani::any(); + let src: [u8; CAP] = kani::any(); + let d = any_mut(&mut dst); + let s = any_ref(&src); + kani::assume(d.len() == s.len()); + d.copy_from_slice(s); + } + + #[kani::proof] + fn check_copy_within() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + let src = kani::any::()..kani::any::(); + let dest = kani::any::(); + if let Some(r) = try_range(src, ..slice.len()) { + let count = r.end - r.start; + if dest <= slice.len() - count { + slice.copy_within(r, dest); + } + } + } + + #[kani::proof_for_contract(<[u8]>::swap_with_slice)] + fn check_swap_with_slice() { + let mut a: [u8; CAP] = kani::any(); + let mut b: [u8; CAP] = kani::any(); + let left = any_mut(&mut a); + let right = any_mut(&mut b); + kani::assume(left.len() == right.len()); + left.swap_with_slice(right); + } + + #[kani::proof] + fn check_as_simd() { + let arr: [u8; 16] = kani::any(); + let _ = any_ref(&arr).as_simd::<4>(); + } + + #[kani::proof] + fn check_as_simd_mut() { + let mut arr: [u8; 16] = kani::any(); + let _ = any_mut(&mut arr).as_simd_mut::<4>(); + } + + #[kani::proof] + fn check_get_disjoint_mut() { + let mut arr: [u8; CAP] = kani::any(); + let slice = any_mut(&mut arr); + let _ = slice.get_disjoint_mut([kani::any::(), kani::any::()]); + } + + #[kani::proof] + fn check_get_disjoint_check_valid() { + let indices = [ + kani::any::(), + kani::any::(), + kani::any::(), + ]; + let _ = get_disjoint_check_valid(&indices, kani::any()); + } + + #[kani::proof] + fn check_as_flattened() { + let arr: [[u8; 2]; 4] = kani::any(); + let slice = any_ref(&arr); + let _ = slice.as_flattened(); + } + + #[kani::proof] + fn check_as_flattened_mut() { + let mut arr: [[u8; 2]; 4] = kani::any(); + let slice = any_mut(&mut arr); + let _ = slice.as_flattened_mut(); } } diff --git a/library/core/src/slice/rotate.rs b/library/core/src/slice/rotate.rs index b3b64422884d5..81c9bc4d97e83 100644 --- a/library/core/src/slice/rotate.rs +++ b/library/core/src/slice/rotate.rs @@ -1,3 +1,7 @@ +use safety::requires; + +#[cfg(kani)] +use crate::kani; use crate::mem::{MaybeUninit, SizedTypeProperties}; use crate::ptr; @@ -11,6 +15,17 @@ type BufType = [usize; 32]; /// /// The specified range must be valid for reading and writing. #[inline] +#[requires( + T::IS_ZST || left == 0 || right == 0 || { + let start = mid.wrapping_sub(left); + crate::ub_checks::can_dereference(ptr::slice_from_raw_parts(start, left + right)) + && crate::ub_checks::can_write(ptr::slice_from_raw_parts_mut(start, left + right)) + } +)] +#[cfg_attr( + kani, + kani::modifies(ptr::slice_from_raw_parts_mut(mid.wrapping_sub(left), left.wrapping_add(right))) +)] pub(super) const unsafe fn ptr_rotate(left: usize, mid: *mut T, right: usize) { if T::IS_ZST { return; diff --git a/library/core/src/slice/sort/select.rs b/library/core/src/slice/sort/select.rs index fc31013caf88c..1b6fc9453d938 100644 --- a/library/core/src/slice/sort/select.rs +++ b/library/core/src/slice/sort/select.rs @@ -26,7 +26,10 @@ where // Puts a lower limit of 1 on `len`. if index >= len { - panic!("partition_at_index index {} greater than length of slice {}", index, len); + panic!( + "partition_at_index index {} greater than length of slice {}", + index, len + ); } if T::IS_ZST { @@ -233,7 +236,19 @@ fn median_of_ninthers bool>(v: &mut [T], is_less: &mut F) let mut a = lo - 4 * frac - gap; let mut b = hi + gap; for i in lo..hi { - ninther(v, is_less, a, i - frac, b, a + 1, i, b + 1, a + 2, i + frac, b + 2); + ninther( + v, + is_less, + a, + i - frac, + b, + a + 1, + i, + b + 1, + a + 2, + i + frac, + b + 2, + ); a += 3; b += 3; } diff --git a/library/core/src/slice/sort/shared/mod.rs b/library/core/src/slice/sort/shared/mod.rs index e2cdcb3dd511d..9f51fccc92f3d 100644 --- a/library/core/src/slice/sort/shared/mod.rs +++ b/library/core/src/slice/sort/shared/mod.rs @@ -1,4 +1,7 @@ -#![cfg_attr(any(feature = "optimize_for_size", target_pointer_width = "16"), allow(dead_code))] +#![cfg_attr( + any(feature = "optimize_for_size", target_pointer_width = "16"), + allow(dead_code) +)] use crate::marker::Freeze; diff --git a/library/core/src/slice/sort/shared/smallsort.rs b/library/core/src/slice/sort/shared/smallsort.rs index e555fce440872..95927e5b351da 100644 --- a/library/core/src/slice/sort/shared/smallsort.rs +++ b/library/core/src/slice/sort/shared/smallsort.rs @@ -267,7 +267,11 @@ fn small_sort_general_with_scratch bool>( // We extend this to desired_len, src is valid for desired_len elements. let src = v_base.add(offset); let dst = scratch_base.add(offset); - let desired_len = if offset == 0 { len_div_2 } else { len - len_div_2 }; + let desired_len = if offset == 0 { + len_div_2 + } else { + len - len_div_2 + }; for i in presorted_len..desired_len { ptr::copy_nonoverlapping(src.add(i), dst.add(i), 1); @@ -276,7 +280,11 @@ fn small_sort_general_with_scratch bool>( } // SAFETY: see comment in `CopyOnDrop::drop`. - let drop_guard = CopyOnDrop { src: scratch_base, dst: v_base, len }; + let drop_guard = CopyOnDrop { + src: scratch_base, + dst: v_base, + len, + }; // SAFETY: at this point scratch_base is fully initialized, allowing us // to use it as the source of our merge back into the original array. @@ -554,7 +562,11 @@ unsafe fn insert_tail bool>(begin: *mut T, tail: *mut T, // the correct insertion position, gap_guard ensures the element is moved // back into the array. let tmp = ManuallyDrop::new(tail.read()); - let mut gap_guard = CopyOnDrop { src: &*tmp, dst: tail, len: 1 }; + let mut gap_guard = CopyOnDrop { + src: &*tmp, + dst: tail, + len: 1, + }; loop { // SAFETY: we move sift into the gap (which is valid), and point the diff --git a/library/core/src/slice/sort/stable/drift.rs b/library/core/src/slice/sort/stable/drift.rs index 1edffe095a89d..29274180b87a8 100644 --- a/library/core/src/slice/sort/stable/drift.rs +++ b/library/core/src/slice/sort/stable/drift.rs @@ -60,8 +60,13 @@ pub fn sort bool>( // with root-level desired depth to fully collapse the merge tree. let (next_run, desired_depth); if scan_idx < len { - next_run = - create_run(&mut v[scan_idx..], scratch, min_good_run_len, eager_sort, is_less); + next_run = create_run( + &mut v[scan_idx..], + scratch, + min_good_run_len, + eager_sort, + is_less, + ); desired_depth = merge_tree_depth( scan_idx - prev_run.len(), scan_idx, diff --git a/library/core/src/slice/sort/stable/merge.rs b/library/core/src/slice/sort/stable/merge.rs index bb2747bfc78ac..e09a5b670e7d0 100644 --- a/library/core/src/slice/sort/stable/merge.rs +++ b/library/core/src/slice/sort/stable/merge.rs @@ -50,7 +50,11 @@ pub fn merge bool>( ptr::copy_nonoverlapping(save_base, buf, save_len); - let mut merge_state = MergeState { start: buf, end: buf.add(save_len), dst: save_base }; + let mut merge_state = MergeState { + start: buf, + end: buf.add(save_len), + dst: save_base, + }; if left_is_shorter { merge_state.merge_up(v_mid, v_end, is_less); diff --git a/library/core/src/slice/sort/stable/mod.rs b/library/core/src/slice/sort/stable/mod.rs index 8b4e5c0c8c3a1..b49d6cb7e46c6 100644 --- a/library/core/src/slice/sort/stable/mod.rs +++ b/library/core/src/slice/sort/stable/mod.rs @@ -153,7 +153,10 @@ struct AlignedStorage { impl AlignedStorage { fn new() -> Self { - Self { _align: [], storage: [const { MaybeUninit::uninit() }; N] } + Self { + _align: [], + storage: [const { MaybeUninit::uninit() }; N], + } } fn as_uninit_slice_mut(&mut self) -> &mut [MaybeUninit] { diff --git a/library/core/src/slice/sort/stable/quicksort.rs b/library/core/src/slice/sort/stable/quicksort.rs index 0439ba870bd2b..ecd069b2d407f 100644 --- a/library/core/src/slice/sort/stable/quicksort.rs +++ b/library/core/src/slice/sort/stable/quicksort.rs @@ -197,7 +197,14 @@ impl PartitionState { /// scan buffer must be initialized. unsafe fn new(scan: *const T, scratch: *mut T, len: usize) -> Self { // SAFETY: See function safety comment. - unsafe { Self { scratch_base: scratch, scan, num_left: 0, scratch_rev: scratch.add(len) } } + unsafe { + Self { + scratch_base: scratch, + scan, + num_left: 0, + scratch_rev: scratch.add(len), + } + } } /// Depending on the value of `towards_left` this function will write a value @@ -220,7 +227,11 @@ impl PartitionState { // SAFETY: now we have scratch_rev == base + len - (i + 1). This means // scratch_rev + num_left == base + len - 1 - num_right < base + len. - let dst_base = if towards_left { self.scratch_base } else { self.scratch_rev }; + let dst_base = if towards_left { + self.scratch_base + } else { + self.scratch_rev + }; let dst = dst_base.add(self.num_left); ptr::copy_nonoverlapping(self.scan, dst, 1); diff --git a/library/core/src/slice/sort/unstable/quicksort.rs b/library/core/src/slice/sort/unstable/quicksort.rs index bdf56a8080305..f274f623cd9fe 100644 --- a/library/core/src/slice/sort/unstable/quicksort.rs +++ b/library/core/src/slice/sort/unstable/quicksort.rs @@ -211,7 +211,10 @@ where let is_first_swap_pair = gap_opt.is_none(); if is_first_swap_pair { - gap_opt = Some(GapGuard { pos: right, value: ManuallyDrop::new(ptr::read(left)) }); + gap_opt = Some(GapGuard { + pos: right, + value: ManuallyDrop::new(ptr::read(left)), + }); } let gap = gap_opt.as_mut().unwrap_unchecked(); @@ -301,7 +304,10 @@ where num_lt: 0, right: v_base.add(1), - gap: GapGuardRaw { pos: v_base, value: &mut *gap_value }, + gap: GapGuardRaw { + pos: v_base, + value: &mut *gap_value, + }, }; // Manual unrolling that works well on x86, Arm and with opt-level=s without murdering @@ -323,7 +329,11 @@ where let end = v_base.add(len); loop { let is_done = state.right == end; - state.right = if is_done { state.gap.value } else { state.right }; + state.right = if is_done { + state.gap.value + } else { + state.right + }; loop_body(&mut state); From 4d3945d914c4ce09e925d9a50cc32742be947306 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 18:06:39 +0530 Subject: [PATCH 2/6] Challenge 17: rustfmt slice modules Apply rust-lang rustfmt (use_small_heuristics = Max) to the slice files from this challenge so upstream_test format passes. --- library/core/src/slice/ascii.rs | 4 +- library/core/src/slice/cmp.rs | 12 +- library/core/src/slice/index.rs | 55 +--- library/core/src/slice/iter.rs | 265 ++++-------------- library/core/src/slice/mod.rs | 112 ++------ library/core/src/slice/sort/select.rs | 19 +- library/core/src/slice/sort/shared/mod.rs | 5 +- .../core/src/slice/sort/shared/smallsort.rs | 18 +- library/core/src/slice/sort/stable/drift.rs | 9 +- library/core/src/slice/sort/stable/merge.rs | 6 +- library/core/src/slice/sort/stable/mod.rs | 5 +- .../core/src/slice/sort/stable/quicksort.rs | 15 +- .../core/src/slice/sort/unstable/quicksort.rs | 16 +- 13 files changed, 99 insertions(+), 442 deletions(-) diff --git a/library/core/src/slice/ascii.rs b/library/core/src/slice/ascii.rs index 849d6ef5d3b1c..ae438f2fa5ca6 100644 --- a/library/core/src/slice/ascii.rs +++ b/library/core/src/slice/ascii.rs @@ -143,9 +143,7 @@ impl [u8] { without modifying the original"] #[stable(feature = "inherent_ascii_escape", since = "1.60.0")] pub fn escape_ascii(&self) -> EscapeAscii<'_> { - EscapeAscii { - inner: self.iter().flat_map(EscapeByte), - } + EscapeAscii { inner: self.iter().flat_map(EscapeByte) } } /// Returns a byte slice with leading ASCII whitespace bytes removed. diff --git a/library/core/src/slice/cmp.rs b/library/core/src/slice/cmp.rs index ac5e59b5921fc..fd1ca23fb79c5 100644 --- a/library/core/src/slice/cmp.rs +++ b/library/core/src/slice/cmp.rs @@ -149,11 +149,7 @@ where // The two slices have been checked to have the same size above. unsafe { let size = size_of_val(self); - compare_bytes( - self.as_ptr() as *const u8, - other.as_ptr() as *const u8, - size, - ) == 0 + compare_bytes(self.as_ptr() as *const u8, other.as_ptr() as *const u8, size) == 0 } } } @@ -316,11 +312,7 @@ impl const SliceOrd for A { let diff = left.len() as isize - right.len() as isize; // This comparison gets optimized away (on x86_64 and ARM) because the // subtraction updates flags. - let len = if left.len() < right.len() { - left.len() - } else { - right.len() - }; + let len = if left.len() < right.len() { left.len() } else { right.len() }; let left = left.as_ptr().cast(); let right = right.as_ptr().cast(); // SAFETY: `left` and `right` are references and are thus guaranteed to diff --git a/library/core/src/slice/index.rs b/library/core/src/slice/index.rs index a3a2011d18b74..e13ddb24dd167 100644 --- a/library/core/src/slice/index.rs +++ b/library/core/src/slice/index.rs @@ -151,10 +151,7 @@ mod private_slice_index { #[rustc_on_unimplemented( on(T = "str", label = "string indices are ranges of `usize`",), on( - all( - any(T = "str", T = "&str", T = "alloc::string::String"), - Self = "{integer}" - ), + all(any(T = "str", T = "&str", T = "alloc::string::String"), Self = "{integer}"), note = "you can use `.chars().nth()` or `.bytes().nth()`\n\ for more information, see chapter 8 in The Book: \ " @@ -319,13 +316,7 @@ unsafe impl const SliceIndex<[T]> for ops::IndexRange { fn get_mut(self, slice: &mut [T]) -> Option<&mut [T]> { if self.end() <= slice.len() { // SAFETY: `self` is checked to be valid and in bounds above. - unsafe { - Some(&mut *get_offset_len_mut_noubcheck( - slice, - self.start(), - self.len(), - )) - } + unsafe { Some(&mut *get_offset_len_mut_noubcheck(slice, self.start(), self.len())) } } else { None } @@ -412,11 +403,7 @@ unsafe impl const SliceIndex<[T]> for ops::Range { && self.end <= slice.len() { // SAFETY: `self` is checked to be valid and in bounds above. - unsafe { - Some(&mut *get_offset_len_mut_noubcheck( - slice, self.start, new_len, - )) - } + unsafe { Some(&mut *get_offset_len_mut_noubcheck(slice, self.start, new_len)) } } else { None } @@ -738,20 +725,12 @@ unsafe impl const SliceIndex<[T]> for ops::RangeInclusive { #[inline] fn get(self, slice: &[T]) -> Option<&[T]> { - if *self.end() == usize::MAX { - None - } else { - self.into_slice_range().get(slice) - } + if *self.end() == usize::MAX { None } else { self.into_slice_range().get(slice) } } #[inline] fn get_mut(self, slice: &mut [T]) -> Option<&mut [T]> { - if *self.end() == usize::MAX { - None - } else { - self.into_slice_range().get_mut(slice) - } + if *self.end() == usize::MAX { None } else { self.into_slice_range().get_mut(slice) } } #[inline] @@ -768,11 +747,7 @@ unsafe impl const SliceIndex<[T]> for ops::RangeInclusive { #[inline] fn index(self, slice: &[T]) -> &[T] { - let Self { - mut start, - mut end, - exhausted, - } = self; + let Self { mut start, mut end, exhausted } = self; let len = slice.len(); if end < len { end = end + 1; @@ -787,11 +762,7 @@ unsafe impl const SliceIndex<[T]> for ops::RangeInclusive { #[inline] fn index_mut(self, slice: &mut [T]) -> &mut [T] { - let Self { - mut start, - mut end, - exhausted, - } = self; + let Self { mut start, mut end, exhausted } = self; let len = slice.len(); if end < len { end = end + 1; @@ -811,11 +782,7 @@ unsafe impl const SliceIndex<[T]> for ops::RangeInclusive { return false; } let exclusive_end = self.end + 1; - let start = if self.exhausted { - exclusive_end - } else { - self.start - }; + let start = if self.exhausted { exclusive_end } else { self.start }; start <= exclusive_end && exclusive_end <= len } } @@ -1100,11 +1067,7 @@ where ops::Bound::Unbounded => len, }; - if start > end || end > len { - None - } else { - Some(ops::Range { start, end }) - } + if start > end || end > len { None } else { Some(ops::Range { start, end }) } } /// Converts a pair of `ops::Bound`s into `ops::Range` without performing any diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index 21d935cb73bae..d56e50c092792 100644 --- a/library/core/src/slice/iter.rs +++ b/library/core/src/slice/iter.rs @@ -103,17 +103,10 @@ impl<'a, T> Iter<'a, T> { let ptr: NonNull = NonNull::from_ref(slice).cast(); // SAFETY: Similar to `IterMut::new`. unsafe { - let end_or_len = if T::IS_ZST { - without_provenance(len) - } else { - ptr.as_ptr().add(len) - }; + let end_or_len = + if T::IS_ZST { without_provenance(len) } else { ptr.as_ptr().add(len) }; - Self { - ptr, - end_or_len, - _marker: PhantomData, - } + Self { ptr, end_or_len, _marker: PhantomData } } } @@ -165,11 +158,7 @@ iterator! {struct Iter -> *const T, &'a T, const, {/* no mut */}, as_ref, { impl Clone for Iter<'_, T> { #[inline] fn clone(&self) -> Self { - Iter { - ptr: self.ptr, - end_or_len: self.end_or_len, - _marker: self._marker, - } + Iter { ptr: self.ptr, end_or_len: self.end_or_len, _marker: self._marker } } } @@ -303,17 +292,10 @@ impl<'a, T> IterMut<'a, T> { // See the `next_unchecked!` and `is_empty!` macros as well as the // `post_inc_start` method for more information. unsafe { - let end_or_len = if T::IS_ZST { - without_provenance_mut(len) - } else { - ptr.as_ptr().add(len) - }; + let end_or_len = + if T::IS_ZST { without_provenance_mut(len) } else { ptr.as_ptr().add(len) }; - Self { - ptr, - end_or_len, - _marker: PhantomData, - } + Self { ptr, end_or_len, _marker: PhantomData } } } @@ -484,11 +466,7 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> Split<'a, T, P> { #[inline] pub(super) fn new(slice: &'a [T], pred: P) -> Self { - Self { - v: slice, - pred, - finished: false, - } + Self { v: slice, pred, finished: false } } /// Returns a slice which contains items not yet handled by split. /// # Example @@ -512,10 +490,7 @@ where P: FnMut(&T) -> bool, { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("Split") - .field("v", &self.v) - .field("finished", &self.finished) - .finish() + f.debug_struct("Split").field("v", &self.v).field("finished", &self.finished).finish() } } @@ -526,11 +501,7 @@ where P: Clone + FnMut(&T) -> bool, { fn clone(&self) -> Self { - Split { - v: self.v, - pred: self.pred.clone(), - finished: self.finished, - } + Split { v: self.v, pred: self.pred.clone(), finished: self.finished } } } @@ -650,11 +621,7 @@ impl<'a, T: 'a, P: FnMut(&T) -> bool> SplitInclusive<'a, T, P> { #[inline] pub(super) fn new(slice: &'a [T], pred: P) -> Self { let finished = slice.is_empty(); - Self { - v: slice, - pred, - finished, - } + Self { v: slice, pred, finished } } } @@ -678,11 +645,7 @@ where P: Clone + FnMut(&T) -> bool, { fn clone(&self) -> Self { - SplitInclusive { - v: self.v, - pred: self.pred.clone(), - finished: self.finished, - } + SplitInclusive { v: self.v, pred: self.pred.clone(), finished: self.finished } } } @@ -699,12 +662,8 @@ where return None; } - let idx = self - .v - .iter() - .position(|x| (self.pred)(x)) - .map(|idx| idx + 1) - .unwrap_or(self.v.len()); + let idx = + self.v.iter().position(|x| (self.pred)(x)).map(|idx| idx + 1).unwrap_or(self.v.len()); if idx == self.v.len() { self.finished = true; } @@ -740,16 +699,8 @@ where // The last index of self.v is already checked and found to match // by the last iteration, so we start searching a new match // one index to the left. - let remainder = if self.v.is_empty() { - &[] - } else { - &self.v[..(self.v.len() - 1)] - }; - let idx = remainder - .iter() - .rposition(|x| (self.pred)(x)) - .map(|idx| idx + 1) - .unwrap_or(0); + let remainder = if self.v.is_empty() { &[] } else { &self.v[..(self.v.len() - 1)] }; + let idx = remainder.iter().rposition(|x| (self.pred)(x)).map(|idx| idx + 1).unwrap_or(0); if idx == 0 { self.finished = true; } @@ -790,11 +741,7 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> SplitMut<'a, T, P> { #[inline] pub(super) fn new(slice: &'a mut [T], pred: P) -> Self { - Self { - v: slice, - pred, - finished: false, - } + Self { v: slice, pred, finished: false } } } @@ -804,10 +751,7 @@ where P: FnMut(&T) -> bool, { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("SplitMut") - .field("v", &self.v) - .field("finished", &self.finished) - .finish() + f.debug_struct("SplitMut").field("v", &self.v).field("finished", &self.finished).finish() } } @@ -927,11 +871,7 @@ impl<'a, T: 'a, P: FnMut(&T) -> bool> SplitInclusiveMut<'a, T, P> { #[inline] pub(super) fn new(slice: &'a mut [T], pred: P) -> Self { let finished = slice.is_empty(); - Self { - v: slice, - pred, - finished, - } + Self { v: slice, pred, finished } } } @@ -1055,9 +995,7 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> RSplit<'a, T, P> { #[inline] pub(super) fn new(slice: &'a [T], pred: P) -> Self { - Self { - inner: Split::new(slice, pred), - } + Self { inner: Split::new(slice, pred) } } } @@ -1081,9 +1019,7 @@ where P: Clone + FnMut(&T) -> bool, { fn clone(&self) -> Self { - RSplit { - inner: self.inner.clone(), - } + RSplit { inner: self.inner.clone() } } } @@ -1156,9 +1092,7 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> RSplitMut<'a, T, P> { #[inline] pub(super) fn new(slice: &'a mut [T], pred: P) -> Self { - Self { - inner: SplitMut::new(slice, pred), - } + Self { inner: SplitMut::new(slice, pred) } } } @@ -1284,9 +1218,7 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> SplitN<'a, T, P> { #[inline] pub(super) fn new(s: Split<'a, T, P>, n: usize) -> Self { - Self { - inner: GenericSplitN { iter: s, count: n }, - } + Self { inner: GenericSplitN { iter: s, count: n } } } } @@ -1296,9 +1228,7 @@ where P: FnMut(&T) -> bool, { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("SplitN") - .field("inner", &self.inner) - .finish() + f.debug_struct("SplitN").field("inner", &self.inner).finish() } } @@ -1332,9 +1262,7 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> RSplitN<'a, T, P> { #[inline] pub(super) fn new(s: RSplit<'a, T, P>, n: usize) -> Self { - Self { - inner: GenericSplitN { iter: s, count: n }, - } + Self { inner: GenericSplitN { iter: s, count: n } } } } @@ -1344,9 +1272,7 @@ where P: FnMut(&T) -> bool, { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("RSplitN") - .field("inner", &self.inner) - .finish() + f.debug_struct("RSplitN").field("inner", &self.inner).finish() } } @@ -1376,9 +1302,7 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> SplitNMut<'a, T, P> { #[inline] pub(super) fn new(s: SplitMut<'a, T, P>, n: usize) -> Self { - Self { - inner: GenericSplitN { iter: s, count: n }, - } + Self { inner: GenericSplitN { iter: s, count: n } } } } @@ -1388,9 +1312,7 @@ where P: FnMut(&T) -> bool, { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("SplitNMut") - .field("inner", &self.inner) - .finish() + f.debug_struct("SplitNMut").field("inner", &self.inner).finish() } } @@ -1421,9 +1343,7 @@ where impl<'a, T: 'a, P: FnMut(&T) -> bool> RSplitNMut<'a, T, P> { #[inline] pub(super) fn new(s: RSplitMut<'a, T, P>, n: usize) -> Self { - Self { - inner: GenericSplitN { iter: s, count: n }, - } + Self { inner: GenericSplitN { iter: s, count: n } } } } @@ -1433,9 +1353,7 @@ where P: FnMut(&T) -> bool, { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("RSplitNMut") - .field("inner", &self.inner) - .finish() + f.debug_struct("RSplitNMut").field("inner", &self.inner).finish() } } @@ -1480,10 +1398,7 @@ impl<'a, T: 'a> Windows<'a, T> { #[stable(feature = "rust1", since = "1.0.0")] impl Clone for Windows<'_, T> { fn clone(&self) -> Self { - Windows { - v: self.v, - size: self.size, - } + Windows { v: self.v, size: self.size } } } @@ -1630,10 +1545,7 @@ pub struct Chunks<'a, T: 'a> { impl<'a, T: 'a> Chunks<'a, T> { #[inline] pub(super) const fn new(slice: &'a [T], size: usize) -> Self { - Self { - v: slice, - chunk_size: size, - } + Self { v: slice, chunk_size: size } } } @@ -1641,10 +1553,7 @@ impl<'a, T: 'a> Chunks<'a, T> { #[stable(feature = "rust1", since = "1.0.0")] impl Clone for Chunks<'_, T> { fn clone(&self) -> Self { - Chunks { - v: self.v, - chunk_size: self.chunk_size, - } + Chunks { v: self.v, chunk_size: self.chunk_size } } } @@ -1731,11 +1640,7 @@ impl<'a, T> DoubleEndedIterator for Chunks<'a, T> { None } else { let remainder = self.v.len() % self.chunk_size; - let chunksz = if remainder != 0 { - remainder - } else { - self.chunk_size - }; + let chunksz = if remainder != 0 { remainder } else { self.chunk_size }; // SAFETY: split_at_unchecked requires the argument be less than or // equal to the length. This is guaranteed, but subtle: `chunksz` // will always either be `self.v.len() % self.chunk_size`, which @@ -1829,11 +1734,7 @@ pub struct ChunksMut<'a, T: 'a> { impl<'a, T: 'a> ChunksMut<'a, T> { #[inline] pub(super) const fn new(slice: &'a mut [T], size: usize) -> Self { - Self { - v: slice, - chunk_size: size, - _marker: PhantomData, - } + Self { v: slice, chunk_size: size, _marker: PhantomData } } } @@ -1928,11 +1829,7 @@ impl<'a, T> DoubleEndedIterator for ChunksMut<'a, T> { None } else { let remainder = self.v.len() % self.chunk_size; - let sz = if remainder != 0 { - remainder - } else { - self.chunk_size - }; + let sz = if remainder != 0 { remainder } else { self.chunk_size }; let len = self.v.len(); // SAFETY: Similar to `Chunks::next_back` let (head, tail) = unsafe { self.v.split_at_mut_unchecked(len - sz) }; @@ -2028,11 +1925,7 @@ impl<'a, T> ChunksExact<'a, T> { let fst_len = slice.len() - rem; // SAFETY: 0 <= fst_len <= slice.len() by construction above let (fst, snd) = unsafe { slice.split_at_unchecked(fst_len) }; - Self { - v: fst, - rem: snd, - chunk_size, - } + Self { v: fst, rem: snd, chunk_size } } /// Returns the remainder of the original slice that is not going to be @@ -2063,11 +1956,7 @@ impl<'a, T> ChunksExact<'a, T> { #[stable(feature = "chunks_exact", since = "1.31.0")] impl Clone for ChunksExact<'_, T> { fn clone(&self) -> Self { - ChunksExact { - v: self.v, - rem: self.rem, - chunk_size: self.chunk_size, - } + ChunksExact { v: self.v, rem: self.rem, chunk_size: self.chunk_size } } } @@ -2217,12 +2106,7 @@ impl<'a, T> ChunksExactMut<'a, T> { let fst_len = slice.len() - rem; // SAFETY: 0 <= fst_len <= slice.len() by construction above let (fst, snd) = unsafe { slice.split_at_mut_unchecked(fst_len) }; - Self { - v: fst, - rem: snd, - chunk_size, - _marker: PhantomData, - } + Self { v: fst, rem: snd, chunk_size, _marker: PhantomData } } /// Returns the remainder of the original slice that is not going to be @@ -2483,10 +2367,7 @@ pub struct RChunks<'a, T: 'a> { impl<'a, T: 'a> RChunks<'a, T> { #[inline] pub(super) const fn new(slice: &'a [T], size: usize) -> Self { - Self { - v: slice, - chunk_size: size, - } + Self { v: slice, chunk_size: size } } } @@ -2494,10 +2375,7 @@ impl<'a, T: 'a> RChunks<'a, T> { #[stable(feature = "rchunks", since = "1.31.0")] impl Clone for RChunks<'_, T> { fn clone(&self) -> Self { - RChunks { - v: self.v, - chunk_size: self.chunk_size, - } + RChunks { v: self.v, chunk_size: self.chunk_size } } } @@ -2590,11 +2468,7 @@ impl<'a, T> DoubleEndedIterator for RChunks<'a, T> { None } else { let remainder = self.v.len() % self.chunk_size; - let chunksz = if remainder != 0 { - remainder - } else { - self.chunk_size - }; + let chunksz = if remainder != 0 { remainder } else { self.chunk_size }; // SAFETY: similar to Chunks::next_back let (fst, snd) = unsafe { self.v.split_at_unchecked(chunksz) }; self.v = snd; @@ -2674,11 +2548,7 @@ pub struct RChunksMut<'a, T: 'a> { impl<'a, T: 'a> RChunksMut<'a, T> { #[inline] pub(super) const fn new(slice: &'a mut [T], size: usize) -> Self { - Self { - v: slice, - chunk_size: size, - _marker: PhantomData, - } + Self { v: slice, chunk_size: size, _marker: PhantomData } } } @@ -2780,11 +2650,7 @@ impl<'a, T> DoubleEndedIterator for RChunksMut<'a, T> { None } else { let remainder = self.v.len() % self.chunk_size; - let sz = if remainder != 0 { - remainder - } else { - self.chunk_size - }; + let sz = if remainder != 0 { remainder } else { self.chunk_size }; // SAFETY: Similar to `Chunks::next_back` let (head, tail) = unsafe { self.v.split_at_mut_unchecked(sz) }; self.v = tail; @@ -2877,11 +2743,7 @@ impl<'a, T> RChunksExact<'a, T> { let rem = slice.len() % chunk_size; // SAFETY: 0 <= rem <= slice.len() by construction above let (fst, snd) = unsafe { slice.split_at_unchecked(rem) }; - Self { - v: snd, - rem: fst, - chunk_size, - } + Self { v: snd, rem: fst, chunk_size } } /// Returns the remainder of the original slice that is not going to be @@ -2913,11 +2775,7 @@ impl<'a, T> RChunksExact<'a, T> { #[stable(feature = "rchunks", since = "1.31.0")] impl<'a, T> Clone for RChunksExact<'a, T> { fn clone(&self) -> RChunksExact<'a, T> { - RChunksExact { - v: self.v, - rem: self.rem, - chunk_size: self.chunk_size, - } + RChunksExact { v: self.v, rem: self.rem, chunk_size: self.chunk_size } } } @@ -3069,11 +2927,7 @@ impl<'a, T> RChunksExactMut<'a, T> { let rem = slice.len() % chunk_size; // SAFETY: 0 <= rem <= slice.len() by construction above let (fst, snd) = unsafe { slice.split_at_mut_unchecked(rem) }; - Self { - v: snd, - rem: fst, - chunk_size, - } + Self { v: snd, rem: fst, chunk_size } } /// Returns the remainder of the original slice that is not going to be @@ -3281,11 +3135,7 @@ where #[inline] fn size_hint(&self) -> (usize, Option) { - if self.slice.is_empty() { - (0, Some(0)) - } else { - (1, Some(self.slice.len())) - } + if self.slice.is_empty() { (0, Some(0)) } else { (1, Some(self.slice.len())) } } #[inline] @@ -3326,19 +3176,14 @@ impl<'a, T: 'a, P> FusedIterator for ChunkBy<'a, T, P> where P: FnMut(&T, &T) -> #[stable(feature = "slice_group_by_clone", since = "1.89.0")] impl<'a, T: 'a, P: Clone> Clone for ChunkBy<'a, T, P> { fn clone(&self) -> Self { - Self { - slice: self.slice, - predicate: self.predicate.clone(), - } + Self { slice: self.slice, predicate: self.predicate.clone() } } } #[stable(feature = "slice_group_by", since = "1.77.0")] impl<'a, T: 'a + fmt::Debug, P> fmt::Debug for ChunkBy<'a, T, P> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("ChunkBy") - .field("slice", &self.slice) - .finish() + f.debug_struct("ChunkBy").field("slice", &self.slice).finish() } } @@ -3393,11 +3238,7 @@ where #[inline] fn size_hint(&self) -> (usize, Option) { - if self.slice.is_empty() { - (0, Some(0)) - } else { - (1, Some(self.slice.len())) - } + if self.slice.is_empty() { (0, Some(0)) } else { (1, Some(self.slice.len())) } } #[inline] @@ -3439,9 +3280,7 @@ impl<'a, T: 'a, P> FusedIterator for ChunkByMut<'a, T, P> where P: FnMut(&T, &T) #[stable(feature = "slice_group_by", since = "1.77.0")] impl<'a, T: 'a + fmt::Debug, P> fmt::Debug for ChunkByMut<'a, T, P> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("ChunkByMut") - .field("slice", &self.slice) - .finish() + f.debug_struct("ChunkByMut").field("slice", &self.slice).finish() } } diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index fc636f78d3034..5fd38a8a8ae9b 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -156,11 +156,7 @@ impl [T] { #[inline] #[must_use] pub const fn first(&self) -> Option<&T> { - if let [first, ..] = self { - Some(first) - } else { - None - } + if let [first, ..] = self { Some(first) } else { None } } /// Returns a mutable reference to the first element of the slice, or `None` if it is empty. @@ -183,11 +179,7 @@ impl [T] { #[inline] #[must_use] pub const fn first_mut(&mut self) -> Option<&mut T> { - if let [first, ..] = self { - Some(first) - } else { - None - } + if let [first, ..] = self { Some(first) } else { None } } /// Returns the first and all the rest of the elements of the slice, or `None` if it is empty. @@ -207,11 +199,7 @@ impl [T] { #[inline] #[must_use] pub const fn split_first(&self) -> Option<(&T, &[T])> { - if let [first, tail @ ..] = self { - Some((first, tail)) - } else { - None - } + if let [first, tail @ ..] = self { Some((first, tail)) } else { None } } /// Returns the first and all the rest of the elements of the slice, or `None` if it is empty. @@ -233,11 +221,7 @@ impl [T] { #[inline] #[must_use] pub const fn split_first_mut(&mut self) -> Option<(&mut T, &mut [T])> { - if let [first, tail @ ..] = self { - Some((first, tail)) - } else { - None - } + if let [first, tail @ ..] = self { Some((first, tail)) } else { None } } /// Returns the last and all the rest of the elements of the slice, or `None` if it is empty. @@ -257,11 +241,7 @@ impl [T] { #[inline] #[must_use] pub const fn split_last(&self) -> Option<(&T, &[T])> { - if let [init @ .., last] = self { - Some((last, init)) - } else { - None - } + if let [init @ .., last] = self { Some((last, init)) } else { None } } /// Returns the last and all the rest of the elements of the slice, or `None` if it is empty. @@ -283,11 +263,7 @@ impl [T] { #[inline] #[must_use] pub const fn split_last_mut(&mut self) -> Option<(&mut T, &mut [T])> { - if let [init @ .., last] = self { - Some((last, init)) - } else { - None - } + if let [init @ .., last] = self { Some((last, init)) } else { None } } /// Returns the last element of the slice, or `None` if it is empty. @@ -306,11 +282,7 @@ impl [T] { #[inline] #[must_use] pub const fn last(&self) -> Option<&T> { - if let [.., last] = self { - Some(last) - } else { - None - } + if let [.., last] = self { Some(last) } else { None } } /// Returns a mutable reference to the last item in the slice, or `None` if it is empty. @@ -333,11 +305,7 @@ impl [T] { #[inline] #[must_use] pub const fn last_mut(&mut self) -> Option<&mut T> { - if let [.., last] = self { - Some(last) - } else { - None - } + if let [.., last] = self { Some(last) } else { None } } /// Returns an array reference to the first `N` items in the slice. @@ -2116,12 +2084,7 @@ impl [T] { ); // SAFETY: Caller has to check that `0 <= mid <= self.len()` - unsafe { - ( - from_raw_parts(ptr, mid), - from_raw_parts(ptr.add(mid), unchecked_sub(len, mid)), - ) - } + unsafe { (from_raw_parts(ptr, mid), from_raw_parts(ptr.add(mid), unchecked_sub(len, mid))) } } /// Divides one mutable slice into two at an index, without doing bounds checking. @@ -4019,10 +3982,7 @@ impl [T] { where T: Copy, { - let Range { - start: src_start, - end: src_end, - } = slice::range(src, ..self.len()); + let Range { start: src_start, end: src_end } = slice::range(src, ..self.len()); let count = src_end - src_start; assert!(dest <= self.len() - count, "dest is out of bounds"); // SAFETY: the conditions for `ptr::copy` have all been checked above, @@ -4089,10 +4049,7 @@ impl [T] { #[requires(self.len() == other.len())] #[cfg_attr(kani, kani::modifies(self, other))] pub const fn swap_with_slice(&mut self, other: &mut [T]) { - assert!( - self.len() == other.len(), - "destination and source slices have different lengths" - ); + assert!(self.len() == other.len(), "destination and source slices have different lengths"); // SAFETY: `self` is valid for `self.len()` elements by definition, and `src` was // checked to have the same length. The slices cannot overlap because // mutable references are exclusive. @@ -4595,8 +4552,7 @@ impl [T] { where P: FnMut(&T) -> bool, { - self.binary_search_by(|x| if pred(x) { Less } else { Greater }) - .unwrap_or_else(|i| i) + self.binary_search_by(|x| if pred(x) { Less } else { Greater }).unwrap_or_else(|i| i) } /// Removes the subslice corresponding to the given range @@ -4909,10 +4865,7 @@ impl [T] { unsafe { for i in 0..N { let idx = indices.get_unchecked(i).clone(); - arr_ptr - .cast::<&mut I::Output>() - .add(i) - .write(&mut *slice.get_unchecked_mut(idx)); + arr_ptr.cast::<&mut I::Output>().add(i).write(&mut *slice.get_unchecked_mut(idx)); } arr.assume_init() } @@ -5030,11 +4983,7 @@ impl [T] { let offset = byte_offset / size_of::(); - if offset < self.len() { - Some(offset) - } else { - None - } + if offset < self.len() { Some(offset) } else { None } } /// Returns the range of indices that a subslice points to. @@ -5089,11 +5038,7 @@ impl [T] { let start = byte_start / size_of::(); let end = start.wrapping_add(subslice.len()); - if start <= self.len() && end <= self.len() { - Some(start..end) - } else { - None - } + if start <= self.len() && end <= self.len() { Some(start..end) } else { None } } } @@ -5333,10 +5278,7 @@ where { #[track_caller] default fn spec_clone_from(&mut self, src: &[T]) { - assert!( - self.len() == src.len(), - "destination and source slices have different lengths" - ); + assert!(self.len() == src.len(), "destination and source slices have different lengths"); // NOTE: We need to explicitly slice them to the same length // to make it easier for the optimizer to elide bounds checking. // But since it can't be relied on we also have an explicit specialization for T: Copy. @@ -5379,11 +5321,7 @@ impl const Default for &mut [T] { } } -#[unstable( - feature = "slice_pattern", - reason = "stopgap trait for slice patterns", - issue = "56345" -)] +#[unstable(feature = "slice_pattern", reason = "stopgap trait for slice patterns", issue = "56345")] /// Patterns in slices - currently, only used by `strip_prefix` and `strip_suffix`. At a future /// point, we hope to generalise `core::str::Pattern` (which at the time of writing is limited to /// `str`) to slices, and then this trait will be replaced or abolished. @@ -5766,10 +5704,7 @@ mod verify { fn check_get_unchecked_core_range() { let arr: [u8; CAP] = kani::any(); let slice = any_ref(&arr); - let idx = range::Range { - start: kani::any(), - end: kani::any(), - }; + let idx = range::Range { start: kani::any(), end: kani::any() }; let _ = unsafe { slice.get_unchecked(idx) }; } @@ -5777,10 +5712,7 @@ mod verify { fn check_get_unchecked_core_range_inclusive() { let arr: [u8; CAP] = kani::any(); let slice = any_ref(&arr); - let idx = range::RangeInclusive { - start: kani::any(), - last: kani::any(), - }; + let idx = range::RangeInclusive { start: kani::any(), last: kani::any() }; let _ = unsafe { slice.get_unchecked(idx) }; } @@ -6098,11 +6030,7 @@ mod verify { #[kani::proof] fn check_get_disjoint_check_valid() { - let indices = [ - kani::any::(), - kani::any::(), - kani::any::(), - ]; + let indices = [kani::any::(), kani::any::(), kani::any::()]; let _ = get_disjoint_check_valid(&indices, kani::any()); } diff --git a/library/core/src/slice/sort/select.rs b/library/core/src/slice/sort/select.rs index 1b6fc9453d938..fc31013caf88c 100644 --- a/library/core/src/slice/sort/select.rs +++ b/library/core/src/slice/sort/select.rs @@ -26,10 +26,7 @@ where // Puts a lower limit of 1 on `len`. if index >= len { - panic!( - "partition_at_index index {} greater than length of slice {}", - index, len - ); + panic!("partition_at_index index {} greater than length of slice {}", index, len); } if T::IS_ZST { @@ -236,19 +233,7 @@ fn median_of_ninthers bool>(v: &mut [T], is_less: &mut F) let mut a = lo - 4 * frac - gap; let mut b = hi + gap; for i in lo..hi { - ninther( - v, - is_less, - a, - i - frac, - b, - a + 1, - i, - b + 1, - a + 2, - i + frac, - b + 2, - ); + ninther(v, is_less, a, i - frac, b, a + 1, i, b + 1, a + 2, i + frac, b + 2); a += 3; b += 3; } diff --git a/library/core/src/slice/sort/shared/mod.rs b/library/core/src/slice/sort/shared/mod.rs index 9f51fccc92f3d..e2cdcb3dd511d 100644 --- a/library/core/src/slice/sort/shared/mod.rs +++ b/library/core/src/slice/sort/shared/mod.rs @@ -1,7 +1,4 @@ -#![cfg_attr( - any(feature = "optimize_for_size", target_pointer_width = "16"), - allow(dead_code) -)] +#![cfg_attr(any(feature = "optimize_for_size", target_pointer_width = "16"), allow(dead_code))] use crate::marker::Freeze; diff --git a/library/core/src/slice/sort/shared/smallsort.rs b/library/core/src/slice/sort/shared/smallsort.rs index 95927e5b351da..e555fce440872 100644 --- a/library/core/src/slice/sort/shared/smallsort.rs +++ b/library/core/src/slice/sort/shared/smallsort.rs @@ -267,11 +267,7 @@ fn small_sort_general_with_scratch bool>( // We extend this to desired_len, src is valid for desired_len elements. let src = v_base.add(offset); let dst = scratch_base.add(offset); - let desired_len = if offset == 0 { - len_div_2 - } else { - len - len_div_2 - }; + let desired_len = if offset == 0 { len_div_2 } else { len - len_div_2 }; for i in presorted_len..desired_len { ptr::copy_nonoverlapping(src.add(i), dst.add(i), 1); @@ -280,11 +276,7 @@ fn small_sort_general_with_scratch bool>( } // SAFETY: see comment in `CopyOnDrop::drop`. - let drop_guard = CopyOnDrop { - src: scratch_base, - dst: v_base, - len, - }; + let drop_guard = CopyOnDrop { src: scratch_base, dst: v_base, len }; // SAFETY: at this point scratch_base is fully initialized, allowing us // to use it as the source of our merge back into the original array. @@ -562,11 +554,7 @@ unsafe fn insert_tail bool>(begin: *mut T, tail: *mut T, // the correct insertion position, gap_guard ensures the element is moved // back into the array. let tmp = ManuallyDrop::new(tail.read()); - let mut gap_guard = CopyOnDrop { - src: &*tmp, - dst: tail, - len: 1, - }; + let mut gap_guard = CopyOnDrop { src: &*tmp, dst: tail, len: 1 }; loop { // SAFETY: we move sift into the gap (which is valid), and point the diff --git a/library/core/src/slice/sort/stable/drift.rs b/library/core/src/slice/sort/stable/drift.rs index 29274180b87a8..1edffe095a89d 100644 --- a/library/core/src/slice/sort/stable/drift.rs +++ b/library/core/src/slice/sort/stable/drift.rs @@ -60,13 +60,8 @@ pub fn sort bool>( // with root-level desired depth to fully collapse the merge tree. let (next_run, desired_depth); if scan_idx < len { - next_run = create_run( - &mut v[scan_idx..], - scratch, - min_good_run_len, - eager_sort, - is_less, - ); + next_run = + create_run(&mut v[scan_idx..], scratch, min_good_run_len, eager_sort, is_less); desired_depth = merge_tree_depth( scan_idx - prev_run.len(), scan_idx, diff --git a/library/core/src/slice/sort/stable/merge.rs b/library/core/src/slice/sort/stable/merge.rs index e09a5b670e7d0..bb2747bfc78ac 100644 --- a/library/core/src/slice/sort/stable/merge.rs +++ b/library/core/src/slice/sort/stable/merge.rs @@ -50,11 +50,7 @@ pub fn merge bool>( ptr::copy_nonoverlapping(save_base, buf, save_len); - let mut merge_state = MergeState { - start: buf, - end: buf.add(save_len), - dst: save_base, - }; + let mut merge_state = MergeState { start: buf, end: buf.add(save_len), dst: save_base }; if left_is_shorter { merge_state.merge_up(v_mid, v_end, is_less); diff --git a/library/core/src/slice/sort/stable/mod.rs b/library/core/src/slice/sort/stable/mod.rs index b49d6cb7e46c6..8b4e5c0c8c3a1 100644 --- a/library/core/src/slice/sort/stable/mod.rs +++ b/library/core/src/slice/sort/stable/mod.rs @@ -153,10 +153,7 @@ struct AlignedStorage { impl AlignedStorage { fn new() -> Self { - Self { - _align: [], - storage: [const { MaybeUninit::uninit() }; N], - } + Self { _align: [], storage: [const { MaybeUninit::uninit() }; N] } } fn as_uninit_slice_mut(&mut self) -> &mut [MaybeUninit] { diff --git a/library/core/src/slice/sort/stable/quicksort.rs b/library/core/src/slice/sort/stable/quicksort.rs index ecd069b2d407f..0439ba870bd2b 100644 --- a/library/core/src/slice/sort/stable/quicksort.rs +++ b/library/core/src/slice/sort/stable/quicksort.rs @@ -197,14 +197,7 @@ impl PartitionState { /// scan buffer must be initialized. unsafe fn new(scan: *const T, scratch: *mut T, len: usize) -> Self { // SAFETY: See function safety comment. - unsafe { - Self { - scratch_base: scratch, - scan, - num_left: 0, - scratch_rev: scratch.add(len), - } - } + unsafe { Self { scratch_base: scratch, scan, num_left: 0, scratch_rev: scratch.add(len) } } } /// Depending on the value of `towards_left` this function will write a value @@ -227,11 +220,7 @@ impl PartitionState { // SAFETY: now we have scratch_rev == base + len - (i + 1). This means // scratch_rev + num_left == base + len - 1 - num_right < base + len. - let dst_base = if towards_left { - self.scratch_base - } else { - self.scratch_rev - }; + let dst_base = if towards_left { self.scratch_base } else { self.scratch_rev }; let dst = dst_base.add(self.num_left); ptr::copy_nonoverlapping(self.scan, dst, 1); diff --git a/library/core/src/slice/sort/unstable/quicksort.rs b/library/core/src/slice/sort/unstable/quicksort.rs index f274f623cd9fe..bdf56a8080305 100644 --- a/library/core/src/slice/sort/unstable/quicksort.rs +++ b/library/core/src/slice/sort/unstable/quicksort.rs @@ -211,10 +211,7 @@ where let is_first_swap_pair = gap_opt.is_none(); if is_first_swap_pair { - gap_opt = Some(GapGuard { - pos: right, - value: ManuallyDrop::new(ptr::read(left)), - }); + gap_opt = Some(GapGuard { pos: right, value: ManuallyDrop::new(ptr::read(left)) }); } let gap = gap_opt.as_mut().unwrap_unchecked(); @@ -304,10 +301,7 @@ where num_lt: 0, right: v_base.add(1), - gap: GapGuardRaw { - pos: v_base, - value: &mut *gap_value, - }, + gap: GapGuardRaw { pos: v_base, value: &mut *gap_value }, }; // Manual unrolling that works well on x86, Arm and with opt-level=s without murdering @@ -329,11 +323,7 @@ where let end = v_base.add(len); loop { let is_done = state.right == end; - state.right = if is_done { - state.gap.value - } else { - state.right - }; + state.right = if is_done { state.gap.value } else { state.right }; loop_body(&mut state); From 2039ebdda3faa5de9a57b209a22976fec794e4fe Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 19:53:10 +0530 Subject: [PATCH 3/6] Challenge 17: fix Kani loop contracts on slice search/dedup Overflow-safe invariants and loop_modifies so check_binary_search_by and check_partition_dedup_by verify. --- library/core/src/slice/mod.rs | 40 +++++++++++++++++++++++++++++------ 1 file changed, 33 insertions(+), 7 deletions(-) diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index 5fd38a8a8ae9b..73f126ff6b606 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -3017,20 +3017,32 @@ impl [T] { return Err(0); } let mut base = 0usize; + let mut half = 0usize; + let mut mid = 0usize; + let mut cmp = Equal; // This loop intentionally doesn't have an early exit if the comparison // returns Equal. We want the number of loop iterations to depend *only* // on the size of the input slice so that the CPU can reliably predict // the loop count. - #[loop_invariant(size >= 1 && base + size <= self.len())] + // Overflow-safe form of `base + size <= self.len()` (Kani havocs before assume). + #[loop_invariant( + size >= 1 + && size <= self.len() + && base.wrapping_add(size) >= base + && base.wrapping_add(size) <= self.len() + && base.wrapping_add(size / 2) >= base + && base.wrapping_add(size / 2) < self.len() + )] + #[cfg_attr(kani, kani::loop_modifies(&size, &base, &half, &mid, &cmp))] while size > 1 { - let half = size / 2; - let mid = base + half; + half = size / 2; + mid = base + half; // SAFETY: the call is made safe by the following invariants: // - `mid >= 0`: by definition // - `mid < size`: `mid = size / 2 + size / 4 + size / 8 ...` - let cmp = f(unsafe { self.get_unchecked(mid) }); + cmp = f(unsafe { self.get_unchecked(mid) }); // Binary search interacts poorly with branch prediction, so force // the compiler to use conditional moves if supported by the target @@ -3611,6 +3623,9 @@ impl [T] { let ptr = self.as_mut_ptr(); let mut next_read: usize = 1; let mut next_write: usize = 1; + let mut ptr_read = ptr; + let mut prev_ptr_write = ptr; + let mut ptr_write = ptr; // SAFETY: the `while` condition guarantees `next_read` and `next_write` // are less than `len`, thus are inside `self`. `prev_ptr_write` points to @@ -3635,12 +3650,23 @@ impl [T] { && next_write <= next_read && next_read >= 1 )] + #[cfg_attr( + kani, + kani::loop_modifies( + unsafe { slice::from_raw_parts_mut(ptr, len) }, + &next_read, + &next_write, + &ptr_read, + &prev_ptr_write, + &ptr_write + ) + )] while next_read < len { - let ptr_read = ptr.add(next_read); - let prev_ptr_write = ptr.add(next_write - 1); + ptr_read = ptr.add(next_read); + prev_ptr_write = ptr.add(next_write - 1); if !same_bucket(&mut *ptr_read, &mut *prev_ptr_write) { if next_read != next_write { - let ptr_write = prev_ptr_write.add(1); + ptr_write = prev_ptr_write.add(1); mem::swap(&mut *ptr_read, &mut *ptr_write); } next_write += 1; From 07515f7cffbade06132bacfadfa7b521d8733fc2 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 21:15:22 +0530 Subject: [PATCH 4/6] chore: re-trigger CI after GitHub runner cancel Autoharness ubuntu ended with runner shutdown after 1h11m, not a Kani counterexample. From a71ac3d7543d7cffa3e86187d5177bb788cda31d Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 23:27:13 +0530 Subject: [PATCH 5/6] Challenge 17: 2-byte rotate/swap harnesses for autoharness timeout CAP=8 plus symbolic mid times out autoharness's 10m CBMC cap on ptr_rotate, rotate_left, rotate_right, and swap_with_slice (1423/4). Fixed length 2 still runs the real memmove / swap_nonoverlapping path. --- library/core/src/slice/mod.rs | 38 ++++++++++++++++++----------------- 1 file changed, 20 insertions(+), 18 deletions(-) diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index 73f126ff6b606..d906f9dcb2f59 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -5976,28 +5976,30 @@ mod verify { let _ = slice.partition_dedup_by(|a, b| a == b); } + // CAP=8 + symbolic mid times out autoharness's 10m CBMC cap on the + // memmove/gcd/swap rotate algorithms. Length 2 still calls the real + // `ptr_rotate` body (including the no-op `mid == 0` / `mid == len` arms). #[kani::proof_for_contract(<[u8]>::rotate_left)] + #[kani::unwind(3)] fn check_rotate_left() { - let mut arr: [u8; CAP] = kani::any(); - let slice = any_mut(&mut arr); - slice.rotate_left(kani::any()); + let mut arr: [u8; 2] = kani::any(); + arr.rotate_left(kani::any_where(|&m: &usize| m <= arr.len())); } #[kani::proof_for_contract(<[u8]>::rotate_right)] + #[kani::unwind(3)] fn check_rotate_right() { - let mut arr: [u8; CAP] = kani::any(); - let slice = any_mut(&mut arr); - slice.rotate_right(kani::any()); + let mut arr: [u8; 2] = kani::any(); + arr.rotate_right(kani::any_where(|&k: &usize| k <= arr.len())); } #[kani::proof_for_contract(super::rotate::ptr_rotate)] + #[kani::unwind(3)] fn check_ptr_rotate() { - let mut arr: [u8; CAP] = kani::any(); - let slice = any_mut(&mut arr); - let mid = kani::any::(); - kani::assume(mid <= slice.len()); - let k = slice.len() - mid; - let p = slice.as_mut_ptr(); + let mut arr: [u8; 2] = kani::any(); + let mid = kani::any_where(|&m: &usize| m <= arr.len()); + let k = arr.len() - mid; + let p = arr.as_mut_ptr(); unsafe { super::rotate::ptr_rotate(mid, p.add(mid), k) }; } @@ -6025,14 +6027,14 @@ mod verify { } } + // CAP=8 + two symbolic equal lengths times out autoharness's 10m CBMC cap + // on `ptr::swap_nonoverlapping`. Length 2 still runs the real swap path. #[kani::proof_for_contract(<[u8]>::swap_with_slice)] + #[kani::unwind(3)] fn check_swap_with_slice() { - let mut a: [u8; CAP] = kani::any(); - let mut b: [u8; CAP] = kani::any(); - let left = any_mut(&mut a); - let right = any_mut(&mut b); - kani::assume(left.len() == right.len()); - left.swap_with_slice(right); + let mut a: [u8; 2] = kani::any(); + let mut b: [u8; 2] = kani::any(); + a.swap_with_slice(&mut b); } #[kani::proof] From 6e8f8be38eb740d104ad17bd9fef1d9aeed88e82 Mon Sep 17 00:00:00 2001 From: Sankalp Thakur Date: Thu, 20 Aug 2026 23:59:14 +0530 Subject: [PATCH 6/6] Challenge 17: bind rotate length before the mutable call GOTO codegen failed E0502: rotate_left/right mut-borrow arr while any_where reads arr.len() in the same argument. Snapshot len first. --- library/core/src/slice/mod.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index d906f9dcb2f59..493f1919a580f 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -5983,14 +5983,16 @@ mod verify { #[kani::unwind(3)] fn check_rotate_left() { let mut arr: [u8; 2] = kani::any(); - arr.rotate_left(kani::any_where(|&m: &usize| m <= arr.len())); + let len = arr.len(); + arr.rotate_left(kani::any_where(|&m: &usize| m <= len)); } #[kani::proof_for_contract(<[u8]>::rotate_right)] #[kani::unwind(3)] fn check_rotate_right() { let mut arr: [u8; 2] = kani::any(); - arr.rotate_right(kani::any_where(|&k: &usize| k <= arr.len())); + let len = arr.len(); + arr.rotate_right(kani::any_where(|&k: &usize| k <= len)); } #[kani::proof_for_contract(super::rotate::ptr_rotate)]