Challenge 17: Kani contracts for slice functions

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;
+
+    /// 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 +289,11 @@ unsafe impl<T> 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
@@ -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 in_bounds(&self, len: usize) -> bool {
+        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 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 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 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 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 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 in_bounds(&self, _len: usize) -> bool {
+        true
+    }
 }
 
 /// The methods `index` and `index_mut` panic if:
@@ -722,6 +774,17 @@ unsafe impl<T> const SliceIndex<[T]> for ops::RangeInclusive<usize> {
         }
         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 +823,15 @@ 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 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 +871,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 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 +915,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 in_bounds(&self, len: usize) -> bool {
+        self.last < len
+    }
 }
 
 /// Performs bounds checking of a range.
@@ -1100,4 +1182,12 @@ 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 in_bounds(&self, len: usize) -> bool {
+        match into_range(len, *self) {
+            Some(r) => r.start <= r.end && r.end <= len,
+            None => false,
+        }
+    }
 }

library/core/src/slice/iter.rs

@@ -3121,7 +3121,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;
@@ -3153,7 +3157,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;
@@ -3215,7 +3223,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);
@@ -3248,7 +3260,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);