Challenge 24: Verify Vec Part2 safety with Kani

library/alloc/src/lib.rs

@@ -131,6 +131,7 @@
 #![feature(panic_internals)]
 #![feature(pattern)]
 #![feature(pin_coerce_unsized_trait)]
+#![feature(proc_macro_hygiene)]
 #![feature(ptr_alignment_type)]
 #![feature(ptr_internals)]
 #![feature(ptr_metadata)]

library/alloc/src/vec/extract_if.rs

@@ -1,3 +1,5 @@
+#[cfg(kani)]
+use core::kani;
 use core::ops::{Range, RangeBounds};
 use core::{fmt, ptr, slice};
 
@@ -64,6 +66,42 @@ where
     type Item = T;
 
     fn next(&mut self) -> Option<T> {
+        #[cfg(kani)]
+        let is_zst = core::mem::size_of::<T>() == 0;
+        #[cfg(kani)]
+        let base = self.vec.as_mut_ptr();
+        #[cfg(kani)]
+        let capacity = self.vec.capacity();
+        #[cfg(kani)]
+        let mut cur = base;
+        #[cfg(kani)]
+        let modified_items = if is_zst {
+            ptr::slice_from_raw_parts(core::ptr::null::<T>(), 0)
+        } else {
+            ptr::slice_from_raw_parts(base, self.old_len)
+        };
+        #[cfg(kani)]
+        let modified_items_mut = if is_zst {
+            ptr::slice_from_raw_parts_mut(core::ptr::null_mut::<T>(), 0)
+        } else {
+            ptr::slice_from_raw_parts_mut(base, self.old_len)
+        };
+        #[cfg(kani)]
+        kani::assume(kani::mem::can_write(modified_items_mut));
+
+        #[cfg_attr(kani, kani::loop_invariant(
+            (is_zst || self.old_len <= capacity)
+                && self.idx <= self.end
+                && self.end <= self.old_len
+                && self.del <= self.idx
+                && kani::mem::can_write(modified_items_mut)
+        ))]
+        #[cfg_attr(kani, kani::loop_modifies(
+            &self.idx,
+            &self.del,
+            &cur,
+            modified_items
+        ))]
         while self.idx < self.end {
             let i = self.idx;
             // SAFETY:
@@ -75,7 +113,20 @@ where
             //
             //  Note: we can't use `vec.get_unchecked_mut(i)` here since the precondition for that
             //  function is that i < vec.len(), but we've set vec's length to zero.
+            #[cfg(kani)]
+            {
+                kani::assume(i < self.old_len && i < capacity);
+                kani::assume(kani::mem::can_write(unsafe { base.add(i) }));
+            }
+            #[cfg(kani)]
+            {
+                cur = unsafe { base.add(i) };
+            }
+            #[cfg(not(kani))]
             let cur = unsafe { &mut *self.vec.as_mut_ptr().add(i) };
+            #[cfg(kani)]
+            let drained = (self.pred)(unsafe { &mut *cur });
+            #[cfg(not(kani))]
             let drained = (self.pred)(cur);
             // Update the index *after* the predicate is called. If the index
             // is updated prior and the predicate panics, the element at this
@@ -89,7 +140,13 @@ where
                 // SAFETY: `self.del` > 0, so the hole slot must not overlap with current element.
                 // We use copy for move, and never touch this element again.
                 unsafe {
-                    let hole_slot = self.vec.as_mut_ptr().add(i - self.del);
+                    let hole = i - self.del;
+                    #[cfg(kani)]
+                    kani::assume(hole < i);
+                    #[cfg(kani)]
+                    let hole_slot = base.add(hole);
+                    #[cfg(not(kani))]
+                    let hole_slot = self.vec.as_mut_ptr().add(hole);
                     ptr::copy_nonoverlapping(cur, hole_slot, 1);
                 }
             }
@@ -133,3 +190,43 @@ where
         f.debug_struct("ExtractIf").field("peek", &peek).finish_non_exhaustive()
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::super::kani_vec_harness_helpers::*;
+    use super::*;
+
+    // Harnesses for ExtractIf::next()
+    macro_rules! gen_extract_if_next_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Create a non-deterministic Vec for the target element type
+                let mut vec = verifier_nondet_bounded_vec::<$ty>();
+                // Choose a non-deterministic in-bounds extraction range
+                let start = kani::any_where(|i: &usize| *i <= vec.len());
+                let end = kani::any_where(|j: &usize| start <= *j && *j <= vec.len());
+                // Create an ExtractIf iterator with a non-deterministic predicate
+                let mut iter = vec.extract_if(start..end, |_x| kani::any::<bool>());
+                // Advance the ExtractIf iterator by one element if one is selected
+                let _ = iter.next();
+            }
+        };
+    }
+
+    gen_extract_if_next_harness!(harness_extract_if_next_u8, u8);
+    gen_extract_if_next_harness!(harness_extract_if_next_u16, u16);
+    gen_extract_if_next_harness!(harness_extract_if_next_u32, u32);
+    gen_extract_if_next_harness!(harness_extract_if_next_u64, u64);
+    gen_extract_if_next_harness!(harness_extract_if_next_u128, u128);
+    gen_extract_if_next_harness!(harness_extract_if_next_usize, usize);
+    gen_extract_if_next_harness!(harness_extract_if_next_i8, i8);
+    gen_extract_if_next_harness!(harness_extract_if_next_i16, i16);
+    gen_extract_if_next_harness!(harness_extract_if_next_i32, i32);
+    gen_extract_if_next_harness!(harness_extract_if_next_i64, i64);
+    gen_extract_if_next_harness!(harness_extract_if_next_i128, i128);
+    gen_extract_if_next_harness!(harness_extract_if_next_isize, isize);
+    gen_extract_if_next_harness!(harness_extract_if_next_unit, ());
+    gen_extract_if_next_harness!(harness_extract_if_next_array, [u8; 4]);
+}