From d4aa09f1f4a7f772c284ec361a8b5926b9877bec Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 15 Jul 2024 20:34:06 -0700 Subject: [PATCH] Add a few intrinsics contracts - This is not working due to a Kani limitation --- doc/src/challenges/0002-intrinsics-memory.md | 1 - library/core/src/intrinsics.rs | 177 ++++++++++++++++++- library/core/src/ub_checks.rs | 66 +++++++ 3 files changed, 241 insertions(+), 3 deletions(-) diff --git a/doc/src/challenges/0002-intrinsics-memory.md b/doc/src/challenges/0002-intrinsics-memory.md index 3eac59fb02681..62ee3a8c4dab6 100644 --- a/doc/src/challenges/0002-intrinsics-memory.md +++ b/doc/src/challenges/0002-intrinsics-memory.md @@ -32,7 +32,6 @@ Intrinsic functions to be annotated with safety contracts |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 | diff --git a/library/core/src/intrinsics.rs b/library/core/src/intrinsics.rs index 1ab7ef9b5dc72..396226d44143c 100644 --- a/library/core/src/intrinsics.rs +++ b/library/core/src/intrinsics.rs @@ -1064,7 +1064,17 @@ extern "rust-intrinsic" { /// The stabilized version of this intrinsic is [`crate::mem::size_of_val`]. #[rustc_const_unstable(feature = "const_size_of_val", issue = "46571")] #[rustc_nounwind] - pub fn size_of_val(_: *const T) -> usize; + // 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`]. @@ -2790,6 +2800,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] +// FIXME(kani): Cannot verify intrinsics contract yet. +// +#[requires(ub_checks::can_dereference(_ptr as *const crate::ptr::DynMetadata))] pub unsafe fn vtable_size(_ptr: *const ()) -> usize { unreachable!() } @@ -2800,6 +2813,9 @@ pub unsafe fn vtable_size(_ptr: *const ()) -> usize { #[unstable(feature = "core_intrinsics", issue = "none")] #[rustc_intrinsic] #[rustc_intrinsic_must_be_overridden] +// FIXME(kani): Cannot verify intrinsics contract yet. +// +#[requires(ub_checks::can_dereference(_ptr as *const crate::ptr::DynMetadata))] pub unsafe fn vtable_align(_ptr: *const ()) -> usize { unreachable!() } @@ -2927,6 +2943,14 @@ impl AggregateRawPtr<*mut T> for *mut P { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_diagnostic_item = "ptr_copy_nonoverlapping"] +#[requires(!count.overflowing_mul(size_of::()).1 + && ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src, count)) + && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)))] +#[requires(src.addr() != dst.addr() || core::mem::size_of::() == 0)] +#[requires((src.addr() >= dst.addr() + core::mem::size_of::()) || (dst.addr() >= src.addr() + core::mem::size_of::()))] +// TODO: Modifies doesn't work with slices today. +// https://github.com/model-checking/kani/pull/3295 +// #[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")] @@ -3029,6 +3053,13 @@ 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"] +// FIXME: How to verify safety for types that do not implement Copy and count > 1?? +#[requires(!count.overflowing_mul(size_of::()).1 + && ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src, count)) + && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)))] +// TODO: Modifies doesn't work with slices today. +// https://github.com/model-checking/kani/pull/3295 +// #[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")] @@ -3048,7 +3079,10 @@ pub const unsafe fn copy(src: *const T, dst: *mut T, count: usize) { align: usize = align_of::(), ) => ub_checks::is_aligned_and_not_null(src, align) - && ub_checks::is_aligned_and_not_null(dst, align) + + + + && ub_checks::is_aligned_and_not_null(dst, align) ); copy(src, dst, count) } @@ -3110,6 +3144,11 @@ 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 as *mut u8, count)))] +// TODO: Modifies doesn't work with slices today. +// https://github.com/model-checking/kani/pull/3295 +// #[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")] @@ -3185,4 +3224,138 @@ mod verify { assert_eq!(y, old_x); assert_eq!(x, old_y); } + + /// Note that in `core` we cannot check allocated pointers. + #[derive(Copy, Clone, Debug, PartialEq, Eq, kani::Arbitrary)] + enum PtrKind { + /// Dangling pointers + Dangling, + /// Null pointers + Null, + /// Stack pointers + Stack, + /// Overlapping pointers + Overlap, + /// Unaligned pointers + Unaligned, + /// Pointer to uninitialized memory + Uninitialized, + } + + struct ArbitraryPointers { + src: *const T, + dst: *mut T, + dst_kind: PtrKind, + src_kind: PtrKind, + } + + impl ArbitraryPointers { + fn with_arbitrary(harness: F) where F: FnOnce(ArbitraryPointers) { + #[repr(C)] + struct WithPadding { + byte: u8, + // padding in the middle. + bytes: u64, + } + let mut single = kani::any::(); + let ptr1 = crate::ptr::addr_of_mut!(single); + + let mut array = [kani::any::(); 100]; + let ptr2 = crate::ptr::addr_of_mut!(array) as *mut u32; + + let mut buffer = [0u8, 6]; + let unaligned = unsafe { crate::ptr::addr_of_mut!(buffer).byte_offset(1) } as *mut u32; + + let mut padding = WithPadding { byte: 0, bytes: 0}; + let uninit = unsafe { crate::ptr::addr_of_mut!(padding.byte).byte_offset(4)} as *mut u32; + + let arbitrary = ArbitraryPointers::from(ptr1, ptr2, unaligned, uninit); + harness(arbitrary); + } + + fn from(ptr1: *mut T, ptr2: *mut T, unaligned: *mut T, uninit: *mut T) -> Self { + let (src_kind, src) = ArbitraryPointers::any(ptr1, ptr2, unaligned, uninit); + let (dst_kind, dst) = ArbitraryPointers::any(ptr2, ptr1, unaligned, uninit); + ArbitraryPointers { + src_kind, + src, + dst_kind, + dst, + } + } + + fn any(unique: *mut T, overlap: *mut T, unaligned: *mut T, uninit: *mut T) -> (PtrKind, *mut T) { + let kind = kani::any::(); + let ptr = match kind { + PtrKind::Dangling => { + crate::ptr::dangling_mut::() + } + PtrKind::Null => { + crate::ptr::null_mut::() + } + PtrKind::Stack => { + unique + } + PtrKind::Overlap => { + if kani::any() { unique } else { overlap } + } + PtrKind::Unaligned => { + unaligned + } + PtrKind::Uninitialized => { + uninit + } + }; + (kind, ptr) + } + } + + /// 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| { + // Skip dangling for now since it makes Kani contract panic. + // Verify this case in a separate harness. + kani::assume(arbitrary.dst_kind != PtrKind::Dangling); + kani::assume(arbitrary.src_kind != PtrKind::Dangling); + unsafe { copy(arbitrary.src, arbitrary.dst, kani::any()) } + }); + } + + /// This harness fails because Kani cannot assume a pointer is valid. + /// + /// The specification should ensure the pointers passed are allocated, and this harness should + /// succeed since `copy` ensures would reject dangling pointers. + #[cfg(ignore)] + #[kani::proof_for_contract(copy)] + fn check_copy_dangling() { + ArbitraryPointers::::with_arbitrary(|arbitrary| { + // Verify the dangling case. + kani::assume(arbitrary.dst_kind == PtrKind::Dangling || arbitrary.src_kind == PtrKind::Dangling); + unsafe { copy(arbitrary.src, arbitrary.dst, kani::any()) } + }); + } + + /// 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| { + // Skip dangling for now since it makes Kani contract panic. + // Verify this case in a separate harness. + kani::assume(arbitrary.dst_kind != PtrKind::Dangling); + kani::assume(arbitrary.src_kind != PtrKind::Dangling); + unsafe { copy_nonoverlapping(arbitrary.src, arbitrary.dst, kani::any()) } + }); + } + + /// 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| { + // Skip dangling for now since it makes Kani contract panic. + // Verify this case in a separate harness. + kani::assume(arbitrary.dst_kind != PtrKind::Dangling); + unsafe { write_bytes(arbitrary.dst, kani::any(), kani::any()) } + }); + } } diff --git a/library/core/src/ub_checks.rs b/library/core/src/ub_checks.rs index b864b63c5c661..faf08abdc2424 100644 --- a/library/core/src/ub_checks.rs +++ b/library/core/src/ub_checks.rs @@ -163,6 +163,72 @@ pub(crate) const fn is_nonoverlapping( pub use predicates::*; +pub(crate) trait MetadataPredicates where T: ?Sized { + /// If the metadata is the length of a slice or str, run the map function. + fn map_len(metadata: *const Self, map: F) -> Option + where + F: Fn(*const usize) -> U; + + /// If the metadata is of type DynMetadata, run the map function and return its result. + fn map_dyn(metadata: *const Self, map: F) -> Option + where + F: Fn(*const crate::ptr::DynMetadata) -> U; +} + +impl MetadataPredicates for () { + /// Return None. + fn map_len(_metadata: *const Self, _map: F) -> Option + where + F: Fn(*const usize) -> U, + { + None + } + + /// Return None. + fn map_dyn(_metadata: *const Self, _map: F) -> Option + where + F: Fn(*const crate::ptr::DynMetadata) -> U, + { + None + } +} + +impl MetadataPredicates for usize where T: ?Sized{ + /// Return the result of the map function. + fn map_len(metadata: *const Self, map: F) -> Option + where + F: Fn(*const usize) -> U, + { + Some(map(metadata)) + } + + /// This is not a DynMetadata. Return `None`. + fn map_dyn(_metadata: *const Self, _map: F) -> Option + where + F: Fn(*const crate::ptr::DynMetadata) -> U + { + None + } +} + +impl MetadataPredicates for crate::ptr::DynMetadata where T: ?Sized { + /// Not a length. Return None. + fn map_len(_metadata: *const Self, _map: F) -> Option + where + F: Fn(*const usize) -> U, + { + None + } + + /// Return the result of the map function. + fn map_dyn(metadata: *const Self, map: F) -> Option + where + F: Fn(*const crate::ptr::DynMetadata) -> U, + { + Some(map(metadata)) + } +} + /// Provide a few predicates to be used in safety contracts. /// /// At runtime, they are no-op, and always return true.