Verify safety of Vec iterator and specialization functions (Challenge 24)

library/alloc/src/vec/extract_if.rs

@@ -133,3 +133,53 @@ where
         f.debug_struct("ExtractIf").field("peek", &peek).finish_non_exhaustive()
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use core::kani;
+
+    use crate::vec::Vec;
+
+    const MAX_LEN: usize = 3;
+
+    fn any_vec<T: kani::Arbitrary, const N: usize>() -> Vec<T> {
+        let arr: [T; N] = kani::Arbitrary::any_array();
+        let mut v = Vec::from(arr);
+        let new_len: usize = kani::any();
+        kani::assume(new_len <= v.len());
+        v.truncate(new_len);
+        v
+    }
+
+    macro_rules! check_extract_if_with_ty {
+        ($mod_name:ident, $ty:ty) => {
+            mod $mod_name {
+                use super::*;
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_extract_if_next() {
+                    let mut v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let orig_len = v.len();
+                    let mut extracted = 0usize;
+                    {
+                        let mut iter = v.extract_if(.., |_| {
+                            let keep: bool = kani::any();
+                            keep
+                        });
+                        while let Some(_) = iter.next() {
+                            extracted += 1;
+                        }
+                    }
+                    assert!(v.len() + extracted == orig_len);
+                }
+            }
+        };
+    }
+
+    check_extract_if_with_ty!(verify_extract_if_u8, u8);
+    check_extract_if_with_ty!(verify_extract_if_unit, ());
+    check_extract_if_with_ty!(verify_extract_if_char, char);
+    check_extract_if_with_ty!(verify_extract_if_tup, (char, u8));
+}

library/alloc/src/vec/into_iter.rs

@@ -541,3 +541,203 @@ unsafe impl<T> AsVecIntoIter for IntoIter<T> {
         self
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use core::kani;
+
+    use crate::vec::Vec;
+
+    const MAX_LEN: usize = 3;
+
+    fn any_vec<T: kani::Arbitrary, const N: usize>() -> Vec<T> {
+        let arr: [T; N] = kani::Arbitrary::any_array();
+        let mut v = Vec::from(arr);
+        let new_len: usize = kani::any();
+        kani::assume(new_len <= v.len());
+        v.truncate(new_len);
+        v
+    }
+
+    macro_rules! check_into_iter_with_ty {
+        ($mod_name:ident, $ty:ty) => {
+            mod $mod_name {
+                use super::*;
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_as_slice() {
+                    let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let orig_len = v.len();
+                    let iter = v.into_iter();
+                    let s = iter.as_slice();
+                    assert!(s.len() == orig_len);
+                }
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_as_mut_slice() {
+                    let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let orig_len = v.len();
+                    let mut iter = v.into_iter();
+                    let s = iter.as_mut_slice();
+                    assert!(s.len() == orig_len);
+                }
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_next() {
+                    let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let orig_len = v.len();
+                    let mut iter = v.into_iter();
+                    if orig_len > 0 {
+                        assert!(iter.next().is_some());
+                        assert!(iter.len() == orig_len - 1);
+                    } else {
+                        assert!(iter.next().is_none());
+                    }
+                }
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_size_hint() {
+                    let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let orig_len = v.len();
+                    let iter = v.into_iter();
+                    let (lo, hi) = iter.size_hint();
+                    assert!(lo == orig_len);
+                    assert!(hi == Some(orig_len));
+                }
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_advance_by() {
+                    let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let orig_len = v.len();
+                    let mut iter = v.into_iter();
+                    let n: usize = kani::any();
+                    kani::assume(n <= MAX_LEN + 1);
+                    let result = iter.advance_by(n);
+                    if n <= orig_len {
+                        assert!(result.is_ok());
+                        assert!(iter.len() == orig_len - n);
+                    } else {
+                        assert!(result.is_err());
+                    }
+                }
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_next_chunk() {
+                    let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let orig_len = v.len();
+                    let mut iter = v.into_iter();
+                    let result = iter.next_chunk::<2>();
+                    if orig_len >= 2 {
+                        assert!(result.is_ok());
+                        assert!(iter.len() == orig_len - 2);
+                    } else {
+                        assert!(result.is_err());
+                    }
+                }
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_fold() {
+                    let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let orig_len = v.len();
+                    let iter = v.into_iter();
+                    let count = iter.fold(0usize, |acc, _| acc + 1);
+                    assert!(count == orig_len);
+                }
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_try_fold() {
+                    let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let orig_len = v.len();
+                    let mut iter = v.into_iter();
+                    let result: Result<usize, ()> = iter.try_fold(0usize, |acc, _| Ok(acc + 1));
+                    assert!(result == Ok(orig_len));
+                }
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_get_unchecked() {
+                    let v: Vec<u8> = any_vec::<u8, MAX_LEN>();
+                    let orig_len = v.len();
+                    kani::assume(orig_len > 0);
+                    let mut iter = v.into_iter();
+                    let i: usize = kani::any();
+                    kani::assume(i < orig_len);
+                    // SAFETY: i < len, and u8: Copy satisfies NonDrop
+                    let _val: u8 = unsafe { iter.__iterator_get_unchecked(i) };
+                }
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_next_back() {
+                    let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let orig_len = v.len();
+                    let mut iter = v.into_iter();
+                    if orig_len > 0 {
+                        assert!(iter.next_back().is_some());
+                        assert!(iter.len() == orig_len - 1);
+                    } else {
+                        assert!(iter.next_back().is_none());
+                    }
+                }
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_advance_back_by() {
+                    let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let orig_len = v.len();
+                    let mut iter = v.into_iter();
+                    let n: usize = kani::any();
+                    kani::assume(n <= MAX_LEN + 1);
+                    let result = iter.advance_back_by(n);
+                    if n <= orig_len {
+                        assert!(result.is_ok());
+                        assert!(iter.len() == orig_len - n);
+                    } else {
+                        assert!(result.is_err());
+                    }
+                }
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_drop() {
+                    let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let iter = v.into_iter();
+                    drop(iter);
+                }
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_forget_allocation_drop_remaining() {
+                    let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let mut iter = v.into_iter();
+                    iter.forget_allocation_drop_remaining();
+                    assert!(iter.len() == 0);
+                }
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_into_vecdeque() {
+                    let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let orig_len = v.len();
+                    let iter = v.into_iter();
+                    let vd = iter.into_vecdeque();
+                    assert!(vd.len() == orig_len);
+                }
+            }
+        };
+    }
+
+    check_into_iter_with_ty!(verify_into_iter_u8, u8);
+    check_into_iter_with_ty!(verify_into_iter_unit, ());
+    check_into_iter_with_ty!(verify_into_iter_char, char);
+    check_into_iter_with_ty!(verify_into_iter_tup, (char, u8));
+}

