Challenge 17: Verify slice safety with Kani

library/core/src/index.rs

@@ -78,6 +78,11 @@ unsafe impl<T> SliceIndex<[T]> for Clamp<usize> {
     fn index_mut(self, slice: &mut [T]) -> &mut Self::Output {
         &mut (*slice)[cmp::min(self.0, slice.len() - 1)]
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        len > 0
+    }
 }
 
 #[unstable(feature = "sliceindex_wrappers", issue = "146179")]
@@ -121,6 +126,11 @@ unsafe impl<T> SliceIndex<[T]> for Clamp<range::Range<usize>> {
         let end = cmp::min(self.0.end, slice.len());
         (start..end).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        cmp::min(self.0.start, len) <= cmp::min(self.0.end, len)
+    }
 }
 
 #[unstable(feature = "sliceindex_wrappers", issue = "146179")]
@@ -164,6 +174,11 @@ unsafe impl<T> SliceIndex<[T]> for Clamp<ops::Range<usize>> {
         let end = cmp::min(self.0.end, slice.len());
         (start..end).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        cmp::min(self.0.start, len) <= cmp::min(self.0.end, len)
+    }
 }
 
 #[unstable(feature = "sliceindex_wrappers", issue = "146179")]
@@ -207,6 +222,17 @@ unsafe impl<T> SliceIndex<[T]> for Clamp<range::RangeInclusive<usize>> {
         let end = cmp::min(self.0.last, slice.len() - 1);
         (start..=end).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        if len == 0 {
+            false
+        } else {
+            let start = cmp::min(self.0.start, len - 1);
+            let end = cmp::min(self.0.last, len - 1);
+            start <= end + 1
+        }
+    }
 }
 
 #[unstable(feature = "sliceindex_wrappers", issue = "146179")]
@@ -250,6 +276,17 @@ unsafe impl<T> SliceIndex<[T]> for Clamp<ops::RangeInclusive<usize>> {
         let end = cmp::min(self.0.end, slice.len() - 1);
         (start..=end).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        if len == 0 {
+            false
+        } else {
+            let start = cmp::min(*self.0.start(), len - 1);
+            let end = cmp::min(*self.0.end(), len - 1);
+            start <= end + 1
+        }
+    }
 }
 
 #[unstable(feature = "sliceindex_wrappers", issue = "146179")]
@@ -281,6 +318,11 @@ unsafe impl<T> SliceIndex<[T]> for Clamp<range::RangeFrom<usize>> {
     fn index_mut(self, slice: &mut [T]) -> &mut Self::Output {
         (cmp::min(self.0.start, slice.len())..).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, _len: usize) -> bool {
+        true
+    }
 }
 
 #[unstable(feature = "sliceindex_wrappers", issue = "146179")]
@@ -312,6 +354,11 @@ unsafe impl<T> SliceIndex<[T]> for Clamp<ops::RangeFrom<usize>> {
     fn index_mut(self, slice: &mut [T]) -> &mut Self::Output {
         (cmp::min(self.0.start, slice.len())..).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, _len: usize) -> bool {
+        true
+    }
 }
 
 #[unstable(feature = "sliceindex_wrappers", issue = "146179")]
@@ -343,6 +390,11 @@ unsafe impl<T> SliceIndex<[T]> for Clamp<range::RangeTo<usize>> {
     fn index_mut(self, slice: &mut [T]) -> &mut Self::Output {
         (..cmp::min(self.0.end, slice.len())).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, _len: usize) -> bool {
+        true
+    }
 }
 
 #[unstable(feature = "sliceindex_wrappers", issue = "146179")]
@@ -374,6 +426,11 @@ unsafe impl<T> SliceIndex<[T]> for Clamp<range::RangeToInclusive<usize>> {
     fn index_mut(self, slice: &mut [T]) -> &mut Self::Output {
         (..=cmp::min(self.0.last, slice.len() - 1)).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        len > 0
+    }
 }
 
 #[unstable(feature = "sliceindex_wrappers", issue = "146179")]
