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/boxed.rs b/library/alloc/src/boxed.rs index 49ff768bed1b2..fd954d9155d36 100644 --- a/library/alloc/src/boxed.rs +++ b/library/alloc/src/boxed.rs @@ -201,6 +201,9 @@ use core::pin::{Pin, PinCoerceUnsized}; use core::ptr::{self, NonNull, Unique}; use core::task::{Context, Poll}; +#[cfg(kani)] +use {crate::vec::Vec, core::kani}; + #[cfg(not(no_global_oom_handling))] use crate::alloc::handle_alloc_error; use crate::alloc::{AllocError, Allocator, Global, Layout}; @@ -941,6 +944,13 @@ impl Box, A> { /// ``` #[stable(feature = "new_uninit", since = "1.82.0")] #[inline] + #[cfg_attr( + kani, + kani::requires({ + let ptr = (&*self) as *const mem::MaybeUninit as *const T; + kani::mem::can_dereference(ptr) + }) + )] pub unsafe fn assume_init(self) -> Box { let (raw, alloc) = Box::into_raw_with_allocator(self); unsafe { Box::from_raw_in(raw as *mut T, alloc) } @@ -1008,6 +1018,13 @@ impl Box<[mem::MaybeUninit], A> { /// ``` #[stable(feature = "new_uninit", since = "1.82.0")] #[inline] + #[cfg_attr( + kani, + kani::requires({ + let ptr = (&*self) as *const [mem::MaybeUninit] as *const [T]; + kani::mem::can_dereference(ptr) + }) + )] pub unsafe fn assume_init(self) -> Box<[T], A> { let (raw, alloc) = Box::into_raw_with_allocator(self); unsafe { Box::from_raw_in(raw as *mut [T], alloc) } @@ -1060,6 +1077,18 @@ impl Box { #[stable(feature = "box_raw", since = "1.4.0")] #[inline] #[must_use = "call `drop(Box::from_raw(ptr))` if you intend to drop the `Box`"] + #[cfg_attr( + kani, + kani::requires({ + let align = kani::mem::checked_align_of_raw(raw); + let size = kani::mem::checked_size_of_raw(raw); + + !raw.is_null() + && align.is_some() + && size.map_or(false, |size| size <= isize::MAX as usize) + && kani::mem::can_dereference(raw) + }) + )] pub unsafe fn from_raw(raw: *mut T) -> Self { unsafe { Self::from_raw_in(raw, Global) } } @@ -1114,6 +1143,25 @@ impl Box { #[unstable(feature = "box_vec_non_null", reason = "new API", issue = "130364")] #[inline] #[must_use = "call `drop(Box::from_non_null(ptr))` if you intend to drop the `Box`"] + #[cfg_attr( + kani, + kani::requires({ + let raw = ptr.as_ptr(); + let align = kani::mem::checked_align_of_raw(raw); + let size = kani::mem::checked_size_of_raw(raw); + + align.is_some() + && size.map_or(false, |size| size <= isize::MAX as usize) + && kani::mem::can_dereference(raw) + }) + )] + #[cfg_attr( + kani, + kani::ensures(|result: &Self| { + let raw = ptr.as_ptr(); + (&**result) as *const T == raw + }) + )] pub unsafe fn from_non_null(ptr: NonNull) -> Self { unsafe { Self::from_raw(ptr.as_ptr()) } } @@ -1287,6 +1335,19 @@ impl Box { /// [memory layout]: self#memory-layout #[unstable(feature = "allocator_api", issue = "32838")] #[inline] + #[cfg_attr( + kani, + kani::requires({ + let align = kani::mem::checked_align_of_raw(raw); + let size = kani::mem::checked_size_of_raw(raw); + + !raw.is_null() + && align.is_some() + && size.map_or(false, |size| size <= isize::MAX as usize) + && kani::mem::can_dereference(raw) + }) + )] + #[cfg_attr(kani, kani::ensures(|result: &Self| (&**result) as *const T == raw))] pub unsafe fn from_raw_in(raw: *mut T, alloc: A) -> Self { Box(unsafe { Unique::new_unchecked(raw) }, alloc) } @@ -1340,6 +1401,19 @@ impl Box { #[unstable(feature = "allocator_api", issue = "32838")] // #[unstable(feature = "box_vec_non_null", reason = "new API", issue = "130364")] #[inline] + #[cfg_attr( + kani, + kani::requires({ + let ptr = raw.as_ptr(); + let align = kani::mem::checked_align_of_raw(ptr); + let size = kani::mem::checked_size_of_raw(ptr); + + align.is_some() + && size.map_or(false, |size| size <= isize::MAX as usize) + && kani::mem::can_dereference(ptr) + }) + )] + #[cfg_attr(kani, kani::ensures(|result: &Self| (&**result) as *const T == raw.as_ptr()))] pub unsafe fn from_non_null_in(raw: NonNull, alloc: A) -> Self { // SAFETY: guaranteed by the caller. unsafe { Box::from_raw_in(raw.as_ptr(), alloc) } @@ -2160,3 +2234,1741 @@ impl Error for Box { Error::provide(&**self, request); } } + +// ============================================================== +// Challenge 29: Verify safety of Boxed functions harnesses +// ============================================================== + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod kani_box_harness_helpers { + use super::*; + + pub(super) fn verifier_nondet_vec() -> Vec { + 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 + } + + pub(super) fn box_slice_layout_ok(len: usize) -> bool { + Layout::array::(len).is_ok() + } + + pub(super) fn nondet_box_slice(vec: &Vec) -> &[T] { + let len = vec.len(); + kani::assume(box_slice_layout_ok::(len)); + vec.as_slice() + } + + pub(super) fn verifier_nondet_vec_box() -> Vec { + let vec = verifier_nondet_vec(); + kani::assume(box_slice_layout_ok::(vec.len())); + vec + } + + pub(super) fn verifier_nondet_box_uninit_slice() -> Box<[mem::MaybeUninit], Global> { + let len = kani::any_where(|l: &usize| box_slice_layout_ok::(*l)); + let mut boxed = Box::<[T]>::new_uninit_slice(len); + unsafe { + ptr::write_bytes( + boxed.as_mut_ptr().cast::(), + kani::any::(), + mem::size_of::() * len, + ); + } + boxed + } +} + +// === UNSAFE FUNCTIONS === + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use core::any::Any; + use core::marker::PhantomPinned; + + use super::kani_box_harness_helpers::*; + use super::*; + + // Kani limitation: proof_for_contract is not reliable for this + // MaybeUninit-based generic impl in boxed.rs, so these harnesses use + // #[kani::proof] and exercise the caller-side safety requirement directly. + // + // Kani cannot express the full generic "value is initialized" predicate + // for arbitrary `T`. The harness models the Safety contract by explicitly + // writing a valid `T` into the boxed MaybeUninit slot before calling + // `assume_init`. + macro_rules! gen_assume_init_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic initialized value of the target type. + let value: $ty = kani::any::<$ty>(); + + // Keep a copy so the initialized result can be compared after conversion. + let expected = value.clone(); + + // Allocate boxed storage for an uninitialized value of the same type. + let mut uninit: Box, Global> = + Box::<$ty, Global>::new_uninit_in(Global); + + // Write a valid `$ty` into the boxed `MaybeUninit` slot. + (*uninit).write(value); + + // Convert the boxed `MaybeUninit` into a boxed initialized value. + let init: Box<$ty, Global> = unsafe { uninit.assume_init() }; + + // Check that the recovered value matches the one written into the slot. + assert_eq!(&*init, &expected); + } + }; + } + + gen_assume_init_harness!(harness_box_assume_init_i8, i8); + gen_assume_init_harness!(harness_box_assume_init_i16, i16); + gen_assume_init_harness!(harness_box_assume_init_i32, i32); + gen_assume_init_harness!(harness_box_assume_init_i64, i64); + gen_assume_init_harness!(harness_box_assume_init_i128, i128); + gen_assume_init_harness!(harness_box_assume_init_u8, u8); + gen_assume_init_harness!(harness_box_assume_init_u16, u16); + gen_assume_init_harness!(harness_box_assume_init_u32, u32); + gen_assume_init_harness!(harness_box_assume_init_u64, u64); + gen_assume_init_harness!(harness_box_assume_init_u128, u128); + gen_assume_init_harness!(harness_box_assume_init_unit, ()); + gen_assume_init_harness!(harness_box_assume_init_array, [u8; 4]); + gen_assume_init_harness!(harness_box_assume_init_bool, bool); + + // Kani limitation: proof_for_contract is not reliable for this + // MaybeUninit-based slice impl in boxed.rs, so these harnesses use + // #[kani::proof] and exercise the caller-side safety requirement directly. + // + // For byte-valid element types, the harness can model the caller-side + // safety requirement with an unbounded byte-level witness: it constructs a + // boxed `[MaybeUninit]` slice using Box's own uninitialized slice API, + // fills the backing bytes nondeterministically, and then converts it to + // `Box<[T]>`. + macro_rules! gen_assume_init_slice_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Build a symbolic boxed slice of `MaybeUninit` elements. + let uninit: Box<[mem::MaybeUninit<$elem>], Global> = + verifier_nondet_box_uninit_slice::<$elem>(); + + // Record the original data pointer before the conversion. + let expected_data = (&*uninit).as_ptr() as *const $elem; + + // Record the original slice length before the conversion. + let expected_len = uninit.len(); + + // Convert the boxed `MaybeUninit` slice into a boxed initialized slice. + let result: Box<[$elem], Global> = unsafe { uninit.assume_init() }; + + // Check that the conversion preserves the backing data pointer. + assert_eq!((&*result).as_ptr(), expected_data); + + // Check that the conversion preserves the slice length. + assert_eq!(result.len(), expected_len); + } + }; + } + + gen_assume_init_slice_harness!(harness_box_assume_init_slice_i8, i8); + gen_assume_init_slice_harness!(harness_box_assume_init_slice_i16, i16); + gen_assume_init_slice_harness!(harness_box_assume_init_slice_i32, i32); + gen_assume_init_slice_harness!(harness_box_assume_init_slice_i64, i64); + gen_assume_init_slice_harness!(harness_box_assume_init_slice_i128, i128); + gen_assume_init_slice_harness!(harness_box_assume_init_slice_u8, u8); + gen_assume_init_slice_harness!(harness_box_assume_init_slice_u16, u16); + gen_assume_init_slice_harness!(harness_box_assume_init_slice_u32, u32); + gen_assume_init_slice_harness!(harness_box_assume_init_slice_u64, u64); + gen_assume_init_slice_harness!(harness_box_assume_init_slice_u128, u128); + gen_assume_init_slice_harness!(harness_box_assume_init_slice_unit, ()); + gen_assume_init_slice_harness!(harness_box_assume_init_slice_array, [u8; 4]); + + macro_rules! gen_from_raw_sized_harness { + ($name:ident, $ty:ty) => { + #[kani::proof_for_contract(Box::<$ty>::from_raw)] + pub fn $name() { + // Create a symbolic value of the target type. + let value: $ty = kani::any(); + + // Build a boxed value whose allocation will become the raw witness. + let boxed: Box<$ty> = Box::new(value); + + // Consume the box and extract the raw pointer expected by `from_raw`. + let ptr: *mut $ty = Box::into_raw(boxed); + + // Rebuild ownership from the raw pointer. + let _recovered: Box<$ty> = unsafe { Box::from_raw(ptr) }; + } + }; + } + + macro_rules! gen_from_raw_unsized_harness { + ($name:ident, $elem:ty) => { + #[kani::proof_for_contract(Box::<[$elem]>::from_raw)] + pub fn $name() { + // Build a symbolic boxed slice of the target element type. + let boxed: Box<[$elem]> = verifier_nondet_vec_box::<$elem>().into_boxed_slice(); + + // Consume the boxed slice and extract the raw fat pointer. + let ptr: *mut [$elem] = Box::into_raw(boxed); + + // Rebuild ownership from the raw slice pointer. + let _recovered: Box<[$elem]> = unsafe { Box::from_raw(ptr) }; + } + }; + } + + gen_from_raw_sized_harness!(harness_box_from_raw_i8, i8); + gen_from_raw_sized_harness!(harness_box_from_raw_i16, i16); + gen_from_raw_sized_harness!(harness_box_from_raw_i32, i32); + gen_from_raw_sized_harness!(harness_box_from_raw_i64, i64); + gen_from_raw_sized_harness!(harness_box_from_raw_i128, i128); + gen_from_raw_sized_harness!(harness_box_from_raw_u8, u8); + gen_from_raw_sized_harness!(harness_box_from_raw_u16, u16); + gen_from_raw_sized_harness!(harness_box_from_raw_u32, u32); + gen_from_raw_sized_harness!(harness_box_from_raw_u64, u64); + gen_from_raw_sized_harness!(harness_box_from_raw_u128, u128); + gen_from_raw_sized_harness!(harness_box_from_raw_bool, bool); + gen_from_raw_sized_harness!(harness_box_from_raw_unit, ()); + gen_from_raw_sized_harness!(harness_box_from_raw_array, [u8; 4]); + + gen_from_raw_unsized_harness!(harness_box_from_raw_vec_u8, u8); + gen_from_raw_unsized_harness!(harness_box_from_raw_vec_u16, u16); + gen_from_raw_unsized_harness!(harness_box_from_raw_vec_u32, u32); + gen_from_raw_unsized_harness!(harness_box_from_raw_vec_u64, u64); + gen_from_raw_unsized_harness!(harness_box_from_raw_vec_u128, u128); + + macro_rules! gen_from_non_null_sized_harness { + ($name:ident, $ty:ty) => { + #[kani::proof_for_contract(Box::<$ty>::from_non_null)] + pub fn $name() { + // Create a symbolic value of the target type. + let value: $ty = kani::any(); + + // Build a boxed value whose allocation will become the non-null witness. + let boxed: Box<$ty> = Box::new(value); + + // Consume the box and extract the non-null pointer expected by `from_non_null`. + let ptr: NonNull<$ty> = Box::into_non_null(boxed); + + // Rebuild ownership from the non-null pointer. + let _recovered: Box<$ty> = unsafe { Box::from_non_null(ptr) }; + } + }; + } + + macro_rules! gen_from_non_null_unsized_harness { + ($name:ident, $elem:ty) => { + #[kani::proof_for_contract(Box::<[$elem]>::from_non_null)] + pub fn $name() { + // Build a symbolic boxed slice of the target element type. + let boxed: Box<[$elem]> = verifier_nondet_vec_box::<$elem>().into_boxed_slice(); + + // Consume the boxed slice and extract the non-null fat pointer. + let ptr: NonNull<[$elem]> = Box::into_non_null(boxed); + + // Rebuild ownership from the non-null slice pointer. + let _recovered: Box<[$elem]> = unsafe { Box::from_non_null(ptr) }; + } + }; + } + + gen_from_non_null_sized_harness!(harness_box_from_non_null_i8, i8); + gen_from_non_null_sized_harness!(harness_box_from_non_null_i16, i16); + gen_from_non_null_sized_harness!(harness_box_from_non_null_i32, i32); + gen_from_non_null_sized_harness!(harness_box_from_non_null_i64, i64); + gen_from_non_null_sized_harness!(harness_box_from_non_null_i128, i128); + gen_from_non_null_sized_harness!(harness_box_from_non_null_u8, u8); + gen_from_non_null_sized_harness!(harness_box_from_non_null_u16, u16); + gen_from_non_null_sized_harness!(harness_box_from_non_null_u32, u32); + gen_from_non_null_sized_harness!(harness_box_from_non_null_u64, u64); + gen_from_non_null_sized_harness!(harness_box_from_non_null_u128, u128); + gen_from_non_null_sized_harness!(harness_box_from_non_null_bool, bool); + gen_from_non_null_sized_harness!(harness_box_from_non_null_unit, ()); + gen_from_non_null_sized_harness!(harness_box_from_non_null_array, [u8; 4]); + + gen_from_non_null_unsized_harness!(harness_box_from_non_null_vec_u8, u8); + gen_from_non_null_unsized_harness!(harness_box_from_non_null_vec_u16, u16); + gen_from_non_null_unsized_harness!(harness_box_from_non_null_vec_u32, u32); + gen_from_non_null_unsized_harness!(harness_box_from_non_null_vec_u64, u64); + gen_from_non_null_unsized_harness!(harness_box_from_non_null_vec_u128, u128); + + // These harnesses allocate raw memory directly instead of using higher-level + // Box constructors. `proof_for_contract` requires a single top-level call to + // `Box::from_raw_in`, while helpers such as `Box::new_in`, + // `Box::new_uninit_slice_in`, and `Vec::into_boxed_slice` eventually route + // through `Box::from_raw_in` during setup. + + macro_rules! gen_from_raw_in_sized_harness { + ($name:ident, $ty:ty) => { + #[kani::proof_for_contract(Box::<$ty, Global>::from_raw_in)] + pub fn $name() { + // Create a symbolic value of the target type. + let value: $ty = kani::any(); + + // Build a raw pointer that satisfies the contract without using + // `Box::new_in`, which would internally call `Box::from_raw_in`. + let ptr: *mut $ty = if mem::size_of::<$ty>() == 0 { + // ZST boxes use a non-null dangling pointer and never allocate. + mem::forget(value); + NonNull::<$ty>::dangling().as_ptr() + } else { + let layout = Layout::new::<$ty>(); + // Allocate backing memory with the same allocator passed to + // the function under test, then initialize it with a valid `$ty`. + let ptr = match Global.allocate(layout) { + Ok(memory) => memory.cast::<$ty>().as_ptr(), + Err(_) => handle_alloc_error(layout), + }; + unsafe { ptr.write(value) }; + ptr + }; + + // Use the same allocator witness that was used to produce the raw pointer. + let alloc = Global; + + // Rebuild ownership from the raw pointer and allocator pair. + let _recovered: Box<$ty, Global> = unsafe { Box::from_raw_in(ptr, alloc) }; + } + }; + } + + macro_rules! gen_from_raw_in_unsized_harness { + ($name:ident, $elem:ty) => { + #[kani::proof_for_contract(Box::<[$elem], Global>::from_raw_in)] + pub fn $name() { + // Keep the slice length symbolic so this remains an unbound + // unsized harness, while still ruling out impossible layouts. + let len: usize = kani::any_where(|len: &usize| box_slice_layout_ok::<$elem>(*len)); + + let data: *mut $elem = if len == 0 { + // Empty slices use a non-null dangling data pointer. + NonNull::<$elem>::dangling().as_ptr() + } else { + let layout = Layout::array::<$elem>(len).unwrap(); + // Allocate raw backing storage for `len` elements with the + // allocator that will later be given to `from_raw_in`. + let ptr = match Global.allocate(layout) { + Ok(memory) => memory.cast::<$elem>().as_ptr(), + Err(_) => handle_alloc_error(layout), + }; + unsafe { + // Fill the allocation with unconstrained bytes before + // packaging it as a raw slice pointer. + ptr::write_bytes( + ptr.cast::(), + kani::any::(), + mem::size_of::<$elem>() * len, + ); + } + ptr + }; + + // Rebuild the fat pointer expected by `Box<[T]>::from_raw_in` + // from the data pointer plus symbolic slice length. + let ptr: *mut [$elem] = ptr::slice_from_raw_parts_mut(data, len); + + // Use the same allocator witness that was used to produce the backing storage. + let alloc = Global; + + // Rebuild ownership from the raw slice pointer and allocator pair. + let _recovered: Box<[$elem], Global> = unsafe { Box::from_raw_in(ptr, alloc) }; + } + }; + } + + gen_from_raw_in_sized_harness!(harness_box_from_raw_in_i8, i8); + gen_from_raw_in_sized_harness!(harness_box_from_raw_in_i16, i16); + gen_from_raw_in_sized_harness!(harness_box_from_raw_in_i32, i32); + gen_from_raw_in_sized_harness!(harness_box_from_raw_in_i64, i64); + gen_from_raw_in_sized_harness!(harness_box_from_raw_in_i128, i128); + gen_from_raw_in_sized_harness!(harness_box_from_raw_in_u8, u8); + gen_from_raw_in_sized_harness!(harness_box_from_raw_in_u16, u16); + gen_from_raw_in_sized_harness!(harness_box_from_raw_in_u32, u32); + gen_from_raw_in_sized_harness!(harness_box_from_raw_in_u64, u64); + gen_from_raw_in_sized_harness!(harness_box_from_raw_in_u128, u128); + gen_from_raw_in_sized_harness!(harness_box_from_raw_in_bool, bool); + gen_from_raw_in_sized_harness!(harness_box_from_raw_in_unit, ()); + gen_from_raw_in_sized_harness!(harness_box_from_raw_in_array, [u8; 4]); + + gen_from_raw_in_unsized_harness!(harness_box_from_raw_in_vec_u8, u8); + gen_from_raw_in_unsized_harness!(harness_box_from_raw_in_vec_u16, u16); + gen_from_raw_in_unsized_harness!(harness_box_from_raw_in_vec_u32, u32); + gen_from_raw_in_unsized_harness!(harness_box_from_raw_in_vec_u64, u64); + gen_from_raw_in_unsized_harness!(harness_box_from_raw_in_vec_u128, u128); + + macro_rules! gen_from_non_null_in_sized_harness { + ($name:ident, $ty:ty) => { + #[kani::proof_for_contract(Box::<$ty, Global>::from_non_null_in)] + pub fn $name() { + // Create a symbolic value of the target type. + let value: $ty = kani::any(); + + // Build the boxed value whose allocation will become the non-null witness. + let boxed: Box<$ty, Global> = Box::new_in(value, Global); + + // Consume the box and extract the non-null pointer together with its allocator. + let (ptr, alloc): (NonNull<$ty>, Global) = Box::into_non_null_with_allocator(boxed); + + // Rebuild ownership from the non-null pointer and allocator pair. + let _recovered: Box<$ty, Global> = unsafe { Box::from_non_null_in(ptr, alloc) }; + } + }; + } + + macro_rules! gen_from_non_null_in_unsized_harness { + ($name:ident, $elem:ty) => { + #[kani::proof_for_contract(Box::<[$elem], Global>::from_non_null_in)] + pub fn $name() { + // Build a symbolic boxed slice of the target element type. + let boxed: Box<[$elem], Global> = + verifier_nondet_vec_box::<$elem>().into_boxed_slice(); + + // Consume the boxed slice and extract the non-null fat pointer together with its allocator. + let (ptr, alloc): (NonNull<[$elem]>, Global) = + Box::into_non_null_with_allocator(boxed); + + // Rebuild ownership from the non-null slice pointer and allocator pair. + let _recovered: Box<[$elem], Global> = unsafe { Box::from_non_null_in(ptr, alloc) }; + } + }; + } + + gen_from_non_null_in_sized_harness!(harness_box_from_non_null_in_i8, i8); + gen_from_non_null_in_sized_harness!(harness_box_from_non_null_in_i16, i16); + gen_from_non_null_in_sized_harness!(harness_box_from_non_null_in_i32, i32); + gen_from_non_null_in_sized_harness!(harness_box_from_non_null_in_i64, i64); + gen_from_non_null_in_sized_harness!(harness_box_from_non_null_in_i128, i128); + gen_from_non_null_in_sized_harness!(harness_box_from_non_null_in_u8, u8); + gen_from_non_null_in_sized_harness!(harness_box_from_non_null_in_u16, u16); + gen_from_non_null_in_sized_harness!(harness_box_from_non_null_in_u32, u32); + gen_from_non_null_in_sized_harness!(harness_box_from_non_null_in_u64, u64); + gen_from_non_null_in_sized_harness!(harness_box_from_non_null_in_u128, u128); + gen_from_non_null_in_sized_harness!(harness_box_from_non_null_in_bool, bool); + gen_from_non_null_in_sized_harness!(harness_box_from_non_null_in_unit, ()); + gen_from_non_null_in_sized_harness!(harness_box_from_non_null_in_array, [u8; 4]); + + gen_from_non_null_in_unsized_harness!(harness_box_from_non_null_in_vec_u8, u8); + gen_from_non_null_in_unsized_harness!(harness_box_from_non_null_in_vec_u16, u16); + gen_from_non_null_in_unsized_harness!(harness_box_from_non_null_in_vec_u32, u32); + gen_from_non_null_in_unsized_harness!(harness_box_from_non_null_in_vec_u64, u64); + gen_from_non_null_in_unsized_harness!(harness_box_from_non_null_in_vec_u128, u128); + + // === SAFE FUNCTIONS === + + macro_rules! gen_box_new_in_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic input value of the target element type. + let value: $ty = kani::any(); + + // Call the safe constructor with the global allocator. + let _boxed: Box<$ty, Global> = Box::<$ty, Global>::new_in(value, Global); + } + }; + } + + macro_rules! gen_box_new_in_vec_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic vector payload for the boxed value. + let vec: Vec<$elem> = verifier_nondet_vec::<$elem>(); + + // Call the safe constructor with the global allocator. + let _boxed: Box, Global> = + Box::, Global>::new_in(vec, Global); + } + }; + } + + gen_box_new_in_harness!(harness_box_new_in_i8, i8); + gen_box_new_in_harness!(harness_box_new_in_i16, i16); + gen_box_new_in_harness!(harness_box_new_in_i32, i32); + gen_box_new_in_harness!(harness_box_new_in_i64, i64); + gen_box_new_in_harness!(harness_box_new_in_i128, i128); + gen_box_new_in_harness!(harness_box_new_in_u8, u8); + gen_box_new_in_harness!(harness_box_new_in_u16, u16); + gen_box_new_in_harness!(harness_box_new_in_u32, u32); + gen_box_new_in_harness!(harness_box_new_in_u64, u64); + gen_box_new_in_harness!(harness_box_new_in_u128, u128); + gen_box_new_in_harness!(harness_box_new_in_unit, ()); + gen_box_new_in_harness!(harness_box_new_in_array, [u8; 4]); + gen_box_new_in_harness!(harness_box_new_in_bool, bool); + + gen_box_new_in_vec_harness!(harness_box_new_in_vec_u8, u8); + gen_box_new_in_vec_harness!(harness_box_new_in_vec_u16, u16); + gen_box_new_in_vec_harness!(harness_box_new_in_vec_u32, u32); + gen_box_new_in_vec_harness!(harness_box_new_in_vec_u64, u64); + gen_box_new_in_vec_harness!(harness_box_new_in_vec_u128, u128); + + macro_rules! gen_box_try_new_in_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic input value of the target element type. + let value: $ty = kani::any(); + + // Call the fallible safe constructor with the global allocator. + let _result = Box::<$ty, Global>::try_new_in(value, Global); + } + }; + } + + macro_rules! gen_box_try_new_in_vec_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic vector payload for the boxed value. + let vec: Vec<$elem> = verifier_nondet_vec::<$elem>(); + + // Call the fallible safe constructor with the global allocator. + let _result = Box::, Global>::try_new_in(vec, Global); + } + }; + } + + gen_box_try_new_in_harness!(harness_box_try_new_in_i8, i8); + gen_box_try_new_in_harness!(harness_box_try_new_in_i16, i16); + gen_box_try_new_in_harness!(harness_box_try_new_in_i32, i32); + gen_box_try_new_in_harness!(harness_box_try_new_in_i64, i64); + gen_box_try_new_in_harness!(harness_box_try_new_in_i128, i128); + gen_box_try_new_in_harness!(harness_box_try_new_in_u8, u8); + gen_box_try_new_in_harness!(harness_box_try_new_in_u16, u16); + gen_box_try_new_in_harness!(harness_box_try_new_in_u32, u32); + gen_box_try_new_in_harness!(harness_box_try_new_in_u64, u64); + gen_box_try_new_in_harness!(harness_box_try_new_in_u128, u128); + gen_box_try_new_in_harness!(harness_box_try_new_in_unit, ()); + gen_box_try_new_in_harness!(harness_box_try_new_in_array, [u8; 4]); + gen_box_try_new_in_harness!(harness_box_try_new_in_bool, bool); + + gen_box_try_new_in_vec_harness!(harness_box_try_new_in_vec_u8, u8); + gen_box_try_new_in_vec_harness!(harness_box_try_new_in_vec_u16, u16); + gen_box_try_new_in_vec_harness!(harness_box_try_new_in_vec_u32, u32); + gen_box_try_new_in_vec_harness!(harness_box_try_new_in_vec_u64, u64); + gen_box_try_new_in_vec_harness!(harness_box_try_new_in_vec_u128, u128); + + macro_rules! gen_box_try_new_uninit_in_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Call the fallible uninitialized constructor with the global allocator. + let _result = Box::<$ty, Global>::try_new_uninit_in(Global); + } + }; + } + + gen_box_try_new_uninit_in_harness!(harness_box_try_new_uninit_in_i8, i8); + gen_box_try_new_uninit_in_harness!(harness_box_try_new_uninit_in_i16, i16); + gen_box_try_new_uninit_in_harness!(harness_box_try_new_uninit_in_i32, i32); + gen_box_try_new_uninit_in_harness!(harness_box_try_new_uninit_in_i64, i64); + gen_box_try_new_uninit_in_harness!(harness_box_try_new_uninit_in_i128, i128); + gen_box_try_new_uninit_in_harness!(harness_box_try_new_uninit_in_u8, u8); + gen_box_try_new_uninit_in_harness!(harness_box_try_new_uninit_in_u16, u16); + gen_box_try_new_uninit_in_harness!(harness_box_try_new_uninit_in_u32, u32); + gen_box_try_new_uninit_in_harness!(harness_box_try_new_uninit_in_u64, u64); + gen_box_try_new_uninit_in_harness!(harness_box_try_new_uninit_in_u128, u128); + gen_box_try_new_uninit_in_harness!(harness_box_try_new_uninit_in_unit, ()); + gen_box_try_new_uninit_in_harness!(harness_box_try_new_uninit_in_array, [u8; 4]); + gen_box_try_new_uninit_in_harness!(harness_box_try_new_uninit_in_bool, bool); + + macro_rules! gen_box_try_new_zeroed_in_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Call the fallible zeroed constructor with the global allocator. + let _result = Box::<$ty, Global>::try_new_zeroed_in(Global); + } + }; + } + + gen_box_try_new_zeroed_in_harness!(harness_box_try_new_zeroed_in_i8, i8); + gen_box_try_new_zeroed_in_harness!(harness_box_try_new_zeroed_in_i16, i16); + gen_box_try_new_zeroed_in_harness!(harness_box_try_new_zeroed_in_i32, i32); + gen_box_try_new_zeroed_in_harness!(harness_box_try_new_zeroed_in_i64, i64); + gen_box_try_new_zeroed_in_harness!(harness_box_try_new_zeroed_in_i128, i128); + gen_box_try_new_zeroed_in_harness!(harness_box_try_new_zeroed_in_u8, u8); + gen_box_try_new_zeroed_in_harness!(harness_box_try_new_zeroed_in_u16, u16); + gen_box_try_new_zeroed_in_harness!(harness_box_try_new_zeroed_in_u32, u32); + gen_box_try_new_zeroed_in_harness!(harness_box_try_new_zeroed_in_u64, u64); + gen_box_try_new_zeroed_in_harness!(harness_box_try_new_zeroed_in_u128, u128); + gen_box_try_new_zeroed_in_harness!(harness_box_try_new_zeroed_in_unit, ()); + gen_box_try_new_zeroed_in_harness!(harness_box_try_new_zeroed_in_array, [u8; 4]); + gen_box_try_new_zeroed_in_harness!(harness_box_try_new_zeroed_in_bool, bool); + + macro_rules! gen_box_into_boxed_slice_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic input value of the target element type. + let value: $ty = kani::any(); + + // Build the boxed scalar value that will be reinterpreted as a slice. + let boxed: Box<$ty, Global> = Box::<$ty, Global>::new_in(value, Global); + + // Convert the boxed scalar into a boxed single-element slice. + let _slice: Box<[$ty], Global> = Box::<$ty, Global>::into_boxed_slice(boxed); + } + }; + } + + macro_rules! gen_box_into_boxed_slice_vec_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic vector payload for the boxed value. + let value: Vec<$elem> = verifier_nondet_vec::<$elem>(); + + // Build the boxed vector value that will be reinterpreted as a slice. + let boxed: Box, Global> = + Box::, Global>::new_in(value, Global); + + // Convert the boxed vector into a boxed single-element slice. + let _slice: Box<[Vec<$elem>], Global> = + Box::, Global>::into_boxed_slice(boxed); + } + }; + } + + gen_box_into_boxed_slice_harness!(harness_box_into_boxed_slice_i8, i8); + gen_box_into_boxed_slice_harness!(harness_box_into_boxed_slice_i16, i16); + gen_box_into_boxed_slice_harness!(harness_box_into_boxed_slice_i32, i32); + gen_box_into_boxed_slice_harness!(harness_box_into_boxed_slice_i64, i64); + gen_box_into_boxed_slice_harness!(harness_box_into_boxed_slice_i128, i128); + gen_box_into_boxed_slice_harness!(harness_box_into_boxed_slice_u8, u8); + gen_box_into_boxed_slice_harness!(harness_box_into_boxed_slice_u16, u16); + gen_box_into_boxed_slice_harness!(harness_box_into_boxed_slice_u32, u32); + gen_box_into_boxed_slice_harness!(harness_box_into_boxed_slice_u64, u64); + gen_box_into_boxed_slice_harness!(harness_box_into_boxed_slice_u128, u128); + gen_box_into_boxed_slice_harness!(harness_box_into_boxed_slice_unit, ()); + gen_box_into_boxed_slice_harness!(harness_box_into_boxed_slice_array, [u8; 4]); + gen_box_into_boxed_slice_harness!(harness_box_into_boxed_slice_bool, bool); + + gen_box_into_boxed_slice_vec_harness!(harness_box_into_boxed_slice_vec_u8, u8); + gen_box_into_boxed_slice_vec_harness!(harness_box_into_boxed_slice_vec_u16, u16); + gen_box_into_boxed_slice_vec_harness!(harness_box_into_boxed_slice_vec_u32, u32); + gen_box_into_boxed_slice_vec_harness!(harness_box_into_boxed_slice_vec_u64, u64); + gen_box_into_boxed_slice_vec_harness!(harness_box_into_boxed_slice_vec_u128, u128); + + macro_rules! gen_box_new_uninit_slice_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic slice length that stays within the box slice layout limits. + let len: usize = kani::any_where(|l: &usize| box_slice_layout_ok::<$ty>(*l)); + + // Construct an uninitialized boxed slice for that symbolic length. + let _boxed: Box<[mem::MaybeUninit<$ty>]> = Box::<[$ty]>::new_uninit_slice(len); + } + }; + } + + gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_i8, i8); + gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_i16, i16); + gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_i32, i32); + gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_i64, i64); + gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_i128, i128); + gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_u8, u8); + gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_u16, u16); + gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_u32, u32); + gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_u64, u64); + gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_u128, u128); + gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_unit, ()); + gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_bool, bool); + gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_array, [u8; 4]); + + macro_rules! gen_box_new_zeroed_slice_harness { + ($name:ident, $elem_ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic slice length that stays within the box slice layout limits. + let len: usize = kani::any_where(|l: &usize| box_slice_layout_ok::<$elem_ty>(*l)); + + // Construct a zeroed boxed slice for that symbolic length. + let _boxed: Box<[mem::MaybeUninit<$elem_ty>]> = + Box::<[$elem_ty]>::new_zeroed_slice(len); + } + }; + } + + gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_i8, i8); + gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_i16, i16); + gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_i32, i32); + gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_i64, i64); + gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_i128, i128); + gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_u8, u8); + gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_u16, u16); + gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_u32, u32); + gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_u64, u64); + gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_u128, u128); + gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_unit, ()); + gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_bool, bool); + gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_array, [u8; 4]); + + macro_rules! gen_box_try_new_uninit_slice_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic slice length for the fallible constructor call. + let len: usize = kani::any(); + + // Call the fallible uninitialized slice constructor with that length. + let _result: Result]>, AllocError> = + Box::<[$ty]>::try_new_uninit_slice(len); + } + }; + } + + gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_i8, i8); + gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_i16, i16); + gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_i32, i32); + gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_i64, i64); + gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_i128, i128); + gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_u8, u8); + gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_u16, u16); + gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_u32, u32); + gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_u64, u64); + gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_u128, u128); + gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_unit, ()); + gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_bool, bool); + gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_array, [u8; 4]); + + macro_rules! gen_box_try_new_zeroed_slice_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic slice length for the fallible constructor call. + let len: usize = kani::any(); + + // Call the fallible zeroed slice constructor with that length. + let _result: Result]>, AllocError> = + Box::<[$ty]>::try_new_zeroed_slice(len); + } + }; + } + + gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_i8, i8); + gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_i16, i16); + gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_i32, i32); + gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_i64, i64); + gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_i128, i128); + gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_u8, u8); + gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_u16, u16); + gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_u32, u32); + gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_u64, u64); + gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_u128, u128); + gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_unit, ()); + gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_bool, bool); + gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_array, [u8; 4]); + + // `Box<[T]>::into_array::` branches only on `self.len() == N`. + // + // The harness builds `self` from a nondeterministic `Vec`, so the slice + // length is symbolic. With `N` fixed to 100, Kani explores: + // - `vec.len() == 100`: `into_array` calls `Box::into_raw(self)`, casts the + // slice pointer to `*mut [T; 100]`, rebuilds it with `Box::from_raw`, and + // returns `Some(Box<[T; 100]>)`. + // - `vec.len() != 100`: the length check fails, so `into_array` returns + // `None` without reinterpreting the slice pointer as an array. + macro_rules! gen_box_into_array_slice_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic vector that determines the slice length at runtime. + let vec: Vec<$ty> = verifier_nondet_vec_box::<$ty>(); + + // Turn the vector into the boxed slice consumed by `into_array`. + let boxed: Box<[$ty]> = vec.into_boxed_slice(); + + // Fix the target array length used by the conversion attempt. + const N: usize = 100; + + // Attempt the safe conversion from a boxed slice into a boxed array. + let _: Option> = boxed.into_array::(); + } + }; + } + + gen_box_into_array_slice_harness!(harness_box_into_array_slice_i8, i8); + gen_box_into_array_slice_harness!(harness_box_into_array_slice_i16, i16); + gen_box_into_array_slice_harness!(harness_box_into_array_slice_i32, i32); + gen_box_into_array_slice_harness!(harness_box_into_array_slice_i64, i64); + gen_box_into_array_slice_harness!(harness_box_into_array_slice_i128, i128); + gen_box_into_array_slice_harness!(harness_box_into_array_slice_u8, u8); + gen_box_into_array_slice_harness!(harness_box_into_array_slice_u16, u16); + gen_box_into_array_slice_harness!(harness_box_into_array_slice_u32, u32); + gen_box_into_array_slice_harness!(harness_box_into_array_slice_u64, u64); + gen_box_into_array_slice_harness!(harness_box_into_array_slice_u128, u128); + gen_box_into_array_slice_harness!(harness_box_into_array_slice_unit, ()); + gen_box_into_array_slice_harness!(harness_box_into_array_slice_array, [u8; 4]); + + macro_rules! gen_box_new_uninit_slice_in_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic slice length that stays within the box slice layout limits. + let len: usize = kani::any_where(|l: &usize| box_slice_layout_ok::<$ty>(*l)); + + // Construct an allocator-aware uninitialized boxed slice with the global allocator. + let _boxed: Box<[mem::MaybeUninit<$ty>], Global> = + Box::<[$ty], Global>::new_uninit_slice_in(len, Global); + } + }; + } + + gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_i8, i8); + gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_i16, i16); + gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_i32, i32); + gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_i64, i64); + gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_i128, i128); + gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_u8, u8); + gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_u16, u16); + gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_u32, u32); + gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_u64, u64); + gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_u128, u128); + gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_unit, ()); + gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_bool, bool); + gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_array, [u8; 4]); + + macro_rules! gen_box_new_zeroed_slice_in_harness { + ($name:ident, $elem_ty:ty) => { + #[kani::proof] + pub fn $name() { + // Name the element type once so the layout helper and the target call stay aligned. + type T = $elem_ty; + + // Create a symbolic slice length that stays within the box slice layout limits. + let len: usize = kani::any_where(|l: &usize| box_slice_layout_ok::(*l)); + + // Construct an allocator-aware zeroed boxed slice with the global allocator. + let _boxed: Box<[mem::MaybeUninit], Global> = + Box::<[T], Global>::new_zeroed_slice_in(len, Global); + } + }; + } + + gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_i8, i8); + gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_i16, i16); + gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_i32, i32); + gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_i64, i64); + gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_i128, i128); + gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_u8, u8); + gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_u16, u16); + gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_u32, u32); + gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_u64, u64); + gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_u128, u128); + gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_unit, ()); + gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_bool, bool); + gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_array, [u8; 4]); + + macro_rules! gen_box_try_new_uninit_slice_in_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic slice length for the target call. + let len: usize = kani::any(); + + // Call the allocator-aware fallible uninitialized slice constructor. + let _result: Result], Global>, AllocError> = + Box::<[$ty], Global>::try_new_uninit_slice_in(len, Global); + } + }; + } + + gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_i8, i8); + gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_i16, i16); + gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_i32, i32); + gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_i64, i64); + gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_i128, i128); + gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_u8, u8); + gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_u16, u16); + gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_u32, u32); + gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_u64, u64); + gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_u128, u128); + gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_unit, ()); + gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_bool, bool); + gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_array, [u8; 4]); + + macro_rules! gen_box_try_new_zeroed_slice_in_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic slice length for the target call. + let len: usize = kani::any(); + + // Call the safe constructor with the global allocator and keep + // the result typed as the exact return shape of the function. + let _result: Result], Global>, AllocError> = + Box::<[$ty], Global>::try_new_zeroed_slice_in(len, Global); + } + }; + } + + gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_i8, i8); + gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_i16, i16); + gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_i32, i32); + gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_i64, i64); + gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_i128, i128); + gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_u8, u8); + gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_u16, u16); + gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_u32, u32); + gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_u64, u64); + gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_u128, u128); + gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_unit, ()); + gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_bool, bool); + gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_array, [u8; 4]); + + macro_rules! gen_box_write_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic initialized value of the target type. + let value: $ty = kani::any(); + + // Allocate boxed storage for an uninitialized value of the same type. + let boxed: Box, Global> = + Box::<$ty, Global>::new_uninit_in(Global); + + // Write the initialized value into the boxed `MaybeUninit` slot. + let _written: Box<$ty, Global> = Box::write(boxed, value); + } + }; + } + + macro_rules! gen_box_write_vec_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic vector payload that owns heap-backed contents. + let value: Vec<$elem> = verifier_nondet_vec::<$elem>(); + + // Allocate boxed storage for an uninitialized vector value. + let boxed: Box>, Global> = + Box::, Global>::new_uninit_in(Global); + + // Write the initialized vector into the boxed `MaybeUninit` slot. + let _written: Box, Global> = Box::write(boxed, value); + } + }; + } + + gen_box_write_harness!(harness_box_write_i8, i8); + gen_box_write_harness!(harness_box_write_i16, i16); + gen_box_write_harness!(harness_box_write_i32, i32); + gen_box_write_harness!(harness_box_write_i64, i64); + gen_box_write_harness!(harness_box_write_i128, i128); + gen_box_write_harness!(harness_box_write_u8, u8); + gen_box_write_harness!(harness_box_write_u16, u16); + gen_box_write_harness!(harness_box_write_u32, u32); + gen_box_write_harness!(harness_box_write_u64, u64); + gen_box_write_harness!(harness_box_write_u128, u128); + gen_box_write_harness!(harness_box_write_unit, ()); + gen_box_write_harness!(harness_box_write_bool, bool); + gen_box_write_harness!(harness_box_write_array, [u8; 4]); + + gen_box_write_vec_harness!(harness_box_write_vec_u8, u8); + gen_box_write_vec_harness!(harness_box_write_vec_u16, u16); + gen_box_write_vec_harness!(harness_box_write_vec_u32, u32); + gen_box_write_vec_harness!(harness_box_write_vec_u64, u64); + gen_box_write_vec_harness!(harness_box_write_vec_u128, u128); + + macro_rules! gen_box_into_non_null_sized_harness { + ($name:ident, dyn Any) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value that can be coerced into `dyn Any`. + let value: i32 = kani::any(); + + // Build the concrete boxed value that will be erased behind the trait object. + let boxed_i32: Box = Box::new(value); + + // Erase the concrete type behind a boxed `dyn Any`. + let boxed: Box = boxed_i32; + + // Consume the box and extract the non-null trait-object pointer. + let ptr: NonNull = Box::::into_non_null(boxed); + + // Rebuild ownership from the non-null trait-object pointer. + let _recovered: Box = unsafe { Box::::from_non_null(ptr) }; + } + }; + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic value of the target type. + let value: $ty = kani::any(); + + // Build the boxed value whose allocation will become the non-null witness. + let boxed: Box<$ty> = Box::new(value); + + // Consume the box and extract the non-null pointer. + let ptr: NonNull<$ty> = Box::<$ty>::into_non_null(boxed); + + // Rebuild ownership from the non-null pointer. + let _recovered: Box<$ty> = unsafe { Box::<$ty>::from_non_null(ptr) }; + } + }; + } + + macro_rules! gen_box_into_non_null_unsized_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic vector whose length determines the boxed slice metadata. + let vec: Vec<$elem> = verifier_nondet_vec_box::<$elem>(); + + // Convert the vector into the boxed slice consumed by `into_non_null`. + let boxed: Box<[$elem]> = vec.into_boxed_slice(); + + // Consume the boxed slice and extract the non-null fat pointer. + let ptr: NonNull<[$elem]> = Box::<[$elem]>::into_non_null(boxed); + + // Rebuild ownership from the non-null slice pointer. + let _recovered: Box<[$elem]> = unsafe { Box::<[$elem]>::from_non_null(ptr) }; + } + }; + } + + gen_box_into_non_null_sized_harness!(harness_box_into_non_null_i8, i8); + gen_box_into_non_null_sized_harness!(harness_box_into_non_null_i16, i16); + gen_box_into_non_null_sized_harness!(harness_box_into_non_null_i32, i32); + gen_box_into_non_null_sized_harness!(harness_box_into_non_null_i64, i64); + gen_box_into_non_null_sized_harness!(harness_box_into_non_null_i128, i128); + gen_box_into_non_null_sized_harness!(harness_box_into_non_null_u8, u8); + gen_box_into_non_null_sized_harness!(harness_box_into_non_null_u16, u16); + gen_box_into_non_null_sized_harness!(harness_box_into_non_null_u32, u32); + gen_box_into_non_null_sized_harness!(harness_box_into_non_null_u64, u64); + gen_box_into_non_null_sized_harness!(harness_box_into_non_null_u128, u128); + gen_box_into_non_null_sized_harness!(harness_box_into_non_null_unit, ()); + gen_box_into_non_null_sized_harness!(harness_box_into_non_null_bool, bool); + gen_box_into_non_null_sized_harness!(harness_box_into_non_null_array, [u8; 4]); + gen_box_into_non_null_sized_harness!(harness_box_into_non_null_dyn_any, dyn Any); + + gen_box_into_non_null_unsized_harness!(harness_box_into_non_null_vec_u8, u8); + gen_box_into_non_null_unsized_harness!(harness_box_into_non_null_vec_u16, u16); + gen_box_into_non_null_unsized_harness!(harness_box_into_non_null_vec_u32, u32); + gen_box_into_non_null_unsized_harness!(harness_box_into_non_null_vec_u64, u64); + gen_box_into_non_null_unsized_harness!(harness_box_into_non_null_vec_u128, u128); + + macro_rules! gen_box_into_raw_with_allocator_sized_harness { + ($name:ident, dyn Any) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value that can be coerced into `dyn Any`. + let value: i32 = kani::any(); + + // Build the concrete boxed value that will be erased behind the trait object. + let boxed_i32: Box = Box::new_in(value, Global); + + // Erase the concrete type behind a boxed `dyn Any`. + let boxed: Box = boxed_i32; + + // Consume the box and extract the raw trait-object pointer together with its allocator. + let (ptr, alloc): (*mut dyn Any, Global) = + Box::::into_raw_with_allocator(boxed); + + // Rebuild ownership from the raw pointer and allocator pair. + let _recovered: Box = + unsafe { Box::::from_raw_in(ptr, alloc) }; + } + }; + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic value of the target type. + let value: $ty = kani::any(); + + // Build the boxed value whose allocation will become the raw-pointer witness. + let boxed: Box<$ty, Global> = Box::new_in(value, Global); + + // Consume the box and extract the raw pointer together with its allocator. + let (ptr, alloc): (*mut $ty, Global) = + Box::<$ty, Global>::into_raw_with_allocator(boxed); + + // Rebuild ownership from the raw pointer and allocator pair. + let _recovered: Box<$ty, Global> = + unsafe { Box::<$ty, Global>::from_raw_in(ptr, alloc) }; + } + }; + } + + macro_rules! gen_box_into_raw_with_allocator_unsized_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic vector whose length determines the boxed slice metadata. + let vec: Vec<$elem> = verifier_nondet_vec_box::<$elem>(); + + // Convert the vector into the boxed slice consumed by `into_raw_with_allocator`. + let boxed: Box<[$elem], Global> = vec.into_boxed_slice(); + + // Consume the boxed slice and extract the raw fat pointer together with its allocator. + let (ptr, alloc): (*mut [$elem], Global) = + Box::<[$elem], Global>::into_raw_with_allocator(boxed); + + // Rebuild ownership from the raw slice pointer and allocator pair. + let _recovered: Box<[$elem], Global> = + unsafe { Box::<[$elem], Global>::from_raw_in(ptr, alloc) }; + } + }; + } + + gen_box_into_raw_with_allocator_sized_harness!(harness_box_into_raw_with_allocator_i8, i8); + gen_box_into_raw_with_allocator_sized_harness!(harness_box_into_raw_with_allocator_i16, i16); + gen_box_into_raw_with_allocator_sized_harness!(harness_box_into_raw_with_allocator_i32, i32); + gen_box_into_raw_with_allocator_sized_harness!(harness_box_into_raw_with_allocator_i64, i64); + gen_box_into_raw_with_allocator_sized_harness!(harness_box_into_raw_with_allocator_i128, i128); + gen_box_into_raw_with_allocator_sized_harness!(harness_box_into_raw_with_allocator_u8, u8); + gen_box_into_raw_with_allocator_sized_harness!(harness_box_into_raw_with_allocator_u16, u16); + gen_box_into_raw_with_allocator_sized_harness!(harness_box_into_raw_with_allocator_u32, u32); + gen_box_into_raw_with_allocator_sized_harness!(harness_box_into_raw_with_allocator_u64, u64); + gen_box_into_raw_with_allocator_sized_harness!(harness_box_into_raw_with_allocator_u128, u128); + gen_box_into_raw_with_allocator_sized_harness!(harness_box_into_raw_with_allocator_unit, ()); + gen_box_into_raw_with_allocator_sized_harness!(harness_box_into_raw_with_allocator_bool, bool); + gen_box_into_raw_with_allocator_sized_harness!( + harness_box_into_raw_with_allocator_array, + [u8; 4] + ); + gen_box_into_raw_with_allocator_sized_harness!( + harness_box_into_raw_with_allocator_dyn_any, + dyn Any + ); + + gen_box_into_raw_with_allocator_unsized_harness!( + harness_box_into_raw_with_allocator_vec_u8, + u8 + ); + gen_box_into_raw_with_allocator_unsized_harness!( + harness_box_into_raw_with_allocator_vec_u16, + u16 + ); + gen_box_into_raw_with_allocator_unsized_harness!( + harness_box_into_raw_with_allocator_vec_u32, + u32 + ); + gen_box_into_raw_with_allocator_unsized_harness!( + harness_box_into_raw_with_allocator_vec_u64, + u64 + ); + gen_box_into_raw_with_allocator_unsized_harness!( + harness_box_into_raw_with_allocator_vec_u128, + u128 + ); + + macro_rules! gen_box_into_non_null_with_allocator_sized_harness { + ($name:ident, dyn Any) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value that can be coerced into `dyn Any`. + let value: i32 = kani::any(); + + // Build the concrete boxed value that will be erased behind the trait object. + let boxed_i32: Box = Box::new_in(value, Global); + + // Erase the concrete type behind a boxed `dyn Any`. + let boxed: Box = boxed_i32; + + // Consume the box and extract the non-null trait-object pointer together with its allocator. + let (ptr, alloc): (NonNull, Global) = + Box::::into_non_null_with_allocator(boxed); + + // Rebuild ownership from the non-null pointer and allocator pair. + let _recovered: Box = + unsafe { Box::::from_non_null_in(ptr, alloc) }; + } + }; + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic value of the target type. + let value: $ty = kani::any(); + + // Build the boxed value whose allocation will become the non-null witness. + let boxed: Box<$ty, Global> = Box::new_in(value, Global); + + // Consume the box and extract the non-null pointer together with its allocator. + let (ptr, alloc): (NonNull<$ty>, Global) = + Box::<$ty, Global>::into_non_null_with_allocator(boxed); + + // Rebuild ownership from the non-null pointer and allocator pair. + let _recovered: Box<$ty, Global> = + unsafe { Box::<$ty, Global>::from_non_null_in(ptr, alloc) }; + } + }; + } + + macro_rules! gen_box_into_non_null_with_allocator_unsized_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic vector whose length determines the boxed slice metadata. + let vec: Vec<$elem> = verifier_nondet_vec_box::<$elem>(); + + // Convert the vector into the boxed slice consumed by `into_non_null_with_allocator`. + let boxed: Box<[$elem], Global> = vec.into_boxed_slice(); + + // Consume the boxed slice and extract the non-null fat pointer together with its allocator. + let (ptr, alloc): (NonNull<[$elem]>, Global) = + Box::<[$elem], Global>::into_non_null_with_allocator(boxed); + + // Rebuild ownership from the non-null slice pointer and allocator pair. + let _recovered: Box<[$elem], Global> = + unsafe { Box::<[$elem], Global>::from_non_null_in(ptr, alloc) }; + } + }; + } + + gen_box_into_non_null_with_allocator_sized_harness!( + harness_box_into_non_null_with_allocator_i8, + i8 + ); + gen_box_into_non_null_with_allocator_sized_harness!( + harness_box_into_non_null_with_allocator_i16, + i16 + ); + gen_box_into_non_null_with_allocator_sized_harness!( + harness_box_into_non_null_with_allocator_i32, + i32 + ); + gen_box_into_non_null_with_allocator_sized_harness!( + harness_box_into_non_null_with_allocator_i64, + i64 + ); + gen_box_into_non_null_with_allocator_sized_harness!( + harness_box_into_non_null_with_allocator_i128, + i128 + ); + gen_box_into_non_null_with_allocator_sized_harness!( + harness_box_into_non_null_with_allocator_u8, + u8 + ); + gen_box_into_non_null_with_allocator_sized_harness!( + harness_box_into_non_null_with_allocator_u16, + u16 + ); + gen_box_into_non_null_with_allocator_sized_harness!( + harness_box_into_non_null_with_allocator_u32, + u32 + ); + gen_box_into_non_null_with_allocator_sized_harness!( + harness_box_into_non_null_with_allocator_u64, + u64 + ); + gen_box_into_non_null_with_allocator_sized_harness!( + harness_box_into_non_null_with_allocator_u128, + u128 + ); + gen_box_into_non_null_with_allocator_sized_harness!( + harness_box_into_non_null_with_allocator_unit, + () + ); + gen_box_into_non_null_with_allocator_sized_harness!( + harness_box_into_non_null_with_allocator_bool, + bool + ); + gen_box_into_non_null_with_allocator_sized_harness!( + harness_box_into_non_null_with_allocator_array, + [u8; 4] + ); + gen_box_into_non_null_with_allocator_sized_harness!( + harness_box_into_non_null_with_allocator_dyn_any, + dyn Any + ); + + gen_box_into_non_null_with_allocator_unsized_harness!( + harness_box_into_non_null_with_allocator_vec_u8, + u8 + ); + gen_box_into_non_null_with_allocator_unsized_harness!( + harness_box_into_non_null_with_allocator_vec_u16, + u16 + ); + gen_box_into_non_null_with_allocator_unsized_harness!( + harness_box_into_non_null_with_allocator_vec_u32, + u32 + ); + gen_box_into_non_null_with_allocator_unsized_harness!( + harness_box_into_non_null_with_allocator_vec_u64, + u64 + ); + gen_box_into_non_null_with_allocator_unsized_harness!( + harness_box_into_non_null_with_allocator_vec_u128, + u128 + ); + + macro_rules! gen_box_into_unique_sized_harness { + ($name:ident, dyn Any) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value that can be coerced into `dyn Any`. + let value: i32 = kani::any(); + + // Build the concrete boxed value that will be erased behind the trait object. + let boxed_i32: Box = Box::new_in(value, Global); + + // Erase the concrete type behind a boxed `dyn Any`. + let boxed: Box = boxed_i32; + + // Consume the box and extract the unique pointer together with its allocator. + let (ptr, alloc): (Unique, Global) = + Box::::into_unique(boxed); + + // Recover the raw pointer from the unique wrapper. + let raw: *mut dyn Any = ptr.as_ptr(); + + // Rebuild ownership from the raw pointer and allocator pair. + let _recovered: Box = + unsafe { Box::::from_raw_in(raw, alloc) }; + } + }; + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic value of the target type. + let value: $ty = kani::any(); + + // Build the boxed value whose allocation will become the unique-pointer witness. + let boxed: Box<$ty, Global> = Box::new_in(value, Global); + + // Consume the box and extract the unique pointer together with its allocator. + let (ptr, alloc): (Unique<$ty>, Global) = Box::<$ty, Global>::into_unique(boxed); + + // Recover the raw pointer from the unique wrapper. + let raw: *mut $ty = ptr.as_ptr(); + + // Rebuild ownership from the raw pointer and allocator pair. + let _recovered: Box<$ty, Global> = + unsafe { Box::<$ty, Global>::from_raw_in(raw, alloc) }; + } + }; + } + + macro_rules! gen_box_into_unique_unsized_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic vector whose length determines the boxed slice metadata. + let vec: Vec<$elem> = verifier_nondet_vec_box::<$elem>(); + + // Convert the vector into the boxed slice consumed by `into_unique`. + let boxed: Box<[$elem], Global> = vec.into_boxed_slice(); + + // Consume the boxed slice and extract the unique fat pointer together with its allocator. + let (ptr, alloc): (Unique<[$elem]>, Global) = + Box::<[$elem], Global>::into_unique(boxed); + + // Recover the raw slice pointer from the unique wrapper. + let raw: *mut [$elem] = ptr.as_ptr(); + + // Rebuild ownership from the raw slice pointer and allocator pair. + let _recovered: Box<[$elem], Global> = + unsafe { Box::<[$elem], Global>::from_raw_in(raw, alloc) }; + } + }; + } + + gen_box_into_unique_sized_harness!(harness_box_into_unique_i8, i8); + gen_box_into_unique_sized_harness!(harness_box_into_unique_i16, i16); + gen_box_into_unique_sized_harness!(harness_box_into_unique_i32, i32); + gen_box_into_unique_sized_harness!(harness_box_into_unique_i64, i64); + gen_box_into_unique_sized_harness!(harness_box_into_unique_i128, i128); + gen_box_into_unique_sized_harness!(harness_box_into_unique_u8, u8); + gen_box_into_unique_sized_harness!(harness_box_into_unique_u16, u16); + gen_box_into_unique_sized_harness!(harness_box_into_unique_u32, u32); + gen_box_into_unique_sized_harness!(harness_box_into_unique_u64, u64); + gen_box_into_unique_sized_harness!(harness_box_into_unique_u128, u128); + gen_box_into_unique_sized_harness!(harness_box_into_unique_unit, ()); + gen_box_into_unique_sized_harness!(harness_box_into_unique_bool, bool); + gen_box_into_unique_sized_harness!(harness_box_into_unique_array, [u8; 4]); + gen_box_into_unique_sized_harness!(harness_box_into_unique_dyn_any, dyn Any); + + gen_box_into_unique_unsized_harness!(harness_box_into_unique_vec_u8, u8); + gen_box_into_unique_unsized_harness!(harness_box_into_unique_vec_u16, u16); + gen_box_into_unique_unsized_harness!(harness_box_into_unique_vec_u32, u32); + gen_box_into_unique_unsized_harness!(harness_box_into_unique_vec_u64, u64); + gen_box_into_unique_unsized_harness!(harness_box_into_unique_vec_u128, u128); + + macro_rules! gen_box_leak_sized_harness { + ($name:ident, dyn Any) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value that can be coerced into `dyn Any`. + let value: i32 = kani::any(); + + // Build the concrete boxed value that will be erased behind the trait object. + let boxed_i32: Box = Box::new(value); + + // Erase the concrete type behind a boxed `dyn Any`. + let boxed: Box = boxed_i32; + + // Leak the box and obtain a mutable trait-object reference to its contents. + let leaked: &mut dyn Any = Box::::leak(boxed); + + // Recover the raw trait-object pointer from the leaked reference. + let ptr: *mut dyn Any = leaked; + + // Rebuild the box so the harness itself does not leave a permanent leak behind. + let _recovered: Box = unsafe { Box::::from_raw(ptr) }; + } + }; + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic value of the target type. + let value: $ty = kani::any(); + + // Build the boxed value that will be consumed by `leak`. + let boxed: Box<$ty> = Box::new(value); + + // Leak the box and obtain a mutable reference to its contents. + let leaked: &mut $ty = Box::<$ty>::leak(boxed); + + // Recover the raw pointer from the leaked mutable reference. + let ptr: *mut $ty = leaked; + + // Rebuild the box so the harness itself does not leave a permanent leak behind. + let _recovered: Box<$ty> = unsafe { Box::<$ty>::from_raw(ptr) }; + } + }; + } + + macro_rules! gen_box_leak_unsized_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic vector whose length determines the boxed slice metadata. + let vec: Vec<$elem> = verifier_nondet_vec_box::<$elem>(); + + // Convert the vector into the boxed slice consumed by `leak`. + let boxed: Box<[$elem]> = vec.into_boxed_slice(); + + // Leak the box and obtain a mutable slice reference to its contents. + let leaked: &mut [$elem] = Box::<[$elem]>::leak(boxed); + + // Recover the raw slice pointer from the leaked mutable reference. + let ptr: *mut [$elem] = leaked; + + // Rebuild the box so the harness itself does not leave a permanent leak behind. + let _recovered: Box<[$elem]> = unsafe { Box::<[$elem]>::from_raw(ptr) }; + } + }; + } + + gen_box_leak_sized_harness!(harness_box_leak_i8, i8); + gen_box_leak_sized_harness!(harness_box_leak_i16, i16); + gen_box_leak_sized_harness!(harness_box_leak_i32, i32); + gen_box_leak_sized_harness!(harness_box_leak_i64, i64); + gen_box_leak_sized_harness!(harness_box_leak_i128, i128); + gen_box_leak_sized_harness!(harness_box_leak_u8, u8); + gen_box_leak_sized_harness!(harness_box_leak_u16, u16); + gen_box_leak_sized_harness!(harness_box_leak_u32, u32); + gen_box_leak_sized_harness!(harness_box_leak_u64, u64); + gen_box_leak_sized_harness!(harness_box_leak_u128, u128); + gen_box_leak_sized_harness!(harness_box_leak_unit, ()); + gen_box_leak_sized_harness!(harness_box_leak_bool, bool); + gen_box_leak_sized_harness!(harness_box_leak_array, [u8; 4]); + gen_box_leak_sized_harness!(harness_box_leak_dyn_any, dyn Any); + + gen_box_leak_unsized_harness!(harness_box_leak_vec_u8, u8); + gen_box_leak_unsized_harness!(harness_box_leak_vec_u16, u16); + gen_box_leak_unsized_harness!(harness_box_leak_vec_u32, u32); + gen_box_leak_unsized_harness!(harness_box_leak_vec_u64, u64); + gen_box_leak_unsized_harness!(harness_box_leak_vec_u128, u128); + + struct NotUnpinSentinel(u8, PhantomPinned); + + macro_rules! gen_box_into_pin_harness { + ($name:ident, dyn Any) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value that can be coerced into `dyn Any`. + let value: i32 = kani::any(); + + // Build the concrete boxed value that will be erased behind the trait object. + let boxed_i32: Box = Box::new_in(value, Global); + + // Erase the concrete type behind a boxed `dyn Any`. + let boxed: Box = boxed_i32; + + // Convert the box into a pinned box without moving its contents. + let _pinned: Pin> = Box::::into_pin(boxed); + } + }; + ($name:ident, NotUnpinSentinel) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic `!Unpin` value to exercise the safety note in `into_pin`. + let value = NotUnpinSentinel(kani::any(), PhantomPinned); + + // Build the boxed value that will be pinned in place. + let boxed: Box = Box::new_in(value, Global); + + // Convert the box into a pinned box without moving its contents. + let _pinned: Pin> = + Box::::into_pin(boxed); + } + }; + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic value of the target type. + let value: $ty = kani::any(); + + // Build the boxed value that will be pinned in place. + let boxed: Box<$ty, Global> = Box::new_in(value, Global); + + // Convert the box into a pinned box without moving its contents. + let _pinned: Pin> = Box::<$ty, Global>::into_pin(boxed); + } + }; + } + + macro_rules! gen_box_into_pin_unsized_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic vector whose length determines the boxed slice metadata. + let vec: Vec<$elem> = verifier_nondet_vec_box::<$elem>(); + + // Convert the vector into the boxed slice consumed by `into_pin`. + let boxed: Box<[$elem], Global> = vec.into_boxed_slice(); + + // Convert the box into a pinned box without moving its contents. + let _pinned: Pin> = Box::<[$elem], Global>::into_pin(boxed); + } + }; + } + + gen_box_into_pin_harness!(harness_box_into_pin_i8, i8); + gen_box_into_pin_harness!(harness_box_into_pin_i16, i16); + gen_box_into_pin_harness!(harness_box_into_pin_i32, i32); + gen_box_into_pin_harness!(harness_box_into_pin_i64, i64); + gen_box_into_pin_harness!(harness_box_into_pin_i128, i128); + gen_box_into_pin_harness!(harness_box_into_pin_u8, u8); + gen_box_into_pin_harness!(harness_box_into_pin_u16, u16); + gen_box_into_pin_harness!(harness_box_into_pin_u32, u32); + gen_box_into_pin_harness!(harness_box_into_pin_u64, u64); + gen_box_into_pin_harness!(harness_box_into_pin_u128, u128); + gen_box_into_pin_harness!(harness_box_into_pin_unit, ()); + gen_box_into_pin_harness!(harness_box_into_pin_bool, bool); + gen_box_into_pin_harness!(harness_box_into_pin_array, [u8; 4]); + gen_box_into_pin_harness!(harness_box_into_pin_dyn_any, dyn Any); + gen_box_into_pin_harness!(harness_box_into_pin_not_unpin, NotUnpinSentinel); + + gen_box_into_pin_unsized_harness!(harness_box_into_pin_vec_u8, u8); + gen_box_into_pin_unsized_harness!(harness_box_into_pin_vec_u16, u16); + gen_box_into_pin_unsized_harness!(harness_box_into_pin_vec_u32, u32); + gen_box_into_pin_unsized_harness!(harness_box_into_pin_vec_u64, u64); + gen_box_into_pin_unsized_harness!(harness_box_into_pin_vec_u128, u128); + + // `Drop for Box` has one explicit control-flow split: + // - `layout.size() != 0`: after the compiler has already dropped `T`, the + // destructor computes the layout of the pointee and calls + // `self.1.deallocate(...)`. + // - `layout.size() == 0`: the destructor skips deallocation entirely. + // + // The harnesses cover that branch in three representative families: + // - sized values: `()` covers the zero-sized path, while the other scalar + // types cover the deallocation path; + // - trait objects: `dyn Any` exercises the `T: ?Sized` object case; + // - slices: `[$elem]` exercises the `T: ?Sized` slice case, and `[$elem]` + // with `$elem = ()` covers a zero-sized unsized pointee. + // + // Each harness simply constructs a `Box` and then calls `drop(boxed)`, + // which is the actual safe surface that triggers ` as Drop>::drop`. + macro_rules! gen_box_drop_harness { + ($name:ident, dyn Any) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value that can be coerced into `dyn Any`. + let value: i32 = kani::any(); + + // Build the concrete boxed value that will be erased behind the trait object. + let boxed_i32: Box = Box::new_in(value, Global); + + // Erase the concrete type behind a boxed `dyn Any`. + let boxed: Box = boxed_i32; + + // Trigger ` as Drop>::drop` through the safe surface. + drop(boxed); + } + }; + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic value of the target type. + let value: $ty = kani::any(); + + // Build the boxed value whose destructor will be exercised. + let boxed: Box<$ty, Global> = Box::new_in(value, Global); + + // Trigger ` as Drop>::drop` through the safe surface. + drop(boxed); + } + }; + } + + macro_rules! gen_box_drop_unsized_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic vector whose length determines the boxed slice metadata. + let vec: Vec<$elem> = verifier_nondet_vec_box::<$elem>(); + + // Convert the vector into the boxed slice whose destructor will be exercised. + let boxed: Box<[$elem], Global> = vec.into_boxed_slice(); + + // Trigger ` as Drop>::drop` through the safe surface. + drop(boxed); + } + }; + } + + gen_box_drop_harness!(harness_box_drop_i8, i8); + gen_box_drop_harness!(harness_box_drop_i16, i16); + gen_box_drop_harness!(harness_box_drop_i32, i32); + gen_box_drop_harness!(harness_box_drop_i64, i64); + gen_box_drop_harness!(harness_box_drop_i128, i128); + gen_box_drop_harness!(harness_box_drop_u8, u8); + gen_box_drop_harness!(harness_box_drop_u16, u16); + gen_box_drop_harness!(harness_box_drop_u32, u32); + gen_box_drop_harness!(harness_box_drop_u64, u64); + gen_box_drop_harness!(harness_box_drop_u128, u128); + gen_box_drop_harness!(harness_box_drop_unit, ()); + gen_box_drop_harness!(harness_box_drop_bool, bool); + gen_box_drop_harness!(harness_box_drop_array, [u8; 4]); + gen_box_drop_harness!(harness_box_drop_dyn_any, dyn Any); + + gen_box_drop_unsized_harness!(harness_box_drop_vec_u8, u8); + gen_box_drop_unsized_harness!(harness_box_drop_vec_u16, u16); + gen_box_drop_unsized_harness!(harness_box_drop_vec_u32, u32); + gen_box_drop_unsized_harness!(harness_box_drop_vec_u64, u64); + gen_box_drop_unsized_harness!(harness_box_drop_vec_u128, u128); + gen_box_drop_unsized_harness!(harness_box_drop_vec_unit, ()); + + macro_rules! gen_box_default_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Construct a boxed value through the `Default for Box` implementation. + let _boxed: Box<$ty> = Box::<$ty>::default(); + } + }; + } + + gen_box_default_harness!(harness_box_default_i8, i8); + gen_box_default_harness!(harness_box_default_i16, i16); + gen_box_default_harness!(harness_box_default_i32, i32); + gen_box_default_harness!(harness_box_default_i64, i64); + gen_box_default_harness!(harness_box_default_i128, i128); + gen_box_default_harness!(harness_box_default_u8, u8); + gen_box_default_harness!(harness_box_default_u16, u16); + gen_box_default_harness!(harness_box_default_u32, u32); + gen_box_default_harness!(harness_box_default_u64, u64); + gen_box_default_harness!(harness_box_default_u128, u128); + gen_box_default_harness!(harness_box_default_unit, ()); + gen_box_default_harness!(harness_box_default_array, [u8; 4]); + gen_box_default_harness!(harness_box_default_bool, bool); + gen_box_default_harness!(harness_box_default_vec_u8, Vec); + gen_box_default_harness!(harness_box_default_vec_u16, Vec); + gen_box_default_harness!(harness_box_default_vec_u32, Vec); + gen_box_default_harness!(harness_box_default_vec_u64, Vec); + gen_box_default_harness!(harness_box_default_vec_u128, Vec); + + macro_rules! gen_box_str_default_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Construct the boxed string through the dedicated `Default for Box` implementation. + let _boxed: Box<$ty> = Box::<$ty>::default(); + } + }; + } + + gen_box_str_default_harness!(harness_box_default_str, str); + + macro_rules! gen_box_clone_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic value of the target cloneable type. + let value: $ty = kani::any(); + + // Build the original boxed value whose clone path will be exercised. + let boxed: Box<$ty, Global> = Box::new_in(value, Global); + + // Clone the box through ` as Clone>::clone`. + let _clone: Box<$ty, Global> = Clone::clone(&boxed); + } + }; + } + + macro_rules! gen_box_clone_vec_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic vector payload whose own `Clone` implementation will be exercised. + let value: Vec<$elem> = verifier_nondet_vec::<$elem>(); + + // Build the original boxed vector whose clone path will be exercised. + let boxed: Box, Global> = Box::new_in(value, Global); + + // Clone the box through ` as Clone>::clone`. + let _clone: Box, Global> = Clone::clone(&boxed); + } + }; + } + + gen_box_clone_harness!(harness_box_clone_i8, i8); + gen_box_clone_harness!(harness_box_clone_i16, i16); + gen_box_clone_harness!(harness_box_clone_i32, i32); + gen_box_clone_harness!(harness_box_clone_i64, i64); + gen_box_clone_harness!(harness_box_clone_i128, i128); + gen_box_clone_harness!(harness_box_clone_u8, u8); + gen_box_clone_harness!(harness_box_clone_u16, u16); + gen_box_clone_harness!(harness_box_clone_u32, u32); + gen_box_clone_harness!(harness_box_clone_u64, u64); + gen_box_clone_harness!(harness_box_clone_u128, u128); + gen_box_clone_harness!(harness_box_clone_unit, ()); + gen_box_clone_harness!(harness_box_clone_array, [u8; 4]); + gen_box_clone_harness!(harness_box_clone_bool, bool); + + gen_box_clone_vec_harness!(harness_box_clone_vec_u8, u8); + gen_box_clone_vec_harness!(harness_box_clone_vec_u16, u16); + gen_box_clone_vec_harness!(harness_box_clone_vec_u32, u32); + gen_box_clone_vec_harness!(harness_box_clone_vec_u64, u64); + gen_box_clone_vec_harness!(harness_box_clone_vec_u128, u128); + + macro_rules! gen_box_str_clone_harness { + ($name:ident, $value:expr) => { + #[kani::proof] + pub fn $name() { + // Build the original boxed string whose clone path will be exercised. + let boxed: Box = Box::::from($value); + + // Clone the boxed string through ` as Clone>::clone`. + let _clone: Box = Clone::clone(&boxed); + } + }; + } + + gen_box_str_clone_harness!(harness_box_clone_str_empty, ""); + gen_box_str_clone_harness!(harness_box_clone_str_nonempty, "test"); +} diff --git a/library/alloc/src/boxed/convert.rs b/library/alloc/src/boxed/convert.rs index 45c46fb526365..32dfa04b954f0 100644 --- a/library/alloc/src/boxed/convert.rs +++ b/library/alloc/src/boxed/convert.rs @@ -1,5 +1,7 @@ use core::any::Any; use core::error::Error; +#[cfg(kani)] +use core::kani; use core::mem; use core::pin::Pin; #[cfg(not(no_global_oom_handling))] @@ -391,6 +393,7 @@ impl Box { /// [`downcast`]: Self::downcast #[inline] #[unstable(feature = "downcast_unchecked", issue = "90850")] + #[cfg_attr(kani, kani::requires(self.is::()))] pub unsafe fn downcast_unchecked(self) -> Box { debug_assert!(self.is::()); unsafe { @@ -450,6 +453,7 @@ impl Box { /// [`downcast`]: Self::downcast #[inline] #[unstable(feature = "downcast_unchecked", issue = "90850")] + #[cfg_attr(kani, kani::requires(self.is::()))] pub unsafe fn downcast_unchecked(self) -> Box { debug_assert!(self.is::()); unsafe { @@ -509,6 +513,7 @@ impl Box { /// [`downcast`]: Self::downcast #[inline] #[unstable(feature = "downcast_unchecked", issue = "90850")] + #[cfg_attr(kani, kani::requires(self.is::()))] pub unsafe fn downcast_unchecked(self) -> Box { debug_assert!(self.is::()); unsafe { @@ -777,3 +782,694 @@ impl dyn Error + Send + Sync { }) } } + +// ============================================================== +// Challenge 29: Verify safety of Boxed functions harnesses +// ============================================================== + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod kani_box_convert_harness_helpers { + use core::fmt; + + use super::*; + + pub trait VerifierErrorWitness { + fn verifier_any() -> Self; + } + + macro_rules! gen_verifier_error_type { + ($name:ident) => { + #[derive(Debug)] + pub struct $name; + + impl fmt::Display for $name { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, stringify!($name)) + } + } + + impl Error for $name {} + + impl VerifierErrorWitness for $name { + fn verifier_any() -> Self { + $name + } + } + }; + ($name:ident, $field:ty) => { + #[derive(Debug)] + pub struct $name(pub $field); + + impl fmt::Display for $name { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, stringify!($name)) + } + } + + impl Error for $name {} + + impl VerifierErrorWitness for $name { + fn verifier_any() -> Self { + $name(kani::any()) + } + } + }; + } + + gen_verifier_error_type!(UnitError); + gen_verifier_error_type!(ByteError, u8); + gen_verifier_error_type!(BoolError, bool); + gen_verifier_error_type!(ArrayError, [u8; 4]); + gen_verifier_error_type!(MismatchError, u8); +} + +// === UNSAFE FUNCTIONS === + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::super::kani_box_harness_helpers::*; + use super::kani_box_convert_harness_helpers::*; + use super::*; + use crate::string::String; + + // `proof_for_contract` currently fails to resolve targets such as + // `Box::downcast_unchecked::`. This is not a failure to find + // the method itself: Kani sees the inherent impl, but it does not bind the + // full target path to a single contract target when the receiver is a + // trait-object instantiation and the method is also generic. The failure + // happens during target-path resolution, before contract checking starts. + // These harnesses therefore use plain `#[kani::proof]` and restate the + // contract's key precondition explicitly with `erased.is::()`. + macro_rules! gen_downcast_unchecked_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value of the target type. + let value: $ty = kani::any(); + + // Erase the concrete type behind a `dyn Any` box. + let erased: Box = Box::new(value); + + // Restate the contract precondition that the erased value is really a `$ty`. + kani::assume(erased.is::<$ty>()); + + // Perform the unchecked downcast back to the concrete box type. + let _downcasted: Box<$ty> = + unsafe { Box::::downcast_unchecked::<$ty>(erased) }; + } + }; + } + + gen_downcast_unchecked_harness!(harness_box_dyn_any_downcast_unchecked_i8, i8); + gen_downcast_unchecked_harness!(harness_box_dyn_any_downcast_unchecked_i16, i16); + gen_downcast_unchecked_harness!(harness_box_dyn_any_downcast_unchecked_i32, i32); + gen_downcast_unchecked_harness!(harness_box_dyn_any_downcast_unchecked_i64, i64); + gen_downcast_unchecked_harness!(harness_box_dyn_any_downcast_unchecked_i128, i128); + gen_downcast_unchecked_harness!(harness_box_dyn_any_downcast_unchecked_u8, u8); + gen_downcast_unchecked_harness!(harness_box_dyn_any_downcast_unchecked_u16, u16); + gen_downcast_unchecked_harness!(harness_box_dyn_any_downcast_unchecked_u32, u32); + gen_downcast_unchecked_harness!(harness_box_dyn_any_downcast_unchecked_u64, u64); + gen_downcast_unchecked_harness!(harness_box_dyn_any_downcast_unchecked_u128, u128); + gen_downcast_unchecked_harness!(harness_box_dyn_any_downcast_unchecked_bool, bool); + gen_downcast_unchecked_harness!(harness_box_dyn_any_downcast_unchecked_unit, ()); + gen_downcast_unchecked_harness!(harness_box_dyn_any_downcast_unchecked_array, [u8; 4]); + + // `proof_for_contract` currently fails to resolve targets such as + // `Box::downcast_unchecked::`. This is not a failure to + // find the method itself: Kani sees the inherent impl, but it does not + // bind the full target path to a single contract target when the receiver + // is a trait-object instantiation and the method is also generic. The + // failure happens during target-path resolution, before contract checking + // starts. These harnesses therefore use plain `#[kani::proof]` and + // restate the contract's key precondition explicitly with `erased.is::()`. + macro_rules! gen_downcast_unchecked_send_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value of the target type. + let value: $ty = kani::any(); + + // Erase the concrete type behind a `dyn Any + Send` box. + let erased: Box = Box::new(value); + + // Restate the contract precondition that the erased value is really a `$ty`. + kani::assume(erased.is::<$ty>()); + + // Perform the unchecked downcast back to the concrete box type. + let _downcasted: Box<$ty> = + unsafe { Box::::downcast_unchecked::<$ty>(erased) }; + } + }; + } + + gen_downcast_unchecked_send_harness!(harness_box_dyn_any_send_downcast_unchecked_i8, i8); + gen_downcast_unchecked_send_harness!(harness_box_dyn_any_send_downcast_unchecked_i16, i16); + gen_downcast_unchecked_send_harness!(harness_box_dyn_any_send_downcast_unchecked_i32, i32); + gen_downcast_unchecked_send_harness!(harness_box_dyn_any_send_downcast_unchecked_i64, i64); + gen_downcast_unchecked_send_harness!(harness_box_dyn_any_send_downcast_unchecked_i128, i128); + gen_downcast_unchecked_send_harness!(harness_box_dyn_any_send_downcast_unchecked_u8, u8); + gen_downcast_unchecked_send_harness!(harness_box_dyn_any_send_downcast_unchecked_u16, u16); + gen_downcast_unchecked_send_harness!(harness_box_dyn_any_send_downcast_unchecked_u32, u32); + gen_downcast_unchecked_send_harness!(harness_box_dyn_any_send_downcast_unchecked_u64, u64); + gen_downcast_unchecked_send_harness!(harness_box_dyn_any_send_downcast_unchecked_u128, u128); + gen_downcast_unchecked_send_harness!(harness_box_dyn_any_send_downcast_unchecked_bool, bool); + gen_downcast_unchecked_send_harness!(harness_box_dyn_any_send_downcast_unchecked_unit, ()); + gen_downcast_unchecked_send_harness!( + harness_box_dyn_any_send_downcast_unchecked_array, + [u8; 4] + ); + + // `proof_for_contract` currently fails to resolve targets such as + // `Box::downcast_unchecked::`. This is not a + // failure to find the method itself: Kani sees the inherent impl, but it + // does not bind the full target path to a single contract target when the + // receiver is a trait-object instantiation and the method is also generic. + // The failure happens during target-path resolution, before contract + // checking starts. These harnesses therefore use plain `#[kani::proof]` + // and restate the contract's key precondition explicitly with + // `erased.is::()`. + macro_rules! gen_downcast_unchecked_send_sync_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value of the target type. + let value: $ty = kani::any(); + + // Erase the concrete type behind a `dyn Any + Send + Sync` box. + let erased: Box = Box::new(value); + + // Restate the contract precondition that the erased value is really a `$ty`. + kani::assume(erased.is::<$ty>()); + + // Perform the unchecked downcast back to the concrete box type. + let _downcasted: Box<$ty> = + unsafe { Box::::downcast_unchecked::<$ty>(erased) }; + } + }; + } + + gen_downcast_unchecked_send_sync_harness!( + harness_box_dyn_any_send_sync_downcast_unchecked_i8, + i8 + ); + gen_downcast_unchecked_send_sync_harness!( + harness_box_dyn_any_send_sync_downcast_unchecked_i16, + i16 + ); + gen_downcast_unchecked_send_sync_harness!( + harness_box_dyn_any_send_sync_downcast_unchecked_i32, + i32 + ); + gen_downcast_unchecked_send_sync_harness!( + harness_box_dyn_any_send_sync_downcast_unchecked_i64, + i64 + ); + gen_downcast_unchecked_send_sync_harness!( + harness_box_dyn_any_send_sync_downcast_unchecked_i128, + i128 + ); + gen_downcast_unchecked_send_sync_harness!( + harness_box_dyn_any_send_sync_downcast_unchecked_u8, + u8 + ); + gen_downcast_unchecked_send_sync_harness!( + harness_box_dyn_any_send_sync_downcast_unchecked_u16, + u16 + ); + gen_downcast_unchecked_send_sync_harness!( + harness_box_dyn_any_send_sync_downcast_unchecked_u32, + u32 + ); + gen_downcast_unchecked_send_sync_harness!( + harness_box_dyn_any_send_sync_downcast_unchecked_u64, + u64 + ); + gen_downcast_unchecked_send_sync_harness!( + harness_box_dyn_any_send_sync_downcast_unchecked_u128, + u128 + ); + gen_downcast_unchecked_send_sync_harness!( + harness_box_dyn_any_send_sync_downcast_unchecked_bool, + bool + ); + gen_downcast_unchecked_send_sync_harness!( + harness_box_dyn_any_send_sync_downcast_unchecked_unit, + () + ); + gen_downcast_unchecked_send_sync_harness!( + harness_box_dyn_any_send_sync_downcast_unchecked_array, + [u8; 4] + ); + + // === SAFE FUNCTIONS === + + macro_rules! gen_box_from_str_harness { + ($name:ident, $value:expr) => { + #[kani::proof] + pub fn $name() { + // Convert the input string slice into a boxed string through `From<&str>`. + let _boxed: Box = Box::::from($value); + } + }; + } + + gen_box_from_str_harness!(harness_box_from_str_empty, ""); + gen_box_from_str_harness!(harness_box_from_str_nonempty, "test"); + + macro_rules! gen_box_from_box_str_to_u8_slice_harness { + ($name:ident, $value:expr) => { + #[kani::proof] + pub fn $name() { + // Build the original boxed string whose backing allocation will be reinterpreted. + let boxed: Box = Box::::from($value); + + // Convert the boxed string into a boxed byte slice through `From>`. + let _boxed_bytes: Box<[u8]> = >::from(boxed); + } + }; + } + + gen_box_from_box_str_to_u8_slice_harness!(harness_box_from_box_str_to_u8_slice_empty, ""); + gen_box_from_box_str_to_u8_slice_harness!( + harness_box_from_box_str_to_u8_slice_nonempty, + "test" + ); + + // ` as TryFrom>>::try_from` branches only on + // `boxed_slice.len() == N`. + // The harness builds `boxed_slice` from a nondeterministic `Vec`, so + // the slice length is symbolic. With `N` fixed to 100, Kani explores: + // - `vec.len() == 100`: the conversion takes the `Ok(...)` path and + // reinterprets the boxed slice in place as `Box<[T; 100]>`. + // - `vec.len() != 100`: the length check fails and the conversion returns + // `Err(boxed_slice)` without reinterpreting the allocation as an array. + macro_rules! gen_box_try_from_box_slice_to_array_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic vector whose length determines the boxed slice metadata. + let vec: Vec<$ty> = verifier_nondet_vec_box::<$ty>(); + + // Convert the vector into the boxed slice consumed by `TryFrom`. + let boxed_slice: Box<[$ty]> = vec.into_boxed_slice(); + + // Fix the target array length used by the conversion attempt. + const N: usize = 100; + + // Attempt the in-place conversion from a boxed slice into a boxed array. + let _result: Result, Box<[$ty]>> = + >::try_from(boxed_slice); + } + }; + } + + gen_box_try_from_box_slice_to_array_harness!(harness_box_try_from_box_slice_to_array_i8, i8); + gen_box_try_from_box_slice_to_array_harness!(harness_box_try_from_box_slice_to_array_i16, i16); + gen_box_try_from_box_slice_to_array_harness!(harness_box_try_from_box_slice_to_array_i32, i32); + gen_box_try_from_box_slice_to_array_harness!(harness_box_try_from_box_slice_to_array_i64, i64); + gen_box_try_from_box_slice_to_array_harness!( + harness_box_try_from_box_slice_to_array_i128, + i128 + ); + gen_box_try_from_box_slice_to_array_harness!(harness_box_try_from_box_slice_to_array_u8, u8); + gen_box_try_from_box_slice_to_array_harness!(harness_box_try_from_box_slice_to_array_u16, u16); + gen_box_try_from_box_slice_to_array_harness!(harness_box_try_from_box_slice_to_array_u32, u32); + gen_box_try_from_box_slice_to_array_harness!(harness_box_try_from_box_slice_to_array_u64, u64); + gen_box_try_from_box_slice_to_array_harness!( + harness_box_try_from_box_slice_to_array_u128, + u128 + ); + gen_box_try_from_box_slice_to_array_harness!(harness_box_try_from_box_slice_to_array_unit, ()); + gen_box_try_from_box_slice_to_array_harness!( + harness_box_try_from_box_slice_to_array_array, + [u8; 4] + ); + + // ` as TryFrom>>::try_from` branches explicitly only on + // `vec.len() == N`. + // The harness keeps the input vector length nondeterministic, so with `N` + // fixed to 100, Kani explores: + // - `vec.len() == 100`: the conversion first turns the vector into + // `Box<[T]>`, then reinterprets that boxed slice in place as + // `Box<[T; 100]>`. + // - `vec.len() != 100`: the length check fails and the function returns + // `Err(vec)` without attempting the boxed-slice-to-array reinterpretation. + macro_rules! gen_box_try_from_vec_to_array_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic vector whose length drives the `TryFrom` branch. + let vec: Vec<$ty> = verifier_nondet_vec_box::<$ty>(); + + // Fix the target array length used by the conversion attempt. + const N: usize = 100; + + // Attempt the conversion from a vector directly into a boxed array. + let _result: Result, Vec<$ty>> = >::try_from(vec); + } + }; + } + + gen_box_try_from_vec_to_array_harness!(harness_box_try_from_vec_to_array_i8, i8); + gen_box_try_from_vec_to_array_harness!(harness_box_try_from_vec_to_array_i16, i16); + gen_box_try_from_vec_to_array_harness!(harness_box_try_from_vec_to_array_i32, i32); + gen_box_try_from_vec_to_array_harness!(harness_box_try_from_vec_to_array_i64, i64); + gen_box_try_from_vec_to_array_harness!(harness_box_try_from_vec_to_array_i128, i128); + gen_box_try_from_vec_to_array_harness!(harness_box_try_from_vec_to_array_u8, u8); + gen_box_try_from_vec_to_array_harness!(harness_box_try_from_vec_to_array_u16, u16); + gen_box_try_from_vec_to_array_harness!(harness_box_try_from_vec_to_array_u32, u32); + gen_box_try_from_vec_to_array_harness!(harness_box_try_from_vec_to_array_u64, u64); + gen_box_try_from_vec_to_array_harness!(harness_box_try_from_vec_to_array_u128, u128); + gen_box_try_from_vec_to_array_harness!(harness_box_try_from_vec_to_array_unit, ()); + gen_box_try_from_vec_to_array_harness!(harness_box_try_from_vec_to_array_array, [u8; 4]); + + // `Box::downcast::` branches only on `self.is::()`. + // The safe wrapper uses that runtime type test to protect the internal + // delegation to `downcast_unchecked::()`: + // - when `self.is::()` is true, the function takes the `Ok(...)` path + // and forwards to the unchecked downcast, which is safe because the + // erased value is known to have the requested concrete type; + // - when `self.is::()` is false, the function returns `Err(self)` and + // never attempts the unchecked reinterpretation. + // These harnesses cover both outcomes explicitly by constructing: + // - a matching erased box whose concrete type is exactly `$ty`; + // - a non-matching erased box whose concrete type is `String`. + macro_rules! gen_box_dyn_any_downcast_harness { + ($name:ident, $ty:ty) => { + mod $name { + use super::*; + + #[kani::proof] + pub fn ok_path() { + // Create a symbolic concrete value of the requested target type. + let value: $ty = kani::any(); + + // Erase that concrete value behind a `dyn Any` box. + let erased: Box = Box::new(value); + + // Attempt the downcast with the matching target type. + let _result: Result, Box> = erased.downcast::<$ty>(); + } + + #[kani::proof] + pub fn err_path() { + // Create a concrete string used to force a mismatched erased type. + let value: String = String::from("mismatch"); + + // Erase that string behind a `dyn Any` box. + let erased: Box = Box::new(value); + + // Attempt the downcast with a target type that does not match `String`. + let _result: Result, Box> = erased.downcast::<$ty>(); + } + } + }; + } + + gen_box_dyn_any_downcast_harness!(harness_box_dyn_any_downcast_i8, i8); + gen_box_dyn_any_downcast_harness!(harness_box_dyn_any_downcast_i16, i16); + gen_box_dyn_any_downcast_harness!(harness_box_dyn_any_downcast_i32, i32); + gen_box_dyn_any_downcast_harness!(harness_box_dyn_any_downcast_i64, i64); + gen_box_dyn_any_downcast_harness!(harness_box_dyn_any_downcast_i128, i128); + gen_box_dyn_any_downcast_harness!(harness_box_dyn_any_downcast_u8, u8); + gen_box_dyn_any_downcast_harness!(harness_box_dyn_any_downcast_u16, u16); + gen_box_dyn_any_downcast_harness!(harness_box_dyn_any_downcast_u32, u32); + gen_box_dyn_any_downcast_harness!(harness_box_dyn_any_downcast_u64, u64); + gen_box_dyn_any_downcast_harness!(harness_box_dyn_any_downcast_u128, u128); + gen_box_dyn_any_downcast_harness!(harness_box_dyn_any_downcast_unit, ()); + gen_box_dyn_any_downcast_harness!(harness_box_dyn_any_downcast_bool, bool); + gen_box_dyn_any_downcast_harness!(harness_box_dyn_any_downcast_array, [u8; 4]); + + // `Box::downcast::` branches only on `self.is::()`. + // The safe wrapper uses that runtime type test to protect the internal + // delegation to `downcast_unchecked::()`: + // - when `self.is::()` is true, the function takes the `Ok(...)` path + // and forwards to the unchecked downcast, which is safe because the + // erased value is known to have the requested concrete type; + // - when `self.is::()` is false, the function returns `Err(self)` and + // never attempts the unchecked reinterpretation. + // These harnesses cover both outcomes explicitly by constructing: + // - a matching erased box whose concrete type is exactly `$ty`; + // - a non-matching erased box whose concrete type is `String`. + macro_rules! gen_box_dyn_any_send_downcast_harness { + ($name:ident, $ty:ty) => { + mod $name { + use super::*; + + #[kani::proof] + pub fn ok_path() { + // Create a symbolic concrete value of the requested target type. + let value: $ty = kani::any(); + + // Erase that concrete value behind a `dyn Any + Send` box. + let erased: Box = Box::new(value); + + // Attempt the downcast with the matching target type. + let _result: Result, Box> = erased.downcast::<$ty>(); + } + + #[kani::proof] + pub fn err_path() { + // Create a concrete string used to force a mismatched erased type. + let value: String = String::from("mismatch"); + + // Erase that string behind a `dyn Any + Send` box. + let erased: Box = Box::new(value); + + // Attempt the downcast with a target type that does not match `String`. + let _result: Result, Box> = erased.downcast::<$ty>(); + } + } + }; + } + + gen_box_dyn_any_send_downcast_harness!(harness_box_dyn_any_send_downcast_i8, i8); + gen_box_dyn_any_send_downcast_harness!(harness_box_dyn_any_send_downcast_i16, i16); + gen_box_dyn_any_send_downcast_harness!(harness_box_dyn_any_send_downcast_i32, i32); + gen_box_dyn_any_send_downcast_harness!(harness_box_dyn_any_send_downcast_i64, i64); + gen_box_dyn_any_send_downcast_harness!(harness_box_dyn_any_send_downcast_i128, i128); + gen_box_dyn_any_send_downcast_harness!(harness_box_dyn_any_send_downcast_u8, u8); + gen_box_dyn_any_send_downcast_harness!(harness_box_dyn_any_send_downcast_u16, u16); + gen_box_dyn_any_send_downcast_harness!(harness_box_dyn_any_send_downcast_u32, u32); + gen_box_dyn_any_send_downcast_harness!(harness_box_dyn_any_send_downcast_u64, u64); + gen_box_dyn_any_send_downcast_harness!(harness_box_dyn_any_send_downcast_u128, u128); + gen_box_dyn_any_send_downcast_harness!(harness_box_dyn_any_send_downcast_unit, ()); + gen_box_dyn_any_send_downcast_harness!(harness_box_dyn_any_send_downcast_bool, bool); + gen_box_dyn_any_send_downcast_harness!(harness_box_dyn_any_send_downcast_array, [u8; 4]); + + // `Box::downcast::` branches only on + // `self.is::()`. + // The safe wrapper uses that runtime type test to protect the internal + // delegation to `downcast_unchecked::()`: + // - when `self.is::()` is true, the function takes the `Ok(...)` path + // and forwards to the unchecked downcast, which is safe because the + // erased value is known to have the requested concrete type; + // - when `self.is::()` is false, the function returns `Err(self)` and + // never attempts the unchecked reinterpretation. + // These harnesses cover both outcomes explicitly by constructing: + // - a matching erased box whose concrete type is exactly `$ty`; + // - a non-matching erased box whose concrete type is `String`. + macro_rules! gen_box_dyn_any_send_sync_downcast_harness { + ($name:ident, $ty:ty) => { + mod $name { + use super::*; + + #[kani::proof] + pub fn ok_path() { + // Create a symbolic concrete value of the requested target type. + let value: $ty = kani::any(); + + // Erase that concrete value behind a `dyn Any + Send + Sync` box. + let erased: Box = Box::new(value); + + // Attempt the downcast with the matching target type. + let _result: Result, Box> = + erased.downcast::<$ty>(); + } + + #[kani::proof] + pub fn err_path() { + // Create a concrete string used to force a mismatched erased type. + let value: String = String::from("mismatch"); + + // Erase that string behind a `dyn Any + Send + Sync` box. + let erased: Box = Box::new(value); + + // Attempt the downcast with a target type that does not match `String`. + let _result: Result, Box> = + erased.downcast::<$ty>(); + } + } + }; + } + + gen_box_dyn_any_send_sync_downcast_harness!(harness_box_dyn_any_send_sync_downcast_i8, i8); + gen_box_dyn_any_send_sync_downcast_harness!(harness_box_dyn_any_send_sync_downcast_i16, i16); + gen_box_dyn_any_send_sync_downcast_harness!(harness_box_dyn_any_send_sync_downcast_i32, i32); + gen_box_dyn_any_send_sync_downcast_harness!(harness_box_dyn_any_send_sync_downcast_i64, i64); + gen_box_dyn_any_send_sync_downcast_harness!(harness_box_dyn_any_send_sync_downcast_i128, i128); + gen_box_dyn_any_send_sync_downcast_harness!(harness_box_dyn_any_send_sync_downcast_u8, u8); + gen_box_dyn_any_send_sync_downcast_harness!(harness_box_dyn_any_send_sync_downcast_u16, u16); + gen_box_dyn_any_send_sync_downcast_harness!(harness_box_dyn_any_send_sync_downcast_u32, u32); + gen_box_dyn_any_send_sync_downcast_harness!(harness_box_dyn_any_send_sync_downcast_u64, u64); + gen_box_dyn_any_send_sync_downcast_harness!(harness_box_dyn_any_send_sync_downcast_u128, u128); + gen_box_dyn_any_send_sync_downcast_harness!(harness_box_dyn_any_send_sync_downcast_unit, ()); + gen_box_dyn_any_send_sync_downcast_harness!(harness_box_dyn_any_send_sync_downcast_bool, bool); + gen_box_dyn_any_send_sync_downcast_harness!( + harness_box_dyn_any_send_sync_downcast_array, + [u8; 4] + ); + + // `::downcast::` branches only on `self.is::()`. + // The safe wrapper uses that runtime type test to protect the raw pointer + // reinterpretation in the `Ok(...)` path: + // - when `self.is::()` is true, the function extracts the raw + // `dyn Error` pointer from the box and reinterprets it as `*mut T`, + // which is safe because the erased value is known to have concrete type + // `T`; + // - when `self.is::()` is false, the function returns `Err(self)` and + // never performs the pointer reinterpretation. + macro_rules! gen_box_dyn_error_downcast_harness { + ($name:ident, $ty:ty) => { + mod $name { + use super::*; + + #[kani::proof] + pub fn ok_path() { + // Create a concrete error value of the requested target type. + let value: $ty = <$ty as VerifierErrorWitness>::verifier_any(); + + // Erase that concrete error behind a `dyn Error` box. + let erased: Box = Box::new(value); + + // Attempt the downcast with the matching target type. + let _result: Result, Box> = erased.downcast::<$ty>(); + } + + #[kani::proof] + pub fn err_path() { + // Create a mismatched concrete error value. + let value: MismatchError = MismatchError(kani::any()); + + // Erase that mismatched value behind a `dyn Error` box. + let erased: Box = Box::new(value); + + // Attempt the downcast with a target type that does not match `MismatchError`. + let _result: Result, Box> = erased.downcast::<$ty>(); + } + } + }; + } + + gen_box_dyn_error_downcast_harness!(harness_box_dyn_error_downcast_unit, UnitError); + gen_box_dyn_error_downcast_harness!(harness_box_dyn_error_downcast_byte, ByteError); + gen_box_dyn_error_downcast_harness!(harness_box_dyn_error_downcast_bool, BoolError); + gen_box_dyn_error_downcast_harness!(harness_box_dyn_error_downcast_array, ArrayError); + + // `::downcast::` delegates to `::downcast` + // after first coercing `Box` into `Box`. + // Its explicit branch behavior is therefore still determined by + // `self.is::()` inside the shared `dyn Error` downcast logic: + // - when the erased error really has concrete type `T`, the delegated + // `dyn Error` downcast returns `Ok(Box)`; + // - otherwise the delegated call returns `Err(Box)`, and this + // wrapper re-applies the `Send` marker with `mem::transmute`. + macro_rules! gen_box_dyn_error_send_downcast_harness { + ($name:ident, $ty:ty) => { + mod $name { + use super::*; + + #[kani::proof] + pub fn ok_path() { + // Create a concrete error value of the requested target type. + let value: $ty = <$ty as VerifierErrorWitness>::verifier_any(); + + // Erase that concrete error behind a `dyn Error + Send` box. + let erased: Box = Box::new(value); + + // Attempt the downcast with the matching target type. + let _result: Result, Box> = erased.downcast::<$ty>(); + } + + #[kani::proof] + pub fn err_path() { + // Create a mismatched concrete error value. + let value: MismatchError = MismatchError(kani::any()); + + // Erase that mismatched value behind a `dyn Error + Send` box. + let erased: Box = Box::new(value); + + // Attempt the downcast with a target type that does not match `MismatchError`. + let _result: Result, Box> = erased.downcast::<$ty>(); + } + } + }; + } + + gen_box_dyn_error_send_downcast_harness!(harness_box_dyn_error_send_downcast_unit, UnitError); + gen_box_dyn_error_send_downcast_harness!(harness_box_dyn_error_send_downcast_byte, ByteError); + gen_box_dyn_error_send_downcast_harness!(harness_box_dyn_error_send_downcast_bool, BoolError); + gen_box_dyn_error_send_downcast_harness!(harness_box_dyn_error_send_downcast_array, ArrayError); + + // `::downcast::` also delegates to + // `::downcast` after coercing the boxed trait object to + // `Box`. + // The branch structure is therefore again inherited from the shared + // `dyn Error` downcast logic: + // - when the erased error really has concrete type `T`, the delegated + // `dyn Error` downcast returns `Ok(Box)`; + // - otherwise the delegated call returns `Err(Box)`, and this + // wrapper re-applies the `Send + Sync` markers with `mem::transmute`. + macro_rules! gen_box_dyn_error_send_sync_downcast_harness { + ($name:ident, $ty:ty) => { + mod $name { + use super::*; + + #[kani::proof] + pub fn ok_path() { + // Create a concrete error value of the requested target type. + let value: $ty = <$ty as VerifierErrorWitness>::verifier_any(); + + // Erase that concrete error behind a `dyn Error + Send + Sync` box. + let erased: Box = Box::new(value); + + // Attempt the downcast with the matching target type. + let _result: Result, Box> = + erased.downcast::<$ty>(); + } + + #[kani::proof] + pub fn err_path() { + // Create a mismatched concrete error value. + let value: MismatchError = MismatchError(kani::any()); + + // Erase that mismatched value behind a `dyn Error + Send + Sync` box. + let erased: Box = Box::new(value); + + // Attempt the downcast with a target type that does not match `MismatchError`. + let _result: Result, Box> = + erased.downcast::<$ty>(); + } + } + }; + } + + gen_box_dyn_error_send_sync_downcast_harness!( + harness_box_dyn_error_send_sync_downcast_unit, + UnitError + ); + gen_box_dyn_error_send_sync_downcast_harness!( + harness_box_dyn_error_send_sync_downcast_byte, + ByteError + ); + gen_box_dyn_error_send_sync_downcast_harness!( + harness_box_dyn_error_send_sync_downcast_bool, + BoolError + ); + gen_box_dyn_error_send_sync_downcast_harness!( + harness_box_dyn_error_send_sync_downcast_array, + ArrayError + ); +} diff --git a/library/alloc/src/boxed/thin.rs b/library/alloc/src/boxed/thin.rs index 1cce36606d2c0..f335a8b3098c6 100644 --- a/library/alloc/src/boxed/thin.rs +++ b/library/alloc/src/boxed/thin.rs @@ -6,6 +6,8 @@ use core::error::Error; use core::fmt::{self, Debug, Display, Formatter}; #[cfg(not(no_global_oom_handling))] use core::intrinsics::{const_allocate, const_make_global}; +#[cfg(kani)] +use core::kani; use core::marker::PhantomData; #[cfg(not(no_global_oom_handling))] use core::marker::Unsize; @@ -430,3 +432,688 @@ impl Error for ThinBox { self.deref().source() } } + +// ============================================================== +// Challenge 29: Verify safety of Boxed functions harnesses +// ============================================================== + +// === SAFE FUNCTIONS === + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use core::any::Any; + + use super::*; + + macro_rules! gen_thinbox_deref_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value of the requested sized type. + let value: $ty = kani::any(); + + // Move that value into a `ThinBox` using the sized constructor. + let thin: ThinBox<$ty> = ThinBox::new(value); + + // Dereference the thin box through the `Deref` implementation. + let _: &$ty = core::ops::Deref::deref(&thin); + } + }; + } + + macro_rules! gen_thinbox_deref_dyn_any_harness { + ($name:ident, $src_ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value that will be unsized into `dyn Any`. + let value: $src_ty = kani::any(); + + // Build a thin box whose pointee metadata is trait-object metadata. + let thin: ThinBox = ThinBox::::new_unsize(value); + + // Dereference the thin box through the `Deref` implementation. + let _: &dyn Any = core::ops::Deref::deref(&thin); + } + }; + } + + macro_rules! gen_thinbox_deref_slice_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Build a non-empty array that will be unsized into a slice. + let value: [$elem; 4] = [kani::any::<$elem>(); 4]; + + // Build a thin box whose pointee metadata is slice length metadata. + let thin: ThinBox<[$elem]> = ThinBox::<[$elem]>::new_unsize(value); + + // Dereference the thin box through the `Deref` implementation. + let _: &[$elem] = core::ops::Deref::deref(&thin); + } + }; + } + + gen_thinbox_deref_harness!(harness_thinbox_deref_i8, i8); + gen_thinbox_deref_harness!(harness_thinbox_deref_i16, i16); + gen_thinbox_deref_harness!(harness_thinbox_deref_i32, i32); + gen_thinbox_deref_harness!(harness_thinbox_deref_i64, i64); + gen_thinbox_deref_harness!(harness_thinbox_deref_i128, i128); + gen_thinbox_deref_harness!(harness_thinbox_deref_u8, u8); + gen_thinbox_deref_harness!(harness_thinbox_deref_u16, u16); + gen_thinbox_deref_harness!(harness_thinbox_deref_u32, u32); + gen_thinbox_deref_harness!(harness_thinbox_deref_u64, u64); + gen_thinbox_deref_harness!(harness_thinbox_deref_u128, u128); + gen_thinbox_deref_harness!(harness_thinbox_deref_bool, bool); + gen_thinbox_deref_harness!(harness_thinbox_deref_unit, ()); + gen_thinbox_deref_harness!(harness_thinbox_deref_array, [u8; 4]); + gen_thinbox_deref_dyn_any_harness!(harness_thinbox_deref_dyn_any, i32); + + gen_thinbox_deref_slice_harness!(harness_thinbox_deref_slice_u8, u8); + gen_thinbox_deref_slice_harness!(harness_thinbox_deref_slice_u16, u16); + gen_thinbox_deref_slice_harness!(harness_thinbox_deref_slice_u32, u32); + gen_thinbox_deref_slice_harness!(harness_thinbox_deref_slice_u64, u64); + gen_thinbox_deref_slice_harness!(harness_thinbox_deref_slice_u128, u128); + + macro_rules! gen_thinbox_deref_mut_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value of the requested sized type. + let value: $ty = kani::any(); + + // Move that value into a mutable `ThinBox` using the sized constructor. + let mut thin: ThinBox<$ty> = ThinBox::new(value); + + // Mutably dereference the thin box through the `DerefMut` implementation. + let _: &mut $ty = core::ops::DerefMut::deref_mut(&mut thin); + } + }; + } + + macro_rules! gen_thinbox_deref_mut_dyn_any_harness { + ($name:ident, $src_ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value that will be unsized into `dyn Any`. + let value: $src_ty = kani::any(); + + // Build a mutable thin box whose pointee metadata is trait-object metadata. + let mut thin: ThinBox = ThinBox::::new_unsize(value); + + // Mutably dereference the thin box through the `DerefMut` implementation. + let _: &mut dyn Any = core::ops::DerefMut::deref_mut(&mut thin); + } + }; + } + + macro_rules! gen_thinbox_deref_mut_slice_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Build a non-empty array that will be unsized into a slice. + let value: [$elem; 4] = [kani::any::<$elem>(); 4]; + + // Build a mutable thin box whose pointee metadata is slice length metadata. + let mut thin: ThinBox<[$elem]> = ThinBox::<[$elem]>::new_unsize(value); + + // Mutably dereference the thin box through the `DerefMut` implementation. + let _: &mut [$elem] = core::ops::DerefMut::deref_mut(&mut thin); + } + }; + } + + gen_thinbox_deref_mut_harness!(harness_thinbox_deref_mut_i8, i8); + gen_thinbox_deref_mut_harness!(harness_thinbox_deref_mut_i16, i16); + gen_thinbox_deref_mut_harness!(harness_thinbox_deref_mut_i32, i32); + gen_thinbox_deref_mut_harness!(harness_thinbox_deref_mut_i64, i64); + gen_thinbox_deref_mut_harness!(harness_thinbox_deref_mut_i128, i128); + gen_thinbox_deref_mut_harness!(harness_thinbox_deref_mut_u8, u8); + gen_thinbox_deref_mut_harness!(harness_thinbox_deref_mut_u16, u16); + gen_thinbox_deref_mut_harness!(harness_thinbox_deref_mut_u32, u32); + gen_thinbox_deref_mut_harness!(harness_thinbox_deref_mut_u64, u64); + gen_thinbox_deref_mut_harness!(harness_thinbox_deref_mut_u128, u128); + gen_thinbox_deref_mut_harness!(harness_thinbox_deref_mut_bool, bool); + gen_thinbox_deref_mut_harness!(harness_thinbox_deref_mut_unit, ()); + gen_thinbox_deref_mut_harness!(harness_thinbox_deref_mut_array, [u8; 4]); + gen_thinbox_deref_mut_dyn_any_harness!(harness_thinbox_deref_mut_dyn_any, i32); + + gen_thinbox_deref_mut_slice_harness!(harness_thinbox_deref_mut_slice_u8, u8); + gen_thinbox_deref_mut_slice_harness!(harness_thinbox_deref_mut_slice_u16, u16); + gen_thinbox_deref_mut_slice_harness!(harness_thinbox_deref_mut_slice_u32, u32); + gen_thinbox_deref_mut_slice_harness!(harness_thinbox_deref_mut_slice_u64, u64); + gen_thinbox_deref_mut_slice_harness!(harness_thinbox_deref_mut_slice_u128, u128); + + macro_rules! gen_thinbox_drop_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value of the requested sized type. + let value: $ty = kani::any(); + + // Move that value into a `ThinBox` using the sized constructor. + let thin: ThinBox<$ty> = ThinBox::new(value); + + // Drop the thin box through the normal safe surface. + core::mem::drop(thin); + } + }; + } + + macro_rules! gen_thinbox_drop_dyn_any_harness { + ($name:ident, $src_ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value that will be unsized into `dyn Any`. + let value: $src_ty = kani::any(); + + // Build a thin box whose pointee metadata is trait-object metadata. + let thin: ThinBox = ThinBox::::new_unsize(value); + + // Drop the thin box through the normal safe surface. + core::mem::drop(thin); + } + }; + } + + macro_rules! gen_thinbox_drop_slice_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Build a non-empty array that will be unsized into a slice. + let value: [$elem; 4] = [kani::any::<$elem>(); 4]; + + // Build a thin box whose pointee metadata is slice length metadata. + let thin: ThinBox<[$elem]> = ThinBox::<[$elem]>::new_unsize(value); + + // Drop the thin box through the normal safe surface. + core::mem::drop(thin); + } + }; + } + + gen_thinbox_drop_harness!(harness_thinbox_drop_i8, i8); + gen_thinbox_drop_harness!(harness_thinbox_drop_i16, i16); + gen_thinbox_drop_harness!(harness_thinbox_drop_i32, i32); + gen_thinbox_drop_harness!(harness_thinbox_drop_i64, i64); + gen_thinbox_drop_harness!(harness_thinbox_drop_i128, i128); + gen_thinbox_drop_harness!(harness_thinbox_drop_u8, u8); + gen_thinbox_drop_harness!(harness_thinbox_drop_u16, u16); + gen_thinbox_drop_harness!(harness_thinbox_drop_u32, u32); + gen_thinbox_drop_harness!(harness_thinbox_drop_u64, u64); + gen_thinbox_drop_harness!(harness_thinbox_drop_u128, u128); + gen_thinbox_drop_harness!(harness_thinbox_drop_bool, bool); + gen_thinbox_drop_harness!(harness_thinbox_drop_unit, ()); + gen_thinbox_drop_harness!(harness_thinbox_drop_array, [u8; 4]); + gen_thinbox_drop_dyn_any_harness!(harness_thinbox_drop_dyn_any, i32); + + gen_thinbox_drop_slice_harness!(harness_thinbox_drop_slice_u8, u8); + gen_thinbox_drop_slice_harness!(harness_thinbox_drop_slice_u16, u16); + gen_thinbox_drop_slice_harness!(harness_thinbox_drop_slice_u32, u32); + gen_thinbox_drop_slice_harness!(harness_thinbox_drop_slice_u64, u64); + gen_thinbox_drop_slice_harness!(harness_thinbox_drop_slice_u128, u128); + + macro_rules! gen_thinbox_meta_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value of the requested sized type. + let value: $ty = kani::any(); + + // Move that value into a `ThinBox` using the sized constructor. + let thin: ThinBox<$ty> = ThinBox::new(value); + + // Read the metadata stored in the thin box header. + let _metadata: <$ty as Pointee>::Metadata = thin.meta(); + } + }; + } + + macro_rules! gen_thinbox_meta_dyn_any_harness { + ($name:ident, $src_ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value that will be unsized into `dyn Any`. + let value: $src_ty = kani::any(); + + // Build a thin box whose pointee metadata is trait-object metadata. + let thin: ThinBox = ThinBox::::new_unsize(value); + + // Read the trait-object metadata stored in the thin box header. + let _metadata: ::Metadata = thin.meta(); + } + }; + } + + macro_rules! gen_thinbox_meta_slice_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Build a non-empty array that will be unsized into a slice. + let value: [$elem; 4] = [kani::any::<$elem>(); 4]; + + // Build a thin box whose pointee metadata is slice length metadata. + let thin: ThinBox<[$elem]> = ThinBox::<[$elem]>::new_unsize(value); + + // Read the slice metadata stored in the thin box header. + let _metadata: <[$elem] as Pointee>::Metadata = thin.meta(); + } + }; + } + + gen_thinbox_meta_harness!(harness_thinbox_meta_i8, i8); + gen_thinbox_meta_harness!(harness_thinbox_meta_i16, i16); + gen_thinbox_meta_harness!(harness_thinbox_meta_i32, i32); + gen_thinbox_meta_harness!(harness_thinbox_meta_i64, i64); + gen_thinbox_meta_harness!(harness_thinbox_meta_i128, i128); + gen_thinbox_meta_harness!(harness_thinbox_meta_u8, u8); + gen_thinbox_meta_harness!(harness_thinbox_meta_u16, u16); + gen_thinbox_meta_harness!(harness_thinbox_meta_u32, u32); + gen_thinbox_meta_harness!(harness_thinbox_meta_u64, u64); + gen_thinbox_meta_harness!(harness_thinbox_meta_u128, u128); + gen_thinbox_meta_harness!(harness_thinbox_meta_bool, bool); + gen_thinbox_meta_harness!(harness_thinbox_meta_unit, ()); + gen_thinbox_meta_harness!(harness_thinbox_meta_array, [u8; 4]); + gen_thinbox_meta_dyn_any_harness!(harness_thinbox_meta_dyn_any, i32); + + gen_thinbox_meta_slice_harness!(harness_thinbox_meta_slice_u8, u8); + gen_thinbox_meta_slice_harness!(harness_thinbox_meta_slice_u16, u16); + gen_thinbox_meta_slice_harness!(harness_thinbox_meta_slice_u32, u32); + gen_thinbox_meta_slice_harness!(harness_thinbox_meta_slice_u64, u64); + gen_thinbox_meta_slice_harness!(harness_thinbox_meta_slice_u128, u128); + + macro_rules! gen_thinbox_with_header_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value of the requested sized type. + let value: $ty = kani::any(); + + // Move that value into a `ThinBox` using the sized constructor. + let thin: ThinBox<$ty> = ThinBox::new(value); + + // Recover the typed header view from the opaque thin-box representation. + let _header = thin.with_header(); + } + }; + } + + macro_rules! gen_thinbox_with_header_dyn_any_harness { + ($name:ident, $src_ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value that will be unsized into `dyn Any`. + let value: $src_ty = kani::any(); + + // Build a thin box whose header stores trait-object metadata. + let thin: ThinBox = ThinBox::::new_unsize(value); + + // Recover the typed header view from the opaque thin-box representation. + let _header = thin.with_header(); + } + }; + } + + macro_rules! gen_thinbox_with_header_slice_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Build a non-empty array that will be unsized into a slice. + let value: [$elem; 4] = [kani::any::<$elem>(); 4]; + + // Build a thin box whose header stores slice length metadata. + let thin: ThinBox<[$elem]> = ThinBox::<[$elem]>::new_unsize(value); + + // Recover the typed header view from the opaque thin-box representation. + let _header = thin.with_header(); + } + }; + } + + gen_thinbox_with_header_harness!(harness_thinbox_with_header_i8, i8); + gen_thinbox_with_header_harness!(harness_thinbox_with_header_i16, i16); + gen_thinbox_with_header_harness!(harness_thinbox_with_header_i32, i32); + gen_thinbox_with_header_harness!(harness_thinbox_with_header_i64, i64); + gen_thinbox_with_header_harness!(harness_thinbox_with_header_i128, i128); + gen_thinbox_with_header_harness!(harness_thinbox_with_header_u8, u8); + gen_thinbox_with_header_harness!(harness_thinbox_with_header_u16, u16); + gen_thinbox_with_header_harness!(harness_thinbox_with_header_u32, u32); + gen_thinbox_with_header_harness!(harness_thinbox_with_header_u64, u64); + gen_thinbox_with_header_harness!(harness_thinbox_with_header_u128, u128); + gen_thinbox_with_header_harness!(harness_thinbox_with_header_bool, bool); + gen_thinbox_with_header_harness!(harness_thinbox_with_header_unit, ()); + gen_thinbox_with_header_harness!(harness_thinbox_with_header_array, [u8; 4]); + gen_thinbox_with_header_dyn_any_harness!(harness_thinbox_with_header_dyn_any, i32); + + gen_thinbox_with_header_slice_harness!(harness_thinbox_with_header_slice_u8, u8); + gen_thinbox_with_header_slice_harness!(harness_thinbox_with_header_slice_u16, u16); + gen_thinbox_with_header_slice_harness!(harness_thinbox_with_header_slice_u32, u32); + gen_thinbox_with_header_slice_harness!(harness_thinbox_with_header_slice_u64, u64); + gen_thinbox_with_header_slice_harness!(harness_thinbox_with_header_slice_u128, u128); + + macro_rules! gen_with_header_new_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value of the requested sized type. + let value: $ty = kani::any(); + + // Compute the metadata header that belongs to this sized value. + let header: <$ty as Pointee>::Metadata = ptr::metadata(&value); + + // Build the raw header/value allocation used by `ThinBox`. + let with_header: WithHeader<<$ty as Pointee>::Metadata> = + WithHeader::new(header, value); + + // Rewrap the raw allocation as a `ThinBox` so normal drop cleans it up. + let _thin: ThinBox<$ty> = + ThinBox { ptr: WithOpaqueHeader(with_header.0), _marker: PhantomData }; + } + }; + } + + macro_rules! gen_with_header_new_dyn_any_harness { + ($name:ident, $src_ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value that will be represented as `dyn Any`. + let value: $src_ty = kani::any(); + + // Compute the trait-object metadata header for the erased pointee type. + let header: ::Metadata = ptr::metadata(&value as &dyn Any); + + // Build the raw header/value allocation used by `ThinBox`. + let with_header: WithHeader<::Metadata> = + WithHeader::new(header, value); + + // Rewrap the raw allocation as a `ThinBox` so normal drop cleans it up. + let _thin: ThinBox = + ThinBox { ptr: WithOpaqueHeader(with_header.0), _marker: PhantomData }; + } + }; + } + + macro_rules! gen_with_header_new_slice_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Build a non-empty array that will be represented as a slice. + let value: [$elem; 4] = [kani::any::<$elem>(); 4]; + + // Compute the slice-length metadata header for the unsized pointee type. + let header: <[$elem] as Pointee>::Metadata = ptr::metadata(&value as &[$elem]); + + // Build the raw header/value allocation used by `ThinBox<[$elem]>`. + let with_header: WithHeader<<[$elem] as Pointee>::Metadata> = + WithHeader::new(header, value); + + // Rewrap the raw allocation as a `ThinBox<[$elem]>` so normal drop cleans it up. + let _thin: ThinBox<[$elem]> = + ThinBox { ptr: WithOpaqueHeader(with_header.0), _marker: PhantomData }; + } + }; + } + + gen_with_header_new_harness!(harness_with_header_new_i8, i8); + gen_with_header_new_harness!(harness_with_header_new_i16, i16); + gen_with_header_new_harness!(harness_with_header_new_i32, i32); + gen_with_header_new_harness!(harness_with_header_new_i64, i64); + gen_with_header_new_harness!(harness_with_header_new_i128, i128); + gen_with_header_new_harness!(harness_with_header_new_u8, u8); + gen_with_header_new_harness!(harness_with_header_new_u16, u16); + gen_with_header_new_harness!(harness_with_header_new_u32, u32); + gen_with_header_new_harness!(harness_with_header_new_u64, u64); + gen_with_header_new_harness!(harness_with_header_new_u128, u128); + gen_with_header_new_harness!(harness_with_header_new_bool, bool); + gen_with_header_new_harness!(harness_with_header_new_unit, ()); + gen_with_header_new_harness!(harness_with_header_new_array, [u8; 4]); + gen_with_header_new_dyn_any_harness!(harness_with_header_new_dyn_any, i32); + + gen_with_header_new_slice_harness!(harness_with_header_new_slice_u8, u8); + gen_with_header_new_slice_harness!(harness_with_header_new_slice_u16, u16); + gen_with_header_new_slice_harness!(harness_with_header_new_slice_u32, u32); + gen_with_header_new_slice_harness!(harness_with_header_new_slice_u64, u64); + gen_with_header_new_slice_harness!(harness_with_header_new_slice_u128, u128); + + macro_rules! gen_with_header_try_new_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value of the requested sized type. + let value: $ty = kani::any(); + + // Compute the metadata header that belongs to this sized value. + let header: <$ty as Pointee>::Metadata = ptr::metadata(&value); + + // Build the fallible raw header/value allocation used by `ThinBox`. + let result: Result< + WithHeader<<$ty as Pointee>::Metadata>, + core::alloc::AllocError, + > = WithHeader::try_new(header, value); + + // Rewrap successful allocations as `ThinBox` so normal drop cleans them up. + let _result: Result, core::alloc::AllocError> = + result.map(|with_header| ThinBox { + ptr: WithOpaqueHeader(with_header.0), + _marker: PhantomData, + }); + } + }; + } + + macro_rules! gen_with_header_try_new_dyn_any_harness { + ($name:ident, $src_ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value that will be represented as `dyn Any`. + let value: $src_ty = kani::any(); + + // Compute the trait-object metadata header for the erased pointee type. + let header: ::Metadata = ptr::metadata(&value as &dyn Any); + + // Build the fallible raw header/value allocation used by `ThinBox`. + let result: Result< + WithHeader<::Metadata>, + core::alloc::AllocError, + > = WithHeader::try_new(header, value); + + // Rewrap successful allocations as `ThinBox` so normal drop cleans them up. + let _result: Result, core::alloc::AllocError> = + result.map(|with_header| ThinBox { + ptr: WithOpaqueHeader(with_header.0), + _marker: PhantomData, + }); + } + }; + } + + macro_rules! gen_with_header_try_new_slice_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Build a non-empty array that will be represented as a slice. + let value: [$elem; 4] = [kani::any::<$elem>(); 4]; + + // Compute the slice-length metadata header for the unsized pointee type. + let header: <[$elem] as Pointee>::Metadata = ptr::metadata(&value as &[$elem]); + + // Build the fallible raw header/value allocation used by `ThinBox<[$elem]>`. + let result: Result< + WithHeader<<[$elem] as Pointee>::Metadata>, + core::alloc::AllocError, + > = WithHeader::try_new(header, value); + + // Rewrap successful allocations as `ThinBox<[$elem]>` so normal drop cleans them up. + let _result: Result, core::alloc::AllocError> = + result.map(|with_header| ThinBox { + ptr: WithOpaqueHeader(with_header.0), + _marker: PhantomData, + }); + } + }; + } + + gen_with_header_try_new_harness!(harness_with_header_try_new_i8, i8); + gen_with_header_try_new_harness!(harness_with_header_try_new_i16, i16); + gen_with_header_try_new_harness!(harness_with_header_try_new_i32, i32); + gen_with_header_try_new_harness!(harness_with_header_try_new_i64, i64); + gen_with_header_try_new_harness!(harness_with_header_try_new_i128, i128); + gen_with_header_try_new_harness!(harness_with_header_try_new_u8, u8); + gen_with_header_try_new_harness!(harness_with_header_try_new_u16, u16); + gen_with_header_try_new_harness!(harness_with_header_try_new_u32, u32); + gen_with_header_try_new_harness!(harness_with_header_try_new_u64, u64); + gen_with_header_try_new_harness!(harness_with_header_try_new_u128, u128); + gen_with_header_try_new_harness!(harness_with_header_try_new_bool, bool); + gen_with_header_try_new_harness!(harness_with_header_try_new_unit, ()); + gen_with_header_try_new_harness!(harness_with_header_try_new_array, [u8; 4]); + gen_with_header_try_new_dyn_any_harness!(harness_with_header_try_new_dyn_any, i32); + + gen_with_header_try_new_slice_harness!(harness_with_header_try_new_slice_u8, u8); + gen_with_header_try_new_slice_harness!(harness_with_header_try_new_slice_u16, u16); + gen_with_header_try_new_slice_harness!(harness_with_header_try_new_slice_u32, u32); + gen_with_header_try_new_slice_harness!(harness_with_header_try_new_slice_u64, u64); + gen_with_header_try_new_slice_harness!(harness_with_header_try_new_slice_u128, u128); + // `WithHeader::new_unsize_zst` is the special constructor used + // when a zero-sized source `T` is unsized into some `Dyn`. + macro_rules! gen_with_header_new_unsize_zst_slice_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Build a zero-length array that can be unsized into a slice. + let value: [$elem; 0] = []; + + // Build the special ZST-unsizing header/value representation. + let _with_header: WithHeader<<[$elem] as Pointee>::Metadata> = + WithHeader::new_unsize_zst::<[$elem], [$elem; 0]>(value); + } + }; + } + + macro_rules! gen_with_header_new_unsize_zst_dyn_any_harness { + ($name:ident, $src_ty:ty) => { + #[kani::proof] + pub fn $name() { + // Build a zero-sized concrete value that can be unsized into `dyn Any`. + let value: $src_ty = <$src_ty>::default(); + + // Build the special ZST-unsizing header/value representation. + let _with_header: WithHeader<::Metadata> = + WithHeader::new_unsize_zst::(value); + } + }; + } + + gen_with_header_new_unsize_zst_slice_harness!(harness_with_header_new_unsize_zst_slice_u8, u8); + gen_with_header_new_unsize_zst_slice_harness!( + harness_with_header_new_unsize_zst_slice_u16, + u16 + ); + gen_with_header_new_unsize_zst_slice_harness!( + harness_with_header_new_unsize_zst_slice_u32, + u32 + ); + gen_with_header_new_unsize_zst_slice_harness!( + harness_with_header_new_unsize_zst_slice_u64, + u64 + ); + // Kani currently cannot prove the alignment returned by `const_allocate` + // for a ZST slice source whose alignment is stricter than pointer-sized + // metadata, such as `[u128; 0] -> [u128]`. The implementation computes a + // correctly aligned value address, but the verifier loses that fact across + // the const allocation model and reports `value_ptr.is_aligned()` as + // possibly false. + gen_with_header_new_unsize_zst_dyn_any_harness!(harness_with_header_new_unsize_zst_dyn_any, ()); + + macro_rules! gen_with_header_header_harness { + ($name:ident, $ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value of the requested sized type. + let value: $ty = kani::any(); + + // Compute the metadata header that belongs to this sized value. + let header: <$ty as Pointee>::Metadata = ptr::metadata(&value); + + // Build the raw header/value allocation used by `ThinBox`. + let with_header: WithHeader<<$ty as Pointee>::Metadata> = + WithHeader::new(header, value); + + // Recover the header pointer from the stored value pointer. + let _header_ptr: *mut <$ty as Pointee>::Metadata = with_header.header(); + + // Rewrap the raw allocation as a `ThinBox` so normal drop cleans it up. + let _thin: ThinBox<$ty> = + ThinBox { ptr: WithOpaqueHeader(with_header.0), _marker: PhantomData }; + } + }; + } + + macro_rules! gen_with_header_header_dyn_any_harness { + ($name:ident, $src_ty:ty) => { + #[kani::proof] + pub fn $name() { + // Create a symbolic concrete value that will be represented as `dyn Any`. + let value: $src_ty = kani::any(); + + // Compute the trait-object metadata header for the erased pointee type. + let header: ::Metadata = ptr::metadata(&value as &dyn Any); + + // Build the raw header/value allocation used by `ThinBox`. + let with_header: WithHeader<::Metadata> = + WithHeader::new(header, value); + + // Recover the header pointer from the stored value pointer. + let _header_ptr: *mut ::Metadata = with_header.header(); + + // Rewrap the raw allocation as a `ThinBox` so normal drop cleans it up. + let _thin: ThinBox = + ThinBox { ptr: WithOpaqueHeader(with_header.0), _marker: PhantomData }; + } + }; + } + + macro_rules! gen_with_header_header_slice_harness { + ($name:ident, $elem:ty) => { + #[kani::proof] + pub fn $name() { + // Build a non-empty array that will be represented as a slice. + let value: [$elem; 4] = [kani::any::<$elem>(); 4]; + + // Compute the slice-length metadata header for the unsized pointee type. + let header: <[$elem] as Pointee>::Metadata = ptr::metadata(&value as &[$elem]); + + // Build the raw header/value allocation used by `ThinBox<[$elem]>`. + let with_header: WithHeader<<[$elem] as Pointee>::Metadata> = + WithHeader::new(header, value); + + // Recover the header pointer from the stored value pointer. + let _header_ptr: *mut <[$elem] as Pointee>::Metadata = with_header.header(); + + // Rewrap the raw allocation as a `ThinBox<[$elem]>` so normal drop cleans it up. + let _thin: ThinBox<[$elem]> = + ThinBox { ptr: WithOpaqueHeader(with_header.0), _marker: PhantomData }; + } + }; + } + + gen_with_header_header_harness!(harness_with_header_header_i8, i8); + gen_with_header_header_harness!(harness_with_header_header_i16, i16); + gen_with_header_header_harness!(harness_with_header_header_i32, i32); + gen_with_header_header_harness!(harness_with_header_header_i64, i64); + gen_with_header_header_harness!(harness_with_header_header_i128, i128); + gen_with_header_header_harness!(harness_with_header_header_u8, u8); + gen_with_header_header_harness!(harness_with_header_header_u16, u16); + gen_with_header_header_harness!(harness_with_header_header_u32, u32); + gen_with_header_header_harness!(harness_with_header_header_u64, u64); + gen_with_header_header_harness!(harness_with_header_header_u128, u128); + gen_with_header_header_harness!(harness_with_header_header_bool, bool); + gen_with_header_header_harness!(harness_with_header_header_unit, ()); + gen_with_header_header_harness!(harness_with_header_header_array, [u8; 4]); + gen_with_header_header_dyn_any_harness!(harness_with_header_header_dyn_any, i32); + + gen_with_header_header_slice_harness!(harness_with_header_header_slice_u8, u8); + gen_with_header_header_slice_harness!(harness_with_header_header_slice_u16, u16); + gen_with_header_header_slice_harness!(harness_with_header_header_slice_u32, u32); + gen_with_header_header_slice_harness!(harness_with_header_header_slice_u64, u64); + gen_with_header_header_slice_harness!(harness_with_header_header_slice_u128, u128); +}