Skip to content

Commit b2eaef8

Browse files
celinvalcelinval
committed
Final adjustments for new harnesses
1 parent 0182ea1 commit b2eaef8

File tree

2 files changed

+90
-122
lines changed

2 files changed

+90
-122
lines changed

‎doc/src/challenges/0002-intrinsics-memory.md

+23-22
Original file line numberDiff line numberDiff line change
@@ -23,28 +23,29 @@ Annotate Rust core::intrinsics functions that manipulate raw pointers with their
2323

2424
Intrinsic functions to be annotated with safety contracts
2525

26-
| Function | Location |
27-
|---------|---------|
28-
|typed_swap | core::intrisics |
29-
|vtable_size| core::intrisics |
30-
|vtable_align| core::intrisics |
31-
|copy_nonoverlapping| core::intrisics |
32-
|copy| core::intrisics |
33-
|write_bytes| core::intrisics |
34-
|size_of_val| core::intrisics |
35-
|volatile_copy_nonoverlapping_memory| core::intrisics |
36-
|volatile_copy_memory| core::intrisics |
37-
|volatile_set_memory| core::intrisics |
38-
|volatile_load| core::intrisics |
39-
|volatile_store| core::intrisics |
40-
|unaligned_volatile_load| core::intrisics |
41-
|unaligned_volatile_store| core::intrisics |
42-
|compare_bytes| core::intrisics |
43-
|min_align_of_val| core::intrisics |
44-
|ptr_offset_from| core::intrisics |
45-
|ptr_offset_from_unsigned| core::intrisics |
46-
|read_via_copy| core::intrisics |
47-
|write_via_move| core::intrisics |
26+
| Function | Location |
27+
|-------------------------------------|---------|
28+
| typed_swap | core::intrisics |
29+
| vtable_size | core::intrisics |
30+
| vtable_align | core::intrisics |
31+
| copy_nonoverlapping | core::intrisics |
32+
| copy | core::intrisics |
33+
| write_bytes | core::intrisics |
34+
| size_of_val | core::intrisics |
35+
| arith_offset | core::intrisics |
36+
| volatile_copy_nonoverlapping_memory | core::intrisics |
37+
| volatile_copy_memory | core::intrisics |
38+
| volatile_set_memory | core::intrisics |
39+
| volatile_load | core::intrisics |
40+
| volatile_store | core::intrisics |
41+
| unaligned_volatile_load | core::intrisics |
42+
| unaligned_volatile_store | core::intrisics |
43+
| compare_bytes | core::intrisics |
44+
| min_align_of_val | core::intrisics |
45+
| ptr_offset_from | core::intrisics |
46+
| ptr_offset_from_unsigned | core::intrisics |
47+
| read_via_copy | core::intrisics |
48+
| write_via_move | core::intrisics |
4849

4950

5051
All the following usages of intrinsics were proven safe:

‎library/core/src/intrinsics.rs

