Skip to content

Commit

Permalink
Add a few intrinsics contracts (#37)
Browse files Browse the repository at this point in the history 
Here are a few limitations:
 1. Harness for`write_bytes` was disabled due to:
     - Issue model-checking/kani#90.
 2. The harnesses explicitly disable cases where a pointer is dangling.
- Kani cannot make assumptions on pointer allocation for dead or
dangling pointers (model-checking/kani#2300).
3. Actual intrinsics are very hard to verify with Kani. The cases we can
verify are those that have wrappers around the actual intrinsic.
     - Issue model-checking/kani#3345

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Michael Tautschnig <[email protected]>
Co-authored-by: Michael Tautschnig <[email protected]>
  • Loading branch information
@celinval @tautschnig
3 people authored Dec 7, 2024
1 parent ee9b7c3 commit d92a7ea
Show file tree
Hide file tree
Showing 2 changed files with 157 additions and 38 deletions.
46 changes: 23 additions & 23 deletions doc/src/challenges/0002-intrinsics-memory.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
149 changes: 134 additions & 15 deletions library/core/src/intrinsics/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -3663,7 +3663,8 @@ pub const fn is_val_statically_known<T: Copy>(_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::<T>() == 0)]
#[requires((x.addr() >= y.addr() + core::mem::size_of::<T>()) || (y.addr() >= x.addr() + core::mem::size_of::<T>()))]
#[requires(ub_checks::maybe_is_nonoverlapping(x as *const (), y as *const (), size_of::<T>(), 1))]
#[ensures(|_| ub_checks::can_dereference(x) && ub_checks::can_dereference(y))]
pub const unsafe fn typed_swap<T>(x: *mut T, y: *mut T) {
// SAFETY: The caller provided single non-overlapping items behind
// pointers, so swapping them with `count: 1` is fine.
Expand Down Expand Up @@ -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):
// <https://github.com/rust-lang/unsafe-code-guidelines/issues/166>
#[requires(ub_checks::can_dereference(_ptr as *const [usize; 3]))]
pub unsafe fn vtable_size(_ptr: *const ()) -> usize {
unreachable!()
}
Expand All @@ -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):
// <https://github.com/rust-lang/unsafe-code-guidelines/issues/166>
#[requires(ub_checks::can_dereference(_ptr as *const [usize; 3]))]
pub unsafe fn vtable_align(_ptr: *const ()) -> usize {
unreachable!()
}
Expand Down Expand Up @@ -4034,6 +4041,13 @@ pub const fn ptr_metadata<P: ptr::Pointee<Metadata = M> + ?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::<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))
&& ub_checks::maybe_is_nonoverlapping(src as *const (), dst as *const (), size_of::<T>(), count))]
#[ensures(|_| { check_copy_untyped(src, dst, count)})]
pub const unsafe fn copy_nonoverlapping<T>(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)]
Expand Down Expand Up @@ -4141,6 +4155,11 @@ pub const unsafe fn copy_nonoverlapping<T>(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::<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(|_| { 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) {
#[cfg_attr(bootstrap, rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0"))]
#[cfg_attr(not(bootstrap), rustc_intrinsic_const_stable_indirect)]
Expand Down Expand Up @@ -4225,6 +4244,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"]
#[requires(!count.overflowing_mul(size_of::<T>()).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>(), T::IS_ZST || count == 0))]
#[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) {
#[cfg_attr(bootstrap, rustc_const_stable(feature = "const_ptr_write", since = "1.83.0"))]
#[cfg_attr(not(bootstrap), rustc_intrinsic_const_stable_indirect)]
Expand Down Expand Up @@ -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<T>(src: *const T, dst: *mut T, count: usize) -> bool {
#[cfg(kani)]
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
}
#[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)]
Expand All @@ -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::<u8>()
run_with_arbitrary_ptrs::<u8>(|x, y| unsafe { typed_swap(x, y) });
}

#[kani::proof_for_contract(typed_swap)]
pub fn check_typed_swap_char() {
check_swap::<char>()
run_with_arbitrary_ptrs::<char>(|x, y| unsafe { typed_swap(x, y) });
}

#[kani::proof_for_contract(typed_swap)]
pub fn check_typed_swap_non_zero() {
check_swap::<core::num::NonZeroI32>()
run_with_arbitrary_ptrs::<core::num::NonZeroI32>(|x, y| unsafe { typed_swap(x, y) });
}

pub fn check_swap<T: kani::Arbitrary + Copy + cmp::PartialEq + fmt::Debug>() {
let mut x = kani::any::<T>();
let old_x = x;
let mut y = kani::any::<T>();
let old_y = y;
#[kani::proof_for_contract(copy)]
fn check_copy() {
run_with_arbitrary_ptrs::<char>(|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<char>; 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::<char>::uninit(); 100];
for i in 0..100 {
if kani::any() {
buffer1[i] = MaybeUninit::new(kani::any());
}
}
let mut buffer2 = [MaybeUninit::<char>::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 <https://github.com/model-checking/kani/issues/90> 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::<char>();
kani::assume(supported_status(status));
unsafe { write_bytes(ptr, kani::any(), kani::any()) };
}

fn run_with_arbitrary_ptrs<T: Arbitrary>(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::<T>();
let ArbitraryPointer {
ptr: dst,
status: dst_status,
..
} = if kani::any() {
generator1.any_alloc_status::<T>()
} else {
generator2.any_alloc_status::<T>()
};
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
}
}

0 comments on commit d92a7ea

Please sign in to comment.