@@ -405,6 +462,11 @@ unsafe impl<T> SliceIndex<[T]> for Clamp<ops::RangeToInclusive<usize>> {
     fn index_mut(self, slice: &mut [T]) -> &mut Self::Output {
         (..=cmp::min(self.0.end, slice.len() - 1)).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        len > 0
+    }
 }
 
 #[unstable(feature = "sliceindex_wrappers", issue = "146179")]
@@ -436,6 +498,11 @@ unsafe impl<T> SliceIndex<[T]> for Clamp<range::RangeFull> {
     fn index_mut(self, slice: &mut [T]) -> &mut Self::Output {
         (..).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, _len: usize) -> bool {
+        true
+    }
 }
 
 #[unstable(feature = "sliceindex_wrappers", issue = "146179")]
@@ -469,4 +536,9 @@ unsafe impl<T> SliceIndex<[T]> for Last {
         // N.B., use intrinsic indexing
         &mut (*slice)[slice.len() - 1]
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        len > 0
+    }
 }

library/core/src/ptr/mod.rs

@@ -1404,6 +1404,15 @@ pub const unsafe fn swap_nonoverlapping<T>(x: *mut T, y: *mut T, count: usize) {
 #[inline]
 const unsafe fn swap_nonoverlapping_const<T>(x: *mut T, y: *mut T, count: usize) {
     let mut i = 0;
+    #[safety::loop_invariant(i <= count)]
+    #[cfg_attr(
+        kani,
+        kani::loop_modifies(
+            &i,
+            slice_from_raw_parts_mut(x, count),
+            slice_from_raw_parts_mut(y, count)
+        )
+    )]
     while i < count {
         // SAFETY: By precondition, `i` is in-bounds because it's below `n`
         let x = unsafe { x.add(i) };
@@ -1445,6 +1454,26 @@ unsafe fn swap_nonoverlapping_bytes(x: *mut u8, y: *mut u8, bytes: NonZero<usize
         chunks: NonZero<usize>,
     ) {
         let chunks = chunks.get();
+        // Kani needs the loop counter to be explicit so it can include it in
+        // the loop frame. This is only a direct `for`-to-`while` rewrite: the
+        // iteration range and swap body are unchanged, so it does not weaken
+        // the verification with a summary or stub.
+        #[cfg(kani)]
+        {
+            let mut i = 0;
+            #[safety::loop_invariant(i <= chunks)]
+            #[kani::loop_modifies(
+                &i,
+                slice_from_raw_parts_mut(x, chunks),
+                slice_from_raw_parts_mut(y, chunks)
+            )]
+            while i < chunks {
+                // SAFETY: i is in [0, chunks) so the adds and dereferences are in-bounds.
+                unsafe { swap_chunk(&mut *x.add(i), &mut *y.add(i)) };
+                i += 1;
+            }
+        }
+        #[cfg(not(kani))]
         for i in 0..chunks {
             // SAFETY: i is in [0, chunks) so the adds and dereferences are in-bounds.
             unsafe { swap_chunk(&mut *x.add(i), &mut *y.add(i)) };

library/core/src/slice/index.rs

@@ -206,6 +206,18 @@ pub const unsafe trait SliceIndex<T: ?Sized>: private_slice_index::Sealed {
     #[unstable(feature = "slice_index_methods", issue = "none")]
     #[track_caller]
     fn index_mut(self, slice: &mut T) -> &mut Self::Output;
+
+    /// Kani-only hook for expressing the documented precondition of
+    /// `get_unchecked` and `get_unchecked_mut`. Every implementation used by a
+    /// contracted caller must override this with its exact bounds condition.
+    /// The unrestricted default makes a missing override fail the caller's
+    /// contract proof instead of making it vacuous.
+    #[cfg(kani)]
+    #[unstable(feature = "kani", issue = "none")]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        let _ = len;
+        true
+    }
 }
 
 /// The methods `index` and `index_mut` panic if the index is out of bounds.
