From aa1b9c25021973de2776ed1cf52ea113d503507b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 15 Jul 2024 20:34:06 -0700 Subject: [PATCH 1/7] 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 b81e8aa0edf7a..b7009684dbbc4 100644 --- a/library/core/src/intrinsics.rs +++ b/library/core/src/intrinsics.rs @@ -1063,7 +1063,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`]. @@ -2789,6 +2799,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!() } @@ -2799,6 +2812,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!() } @@ -2940,6 +2956,14 @@ 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"] +#[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")] @@ -3042,6 +3066,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")] @@ -3060,7 +3091,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) } @@ -3122,6 +3156,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")] @@ -3197,4 +3236,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. From 1ad91c8cc901fd82403e42c74338d778f67ab16d Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 16 Jul 2024 11:25:50 -0700 Subject: [PATCH 2/7] Fix copy* contract to make it untyped The intrinsics `copy` and `copy_nonoverlapping` are untyped copies, so they don't respect the validity requirements of `T`. --- library/core/src/intrinsics.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/library/core/src/intrinsics.rs b/library/core/src/intrinsics.rs index b7009684dbbc4..4b10823b5fea5 100644 --- a/library/core/src/intrinsics.rs +++ b/library/core/src/intrinsics.rs @@ -2727,7 +2727,7 @@ 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::is_nonoverlapping(x as *const (), x as *const (), size_of::(), 1))] 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. @@ -2956,11 +2956,11 @@ 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". #[requires(!count.overflowing_mul(size_of::()).1 - && ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src, count)) + && 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(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::()))] +#[requires(ub_checks::is_nonoverlapping(src as *const (), dst as *const (), size_of::(), 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)))] @@ -3068,8 +3068,8 @@ pub const unsafe fn copy_nonoverlapping(src: *const T, dst: *mut T, count: us #[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)))] + && 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)))] // 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)))] From 898f08f1b29cbe7d5b701b748f1059f167d9e186 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 17 Jul 2024 13:46:04 -0700 Subject: [PATCH 3/7] Fix Rust build and make MetadataPredicates public --- library/core/src/ub_checks.rs | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/library/core/src/ub_checks.rs b/library/core/src/ub_checks.rs index faf08abdc2424..ae24b32e28d21 100644 --- a/library/core/src/ub_checks.rs +++ b/library/core/src/ub_checks.rs @@ -163,7 +163,7 @@ pub(crate) const fn is_nonoverlapping( pub use predicates::*; -pub(crate) trait MetadataPredicates where T: ?Sized { +pub 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 @@ -193,7 +193,10 @@ impl MetadataPredicates for () { } } -impl MetadataPredicates for usize where T: ?Sized{ +impl MetadataPredicates for usize +where + T: ?Sized +{ /// Return the result of the map function. fn map_len(metadata: *const Self, map: F) -> Option where @@ -211,7 +214,10 @@ impl MetadataPredicates for usize where T: ?Sized{ } } -impl MetadataPredicates for crate::ptr::DynMetadata where T: ?Sized { +impl MetadataPredicates for crate::ptr::DynMetadata +where + T: ?Sized +{ /// Not a length. Return None. fn map_len(_metadata: *const Self, _map: F) -> Option where @@ -225,7 +231,7 @@ impl MetadataPredicates for crate::ptr::DynMetadata where T: ?Sized { where F: Fn(*const crate::ptr::DynMetadata) -> U, { - Some(map(metadata)) + Some(map(metadata)) } } From 79c65367fc7259bf251facc75416e1efcff87e90 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 22 Jul 2024 18:48:53 -0700 Subject: [PATCH 4/7] Add a few ensure clauses --- library/core/src/intrinsics.rs | 64 +++++++++++++++++++++++----------- 1 file changed, 44 insertions(+), 20 deletions(-) diff --git a/library/core/src/intrinsics.rs b/library/core/src/intrinsics.rs index 4b10823b5fea5..4589d99d9b491 100644 --- a/library/core/src/intrinsics.rs +++ b/library/core/src/intrinsics.rs @@ -63,7 +63,7 @@ )] #![allow(missing_docs)] -use safety::requires; +use safety::{ensures, requires}; use crate::marker::DiscriminantKind; use crate::marker::Tuple; use crate::ptr; @@ -2728,6 +2728,7 @@ pub const fn is_val_statically_known(_arg: T) -> bool { #[requires(ub_checks::can_dereference(y) && ub_checks::can_write(y))] #[requires(x.addr() != y.addr() || core::mem::size_of::() == 0)] #[requires(ub_checks::is_nonoverlapping(x as *const (), x 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. @@ -2957,13 +2958,23 @@ pub const fn ptr_metadata + ?Sized, M>(_ptr: *cons #[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)))] #[requires(ub_checks::is_nonoverlapping(src as *const (), dst as *const (), size_of::(), 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)))] +// 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) }) + } +})] 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")] @@ -3066,13 +3077,20 @@ 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?? +// FIXME(kani): 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 as *const crate::mem::MaybeUninit, 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)))] +#[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) }) + } +})] 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")] @@ -3156,11 +3174,14 @@ 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: 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)))] +// 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) +})] 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")] @@ -3208,6 +3229,7 @@ pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize #[unstable(feature="kani", issue="none")] mod verify { use core::{cmp, fmt}; + use core::ptr::addr_of_mut; use super::*; use crate::kani; @@ -3270,16 +3292,18 @@ mod verify { bytes: u64, } let mut single = kani::any::(); - let ptr1 = crate::ptr::addr_of_mut!(single); + let ptr1 = addr_of_mut!(single); - let mut array = [kani::any::(); 100]; - let ptr2 = crate::ptr::addr_of_mut!(array) as *mut u32; + // 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 buffer = [0u8, 6]; - let unaligned = unsafe { crate::ptr::addr_of_mut!(buffer).byte_offset(1) } as *mut u32; + let mut buffer = [0u8; 6]; + let unaligned = unsafe { 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 mut padding = WithPadding { byte: kani::any(), bytes: kani::any()}; + let uninit = unsafe { addr_of_mut!(padding.byte).byte_offset(4)} as *mut u32; let arbitrary = ArbitraryPointers::from(ptr1, ptr2, unaligned, uninit); harness(arbitrary); @@ -3348,7 +3372,7 @@ mod verify { }); } - /// This harness currently fails because we cannot define the modifies clause for slices. + /// 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| { @@ -3360,7 +3384,7 @@ mod verify { }); } - /// This harness currently fails because we cannot define the modifies clause for slices. + /// 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| { From 87dc8902499448d3137b00606fd69448ca7c779a Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 18 Sep 2024 15:17:05 -0700 Subject: [PATCH 5/7] Final adjustments for new harnesses --- doc/src/challenges/0002-intrinsics-memory.md | 45 ++--- library/core/src/intrinsics.rs | 168 ++++++++----------- 2 files changed, 91 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..eb4c345e8c352 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,22 @@ 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. +#[allow(dead_code)] +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 +3586,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 +3641,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 +3719,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 +3744,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 +3755,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| { From a38c1617ad1ab13066057704a76b159fae73d8e0 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 19 Sep 2024 18:28:48 -0700 Subject: [PATCH 6/7] Clean up arbitrary pointer --- library/core/src/intrinsics.rs | 201 +++++++++++++++------------------ 1 file changed, 89 insertions(+), 112 deletions(-) diff --git a/library/core/src/intrinsics.rs b/library/core/src/intrinsics.rs index eb4c345e8c352..cc49acaeb3295 100644 --- a/library/core/src/intrinsics.rs +++ b/library/core/src/intrinsics.rs @@ -3616,152 +3616,129 @@ mod verify { assert_eq!(x, old_y); } - /// Note that in `core` we cannot check allocated pointers. #[derive(Copy, Clone, Debug, PartialEq, Eq, kani::Arbitrary)] - enum PtrKind { + enum AllocationStatus { /// Dangling pointers Dangling, + /// Pointer to dead object + DeadObj, /// Null pointers Null, - /// Stack pointers - Stack, - /// Overlapping pointers - Overlap, - /// Unaligned pointers - Unaligned, - /// Pointer to uninitialized memory - Uninitialized, + /// In bounds pointer (it may be unaligned) + InBounds, + /// Out of bounds + OutBounds, } - struct ArbitraryPointers { - src: *const T, - dst: *mut T, - dst_kind: PtrKind, - src_kind: PtrKind, + struct PointerGenerator { + // Internal allocation that may be used to generate valid pointers. + buf: MaybeUninit<[T; BUF_LEN]>, } - impl 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) { + struct ArbitraryPointer { + pub ptr: *mut T, + pub status: AllocationStatus, + pub is_initialized: bool, + } - #[repr(C)] - struct WithUninit { - bytes: [MaybeUninit; SIZE], - } + impl PointerGenerator { + const SZ : usize = BUF_LEN * size_of::(); - #[repr(C)] - #[repr(packed)] - #[derive(kani::Arbitrary)] - struct Unaligned { - first: u8, - val: T, // If alignment of T > 1, this value will be unaligned but valid otherwise. + pub fn new() -> Self { + PointerGenerator { + buf: MaybeUninit::uninit() } + } - let mut single = kani::any::(); - let single_ptr = addr_of_mut!(single); - - let mut array: [T; 100] = kani::any(); - let array_ptr = addr_of_mut!(array) as *mut T; + /// Create another ArbitraryPointer that may have the same precedence as the `other` pointer. + /// + /// I.e.: Non-deterministically derive a pointer from the given pointer or create a new + /// arbitrary pointer. + pub fn generate_ptr(&mut self) -> ArbitraryPointer { + // Create an arbitrary pointer, but leave `ptr` as unset for now. + let mut arbitrary = ArbitraryPointer { + ptr: ptr::null_mut::(), + is_initialized: false, + status: kani::any(), + }; - let mut unaligned: Unaligned = kani::any(); - let unaligned_ptr = addr_of_mut!(unaligned.val) as *mut T; + let buf_ptr = addr_of_mut!(self.buf) 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(); + // Offset is used to potentially generate unaligned pointer. + let offset = kani::any_where(|b: &usize| *b < size_of::()); + let ptr = match arbitrary.status { + AllocationStatus::Dangling => { + crate::ptr::dangling_mut::().wrapping_add(offset) } - } - let uninit_ptr = &mut uninit as *mut _ as *mut T; - - let arbitrary = ArbitraryPointers::from(single_ptr, array_ptr, unaligned_ptr, uninit_ptr); - 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::() + AllocationStatus::DeadObj => { + let mut obj: T = kani::any(); + &mut obj as *mut _ } - PtrKind::Null => { + AllocationStatus::Null => { crate::ptr::null_mut::() } - PtrKind::Stack => { - unique + AllocationStatus::InBounds => { + let pos = kani::any_where(|i: &usize| *i < (BUF_LEN - 1)); + let ptr: *mut T = buf_ptr.wrapping_add(pos).wrapping_byte_add(offset); + if kani::any() { + arbitrary.is_initialized = true; + // This should be in bounds of arbitrary.alloc. + unsafe { ptr.write_unaligned(kani::any()) }; + } + ptr } - PtrKind::Overlap => { - if kani::any() { unique } else { overlap } - } - PtrKind::Unaligned => { - unaligned - } - PtrKind::Uninitialized => { - uninit + AllocationStatus::OutBounds => { + if kani::any() { + buf_ptr.wrapping_add(BUF_LEN).wrapping_byte_sub(offset) + } else { + buf_ptr.wrapping_add(BUF_LEN).wrapping_byte_add(offset) + } } }; - (kind, ptr) + + arbitrary } } - #[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()) } - }); + fn check_copy() { + let mut generator = PointerGenerator::::new(); + let src = generator.generate_ptr(); + let dst = if kani::any() { + generator.generate_ptr(); + } else { + PointerGenerator::::new().generate_ptr() + }; + // Skip dangling for now since it makes Kani contract panic. + kani::assume(src.status != AllocationStatus::Dangling); + kani::assume(dst.status != AllocationStatus::Dangling); + unsafe { copy(src.ptr, dst.ptr, kani::any()) } } #[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()) } - }); + let mut generator = PointerGenerator::::new(); + let src = generator.generate_ptr(); + // Destination may or may not have the same precedence as src. + let dst = if kani::any() { + generator.generate_ptr(); + } else { + PointerGenerator::::new().generate_ptr() + }; + // Skip dangling for now since it makes Kani contract panic. + kani::assume(src.status != AllocationStatus::Dangling); + kani::assume(dst.status != AllocationStatus::Dangling); + unsafe { copy_nonoverlapping(src.ptr, dst.ptr, kani::any()) } } #[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()) } - }); + let mut generator = PointerGenerator::::new(); + let src = generator.generate_ptr(); + kani::assume(src.status != AllocationStatus::Dangling); + // Skip dangling for now since it makes Kani contract panic. + // Verify this case in a separate harness. + unsafe { write_bytes(src.ptr, kani::any(), kani::any()) } } } From d41e5c10cf6a764ec13ff3aaf2f0ddcf04984ccf Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 19 Sep 2024 18:40:09 -0700 Subject: [PATCH 7/7] Update intrinsics.rs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Silly brain... 🤦‍♀️ --- library/core/src/intrinsics.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/intrinsics.rs b/library/core/src/intrinsics.rs index cc49acaeb3295..9722378f2d67c 100644 --- a/library/core/src/intrinsics.rs +++ b/library/core/src/intrinsics.rs @@ -3720,7 +3720,7 @@ mod verify { fn check_copy_nonoverlapping() { let mut generator = PointerGenerator::::new(); let src = generator.generate_ptr(); - // Destination may or may not have the same precedence as src. + // Destination may or may not have the same provenance as src. let dst = if kani::any() { generator.generate_ptr(); } else {