library/alloc/src/vec/spec_extend.rs

@@ -55,3 +55,77 @@ where
         unsafe { self.append_elements(slice) };
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use core::kani;
+
+    use super::*;
+
+    const MAX_LEN: usize = 3;
+
+    fn any_vec<T: kani::Arbitrary, const N: usize>() -> Vec<T> {
+        let arr: [T; N] = kani::Arbitrary::any_array();
+        let mut v = Vec::from(arr);
+        let new_len: usize = kani::any();
+        kani::assume(new_len <= v.len());
+        v.truncate(new_len);
+        v
+    }
+
+    macro_rules! check_spec_extend_with_ty {
+        ($mod_name:ident, $ty:ty) => {
+            mod $mod_name {
+                use super::*;
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_spec_extend_into_iter() {
+                    let mut dest: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let src: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let dest_len = dest.len();
+                    let src_len = src.len();
+                    let src_iter = src.into_iter();
+                    <Vec<$ty> as SpecExtend<$ty, IntoIter<$ty>>>::spec_extend(&mut dest, src_iter);
+                    assert!(dest.len() == dest_len + src_len);
+                }
+            }
+        };
+    }
+
+    // spec_extend for slice::Iter requires T: Copy, so only verify for Copy types
+    macro_rules! check_spec_extend_slice_iter_with_ty {
+        ($mod_name:ident, $ty:ty) => {
+            mod $mod_name {
+                use super::*;
+
+                #[kani::proof]
+                #[kani::unwind(8)]
+                fn check_spec_extend_slice_iter() {
+                    let mut dest: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let src: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
+                    let dest_len = dest.len();
+                    let src_len = src.len();
+                    let src_slice = src.as_slice();
+                    <Vec<$ty> as SpecExtend<&$ty, slice::Iter<'_, $ty>>>::spec_extend(
+                        &mut dest,
+                        src_slice.iter(),
+                    );
+                    assert!(dest.len() == dest_len + src_len);
+                }
+            }
+        };
+    }
+
+    check_spec_extend_with_ty!(verify_spec_extend_u8, u8);
+    check_spec_extend_with_ty!(verify_spec_extend_unit, ());
+    check_spec_extend_with_ty!(verify_spec_extend_char, char);
+    check_spec_extend_with_ty!(verify_spec_extend_tup, (char, u8));
+
+    // slice::Iter specialization requires T: Copy
+    check_spec_extend_slice_iter_with_ty!(verify_spec_extend_slice_u8, u8);
+    check_spec_extend_slice_iter_with_ty!(verify_spec_extend_slice_unit, ());
+    check_spec_extend_slice_iter_with_ty!(verify_spec_extend_slice_char, char);
+    check_spec_extend_slice_iter_with_ty!(verify_spec_extend_slice_tup, (char, u8));
+}

library/alloc/src/vec/spec_from_elem.rs

@@ -73,3 +73,43 @@ impl SpecFromElem for () {
         v
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use core::kani;
+
+    use super::*;
+
+    #[kani::proof]
+    fn check_from_elem_i8() {
+        let elem: i8 = kani::any();
+        let n: usize = kani::any();
+        kani::assume(n <= 3);
+        let v = <i8 as SpecFromElem>::from_elem(elem, n, crate::alloc::Global);
+        assert!(v.len() == n);
+        let k: usize = kani::any();
+        kani::assume(k < n);
+        assert!(v[k] == elem);
+    }
+
+    #[kani::proof]
+    fn check_from_elem_u8() {
+        let elem: u8 = kani::any();
+        let n: usize = kani::any();
+        kani::assume(n <= 3);
+        let v = <u8 as SpecFromElem>::from_elem(elem, n, crate::alloc::Global);
+        assert!(v.len() == n);
+        let k: usize = kani::any();
+        kani::assume(k < n);
+        assert!(v[k] == elem);
+    }
+
+    #[kani::proof]
+    fn check_from_elem_unit() {
+        let n: usize = kani::any();
+        kani::assume(n <= 3);
+        let v = <() as SpecFromElem>::from_elem((), n, crate::alloc::Global);
+        assert!(v.len() == n);
+    }
+}