@@ -277,6 +289,11 @@ unsafe impl<T> const SliceIndex<[T]> for usize {
         // N.B., use intrinsic indexing
         &mut (*slice)[self]
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        *self < len
+    }
 }
 
 /// Because `IndexRange` guarantees `start <= end`, fewer checks are needed here
@@ -352,6 +369,11 @@ unsafe impl<T> const SliceIndex<[T]> for ops::IndexRange {
             slice_index_fail(self.start(), self.end(), slice.len())
         }
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        self.start() <= self.end() && self.end() <= len
+    }
 }
 
 /// The methods `index` and `index_mut` panic if:
@@ -456,6 +478,11 @@ unsafe impl<T> const SliceIndex<[T]> for ops::Range<usize> {
             slice_index_fail(self.start, self.end, slice.len())
         }
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        self.start <= self.end && self.end <= len
+    }
 }
 
 #[unstable(feature = "new_range_api", issue = "125687")]
@@ -494,6 +521,11 @@ unsafe impl<T> const SliceIndex<[T]> for range::Range<usize> {
     fn index_mut(self, slice: &mut [T]) -> &mut [T] {
         ops::Range::from(self).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_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 +565,11 @@ unsafe impl<T> const SliceIndex<[T]> for ops::RangeTo<usize> {
     fn index_mut(self, slice: &mut [T]) -> &mut [T] {
         (0..self.end).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_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 +623,11 @@ unsafe impl<T> const SliceIndex<[T]> for ops::RangeFrom<usize> {
             &mut *get_offset_len_mut_noubcheck(slice, self.start, new_len)
         }
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        self.start <= len
+    }
 }
 
 #[unstable(feature = "new_range_api", issue = "125687")]
@@ -624,6 +666,11 @@ unsafe impl<T> const SliceIndex<[T]> for range::RangeFrom<usize> {
     fn index_mut(self, slice: &mut [T]) -> &mut [T] {
         ops::RangeFrom::from(self).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        self.start <= len
+    }
 }
 
 #[stable(feature = "slice_get_slice_impls", since = "1.15.0")]
@@ -660,6 +707,11 @@ unsafe impl<T> const SliceIndex<[T]> for ops::RangeFull {
     fn index_mut(self, slice: &mut [T]) -> &mut [T] {
         slice
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, _len: usize) -> bool {
+        true
+    }
 }
 
 /// The methods `index` and `index_mut` panic if:
@@ -722,6 +774,11 @@ unsafe impl<T> const SliceIndex<[T]> for ops::RangeInclusive<usize> {
         }
         slice_index_fail(start, end, slice.len())
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        self.end < len && (self.exhausted || self.start <= self.end + 1)
+    }
 }
 
 #[unstable(feature = "new_range_api", issue = "125687")]
@@ -760,6 +817,11 @@ unsafe impl<T> const SliceIndex<[T]> for range::RangeInclusive<usize> {
     fn index_mut(self, slice: &mut [T]) -> &mut [T] {
         ops::RangeInclusive::from(self).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        self.last < len && self.start <= self.last + 1
+    }
 }
 
 /// The methods `index` and `index_mut` panic if the end of the range is out of bounds.
@@ -799,6 +861,11 @@ unsafe impl<T> const SliceIndex<[T]> for ops::RangeToInclusive<usize> {
     fn index_mut(self, slice: &mut [T]) -> &mut [T] {
         (0..=self.end).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_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 +905,11 @@ unsafe impl<T> const SliceIndex<[T]> for range::RangeToInclusive<usize> {
     fn index_mut(self, slice: &mut [T]) -> &mut [T] {
         (0..=self.last).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        self.last < len
+    }
 }
 
 /// Performs bounds checking of a range.
@@ -1100,4 +1172,9 @@ unsafe impl<T> SliceIndex<[T]> for (ops::Bound<usize>, ops::Bound<usize>) {
     fn index_mut(self, slice: &mut [T]) -> &mut Self::Output {
         into_slice_range(slice.len(), self).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn kani_in_bounds(&self, len: usize) -> bool {
+        into_range(len, *self).is_some_and(|range| range.start <= range.end && range.end <= len)
+    }
 }