From d92a7ea57f9096171354b47b45bd4f6e31baba2a Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 6 Dec 2024 17:44:00 -0800 Subject: [PATCH 1/4] Add a few intrinsics contracts (#37) Here are a few limitations: 1. Harness for`write_bytes` was disabled due to: - Issue https://github.com/model-checking/kani/issues/90. 2. The harnesses explicitly disable cases where a pointer is dangling. - Kani cannot make assumptions on pointer allocation for dead or dangling pointers (https://github.com/model-checking/kani/issues/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 https://github.com/model-checking/kani/issues/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 Co-authored-by: Michael Tautschnig --- doc/src/challenges/0002-intrinsics-memory.md | 46 +++--- library/core/src/intrinsics/mod.rs | 149 +++++++++++++++++-- 2 files changed, 157 insertions(+), 38 deletions(-) diff --git a/doc/src/challenges/0002-intrinsics-memory.md b/doc/src/challenges/0002-intrinsics-memory.md index 31c1c43225250..adb4176254804 100644 --- a/doc/src/challenges/0002-intrinsics-memory.md +++ b/doc/src/challenges/0002-intrinsics-memory.md @@ -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: diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index 38dbe91bea64a..29ef19daaf679 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -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; @@ -3663,7 +3663,8 @@ 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::maybe_is_nonoverlapping(x as *const (), y 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. @@ -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): +// +#[requires(ub_checks::can_dereference(_ptr as *const [usize; 3]))] pub unsafe fn vtable_size(_ptr: *const ()) -> usize { unreachable!() } @@ -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): +// +#[requires(ub_checks::can_dereference(_ptr as *const [usize; 3]))] pub unsafe fn vtable_align(_ptr: *const ()) -> usize { unreachable!() } @@ -4034,6 +4041,13 @@ 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". +#[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)) + && ub_checks::maybe_is_nonoverlapping(src as *const (), dst as *const (), size_of::(), count))] +#[ensures(|_| { check_copy_untyped(src, dst, count)})] pub const unsafe fn copy_nonoverlapping(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)] @@ -4141,6 +4155,11 @@ 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"] +#[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(|_| { 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) { #[cfg_attr(bootstrap, rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0"))] #[cfg_attr(not(bootstrap), rustc_intrinsic_const_stable_indirect)] @@ -4225,6 +4244,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"] +#[requires(!count.overflowing_mul(size_of::()).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::IS_ZST || count == 0))] +#[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) { #[cfg_attr(bootstrap, rustc_const_stable(feature = "const_ptr_write", since = "1.83.0"))] #[cfg_attr(not(bootstrap), rustc_intrinsic_const_stable_indirect)] @@ -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(src: *const T, dst: *mut T, count: usize) -> bool { + #[cfg(kani)] + if count > 0 { + let byte = kani::any_where(|sz: &usize| *sz < size_of::()); + 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)] @@ -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::() + run_with_arbitrary_ptrs::(|x, y| unsafe { typed_swap(x, y) }); } #[kani::proof_for_contract(typed_swap)] pub fn check_typed_swap_char() { - check_swap::() + run_with_arbitrary_ptrs::(|x, y| unsafe { typed_swap(x, y) }); } #[kani::proof_for_contract(typed_swap)] pub fn check_typed_swap_non_zero() { - check_swap::() + run_with_arbitrary_ptrs::(|x, y| unsafe { typed_swap(x, y) }); } - pub fn check_swap() { - let mut x = kani::any::(); - let old_x = x; - let mut y = kani::any::(); - let old_y = y; + #[kani::proof_for_contract(copy)] + fn check_copy() { + run_with_arbitrary_ptrs::(|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; 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::::uninit(); 100]; + for i in 0..100 { + if kani::any() { + buffer1[i] = MaybeUninit::new(kani::any()); + } + } + let mut buffer2 = [MaybeUninit::::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 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::(); + kani::assume(supported_status(status)); + unsafe { write_bytes(ptr, kani::any(), kani::any()) }; + } + + fn run_with_arbitrary_ptrs(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::(); + let ArbitraryPointer { + ptr: dst, + status: dst_status, + .. + } = if kani::any() { + generator1.any_alloc_status::() + } else { + generator2.any_alloc_status::() + }; + 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 } } From 8a0d0ce22d8094799ca302248956b18b36fdc564 Mon Sep 17 00:00:00 2001 From: stogaru <143449212+stogaru@users.noreply.github.com> Date: Sat, 7 Dec 2024 16:51:44 -0800 Subject: [PATCH 2/4] Contracts and Harnesses for `core::ptr::byte_offset_from` (#186) --- library/core/src/ptr/const_ptr.rs | 205 +++++++++++++++++++++++++++++- library/core/src/ptr/mut_ptr.rs | 205 +++++++++++++++++++++++++++++- 2 files changed, 407 insertions(+), 3 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index a210821f08d10..32baf1b33941a 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -730,6 +730,16 @@ impl *const T { #[stable(feature = "pointer_byte_offsets", since = "1.75.0")] #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires( + (mem::size_of_val_raw(self) != 0) && + // Ensures subtracting `origin` from `self` doesn't overflow + (self.addr() as isize).checked_sub(origin.addr() as isize).is_some() && + // Ensure both pointers are in the same allocation or are pointing to the same address + (self.addr() == origin.addr() || + core::ub_checks::same_allocation(self as *const u8, origin as *const u8)) + )] + // The result should equal the distance in terms of bytes + #[ensures(|result| *result == (self.addr() as isize - origin.addr() as isize))] pub const unsafe fn byte_offset_from(self, origin: *const U) -> isize { // SAFETY: the caller must uphold the safety contract for `offset_from`. unsafe { self.cast::().offset_from(origin.cast::()) } @@ -1940,7 +1950,7 @@ mod verify { check_const_offset_usize ); - // Generte harnesses for composite types (add, sub, offset) + // Generate harnesses for composite types (add, sub, offset) generate_arithmetic_harnesses!( (i8, i8), check_const_add_tuple_1, @@ -2116,6 +2126,17 @@ mod verify { // PointerGenerator does not support dynamic sized arrays. const ARRAY_LEN: usize = 40; + #[kani::proof] + pub fn check_const_byte_offset_from_fixed_offset() { + let arr: [u32; ARRAY_LEN] = kani::Arbitrary::any_array(); + let offset: usize = kani::any_where(|&x| x <= ARRAY_LEN); + let origin_ptr: *const u32 = arr.as_ptr(); + let self_ptr: *const u32 = unsafe { origin_ptr.byte_offset(offset as isize) }; + let result: isize = unsafe { self_ptr.byte_offset_from(origin_ptr) }; + assert_eq!(result, offset as isize); + assert_eq!(result, (self_ptr.addr() as isize - origin_ptr.addr() as isize)); + } + macro_rules! generate_offset_from_harness { ($type: ty, $proof_name1: ident, $proof_name2: ident) => { // Proof for a single element @@ -2156,7 +2177,7 @@ mod verify { }; } - // Proof for unit size will panic as offset_from needs the pointee size to be greater then 0 + // Proof for unit size will panic as offset_from needs the pointee size to be greater than 0 #[kani::proof_for_contract(<*const ()>::offset_from)] #[kani::should_panic] pub fn check_const_offset_from_unit() { @@ -2252,6 +2273,186 @@ mod verify { check_const_offset_from_tuple_4_arr ); + // Proof for contact of byte_offset_from to verify unit type + #[kani::proof_for_contract(<*const ()>::byte_offset_from)] + pub fn check_const_byte_offset_from_unit() { + let val: () = (); + let src_ptr: *const () = &val; + let dest_ptr: *const () = &val; + unsafe { + dest_ptr.byte_offset_from(src_ptr); + } + } + + // generate proofs for contracts for byte_offset_from to verify int and composite + // types + // - `$type`: pointee type + // - `$proof_name1`: name of the harness for single element + // - `$proof_name2`: name of the harness for array of elements + macro_rules! generate_const_byte_offset_from_harness { + ($type: ty, $proof_name1: ident, $proof_name2: ident) => { + // Proof for a single element + #[kani::proof_for_contract(<*const $type>::byte_offset_from)] + pub fn $proof_name1() { + const gen_size: usize = mem::size_of::<$type>(); + let mut generator1 = PointerGenerator::::new(); + let mut generator2 = PointerGenerator::::new(); + let ptr1: *const $type = generator1.any_in_bounds().ptr; + let ptr2: *const $type = if kani::any() { + generator1.any_alloc_status().ptr + } else { + generator2.any_alloc_status().ptr + }; + + unsafe { + ptr1.byte_offset_from(ptr2); + } + } + + // Proof for large arrays + #[kani::proof_for_contract(<*const $type>::byte_offset_from)] + pub fn $proof_name2() { + const gen_size: usize = mem::size_of::<$type>(); + let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let ptr1: *const $type = generator1.any_in_bounds().ptr; + let ptr2: *const $type = if kani::any() { + generator1.any_alloc_status().ptr + } else { + generator2.any_alloc_status().ptr + }; + + unsafe { + ptr1.byte_offset_from(ptr2); + } + } + }; + } + + generate_const_byte_offset_from_harness!( + u8, + check_const_byte_offset_from_u8, + check_const_byte_offset_from_u8_arr + ); + generate_const_byte_offset_from_harness!( + u16, + check_const_byte_offset_from_u16, + check_const_byte_offset_from_u16_arr + ); + generate_const_byte_offset_from_harness!( + u32, + check_const_byte_offset_from_u32, + check_const_byte_offset_from_u32_arr + ); + generate_const_byte_offset_from_harness!( + u64, + check_const_byte_offset_from_u64, + check_const_byte_offset_from_u64_arr + ); + generate_const_byte_offset_from_harness!( + u128, + check_const_byte_offset_from_u128, + check_const_byte_offset_from_u128_arr + ); + generate_const_byte_offset_from_harness!( + usize, + check_const_byte_offset_from_usize, + check_const_byte_offset_from_usize_arr + ); + + generate_const_byte_offset_from_harness!( + i8, + check_const_byte_offset_from_i8, + check_const_byte_offset_from_i8_arr + ); + generate_const_byte_offset_from_harness!( + i16, + check_const_byte_offset_from_i16, + check_const_byte_offset_from_i16_arr + ); + generate_const_byte_offset_from_harness!( + i32, + check_const_byte_offset_from_i32, + check_const_byte_offset_from_i32_arr + ); + generate_const_byte_offset_from_harness!( + i64, + check_const_byte_offset_from_i64, + check_const_byte_offset_from_i64_arr + ); + generate_const_byte_offset_from_harness!( + i128, + check_const_byte_offset_from_i128, + check_const_byte_offset_from_i128_arr + ); + generate_const_byte_offset_from_harness!( + isize, + check_const_byte_offset_from_isize, + check_const_byte_offset_from_isize_arr + ); + + generate_const_byte_offset_from_harness!( + (i8, i8), + check_const_byte_offset_from_tuple_1, + check_const_byte_offset_from_tuple_1_arr + ); + generate_const_byte_offset_from_harness!( + (f64, bool), + check_const_byte_offset_from_tuple_2, + check_const_byte_offset_from_tuple_2_arr + ); + generate_const_byte_offset_from_harness!( + (u32, i16, f32), + check_const_byte_offset_from_tuple_3, + check_const_byte_offset_from_tuple_3_arr + ); + generate_const_byte_offset_from_harness!( + ((), bool, u8, u16, i32, f64, i128, usize), + check_const_byte_offset_from_tuple_4, + check_const_byte_offset_from_tuple_4_arr + ); + + // length of the slice generated from PointerGenerator + const SLICE_LEN: usize = 10; + + // generate proofs for contracts for byte_offset_from to verify slices + // - `$type`: type of the underlyign element within the slice pointer + // - `$proof_name`: name of the harness + macro_rules! generate_const_byte_offset_from_slice_harness { + ($type: ty, $proof_name: ident) => { + #[kani::proof_for_contract(<*const [$type]>::byte_offset_from)] + pub fn $proof_name() { + const gen_size: usize = mem::size_of::<$type>(); + let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let ptr1: *const [$type] = + generator1.any_in_bounds().ptr as *const [$type; SLICE_LEN]; + let ptr2: *const [$type] = if kani::any() { + generator1.any_alloc_status().ptr as *const [$type; SLICE_LEN] + } else { + generator2.any_alloc_status().ptr as *const [$type; SLICE_LEN] + }; + + unsafe { + ptr1.byte_offset_from(ptr2); + } + } + }; + } + + generate_const_byte_offset_from_slice_harness!(u8, check_const_byte_offset_from_u8_slice); + generate_const_byte_offset_from_slice_harness!(u16, check_const_byte_offset_from_u16_slice); + generate_const_byte_offset_from_slice_harness!(u32, check_const_byte_offset_from_u32_slice); + generate_const_byte_offset_from_slice_harness!(u64, check_const_byte_offset_from_u64_slice); + generate_const_byte_offset_from_slice_harness!(u128, check_const_byte_offset_from_u128_slice); + generate_const_byte_offset_from_slice_harness!(usize, check_const_byte_offset_from_usize_slice); + generate_const_byte_offset_from_slice_harness!(i8, check_const_byte_offset_from_i8_slice); + generate_const_byte_offset_from_slice_harness!(i16, check_const_byte_offset_from_i16_slice); + generate_const_byte_offset_from_slice_harness!(i32, check_const_byte_offset_from_i32_slice); + generate_const_byte_offset_from_slice_harness!(i64, check_const_byte_offset_from_i64_slice); + generate_const_byte_offset_from_slice_harness!(i128, check_const_byte_offset_from_i128_slice); + generate_const_byte_offset_from_slice_harness!(isize, check_const_byte_offset_from_isize_slice); + #[kani::proof_for_contract(<*const ()>::byte_offset)] #[kani::should_panic] pub fn check_const_byte_offset_unit_invalid_count() { diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index fd7e4d80e676d..ef291233ae336 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -894,6 +894,16 @@ impl *mut T { #[stable(feature = "pointer_byte_offsets", since = "1.75.0")] #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires( + (mem::size_of_val_raw(self) != 0) && + // Ensures subtracting `origin` from `self` doesn't overflow + (self.addr() as isize).checked_sub(origin.addr() as isize).is_some() && + // Ensure both pointers are in the same allocation or are pointing to the same address + (self.addr() == origin.addr() || + core::ub_checks::same_allocation(self as *const u8, origin as *const u8)) + )] + // The result should equal the distance in terms of bytes + #[ensures(|result| *result == (self.addr() as isize - origin.addr() as isize))] pub const unsafe fn byte_offset_from(self, origin: *const U) -> isize { // SAFETY: the caller must uphold the safety contract for `offset_from`. unsafe { self.cast::().offset_from(origin.cast::()) } @@ -2236,9 +2246,202 @@ mod verify { // The array's length is set to an arbitrary value, which defines its size. // In this case, implementing a dynamic array is not possible, because - // PointerGenerator does not support dynamic sized arrays. + // PointerGenerator or any_array() do not support dynamic sized arrays. const ARRAY_LEN: usize = 40; + #[kani::proof] + pub fn check_mut_byte_offset_from_fixed_offset() { + let mut arr: [u32; ARRAY_LEN] = kani::Arbitrary::any_array(); + let offset: usize = kani::any_where(|&x| x <= ARRAY_LEN); + let origin_ptr: *mut u32 = arr.as_mut_ptr(); + let self_ptr: *mut u32 = unsafe { origin_ptr.byte_offset(offset as isize) }; + let result: isize = unsafe { self_ptr.byte_offset_from(origin_ptr) }; + assert_eq!(result, offset as isize); + assert_eq!(result, (self_ptr.addr() as isize - origin_ptr.addr() as isize)); + } + + // Proof for unit size + #[kani::proof_for_contract(<*mut ()>::byte_offset_from)] + pub fn check_mut_byte_offset_from_unit() { + let mut val: () = (); + let src_ptr: *mut () = &mut val; + let dest_ptr: *mut () = &mut val; + unsafe { + dest_ptr.byte_offset_from(src_ptr); + } + } + + // generate proofs for contracts for byte_offset_from to verify int and composite + // types + // - `$type`: pointee type + // - `$proof_name1`: name of the harness for single element + // - `$proof_name2`: name of the harness for array of elements + macro_rules! generate_mut_byte_offset_from_harness { + ($type: ty, $proof_name1: ident, $proof_name2: ident) => { + // Proof for a single element + #[kani::proof_for_contract(<*mut $type>::byte_offset_from)] + pub fn $proof_name1() { + const gen_size: usize = mem::size_of::<$type>(); + let mut generator1 = PointerGenerator::::new(); + let mut generator2 = PointerGenerator::::new(); + let ptr1: *mut $type = generator1.any_in_bounds().ptr; + let ptr2: *mut $type = if kani::any() { + generator1.any_alloc_status().ptr + } else { + generator2.any_alloc_status().ptr + }; + + unsafe { + ptr1.byte_offset_from(ptr2); + } + } + + // Proof for large arrays + #[kani::proof_for_contract(<*mut $type>::byte_offset_from)] + pub fn $proof_name2() { + const gen_size: usize = mem::size_of::<$type>(); + let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let ptr1: *mut $type = generator1.any_in_bounds().ptr; + let ptr2: *mut $type = if kani::any() { + generator1.any_alloc_status().ptr + } else { + generator2.any_alloc_status().ptr + }; + + unsafe { + ptr1.byte_offset_from(ptr2); + } + } + }; + } + + generate_mut_byte_offset_from_harness!( + u8, + check_mut_byte_offset_from_u8, + check_mut_byte_offset_from_u8_arr + ); + generate_mut_byte_offset_from_harness!( + u16, + check_mut_byte_offset_from_u16, + check_mut_byte_offset_from_u16_arr + ); + generate_mut_byte_offset_from_harness!( + u32, + check_mut_byte_offset_from_u32, + check_mut_byte_offset_from_u32_arr + ); + generate_mut_byte_offset_from_harness!( + u64, + check_mut_byte_offset_from_u64, + check_mut_byte_offset_from_u64_arr + ); + generate_mut_byte_offset_from_harness!( + u128, + check_mut_byte_offset_from_u128, + check_mut_byte_offset_from_u128_arr + ); + generate_mut_byte_offset_from_harness!( + usize, + check_mut_byte_offset_from_usize, + check_mut_byte_offset_from_usize_arr + ); + + generate_mut_byte_offset_from_harness!( + i8, + check_mut_byte_offset_from_i8, + check_mut_byte_offset_from_i8_arr + ); + generate_mut_byte_offset_from_harness!( + i16, + check_mut_byte_offset_from_i16, + check_mut_byte_offset_from_i16_arr + ); + generate_mut_byte_offset_from_harness!( + i32, + check_mut_byte_offset_from_i32, + check_mut_byte_offset_from_i32_arr + ); + generate_mut_byte_offset_from_harness!( + i64, + check_mut_byte_offset_from_i64, + check_mut_byte_offset_from_i64_arr + ); + generate_mut_byte_offset_from_harness!( + i128, + check_mut_byte_offset_from_i128, + check_mut_byte_offset_from_i128_arr + ); + generate_mut_byte_offset_from_harness!( + isize, + check_mut_byte_offset_from_isize, + check_mut_byte_offset_from_isize_arr + ); + + generate_mut_byte_offset_from_harness!( + (i8, i8), + check_mut_byte_offset_from_tuple_1, + check_mut_byte_offset_from_tuple_1_arr + ); + generate_mut_byte_offset_from_harness!( + (f64, bool), + check_mut_byte_offset_from_tuple_2, + check_mut_byte_offset_from_tuple_2_arr + ); + generate_mut_byte_offset_from_harness!( + (u32, i16, f32), + check_mut_byte_offset_from_tuple_3, + check_mut_byte_offset_from_tuple_3_arr + ); + generate_mut_byte_offset_from_harness!( + ((), bool, u8, u16, i32, f64, i128, usize), + check_mut_byte_offset_from_tuple_4, + check_mut_byte_offset_from_tuple_4_arr + ); + + // The length of a slice is set to an arbitrary value, which defines its size. + // In this case, implementing a slice with a dynamic size set using kani::any() + // is not possible, because PointerGenerator does not support non-deterministic + // slice pointers. + const SLICE_LEN: usize = 10; + + // generate proofs for contracts for byte_offset_from to verify slices + // - `$type`: type of the underlyign element within the slice pointer + // - `$proof_name`: name of the harness + macro_rules! generate_mut_byte_offset_from_slice_harness { + ($type: ty, $proof_name: ident) => { + #[kani::proof_for_contract(<*mut [$type]>::byte_offset_from)] + pub fn $proof_name() { + const gen_size: usize = mem::size_of::<$type>(); + let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let ptr1: *mut [$type] = generator1.any_in_bounds().ptr as *mut [$type; SLICE_LEN]; + let ptr2: *mut [$type] = if kani::any() { + generator1.any_alloc_status().ptr as *mut [$type; SLICE_LEN] + } else { + generator2.any_alloc_status().ptr as *mut [$type; SLICE_LEN] + }; + + unsafe { + ptr1.byte_offset_from(ptr2); + } + } + }; + } + + generate_mut_byte_offset_from_slice_harness!(u8, check_mut_byte_offset_from_u8_slice); + generate_mut_byte_offset_from_slice_harness!(u16, check_mut_byte_offset_from_u16_slice); + generate_mut_byte_offset_from_slice_harness!(u32, check_mut_byte_offset_from_u32_slice); + generate_mut_byte_offset_from_slice_harness!(u64, check_mut_byte_offset_from_u64_slice); + generate_mut_byte_offset_from_slice_harness!(u128, check_mut_byte_offset_from_u128_slice); + generate_mut_byte_offset_from_slice_harness!(usize, check_mut_byte_offset_from_usize_slice); + generate_mut_byte_offset_from_slice_harness!(i8, check_mut_byte_offset_from_i8_slice); + generate_mut_byte_offset_from_slice_harness!(i16, check_mut_byte_offset_from_i16_slice); + generate_mut_byte_offset_from_slice_harness!(i32, check_mut_byte_offset_from_i32_slice); + generate_mut_byte_offset_from_slice_harness!(i64, check_mut_byte_offset_from_i64_slice); + generate_mut_byte_offset_from_slice_harness!(i128, check_mut_byte_offset_from_i128_slice); + generate_mut_byte_offset_from_slice_harness!(isize, check_mut_byte_offset_from_isize_slice); + #[kani::proof_for_contract(<*mut ()>::byte_offset)] #[kani::should_panic] pub fn check_mut_byte_offset_unit_invalid_count() { From 607745967103ec9e47ac0a4c822b1c98c1bc7c14 Mon Sep 17 00:00:00 2001 From: Yifei Wang <40480373+xsxszab@users.noreply.github.com> Date: Mon, 9 Dec 2024 13:43:34 -0800 Subject: [PATCH 3/4] Added `` Proof for Contracts for `byte_add`, `byte_sub`, and `byte_offset` (#188) Towards #76 This pull request impelments proof for contracts for `byte_add`, `byte_sub` and `byte_offset` for ``. Both `const` and `mut` versions are included. It serves as an addition to an existing [PR](https://github.com/model-checking/verify-rust-std/pull/169) but is submitted separately to avoid disrupting the ongoing review process for that PR. --------- Co-authored-by: Surya Togaru Co-authored-by: stogaru <143449212+stogaru@users.noreply.github.com> Co-authored-by: Felipe R. Monteiro --- library/core/src/ptr/const_ptr.rs | 425 ++++++++++++--------- library/core/src/ptr/mut_ptr.rs | 598 +++++++++++++++++++++--------- 2 files changed, 668 insertions(+), 355 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 32baf1b33941a..5f818f90904bf 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -2122,7 +2122,7 @@ mod verify { ); // The array's length is set to an arbitrary value, which defines its size. - // In this case, implementing a dynamic array is not possible, because + // In this case, implementing a dynamic array is not possible, because // PointerGenerator does not support dynamic sized arrays. const ARRAY_LEN: usize = 40; @@ -2134,7 +2134,10 @@ mod verify { let self_ptr: *const u32 = unsafe { origin_ptr.byte_offset(offset as isize) }; let result: isize = unsafe { self_ptr.byte_offset_from(origin_ptr) }; assert_eq!(result, offset as isize); - assert_eq!(result, (self_ptr.addr() as isize - origin_ptr.addr() as isize)); + assert_eq!( + result, + (self_ptr.addr() as isize - origin_ptr.addr() as isize) + ); } macro_rules! generate_offset_from_harness { @@ -2273,186 +2276,6 @@ mod verify { check_const_offset_from_tuple_4_arr ); - // Proof for contact of byte_offset_from to verify unit type - #[kani::proof_for_contract(<*const ()>::byte_offset_from)] - pub fn check_const_byte_offset_from_unit() { - let val: () = (); - let src_ptr: *const () = &val; - let dest_ptr: *const () = &val; - unsafe { - dest_ptr.byte_offset_from(src_ptr); - } - } - - // generate proofs for contracts for byte_offset_from to verify int and composite - // types - // - `$type`: pointee type - // - `$proof_name1`: name of the harness for single element - // - `$proof_name2`: name of the harness for array of elements - macro_rules! generate_const_byte_offset_from_harness { - ($type: ty, $proof_name1: ident, $proof_name2: ident) => { - // Proof for a single element - #[kani::proof_for_contract(<*const $type>::byte_offset_from)] - pub fn $proof_name1() { - const gen_size: usize = mem::size_of::<$type>(); - let mut generator1 = PointerGenerator::::new(); - let mut generator2 = PointerGenerator::::new(); - let ptr1: *const $type = generator1.any_in_bounds().ptr; - let ptr2: *const $type = if kani::any() { - generator1.any_alloc_status().ptr - } else { - generator2.any_alloc_status().ptr - }; - - unsafe { - ptr1.byte_offset_from(ptr2); - } - } - - // Proof for large arrays - #[kani::proof_for_contract(<*const $type>::byte_offset_from)] - pub fn $proof_name2() { - const gen_size: usize = mem::size_of::<$type>(); - let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); - let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); - let ptr1: *const $type = generator1.any_in_bounds().ptr; - let ptr2: *const $type = if kani::any() { - generator1.any_alloc_status().ptr - } else { - generator2.any_alloc_status().ptr - }; - - unsafe { - ptr1.byte_offset_from(ptr2); - } - } - }; - } - - generate_const_byte_offset_from_harness!( - u8, - check_const_byte_offset_from_u8, - check_const_byte_offset_from_u8_arr - ); - generate_const_byte_offset_from_harness!( - u16, - check_const_byte_offset_from_u16, - check_const_byte_offset_from_u16_arr - ); - generate_const_byte_offset_from_harness!( - u32, - check_const_byte_offset_from_u32, - check_const_byte_offset_from_u32_arr - ); - generate_const_byte_offset_from_harness!( - u64, - check_const_byte_offset_from_u64, - check_const_byte_offset_from_u64_arr - ); - generate_const_byte_offset_from_harness!( - u128, - check_const_byte_offset_from_u128, - check_const_byte_offset_from_u128_arr - ); - generate_const_byte_offset_from_harness!( - usize, - check_const_byte_offset_from_usize, - check_const_byte_offset_from_usize_arr - ); - - generate_const_byte_offset_from_harness!( - i8, - check_const_byte_offset_from_i8, - check_const_byte_offset_from_i8_arr - ); - generate_const_byte_offset_from_harness!( - i16, - check_const_byte_offset_from_i16, - check_const_byte_offset_from_i16_arr - ); - generate_const_byte_offset_from_harness!( - i32, - check_const_byte_offset_from_i32, - check_const_byte_offset_from_i32_arr - ); - generate_const_byte_offset_from_harness!( - i64, - check_const_byte_offset_from_i64, - check_const_byte_offset_from_i64_arr - ); - generate_const_byte_offset_from_harness!( - i128, - check_const_byte_offset_from_i128, - check_const_byte_offset_from_i128_arr - ); - generate_const_byte_offset_from_harness!( - isize, - check_const_byte_offset_from_isize, - check_const_byte_offset_from_isize_arr - ); - - generate_const_byte_offset_from_harness!( - (i8, i8), - check_const_byte_offset_from_tuple_1, - check_const_byte_offset_from_tuple_1_arr - ); - generate_const_byte_offset_from_harness!( - (f64, bool), - check_const_byte_offset_from_tuple_2, - check_const_byte_offset_from_tuple_2_arr - ); - generate_const_byte_offset_from_harness!( - (u32, i16, f32), - check_const_byte_offset_from_tuple_3, - check_const_byte_offset_from_tuple_3_arr - ); - generate_const_byte_offset_from_harness!( - ((), bool, u8, u16, i32, f64, i128, usize), - check_const_byte_offset_from_tuple_4, - check_const_byte_offset_from_tuple_4_arr - ); - - // length of the slice generated from PointerGenerator - const SLICE_LEN: usize = 10; - - // generate proofs for contracts for byte_offset_from to verify slices - // - `$type`: type of the underlyign element within the slice pointer - // - `$proof_name`: name of the harness - macro_rules! generate_const_byte_offset_from_slice_harness { - ($type: ty, $proof_name: ident) => { - #[kani::proof_for_contract(<*const [$type]>::byte_offset_from)] - pub fn $proof_name() { - const gen_size: usize = mem::size_of::<$type>(); - let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); - let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); - let ptr1: *const [$type] = - generator1.any_in_bounds().ptr as *const [$type; SLICE_LEN]; - let ptr2: *const [$type] = if kani::any() { - generator1.any_alloc_status().ptr as *const [$type; SLICE_LEN] - } else { - generator2.any_alloc_status().ptr as *const [$type; SLICE_LEN] - }; - - unsafe { - ptr1.byte_offset_from(ptr2); - } - } - }; - } - - generate_const_byte_offset_from_slice_harness!(u8, check_const_byte_offset_from_u8_slice); - generate_const_byte_offset_from_slice_harness!(u16, check_const_byte_offset_from_u16_slice); - generate_const_byte_offset_from_slice_harness!(u32, check_const_byte_offset_from_u32_slice); - generate_const_byte_offset_from_slice_harness!(u64, check_const_byte_offset_from_u64_slice); - generate_const_byte_offset_from_slice_harness!(u128, check_const_byte_offset_from_u128_slice); - generate_const_byte_offset_from_slice_harness!(usize, check_const_byte_offset_from_usize_slice); - generate_const_byte_offset_from_slice_harness!(i8, check_const_byte_offset_from_i8_slice); - generate_const_byte_offset_from_slice_harness!(i16, check_const_byte_offset_from_i16_slice); - generate_const_byte_offset_from_slice_harness!(i32, check_const_byte_offset_from_i32_slice); - generate_const_byte_offset_from_slice_harness!(i64, check_const_byte_offset_from_i64_slice); - generate_const_byte_offset_from_slice_harness!(i128, check_const_byte_offset_from_i128_slice); - generate_const_byte_offset_from_slice_harness!(isize, check_const_byte_offset_from_isize_slice); - #[kani::proof_for_contract(<*const ()>::byte_offset)] #[kani::should_panic] pub fn check_const_byte_offset_unit_invalid_count() { @@ -2709,4 +2532,242 @@ mod verify { byte_offset, check_const_byte_offset_usize_slice ); + + // Trait used exclusively for implementing proofs for contracts for `dyn Trait` type. + trait TestTrait {} + + // Struct used exclusively for implementing proofs for contracts for `dyn Trait` type. + struct TestStruct { + value: i64, + } + + impl TestTrait for TestStruct {} + + // generate `dyn Trait` proof for contracts for byte_add, byte_sub and byte_offset. + // - `$fn_name`: function for which the contract must be verified + // - `$proof_name`: name of the harness generated + macro_rules! gen_const_byte_arith_harness_for_dyn { + (byte_offset, $proof_name:ident) => { + // tracking issue: https://github.com/model-checking/kani/issues/3763 + // Workaround: Directly verifying the method `<*const dyn TestTrait>::byte_offset` + // causes a compilation error. As a workaround, the proof is annotated with the + // underlying struct type instead. + #[kani::proof_for_contract(<*const TestStruct>::byte_offset)] + pub fn $proof_name() { + let test_struct = TestStruct { value: 42 }; + let trait_object: &dyn TestTrait = &test_struct; + let test_ptr: *const dyn TestTrait = trait_object; + + let count: isize = kani::any(); + + unsafe { + test_ptr.byte_offset(count); + } + } + }; + + ($fn_name: ident, $proof_name:ident) => { + // tracking issue: https://github.com/model-checking/kani/issues/3763 + // Workaround: Directly verifying the method `<*const dyn TestTrait>::$fn_name` + // causes a compilation error. As a workaround, the proof is annotated with the + // underlying struct type instead. + #[kani::proof_for_contract(<*const TestStruct>::$fn_name)] + pub fn $proof_name() { + let test_struct = TestStruct { value: 42 }; + let trait_object: &dyn TestTrait = &test_struct; + let test_ptr: *const dyn TestTrait = trait_object; + + //byte_add and byte_sub need count to be usize unlike byte_offset + let count: usize = kani::any(); + + unsafe { + test_ptr.$fn_name(count); + } + } + }; + } + + gen_const_byte_arith_harness_for_dyn!(byte_add, check_const_byte_add_dyn); + gen_const_byte_arith_harness_for_dyn!(byte_sub, check_const_byte_sub_dyn); + gen_const_byte_arith_harness_for_dyn!(byte_offset, check_const_byte_offset_dyn); + + // Proof for contact of byte_offset_from to verify unit type + #[kani::proof_for_contract(<*const ()>::byte_offset_from)] + pub fn check_const_byte_offset_from_unit() { + let val: () = (); + let src_ptr: *const () = &val; + let dest_ptr: *const () = &val; + unsafe { + dest_ptr.byte_offset_from(src_ptr); + } + } + + // generate proofs for contracts for byte_offset_from to verify int and composite + // types + // - `$type`: pointee type + // - `$proof_name1`: name of the harness for single element + // - `$proof_name2`: name of the harness for array of elements + macro_rules! generate_const_byte_offset_from_harness { + ($type: ty, $proof_name1: ident, $proof_name2: ident) => { + // Proof for pointers to a single element + #[kani::proof_for_contract(<*const $type>::byte_offset_from)] + pub fn $proof_name1() { + const gen_size: usize = mem::size_of::<$type>(); + let mut generator1 = PointerGenerator::::new(); + let mut generator2 = PointerGenerator::::new(); + let ptr1: *const $type = generator1.any_in_bounds().ptr; + let ptr2: *const $type = if kani::any() { + generator1.any_alloc_status().ptr + } else { + generator2.any_alloc_status().ptr + }; + + unsafe { + ptr1.byte_offset_from(ptr2); + } + } + + // Proof for pointers to large arrays + #[kani::proof_for_contract(<*const $type>::byte_offset_from)] + pub fn $proof_name2() { + const gen_size: usize = mem::size_of::<$type>(); + let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let ptr1: *const $type = generator1.any_in_bounds().ptr; + let ptr2: *const $type = if kani::any() { + generator1.any_alloc_status().ptr + } else { + generator2.any_alloc_status().ptr + }; + + unsafe { + ptr1.byte_offset_from(ptr2); + } + } + }; + } + + generate_const_byte_offset_from_harness!( + u8, + check_const_byte_offset_from_u8, + check_const_byte_offset_from_u8_arr + ); + generate_const_byte_offset_from_harness!( + u16, + check_const_byte_offset_from_u16, + check_const_byte_offset_from_u16_arr + ); + generate_const_byte_offset_from_harness!( + u32, + check_const_byte_offset_from_u32, + check_const_byte_offset_from_u32_arr + ); + generate_const_byte_offset_from_harness!( + u64, + check_const_byte_offset_from_u64, + check_const_byte_offset_from_u64_arr + ); + generate_const_byte_offset_from_harness!( + u128, + check_const_byte_offset_from_u128, + check_const_byte_offset_from_u128_arr + ); + generate_const_byte_offset_from_harness!( + usize, + check_const_byte_offset_from_usize, + check_const_byte_offset_from_usize_arr + ); + + generate_const_byte_offset_from_harness!( + i8, + check_const_byte_offset_from_i8, + check_const_byte_offset_from_i8_arr + ); + generate_const_byte_offset_from_harness!( + i16, + check_const_byte_offset_from_i16, + check_const_byte_offset_from_i16_arr + ); + generate_const_byte_offset_from_harness!( + i32, + check_const_byte_offset_from_i32, + check_const_byte_offset_from_i32_arr + ); + generate_const_byte_offset_from_harness!( + i64, + check_const_byte_offset_from_i64, + check_const_byte_offset_from_i64_arr + ); + generate_const_byte_offset_from_harness!( + i128, + check_const_byte_offset_from_i128, + check_const_byte_offset_from_i128_arr + ); + generate_const_byte_offset_from_harness!( + isize, + check_const_byte_offset_from_isize, + check_const_byte_offset_from_isize_arr + ); + + generate_const_byte_offset_from_harness!( + (i8, i8), + check_const_byte_offset_from_tuple_1, + check_const_byte_offset_from_tuple_1_arr + ); + generate_const_byte_offset_from_harness!( + (f64, bool), + check_const_byte_offset_from_tuple_2, + check_const_byte_offset_from_tuple_2_arr + ); + generate_const_byte_offset_from_harness!( + (u32, i16, f32), + check_const_byte_offset_from_tuple_3, + check_const_byte_offset_from_tuple_3_arr + ); + generate_const_byte_offset_from_harness!( + ((), bool, u8, u16, i32, f64, i128, usize), + check_const_byte_offset_from_tuple_4, + check_const_byte_offset_from_tuple_4_arr + ); + + // Length of the slice generated from PointerGenerator. + const SLICE_LEN: usize = 10; + + // Generate proofs for contracts for byte_offset_from to verify slice pointee types. + // - `$type`: type of the underlyign element within the slice pointer. + // - `$proof_name`: name of the harness. + macro_rules! generate_const_byte_offset_from_slice_harness { + ($type: ty, $proof_name: ident) => { + #[kani::proof_for_contract(<*const [$type]>::byte_offset_from)] + pub fn $proof_name() { + const gen_size: usize = mem::size_of::<$type>(); + let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let ptr1: *const [$type] = + generator1.any_in_bounds().ptr as *const [$type; SLICE_LEN]; + let ptr2: *const [$type] = if kani::any() { + generator1.any_alloc_status().ptr as *const [$type; SLICE_LEN] + } else { + generator2.any_alloc_status().ptr as *const [$type; SLICE_LEN] + }; + + unsafe { + ptr1.byte_offset_from(ptr2); + } + } + }; + } + + generate_const_byte_offset_from_slice_harness!(u8, check_const_byte_offset_from_u8_slice); + generate_const_byte_offset_from_slice_harness!(u16, check_const_byte_offset_from_u16_slice); + generate_const_byte_offset_from_slice_harness!(u32, check_const_byte_offset_from_u32_slice); + generate_const_byte_offset_from_slice_harness!(u64, check_const_byte_offset_from_u64_slice); + generate_const_byte_offset_from_slice_harness!(u128, check_const_byte_offset_from_u128_slice); + generate_const_byte_offset_from_slice_harness!(usize, check_const_byte_offset_from_usize_slice); + generate_const_byte_offset_from_slice_harness!(i8, check_const_byte_offset_from_i8_slice); + generate_const_byte_offset_from_slice_harness!(i16, check_const_byte_offset_from_i16_slice); + generate_const_byte_offset_from_slice_harness!(i32, check_const_byte_offset_from_i32_slice); + generate_const_byte_offset_from_slice_harness!(i64, check_const_byte_offset_from_i64_slice); + generate_const_byte_offset_from_slice_harness!(i128, check_const_byte_offset_from_i128_slice); + generate_const_byte_offset_from_slice_harness!(isize, check_const_byte_offset_from_isize_slice); } diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index ef291233ae336..af749191f5949 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -414,12 +414,12 @@ impl *mut T { // Precondition 3: If `T` is a unit type (`size_of::() == 0`), this check is unnecessary as it has no allocated memory. // Otherwise, for non-unit types, `self` and `self.wrapping_offset(count)` should point to the same allocated object, // restricting `count` to prevent crossing allocation boundaries. - ((core::mem::size_of::() == 0) || (kani::mem::same_allocation(self, self.wrapping_offset(count)))) + ((core::mem::size_of::() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_offset(count)))) )] // Postcondition: If `T` is a unit type (`size_of::() == 0`), no allocation check is needed. // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object, // verifying that the result remains within the same allocation as `self`. - #[ensures(|result| (core::mem::size_of::() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))] + #[ensures(|result| (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self as *const T, *result as *const T))] pub const unsafe fn offset(self, count: isize) -> *mut T where T: Sized, @@ -480,7 +480,7 @@ impl *mut T { (count == 0) || // Else if count is not zero, then ensure that subtracting `count` doesn't // cause overflow and that both pointers `self` and the result are in the - // same allocation + // same allocation. ((self.addr() as isize).checked_add(count).is_some() && core::ub_checks::same_allocation(self, self.wrapping_byte_offset(count))) )] @@ -1063,12 +1063,12 @@ impl *mut T { // Precondition 3: If `T` is a unit type (`size_of::() == 0`), this check is unnecessary as it has no allocated memory. // Otherwise, for non-unit types, `self` and `self.wrapping_add(count)` should point to the same allocated object, // restricting `count` to prevent crossing allocation boundaries. - ((core::mem::size_of::() == 0) || (kani::mem::same_allocation(self, self.wrapping_add(count)))) + ((core::mem::size_of::() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_add(count)))) )] // Postcondition: If `T` is a unit type (`size_of::() == 0`), no allocation check is needed. // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object, // verifying that the result remains within the same allocation as `self`. - #[ensures(|result| (core::mem::size_of::() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))] + #[ensures(|result| (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self as *const T, *result as *const T))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -1126,7 +1126,7 @@ impl *mut T { (count == 0) || // Else if count is not zero, then ensure that subtracting `count` doesn't // cause overflow and that both pointers `self` and the result are in the - // same allocation + // same allocation. ((self.addr() as isize).checked_add(count as isize).is_some() && core::ub_checks::same_allocation(self, self.wrapping_byte_add(count))) )] @@ -1203,12 +1203,12 @@ impl *mut T { // Precondition 3: If `T` is a unit type (`size_of::() == 0`), this check is unnecessary as it has no allocated memory. // Otherwise, for non-unit types, `self` and `self.wrapping_sub(count)` should point to the same allocated object, // restricting `count` to prevent crossing allocation boundaries. - ((core::mem::size_of::() == 0) || (kani::mem::same_allocation(self, self.wrapping_sub(count)))) + ((core::mem::size_of::() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_sub(count)))) )] // Postcondition: If `T` is a unit type (`size_of::() == 0`), no allocation check is needed. // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object, // verifying that the result remains within the same allocation as `self`. - #[ensures(|result| (core::mem::size_of::() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))] + #[ensures(|result| (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self as *const T, *result as *const T))] pub const unsafe fn sub(self, count: usize) -> Self where T: Sized, @@ -1272,7 +1272,7 @@ impl *mut T { (count == 0) || // Else if count is not zero, then ensure that subtracting `count` doesn't // cause overflow and that both pointers `self` and the result are in the - // same allocation + // same allocation. ((self.addr() as isize).checked_sub(count as isize).is_some() && core::ub_checks::same_allocation(self, self.wrapping_byte_sub(count))) )] @@ -2244,42 +2244,155 @@ mod verify { use core::mem; use kani::PointerGenerator; - // The array's length is set to an arbitrary value, which defines its size. - // In this case, implementing a dynamic array is not possible, because - // PointerGenerator or any_array() do not support dynamic sized arrays. - const ARRAY_LEN: usize = 40; - - #[kani::proof] - pub fn check_mut_byte_offset_from_fixed_offset() { - let mut arr: [u32; ARRAY_LEN] = kani::Arbitrary::any_array(); - let offset: usize = kani::any_where(|&x| x <= ARRAY_LEN); - let origin_ptr: *mut u32 = arr.as_mut_ptr(); - let self_ptr: *mut u32 = unsafe { origin_ptr.byte_offset(offset as isize) }; - let result: isize = unsafe { self_ptr.byte_offset_from(origin_ptr) }; - assert_eq!(result, offset as isize); - assert_eq!(result, (self_ptr.addr() as isize - origin_ptr.addr() as isize)); + /// This macro generates a single verification harness for the `offset`, `add`, or `sub` + /// pointer operations, supporting integer, composite, or unit types. + /// - `$ty`: The type of the slice's elements (e.g., `i32`, `u32`, tuples). + /// - `$fn_name`: The name of the function being checked (`add`, `sub`, or `offset`). + /// - `$proof_name`: The name assigned to the generated proof for the contract. + /// - `$count_ty:ty`: The type of the input variable passed to the method being invoked. + /// + /// Note: This macro is intended for internal use only and should be invoked exclusively + /// by the `generate_arithmetic_harnesses` macro. Its purpose is to reduce code duplication, + /// and it is not meant to be used directly elsewhere in the codebase. + macro_rules! generate_single_arithmetic_harness { + ($ty:ty, $proof_name:ident, $fn_name:ident, $count_ty:ty) => { + #[kani::proof_for_contract(<*mut $ty>::$fn_name)] + pub fn $proof_name() { + // 200 bytes are large enough to cover all pointee types used for testing + const BUF_SIZE: usize = 200; + let mut generator = kani::PointerGenerator::::new(); + let test_ptr: *mut $ty = generator.any_in_bounds().ptr; + let count: $count_ty = kani::any(); + unsafe { + test_ptr.$fn_name(count); + } + } + }; } - // Proof for unit size - #[kani::proof_for_contract(<*mut ()>::byte_offset_from)] - pub fn check_mut_byte_offset_from_unit() { - let mut val: () = (); - let src_ptr: *mut () = &mut val; - let dest_ptr: *mut () = &mut val; - unsafe { - dest_ptr.byte_offset_from(src_ptr); - } + /// This macro generates verification harnesses for the `offset`, `add`, and `sub` + /// pointer operations, supporting integer, composite, and unit types. + /// - `$ty`: The pointee type (e.g., i32, u32, tuples). + /// - `$offset_fn_name`: The name for the `offset` proof for contract. + /// - `$add_fn_name`: The name for the `add` proof for contract. + /// - `$sub_fn_name`: The name for the `sub` proof for contract. + macro_rules! generate_arithmetic_harnesses { + ($ty:ty, $add_fn_name:ident, $sub_fn_name:ident, $offset_fn_name:ident) => { + generate_single_arithmetic_harness!($ty, $add_fn_name, add, usize); + generate_single_arithmetic_harness!($ty, $sub_fn_name, sub, usize); + generate_single_arithmetic_harness!($ty, $offset_fn_name, offset, isize); + }; } - // generate proofs for contracts for byte_offset_from to verify int and composite - // types - // - `$type`: pointee type - // - `$proof_name1`: name of the harness for single element - // - `$proof_name2`: name of the harness for array of elements - macro_rules! generate_mut_byte_offset_from_harness { + // Generate harnesses for unit type (add, sub, offset) + generate_arithmetic_harnesses!( + (), + check_mut_add_unit, + check_mut_sub_unit, + check_mut_offset_unit + ); + + // Generate harnesses for integer types (add, sub, offset) + generate_arithmetic_harnesses!(i8, check_mut_add_i8, check_mut_sub_i8, check_mut_offset_i8); + generate_arithmetic_harnesses!( + i16, + check_mut_add_i16, + check_mut_sub_i16, + check_mut_offset_i16 + ); + generate_arithmetic_harnesses!( + i32, + check_mut_add_i32, + check_mut_sub_i32, + check_mut_offset_i32 + ); + generate_arithmetic_harnesses!( + i64, + check_mut_add_i64, + check_mut_sub_i64, + check_mut_offset_i64 + ); + generate_arithmetic_harnesses!( + i128, + check_mut_add_i128, + check_mut_sub_i128, + check_mut_offset_i128 + ); + generate_arithmetic_harnesses!( + isize, + check_mut_add_isize, + check_mut_sub_isize, + check_mut_offset_isize + ); + // Due to a bug of kani the test `check_mut_add_u8` is malfunctioning for now. + // Tracking issue: https://github.com/model-checking/kani/issues/3743 + // generate_arithmetic_harnesses!(u8, check_mut_add_u8, check_mut_sub_u8, check_mut_offset_u8); + generate_arithmetic_harnesses!( + u16, + check_mut_add_u16, + check_mut_sub_u16, + check_mut_offset_u16 + ); + generate_arithmetic_harnesses!( + u32, + check_mut_add_u32, + check_mut_sub_u32, + check_mut_offset_u32 + ); + generate_arithmetic_harnesses!( + u64, + check_mut_add_u64, + check_mut_sub_u64, + check_mut_offset_u64 + ); + generate_arithmetic_harnesses!( + u128, + check_mut_add_u128, + check_mut_sub_u128, + check_mut_offset_u128 + ); + generate_arithmetic_harnesses!( + usize, + check_mut_add_usize, + check_mut_sub_usize, + check_mut_offset_usize + ); + + // Generte harnesses for composite types (add, sub, offset) + generate_arithmetic_harnesses!( + (i8, i8), + check_mut_add_tuple_1, + check_mut_sub_tuple_1, + check_mut_offset_tuple_1 + ); + generate_arithmetic_harnesses!( + (f64, bool), + check_mut_add_tuple_2, + check_mut_sub_tuple_2, + check_mut_offset_tuple_2 + ); + generate_arithmetic_harnesses!( + (i32, f64, bool), + check_mut_add_tuple_3, + check_mut_sub_tuple_3, + check_mut_offset_tuple_3 + ); + generate_arithmetic_harnesses!( + (i8, u16, i32, u64, isize), + check_mut_add_tuple_4, + check_mut_sub_tuple_4, + check_mut_offset_tuple_4 + ); + + // The array's length is set to an arbitrary value, which defines its size. + // In this case, implementing a dynamic array is not possible, because + // PointerGenerator does not support dynamic sized arrays. + const ARRAY_LEN: usize = 40; + + macro_rules! generate_offset_from_harness { ($type: ty, $proof_name1: ident, $proof_name2: ident) => { - // Proof for a single element - #[kani::proof_for_contract(<*mut $type>::byte_offset_from)] + #[kani::proof_for_contract(<*mut $type>::offset_from)] + // Below function is for a single element. pub fn $proof_name1() { const gen_size: usize = mem::size_of::<$type>(); let mut generator1 = PointerGenerator::::new(); @@ -2292,12 +2405,11 @@ mod verify { }; unsafe { - ptr1.byte_offset_from(ptr2); + ptr1.offset_from(ptr2); } } - // Proof for large arrays - #[kani::proof_for_contract(<*mut $type>::byte_offset_from)] + // Below function is for large arrays pub fn $proof_name2() { const gen_size: usize = mem::size_of::<$type>(); let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); @@ -2310,138 +2422,99 @@ mod verify { }; unsafe { - ptr1.byte_offset_from(ptr2); + ptr1.offset_from(ptr2); } } }; } - generate_mut_byte_offset_from_harness!( - u8, - check_mut_byte_offset_from_u8, - check_mut_byte_offset_from_u8_arr - ); - generate_mut_byte_offset_from_harness!( + // The proof for a unit type panics as offset_from needs the pointee size > 0 + #[kani::proof_for_contract(<*mut ()>::offset_from)] + #[kani::should_panic] + pub fn check_mut_offset_from_unit() { + let mut val: () = (); + let src_ptr: *mut () = &mut val; + let dest_ptr: *mut () = &mut val; + unsafe { + dest_ptr.offset_from(src_ptr); + } + } + + generate_offset_from_harness!(u8, check_mut_offset_from_u8, check_mut_offset_from_u8_array); + generate_offset_from_harness!( u16, - check_mut_byte_offset_from_u16, - check_mut_byte_offset_from_u16_arr + check_mut_offset_from_u16, + check_mut_offset_from_u16_array ); - generate_mut_byte_offset_from_harness!( + generate_offset_from_harness!( u32, - check_mut_byte_offset_from_u32, - check_mut_byte_offset_from_u32_arr + check_mut_offset_from_u32, + check_mut_offset_from_u32_array ); - generate_mut_byte_offset_from_harness!( + generate_offset_from_harness!( u64, - check_mut_byte_offset_from_u64, - check_mut_byte_offset_from_u64_arr + check_mut_offset_from_u64, + check_mut_offset_from_u64_array ); - generate_mut_byte_offset_from_harness!( + generate_offset_from_harness!( u128, - check_mut_byte_offset_from_u128, - check_mut_byte_offset_from_u128_arr + check_mut_offset_from_u128, + check_mut_offset_from_u128_array ); - generate_mut_byte_offset_from_harness!( + generate_offset_from_harness!( usize, - check_mut_byte_offset_from_usize, - check_mut_byte_offset_from_usize_arr + check_mut_offset_from_usize, + check_mut_offset_from_usize_array ); - generate_mut_byte_offset_from_harness!( - i8, - check_mut_byte_offset_from_i8, - check_mut_byte_offset_from_i8_arr - ); - generate_mut_byte_offset_from_harness!( + generate_offset_from_harness!(i8, check_mut_offset_from_i8, check_mut_offset_from_i8_array); + generate_offset_from_harness!( i16, - check_mut_byte_offset_from_i16, - check_mut_byte_offset_from_i16_arr + check_mut_offset_from_i16, + check_mut_offset_from_i16_array ); - generate_mut_byte_offset_from_harness!( + generate_offset_from_harness!( i32, - check_mut_byte_offset_from_i32, - check_mut_byte_offset_from_i32_arr + check_mut_offset_from_i32, + check_mut_offset_from_i32_array ); - generate_mut_byte_offset_from_harness!( + generate_offset_from_harness!( i64, - check_mut_byte_offset_from_i64, - check_mut_byte_offset_from_i64_arr + check_mut_offset_from_i64, + check_mut_offset_from_i64_array ); - generate_mut_byte_offset_from_harness!( + generate_offset_from_harness!( i128, - check_mut_byte_offset_from_i128, - check_mut_byte_offset_from_i128_arr + check_mut_offset_from_i128, + check_mut_offset_from_i128_array ); - generate_mut_byte_offset_from_harness!( + generate_offset_from_harness!( isize, - check_mut_byte_offset_from_isize, - check_mut_byte_offset_from_isize_arr + check_mut_offset_from_isize, + check_mut_offset_from_isize_array ); - generate_mut_byte_offset_from_harness!( + generate_offset_from_harness!( (i8, i8), - check_mut_byte_offset_from_tuple_1, - check_mut_byte_offset_from_tuple_1_arr + check_mut_offset_from_tuple_1, + check_mut_offset_from_tuple_1_array ); - generate_mut_byte_offset_from_harness!( + generate_offset_from_harness!( (f64, bool), - check_mut_byte_offset_from_tuple_2, - check_mut_byte_offset_from_tuple_2_arr + check_mut_offset_from_tuple_2, + check_mut_offset_from_tuple_2_array ); - generate_mut_byte_offset_from_harness!( + generate_offset_from_harness!( (u32, i16, f32), - check_mut_byte_offset_from_tuple_3, - check_mut_byte_offset_from_tuple_3_arr + check_mut_offset_from_tuple_3, + check_mut_offset_from_tuple_3_array ); - generate_mut_byte_offset_from_harness!( + generate_offset_from_harness!( ((), bool, u8, u16, i32, f64, i128, usize), - check_mut_byte_offset_from_tuple_4, - check_mut_byte_offset_from_tuple_4_arr + check_mut_offset_from_tuple_4, + check_mut_offset_from_tuple_4_array ); - // The length of a slice is set to an arbitrary value, which defines its size. - // In this case, implementing a slice with a dynamic size set using kani::any() - // is not possible, because PointerGenerator does not support non-deterministic - // slice pointers. - const SLICE_LEN: usize = 10; - - // generate proofs for contracts for byte_offset_from to verify slices - // - `$type`: type of the underlyign element within the slice pointer - // - `$proof_name`: name of the harness - macro_rules! generate_mut_byte_offset_from_slice_harness { - ($type: ty, $proof_name: ident) => { - #[kani::proof_for_contract(<*mut [$type]>::byte_offset_from)] - pub fn $proof_name() { - const gen_size: usize = mem::size_of::<$type>(); - let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); - let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); - let ptr1: *mut [$type] = generator1.any_in_bounds().ptr as *mut [$type; SLICE_LEN]; - let ptr2: *mut [$type] = if kani::any() { - generator1.any_alloc_status().ptr as *mut [$type; SLICE_LEN] - } else { - generator2.any_alloc_status().ptr as *mut [$type; SLICE_LEN] - }; - - unsafe { - ptr1.byte_offset_from(ptr2); - } - } - }; - } - - generate_mut_byte_offset_from_slice_harness!(u8, check_mut_byte_offset_from_u8_slice); - generate_mut_byte_offset_from_slice_harness!(u16, check_mut_byte_offset_from_u16_slice); - generate_mut_byte_offset_from_slice_harness!(u32, check_mut_byte_offset_from_u32_slice); - generate_mut_byte_offset_from_slice_harness!(u64, check_mut_byte_offset_from_u64_slice); - generate_mut_byte_offset_from_slice_harness!(u128, check_mut_byte_offset_from_u128_slice); - generate_mut_byte_offset_from_slice_harness!(usize, check_mut_byte_offset_from_usize_slice); - generate_mut_byte_offset_from_slice_harness!(i8, check_mut_byte_offset_from_i8_slice); - generate_mut_byte_offset_from_slice_harness!(i16, check_mut_byte_offset_from_i16_slice); - generate_mut_byte_offset_from_slice_harness!(i32, check_mut_byte_offset_from_i32_slice); - generate_mut_byte_offset_from_slice_harness!(i64, check_mut_byte_offset_from_i64_slice); - generate_mut_byte_offset_from_slice_harness!(i128, check_mut_byte_offset_from_i128_slice); - generate_mut_byte_offset_from_slice_harness!(isize, check_mut_byte_offset_from_isize_slice); - #[kani::proof_for_contract(<*mut ()>::byte_offset)] #[kani::should_panic] pub fn check_mut_byte_offset_unit_invalid_count() { @@ -2465,7 +2538,7 @@ mod verify { } // generate proof for contracts of byte_add, byte_sub and byte_offset to verify - // unit pointee type + // unit pointee type. // - `$fn_name`: function for which the contract must be verified // - `$proof_name`: name of the harness generated macro_rules! gen_mut_byte_arith_harness_for_unit { @@ -2686,22 +2759,99 @@ mod verify { gen_mut_byte_arith_harness_for_slice!(u128, byte_offset, check_mut_byte_offset_u128_slice); gen_mut_byte_arith_harness_for_slice!(usize, byte_offset, check_mut_byte_offset_usize_slice); - // The proof for a unit type panics as offset_from needs the pointee size > 0 - #[kani::proof_for_contract(<*mut ()>::offset_from)] - #[kani::should_panic] - pub fn check_mut_offset_from_unit() { + // Trait used exclusively for implementing proofs for contracts for `dyn Trait` type. + trait TestTrait {} + + // Struct used exclusively for implementing proofs for contracts for `dyn Trait` type. + struct TestStruct { + value: i64, + } + + impl TestTrait for TestStruct {} + + /// This macro generates proofs for contracts on `byte_add`, `byte_sub`, and `byte_offset` + /// operations for pointers to dyn Trait. + /// - `$fn_name`: Specifies the arithmetic operation to verify. + /// - `$proof_name`: Specifies the name of the generated proof for contract. + macro_rules! gen_mut_byte_arith_harness_for_dyn { + (byte_offset, $proof_name:ident) => { + //tracking issue: https://github.com/model-checking/kani/issues/3763 + // Workaround: Directly verifying the method `<*mut dyn TestTrait>::byte_offset` + // causes a compilation error. As a workaround, the proof is annotated with the + // underlying struct type instead. + #[kani::proof_for_contract(<*mut TestStruct>::byte_offset)] + pub fn $proof_name() { + let mut test_struct = TestStruct { value: 42 }; + let trait_object: &mut dyn TestTrait = &mut test_struct; + let test_ptr: *mut dyn TestTrait = trait_object; + + let count: isize = kani::any(); + + unsafe { + test_ptr.byte_offset(count); + } + } + }; + ($fn_name: ident, $proof_name:ident) => { + //tracking issue: https://github.com/model-checking/kani/issues/3763 + // Workaround: Directly verifying the method `<*mut dyn TestTrait>::$fn_name` + // causes a compilation error. As a workaround, the proof is annotated with the + // underlying struct type instead. + #[kani::proof_for_contract(<*mut TestStruct>::$fn_name)] + pub fn $proof_name() { + let mut test_struct = TestStruct { value: 42 }; + let trait_object: &mut dyn TestTrait = &mut test_struct; + let test_ptr: *mut dyn TestTrait = trait_object; + + //byte_add and byte_sub need count to be usize unlike byte_offset + let count: usize = kani::any(); + + unsafe { + test_ptr.$fn_name(count); + } + } + }; + } + + // fn <*mut T>::add(), <*mut T>::sub() and <*mut T>::offset() dyn Trait verification + gen_mut_byte_arith_harness_for_dyn!(byte_add, check_mut_byte_add_dyn); + gen_mut_byte_arith_harness_for_dyn!(byte_sub, check_mut_byte_sub_dyn); + gen_mut_byte_arith_harness_for_dyn!(byte_offset, check_mut_byte_offset_dyn); + + #[kani::proof] + pub fn check_mut_byte_offset_from_fixed_offset() { + let mut arr: [u32; ARRAY_LEN] = kani::Arbitrary::any_array(); + let offset: usize = kani::any_where(|&x| x <= ARRAY_LEN); + let origin_ptr: *mut u32 = arr.as_mut_ptr(); + let self_ptr: *mut u32 = unsafe { origin_ptr.byte_offset(offset as isize) }; + let result: isize = unsafe { self_ptr.byte_offset_from(origin_ptr) }; + assert_eq!(result, offset as isize); + assert_eq!( + result, + (self_ptr.addr() as isize - origin_ptr.addr() as isize) + ); + } + + // Proof for unit size + #[kani::proof_for_contract(<*mut ()>::byte_offset_from)] + pub fn check_mut_byte_offset_from_unit() { let mut val: () = (); let src_ptr: *mut () = &mut val; let dest_ptr: *mut () = &mut val; unsafe { - dest_ptr.offset_from(src_ptr); + dest_ptr.byte_offset_from(src_ptr); } } - macro_rules! generate_offset_from_harness { + // Generate proofs for contracts for byte_offset_from to verify pointer to int + // and composite types. + // - `$type`: pointee type. + // - `$proof_name1`: name of the harness for single element. + // - `$proof_name2`: name of the harness for array of elements. + macro_rules! generate_mut_byte_offset_from_harness { ($type: ty, $proof_name1: ident, $proof_name2: ident) => { - #[kani::proof_for_contract(<*mut $type>::offset_from)] - // Below function is for a single element + // Proof for a single element + #[kani::proof_for_contract(<*mut $type>::byte_offset_from)] pub fn $proof_name1() { const gen_size: usize = mem::size_of::<$type>(); let mut generator1 = PointerGenerator::::new(); @@ -2712,13 +2862,14 @@ mod verify { } else { generator2.any_alloc_status().ptr }; - + unsafe { - ptr1.offset_from(ptr2); + ptr1.byte_offset_from(ptr2); } } - // Below function is for large arrays + // Proof for large arrays + #[kani::proof_for_contract(<*mut $type>::byte_offset_from)] pub fn $proof_name2() { const gen_size: usize = mem::size_of::<$type>(); let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); @@ -2729,36 +2880,137 @@ mod verify { } else { generator2.any_alloc_status().ptr }; - + unsafe { - ptr1.offset_from(ptr2); + ptr1.byte_offset_from(ptr2); } } - }; } - generate_offset_from_harness!(u8, check_mut_offset_from_u8, check_mut_offset_from_u8_array); - generate_offset_from_harness!(u16, check_mut_offset_from_u16, check_mut_offset_from_u16_array); - generate_offset_from_harness!(u32, check_mut_offset_from_u32, check_mut_offset_from_u32_array); - generate_offset_from_harness!(u64, check_mut_offset_from_u64, check_mut_offset_from_u64_array); - generate_offset_from_harness!(u128, check_mut_offset_from_u128, check_mut_offset_from_u128_array); - generate_offset_from_harness!(usize, check_mut_offset_from_usize, check_mut_offset_from_usize_array); + generate_mut_byte_offset_from_harness!( + u8, + check_mut_byte_offset_from_u8, + check_mut_byte_offset_from_u8_arr + ); + generate_mut_byte_offset_from_harness!( + u16, + check_mut_byte_offset_from_u16, + check_mut_byte_offset_from_u16_arr + ); + generate_mut_byte_offset_from_harness!( + u32, + check_mut_byte_offset_from_u32, + check_mut_byte_offset_from_u32_arr + ); + generate_mut_byte_offset_from_harness!( + u64, + check_mut_byte_offset_from_u64, + check_mut_byte_offset_from_u64_arr + ); + generate_mut_byte_offset_from_harness!( + u128, + check_mut_byte_offset_from_u128, + check_mut_byte_offset_from_u128_arr + ); + generate_mut_byte_offset_from_harness!( + usize, + check_mut_byte_offset_from_usize, + check_mut_byte_offset_from_usize_arr + ); - generate_offset_from_harness!(i8, check_mut_offset_from_i8, check_mut_offset_from_i8_array); - generate_offset_from_harness!(i16, check_mut_offset_from_i16, check_mut_offset_from_i16_array); - generate_offset_from_harness!(i32, check_mut_offset_from_i32, check_mut_offset_from_i32_array); - generate_offset_from_harness!(i64, check_mut_offset_from_i64, check_mut_offset_from_i64_array); - generate_offset_from_harness!(i128, check_mut_offset_from_i128, check_mut_offset_from_i128_array); - generate_offset_from_harness!(isize, check_mut_offset_from_isize, check_mut_offset_from_isize_array); - - generate_offset_from_harness!((i8, i8), check_mut_offset_from_tuple_1, check_mut_offset_from_tuple_1_array); - generate_offset_from_harness!((f64, bool), check_mut_offset_from_tuple_2, check_mut_offset_from_tuple_2_array); - generate_offset_from_harness!((u32, i16, f32), check_mut_offset_from_tuple_3, check_mut_offset_from_tuple_3_array); - generate_offset_from_harness!( + generate_mut_byte_offset_from_harness!( + i8, + check_mut_byte_offset_from_i8, + check_mut_byte_offset_from_i8_arr + ); + generate_mut_byte_offset_from_harness!( + i16, + check_mut_byte_offset_from_i16, + check_mut_byte_offset_from_i16_arr + ); + generate_mut_byte_offset_from_harness!( + i32, + check_mut_byte_offset_from_i32, + check_mut_byte_offset_from_i32_arr + ); + generate_mut_byte_offset_from_harness!( + i64, + check_mut_byte_offset_from_i64, + check_mut_byte_offset_from_i64_arr + ); + generate_mut_byte_offset_from_harness!( + i128, + check_mut_byte_offset_from_i128, + check_mut_byte_offset_from_i128_arr + ); + generate_mut_byte_offset_from_harness!( + isize, + check_mut_byte_offset_from_isize, + check_mut_byte_offset_from_isize_arr + ); + + generate_mut_byte_offset_from_harness!( + (i8, i8), + check_mut_byte_offset_from_tuple_1, + check_mut_byte_offset_from_tuple_1_arr + ); + generate_mut_byte_offset_from_harness!( + (f64, bool), + check_mut_byte_offset_from_tuple_2, + check_mut_byte_offset_from_tuple_2_arr + ); + generate_mut_byte_offset_from_harness!( + (u32, i16, f32), + check_mut_byte_offset_from_tuple_3, + check_mut_byte_offset_from_tuple_3_arr + ); + generate_mut_byte_offset_from_harness!( ((), bool, u8, u16, i32, f64, i128, usize), - check_mut_offset_from_tuple_4, - check_mut_offset_from_tuple_4_array + check_mut_byte_offset_from_tuple_4, + check_mut_byte_offset_from_tuple_4_arr ); + // The length of a slice is set to an arbitrary value, which defines its size. + // In this case, implementing a slice with a dynamic size set using kani::any() + // is not possible, because PointerGenerator does not support non-deterministic + // slice pointers. + const SLICE_LEN: usize = 10; + + // Generate proofs for contracts for byte_offset_from to verify pointers to slices + // - `$type`: type of the underlyign element within the slice pointer. + // - `$proof_name`: name of the harness. + macro_rules! generate_mut_byte_offset_from_slice_harness { + ($type: ty, $proof_name: ident) => { + #[kani::proof_for_contract(<*mut [$type]>::byte_offset_from)] + pub fn $proof_name() { + const gen_size: usize = mem::size_of::<$type>(); + let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let ptr1: *mut [$type] = generator1.any_in_bounds().ptr as *mut [$type; SLICE_LEN]; + let ptr2: *mut [$type] = if kani::any() { + generator1.any_alloc_status().ptr as *mut [$type; SLICE_LEN] + } else { + generator2.any_alloc_status().ptr as *mut [$type; SLICE_LEN] + }; + + unsafe { + ptr1.byte_offset_from(ptr2); + } + } + }; + } + + generate_mut_byte_offset_from_slice_harness!(u8, check_mut_byte_offset_from_u8_slice); + generate_mut_byte_offset_from_slice_harness!(u16, check_mut_byte_offset_from_u16_slice); + generate_mut_byte_offset_from_slice_harness!(u32, check_mut_byte_offset_from_u32_slice); + generate_mut_byte_offset_from_slice_harness!(u64, check_mut_byte_offset_from_u64_slice); + generate_mut_byte_offset_from_slice_harness!(u128, check_mut_byte_offset_from_u128_slice); + generate_mut_byte_offset_from_slice_harness!(usize, check_mut_byte_offset_from_usize_slice); + generate_mut_byte_offset_from_slice_harness!(i8, check_mut_byte_offset_from_i8_slice); + generate_mut_byte_offset_from_slice_harness!(i16, check_mut_byte_offset_from_i16_slice); + generate_mut_byte_offset_from_slice_harness!(i32, check_mut_byte_offset_from_i32_slice); + generate_mut_byte_offset_from_slice_harness!(i64, check_mut_byte_offset_from_i64_slice); + generate_mut_byte_offset_from_slice_harness!(i128, check_mut_byte_offset_from_i128_slice); + generate_mut_byte_offset_from_slice_harness!(isize, check_mut_byte_offset_from_isize_slice); } From 6928d22ac9f10e015c165ae4b228bbdc50923e71 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 9 Dec 2024 16:59:51 -0800 Subject: [PATCH 4/4] Prepare repo for enabling merge queue (#215) Add `merge_group` as a trigger for our workflows. For the review check workflow, I also added a review dismissed option, and for the `merge_group` case, the workflow does nothing. 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: Carolyn Zech Co-authored-by: Michael Tautschnig --- .github/workflows/book.yml | 1 + .github/workflows/kani.yml | 1 + .github/workflows/pr_approval.yml | 20 ++++++++++++++------ .github/workflows/rustc.yml | 1 + 4 files changed, 17 insertions(+), 6 deletions(-) diff --git a/.github/workflows/book.yml b/.github/workflows/book.yml index 9b1ab637140c3..200068be74745 100644 --- a/.github/workflows/book.yml +++ b/.github/workflows/book.yml @@ -3,6 +3,7 @@ name: Build Book on: workflow_dispatch: + merge_group: pull_request: branches: [ main ] push: diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index b3c8aa3882066..7e0ccfd3551e4 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -2,6 +2,7 @@ name: Kani on: workflow_dispatch: + merge_group: pull_request: branches: [ main ] push: diff --git a/.github/workflows/pr_approval.yml b/.github/workflows/pr_approval.yml index f261da3ad2ac2..06dbb1599d93f 100644 --- a/.github/workflows/pr_approval.yml +++ b/.github/workflows/pr_approval.yml @@ -1,12 +1,17 @@ +# This workflow checks that the PR has been approved by 2+ members of the committee listed in `pull_requests.toml`. +# +# Run this action when a pull request review is submitted / dismissed. +# Note that an approval can be dismissed, and this can affect the job status. +# We currently trust that contributors won't make significant changes to their PRs after approval, so we accept +# changes after approval. +# +# We still need to run this in the case of a merge group, since it is a required step. In that case, the workflow +# is a NOP. name: Check PR Approvals - -# For now, the workflow gets triggered only when a review is submitted -# This technically means, a PR with zero approvals can be merged by the rules of this workflow alone -# To protect against that scenario, we can turn on number of approvals required to 2 in the github settings -# of the repository on: + merge_group: pull_request_review: - types: [submitted] + types: [submitted, dismissed] jobs: check-approvals: @@ -14,12 +19,15 @@ jobs: steps: - name: Checkout repository uses: actions/checkout@v2 + if: ${{ github.event_name != 'merge_group' }} - name: Install TOML parser run: npm install @iarna/toml + if: ${{ github.event_name != 'merge_group' }} - name: Check PR Relevance and Approvals uses: actions/github-script@v6 + if: ${{ github.event_name != 'merge_group' }} with: script: | const fs = require('fs'); diff --git a/.github/workflows/rustc.yml b/.github/workflows/rustc.yml index 112c1f58f7ce8..498c64c3b447f 100644 --- a/.github/workflows/rustc.yml +++ b/.github/workflows/rustc.yml @@ -4,6 +4,7 @@ name: Rust Tests on: workflow_dispatch: + merge_group: pull_request: branches: [ main ] push: