Skip to content

Commit

Permalink
Final adjustments for new harnesses
Browse files Browse the repository at this point in the history
  • Loading branch information
@celinval
celinval committed Sep 19, 2024
1 parent 0182ea1 commit 87dc890
Show file tree
Hide file tree
Showing 2 changed files with 91 additions and 122 deletions.
45 changes: 23 additions & 22 deletions doc/src/challenges/0002-intrinsics-memory.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
168 changes: 68 additions & 100 deletions library/core/src/intrinsics.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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!(
<T as Pointee>::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!(
<T as Pointee>::Metadata::map_len(crate::ptr::metadata(_val)::metadata(),
|_| { ub_checks::can_dereference(_val)}),
None | Some(true))))]
pub fn size_of_val<T: ?Sized>(_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<T: ?Sized>(_: *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<T: ?Sized>() -> &'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<T: ?Sized + 'static>() -> u128;

/// A guard for unsafe functions that cannot ever be executed if `T` is uninhabited:
/// This will statically either panic, or do nothing.
///
Expand Down Expand Up @@ -3166,6 +3116,14 @@ pub const fn variant_count<T>() -> usize {
#[rustc_const_unstable(feature = "const_size_of_val", issue = "46571")]
#[rustc_intrinsic]
#[rustc_intrinsic_must_be_overridden]
#[cfg_attr(not(kani), requires(matches!(
<T as Pointee>::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!(
<T as Pointee>::Metadata::map_len(crate::ptr::metadata(_val)::metadata(),
|_| { ub_checks::can_dereference(_val)}),
None | Some(true))))]
pub const unsafe fn size_of_val<T: ?Sized>(_ptr: *const T) -> usize {
unreachable!()
}
Expand Down Expand Up @@ -3363,20 +3321,10 @@ pub const fn ptr_metadata<P: ptr::Pointee<Metadata = M> + ?Sized, M>(_ptr: *cons
#[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))]
#[requires(!count.overflowing_mul(size_of::<T>()).1
&& ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src as *const crate::mem::MaybeUninit<T>, 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::<T>(), 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::<T>(), 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<T>(src: *const T, dst: *mut T, count: usize) {
extern "rust-intrinsic" {
#[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")]
Expand Down Expand Up @@ -3483,16 +3431,8 @@ pub const unsafe fn copy_nonoverlapping<T>(src: *const T, dst: *mut T, count: us
#[requires(!count.overflowing_mul(size_of::<T>()).1
&& ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src as *const crate::mem::MaybeUninit<T>, 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<T>(src: *const T, dst: *mut T, count: usize) {
extern "rust-intrinsic" {
#[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")]
Expand Down Expand Up @@ -3576,14 +3516,12 @@ pub const unsafe fn copy<T>(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::<T>()).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::<T>()))]
#[ensures(|_|
ub_checks::can_dereference(crate::ptr::slice_from_raw_parts(dst as *const u8, count * size_of::<T>())))]
#[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))]
pub const unsafe fn write_bytes<T>(dst: *mut T, val: u8, count: usize) {
extern "rust-intrinsic" {
#[rustc_const_unstable(feature = "const_ptr_write", issue = "86302")]
Expand All @@ -3605,6 +3543,22 @@ pub const unsafe fn write_bytes<T>(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<T>(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) {
Expand Down Expand Up @@ -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;

Expand Down Expand Up @@ -3686,28 +3641,44 @@ mod verify {
}

impl<T: kani::Arbitrary> ArbitraryPointers<T> {
fn with_arbitrary<F>(harness: F) where F: FnOnce(ArbitraryPointers<u32>) {
const MAX_SIZE_T: usize = 100;
const SIZE_T: usize = size_of::<T>();

const IS_VALID: () = assert!(Self::SIZE_T < Self::MAX_SIZE_T, "Exceeded supported type size");

fn with_arbitrary<F>(harness: F) where F: FnOnce(ArbitraryPointers<T>) {

#[repr(C)]
struct WithUninit<const SIZE: usize> {
bytes: [MaybeUninit<u8>; SIZE],
}

#[repr(C)]
struct WithPadding {
byte: u8,
// padding in the middle.
bytes: u64,
#[repr(packed)]
#[derive(kani::Arbitrary)]
struct Unaligned<T> {
first: u8,
val: T, // If alignment of T > 1, this value will be unaligned but valid otherwise.
}
let mut single = kani::any::<u32>();
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::<u32>(), 100];
let ptr2 = addr_of_mut!(array) as *mut u32;
let mut single = kani::any::<T>();
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<T> = 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);
}

Expand Down Expand Up @@ -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::<u32>::with_arbitrary(|arbitrary| {
Expand All @@ -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::<u32>::with_arbitrary(|arbitrary| {
Expand All @@ -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::<u32>::with_arbitrary(|arbitrary| {
Expand Down

0 comments on commit 87dc890

Please sign in to comment.