From b2eaef87e8f90bb6bf105db6011fb207c0d333bd Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 18 Sep 2024 15:17:05 -0700 Subject: [PATCH] Final adjustments for new harnesses --- doc/src/challenges/0002-intrinsics-memory.md | 45 ++--- library/core/src/intrinsics.rs | 167 ++++++++----------- 2 files changed, 90 insertions(+), 122 deletions(-) diff --git a/doc/src/challenges/0002-intrinsics-memory.md b/doc/src/challenges/0002-intrinsics-memory.md index ec086b5d73dc5..ce8facf3bc278 100644 --- a/doc/src/challenges/0002-intrinsics-memory.md +++ b/doc/src/challenges/0002-intrinsics-memory.md @@ -23,28 +23,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 | -|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.rs b/library/core/src/intrinsics.rs index d6e54edc1cfcb..cf0467ede4827 100644 --- a/library/core/src/intrinsics.rs +++ b/library/core/src/intrinsics.rs @@ -1042,56 +1042,6 @@ extern "rust-intrinsic" { #[rustc_nounwind] pub fn breakpoint(); - /// Executes a breakpoint trap, for inspection by a debugger. - /// - /// This intrinsic does not have a stable counterpart. - #[rustc_nounwind] - // FIXME: Kani currently does not support annotating intrinsics. - // See https://github.com/model-checking/kani/issues/3325 - #[cfg_attr(not(kani), requires(matches!( - ::Metadata::map_dyn(crate::ptr::metadata(_val)::metadata(), - |dyn_meta| { ub_checks::can_dereference(dyn_meta)}), - None | Some(true))))] - #[cfg_attr(not(kani), requires(matches!( - ::Metadata::map_len(crate::ptr::metadata(_val)::metadata(), - |_| { ub_checks::can_dereference(_val)}), - None | Some(true))))] - pub fn size_of_val(_val: *const T) -> usize; - /// The required alignment of the referenced value. - /// - /// The stabilized version of this intrinsic is [`core::mem::align_of_val`]. - #[rustc_const_unstable(feature = "const_align_of_val", issue = "46571")] - #[rustc_nounwind] - pub fn min_align_of_val(_: *const T) -> usize; - - /// Gets a static string slice containing the name of a type. - /// - /// Note that, unlike most intrinsics, this is safe to call; - /// it does not require an `unsafe` block. - /// Therefore, implementations must not require the user to uphold - /// any safety invariants. - /// - /// The stabilized version of this intrinsic is [`core::any::type_name`]. - #[rustc_const_unstable(feature = "const_type_name", issue = "63084")] - #[rustc_safe_intrinsic] - #[rustc_nounwind] - pub fn type_name() -> &'static str; - - /// Gets an identifier which is globally unique to the specified type. This - /// function will return the same value for a type regardless of whichever - /// crate it is invoked in. - /// - /// Note that, unlike most intrinsics, this is safe to call; - /// it does not require an `unsafe` block. - /// Therefore, implementations must not require the user to uphold - /// any safety invariants. - /// - /// The stabilized version of this intrinsic is [`core::any::TypeId::of`]. - #[rustc_const_unstable(feature = "const_type_id", issue = "77125")] - #[rustc_safe_intrinsic] - #[rustc_nounwind] - pub fn type_id() -> u128; - /// A guard for unsafe functions that cannot ever be executed if `T` is uninhabited: /// This will statically either panic, or do nothing. /// @@ -3166,6 +3116,14 @@ pub const fn variant_count() -> usize { #[rustc_const_unstable(feature = "const_size_of_val", issue = "46571")] #[rustc_intrinsic] #[rustc_intrinsic_must_be_overridden] +#[cfg_attr(not(kani), requires(matches!( + ::Metadata::map_dyn(crate::ptr::metadata(_val)::metadata(), + |dyn_meta| { ub_checks::can_dereference(dyn_meta)}), + None | Some(true))))] +#[cfg_attr(not(kani), requires(matches!( + ::Metadata::map_len(crate::ptr::metadata(_val)::metadata(), + |_| { ub_checks::can_dereference(_val)}), + None | Some(true))))] pub const unsafe fn size_of_val(_ptr: *const T) -> usize { unreachable!() } @@ -3363,20 +3321,10 @@ pub const fn ptr_metadata + ?Sized, M>(_ptr: *cons #[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)))] -#[requires(ub_checks::is_nonoverlapping(src as *const (), dst as *const (), size_of::(), count))] -// TODO: Use quantifiers once it's available. -// Ensures the initialization state is preserved. -#[ensures(|_| { - if count > 0 { - let byte = kani::any_where(| sz: &usize | *sz < size_of::< T >); - let elem = kani::any_where(| val: &usize | *val < count); - let src_data = src as * const u8; - let dst_data = unsafe { dst.offset(elem) } as * const u8; - ub_checks::can_dereference(unsafe { src_data.offset(byte) }) - == ub_checks::can_dereference(unsafe { dst_data.offset(byte) }) - } -})] + && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)) + && ub_checks::is_nonoverlapping(src as *const (), dst as *const (), size_of::(), 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_nonoverlapping(src: *const T, dst: *mut T, count: usize) { extern "rust-intrinsic" { #[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")] @@ -3483,16 +3431,8 @@ pub const unsafe fn copy_nonoverlapping(src: *const T, dst: *mut T, count: us #[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(|_| { - if count > 0 { - let byte = kani::any_where(| sz: &usize | *sz < size_of::< T >); - let elem = kani::any_where(| val: &usize | *val < count); - let src_data = src as * const u8; - let dst_data = unsafe { dst.offset(elem) } as * const u8; - ub_checks::can_dereference(unsafe { src_data.offset(byte) }) - == ub_checks::can_dereference(unsafe { dst_data.offset(byte) }) - } -})] +#[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) { extern "rust-intrinsic" { #[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")] @@ -3576,14 +3516,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"] -#[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))] #[requires(!count.overflowing_mul(size_of::()).1 - && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst as *mut u8, count)))] -// TODO: Change this to quantifiers when available. -#[ensures(|_| { - let idx = kani::any_where(|idx: &usize| *idx < count); - ub_checks::can_dereference(dst.offset(idx) as * const u8) -})] + && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)))] +#[requires(count > 0 || ub_checks::is_aligned_and_not_null(dst as *const (), align_of::()))] +#[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) { extern "rust-intrinsic" { #[rustc_const_unstable(feature = "const_ptr_write", issue = "86302")] @@ -3605,6 +3543,21 @@ pub const unsafe fn write_bytes(dst: *mut T, val: u8, count: usize) { } } +// Ensures the initialization state is preserved. +// This is used for contracts only. +fn check_copy_untyped(src: *const T, dst: *mut T, count: usize) -> bool { + if count > 0 { + let byte = kani::any_where(| sz: &usize | *sz < size_of::< T >()); + 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 + } +} + /// Inform Miri that a given pointer definitely has a certain alignment. #[cfg(miri)] pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize) { @@ -3632,6 +3585,7 @@ pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize mod verify { use core::{cmp, fmt}; use core::ptr::addr_of_mut; + use core::mem::MaybeUninit; use super::*; use crate::kani; @@ -3686,28 +3640,44 @@ mod verify { } impl ArbitraryPointers { - fn with_arbitrary(harness: F) where F: FnOnce(ArbitraryPointers) { + const MAX_SIZE_T: usize = 100; + const SIZE_T: usize = size_of::(); + + const IS_VALID: () = assert!(Self::SIZE_T < Self::MAX_SIZE_T, "Exceeded supported type size"); + + fn with_arbitrary(harness: F) where F: FnOnce(ArbitraryPointers) { + + #[repr(C)] + struct WithUninit { + bytes: [MaybeUninit; SIZE], + } + #[repr(C)] - struct WithPadding { - byte: u8, - // padding in the middle. - bytes: u64, + #[repr(packed)] + #[derive(kani::Arbitrary)] + struct Unaligned { + first: u8, + val: T, // If alignment of T > 1, this value will be unaligned but valid otherwise. } - let mut single = kani::any::(); - let ptr1 = addr_of_mut!(single); - // FIXME(kani) this should be but this is not available in `kani_core` yet: - // let mut array: [u8; 100] = kani::any(); - let mut array = [kani::any::(), 100]; - let ptr2 = addr_of_mut!(array) as *mut u32; + let mut single = kani::any::(); + let single_ptr = addr_of_mut!(single); - let mut buffer = [0u8; 6]; - let unaligned = unsafe { addr_of_mut!(buffer).byte_offset(1) } as *mut u32; + let mut array: [T; 100] = kani::any(); + let array_ptr = addr_of_mut!(array) as *mut T; - let mut padding = WithPadding { byte: kani::any(), bytes: kani::any()}; - let uninit = unsafe { addr_of_mut!(padding.byte).byte_offset(4)} as *mut u32; + let mut unaligned: Unaligned = kani::any(); + let unaligned_ptr = addr_of_mut!(unaligned.val) as *mut T; + + let mut uninit = WithUninit { bytes: [MaybeUninit::zeroed(); Self::MAX_SIZE_T] }; + for i in 0..Self::SIZE_T { + if kani::any() { + uninit.bytes[i] = MaybeUninit::uninit(); + } + } + let uninit_ptr = &mut uninit as *mut _ as *mut T; - let arbitrary = ArbitraryPointers::from(ptr1, ptr2, unaligned, uninit); + let arbitrary = ArbitraryPointers::from(single_ptr, array_ptr, unaligned_ptr, uninit_ptr); harness(arbitrary); } @@ -3748,7 +3718,6 @@ mod verify { } } - /// This harness currently fails because we cannot define the modifies clause for slices. #[kani::proof_for_contract(copy)] fn check_copy() { ArbitraryPointers::::with_arbitrary(|arbitrary| { @@ -3774,7 +3743,6 @@ mod verify { }); } - /// FIXME(kani): This harness currently fails because we cannot define the modifies clause for slices. #[kani::proof_for_contract(copy_nonoverlapping)] fn check_copy_nonoverlapping() { ArbitraryPointers::::with_arbitrary(|arbitrary| { @@ -3786,7 +3754,6 @@ mod verify { }); } - /// FIXME(kani): This harness currently fails because we cannot define the modifies clause for slices. #[kani::proof_for_contract(write_bytes)] fn check_write_bytes() { ArbitraryPointers::::with_arbitrary(|arbitrary| {