+67-100
Original file line numberDiff line numberDiff line change
@@ -1042,56 +1042,6 @@ extern "rust-intrinsic" {
10421042
#[rustc_nounwind]
10431043
pub fn breakpoint();
10441044

1045-
/// Executes a breakpoint trap, for inspection by a debugger.
1046-
///
1047-
/// This intrinsic does not have a stable counterpart.
1048-
#[rustc_nounwind]
1049-
// FIXME: Kani currently does not support annotating intrinsics.
1050-
// See https://github.com/model-checking/kani/issues/3325
1051-
#[cfg_attr(not(kani), requires(matches!(
1052-
<T as Pointee>::Metadata::map_dyn(crate::ptr::metadata(_val)::metadata(),
1053-
|dyn_meta| { ub_checks::can_dereference(dyn_meta)}),
1054-
None | Some(true))))]
1055-
#[cfg_attr(not(kani), requires(matches!(
1056-
<T as Pointee>::Metadata::map_len(crate::ptr::metadata(_val)::metadata(),
1057-
|_| { ub_checks::can_dereference(_val)}),
1058-
None | Some(true))))]
1059-
pub fn size_of_val<T: ?Sized>(_val: *const T) -> usize;
1060-
/// The required alignment of the referenced value.
1061-
///
1062-
/// The stabilized version of this intrinsic is [`core::mem::align_of_val`].
1063-
#[rustc_const_unstable(feature = "const_align_of_val", issue = "46571")]
1064-
#[rustc_nounwind]
1065-
pub fn min_align_of_val<T: ?Sized>(_: *const T) -> usize;
1066-
1067-
/// Gets a static string slice containing the name of a type.
1068-
///
1069-
/// Note that, unlike most intrinsics, this is safe to call;
1070-
/// it does not require an `unsafe` block.
1071-
/// Therefore, implementations must not require the user to uphold
1072-
/// any safety invariants.
1073-
///
1074-
/// The stabilized version of this intrinsic is [`core::any::type_name`].
1075-
#[rustc_const_unstable(feature = "const_type_name", issue = "63084")]
1076-
#[rustc_safe_intrinsic]
1077-
#[rustc_nounwind]
1078-
pub fn type_name<T: ?Sized>() -> &'static str;
1079-
1080-
/// Gets an identifier which is globally unique to the specified type. This
1081-
/// function will return the same value for a type regardless of whichever
1082-
/// crate it is invoked in.
1083-
///
1084-
/// Note that, unlike most intrinsics, this is safe to call;
1085-
/// it does not require an `unsafe` block.
1086-
/// Therefore, implementations must not require the user to uphold
1087-
/// any safety invariants.
1088-
///
1089-
/// The stabilized version of this intrinsic is [`core::any::TypeId::of`].
1090-
#[rustc_const_unstable(feature = "const_type_id", issue = "77125")]
1091-
#[rustc_safe_intrinsic]
1092-
#[rustc_nounwind]
1093-
pub fn type_id<T: ?Sized + 'static>() -> u128;
1094-
10951045
/// A guard for unsafe functions that cannot ever be executed if `T` is uninhabited:
10961046
/// This will statically either panic, or do nothing.
10971047
///
@@ -3166,6 +3116,14 @@ pub const fn variant_count<T>() -> usize {
31663116
#[rustc_const_unstable(feature = "const_size_of_val", issue = "46571")]
31673117
#[rustc_intrinsic]
31683118
#[rustc_intrinsic_must_be_overridden]
3119+
#[cfg_attr(not(kani), requires(matches!(
3120+
<T as Pointee>::Metadata::map_dyn(crate::ptr::metadata(_val)::metadata(),
3121+
|dyn_meta| { ub_checks::can_dereference(dyn_meta)}),
3122+
None | Some(true))))]
3123+
#[cfg_attr(not(kani), requires(matches!(
3124+
<T as Pointee>::Metadata::map_len(crate::ptr::metadata(_val)::metadata(),
3125+
|_| { ub_checks::can_dereference(_val)}),
3126+
None | Some(true))))]
31693127
pub const unsafe fn size_of_val<T: ?Sized>(_ptr: *const T) -> usize {
31703128
unreachable!()
31713129
}
@@ -3363,20 +3321,10 @@ pub const fn ptr_metadata<P: ptr::Pointee<Metadata = M> + ?Sized, M>(_ptr: *cons
33633321
#[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))]
33643322
#[requires(!count.overflowing_mul(size_of::<T>()).1
33653323
&& ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src as *const crate::mem::MaybeUninit<T>, count))
3366-
&& ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)))]
3367-
#[requires(ub_checks::is_nonoverlapping(src as *const (), dst as *const (), size_of::<T>(), count))]
3368-
// TODO: Use quantifiers once it's available.
3369-
// Ensures the initialization state is preserved.
3370-
#[ensures(|_| {
3371-
if count > 0 {
3372-
let byte = kani::any_where(| sz: &usize | *sz < size_of::< T >);
3373-
let elem = kani::any_where(| val: &usize | *val < count);
3374-
let src_data = src as * const u8;
3375-
let dst_data = unsafe { dst.offset(elem) } as * const u8;
3376-
ub_checks::can_dereference(unsafe { src_data.offset(byte) })
3377-
== ub_checks::can_dereference(unsafe { dst_data.offset(byte) })
3378-
}
3379-
})]
3324+
&& ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count))
3325+
&& ub_checks::is_nonoverlapping(src as *const (), dst as *const (), size_of::<T>(), count))]
3326+
#[ensures(|_| { check_copy_untyped(src, dst, count)}) ]
3327+
#[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))]
33803328
pub const unsafe fn copy_nonoverlapping<T>(src: *const T, dst: *mut T, count: usize) {
33813329
extern "rust-intrinsic" {
33823330
#[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")]
@@ -3483,16 +3431,8 @@ pub const unsafe fn copy_nonoverlapping<T>(src: *const T, dst: *mut T, count: us
34833431
#[requires(!count.overflowing_mul(size_of::<T>()).1
34843432
&& ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src as *const crate::mem::MaybeUninit<T>, count))
34853433
&& ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)))]
3486-
#[ensures(|_| {
3487-
if count > 0 {
3488-
let byte = kani::any_where(| sz: &usize | *sz < size_of::< T >);
3489-
let elem = kani::any_where(| val: &usize | *val < count);
3490-
let src_data = src as * const u8;
3491-
let dst_data = unsafe { dst.offset(elem) } as * const u8;
3492-
ub_checks::can_dereference(unsafe { src_data.offset(byte) })
3493-
== ub_checks::can_dereference(unsafe { dst_data.offset(byte) })
3494-
}
3495-
})]
3434+
#[ensures(|_| { check_copy_untyped(src, dst, count) })]
3435+
#[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))]
34963436
pub const unsafe fn copy<T>(src: *const T, dst: *mut T, count: usize) {
34973437
extern "rust-intrinsic" {
34983438
#[rustc_const_unstable(feature = "const_intrinsic_copy", issue = "80697")]
@@ -3576,14 +3516,12 @@ pub const unsafe fn copy<T>(src: *const T, dst: *mut T, count: usize) {
35763516
#[inline(always)]
35773517
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
35783518
#[rustc_diagnostic_item = "ptr_write_bytes"]
3579-
#[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))]
35803519
#[requires(!count.overflowing_mul(size_of::<T>()).1
3581-
&& ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst as *mut u8, count)))]
3582-
// TODO: Change this to quantifiers when available.
3583-
#[ensures(|_| {
3584-
let idx = kani::any_where(|idx: &usize| *idx < count);
3585-
ub_checks::can_dereference(dst.offset(idx) as * const u8)
3586-
})]
3520+
&& ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)))]
3521+
#[requires(count > 0 || ub_checks::is_aligned_and_not_null(dst as *const (), align_of::<T>()))]
3522+
#[ensures(|_|
3523+
ub_checks::can_dereference(crate::ptr::slice_from_raw_parts(dst as *const u8, count * size_of::<T>())))]
3524+
#[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))]
35873525
pub const unsafe fn write_bytes<T>(dst: *mut T, val: u8, count: usize) {
35883526
extern "rust-intrinsic" {
35893527
#[rustc_const_unstable(feature = "const_ptr_write", issue = "86302")]
@@ -3605,6 +3543,21 @@ pub const unsafe fn write_bytes<T>(dst: *mut T, val: u8, count: usize) {
36053543
}
36063544
}
36073545

3546+
// Ensures the initialization state is preserved.
3547+
// This is used for contracts only.
3548+
fn check_copy_untyped<T>(src: *const T, dst: *mut T, count: usize) -> bool {
3549+
if count > 0 {
3550+
let byte = kani::any_where(| sz: &usize | *sz < size_of::< T >());
3551+
let elem = kani::any_where(| val: &usize | *val < count);
3552+
let src_data = src as * const u8;
3553+
let dst_data = unsafe { dst.add(elem) } as * const u8;
3554+
ub_checks::can_dereference(unsafe { src_data.add(byte) })
3555+
== ub_checks::can_dereference(unsafe { dst_data.add(byte) })
3556+
} else {
3557+
true
3558+
}
3559+
}
3560+
36083561
/// Inform Miri that a given pointer definitely has a certain alignment.
36093562
#[cfg(miri)]
36103563
pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize) {
@@ -3632,6 +3585,7 @@ pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize
36323585
mod verify {
36333586
use core::{cmp, fmt};
36343587
use core::ptr::addr_of_mut;
3588+
use core::mem::MaybeUninit;
36353589
use super::*;
36363590
use crate::kani;
36373591

@@ -3686,28 +3640,44 @@ mod verify {
36863640
}
36873641

36883642
impl<T: kani::Arbitrary> ArbitraryPointers<T> {
3689-
fn with_arbitrary<F>(harness: F) where F: FnOnce(ArbitraryPointers<u32>) {
3643+
const MAX_SIZE_T: usize = 100;
3644+
const SIZE_T: usize = size_of::<T>();
3645+
3646+
const IS_VALID: () = assert!(Self::SIZE_T < Self::MAX_SIZE_T, "Exceeded supported type size");
3647+
3648+
fn with_arbitrary<F>(harness: F) where F: FnOnce(ArbitraryPointers<T>) {
3649+
3650+
#[repr(C)]
3651+
struct WithUninit<const SIZE: usize> {
3652+
bytes: [MaybeUninit<u8>; SIZE],
3653+
}
3654+
36903655
#[repr(C)]
3691-
struct WithPadding {
3692-
byte: u8,
3693-
// padding in the middle.
3694-
bytes: u64,
3656+
#[repr(packed)]
3657+
#[derive(kani::Arbitrary)]
3658+
struct Unaligned<T> {
3659+
first: u8,
3660+
val: T, // If alignment of T > 1, this value will be unaligned but valid otherwise.
36953661
}
3696-
let mut single = kani::any::<u32>();
3697-
let ptr1 = addr_of_mut!(single);
36983662

3699-
// FIXME(kani) this should be but this is not available in `kani_core` yet:
3700-
// let mut array: [u8; 100] = kani::any();
3701-
let mut array = [kani::any::<u32>(), 100];
3702-
let ptr2 = addr_of_mut!(array) as *mut u32;
3663+
let mut single = kani::any::<T>();
3664+
let single_ptr = addr_of_mut!(single);
37033665

3704-
let mut buffer = [0u8; 6];
3705-
let unaligned = unsafe { addr_of_mut!(buffer).byte_offset(1) } as *mut u32;
3666+
let mut array: [T; 100] = kani::any();
3667+
let array_ptr = addr_of_mut!(array) as *mut T;
37063668

3707-
let mut padding = WithPadding { byte: kani::any(), bytes: kani::any()};
3708-
let uninit = unsafe { addr_of_mut!(padding.byte).byte_offset(4)} as *mut u32;
3669+
let mut unaligned: Unaligned<T> = kani::any();
3670+
let unaligned_ptr = addr_of_mut!(unaligned.val) as *mut T;
3671+
3672+
let mut uninit = WithUninit { bytes: [MaybeUninit::zeroed(); Self::MAX_SIZE_T] };
3673+
for i in 0..Self::SIZE_T {
3674+
if kani::any() {
3675+
uninit.bytes[i] = MaybeUninit::uninit();
3676+
}
3677+
}
3678+
let uninit_ptr = &mut uninit as *mut _ as *mut T;
37093679

3710-
let arbitrary = ArbitraryPointers::from(ptr1, ptr2, unaligned, uninit);
3680+
let arbitrary = ArbitraryPointers::from(single_ptr, array_ptr, unaligned_ptr, uninit_ptr);
37113681
harness(arbitrary);
37123682
}
37133683

@@ -3748,7 +3718,6 @@ mod verify {
37483718
}
37493719
}
37503720

3751-
/// This harness currently fails because we cannot define the modifies clause for slices.
37523721
#[kani::proof_for_contract(copy)]
37533722
fn check_copy() {
37543723
ArbitraryPointers::<u32>::with_arbitrary(|arbitrary| {
@@ -3774,7 +3743,6 @@ mod verify {
37743743
});
37753744
}
37763745

3777-
/// FIXME(kani): This harness currently fails because we cannot define the modifies clause for slices.
37783746
#[kani::proof_for_contract(copy_nonoverlapping)]
37793747
fn check_copy_nonoverlapping() {
37803748
ArbitraryPointers::<u32>::with_arbitrary(|arbitrary| {
@@ -3786,7 +3754,6 @@ mod verify {
37863754
});
37873755
}
37883756

3789-
/// FIXME(kani): This harness currently fails because we cannot define the modifies clause for slices.
37903757
#[kani::proof_for_contract(write_bytes)]
37913758
fn check_write_bytes() {
37923759
ArbitraryPointers::<u32>::with_arbitrary(|arbitrary| {

0 commit comments

Comments
 (0)