diff --git a/doc/src/challenges/0002-intrinsics-memory.md b/doc/src/challenges/0002-intrinsics-memory.md index 31c1c43225250..adb4176254804 100644 --- a/doc/src/challenges/0002-intrinsics-memory.md +++ b/doc/src/challenges/0002-intrinsics-memory.md @@ -24,29 +24,29 @@ Annotate Rust core::intrinsics functions that manipulate raw pointers with their Intrinsic functions to be annotated with safety contracts -| Function | Location | -|---------|---------| -|typed_swap | core::intrisics | -|vtable_size| core::intrisics | -|vtable_align| core::intrisics | -|copy_nonoverlapping| core::intrisics | -|copy| core::intrisics | -|write_bytes| core::intrisics | -|size_of_val| core::intrisics | -|arith_offset| core::intrisics | -|volatile_copy_nonoverlapping_memory| core::intrisics | -|volatile_copy_memory| core::intrisics | -|volatile_set_memory| core::intrisics | -|volatile_load| core::intrisics | -|volatile_store| core::intrisics | -|unaligned_volatile_load| core::intrisics | -|unaligned_volatile_store| core::intrisics | -|compare_bytes| core::intrisics | -|min_align_of_val| core::intrisics | -|ptr_offset_from| core::intrisics | -|ptr_offset_from_unsigned| core::intrisics | -|read_via_copy| core::intrisics | -|write_via_move| core::intrisics | +| Function | Location | +|-------------------------------------|-----------------| +| typed_swap | core::intrisics | +| vtable_size | core::intrisics | +| vtable_align | core::intrisics | +| copy_nonoverlapping | core::intrisics | +| copy | core::intrisics | +| write_bytes | core::intrisics | +| size_of_val | core::intrisics | +| arith_offset | core::intrisics | +| volatile_copy_nonoverlapping_memory | core::intrisics | +| volatile_copy_memory | core::intrisics | +| volatile_set_memory | core::intrisics | +| volatile_load | core::intrisics | +| volatile_store | core::intrisics | +| unaligned_volatile_load | core::intrisics | +| unaligned_volatile_store | core::intrisics | +| compare_bytes | core::intrisics | +| min_align_of_val | core::intrisics | +| ptr_offset_from | core::intrisics | +| ptr_offset_from_unsigned | core::intrisics | +| read_via_copy | core::intrisics | +| write_via_move | core::intrisics | All the following usages of intrinsics were proven safe: diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index 38dbe91bea64a..29ef19daaf679 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -64,10 +64,10 @@ )] #![allow(missing_docs)] -use safety::requires; use crate::marker::{DiscriminantKind, Tuple}; use crate::mem::SizedTypeProperties; use crate::{ptr, ub_checks}; +use safety::{ensures, requires}; #[cfg(kani)] use crate::kani; @@ -3663,7 +3663,8 @@ pub const fn is_val_statically_known(_arg: T) -> bool { #[requires(ub_checks::can_dereference(x) && ub_checks::can_write(x))] #[requires(ub_checks::can_dereference(y) && ub_checks::can_write(y))] #[requires(x.addr() != y.addr() || core::mem::size_of::() == 0)] -#[requires((x.addr() >= y.addr() + core::mem::size_of::()) || (y.addr() >= x.addr() + core::mem::size_of::()))] +#[requires(ub_checks::maybe_is_nonoverlapping(x as *const (), y as *const (), size_of::(), 1))] +#[ensures(|_| ub_checks::can_dereference(x) && ub_checks::can_dereference(y))] pub const unsafe fn typed_swap(x: *mut T, y: *mut T) { // SAFETY: The caller provided single non-overlapping items behind // pointers, so swapping them with `count: 1` is fine. @@ -3737,6 +3738,9 @@ pub const unsafe fn const_deallocate(_ptr: *mut u8, _size: usize, _align: usize) #[unstable(feature = "core_intrinsics", issue = "none")] #[rustc_intrinsic] #[rustc_intrinsic_must_be_overridden] +// VTable pointers must be valid for dereferencing at least 3 `usize` (size, alignment and drop): +// +#[requires(ub_checks::can_dereference(_ptr as *const [usize; 3]))] pub unsafe fn vtable_size(_ptr: *const ()) -> usize { unreachable!() } @@ -3750,6 +3754,9 @@ pub unsafe fn vtable_size(_ptr: *const ()) -> usize { #[unstable(feature = "core_intrinsics", issue = "none")] #[rustc_intrinsic] #[rustc_intrinsic_must_be_overridden] +// VTable pointers must be valid for dereferencing at least 3 `usize` (size, alignment and drop): +// +#[requires(ub_checks::can_dereference(_ptr as *const [usize; 3]))] pub unsafe fn vtable_align(_ptr: *const ()) -> usize { unreachable!() } @@ -4034,6 +4041,13 @@ pub const fn ptr_metadata + ?Sized, M>(_ptr: *cons #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_diagnostic_item = "ptr_copy_nonoverlapping"] +// Copy is "untyped". +#[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))] +#[requires(!count.overflowing_mul(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 (), size_of::(), count))] +#[ensures(|_| { check_copy_untyped(src, dst, count)})] pub const unsafe fn copy_nonoverlapping(src: *const T, dst: *mut T, count: usize) { #[cfg_attr(bootstrap, rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0"))] #[cfg_attr(not(bootstrap), rustc_intrinsic_const_stable_indirect)] @@ -4141,6 +4155,11 @@ pub const unsafe fn copy_nonoverlapping(src: *const T, dst: *mut T, count: us #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_diagnostic_item = "ptr_copy"] +#[requires(!count.overflowing_mul(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)))] pub const unsafe fn copy(src: *const T, dst: *mut T, count: usize) { #[cfg_attr(bootstrap, rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0"))] #[cfg_attr(not(bootstrap), rustc_intrinsic_const_stable_indirect)] @@ -4225,6 +4244,12 @@ 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"] +#[requires(!count.overflowing_mul(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 (), align_of::(), T::IS_ZST || count == 0))] +#[ensures(|_| + ub_checks::can_dereference(crate::ptr::slice_from_raw_parts(dst as *const u8, count * size_of::())))] +#[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))] pub const unsafe fn write_bytes(dst: *mut T, val: u8, count: usize) { #[cfg_attr(bootstrap, rustc_const_stable(feature = "const_ptr_write", since = "1.83.0"))] #[cfg_attr(not(bootstrap), rustc_intrinsic_const_stable_indirect)] @@ -4513,6 +4538,36 @@ pub const unsafe fn copysignf128(_x: f128, _y: f128) -> f128 { unimplemented!(); } +/// Return whether the initialization state is preserved. +/// +/// For untyped copy, done via `copy` and `copy_nonoverlapping`, the copies of non-initialized +/// bytes (such as padding bytes) should result in a non-initialized copy, while copies of +/// initialized bytes result in initialized bytes. +/// +/// It is UB to read the uninitialized bytes, so we cannot compare their values only their +/// initialization state. +/// +/// This is used for contracts only. +/// +/// FIXME: Change this once we add support to quantifiers. +#[allow(dead_code)] +#[allow(unused_variables)] +fn check_copy_untyped(src: *const T, dst: *mut T, count: usize) -> bool { + #[cfg(kani)] + if count > 0 { + let byte = kani::any_where(|sz: &usize| *sz < size_of::()); + let elem = kani::any_where(|val: &usize| *val < count); + let src_data = src 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) }) + } else { + true + } + #[cfg(not(kani))] + false +} + /// Inform Miri that a given pointer definitely has a certain alignment. #[cfg(miri)] #[rustc_allow_const_fn_unstable(const_eval_select)] @@ -4538,35 +4593,99 @@ pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize } #[cfg(kani)] -#[unstable(feature="kani", issue="none")] +#[unstable(feature = "kani", issue = "none")] mod verify { - use core::{cmp, fmt}; use super::*; use crate::kani; + use core::mem::MaybeUninit; + use kani::{AllocationStatus, Arbitrary, ArbitraryPointer, PointerGenerator}; #[kani::proof_for_contract(typed_swap)] pub fn check_typed_swap_u8() { - check_swap::() + run_with_arbitrary_ptrs::(|x, y| unsafe { typed_swap(x, y) }); } #[kani::proof_for_contract(typed_swap)] pub fn check_typed_swap_char() { - check_swap::() + run_with_arbitrary_ptrs::(|x, y| unsafe { typed_swap(x, y) }); } #[kani::proof_for_contract(typed_swap)] pub fn check_typed_swap_non_zero() { - check_swap::() + run_with_arbitrary_ptrs::(|x, y| unsafe { typed_swap(x, y) }); } - pub fn check_swap() { - let mut x = kani::any::(); - let old_x = x; - let mut y = kani::any::(); - let old_y = y; + #[kani::proof_for_contract(copy)] + fn check_copy() { + run_with_arbitrary_ptrs::(|src, dst| unsafe { copy(src, dst, kani::any()) }); + } - unsafe { typed_swap(&mut x, &mut y) }; - assert_eq!(y, old_x); - assert_eq!(x, old_y); + #[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()) } + } + + // 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()) }; + } + + fn run_with_arbitrary_ptrs(harness: impl Fn(*mut T, *mut T)) { + let mut generator1 = PointerGenerator::<100>::new(); + let mut generator2 = PointerGenerator::<100>::new(); + let ArbitraryPointer { + ptr: src, + status: src_status, + .. + } = generator1.any_alloc_status::(); + let ArbitraryPointer { + ptr: dst, + status: dst_status, + .. + } = if kani::any() { + generator1.any_alloc_status::() + } else { + generator2.any_alloc_status::() + }; + kani::assume(supported_status(src_status)); + kani::assume(supported_status(dst_status)); + harness(src, dst); + } + + /// Return whether the current status is supported by Kani's contract. + /// + /// Kani memory predicates currently doesn't support pointers to dangling or dead allocations. + /// Thus, we have to explicitly exclude those cases. + fn supported_status(status: AllocationStatus) -> bool { + status != AllocationStatus::Dangling && status != AllocationStatus::DeadObject } }