From 44af7e17b92267b5a6805e88501baacee8765101 Mon Sep 17 00:00:00 2001 From: v3risec Date: Thu, 11 Jun 2026 16:12:22 +0800 Subject: [PATCH] Verify Vec iterator functions for challenge 24 --- library/Cargo.lock | 90 +++ library/alloc/src/lib.rs | 1 + library/alloc/src/vec/extract_if.rs | 99 ++- library/alloc/src/vec/into_iter.rs | 707 +++++++++++++++++- library/alloc/src/vec/mod.rs | 211 ++++++ library/alloc/src/vec/spec_extend.rs | 85 +++ library/alloc/src/vec/spec_from_elem.rs | 44 ++ library/alloc/src/vec/spec_from_iter.rs | 44 ++ .../alloc/src/vec/spec_from_iter_nested.rs | 41 + 9 files changed, 1315 insertions(+), 7 deletions(-) diff --git a/library/Cargo.lock b/library/Cargo.lock index 47fbf5169f491..4689c78a98f7d 100644 --- a/library/Cargo.lock +++ b/library/Cargo.lock @@ -28,6 +28,7 @@ version = "0.0.0" dependencies = [ "compiler_builtins", "core", + "safety", ] [[package]] @@ -67,6 +68,9 @@ dependencies = [ [[package]] name = "core" version = "0.0.0" +dependencies = [ + "safety", +] [[package]] name = "coretests" @@ -196,6 +200,39 @@ dependencies = [ "unwind", ] +[[package]] +name = "proc-macro-error" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" +dependencies = [ + "proc-macro-error-attr", + "proc-macro2", + "quote", + "syn 1.0.109", + "version_check", +] + +[[package]] +name = "proc-macro-error-attr" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" +dependencies = [ + "proc-macro2", + "quote", + "version_check", +] + +[[package]] +name = "proc-macro2" +version = "1.0.106" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934" +dependencies = [ + "unicode-ident", +] + [[package]] name = "proc_macro" version = "0.0.0" @@ -212,6 +249,15 @@ dependencies = [ "cc", ] +[[package]] +name = "quote" +version = "1.0.45" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924" +dependencies = [ + "proc-macro2", +] + [[package]] name = "r-efi" version = "5.3.0" @@ -296,6 +342,16 @@ dependencies = [ "std", ] +[[package]] +name = "safety" +version = "0.1.0" +dependencies = [ + "proc-macro-error", + "proc-macro2", + "quote", + "syn 2.0.117", +] + [[package]] name = "shlex" version = "1.3.0" @@ -324,6 +380,7 @@ dependencies = [ "rand", "rand_xorshift", "rustc-demangle", + "safety", "std_detect", "unwind", "vex-sdk", @@ -341,6 +398,27 @@ dependencies = [ "rustc-std-workspace-core", ] +[[package]] +name = "syn" +version = "1.0.109" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" +dependencies = [ + "proc-macro2", + "unicode-ident", +] + +[[package]] +name = "syn" +version = "2.0.117" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + [[package]] name = "sysroot" version = "0.0.0" @@ -361,6 +439,12 @@ dependencies = [ "std", ] +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + [[package]] name = "unwind" version = "0.0.0" @@ -380,6 +464,12 @@ dependencies = [ "rustc-std-workspace-core", ] +[[package]] +name = "version_check" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" + [[package]] name = "vex-sdk" version = "0.27.0" diff --git a/library/alloc/src/lib.rs b/library/alloc/src/lib.rs index 11abf49c8b391..1ab7d26c83ca9 100644 --- a/library/alloc/src/lib.rs +++ b/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)] diff --git a/library/alloc/src/vec/extract_if.rs b/library/alloc/src/vec/extract_if.rs index cb9e14f554d41..c438e580971c9 100644 --- a/library/alloc/src/vec/extract_if.rs +++ b/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 { + #[cfg(kani)] + let is_zst = core::mem::size_of::() == 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::(), 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::(), 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::()); + // 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]); +} diff --git a/library/alloc/src/vec/into_iter.rs b/library/alloc/src/vec/into_iter.rs index 35ff96027d804..2775010bcf7de 100644 --- a/library/alloc/src/vec/into_iter.rs +++ b/library/alloc/src/vec/into_iter.rs @@ -309,23 +309,99 @@ impl Iterator for IntoIter { F: FnMut(B, Self::Item) -> B, { if T::IS_ZST { - while self.ptr.as_ptr() != self.end.cast_mut() { + #[cfg(kani)] + let fold_ptr = self.ptr.as_ptr(); + #[cfg(kani)] + let fold_ptr_is_aligned = fold_ptr.is_aligned(); + #[cfg(kani)] + let mut remaining = self.end.addr().wrapping_sub(fold_ptr.addr()); + #[cfg(kani)] + let initial_remaining = remaining; + + #[cfg_attr(kani, kani::loop_invariant( + remaining <= initial_remaining + && (remaining == 0) == (fold_ptr == self.end.cast_mut()) + && fold_ptr_is_aligned + ))] + #[cfg_attr(kani, kani::loop_modifies(&self.end, &remaining))] + while { + #[cfg(kani)] + { + fold_ptr != self.end.cast_mut() + } + #[cfg(not(kani))] + { + self.ptr.as_ptr() != self.end.cast_mut() + } + } { + #[cfg(kani)] + kani::assume(remaining > 0); // SAFETY: we just checked that `self.ptr` is in bounds. + #[cfg(kani)] + let tmp = unsafe { fold_ptr.read() }; + #[cfg(not(kani))] let tmp = unsafe { self.ptr.read() }; // See `next` for why we subtract from `end` here. self.end = self.end.wrapping_byte_sub(1); + #[cfg(kani)] + { + remaining -= 1; + kani::assume((remaining == 0) == (fold_ptr == self.end.cast_mut())); + } accum = f(accum, tmp); } } else { + #[cfg(kani)] + let base_ptr = self.ptr.as_ptr(); + #[cfg(kani)] + let mut remaining = self.size_hint().0; + #[cfg(kani)] + let initial_remaining = remaining; + #[cfg(kani)] + let initial_items = ptr::slice_from_raw_parts(base_ptr as *const T, initial_remaining); + #[cfg(kani)] + kani::assume(kani::mem::can_dereference(initial_items)); + + #[cfg_attr(kani, kani::loop_invariant(remaining <= initial_remaining))] + #[cfg_attr(kani, kani::loop_modifies(&accum, &remaining))] // SAFETY: `self.end` can only be null if `T` is a ZST. - while self.ptr != non_null!(self.end, T) { + while { + #[cfg(kani)] + { + remaining > 0 + } + #[cfg(not(kani))] + { + self.ptr != non_null!(self.end, T) + } + } { + #[cfg(kani)] + let cur = unsafe { base_ptr.add(initial_remaining - remaining) }; + #[cfg(kani)] + kani::assume(kani::mem::can_dereference(cur as *const T)); // SAFETY: we just checked that `self.ptr` is in bounds. + #[cfg(kani)] + let tmp = unsafe { cur.read() }; + #[cfg(not(kani))] let tmp = unsafe { self.ptr.read() }; // SAFETY: the maximum this can be is `self.end`. // Increment `self.ptr` first to avoid double dropping in the event of a panic. - self.ptr = unsafe { self.ptr.add(1) }; + #[cfg(not(kani))] + { + self.ptr = unsafe { self.ptr.add(1) }; + } + #[cfg(kani)] + { + remaining -= 1; + } accum = f(accum, tmp); } + #[cfg(kani)] + { + let fold_end = self.end.cast_mut(); + kani::assume(!fold_end.is_null()); + self.ptr = unsafe { NonNull::new_unchecked(fold_end) }; + } } accum } @@ -337,23 +413,108 @@ impl Iterator for IntoIter { R: core::ops::Try, { if T::IS_ZST { - while self.ptr.as_ptr() != self.end.cast_mut() { + #[cfg(kani)] + let try_fold_ptr = self.ptr.as_ptr(); + #[cfg(kani)] + let try_fold_ptr_addr = try_fold_ptr.addr(); + #[cfg(kani)] + let try_fold_ptr_is_aligned = try_fold_ptr.is_aligned(); + #[cfg(kani)] + let mut remaining = self.end.addr().wrapping_sub(try_fold_ptr_addr); + #[cfg(kani)] + let initial_remaining = remaining; + + #[cfg_attr(kani, kani::loop_invariant( + remaining <= initial_remaining + && (remaining == 0) == (try_fold_ptr_addr == self.end.addr()) + && try_fold_ptr_is_aligned + ))] + #[cfg_attr(kani, kani::loop_modifies(&self.end, &remaining))] + while { + #[cfg(kani)] + { + try_fold_ptr_addr != self.end.addr() + } + #[cfg(not(kani))] + { + self.ptr.as_ptr() != self.end.cast_mut() + } + } { + #[cfg(kani)] + kani::assume(remaining > 0); // SAFETY: we just checked that `self.ptr` is in bounds. + #[cfg(kani)] + let tmp = unsafe { try_fold_ptr.read() }; + #[cfg(not(kani))] let tmp = unsafe { self.ptr.read() }; // See `next` for why we subtract from `end` here. self.end = self.end.wrapping_byte_sub(1); + #[cfg(kani)] + { + remaining -= 1; + kani::assume((remaining == 0) == (try_fold_ptr_addr == self.end.addr())); + } accum = f(accum, tmp)?; } } else { + #[cfg(kani)] + let base_ptr = self.ptr.as_ptr(); + #[cfg(kani)] + let initial_remaining = self.size_hint().0; + #[cfg(kani)] + let mut processed = 0usize; + #[cfg(kani)] + let initial_items = ptr::slice_from_raw_parts(base_ptr as *const T, initial_remaining); + #[cfg(kani)] + kani::assume(kani::mem::can_dereference(initial_items)); + #[cfg(kani)] + let self_ptr_slot = (&raw mut self.ptr).cast::<*mut T>(); + #[cfg(kani)] + kani::assume(kani::mem::can_write(self_ptr_slot)); + + #[cfg_attr(kani, kani::loop_invariant(processed <= initial_remaining))] + #[cfg_attr(kani, kani::loop_modifies(self_ptr_slot, &accum, &processed))] // SAFETY: `self.end` can only be null if `T` is a ZST. - while self.ptr != non_null!(self.end, T) { + while { + #[cfg(kani)] + { + processed < initial_remaining + } + #[cfg(not(kani))] + { + self.ptr != non_null!(self.end, T) + } + } { + #[cfg(kani)] + let cur = unsafe { base_ptr.add(processed) }; + #[cfg(kani)] + kani::assume(kani::mem::can_dereference(cur as *const T)); // SAFETY: we just checked that `self.ptr` is in bounds. + #[cfg(kani)] + let tmp = unsafe { cur.read() }; + #[cfg(not(kani))] let tmp = unsafe { self.ptr.read() }; // SAFETY: the maximum this can be is `self.end`. // Increment `self.ptr` first to avoid double dropping in the event of a panic. - self.ptr = unsafe { self.ptr.add(1) }; + #[cfg(not(kani))] + { + self.ptr = unsafe { self.ptr.add(1) }; + } + #[cfg(kani)] + { + let next = unsafe { cur.add(1) }; + kani::assume(!next.is_null()); + unsafe { *self_ptr_slot = next }; + processed += 1; + } accum = f(accum, tmp)?; } + #[cfg(kani)] + { + let try_fold_end = self.end.cast_mut(); + kani::assume(!try_fold_end.is_null()); + unsafe { *self_ptr_slot = try_fold_end }; + } } R::from_output(accum) } @@ -541,3 +702,537 @@ unsafe impl AsVecIntoIter for IntoIter { self } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::super::Vec; + use super::super::kani_vec_harness_helpers::*; + use super::*; + + // Harnesses for IntoIter::as_slice() + macro_rules! gen_into_iter_as_slice_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a non-deterministic Vec for the target element type + let vec = verifier_nondet_vec::<$ty>(); + // Convert the Vec into its owning iterator + let iter = vec.into_iter(); + // Borrow the remaining iterator elements as an immutable slice + let _: &[$ty] = iter.as_slice(); + } + }; + } + + gen_into_iter_as_slice_harness!(harness_into_iter_as_slice_u8, u8); + gen_into_iter_as_slice_harness!(harness_into_iter_as_slice_u16, u16); + gen_into_iter_as_slice_harness!(harness_into_iter_as_slice_u32, u32); + gen_into_iter_as_slice_harness!(harness_into_iter_as_slice_u64, u64); + gen_into_iter_as_slice_harness!(harness_into_iter_as_slice_u128, u128); + gen_into_iter_as_slice_harness!(harness_into_iter_as_slice_usize, usize); + gen_into_iter_as_slice_harness!(harness_into_iter_as_slice_i8, i8); + gen_into_iter_as_slice_harness!(harness_into_iter_as_slice_i16, i16); + gen_into_iter_as_slice_harness!(harness_into_iter_as_slice_i32, i32); + gen_into_iter_as_slice_harness!(harness_into_iter_as_slice_i64, i64); + gen_into_iter_as_slice_harness!(harness_into_iter_as_slice_i128, i128); + gen_into_iter_as_slice_harness!(harness_into_iter_as_slice_isize, isize); + gen_into_iter_as_slice_harness!(harness_into_iter_as_slice_unit, ()); + gen_into_iter_as_slice_harness!(harness_into_iter_as_slice_array, [u8; 4]); + + // Harnesses for IntoIter::as_mut_slice() + macro_rules! gen_into_iter_as_mut_slice_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a non-deterministic Vec for the target element type + let vec = verifier_nondet_vec::<$ty>(); + // Convert the Vec into its owning iterator + let mut iter = vec.into_iter(); + // Borrow the remaining iterator elements as a mutable slice + let _: &mut [$ty] = iter.as_mut_slice(); + } + }; + } + + gen_into_iter_as_mut_slice_harness!(harness_into_iter_as_mut_slice_u8, u8); + gen_into_iter_as_mut_slice_harness!(harness_into_iter_as_mut_slice_u16, u16); + gen_into_iter_as_mut_slice_harness!(harness_into_iter_as_mut_slice_u32, u32); + gen_into_iter_as_mut_slice_harness!(harness_into_iter_as_mut_slice_u64, u64); + gen_into_iter_as_mut_slice_harness!(harness_into_iter_as_mut_slice_u128, u128); + gen_into_iter_as_mut_slice_harness!(harness_into_iter_as_mut_slice_usize, usize); + gen_into_iter_as_mut_slice_harness!(harness_into_iter_as_mut_slice_i8, i8); + gen_into_iter_as_mut_slice_harness!(harness_into_iter_as_mut_slice_i16, i16); + gen_into_iter_as_mut_slice_harness!(harness_into_iter_as_mut_slice_i32, i32); + gen_into_iter_as_mut_slice_harness!(harness_into_iter_as_mut_slice_i64, i64); + gen_into_iter_as_mut_slice_harness!(harness_into_iter_as_mut_slice_i128, i128); + gen_into_iter_as_mut_slice_harness!(harness_into_iter_as_mut_slice_isize, isize); + gen_into_iter_as_mut_slice_harness!(harness_into_iter_as_mut_slice_unit, ()); + gen_into_iter_as_mut_slice_harness!(harness_into_iter_as_mut_slice_array, [u8; 4]); + + // Harnesses for IntoIter::forget_allocation_drop_remaining() + macro_rules! gen_into_iter_forget_allocation_drop_remaining_harness { + ($name:ident, $ty:ty) => { + #[cfg(not(no_global_oom_handling))] + #[kani::proof] + pub fn $name() { + // Create a non-deterministic Vec for the target element type + let vec = verifier_nondet_vec::<$ty>(); + // Convert the Vec into its owning iterator + let mut iter = vec.into_iter(); + // Drop the remaining elements and forget the backing allocation + iter.forget_allocation_drop_remaining(); + } + }; + } + + gen_into_iter_forget_allocation_drop_remaining_harness!( + harness_into_iter_forget_allocation_drop_remaining_u8, + u8 + ); + gen_into_iter_forget_allocation_drop_remaining_harness!( + harness_into_iter_forget_allocation_drop_remaining_u16, + u16 + ); + gen_into_iter_forget_allocation_drop_remaining_harness!( + harness_into_iter_forget_allocation_drop_remaining_u32, + u32 + ); + gen_into_iter_forget_allocation_drop_remaining_harness!( + harness_into_iter_forget_allocation_drop_remaining_u64, + u64 + ); + gen_into_iter_forget_allocation_drop_remaining_harness!( + harness_into_iter_forget_allocation_drop_remaining_u128, + u128 + ); + gen_into_iter_forget_allocation_drop_remaining_harness!( + harness_into_iter_forget_allocation_drop_remaining_usize, + usize + ); + gen_into_iter_forget_allocation_drop_remaining_harness!( + harness_into_iter_forget_allocation_drop_remaining_i8, + i8 + ); + gen_into_iter_forget_allocation_drop_remaining_harness!( + harness_into_iter_forget_allocation_drop_remaining_i16, + i16 + ); + gen_into_iter_forget_allocation_drop_remaining_harness!( + harness_into_iter_forget_allocation_drop_remaining_i32, + i32 + ); + gen_into_iter_forget_allocation_drop_remaining_harness!( + harness_into_iter_forget_allocation_drop_remaining_i64, + i64 + ); + gen_into_iter_forget_allocation_drop_remaining_harness!( + harness_into_iter_forget_allocation_drop_remaining_i128, + i128 + ); + gen_into_iter_forget_allocation_drop_remaining_harness!( + harness_into_iter_forget_allocation_drop_remaining_isize, + isize + ); + gen_into_iter_forget_allocation_drop_remaining_harness!( + harness_into_iter_forget_allocation_drop_remaining_unit, + () + ); + gen_into_iter_forget_allocation_drop_remaining_harness!( + harness_into_iter_forget_allocation_drop_remaining_array, + [u8; 4] + ); + + // Harnesses for IntoIter::into_vecdeque() + macro_rules! gen_into_iter_into_vecdeque_harness { + ($name:ident, $ty:ty) => { + #[cfg(not(no_global_oom_handling))] + #[kani::proof] + pub fn $name() { + // Create a non-deterministic Vec for the target element type + let vec = verifier_nondet_vec::<$ty>(); + // Convert the Vec into its owning iterator + let mut iter = vec.into_iter(); + // Repackage the remaining iterator range as a VecDeque + let _ = iter.into_vecdeque(); + } + }; + } + + gen_into_iter_into_vecdeque_harness!(harness_into_iter_into_vecdeque_u8, u8); + gen_into_iter_into_vecdeque_harness!(harness_into_iter_into_vecdeque_u16, u16); + gen_into_iter_into_vecdeque_harness!(harness_into_iter_into_vecdeque_u32, u32); + gen_into_iter_into_vecdeque_harness!(harness_into_iter_into_vecdeque_u64, u64); + gen_into_iter_into_vecdeque_harness!(harness_into_iter_into_vecdeque_u128, u128); + gen_into_iter_into_vecdeque_harness!(harness_into_iter_into_vecdeque_usize, usize); + gen_into_iter_into_vecdeque_harness!(harness_into_iter_into_vecdeque_i8, i8); + gen_into_iter_into_vecdeque_harness!(harness_into_iter_into_vecdeque_i16, i16); + gen_into_iter_into_vecdeque_harness!(harness_into_iter_into_vecdeque_i32, i32); + gen_into_iter_into_vecdeque_harness!(harness_into_iter_into_vecdeque_i64, i64); + gen_into_iter_into_vecdeque_harness!(harness_into_iter_into_vecdeque_i128, i128); + gen_into_iter_into_vecdeque_harness!(harness_into_iter_into_vecdeque_isize, isize); + gen_into_iter_into_vecdeque_harness!(harness_into_iter_into_vecdeque_unit, ()); + gen_into_iter_into_vecdeque_harness!(harness_into_iter_into_vecdeque_array, [u8; 4]); + + // Harnesses for IntoIter::next() + macro_rules! gen_into_iter_next_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a non-deterministic Vec for the target element type + let vec = verifier_nondet_vec::<$ty>(); + // Convert the Vec into its owning iterator + let mut iter = vec.into_iter(); + // Advance the iterator from the front by one element if possible + let _ = iter.next(); + } + }; + } + + gen_into_iter_next_harness!(harness_into_iter_next_u8, u8); + gen_into_iter_next_harness!(harness_into_iter_next_u16, u16); + gen_into_iter_next_harness!(harness_into_iter_next_u32, u32); + gen_into_iter_next_harness!(harness_into_iter_next_u64, u64); + gen_into_iter_next_harness!(harness_into_iter_next_u128, u128); + gen_into_iter_next_harness!(harness_into_iter_next_usize, usize); + gen_into_iter_next_harness!(harness_into_iter_next_i8, i8); + gen_into_iter_next_harness!(harness_into_iter_next_i16, i16); + gen_into_iter_next_harness!(harness_into_iter_next_i32, i32); + gen_into_iter_next_harness!(harness_into_iter_next_i64, i64); + gen_into_iter_next_harness!(harness_into_iter_next_i128, i128); + gen_into_iter_next_harness!(harness_into_iter_next_isize, isize); + gen_into_iter_next_harness!(harness_into_iter_next_unit, ()); + gen_into_iter_next_harness!(harness_into_iter_next_array, [u8; 4]); + + // Harnesses for IntoIter::size_hint() + macro_rules! gen_into_iter_size_hint_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a non-deterministic Vec for the target element type + let vec = verifier_nondet_vec::<$ty>(); + // Convert the Vec into its owning iterator + let iter = vec.into_iter(); + // Query the exact remaining iterator length + let _ = iter.size_hint(); + } + }; + } + + gen_into_iter_size_hint_harness!(harness_into_iter_size_hint_u8, u8); + gen_into_iter_size_hint_harness!(harness_into_iter_size_hint_u16, u16); + gen_into_iter_size_hint_harness!(harness_into_iter_size_hint_u32, u32); + gen_into_iter_size_hint_harness!(harness_into_iter_size_hint_u64, u64); + gen_into_iter_size_hint_harness!(harness_into_iter_size_hint_u128, u128); + gen_into_iter_size_hint_harness!(harness_into_iter_size_hint_usize, usize); + gen_into_iter_size_hint_harness!(harness_into_iter_size_hint_i8, i8); + gen_into_iter_size_hint_harness!(harness_into_iter_size_hint_i16, i16); + gen_into_iter_size_hint_harness!(harness_into_iter_size_hint_i32, i32); + gen_into_iter_size_hint_harness!(harness_into_iter_size_hint_i64, i64); + gen_into_iter_size_hint_harness!(harness_into_iter_size_hint_i128, i128); + gen_into_iter_size_hint_harness!(harness_into_iter_size_hint_isize, isize); + gen_into_iter_size_hint_harness!(harness_into_iter_size_hint_unit, ()); + gen_into_iter_size_hint_harness!(harness_into_iter_size_hint_array, [u8; 4]); + + // Harnesses for IntoIter::advance_by() + macro_rules! gen_into_iter_advance_by_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a non-deterministic Vec for the target element type + let vec = verifier_nondet_vec::<$ty>(); + // Convert the Vec into its owning iterator + let mut iter = vec.into_iter(); + // Choose a non-deterministic number of front elements to skip + let n: usize = kani::any(); + // Advance the iterator from the front by the selected count + let _ = iter.advance_by(n); + } + }; + } + + gen_into_iter_advance_by_harness!(harness_into_iter_advance_by_u8, u8); + gen_into_iter_advance_by_harness!(harness_into_iter_advance_by_u16, u16); + gen_into_iter_advance_by_harness!(harness_into_iter_advance_by_u32, u32); + gen_into_iter_advance_by_harness!(harness_into_iter_advance_by_u64, u64); + gen_into_iter_advance_by_harness!(harness_into_iter_advance_by_u128, u128); + gen_into_iter_advance_by_harness!(harness_into_iter_advance_by_usize, usize); + gen_into_iter_advance_by_harness!(harness_into_iter_advance_by_i8, i8); + gen_into_iter_advance_by_harness!(harness_into_iter_advance_by_i16, i16); + gen_into_iter_advance_by_harness!(harness_into_iter_advance_by_i32, i32); + gen_into_iter_advance_by_harness!(harness_into_iter_advance_by_i64, i64); + gen_into_iter_advance_by_harness!(harness_into_iter_advance_by_i128, i128); + gen_into_iter_advance_by_harness!(harness_into_iter_advance_by_isize, isize); + gen_into_iter_advance_by_harness!(harness_into_iter_advance_by_unit, ()); + gen_into_iter_advance_by_harness!(harness_into_iter_advance_by_array, [u8; 4]); + + // Harnesses for IntoIter::next_chunk() + macro_rules! gen_into_iter_next_chunk_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a non-deterministic Vec for the target element type + let vec = verifier_nondet_vec::<$ty>(); + // Convert the Vec into its owning iterator + let mut iter = vec.into_iter(); + // Try to collect the next fixed-size chunk from the iterator + let _ = iter.next_chunk::<4>(); + } + }; + } + + gen_into_iter_next_chunk_harness!(harness_into_iter_next_chunk_u8, u8); + gen_into_iter_next_chunk_harness!(harness_into_iter_next_chunk_u16, u16); + gen_into_iter_next_chunk_harness!(harness_into_iter_next_chunk_u32, u32); + gen_into_iter_next_chunk_harness!(harness_into_iter_next_chunk_u64, u64); + gen_into_iter_next_chunk_harness!(harness_into_iter_next_chunk_u128, u128); + gen_into_iter_next_chunk_harness!(harness_into_iter_next_chunk_usize, usize); + gen_into_iter_next_chunk_harness!(harness_into_iter_next_chunk_i8, i8); + gen_into_iter_next_chunk_harness!(harness_into_iter_next_chunk_i16, i16); + gen_into_iter_next_chunk_harness!(harness_into_iter_next_chunk_i32, i32); + gen_into_iter_next_chunk_harness!(harness_into_iter_next_chunk_i64, i64); + gen_into_iter_next_chunk_harness!(harness_into_iter_next_chunk_i128, i128); + gen_into_iter_next_chunk_harness!(harness_into_iter_next_chunk_isize, isize); + gen_into_iter_next_chunk_harness!(harness_into_iter_next_chunk_unit, ()); + gen_into_iter_next_chunk_harness!(harness_into_iter_next_chunk_array, [u8; 4]); + + // Harnesses for IntoIter::fold() + macro_rules! gen_into_iter_fold_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a non-deterministic Vec for the target element type + let vec = verifier_nondet_vec::<$ty>(); + // Convert the Vec into its owning iterator + let iter = vec.into_iter(); + // Create a non-deterministic initial accumulator + let accum: $ty = kani::any(); + // Fold all remaining elements while preserving the accumulator + let _ = iter.fold(accum, |accum, _item| accum); + } + }; + } + + gen_into_iter_fold_harness!(harness_into_iter_fold_u8, u8); + gen_into_iter_fold_harness!(harness_into_iter_fold_u16, u16); + gen_into_iter_fold_harness!(harness_into_iter_fold_u32, u32); + gen_into_iter_fold_harness!(harness_into_iter_fold_u64, u64); + gen_into_iter_fold_harness!(harness_into_iter_fold_u128, u128); + gen_into_iter_fold_harness!(harness_into_iter_fold_usize, usize); + gen_into_iter_fold_harness!(harness_into_iter_fold_i8, i8); + gen_into_iter_fold_harness!(harness_into_iter_fold_i16, i16); + gen_into_iter_fold_harness!(harness_into_iter_fold_i32, i32); + gen_into_iter_fold_harness!(harness_into_iter_fold_i64, i64); + gen_into_iter_fold_harness!(harness_into_iter_fold_i128, i128); + gen_into_iter_fold_harness!(harness_into_iter_fold_isize, isize); + gen_into_iter_fold_harness!(harness_into_iter_fold_unit, ()); + gen_into_iter_fold_harness!(harness_into_iter_fold_array, [u8; 4]); + + // Harnesses for IntoIter::try_fold() + macro_rules! gen_into_iter_try_fold_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a non-deterministic Vec for the target element type + let vec = verifier_nondet_vec::<$ty>(); + // Convert the Vec into its owning iterator + let mut iter = vec.into_iter(); + // Create a non-deterministic initial accumulator + let accum: $ty = kani::any(); + // Try to fold all remaining elements, allowing early termination + let _: Result<$ty, ()> = + iter.try_fold( + accum, + |accum, _item| { + if kani::any::() { Ok(accum) } else { Err(()) } + }, + ); + } + }; + } + + gen_into_iter_try_fold_harness!(harness_into_iter_try_fold_u8, u8); + gen_into_iter_try_fold_harness!(harness_into_iter_try_fold_u16, u16); + gen_into_iter_try_fold_harness!(harness_into_iter_try_fold_u32, u32); + gen_into_iter_try_fold_harness!(harness_into_iter_try_fold_u64, u64); + gen_into_iter_try_fold_harness!(harness_into_iter_try_fold_u128, u128); + gen_into_iter_try_fold_harness!(harness_into_iter_try_fold_usize, usize); + gen_into_iter_try_fold_harness!(harness_into_iter_try_fold_i8, i8); + gen_into_iter_try_fold_harness!(harness_into_iter_try_fold_i16, i16); + gen_into_iter_try_fold_harness!(harness_into_iter_try_fold_i32, i32); + gen_into_iter_try_fold_harness!(harness_into_iter_try_fold_i64, i64); + gen_into_iter_try_fold_harness!(harness_into_iter_try_fold_i128, i128); + gen_into_iter_try_fold_harness!(harness_into_iter_try_fold_isize, isize); + gen_into_iter_try_fold_harness!(harness_into_iter_try_fold_unit, ()); + gen_into_iter_try_fold_harness!(harness_into_iter_try_fold_array, [u8; 4]); + + // Harnesses for IntoIter::__iterator_get_unchecked() + macro_rules! gen_into_iter_iterator_get_unchecked_harness { + ($name:ident, $ty:ty) => { + // `__iterator_get_unchecked` is an `Iterator` method implemented by + // the generic impl `impl Iterator for IntoIter`. + // Kani currently cannot resolve a `proof_for_contract` target such as + // ` as core::iter::Iterator>::__iterator_get_unchecked` + // back to that generic trait impl's concrete monomorphization. Use a + // plain proof and enforce the contract precondition in this harness. + // #[kani::proof_for_contract( + // as core::iter::Iterator>::__iterator_get_unchecked + // )] + #[kani::proof] + pub fn $name() { + // Create a non-deterministic Vec for the target element type + let vec = verifier_nondet_vec::<$ty>(); + // Convert the Vec into its owning iterator + let mut iter = vec.into_iter(); + // This is the safety precondition for `__iterator_get_unchecked`: + // the unchecked index must be within the iterator's remaining range. + let i = kani::any_where(|i: &usize| *i < iter.len()); + // Execute the unsafe implementation of `__iterator_get_unchecked` with the selected index + let _ = unsafe { iter.__iterator_get_unchecked(i) }; + } + }; + } + + gen_into_iter_iterator_get_unchecked_harness!(harness_into_iter_iterator_get_unchecked_u8, u8); + gen_into_iter_iterator_get_unchecked_harness!( + harness_into_iter_iterator_get_unchecked_u16, + u16 + ); + gen_into_iter_iterator_get_unchecked_harness!( + harness_into_iter_iterator_get_unchecked_u32, + u32 + ); + gen_into_iter_iterator_get_unchecked_harness!( + harness_into_iter_iterator_get_unchecked_u64, + u64 + ); + gen_into_iter_iterator_get_unchecked_harness!( + harness_into_iter_iterator_get_unchecked_u128, + u128 + ); + gen_into_iter_iterator_get_unchecked_harness!( + harness_into_iter_iterator_get_unchecked_usize, + usize + ); + gen_into_iter_iterator_get_unchecked_harness!(harness_into_iter_iterator_get_unchecked_i8, i8); + gen_into_iter_iterator_get_unchecked_harness!( + harness_into_iter_iterator_get_unchecked_i16, + i16 + ); + gen_into_iter_iterator_get_unchecked_harness!( + harness_into_iter_iterator_get_unchecked_i32, + i32 + ); + gen_into_iter_iterator_get_unchecked_harness!( + harness_into_iter_iterator_get_unchecked_i64, + i64 + ); + gen_into_iter_iterator_get_unchecked_harness!( + harness_into_iter_iterator_get_unchecked_i128, + i128 + ); + gen_into_iter_iterator_get_unchecked_harness!( + harness_into_iter_iterator_get_unchecked_isize, + isize + ); + gen_into_iter_iterator_get_unchecked_harness!( + harness_into_iter_iterator_get_unchecked_unit, + () + ); + gen_into_iter_iterator_get_unchecked_harness!( + harness_into_iter_iterator_get_unchecked_array, + [u8; 4] + ); + + // Harnesses for IntoIter::next_back() + macro_rules! gen_into_iter_next_back_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a non-deterministic Vec for the target element type + let vec = verifier_nondet_vec::<$ty>(); + // Convert the Vec into its owning iterator + let mut iter = vec.into_iter(); + // Advance the iterator from the back by one element if possible + let _ = iter.next_back(); + } + }; + } + + gen_into_iter_next_back_harness!(harness_into_iter_next_back_u8, u8); + gen_into_iter_next_back_harness!(harness_into_iter_next_back_u16, u16); + gen_into_iter_next_back_harness!(harness_into_iter_next_back_u32, u32); + gen_into_iter_next_back_harness!(harness_into_iter_next_back_u64, u64); + gen_into_iter_next_back_harness!(harness_into_iter_next_back_u128, u128); + gen_into_iter_next_back_harness!(harness_into_iter_next_back_usize, usize); + gen_into_iter_next_back_harness!(harness_into_iter_next_back_i8, i8); + gen_into_iter_next_back_harness!(harness_into_iter_next_back_i16, i16); + gen_into_iter_next_back_harness!(harness_into_iter_next_back_i32, i32); + gen_into_iter_next_back_harness!(harness_into_iter_next_back_i64, i64); + gen_into_iter_next_back_harness!(harness_into_iter_next_back_i128, i128); + gen_into_iter_next_back_harness!(harness_into_iter_next_back_isize, isize); + gen_into_iter_next_back_harness!(harness_into_iter_next_back_unit, ()); + gen_into_iter_next_back_harness!(harness_into_iter_next_back_array, [u8; 4]); + + // Harnesses for IntoIter::advance_back_by() + macro_rules! gen_into_iter_advance_back_by_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a non-deterministic Vec for the target element type + let vec = verifier_nondet_vec::<$ty>(); + // Convert the Vec into its owning iterator + let mut iter = vec.into_iter(); + // Choose a non-deterministic number of back elements to skip + let n: usize = kani::any(); + // Advance the iterator from the back by the selected count + let _ = iter.advance_back_by(n); + } + }; + } + + gen_into_iter_advance_back_by_harness!(harness_into_iter_advance_back_by_u8, u8); + gen_into_iter_advance_back_by_harness!(harness_into_iter_advance_back_by_u16, u16); + gen_into_iter_advance_back_by_harness!(harness_into_iter_advance_back_by_u32, u32); + gen_into_iter_advance_back_by_harness!(harness_into_iter_advance_back_by_u64, u64); + gen_into_iter_advance_back_by_harness!(harness_into_iter_advance_back_by_u128, u128); + gen_into_iter_advance_back_by_harness!(harness_into_iter_advance_back_by_usize, usize); + gen_into_iter_advance_back_by_harness!(harness_into_iter_advance_back_by_i8, i8); + gen_into_iter_advance_back_by_harness!(harness_into_iter_advance_back_by_i16, i16); + gen_into_iter_advance_back_by_harness!(harness_into_iter_advance_back_by_i32, i32); + gen_into_iter_advance_back_by_harness!(harness_into_iter_advance_back_by_i64, i64); + gen_into_iter_advance_back_by_harness!(harness_into_iter_advance_back_by_i128, i128); + gen_into_iter_advance_back_by_harness!(harness_into_iter_advance_back_by_isize, isize); + gen_into_iter_advance_back_by_harness!(harness_into_iter_advance_back_by_unit, ()); + gen_into_iter_advance_back_by_harness!(harness_into_iter_advance_back_by_array, [u8; 4]); + + // Harnesses for IntoIter::drop() + macro_rules! gen_into_iter_drop_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a non-deterministic Vec for the target element type + let vec = verifier_nondet_vec::<$ty>(); + // Convert the Vec into its owning iterator + let iter = vec.into_iter(); + // Drop the iterator and any remaining elements + drop(iter); + } + }; + } + + gen_into_iter_drop_harness!(harness_into_iter_drop_u8, u8); + gen_into_iter_drop_harness!(harness_into_iter_drop_u16, u16); + gen_into_iter_drop_harness!(harness_into_iter_drop_u32, u32); + gen_into_iter_drop_harness!(harness_into_iter_drop_u64, u64); + gen_into_iter_drop_harness!(harness_into_iter_drop_u128, u128); + gen_into_iter_drop_harness!(harness_into_iter_drop_usize, usize); + gen_into_iter_drop_harness!(harness_into_iter_drop_i8, i8); + gen_into_iter_drop_harness!(harness_into_iter_drop_i16, i16); + gen_into_iter_drop_harness!(harness_into_iter_drop_i32, i32); + gen_into_iter_drop_harness!(harness_into_iter_drop_i64, i64); + gen_into_iter_drop_harness!(harness_into_iter_drop_i128, i128); + gen_into_iter_drop_harness!(harness_into_iter_drop_isize, isize); + gen_into_iter_drop_harness!(harness_into_iter_drop_unit, ()); + gen_into_iter_drop_harness!(harness_into_iter_drop_array, [u8; 4]); +} diff --git a/library/alloc/src/vec/mod.rs b/library/alloc/src/vec/mod.rs index 78d2ef5412f9c..2249bbc94f901 100644 --- a/library/alloc/src/vec/mod.rs +++ b/library/alloc/src/vec/mod.rs @@ -79,6 +79,8 @@ use core::cmp::Ordering; use core::hash::{Hash, Hasher}; #[cfg(not(no_global_oom_handling))] use core::iter; +#[cfg(kani)] +use core::kani; use core::marker::PhantomData; use core::mem::{self, ManuallyDrop, MaybeUninit, SizedTypeProperties}; use core::ops::{self, Index, IndexMut, Range, RangeBounds}; @@ -3790,6 +3792,111 @@ impl Vec { // for item in iterator { // self.push(item); // } + #[cfg(kani)] + { + let original_len = self.len; + let mut written = 0usize; + let mut cur_len = self.len; + let cur_cap = self.capacity(); + let spare_capacity = cur_cap.saturating_sub(original_len); + let len_ptr = core::ptr::addr_of_mut!(self.len); + + kani::assume(original_len <= cur_cap); + kani::assume(kani::mem::can_write(len_ptr)); + + if mem::size_of::() == 0 { + let zst_ptr = self.as_mut_ptr(); + + #[kani::loop_invariant( + original_len <= cur_cap + && self.len == cur_len + && original_len <= cur_len + && cur_len <= cur_cap + && written <= spare_capacity + && cur_len == original_len + written + && kani::mem::can_write(len_ptr) + )] + #[kani::loop_modifies(&iterator, &written, &cur_len, len_ptr)] + loop { + let Some(element) = iterator.next() else { + break; + }; + let len = self.len(); + kani::assume(len == cur_len); + kani::assume(written < spare_capacity); + kani::assume(len < cur_cap); + if len == cur_cap { + kani::assume(false); + } + let new_len = len + 1; + + unsafe { + ptr::write(zst_ptr, element); + // Since next() executes user code which can panic we have to bump the + // length after each step. + // NB can't overflow since we would have had to alloc the address space + self.set_len(new_len); + } + + cur_len = new_len; + if let Some(next_written) = written.checked_add(1) { + written = next_written; + } else { + kani::assume(false); + } + } + } else { + let spare_ptr = unsafe { self.as_mut_ptr().add(original_len) }; + let spare_write_set = + core::ptr::slice_from_raw_parts_mut(spare_ptr, spare_capacity); + kani::assume(kani::mem::can_write(spare_write_set)); + + #[kani::loop_invariant( + original_len <= cur_cap + && self.len == cur_len + && original_len <= cur_len + && cur_len <= cur_cap + && written <= spare_capacity + && cur_len == original_len + written + && kani::mem::can_write(len_ptr) + && kani::mem::can_write(spare_write_set) + )] + #[kani::loop_modifies(&iterator, &written, &cur_len, len_ptr, spare_write_set)] + loop { + let Some(element) = iterator.next() else { + break; + }; + let len = self.len(); + kani::assume(len == cur_len); + kani::assume(written < spare_capacity); + kani::assume(len < cur_cap); + if len == cur_cap { + kani::assume(false); + } + let new_len = len + 1; + + unsafe { + let dst = spare_ptr.add(written); + ptr::write(dst, element); + // Since next() executes user code which can panic we have to bump the + // length after each step. + // NB can't overflow since we would have had to alloc the address space + self.set_len(new_len); + } + + cur_len = new_len; + if let Some(next_written) = written.checked_add(1) { + written = next_written; + } else { + kani::assume(false); + } + } + } + + return; + } + + #[cfg(not(kani))] while let Some(element) = iterator.next() { let len = self.len(); if len == self.capacity() { @@ -4351,3 +4458,107 @@ mod verify { } } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod kani_vec_harness_helpers { + use core::alloc::Layout; + use core::{mem, ptr}; + + use super::{Vec, *}; + + pub(super) fn verifier_nondet_vec() -> Vec { + if mem::size_of::() == 0 { + let mut v = Vec::::new(); + unsafe { + let sz: usize = kani::any(); + v.set_len(sz); + } + return v; + } + + let cap: usize = kani::any(); + let elem_layout = Layout::new::(); + kani::assume(elem_layout.repeat(cap).is_ok()); + let mut v = Vec::::with_capacity(cap); + unsafe { + let sz: usize = kani::any(); + kani::assume(sz <= cap); + v.set_len(sz); + + ptr::write_bytes( + v.as_mut_ptr().cast::(), + kani::any::(), + mem::size_of::() * sz, + ); + } + v + } + + const MAX_VEC_LEN: usize = 4; + + pub(super) fn verifier_nondet_bounded_vec() -> Vec + where + T: kani::Arbitrary, + { + let values: [T; MAX_VEC_LEN] = kani::any(); + let len = kani::any_where(|len: &usize| *len <= MAX_VEC_LEN); + let mut vec = Vec::from(values); + vec.truncate(len); + vec + } + + // Constrain states so that `reserve(additional)` cannot fail with `CapacityOverflow`. + pub(super) fn assume_reserve_no_capacity_overflow( + len: usize, + cap: usize, + additional: usize, + ) { + // Keep the symbolic Vec state within the core Vec invariant. + kani::assume(len <= cap); + + // Compute the currently available spare capacity. + let spare = cap - len; + + // Return when `reserve` can finish without growing the allocation. + if additional <= spare { + return; + } + + // Read the element size once to mirror RawVec growth decisions. + let elem_size = mem::size_of::(); + + // Reject ZST states that would require growing past `usize::MAX` logical capacity. + if elem_size == 0 { + kani::assume(false); + return; + } + + // Require the post-reserve length to fit in `usize`. + let Some(required_cap) = len.checked_add(additional) else { + kani::assume(false); + return; + }; + + // Require RawVec doubling to stay within `usize`. + let Some(doubled_cap) = cap.checked_mul(2) else { + kani::assume(false); + return; + }; + + // Match RawVec::min_non_zero_cap for small non-empty allocations. + let min_cap = if elem_size == 1 { + 8 + } else if elem_size <= 1024 { + 4 + } else { + 1 + }; + + // Match RawVec::grow_amortized capacity selection. + let new_cap = core::cmp::max(core::cmp::max(doubled_cap, required_cap), min_cap); + + // Keep only states whose selected allocation layout is representable. + kani::assume(Layout::array::(new_cap).is_ok()); + } +} diff --git a/library/alloc/src/vec/spec_extend.rs b/library/alloc/src/vec/spec_extend.rs index 7085bceef5baa..1a9c3b966f979 100644 --- a/library/alloc/src/vec/spec_extend.rs +++ b/library/alloc/src/vec/spec_extend.rs @@ -1,4 +1,6 @@ use core::iter::TrustedLen; +#[cfg(kani)] +use core::kani; use core::slice::{self}; use super::{IntoIter, Vec}; @@ -55,3 +57,86 @@ where unsafe { self.append_elements(slice) }; } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::super::kani_vec_harness_helpers::*; + use super::*; + + // Harnesses for `Vec::spec_extend` with `IntoIter` + macro_rules! gen_spec_extend_into_iter_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create the destination Vec for the target element type + let mut vec = verifier_nondet_vec::<$ty>(); + // Create the source Vec whose elements will be moved by IntoIter + let source = verifier_nondet_vec::<$ty>(); + // Convert the source Vec into its owning iterator + let iter = source.into_iter(); + // Require enough capacity for all remaining source elements + assume_reserve_no_capacity_overflow::<$ty>( + vec.len(), + vec.capacity(), + iter.as_slice().len(), + ); + // Extend the destination Vec from the owning iterator specialization + vec.spec_extend(iter); + } + }; + } + + gen_spec_extend_into_iter_harness!(harness_spec_extend_into_iter_u8, u8); + gen_spec_extend_into_iter_harness!(harness_spec_extend_into_iter_u16, u16); + gen_spec_extend_into_iter_harness!(harness_spec_extend_into_iter_u32, u32); + gen_spec_extend_into_iter_harness!(harness_spec_extend_into_iter_u64, u64); + gen_spec_extend_into_iter_harness!(harness_spec_extend_into_iter_u128, u128); + gen_spec_extend_into_iter_harness!(harness_spec_extend_into_iter_usize, usize); + gen_spec_extend_into_iter_harness!(harness_spec_extend_into_iter_i8, i8); + gen_spec_extend_into_iter_harness!(harness_spec_extend_into_iter_i16, i16); + gen_spec_extend_into_iter_harness!(harness_spec_extend_into_iter_i32, i32); + gen_spec_extend_into_iter_harness!(harness_spec_extend_into_iter_i64, i64); + gen_spec_extend_into_iter_harness!(harness_spec_extend_into_iter_i128, i128); + gen_spec_extend_into_iter_harness!(harness_spec_extend_into_iter_isize, isize); + gen_spec_extend_into_iter_harness!(harness_spec_extend_into_iter_unit, ()); + gen_spec_extend_into_iter_harness!(harness_spec_extend_into_iter_array, [u8; 4]); + + // Harnesses for `Vec::spec_extend` with `slice::Iter` + macro_rules! gen_spec_extend_slice_iter_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create the destination Vec for the target element type + let mut vec = verifier_nondet_vec::<$ty>(); + // Create the source Vec whose elements will be cloned from a slice iterator + let source = verifier_nondet_vec::<$ty>(); + // Borrow the source Vec through its slice iterator + let iter = source.iter(); + // Require enough capacity for all remaining source elements + assume_reserve_no_capacity_overflow::<$ty>( + vec.len(), + vec.capacity(), + iter.as_slice().len(), + ); + // Extend the destination Vec from the slice iterator specialization + vec.spec_extend(iter); + } + }; + } + + gen_spec_extend_slice_iter_harness!(harness_spec_extend_slice_iter_u8, u8); + gen_spec_extend_slice_iter_harness!(harness_spec_extend_slice_iter_u16, u16); + gen_spec_extend_slice_iter_harness!(harness_spec_extend_slice_iter_u32, u32); + gen_spec_extend_slice_iter_harness!(harness_spec_extend_slice_iter_u64, u64); + gen_spec_extend_slice_iter_harness!(harness_spec_extend_slice_iter_u128, u128); + gen_spec_extend_slice_iter_harness!(harness_spec_extend_slice_iter_usize, usize); + gen_spec_extend_slice_iter_harness!(harness_spec_extend_slice_iter_i8, i8); + gen_spec_extend_slice_iter_harness!(harness_spec_extend_slice_iter_i16, i16); + gen_spec_extend_slice_iter_harness!(harness_spec_extend_slice_iter_i32, i32); + gen_spec_extend_slice_iter_harness!(harness_spec_extend_slice_iter_i64, i64); + gen_spec_extend_slice_iter_harness!(harness_spec_extend_slice_iter_i128, i128); + gen_spec_extend_slice_iter_harness!(harness_spec_extend_slice_iter_isize, isize); + gen_spec_extend_slice_iter_harness!(harness_spec_extend_slice_iter_unit, ()); + gen_spec_extend_slice_iter_harness!(harness_spec_extend_slice_iter_array, [u8; 4]); +} diff --git a/library/alloc/src/vec/spec_from_elem.rs b/library/alloc/src/vec/spec_from_elem.rs index 96d701e15d487..264b34e6fb291 100644 --- a/library/alloc/src/vec/spec_from_elem.rs +++ b/library/alloc/src/vec/spec_from_elem.rs @@ -1,3 +1,5 @@ +#[cfg(kani)] +use core::kani; use core::ptr; use super::{IsZero, Vec}; @@ -73,3 +75,45 @@ impl SpecFromElem for () { v } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::alloc::Global; + + // Harness for `SpecFromElem::from_elem` for `i8` + #[kani::proof] + pub fn harness_from_elem_for_i8() { + // Create a non-deterministic element to repeat + let elem: i8 = kani::any(); + // Choose a non-deterministic output length + let n: usize = kani::any(); + // Require the requested allocation layout to be representable + kani::assume(core::alloc::Layout::array::(n).is_ok()); + // Build a Vec by repeating the selected element + let _ = ::from_elem(elem, n, Global); + } + + // Harness for `SpecFromElem::from_elem` for `u8` + #[kani::proof] + pub fn harness_from_elem_for_u8() { + // Create a non-deterministic element to repeat + let elem: u8 = kani::any(); + // Choose a non-deterministic output length + let n: usize = kani::any(); + // Require the requested allocation layout to be representable + kani::assume(core::alloc::Layout::array::(n).is_ok()); + // Build a Vec by repeating the selected element + let _ = ::from_elem(elem, n, Global); + } + + // Harness for `SpecFromElem::from_elem` for `()` + #[kani::proof] + pub fn harness_from_elem_for_unit() { + // Choose a non-deterministic output length for the zero-sized element type + let n: usize = kani::any(); + // Build a Vec by repeating the unit element + let _ = <() as SpecFromElem>::from_elem((), n, Global); + } +} diff --git a/library/alloc/src/vec/spec_from_iter.rs b/library/alloc/src/vec/spec_from_iter.rs index e1f0b639bdfd6..e3a2e4afb8b92 100644 --- a/library/alloc/src/vec/spec_from_iter.rs +++ b/library/alloc/src/vec/spec_from_iter.rs @@ -1,3 +1,5 @@ +#[cfg(kani)] +use core::kani; use core::mem::ManuallyDrop; use core::ptr::{self}; @@ -62,3 +64,45 @@ impl SpecFromIter> for Vec { vec } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::super::kani_vec_harness_helpers::*; + use super::*; + + // Harness for `SpecFromIter::from_iter` + macro_rules! gen_from_iter_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a non-deterministic Vec for the target element type + let vec = verifier_nondet_vec::<$ty>(); + // Convert the Vec into its owning iterator + let mut iter = vec.into_iter(); + // Optionally consume one element before collecting the remaining iterator + // to cover both the advanced and unadvanced IntoIter cases + if kani::any::() { + let _ = iter.next(); + } + // Collect the remaining IntoIter through the FromIterator specialization + let _ = as SpecFromIter<$ty, IntoIter<$ty>>>::from_iter(iter); + } + }; + } + + gen_from_iter_harness!(harness_from_iter_u8, u8); + gen_from_iter_harness!(harness_from_iter_u16, u16); + gen_from_iter_harness!(harness_from_iter_u32, u32); + gen_from_iter_harness!(harness_from_iter_u64, u64); + gen_from_iter_harness!(harness_from_iter_u128, u128); + gen_from_iter_harness!(harness_from_iter_usize, usize); + gen_from_iter_harness!(harness_from_iter_i8, i8); + gen_from_iter_harness!(harness_from_iter_i16, i16); + gen_from_iter_harness!(harness_from_iter_i32, i32); + gen_from_iter_harness!(harness_from_iter_i64, i64); + gen_from_iter_harness!(harness_from_iter_i128, i128); + gen_from_iter_harness!(harness_from_iter_isize, isize); + gen_from_iter_harness!(harness_from_iter_unit, ()); + gen_from_iter_harness!(harness_from_iter_array, [u8; 4]); +} diff --git a/library/alloc/src/vec/spec_from_iter_nested.rs b/library/alloc/src/vec/spec_from_iter_nested.rs index 77f7761d22f95..22b92e376c1d9 100644 --- a/library/alloc/src/vec/spec_from_iter_nested.rs +++ b/library/alloc/src/vec/spec_from_iter_nested.rs @@ -1,4 +1,6 @@ use core::iter::TrustedLen; +#[cfg(kani)] +use core::kani; use core::{cmp, ptr}; use super::{SpecExtend, Vec}; @@ -61,3 +63,42 @@ where vector } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::super::Vec; + use super::*; + + // Harness for `SpecFromIterNested::from_iter` + macro_rules! gen_from_iter_default_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Choose a bounded non-deterministic iterator length + let len = kani::any_where(|len: &usize| *len <= 8); + // Build an iterator that yields non-deterministic elements and prevents specialization shortcuts + let iter = (0..len).map(|_| kani::any::<$ty>()).inspect(|_| ()); + // Collect the iterator through the nested FromIterator specialization + let vector = as SpecFromIterNested<$ty, _>>::from_iter(iter); + // Keep the harness focused on construction rather than drop behavior + core::mem::forget(vector); + } + }; + } + + gen_from_iter_default_harness!(harness_from_iter_default_u8, u8); + gen_from_iter_default_harness!(harness_from_iter_default_u16, u16); + gen_from_iter_default_harness!(harness_from_iter_default_u32, u32); + gen_from_iter_default_harness!(harness_from_iter_default_u64, u64); + gen_from_iter_default_harness!(harness_from_iter_default_u128, u128); + gen_from_iter_default_harness!(harness_from_iter_default_usize, usize); + gen_from_iter_default_harness!(harness_from_iter_default_i8, i8); + gen_from_iter_default_harness!(harness_from_iter_default_i16, i16); + gen_from_iter_default_harness!(harness_from_iter_default_i32, i32); + gen_from_iter_default_harness!(harness_from_iter_default_i64, i64); + gen_from_iter_default_harness!(harness_from_iter_default_i128, i128); + gen_from_iter_default_harness!(harness_from_iter_default_isize, isize); + gen_from_iter_default_harness!(harness_from_iter_default_unit, ()); + gen_from_iter_default_harness!(harness_from_iter_default_array, [u8; 4]); +}