From 469a999562ee8a40829d9a66cd587d947d4d49db Mon Sep 17 00:00:00 2001 From: Stefan Zetzsche Date: Thu, 20 Aug 2026 14:14:31 +0000 Subject: [PATCH] Challenge 2 --- library/core/src/fmt/num.rs | 76 ++ library/core/src/intrinsics/mod.rs | 1042 +++++++++++++++++++++++++- library/core/src/mem/maybe_uninit.rs | 67 ++ library/core/src/mem/mod.rs | 156 +++- library/core/src/ptr/mod.rs | 128 ++++ library/core/src/slice/mod.rs | 46 ++ 6 files changed, 1478 insertions(+), 37 deletions(-) diff --git a/library/core/src/fmt/num.rs b/library/core/src/fmt/num.rs index 253a7b7587e49..a2ff0015d3fb1 100644 --- a/library/core/src/fmt/num.rs +++ b/library/core/src/fmt/num.rs @@ -862,3 +862,79 @@ fn div_rem_1e16(n: u128) -> (u128, u64) { let rem = n - quot * D; (quot, rem as u64) } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use safety::{ensures, requires}; + + use super::*; + use crate::kani; + + // --------------------------------------------------------------------- + // `fmt::num::parse_u64_into` (the challenge's listed usage site) was + // removed when decimal formatting was rewritten; `u64::_fmt` is its + // successor and fills the tail of a `MaybeUninit` buffer with the + // ASCII digits of `self` exactly as `parse_u64_into` did. Its documented + // safety condition ("`buf` will always be big enough to contain all + // digits") is stated as `requires` on this wrapper: `_fmt` is generated + // by `impl_Display!` for every integer type, so annotating it directly + // would touch the runtime definition of all of them (the approach #643 + // takes); the wrapper keeps the annotation surface at zero. + // --------------------------------------------------------------------- + + /// Digits of `u64::MAX` (= 20); any `u64` fits in this many bytes. + const U64_MAX_DEC_N: usize = u64::MAX.ilog10() as usize + 1; + + #[cfg(not(feature = "optimize_for_size"))] + #[requires(buf.len() >= U64_MAX_DEC_N)] + #[ensures(|result: &&str| !result.is_empty() && result.len() <= U64_MAX_DEC_N)] + #[ensures(|result: &&str| result.as_bytes().iter().all(|b| b.is_ascii_digit()))] + #[kani::modifies(crate::ptr::slice_from_raw_parts_mut(buf.as_mut_ptr(), buf.len()))] + #[allow(dead_code)] + fn u64_fmt_wrapper<'a>(n: u64, buf: &'a mut [MaybeUninit]) -> &'a str { + // SAFETY: guaranteed by the precondition (`buf` holds any `u64`'s digits). + unsafe { n._fmt(buf) } + } + + // Verifies the `ensures` plus the UB checks along `_fmt_inner`'s + // buffer-filling walk and the final `slice_buffer_to_str` cast + // (`get_unchecked`, `assume_init_ref`, `from_utf8_unchecked`). + // Unwind: the digit loop runs at most 5 times (4 digits each), the + // byte-level `ensures` scan up to `U64_MAX_DEC_N` times. + #[cfg(not(feature = "optimize_for_size"))] + #[kani::proof_for_contract(u64_fmt_wrapper)] + #[kani::unwind(21)] + fn check_u64_fmt() { + let n: u64 = kani::any(); + let mut buf = [MaybeUninit::::uninit(); U64_MAX_DEC_N]; + let s = u64_fmt_wrapper(n, &mut buf); + kani::cover(s.len() == 1, "single digit"); + kani::cover(s.len() > 1, "multiple digits"); + } + + // Value-level fidelity on a bounded window (full 20-digit decimal + // equality for arbitrary `u64` does not converge): below 100 the result + // is exactly the one- or two-digit decimal of `n`, pinning the lookup + // table path against, e.g., a swapped-pair mutant. + #[cfg(not(feature = "optimize_for_size"))] + #[kani::proof] + #[kani::unwind(21)] + fn check_u64_fmt_small_values() { + let n: u64 = kani::any(); + kani::assume(n < 100); + let mut buf = [MaybeUninit::::uninit(); U64_MAX_DEC_N]; + let s = unsafe { n._fmt(&mut buf) }; + let bytes = s.as_bytes(); + if n < 10 { + assert_eq!(bytes.len(), 1); + assert_eq!(bytes[0], b'0' + n as u8); + } else { + assert_eq!(bytes.len(), 2); + assert_eq!(bytes[0], b'0' + (n / 10) as u8); + assert_eq!(bytes[1], b'0' + (n % 10) as u8); + } + kani::cover(n < 10, "one digit"); + kani::cover(n >= 10, "two digits"); + } +} diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index ddadeeb3c786a..dbc16e83ccc93 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -2960,7 +2960,10 @@ fn check_copy_untyped(src: *const T, dst: *mut T, count: usize) -> bool { // them and check it. Using quantifiers would not add value as we can rely on the solver to // pick an uninitialized element if such an element exists. let elem = kani::any_where(|val: &usize| *val < count); - let src_data = src as *const u8; + // Offset *both* sides by `elem`: comparing `dst[elem]` against `src[0]` + // would be wrong whenever initialization differs across elements. + // (Oracle fix independently found by #643.) + let src_data = unsafe { src.add(elem) } as *const u8; let dst_data = unsafe { dst.add(elem) } as *const u8; ub_checks::can_dereference(unsafe { src_data.add(byte) }) == ub_checks::can_dereference(unsafe { dst_data.add(byte) }) @@ -3497,33 +3500,410 @@ mod verify { }); } - // #[kani::proof_for_contract(copy)] - // fn check_copy() { - // run_with_arbitrary_ptrs::(|src, dst| unsafe { copy(src, dst, kani::any()) }); - // } - - // #[kani::proof_for_contract(copy_nonoverlapping)] - // fn check_copy_nonoverlapping() { - // // Note: cannot use `ArbitraryPointer` here. - // // The `ArbitraryPtr` will arbitrarily initialize memory by indirectly invoking - // // `copy_nonoverlapping`. - // // Kani contract checking would fail due to existing restriction on calls to - // // the function under verification. - // let gen_any_ptr = |buf: &mut [MaybeUninit; 100]| -> *mut char { - // let base = buf.as_mut_ptr() as *mut u8; - // base.wrapping_add(kani::any_where(|offset: &usize| *offset < 400)) as *mut char - // }; - // let mut buffer1 = [MaybeUninit::::uninit(); 100]; - // for i in 0..100 { - // if kani::any() { - // buffer1[i] = MaybeUninit::new(kani::any()); - // } - // } - // let mut buffer2 = [MaybeUninit::::uninit(); 100]; - // let src = gen_any_ptr(&mut buffer1); - // let dst = if kani::any() { gen_any_ptr(&mut buffer2) } else { gen_any_ptr(&mut buffer1) }; - // unsafe { copy_nonoverlapping(src, dst, kani::any()) } - // } + // ---- vtable_size ---- + // Wrapper pattern, used throughout: Kani cannot attach contracts to body-less + // `#[rustc_intrinsic]`s (rust-lang/rust#137489, model-checking/kani#3325), so + // each contract lives on a thin wrapper (or `*_model`) fn; harnesses verify that. + // `[usize; 3]`: vtable = (size, align, drop-in-place), per rust-lang/unsafe-code-guidelines#166. + #[requires(ub_checks::can_dereference(ptr as *const [usize; 3]))] + #[ensures(|result: &usize| *result <= isize::MAX as usize)] + #[allow(dead_code)] + unsafe fn vtable_size_wrapper(ptr: *const ()) -> usize { + // SAFETY: guaranteed by the precondition (`ptr` points to a vtable). + unsafe { vtable_size(ptr) } + } + + // Real vtable pointer via `dyn Debug`; the `assert_eq!` pins Kani's model + // and witnesses non-vacuity. + macro_rules! check_vtable_size_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(vtable_size_wrapper)] + fn $harness() { + let val: $ty = kani::any(); + let obj: &dyn core::fmt::Debug = &val; + let fat: *const dyn core::fmt::Debug = obj; + let meta = core::ptr::metadata(fat); + // Same transmute `DynMetadata::vtable_ptr` performs (layout-compatible). + let vptr = unsafe { + core::mem::transmute::, *const ()>( + meta, + ) + }; + let size = unsafe { vtable_size_wrapper(vptr) }; + kani::cover(true, "vtable_size call is reachable"); + assert_eq!(size, core::mem::size_of::<$ty>()); + } + }; + } + + check_vtable_size_for!(check_vtable_size_u8, u8); + check_vtable_size_for!(check_vtable_size_u32, u32); + check_vtable_size_for!(check_vtable_size_u64, u64); + check_vtable_size_for!(check_vtable_size_i128, i128); + + // ---- vtable_align ---- + // As `vtable_size`; the ensures encodes non-zero power of two. + #[requires(ub_checks::can_dereference(ptr as *const [usize; 3]))] + #[ensures(|result: &usize| result.is_power_of_two())] + #[allow(dead_code)] + unsafe fn vtable_align_wrapper(ptr: *const ()) -> usize { + // SAFETY: guaranteed by the precondition (`ptr` points to a vtable). + unsafe { vtable_align(ptr) } + } + + macro_rules! check_vtable_align_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(vtable_align_wrapper)] + fn $harness() { + let val: $ty = kani::any(); + let obj: &dyn core::fmt::Debug = &val; + let fat: *const dyn core::fmt::Debug = obj; + let meta = core::ptr::metadata(fat); + // Same transmute `DynMetadata::vtable_ptr` performs. + let vptr = unsafe { + core::mem::transmute::, *const ()>( + meta, + ) + }; + let align = unsafe { vtable_align_wrapper(vptr) }; + kani::cover(true, "vtable_align call is reachable"); + assert_eq!(align, core::mem::align_of::<$ty>()); + } + }; + } + + check_vtable_align_for!(check_vtable_align_u8, u8); + check_vtable_align_for!(check_vtable_align_u32, u32); + check_vtable_align_for!(check_vtable_align_u64, u64); + check_vtable_align_for!(check_vtable_align_i128, i128); + + // ---- size_of_val ---- + // Kani models this intrinsic (no fallback body); harness asserts pin it. + // `size_of_val_raw` documents per-case safety, so each case gets its own + // wrapper: `Sized` is always safe; a slice needs total size <= `isize::MAX`. + #[ensures(|result: &usize| *result <= isize::MAX as usize)] + #[allow(dead_code)] + unsafe fn size_of_val_sized_wrapper(ptr: *const T) -> usize { + // SAFETY: `Sized` case never reads `*ptr`; safe for any pointer. + unsafe { size_of_val(ptr) } + } + + // Division-first so the check never overflows; a ZST element makes it 0. + #[requires(size_of::() == 0 || ptr.len() <= (isize::MAX as usize) / size_of::())] + #[ensures(|result: &usize| *result <= isize::MAX as usize)] + #[allow(dead_code)] + unsafe fn size_of_val_slice_wrapper(ptr: *const [E]) -> usize { + // SAFETY: only the length metadata is read; precondition bounds the size. + unsafe { size_of_val(ptr) } + } + + // Model must return `size_of::()`, pointer-independent. + macro_rules! check_size_of_val_sized_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(size_of_val_sized_wrapper)] + fn $harness() { + let val: $ty = kani::any(); + let ptr: *const $ty = &val; + let size = unsafe { size_of_val_sized_wrapper(ptr) }; + kani::cover(true, "size_of_val (sized) call is reachable"); + assert_eq!(size, core::mem::size_of::<$ty>()); + } + }; + } + + check_size_of_val_sized_for!(check_size_of_val_u8, u8); + check_size_of_val_sized_for!(check_size_of_val_u32, u32); + check_size_of_val_sized_for!(check_size_of_val_u64, u64); + check_size_of_val_sized_for!(check_size_of_val_i128, i128); + check_size_of_val_sized_for!(check_size_of_val_char, char); + + // In-bounds `len` over a real array; model must return `len * size_of::()`. + macro_rules! check_size_of_val_slice_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(size_of_val_slice_wrapper)] + fn $harness() { + const N: usize = 4; + let arr: [$ty; N] = kani::any(); + let len: usize = kani::any_where(|l: &usize| *l <= N); + let ptr: *const [$ty] = core::ptr::slice_from_raw_parts(arr.as_ptr(), len); + let size = unsafe { size_of_val_slice_wrapper(ptr) }; + kani::cover(len > 0, "size_of_val measures a non-empty slice"); + assert_eq!(size, len * core::mem::size_of::<$ty>()); + } + }; + } + + check_size_of_val_slice_for!(check_size_of_val_slice_u8, u8); + check_size_of_val_slice_for!(check_size_of_val_slice_u32, u32); + check_size_of_val_slice_for!(check_size_of_val_slice_i64, i64); + + // ---- align_of_val (historically `min_align_of_val`) ---- + // Same modeling and per-case wrapper split as `size_of_val`; the slice + // contract keeps the documented size-fits-`isize` condition. + #[ensures(|result: &usize| result.is_power_of_two())] + #[allow(dead_code)] + unsafe fn align_of_val_sized_wrapper(ptr: *const T) -> usize { + // SAFETY: `Sized` case never reads `*ptr`; safe for any pointer. + unsafe { align_of_val(ptr) } + } + + #[requires(size_of::() == 0 || ptr.len() <= (isize::MAX as usize) / size_of::())] + #[ensures(|result: &usize| result.is_power_of_two())] + #[allow(dead_code)] + unsafe fn align_of_val_slice_wrapper(ptr: *const [E]) -> usize { + // SAFETY: only the length metadata is read; precondition bounds the size. + unsafe { align_of_val(ptr) } + } + + // Model must return `align_of::()`, pointer-independent. + macro_rules! check_align_of_val_sized_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(align_of_val_sized_wrapper)] + fn $harness() { + let val: $ty = kani::any(); + let ptr: *const $ty = &val; + let align = unsafe { align_of_val_sized_wrapper(ptr) }; + kani::cover(true, "align_of_val (sized) call is reachable"); + assert_eq!(align, core::mem::align_of::<$ty>()); + } + }; + } + + check_align_of_val_sized_for!(check_align_of_val_u8, u8); + check_align_of_val_sized_for!(check_align_of_val_u32, u32); + check_align_of_val_sized_for!(check_align_of_val_u64, u64); + check_align_of_val_sized_for!(check_align_of_val_i128, i128); + check_align_of_val_sized_for!(check_align_of_val_char, char); + + // In-bounds `len`; model must return `align_of::()` regardless of `len`. + macro_rules! check_align_of_val_slice_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(align_of_val_slice_wrapper)] + fn $harness() { + const N: usize = 4; + let arr: [$ty; N] = kani::any(); + let len: usize = kani::any_where(|l: &usize| *l <= N); + let ptr: *const [$ty] = core::ptr::slice_from_raw_parts(arr.as_ptr(), len); + let align = unsafe { align_of_val_slice_wrapper(ptr) }; + kani::cover(len > 0, "align_of_val measures a non-empty slice"); + assert_eq!(align, core::mem::align_of::<$ty>()); + } + }; + } + + check_align_of_val_slice_for!(check_align_of_val_slice_u8, u8); + check_align_of_val_slice_for!(check_align_of_val_slice_u32, u32); + check_align_of_val_slice_for!(check_align_of_val_slice_i64, i64); + + // ---- size_of_val / align_of_val: trait-object (`dyn`) tails ---- + // Third documented case of `size_of_val_raw` / `align_of_val_raw`: the + // vtable must be valid. Kani has no vtable predicate, so (exactly as for + // `vtable_size_wrapper`) dereferenceability of the three metadata words is + // the necessary approximation; harnesses supply real compiler-produced + // vtables, so the precondition is satisfied non-vacuously. + #[allow(dead_code)] + fn dyn_vtable_ptr(ptr: *const dyn core::fmt::Debug) -> *const () { + let meta = core::ptr::metadata(ptr); + // Same transmute `DynMetadata::vtable_ptr` performs (layout-compatible). + unsafe { + core::mem::transmute::, *const ()>(meta) + } + } + + #[requires(ub_checks::can_dereference(dyn_vtable_ptr(ptr) as *const [usize; 3]))] + #[ensures(|result: &usize| *result <= isize::MAX as usize)] + #[allow(dead_code)] + unsafe fn size_of_val_dyn_wrapper(ptr: *const dyn core::fmt::Debug) -> usize { + // SAFETY: only the vtable is read; readable by the precondition. + unsafe { size_of_val(ptr) } + } + + #[requires(ub_checks::can_dereference(dyn_vtable_ptr(ptr) as *const [usize; 3]))] + #[ensures(|result: &usize| result.is_power_of_two())] + #[allow(dead_code)] + unsafe fn align_of_val_dyn_wrapper(ptr: *const dyn core::fmt::Debug) -> usize { + // SAFETY: only the vtable is read; readable by the precondition. + unsafe { align_of_val(ptr) } + } + + // Erased-type fidelity: the model must return the *underlying* type's + // size/align through the vtable, not a fixture value. + macro_rules! check_size_of_val_dyn_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(size_of_val_dyn_wrapper)] + fn $harness() { + let val: $ty = kani::any(); + let obj: &dyn core::fmt::Debug = &val; + let size = unsafe { size_of_val_dyn_wrapper(obj) }; + kani::cover(true, "size_of_val (dyn) call is reachable"); + assert_eq!(size, core::mem::size_of::<$ty>()); + } + }; + } + + check_size_of_val_dyn_for!(check_size_of_val_dyn_u8, u8); + check_size_of_val_dyn_for!(check_size_of_val_dyn_u32, u32); + check_size_of_val_dyn_for!(check_size_of_val_dyn_i128, i128); + + macro_rules! check_align_of_val_dyn_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(align_of_val_dyn_wrapper)] + fn $harness() { + let val: $ty = kani::any(); + let obj: &dyn core::fmt::Debug = &val; + let align = unsafe { align_of_val_dyn_wrapper(obj) }; + kani::cover(true, "align_of_val (dyn) call is reachable"); + assert_eq!(align, core::mem::align_of::<$ty>()); + } + }; + } + + check_align_of_val_dyn_for!(check_align_of_val_dyn_u8, u8); + check_align_of_val_dyn_for!(check_align_of_val_dyn_u32, u32); + check_align_of_val_dyn_for!(check_align_of_val_dyn_i128, i128); + + // ---- copy_nonoverlapping ---- + // Restores the pre-body-removal contract. `MaybeUninit` because the copy is + // untyped; the ensures checks per-byte initialization state is preserved. + #[requires(!count.overflowing_mul(crate::mem::size_of::()).1 + && ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src as *const crate::mem::MaybeUninit, count)) + && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)) + && ub_checks::maybe_is_nonoverlapping(src as *const (), dst as *const (), crate::mem::size_of::(), count))] + #[ensures(|_| check_copy_untyped(src, dst, count))] + #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))] + #[allow(dead_code)] + unsafe fn copy_nonoverlapping_wrapper(src: *const T, dst: *mut T, count: usize) { + // SAFETY: guaranteed by the precondition. + unsafe { copy_nonoverlapping(src, dst, count) } + } + + // No `ArbitraryPointer`: it initializes memory via the function under + // verification. Non-deterministic `src` init gives the untyped-copy ensures + // teeth; `dst` may alias `buffer1` so non-overlap is genuinely exercised. + macro_rules! check_copy_nonoverlapping_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(copy_nonoverlapping_wrapper)] + fn $harness() { + const N: usize = 100; + let gen_any_ptr = |buf: &mut [MaybeUninit<$ty>; N]| -> *mut $ty { + let base = buf.as_mut_ptr() as *mut u8; + base.wrapping_add(kani::any_where(|o: &usize| { + *o < N * core::mem::size_of::<$ty>() + })) as *mut $ty + }; + let mut buffer1 = [MaybeUninit::<$ty>::uninit(); N]; + for i in 0..N { + if kani::any() { + buffer1[i] = MaybeUninit::new(kani::any()); + } + } + let mut buffer2 = [MaybeUninit::<$ty>::uninit(); N]; + let src = gen_any_ptr(&mut buffer1) as *const $ty; + let dst = + if kani::any() { gen_any_ptr(&mut buffer2) } else { gen_any_ptr(&mut buffer1) }; + let count: usize = kani::any(); + kani::cover(count > 0, "copy_nonoverlapping copies a non-empty range"); + unsafe { copy_nonoverlapping_wrapper(src, dst, count) }; + } + }; + } + + check_copy_nonoverlapping_for!(check_copy_nonoverlapping_u8, u8); + check_copy_nonoverlapping_for!(check_copy_nonoverlapping_char, char); + check_copy_nonoverlapping_for!(check_copy_nonoverlapping_u32, u32); + + // ---- copy ---- + // Memmove: overlap permitted, so `copy_nonoverlapping`'s contract minus the + // non-overlap clause. + #[requires(!count.overflowing_mul(crate::mem::size_of::()).1 + && ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src as *const crate::mem::MaybeUninit, count)) + && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)))] + #[ensures(|_| check_copy_untyped(src, dst, count))] + #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))] + #[allow(dead_code)] + unsafe fn copy_wrapper(src: *const T, dst: *mut T, count: usize) { + // SAFETY: guaranteed by the precondition. + unsafe { copy(src, dst, count) } + } + + // Same setup as `copy_nonoverlapping`, but the aliasing `dst` now exercises + // the overlapping case `copy` permits. + macro_rules! check_copy_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(copy_wrapper)] + fn $harness() { + const N: usize = 100; + let gen_any_ptr = |buf: &mut [MaybeUninit<$ty>; N]| -> *mut $ty { + let base = buf.as_mut_ptr() as *mut u8; + base.wrapping_add(kani::any_where(|o: &usize| { + *o < N * core::mem::size_of::<$ty>() + })) as *mut $ty + }; + let mut buffer1 = [MaybeUninit::<$ty>::uninit(); N]; + for i in 0..N { + if kani::any() { + buffer1[i] = MaybeUninit::new(kani::any()); + } + } + let mut buffer2 = [MaybeUninit::<$ty>::uninit(); N]; + let src = gen_any_ptr(&mut buffer1) as *const $ty; + // `dst` may alias `buffer1` (overlap is permitted by `copy`). + let dst = + if kani::any() { gen_any_ptr(&mut buffer2) } else { gen_any_ptr(&mut buffer1) }; + let count: usize = kani::any(); + kani::cover(count > 0, "copy copies a non-empty range"); + unsafe { copy_wrapper(src, dst, count) }; + } + }; + } + + check_copy_for!(check_copy_u8, u8); + check_copy_for!(check_copy_char, char); + check_copy_for!(check_copy_u32, u32); + + // ---- write_bytes ---- + // C `memset`; contract is the pre-body-removal one. Supersedes the old + // harness parked on . + // Ensures is over `*const u8`: arbitrary `val` bytes need not form a valid `T`. + #[requires(!count.overflowing_mul(crate::mem::size_of::()).1 + && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)))] + #[requires(ub_checks::maybe_is_aligned_and_not_null( + dst as *const (), + crate::mem::align_of::(), + crate::mem::size_of::() == 0 || count == 0, + ))] + #[ensures(|_| ub_checks::can_dereference( + core::ptr::slice_from_raw_parts(dst as *const u8, count * crate::mem::size_of::())))] + #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))] + #[allow(dead_code)] + unsafe fn write_bytes_wrapper(dst: *mut T, val: u8, count: usize) { + // SAFETY: guaranteed by the precondition. + unsafe { write_bytes(dst, val, count) } + } + + // `dst` stays inside a real stack allocation; the byte-granular offset + // generates misaligned pointers the alignment clause must prune. + macro_rules! check_write_bytes_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(write_bytes_wrapper)] + fn $harness() { + const N: usize = 100; + let mut buffer = [MaybeUninit::<$ty>::uninit(); N]; + let base = buffer.as_mut_ptr() as *mut u8; + let dst = base + .wrapping_add(kani::any_where(|o: &usize| *o < N * core::mem::size_of::<$ty>())) + as *mut $ty; + let val: u8 = kani::any(); + let count: usize = kani::any(); + kani::cover(count > 0, "write_bytes writes a non-empty range"); + unsafe { write_bytes_wrapper(dst, val, count) }; + } + }; + } + + check_write_bytes_for!(check_write_bytes_u8, u8); + check_write_bytes_for!(check_write_bytes_char, char); + check_write_bytes_for!(check_write_bytes_u32, u32); //We need this wrapper because transmute_unchecked is an intrinsic, for which Kani does //not currently support contracts (https://github.com/model-checking/kani/issues/3345) @@ -4116,17 +4496,607 @@ mod verify { gen_compound_harnesses!(arr_mod, [u8; 2]); gen_compound_harnesses!(struct_mod, u8_struct); + // ---- arith_offset ---- + // Kani models this as wrapping pointer arithmetic; no safety precondition, + // hence no `requires`. Ensures: address displaced by `offset` elements, + // wrapping over the pointer width (unlike the bounds-restricted `offset`). + #[ensures(|result: &*const T| + (*result).addr() + == dst.addr().wrapping_add((offset as usize).wrapping_mul(crate::mem::size_of::())))] + #[allow(dead_code)] + unsafe fn arith_offset_wrapper(dst: *const T, offset: isize) -> *const T { + // SAFETY: no preconditions; pure wrapping arithmetic, no memory access. + unsafe { arith_offset(dst, offset) } + } + + // Nothing is dereferenced, so a provenance-free integer address is the most + // general base. CBMC mismodels arithmetic near NULL and `usize::MAX`, so the + // harness pins the base to a mid-range window and bounds `|offset|`. + macro_rules! check_arith_offset_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(arith_offset_wrapper)] + fn $harness() { + // `base_addr` in `[2^32, 2^45]`, `|offset| <= 2^20`: result stays + // in `(0, 2^46)` for every `T` here, clear of NULL and wrap edges. + let base_addr: usize = kani::any(); + kani::assume(base_addr >= (1usize << 32) && base_addr <= (1usize << 45)); + let offset: isize = kani::any(); + kani::assume(offset >= -(1isize << 20) && offset <= (1isize << 20)); + + let dst: *const $ty = crate::ptr::without_provenance(base_addr); + kani::cover(offset > 0, "arith_offset applies a forward displacement"); + kani::cover(offset < 0, "arith_offset applies a backward displacement"); + let _ = unsafe { arith_offset_wrapper::<$ty>(dst, offset) }; + } + }; + } + + check_arith_offset_for!(check_arith_offset_u8, u8); + check_arith_offset_for!(check_arith_offset_u32, u32); + check_arith_offset_for!(check_arith_offset_u64, u64); + check_arith_offset_for!(check_arith_offset_i128, i128); + + // ---- volatile_copy_nonoverlapping_memory ---- + // Volatile-model scheme, used for all volatile intrinsics Kani does not + // support: the contract is verified on a `*_model` fn whose body is the + // non-volatile equivalent (here `copy_nonoverlapping`). Fidelity: the two + // differ only in LLVM's volatile flag, an optimization barrier with no + // effect on the abstract memory state CBMC reasons about. + #[requires(!count.overflowing_mul(crate::mem::size_of::()).1 + && ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src as *const crate::mem::MaybeUninit, count)) + && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)) + && ub_checks::maybe_is_nonoverlapping(src as *const (), dst as *const (), crate::mem::size_of::(), count))] + #[ensures(|_| check_copy_untyped(src, dst, count))] + #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))] + #[allow(dead_code)] + unsafe fn volatile_copy_nonoverlapping_memory_model( + dst: *mut T, + src: *const T, + count: usize, + ) { + // MODEL: forwards to the non-volatile copy (identical memory effects). + // SAFETY: guaranteed by the precondition. + unsafe { copy_nonoverlapping(src, dst, count) } + } + + // Same setup rationale as `check_copy_nonoverlapping_for`. + macro_rules! check_volatile_copy_nonoverlapping_memory_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(volatile_copy_nonoverlapping_memory_model)] + fn $harness() { + const N: usize = 100; + let gen_any_ptr = |buf: &mut [MaybeUninit<$ty>; N]| -> *mut $ty { + let base = buf.as_mut_ptr() as *mut u8; + base.wrapping_add(kani::any_where(|o: &usize| { + *o < N * core::mem::size_of::<$ty>() + })) as *mut $ty + }; + let mut buffer1 = [MaybeUninit::<$ty>::uninit(); N]; + for i in 0..N { + if kani::any() { + buffer1[i] = MaybeUninit::new(kani::any()); + } + } + let mut buffer2 = [MaybeUninit::<$ty>::uninit(); N]; + let src = gen_any_ptr(&mut buffer1) as *const $ty; + // `dst` may point into a separate buffer or alias `buffer1`. + let dst = + if kani::any() { gen_any_ptr(&mut buffer2) } else { gen_any_ptr(&mut buffer1) }; + let count: usize = kani::any(); + kani::cover( + count > 0, + "volatile_copy_nonoverlapping_memory copies a non-empty range", + ); + unsafe { volatile_copy_nonoverlapping_memory_model(dst, src, count) }; + } + }; + } + + check_volatile_copy_nonoverlapping_memory_for!( + check_volatile_copy_nonoverlapping_memory_u8, + u8 + ); + check_volatile_copy_nonoverlapping_memory_for!( + check_volatile_copy_nonoverlapping_memory_char, + char + ); + check_volatile_copy_nonoverlapping_memory_for!( + check_volatile_copy_nonoverlapping_memory_u32, + u32 + ); + + // ---- volatile_copy_memory ---- + // Same volatile-model scheme, body `copy` (memmove): the contract is + // `volatile_copy_nonoverlapping_memory`'s minus the non-overlap clause. + #[requires(!count.overflowing_mul(crate::mem::size_of::()).1 + && ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src as *const crate::mem::MaybeUninit, count)) + && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)))] + #[ensures(|_| check_copy_untyped(src, dst, count))] + #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))] + #[allow(dead_code)] + unsafe fn volatile_copy_memory_model(dst: *mut T, src: *const T, count: usize) { + // MODEL: non-volatile `copy`. SAFETY: guaranteed by the precondition. + unsafe { copy(src, dst, count) } + } + + // Same setup as `check_copy_for`, including the aliasing `dst`. + macro_rules! check_volatile_copy_memory_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(volatile_copy_memory_model)] + fn $harness() { + const N: usize = 100; + let gen_any_ptr = |buf: &mut [MaybeUninit<$ty>; N]| -> *mut $ty { + let base = buf.as_mut_ptr() as *mut u8; + base.wrapping_add(kani::any_where(|o: &usize| { + *o < N * core::mem::size_of::<$ty>() + })) as *mut $ty + }; + let mut buffer1 = [MaybeUninit::<$ty>::uninit(); N]; + for i in 0..N { + if kani::any() { + buffer1[i] = MaybeUninit::new(kani::any()); + } + } + let mut buffer2 = [MaybeUninit::<$ty>::uninit(); N]; + let src = gen_any_ptr(&mut buffer1) as *const $ty; + let dst = + if kani::any() { gen_any_ptr(&mut buffer2) } else { gen_any_ptr(&mut buffer1) }; + let count: usize = kani::any(); + kani::cover(count > 0, "volatile_copy_memory copies a non-empty range"); + unsafe { volatile_copy_memory_model(dst, src, count) }; + } + }; + } + + check_volatile_copy_memory_for!(check_volatile_copy_memory_u8, u8); + check_volatile_copy_memory_for!(check_volatile_copy_memory_char, char); + check_volatile_copy_memory_for!(check_volatile_copy_memory_u32, u32); + + // ---- volatile_set_memory ---- + // Same volatile-model scheme, body `write_bytes` (memset); contract is + // `write_bytes`'s verbatim, including the bytes-only ensures. + #[requires(!count.overflowing_mul(crate::mem::size_of::()).1 + && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)))] + #[requires(ub_checks::maybe_is_aligned_and_not_null( + dst as *const (), + crate::mem::align_of::(), + crate::mem::size_of::() == 0 || count == 0, + ))] + #[ensures(|_| ub_checks::can_dereference( + core::ptr::slice_from_raw_parts(dst as *const u8, count * crate::mem::size_of::())))] + #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))] + #[allow(dead_code)] + unsafe fn volatile_set_memory_model(dst: *mut T, val: u8, count: usize) { + // MODEL: non-volatile `write_bytes`. SAFETY: guaranteed by the precondition. + unsafe { write_bytes(dst, val, count) } + } + + // Same setup rationale as `check_write_bytes_for`. + macro_rules! check_volatile_set_memory_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(volatile_set_memory_model)] + fn $harness() { + const N: usize = 100; + let mut buffer = [MaybeUninit::<$ty>::uninit(); N]; + let base = buffer.as_mut_ptr() as *mut u8; + let dst = base + .wrapping_add(kani::any_where(|o: &usize| *o < N * core::mem::size_of::<$ty>())) + as *mut $ty; + let val: u8 = kani::any(); + let count: usize = kani::any(); + kani::cover(count > 0, "volatile_set_memory sets a non-empty range"); + unsafe { volatile_set_memory_model(dst, val, count) }; + } + }; + } + + check_volatile_set_memory_for!(check_volatile_set_memory_u8, u8); + check_volatile_set_memory_for!(check_volatile_set_memory_char, char); + check_volatile_set_memory_for!(check_volatile_set_memory_u32, u32); + + // ---- volatile_load ---- + // Backs `ptr::read_volatile`; Kani models it as the same read. Requires is + // verbatim from `read_volatile`; a read has no `modifies` and no ensures. + #[requires(ub_checks::can_dereference(src))] + #[allow(dead_code)] + unsafe fn volatile_load_model(src: *const T) -> T { + // SAFETY: guaranteed by the precondition. + unsafe { volatile_load(src) } + } + + // `src` stays inside a fully initialized stack allocation (uninit would make + // `can_dereference` unsatisfiable, hence vacuous); the byte-granular offset + // generates misaligned pointers the alignment clause must prune. + macro_rules! check_volatile_load_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(volatile_load_model)] + fn $harness() { + const N: usize = 100; + let mut buffer = [MaybeUninit::<$ty>::uninit(); N]; + for i in 0..N { + buffer[i] = MaybeUninit::new(kani::any()); + } + let base = buffer.as_ptr() as *const u8; + let src = base + .wrapping_add(kani::any_where(|o: &usize| *o < N * core::mem::size_of::<$ty>())) + as *const $ty; + kani::cover(true, "volatile_load reaches a dereferenceable src"); + let _val = unsafe { volatile_load_model(src) }; + } + }; + } + + check_volatile_load_for!(check_volatile_load_u8, u8); + check_volatile_load_for!(check_volatile_load_char, char); + check_volatile_load_for!(check_volatile_load_u32, u32); + + // ---- volatile_store ---- + // Backs `ptr::write_volatile`; Kani models it as the same write. Requires is + // verbatim from `write_volatile`; `modifies(dst)` scopes the write. No + // ensures: `dst` may be write-only I/O memory, so asserting post-state + // readability would over-claim; fidelity is pinned by the harness read-back. + #[requires(ub_checks::can_write(dst))] + #[cfg_attr(kani, kani::modifies(dst))] + #[allow(dead_code)] + unsafe fn volatile_store_model(dst: *mut T, val: T) { + // SAFETY: guaranteed by the precondition. + unsafe { volatile_store(dst, val) } + } + + // `dst` need not be initialized (the store only writes); misaligned pointers + // from the byte-granular offset must be pruned by the alignment clause. + macro_rules! check_volatile_store_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(volatile_store_model)] + fn $harness() { + const N: usize = 100; + let mut buffer = [MaybeUninit::<$ty>::uninit(); N]; + let base = buffer.as_mut_ptr() as *mut u8; + let dst = base + .wrapping_add(kani::any_where(|o: &usize| *o < N * core::mem::size_of::<$ty>())) + as *mut $ty; + let val: $ty = kani::any(); + kani::cover(true, "volatile_store reaches a writeable dst"); + unsafe { volatile_store_model(dst, val) }; + // Fidelity: the model actually stored `val` at `dst`. + let read_back = unsafe { volatile_load(dst) }; + assert!(read_back == val); + } + }; + } + + check_volatile_store_for!(check_volatile_store_u8, u8); + check_volatile_store_for!(check_volatile_store_char, char); + check_volatile_store_for!(check_volatile_store_u32, u32); + + // ---- unaligned_volatile_load ---- + // Volatile analogue of `ptr::read_unaligned`; same volatile-model scheme. + // Requires `can_read_unaligned(src)`: dropping the alignment obligation is + // the whole difference from `volatile_load`. + #[requires(ub_checks::can_read_unaligned(src))] + #[allow(dead_code)] + unsafe fn unaligned_volatile_load_model(src: *const T) -> T { + // MODEL: non-volatile `read_unaligned`. SAFETY: guaranteed by the precondition. + unsafe { crate::ptr::read_unaligned(src) } + } + + // As `check_volatile_load_for`, but misaligned pointers are NOT pruned; the + // cover witnesses that a misaligned read is actually reachable. + macro_rules! check_unaligned_volatile_load_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(unaligned_volatile_load_model)] + fn $harness() { + const N: usize = 100; + let mut buffer = [MaybeUninit::<$ty>::uninit(); N]; + for i in 0..N { + buffer[i] = MaybeUninit::new(kani::any()); + } + let base = buffer.as_ptr() as *const u8; + let src = base + .wrapping_add(kani::any_where(|o: &usize| *o < N * core::mem::size_of::<$ty>())) + as *const $ty; + kani::cover( + src.addr() % core::mem::align_of::<$ty>() != 0, + "unaligned_volatile_load reaches a misaligned src", + ); + let _val = unsafe { unaligned_volatile_load_model(src) }; + } + }; + } + + // `char`/`u32` (alignment > 1) make the misaligned cover satisfiable; `u8` + // is handled separately since every address is 1-aligned. + check_unaligned_volatile_load_for!(check_unaligned_volatile_load_char, char); + check_unaligned_volatile_load_for!(check_unaligned_volatile_load_u32, u32); + + #[kani::proof_for_contract(unaligned_volatile_load_model)] + fn check_unaligned_volatile_load_u8() { + const N: usize = 100; + let mut buffer = [MaybeUninit::::uninit(); N]; + for i in 0..N { + buffer[i] = MaybeUninit::new(kani::any()); + } + let base = buffer.as_ptr(); + let src = base.wrapping_add(kani::any_where(|o: &usize| *o < N)) as *const u8; + // `u8` is always aligned; just witness a dereferenceable read (non-vacuity). + kani::cover(true, "unaligned_volatile_load reaches a dereferenceable src"); + let _val = unsafe { unaligned_volatile_load_model(src) }; + } + + // ---- unaligned_volatile_store ---- + // Volatile analogue of `ptr::write_unaligned`; same volatile-model scheme. + // Requires `can_write_unaligned(dst)`: dropping alignment is the whole + // difference from `volatile_store`. No ensures (write-only I/O memory); + // fidelity is pinned by the harness read-back. + #[requires(ub_checks::can_write_unaligned(dst))] + #[cfg_attr(kani, kani::modifies(dst))] + #[allow(dead_code)] + unsafe fn unaligned_volatile_store_model(dst: *mut T, val: T) { + // MODEL: non-volatile `write_unaligned`. SAFETY: guaranteed by the precondition. + unsafe { crate::ptr::write_unaligned(dst, val) } + } + + // As `check_volatile_store_for`, but misaligned pointers are NOT pruned; the + // cover witnesses a misaligned write, and the read-back assert pins fidelity. + macro_rules! check_unaligned_volatile_store_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(unaligned_volatile_store_model)] + fn $harness() { + const N: usize = 100; + let mut buffer = [MaybeUninit::<$ty>::uninit(); N]; + let base = buffer.as_mut_ptr() as *mut u8; + let dst = base + .wrapping_add(kani::any_where(|o: &usize| *o < N * core::mem::size_of::<$ty>())) + as *mut $ty; + let val: $ty = kani::any(); + kani::cover( + dst.addr() % core::mem::align_of::<$ty>() != 0, + "unaligned_volatile_store reaches a misaligned dst", + ); + unsafe { unaligned_volatile_store_model(dst, val) }; + // Fidelity: the model actually stored `val` at `dst`. + let read_back = unsafe { crate::ptr::read_unaligned(dst) }; + assert!(read_back == val); + } + }; + } + + // `char`/`u32` have alignment > 1, so the misaligned cover is satisfiable; + // `u8` is handled separately as for the load case. + check_unaligned_volatile_store_for!(check_unaligned_volatile_store_char, char); + check_unaligned_volatile_store_for!(check_unaligned_volatile_store_u32, u32); + + #[kani::proof_for_contract(unaligned_volatile_store_model)] + fn check_unaligned_volatile_store_u8() { + const N: usize = 100; + let mut buffer = [MaybeUninit::::uninit(); N]; + let base = buffer.as_mut_ptr(); + let dst = base.wrapping_add(kani::any_where(|o: &usize| *o < N)) as *mut u8; + let val: u8 = kani::any(); + // `u8` is always aligned; just witness a writeable dst (non-vacuity). + kani::cover(true, "unaligned_volatile_store reaches a writeable dst"); + unsafe { unaligned_volatile_store_model(dst, val) }; + let read_back = unsafe { crate::ptr::read_unaligned(dst) }; + assert!(read_back == val); + } + + // ---- ptr_offset_from ---- + // Kani models this as the CBMC pointer difference scaled to units of `T` + // (primitive behind `<*const T>::offset_from`). The four `requires` encode + // the `# Safety` of `offset_from`, matching the already-verified contract in + // `ptr/const_ptr.rs`. Ensures: the exact signed element distance. + #[requires(crate::mem::size_of::() != 0)] + // Subtracting `base` from `ptr` (as addresses) does not overflow `isize`. + #[requires((ptr as isize).checked_sub(base as isize).is_some())] + // The byte distance is an exact multiple of the pointee size. + #[requires((ptr as isize - base as isize) % (crate::mem::size_of::() as isize) == 0)] + // The pointers share an allocation (or are literally the same address). + #[requires(ptr as isize == base as isize || ub_checks::same_allocation(ptr, base))] + #[ensures(|result: &isize| + *result == (ptr as isize - base as isize) / (crate::mem::size_of::() as isize))] + #[allow(dead_code)] + unsafe fn ptr_offset_from_wrapper(ptr: *const T, base: *const T) -> isize { + // SAFETY: guaranteed by the preconditions. + unsafe { ptr_offset_from(ptr, base) } + } + + // Same-generator pairs satisfy `same_allocation`; cross-generator pairs are + // pruned. For these primitive `T`, size == align, so in-bounds pairs satisfy + // the exact-multiple clause; covers witness zero/forward/backward distances. + macro_rules! check_ptr_offset_from_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(ptr_offset_from_wrapper)] + fn $harness() { + const GEN_SIZE: usize = mem::size_of::<$ty>(); + let mut generator1 = PointerGenerator::<{ GEN_SIZE * 4 }>::new(); + let mut generator2 = PointerGenerator::<{ GEN_SIZE * 4 }>::new(); + let ptr: *const $ty = generator1.any_in_bounds().ptr; + let base: *const $ty = if kani::any() { + generator1.any_in_bounds().ptr + } else { + generator2.any_in_bounds().ptr + }; + kani::cover(ptr.addr() == base.addr(), "offset_from: zero distance"); + kani::cover(ptr.addr() > base.addr(), "offset_from: forward distance"); + kani::cover(ptr.addr() < base.addr(), "offset_from: backward distance"); + let _ = unsafe { ptr_offset_from_wrapper::<$ty>(ptr, base) }; + } + }; + } + + check_ptr_offset_from_for!(check_ptr_offset_from_u8, u8); + check_ptr_offset_from_for!(check_ptr_offset_from_u32, u32); + check_ptr_offset_from_for!(check_ptr_offset_from_u64, u64); + check_ptr_offset_from_for!(check_ptr_offset_from_i32, i32); + check_ptr_offset_from_for!(check_ptr_offset_from_i128, i128); + + // ---- ptr_offset_from_unsigned ---- + // Unsigned variant of `ptr_offset_from`, same model. The first four + // `requires` are shared verbatim with `ptr_offset_from_wrapper`; the fifth + // adds the variant-specific `ptr >= base`. Ensures: the exact unsigned + // element distance (loss-free cast, since the distance is non-negative). + #[requires(crate::mem::size_of::() != 0)] + #[requires((ptr as isize).checked_sub(base as isize).is_some())] + #[requires((ptr as isize - base as isize) % (crate::mem::size_of::() as isize) == 0)] + #[requires(ptr as isize == base as isize || ub_checks::same_allocation(ptr, base))] + #[requires(ptr as isize >= base as isize)] + #[ensures(|result: &usize| + *result == ((ptr as isize - base as isize) / (crate::mem::size_of::() as isize)) as usize)] + #[allow(dead_code)] + unsafe fn ptr_offset_from_unsigned_wrapper(ptr: *const T, base: *const T) -> usize { + // SAFETY: guaranteed by the preconditions. + unsafe { ptr_offset_from_unsigned(ptr, base) } + } + + // As `check_ptr_offset_from_for`; `ptr >= base` prunes backward distances, + // so only the zero and forward covers remain. + macro_rules! check_ptr_offset_from_unsigned_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(ptr_offset_from_unsigned_wrapper)] + fn $harness() { + const GEN_SIZE: usize = mem::size_of::<$ty>(); + let mut generator1 = PointerGenerator::<{ GEN_SIZE * 4 }>::new(); + let mut generator2 = PointerGenerator::<{ GEN_SIZE * 4 }>::new(); + let ptr: *const $ty = generator1.any_in_bounds().ptr; + let base: *const $ty = if kani::any() { + generator1.any_in_bounds().ptr + } else { + generator2.any_in_bounds().ptr + }; + kani::cover(ptr.addr() == base.addr(), "offset_from_unsigned: zero distance"); + kani::cover(ptr.addr() > base.addr(), "offset_from_unsigned: forward distance"); + let _ = unsafe { ptr_offset_from_unsigned_wrapper::<$ty>(ptr, base) }; + } + }; + } + + check_ptr_offset_from_unsigned_for!(check_ptr_offset_from_unsigned_u8, u8); + check_ptr_offset_from_unsigned_for!(check_ptr_offset_from_unsigned_u32, u32); + check_ptr_offset_from_unsigned_for!(check_ptr_offset_from_unsigned_u64, u64); + check_ptr_offset_from_unsigned_for!(check_ptr_offset_from_unsigned_i32, i32); + check_ptr_offset_from_unsigned_for!(check_ptr_offset_from_unsigned_i128, i128); + + // ---- read_via_copy ---- + // Backs `ptr::read`; Kani models it as the plain typed load. Requires + // `can_dereference(ptr)`, the `# Safety` of `ptr::read`; a read has no + // `modifies` and no ensures. + #[requires(ub_checks::can_dereference(ptr))] + #[allow(dead_code)] + unsafe fn read_via_copy_model(ptr: *const T) -> T { + // SAFETY: guaranteed by the precondition. + unsafe { read_via_copy(ptr) } + } + + // Same setup rationale as `check_volatile_load_for`. + macro_rules! check_read_via_copy_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(read_via_copy_model)] + fn $harness() { + const N: usize = 100; + let mut buffer = [MaybeUninit::<$ty>::uninit(); N]; + for i in 0..N { + buffer[i] = MaybeUninit::new(kani::any()); + } + let base = buffer.as_ptr() as *const u8; + let ptr = base + .wrapping_add(kani::any_where(|o: &usize| *o < N * core::mem::size_of::<$ty>())) + as *const $ty; + kani::cover(true, "read_via_copy reaches a dereferenceable ptr"); + let _val = unsafe { read_via_copy_model(ptr) }; + } + }; + } + + check_read_via_copy_for!(check_read_via_copy_u8, u8); + check_read_via_copy_for!(check_read_via_copy_char, char); + check_read_via_copy_for!(check_read_via_copy_u32, u32); + + // ---- write_via_move ---- + // Backs `ptr::write`; Kani models it as the plain typed store. Requires only + // `can_write(ptr)`: the write overwrites without reading. Ensures the + // destination holds a fully-formed `T`; `*ptr == value` is not expressible + // because `value` is moved and generic `T: !Copy` cannot be re-read. + #[requires(ub_checks::can_write(ptr))] + #[ensures(|_| ub_checks::can_dereference(ptr as *const T))] + #[cfg_attr(kani, kani::modifies(ptr))] + #[allow(dead_code)] + unsafe fn write_via_move_model(ptr: *mut T, value: T) { + // SAFETY: guaranteed by the precondition. + unsafe { write_via_move(ptr, value) } + } + + // Destination deliberately left `MaybeUninit`: overwriting uninit memory is + // legal and exercised here; misaligned pointers from the byte-granular + // offset must be pruned by the alignment clause. + macro_rules! check_write_via_move_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(write_via_move_model)] + fn $harness() { + const N: usize = 100; + let mut buffer = [MaybeUninit::<$ty>::uninit(); N]; + let base = buffer.as_mut_ptr() as *mut u8; + let ptr = base + .wrapping_add(kani::any_where(|o: &usize| *o < N * core::mem::size_of::<$ty>())) + as *mut $ty; + let value: $ty = kani::any(); + kani::cover(true, "write_via_move reaches a writeable ptr"); + unsafe { write_via_move_model(ptr, value) }; + } + }; + } + + check_write_via_move_for!(check_write_via_move_u8, u8); + check_write_via_move_for!(check_write_via_move_char, char); + check_write_via_move_for!(check_write_via_move_u32, u32); + + // ---- compare_bytes ---- + // Backs slice comparison; Kani models it as a memcmp. Requires each pointer + // readable and initialized for the WHOLE `bytes` range, not merely up to the + // first differing byte (the docs stress chunked reads). No ensures: relating + // the returned sign to the first differing byte is functional, not safety. + #[requires(ub_checks::can_dereference(core::ptr::slice_from_raw_parts(left, bytes)) + && ub_checks::can_dereference(core::ptr::slice_from_raw_parts(right, bytes)))] + #[allow(dead_code)] + unsafe fn compare_bytes_model(left: *const u8, right: *const u8, bytes: usize) -> i32 { + // SAFETY: guaranteed by the precondition. + unsafe { compare_bytes(left, right, bytes) } + } + + // Both buffers fully initialized (whole-range clause otherwise + // unsatisfiable); `right` may alias `buffer1`. BOUNDED DOMAIN: the per-byte + // memcmp loop does not terminate under bounded model checking for unbounded + // `bytes`, so the range is capped at `MAX_BYTES = 8` with matching + // `kani::unwind`; the bound limits the checked instances, not the contract. + const MAX_BYTES: usize = 8; + + #[kani::proof_for_contract(compare_bytes_model)] + #[kani::unwind(9)] // MAX_BYTES + 1 + fn check_compare_bytes() { + const N: usize = MAX_BYTES; + let mut buffer1 = [MaybeUninit::::uninit(); N]; + let mut buffer2 = [MaybeUninit::::uninit(); N]; + for i in 0..N { + buffer1[i] = MaybeUninit::new(kani::any()); + buffer2[i] = MaybeUninit::new(kani::any()); + } + let gen_any_ptr = |buf: &[MaybeUninit; N]| -> *const u8 { + (buf.as_ptr() as *const u8).wrapping_add(kani::any_where(|o: &usize| *o < N)) + }; + let left = gen_any_ptr(&buffer1); + // `right` may alias `buffer1` or point into a separate allocation. + let right = if kani::any() { gen_any_ptr(&buffer2) } else { gen_any_ptr(&buffer1) }; + // Unconstrained `bytes` is pruned to `<= MAX_BYTES` by `can_dereference`. + let bytes: usize = kani::any(); + kani::cover(bytes > 0, "compare_bytes compares a non-empty range"); + let _ = unsafe { compare_bytes_model(left, right, bytes) }; + } + // FIXME: Enable this harness once is fixed. // Harness triggers a spurious failure when writing 0 bytes to an invalid memory location, // which is a safe operation. - #[cfg(not(kani))] - #[kani::proof_for_contract(write_bytes)] - fn check_write_bytes() { - let mut generator = PointerGenerator::<100>::new(); - let ArbitraryPointer { ptr, status, .. } = generator.any_alloc_status::(); - kani::assume(supported_status(status)); - unsafe { write_bytes(ptr, kani::any(), kani::any()) }; - } + // + // Superseded by `write_bytes_wrapper` + `check_write_bytes_*` above, which + // carry a contract and keep `dst` in a live allocation (sidestepping #90). fn run_with_arbitrary_ptrs(harness: impl Fn(*mut T, *mut T)) { let mut generator1 = PointerGenerator::<100>::new(); diff --git a/library/core/src/mem/maybe_uninit.rs b/library/core/src/mem/maybe_uninit.rs index 3507d1a0a9a8c..a956dd846baae 100644 --- a/library/core/src/mem/maybe_uninit.rs +++ b/library/core/src/mem/maybe_uninit.rs @@ -1,5 +1,9 @@ +use safety::ensures; + use crate::any::type_name; use crate::clone::TrivialClone; +#[cfg(kani)] +use crate::kani; use crate::marker::Destruct; use crate::mem::ManuallyDrop; use crate::{fmt, intrinsics, ptr, slice}; @@ -467,6 +471,17 @@ impl MaybeUninit { #[rustc_diagnostic_item = "maybe_uninit_zeroed"] #[stable(feature = "maybe_uninit", since = "1.36.0")] #[rustc_const_stable(feature = "const_maybe_uninit_zeroed", since = "1.75.0")] + // No `requires` (challenge 2, part 2): the `intrinsics::write_bytes` conditions + // hold structurally for the fresh stack local `u`. Ensures covers bytes only; + // whether they form a valid `T` remains the caller's concern. + #[ensures(|result: &MaybeUninit| { + // SAFETY: `zeroed` just initialized every backing byte; `u8` has no + // invalid bit patterns. + let bytes = unsafe { + slice::from_raw_parts(result.as_ptr() as *const u8, crate::mem::size_of::()) + }; + bytes.iter().all(|b| *b == 0) + })] pub const fn zeroed() -> MaybeUninit { let mut u = MaybeUninit::::uninit(); // SAFETY: `u.as_mut_ptr()` points to allocated memory. @@ -1614,3 +1629,55 @@ impl SpecFill for [MaybeUninit] { self.fill_with(|| MaybeUninit::new(unsafe { ptr::read(&value) })); } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + // ------------------------------------------------------------------------- + // zeroed: `write_bytes` is body-less (Kani models it as `memset`), so nothing + // to stub (https://github.com/model-checking/kani/issues/3325); intrinsic-side + // contract is on `write_bytes_wrapper` in `intrinsics/mod.rs`. The byte-level + // `ensures` also pins the model's fidelity. No arguments, so non-vacuous. + + // Safety + byte-fidelity family; `(u8, bool)` covers the documented + // padding-free "all fields hold bit-pattern 0" case. + macro_rules! check_zeroed_usage_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(MaybeUninit::zeroed)] + fn $harness() { + let _m = MaybeUninit::<$ty>::zeroed(); + kani::cover(true, "zeroed usage is reachable"); + } + }; + } + + check_zeroed_usage_for!(check_zeroed_usage_u8, u8); + check_zeroed_usage_for!(check_zeroed_usage_u32, u32); + check_zeroed_usage_for!(check_zeroed_usage_u64, u64); + check_zeroed_usage_for!(check_zeroed_usage_i128, i128); + check_zeroed_usage_for!(check_zeroed_usage_char, char); + check_zeroed_usage_for!(check_zeroed_usage_pair, (u8, bool)); + + // Value family: connects the byte-level `ensures` to the numeric zero for + // types where the all-zero pattern is a valid value. + macro_rules! check_zeroed_value_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(MaybeUninit::zeroed)] + fn $harness() { + let m = MaybeUninit::<$ty>::zeroed(); + kani::cover(true, "zeroed value usage is reachable"); + // SAFETY: `0` is a valid bit pattern for `$ty`. + let v = unsafe { m.assume_init() }; + assert!(v == 0 as $ty, "zeroed initializes to the numeric zero"); + } + }; + } + + check_zeroed_value_for!(check_zeroed_value_u8, u8); + check_zeroed_value_for!(check_zeroed_value_u32, u32); + check_zeroed_value_for!(check_zeroed_value_u64, u64); + check_zeroed_value_for!(check_zeroed_value_i128, i128); +} diff --git a/library/core/src/mem/mod.rs b/library/core/src/mem/mod.rs index eb235cbf10147..49a93d5bb42d5 100644 --- a/library/core/src/mem/mod.rs +++ b/library/core/src/mem/mod.rs @@ -5,13 +5,15 @@ #![stable(feature = "rust1", since = "1.0.0")] +use safety::{ensures, requires}; + use crate::alloc::Layout; use crate::clone::TrivialClone; #[cfg(kani)] use crate::kani; use crate::marker::{Destruct, DiscriminantKind}; use crate::panic::const_assert; -use crate::{clone, cmp, fmt, hash, intrinsics, ptr}; +use crate::{clone, cmp, fmt, hash, intrinsics, ptr, ub_checks}; mod manually_drop; #[stable(feature = "manually_drop", since = "1.20.0")] @@ -510,6 +512,10 @@ pub const fn align_of() -> usize { #[must_use] #[stable(feature = "rust1", since = "1.0.0")] #[rustc_const_stable(feature = "const_align_of_val", since = "1.85.0")] +// No `requires` (challenge 2, part 2): the intrinsic's sole documented condition, +// `can_dereference`, holds structurally for the live reference `val: &T`. +// Intrinsic-side contract: `align_of_val_{sized,slice}_wrapper` in `intrinsics/mod.rs`. +#[ensures(|result: &usize| result.is_power_of_two())] pub const fn align_of_val(val: &T) -> usize { // SAFETY: val is a reference, so it's a valid raw pointer unsafe { intrinsics::align_of_val(val) } @@ -557,6 +563,10 @@ pub const fn align_of_val(val: &T) -> usize { #[inline] #[must_use] #[unstable(feature = "layout_for_ptr", issue = "69835")] +// No `requires` (challenge 2, part 3): the documented `# Safety` condition is per-case, +// and the Kani-modeled intrinsic reads only pointer metadata, never the referent; +// per-case demos: `align_of_val_{sized,slice}_wrapper` in `intrinsics/mod.rs`. +#[ensures(|result: &usize| result.is_power_of_two())] pub const unsafe fn align_of_val_raw(val: *const T) -> usize { // SAFETY: the caller must provide a valid raw pointer unsafe { intrinsics::align_of_val(val) } @@ -1529,4 +1539,148 @@ mod verify { forget(x); forget(y); } + + // ------------------------------------------------------------------------- + // swap: two live `&mut T` structurally satisfy the `typed_swap_nonoverlapping` + // contract (`intrinsics/mod.rs`). `stub_verified` turns each intrinsic + // `requires` into a call-site obligation; without the stub they are absent. + // Value equality is per concrete type: bound is only `T`, no `PartialEq`. + macro_rules! check_swap_usage_for { + ($safety:ident, $value:ident, $ty:ty) => { + #[kani::proof_for_contract(swap)] + #[kani::stub_verified(intrinsics::typed_swap_nonoverlapping)] + fn $safety() { + let mut x: $ty = kani::any(); + let mut y: $ty = kani::any(); + // Non-vacuity witness: no assume narrows the inputs. + kani::cover(true, "swap usage: the &mut argument space is non-empty"); + swap(&mut x, &mut y); + } + + #[kani::proof_for_contract(swap)] + fn $value() { + let mut x: $ty = kani::any(); + let mut y: $ty = kani::any(); + let old_x = x; + let old_y = y; + kani::cover(old_x != old_y, "swap exchanges two distinct values"); + swap(&mut x, &mut y); + assert!(x == old_y && y == old_x, "swap exchanges the two values"); + } + }; + } + + check_swap_usage_for!(check_swap_usage_u8, check_swap_value_u8, u8); + check_swap_usage_for!(check_swap_usage_u16, check_swap_value_u16, u16); + check_swap_usage_for!(check_swap_usage_u32, check_swap_value_u32, u32); + check_swap_usage_for!(check_swap_usage_u64, check_swap_value_u64, u64); + check_swap_usage_for!(check_swap_usage_char, check_swap_value_char, char); + + // ------------------------------------------------------------------------- + // align_of_val: body-less intrinsic, so no contract to stub + // (https://github.com/model-checking/kani/issues/3325); intrinsic-side contract + // is on `align_of_val_{sized,slice}_wrapper` in `intrinsics/mod.rs`. Harnesses + // pin Kani's model per type (generic `ensures` impossible for `T: ?Sized`). + + // Sized case: model must return `align_of::()`, pointer-independent. + macro_rules! check_align_of_val_usage_sized_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(align_of_val)] + fn $harness() { + let val: $ty = kani::any(); + let r = align_of_val(&val); + kani::cover(true, "align_of_val usage (sized) is reachable"); + assert_eq!(r, align_of::<$ty>()); + } + }; + } + + check_align_of_val_usage_sized_for!(check_align_of_val_usage_u8, u8); + check_align_of_val_usage_sized_for!(check_align_of_val_usage_u32, u32); + check_align_of_val_usage_sized_for!(check_align_of_val_usage_u64, u64); + check_align_of_val_usage_sized_for!(check_align_of_val_usage_i128, i128); + check_align_of_val_usage_sized_for!(check_align_of_val_usage_char, char); + + // Slice case: a slice's alignment is its element's, independent of `len`. + macro_rules! check_align_of_val_usage_slice_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(align_of_val)] + fn $harness() { + const N: usize = 4; + let arr: [$ty; N] = kani::any(); + let len: usize = kani::any_where(|l: &usize| *l <= N); + let s: &[$ty] = &arr[..len]; + kani::cover(len > 0, "align_of_val usage measures a non-empty slice"); + let r = align_of_val(s); + assert_eq!(r, align_of::<$ty>()); + } + }; + } + + check_align_of_val_usage_slice_for!(check_align_of_val_usage_slice_u8, u8); + check_align_of_val_usage_slice_for!(check_align_of_val_usage_slice_u32, u32); + check_align_of_val_usage_slice_for!(check_align_of_val_usage_slice_i64, i64); + + // ------------------------------------------------------------------------- + // align_of_val_raw (challenge 2, part 3): raw-pointer sibling; same body-less + // modeling as above, pinned per type. Each harness builds `val` from a live + // allocation, so the input space is non-empty. + + // Sized case: model must return `align_of::()`, pointer-independent. + macro_rules! check_align_of_val_raw_sized_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(align_of_val_raw)] + fn $harness() { + let val: $ty = kani::any(); + let ptr: *const $ty = &val; + let align = unsafe { align_of_val_raw(ptr) }; + kani::cover(true, "align_of_val_raw (sized) call is reachable"); + assert_eq!(align, align_of::<$ty>()); + } + }; + } + + check_align_of_val_raw_sized_for!(check_align_of_val_raw_u8, u8); + check_align_of_val_raw_sized_for!(check_align_of_val_raw_u32, u32); + check_align_of_val_raw_sized_for!(check_align_of_val_raw_u64, u64); + check_align_of_val_raw_sized_for!(check_align_of_val_raw_i128, i128); + check_align_of_val_raw_sized_for!(check_align_of_val_raw_char, char); + + // Sized + dangling: demonstrates the documented "always safe if `T: Sized`", + // even non-dereferenceable (the modeled intrinsic reads no memory). + macro_rules! check_align_of_val_raw_dangling_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(align_of_val_raw)] + fn $harness() { + let ptr: *const $ty = crate::ptr::dangling(); + let align = unsafe { align_of_val_raw(ptr) }; + kani::cover(true, "align_of_val_raw accepts a dangling sized pointer"); + assert_eq!(align, align_of::<$ty>()); + } + }; + } + + check_align_of_val_raw_dangling_for!(check_align_of_val_raw_dangling_u8, u8); + check_align_of_val_raw_dangling_for!(check_align_of_val_raw_dangling_u64, u64); + + // Slice case: initialized backing array so `can_dereference` holds; + // alignment is independent of `len`. + macro_rules! check_align_of_val_raw_slice_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(align_of_val_raw)] + fn $harness() { + const N: usize = 4; + let arr: [$ty; N] = kani::any(); + let len: usize = kani::any_where(|l: &usize| *l <= N); + let ptr: *const [$ty] = core::ptr::slice_from_raw_parts(arr.as_ptr(), len); + let align = unsafe { align_of_val_raw(ptr) }; + kani::cover(len > 0, "align_of_val_raw measures a non-empty slice"); + assert_eq!(align, align_of::<$ty>()); + } + }; + } + + check_align_of_val_raw_slice_for!(check_align_of_val_raw_slice_u8, u8); + check_align_of_val_raw_slice_for!(check_align_of_val_raw_slice_u32, u32); + check_align_of_val_raw_slice_for!(check_align_of_val_raw_slice_i64, i64); } diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index 52556a7019014..207898d91d848 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -696,6 +696,20 @@ pub const unsafe fn copy(src: *const T, dst: *mut T, count: usize) { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_diagnostic_item = "ptr_write_bytes"] +// Challenge 2, part 3: the intrinsic's contract carried through this thin wrapper +// (identical to `write_bytes_wrapper` in `intrinsics/mod.rs`). Alignment is demanded +// even for a zero-sized write, matching the body's `assert_unsafe_precondition!`. +// Ensures as `*const u8`: the region is initialized as bytes, need not be a valid `T`. +#[cfg_attr(kani, kani::modifies(slice_from_raw_parts(dst, count)))] +#[safety::requires(!count.overflowing_mul(mem::size_of::()).1 + && ub_checks::can_write(slice_from_raw_parts_mut(dst, count)))] +#[safety::requires(ub_checks::maybe_is_aligned_and_not_null( + dst as *const (), + mem::align_of::(), + mem::size_of::() == 0 || count == 0, +))] +#[safety::ensures(|_| ub_checks::can_dereference( + slice_from_raw_parts(dst as *const u8, count * mem::size_of::())))] pub const unsafe fn write_bytes(dst: *mut T, val: u8, count: usize) { // SAFETY: the safety contract for `write_bytes` must be upheld by the caller. unsafe { @@ -1296,6 +1310,14 @@ pub const fn slice_from_raw_parts_mut(data: *mut T, len: usize) -> *mut [T] { #[stable(feature = "rust1", since = "1.0.0")] #[rustc_const_stable(feature = "const_swap", since = "1.85.0")] #[rustc_diagnostic_item = "ptr_swap"] +// `swap` permits overlap (unlike `swap_nonoverlapping`), so no non-overlap clause. +// Ensures mirrors `typed_swap_nonoverlapping`: both pointers stay dereferenceable. +// `modifies` covers caller-visible writes only (the scratch is a function local). +#[cfg_attr(kani, kani::modifies(x))] +#[cfg_attr(kani, kani::modifies(y))] +#[safety::requires(ub_checks::can_dereference(x) && ub_checks::can_write(x))] +#[safety::requires(ub_checks::can_dereference(y) && ub_checks::can_write(y))] +#[safety::ensures(|_| ub_checks::can_dereference(x) && ub_checks::can_dereference(y))] pub const unsafe fn swap(x: *mut T, y: *mut T) { // Give ourselves some scratch space to work with. // We do not have to worry about drops: `MaybeUninit` does nothing when dropped. @@ -2854,4 +2876,110 @@ mod verify { let p = kani::any::() as *const [char; 5]; check_align_offset(p); } + + // ------------------------------------------------------------------------- + // swap: the `copy` / `copy_nonoverlapping` intrinsics carry no attachable + // contract (kani#3325 note in `intrinsics/mod.rs`), so nothing to stub; verify + // against Kani's model. Contract harnesses exercise the overlap-permitted + // path; value harnesses are per type (bound is only `T`, no `PartialEq`). + + // `y` may come from `x`'s generator, so regions may overlap (for these + // `align == size` types aligned overlap means `x == y`). Dangling / dead + // allocations are excluded: Kani's memory predicates do not model them + // (same restriction as the intrinsics' `run_with_arbitrary_ptrs`). + fn swap_with_arbitrary_ptrs(harness: impl Fn(*mut T, *mut T)) { + let mut generator1 = kani::PointerGenerator::<100>::new(); + let mut generator2 = kani::PointerGenerator::<100>::new(); + let kani::ArbitraryPointer { ptr: x, status: x_status, .. } = + generator1.any_alloc_status::(); + let kani::ArbitraryPointer { ptr: y, status: y_status, .. } = if kani::any() { + generator1.any_alloc_status::() + } else { + generator2.any_alloc_status::() + }; + kani::assume( + x_status != kani::AllocationStatus::Dangling + && x_status != kani::AllocationStatus::DeadObject, + ); + kani::assume( + y_status != kani::AllocationStatus::Dangling + && y_status != kani::AllocationStatus::DeadObject, + ); + // Non-vacuity witness for the assumed pointer space. + kani::cover(true, "swap contract: the arbitrary-pointer input space is non-empty"); + harness(x, y); + } + + macro_rules! check_swap_contract_for { + ($name:ident, $ty:ty) => { + #[kani::proof_for_contract(swap)] + fn $name() { + swap_with_arbitrary_ptrs::<$ty>(|x, y| unsafe { swap(x, y) }); + } + }; + } + + check_swap_contract_for!(check_swap_contract_u8, u8); + check_swap_contract_for!(check_swap_contract_u16, u16); + check_swap_contract_for!(check_swap_contract_u32, u32); + check_swap_contract_for!(check_swap_contract_u64, u64); + check_swap_contract_for!(check_swap_contract_char, char); + check_swap_contract_for!(check_swap_contract_non_zero, core::num::NonZeroI32); + + macro_rules! check_swap_value_for { + ($name:ident, $ty:ty) => { + #[kani::proof_for_contract(swap)] + fn $name() { + let mut a: $ty = kani::any(); + let mut b: $ty = kani::any(); + let old_a = a; + let old_b = b; + kani::cover(old_a != old_b, "swap exchanges two distinct values"); + unsafe { swap(&mut a as *mut $ty, &mut b as *mut $ty) }; + assert!(a == old_b && b == old_a, "swap exchanges the two values"); + } + }; + } + + check_swap_value_for!(check_swap_value_u8, u8); + check_swap_value_for!(check_swap_value_u16, u16); + check_swap_value_for!(check_swap_value_u32, u32); + check_swap_value_for!(check_swap_value_u64, u64); + check_swap_value_for!(check_swap_value_char, char); + + // ------------------------------------------------------------------------- + // write_bytes: challenge-2 part-3 raw-pointer item for `zeroed` (`ptr_zeroed`). + // The intrinsic is body-less (dummy body removed by rust-lang/rust#137489), so + // nothing to stub; verify the wrapper's contract against Kani's `memset` model. + // Post-write content is deliberately not asserted; see note after the harnesses. + + // Manual pointer setup keeps `dst` in a real allocation with byte-granular + // offsets, so misaligned `*mut $ty` values give the alignment clause teeth. + // Mirrors the intrinsic-side `check_write_bytes_*` in `intrinsics/mod.rs`. + macro_rules! check_ptr_write_bytes_for { + ($harness:ident, $ty:ty) => { + #[kani::proof_for_contract(write_bytes)] + fn $harness() { + const N: usize = 100; + let mut buffer = [MaybeUninit::<$ty>::uninit(); N]; + let base = buffer.as_mut_ptr() as *mut u8; + let dst = base + .wrapping_add(kani::any_where(|o: &usize| *o < N * core::mem::size_of::<$ty>())) + as *mut $ty; + let val: u8 = kani::any(); + let count: usize = kani::any(); + kani::cover(count > 0, "write_bytes writes a non-empty range"); + unsafe { write_bytes(dst, val, count) }; + } + }; + } + + check_ptr_write_bytes_for!(check_ptr_write_bytes_u8, u8); + check_ptr_write_bytes_for!(check_ptr_write_bytes_char, char); + check_ptr_write_bytes_for!(check_ptr_write_bytes_u32, u32); + check_ptr_write_bytes_for!(check_ptr_write_bytes_u64, u64); + + // No content harness: the `zeroed` case is pinned by `check_zeroed_value_*` + // in `maybe_uninit.rs`. A byte-granular post-read yields a spurious + // counterexample for multi-byte types in this Kani version, so left out. } diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index 8e19bbdca0cd4..491a022995ee5 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -3898,6 +3898,12 @@ impl [T] { #[stable(feature = "copy_from_slice", since = "1.9.0")] #[rustc_const_stable(feature = "const_copy_from_slice", since = "1.87.0")] #[track_caller] + // Equal lengths select the non-panicking path and make `ptr::copy_nonoverlapping` + // sound: both regions span `len` elements and cannot overlap (`&mut [T]` is + // exclusive). Element equality is per type below (`T: Copy`, no `PartialEq`). + #[requires(self.len() == src.len())] + #[ensures(|_| self.len() == src.len())] + #[cfg_attr(kani, kani::modifies(self))] pub const fn copy_from_slice(&mut self, src: &[T]) where T: Copy, @@ -5556,4 +5562,44 @@ mod verify { let mut a: [u8; 100] = kani::any(); a.reverse(); } + + // ------------------------------------------------------------------------- + // copy_from_slice: safety harnesses use a nondeterministic `len <= N`; value + // harnesses assert equality at one nondeterministic index over fixed `N` + // (the `check_copy_untyped` idiom in `intrinsics`). Fixed length is required: + // a symbolic index after a symbolic-length copy exceeds the memcpy model. + macro_rules! check_copy_from_slice_for { + ($safety:ident, $value:ident, $ty:ty) => { + #[kani::proof_for_contract(<[$ty]>::copy_from_slice)] + fn $safety() { + const N: usize = 32; + let src_arr: [$ty; N] = kani::any(); + let mut dst_arr: [$ty; N] = kani::any(); + let len = kani::any_where(|l: &usize| *l <= N); + let src = &src_arr[..len]; + let dst = &mut dst_arr[..len]; + kani::cover(len > 0, "copy_from_slice copies a non-empty slice"); + dst.copy_from_slice(src); + } + + #[kani::proof_for_contract(<[$ty]>::copy_from_slice)] + fn $value() { + const N: usize = 32; + let src_arr: [$ty; N] = kani::any(); + let mut dst_arr: [$ty; N] = kani::any(); + let src = &src_arr[..]; + let dst = &mut dst_arr[..]; + kani::cover(N > 0, "copy_from_slice copies a non-empty slice"); + dst.copy_from_slice(src); + let i = kani::any_where(|i: &usize| *i < N); + assert!(dst[i] == src[i], "copy_from_slice preserves elements"); + } + }; + } + + check_copy_from_slice_for!(check_copy_from_slice_u8, check_copy_from_slice_value_u8, u8); + check_copy_from_slice_for!(check_copy_from_slice_u16, check_copy_from_slice_value_u16, u16); + check_copy_from_slice_for!(check_copy_from_slice_u32, check_copy_from_slice_value_u32, u32); + check_copy_from_slice_for!(check_copy_from_slice_u64, check_copy_from_slice_value_u64, u64); + check_copy_from_slice_for!(check_copy_from_slice_char, check_copy_from_slice_value_char, char); }