Skip to content

Commit

Permalink
Merge branch 'main' into chores-merge-queue
Browse files Browse the repository at this point in the history
  • Loading branch information
@carolynzech
carolynzech authored Dec 9, 2024
2 parents c40ab3a + 8a0d0ce commit ae2265a
Show file tree
Hide file tree
Showing 7 changed files with 579 additions and 55 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
2 changes: 1 addition & 1 deletion doc/src/tools.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ The verification tool ecosystem for Rust is rapidly growing, and we welcome the
In this chapter, you can find a list of tools that have already been approved for new solutions,
what is their CI current status, as well as more details on how to use them.

If the tool you would like to add a new tool to the list of tool applications,
If you would like to add a new tool to the list of tool applications,
please see the [Tool Application](general-rules.md#tool-applications) section.

## Approved tools:
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
}
}
Loading

0 comments on commit ae2265a

Please sign in to comment.