From c841a12bf045cc71cc2a181a6f80b0ac06125a88 Mon Sep 17 00:00:00 2001 From: Dhvani-Kapadia <159494547+Dhvani-Kapadia@users.noreply.github.com> Date: Wed, 4 Dec 2024 17:20:13 -0800 Subject: [PATCH 01/14] Contract and harness for as_ptr, cast, as_mut_ptr, and as_non_null_ptr (#126) ### Description This PR includes contracts and proof harnesses for the four APIs as_ptr, cast, as_mut_ptr, and as_non_null_ptr which are part of the NonNull library in Rust. ### Changes Overview: Covered APIs: NonNull::as_ptr: Acquires the underlying *mut pointer NonNull::cast: Casts to a pointer of another type NonNull:: as_mut_ptr: Returns raw pointer to array's buffer NonNull::as_non_null_ptr: Returns a non-null pointer to slice's buffer Proof harness: non_null_check_as_ptr non_null_check_cast non_null_check_as_mut_ptr non_null_check_as_non_null_ptr Revalidation To revalidate the verification results, run kani verify-std -Z unstable-options "path/to/library" -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify. This will run all four harnesses in the module. All default checks should pass: ``` SUMMARY: ** 0 of 128 failed VERIFICATION:- SUCCESSFUL Verification Time: 0.8232234s Complete - 4 successfully verified harnesses, 0 failures, 4 total. ``` Towards issue #53 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: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Co-authored-by: Zyad Hassan Co-authored-by: Michael Tautschnig Co-authored-by: Qinyuan Wu <53478459+QinyuanWu@users.noreply.github.com> --- library/core/src/ptr/non_null.rs | 44 ++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index c347d8b82c4ac..4174377a84408 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -353,6 +353,8 @@ impl NonNull { #[rustc_never_returns_null_ptr] #[must_use] #[inline(always)] + //Ensures address of resulting pointer is same as original + #[ensures(|result: &*mut T| *result == self.pointer as *mut T)] pub const fn as_ptr(self) -> *mut T { self.pointer as *mut T } @@ -454,6 +456,8 @@ impl NonNull { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline] + // Address preservation + #[ensures(|result: &NonNull| result.as_ptr().addr() == self.as_ptr().addr())] pub const fn cast(self) -> NonNull { // SAFETY: `self` is a `NonNull` pointer which is necessarily non-null unsafe { NonNull { pointer: self.as_ptr() as *mut U } } @@ -1470,6 +1474,8 @@ impl NonNull<[T]> { #[inline] #[must_use] #[unstable(feature = "slice_ptr_get", issue = "74265")] + // Address preservation + #[ensures(|result: &NonNull| result.as_ptr().addr() == self.as_ptr().addr())] pub const fn as_non_null_ptr(self) -> NonNull { self.cast() } @@ -1489,6 +1495,8 @@ impl NonNull<[T]> { #[must_use] #[unstable(feature = "slice_ptr_get", issue = "74265")] #[rustc_never_returns_null_ptr] + // Address preservation + #[ensures(|result: &*mut T| *result == self.pointer as *mut T)] pub const fn as_mut_ptr(self) -> *mut T { self.as_non_null_ptr().as_ptr() } @@ -2186,6 +2194,42 @@ mod verify { } } + #[kani::proof_for_contract(NonNull::as_ptr)] + pub fn non_null_check_as_ptr() { + // Create a non-null pointer to a random value + let non_null_ptr: *mut i32 = kani::any::() as *mut i32; + if let Some(ptr) = NonNull::new(non_null_ptr) { + let result = ptr.as_ptr(); + } + + } + + #[kani::proof_for_contract(NonNull::<[T]>::as_mut_ptr)] + pub fn non_null_check_as_mut_ptr() { + const ARR_LEN: usize = 100; + let mut values: [i32; ARR_LEN] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut values); + let non_null_ptr = NonNull::new(slice as *mut [i32]).unwrap(); + let result = non_null_ptr.as_mut_ptr(); + } + #[kani::proof_for_contract(NonNull::::cast)] + pub fn non_null_check_cast() { + // Create a non-null pointer to a random value + let non_null_ptr: *mut i32 = kani::any::() as *mut i32; + if let Some(ptr) = NonNull::new(non_null_ptr) { + let result: NonNull = ptr.cast(); + } + } + + #[kani::proof_for_contract(NonNull::<[T]>::as_non_null_ptr)] + pub fn non_null_check_as_non_null_ptr() { + const ARR_LEN: usize = 100; + let mut values: [i32; ARR_LEN] = kani::any(); + let slice = kani::slice::any_slice_of_array_mut(&mut values); + let non_null_ptr = NonNull::new(slice as *mut [i32]).unwrap(); + let result = non_null_ptr.as_non_null_ptr(); + } + #[kani::proof] pub fn non_null_check_len() { // Create a non-deterministic NonNull pointer using kani::any() From 30c756d913d1ae234822b9eb995ab3d74a234c9e Mon Sep 17 00:00:00 2001 From: MWDZ <101102544+MWDZ@users.noreply.github.com> Date: Wed, 4 Dec 2024 23:25:20 -0800 Subject: [PATCH 02/14] Contracts & Harnesses for [f16, f128] to_int_unchecked (#163) --- library/core/src/num/f128.rs | 8 ++++++++ library/core/src/num/f16.rs | 7 +++++++ library/core/src/num/mod.rs | 30 ++++++++++++++++++++++++++++++ 3 files changed, 45 insertions(+) diff --git a/library/core/src/num/f128.rs b/library/core/src/num/f128.rs index abeccb7eea248..1bccfe4f7f278 100644 --- a/library/core/src/num/f128.rs +++ b/library/core/src/num/f128.rs @@ -17,7 +17,13 @@ use crate::intrinsics; use crate::mem; use crate::num::FpCategory; use crate::panic::const_assert; +use safety::requires; +#[cfg(kani)] +use crate::kani; + +#[allow(unused_imports)] +use crate::ub_checks::float_to_int_in_range; /// Basic mathematical constants. #[unstable(feature = "f128", issue = "116909")] pub mod consts { @@ -869,6 +875,8 @@ impl f128 { #[inline] #[unstable(feature = "f128", issue = "116909")] #[must_use = "this returns the result of the operation, without modifying the original"] + // is_finite() checks if the given float is neither infinite nor NaN. + #[requires(self.is_finite() && float_to_int_in_range::(self))] pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt, diff --git a/library/core/src/num/f16.rs b/library/core/src/num/f16.rs index 0d3e92695707c..41a37321f4870 100644 --- a/library/core/src/num/f16.rs +++ b/library/core/src/num/f16.rs @@ -17,7 +17,13 @@ use crate::intrinsics; use crate::mem; use crate::num::FpCategory; use crate::panic::const_assert; +use safety::requires; +#[cfg(kani)] +use crate::kani; + +#[allow(unused_imports)] +use crate::ub_checks::float_to_int_in_range; /// Basic mathematical constants. #[unstable(feature = "f16", issue = "116909")] pub mod consts { @@ -855,6 +861,7 @@ impl f16 { #[inline] #[unstable(feature = "f16", issue = "116909")] #[must_use = "this returns the result of the operation, without modifying the original"] + #[requires(self.is_finite() && float_to_int_in_range::(self))] pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt, diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 15452a7a508fc..cea05a55a7cda 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -2185,4 +2185,34 @@ mod verify { u128, checked_f64_to_int_unchecked_u128, usize, checked_f64_to_int_unchecked_usize ); + + generate_to_int_unchecked_harness!(f16, + i8, checked_f16_to_int_unchecked_i8, + i16, checked_f16_to_int_unchecked_i16, + i32, checked_f16_to_int_unchecked_i32, + i64, checked_f16_to_int_unchecked_i64, + i128, checked_f16_to_int_unchecked_i128, + isize, checked_f16_to_int_unchecked_isize, + u8, checked_f16_to_int_unchecked_u8, + u16, checked_f16_to_int_unchecked_u16, + u32, checked_f16_to_int_unchecked_u32, + u64, checked_f16_to_int_unchecked_u64, + u128, checked_f16_to_int_unchecked_u128, + usize, checked_f16_to_int_unchecked_usize + ); + + generate_to_int_unchecked_harness!(f128, + i8, checked_f128_to_int_unchecked_i8, + i16, checked_f128_to_int_unchecked_i16, + i32, checked_f128_to_int_unchecked_i32, + i64, checked_f128_to_int_unchecked_i64, + i128, checked_f128_to_int_unchecked_i128, + isize, checked_f128_to_int_unchecked_isize, + u8, checked_f128_to_int_unchecked_u8, + u16, checked_f128_to_int_unchecked_u16, + u32, checked_f128_to_int_unchecked_u32, + u64, checked_f128_to_int_unchecked_u64, + u128, checked_f128_to_int_unchecked_u128, + usize, checked_f128_to_int_unchecked_usize + ); } From dd7522549d3f8f683a943155680c92c477d52994 Mon Sep 17 00:00:00 2001 From: stogaru <143449212+stogaru@users.noreply.github.com> Date: Thu, 5 Dec 2024 09:28:34 -0800 Subject: [PATCH 03/14] Contract and Harnesses for `byte_add`, `byte_sub` and `byte_offset` (#169) Towards https://github.com/model-checking/verify-rust-std/issues/76 ### Changes * Adds contracts for `<*mut T>::byte_add`, `<*mut T>::byte_sub` and `<*mut T>::byte_offset`. * Adds harnesses for the function verifying the following pointee types: * All integer types * Tuples (composite types) * Unit Type * Slices * Accomplishes this using a few macros. 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: Yifei Wang <40480373+xsxszab@users.noreply.github.com> Co-authored-by: Yifei Wang <1277495324@qq.com> --- library/core/src/ptr/const_ptr.rs | 304 +++++++++++++++++++++++++++++- library/core/src/ptr/mut_ptr.rs | 294 +++++++++++++++++++++++++++++ 2 files changed, 597 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index ec67d891686fd..a210821f08d10 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -7,6 +7,7 @@ use safety::{ensures, requires}; #[cfg(kani)] use crate::kani; +use core::mem; impl *const T { /// Returns `true` if the pointer is null. @@ -474,6 +475,20 @@ 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( + // If count is zero, any pointer is valid including null pointer. + (count == 0) || + // Else if count is not zero, then ensure that adding `count` doesn't cause + // overflow and that both pointers `self` and the result are in the same + // allocation + ((self.addr() as isize).checked_add(count).is_some() && + core::ub_checks::same_allocation(self, self.wrapping_byte_offset(count))) + )] + #[ensures(|&result| + // The resulting pointer should either be unchanged or still point to the same allocation + (self.addr() == result.addr()) || + (core::ub_checks::same_allocation(self, result)) + )] pub const unsafe fn byte_offset(self, count: isize) -> Self { // SAFETY: the caller must uphold the safety contract for `offset`. unsafe { self.cast::().offset(count).with_metadata_of(self) } @@ -1012,6 +1027,20 @@ 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( + // If count is zero, any pointer is valid including null pointer. + (count == 0) || + // Else if count is not zero, then ensure that adding `count` doesn't cause + // overflow and that both pointers `self` and the result are in the same + // allocation + ((self.addr() as isize).checked_add(count as isize).is_some() && + core::ub_checks::same_allocation(self, self.wrapping_byte_add(count))) + )] + #[ensures(|&result| + // The resulting pointer should either be unchanged or still point to the same allocation + (self.addr() == result.addr()) || + (core::ub_checks::same_allocation(self, result)) + )] pub const unsafe fn byte_add(self, count: usize) -> Self { // SAFETY: the caller must uphold the safety contract for `add`. unsafe { self.cast::().add(count).with_metadata_of(self) } @@ -1142,6 +1171,20 @@ 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( + // If count is zero, any pointer is valid including null pointer. + (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 + ((self.addr() as isize).checked_sub(count as isize).is_some() && + core::ub_checks::same_allocation(self, self.wrapping_byte_sub(count))) + )] + #[ensures(|&result| + // The resulting pointer should either be unchanged or still point to the same allocation + (self.addr() == result.addr()) || + (core::ub_checks::same_allocation(self, result)) + )] pub const unsafe fn byte_sub(self, count: usize) -> Self { // SAFETY: the caller must uphold the safety contract for `sub`. unsafe { self.cast::().sub(count).with_metadata_of(self) } @@ -2068,7 +2111,9 @@ mod verify { check_const_offset_slice_tuple_4 ); - // Array size bound for kani::any_array for `offset_from` verification + // 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 { @@ -2206,4 +2251,261 @@ mod verify { check_const_offset_from_tuple_4, check_const_offset_from_tuple_4_arr ); + + #[kani::proof_for_contract(<*const ()>::byte_offset)] + #[kani::should_panic] + pub fn check_const_byte_offset_unit_invalid_count() { + let val = (); + let ptr: *const () = &val; + let count: isize = kani::any_where(|&x| x != (mem::size_of::<()>() as isize)); + unsafe { + ptr.byte_offset(count); + } + } + + #[kani::proof_for_contract(<*const ()>::byte_offset)] + pub fn check_const_byte_offset_cast_unit() { + let mut generator = PointerGenerator::::new(); + let ptr: *const u8 = generator.any_in_bounds().ptr; + let ptr1: *const () = ptr as *const (); + let count: isize = kani::any(); + unsafe { + ptr1.byte_offset(count); + } + } + + // generate proof for contracts of byte_add, byte_sub and byte_offset to verify + // unit pointee type + // - `$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_unit { + (byte_offset, $proof_name:ident) => { + #[kani::proof_for_contract(<*const ()>::byte_offset)] + pub fn $proof_name() { + let val = (); + let ptr: *const () = &val; + let count: isize = mem::size_of::<()>() as isize; + unsafe { + ptr.byte_offset(count); + } + } + }; + + ($fn_name:ident, $proof_name:ident) => { + #[kani::proof_for_contract(<*const ()>::$fn_name)] + pub fn $proof_name() { + let val = (); + let ptr: *const () = &val; + //byte_add and byte_sub need count to be usize unlike byte_offset + let count: usize = mem::size_of::<()>(); + unsafe { + ptr.$fn_name(count); + } + } + }; + } + + gen_const_byte_arith_harness_for_unit!(byte_add, check_const_byte_add_unit); + gen_const_byte_arith_harness_for_unit!(byte_sub, check_const_byte_sub_unit); + gen_const_byte_arith_harness_for_unit!(byte_offset, check_const_byte_offset_unit); + + // generate proof for contracts for byte_add, byte_sub and byte_offset + // - `$type`: pointee type + // - `$fn_name`: function for which the contract must be verified + // - `$proof_name`: name of the harness generated + macro_rules! gen_const_byte_arith_harness { + ($type:ty, byte_offset, $proof_name:ident) => { + #[kani::proof_for_contract(<*const $type>::byte_offset)] + pub fn $proof_name() { + // generator with space for single element + let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new(); + // generator with space for multiple elements + let mut generator2 = + PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new(); + + let ptr: *const $type = if kani::any() { + generator1.any_in_bounds().ptr + } else { + generator2.any_in_bounds().ptr + }; + + let count: isize = kani::any(); + + unsafe { + ptr.byte_offset(count); + } + } + }; + + ($type:ty, $fn_name:ident, $proof_name:ident) => { + #[kani::proof_for_contract(<*const $type>::$fn_name)] + pub fn $proof_name() { + // generator with space for single element + let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new(); + // generator with space for multiple elements + let mut generator2 = + PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new(); + + let ptr: *const $type = if kani::any() { + generator1.any_in_bounds().ptr + } else { + generator2.any_in_bounds().ptr + }; + + //byte_add and byte_sub need count to be usize unlike byte_offset + let count: usize = kani::any(); + + unsafe { + ptr.$fn_name(count); + } + } + }; + } + + gen_const_byte_arith_harness!(i8, byte_add, check_const_byte_add_i8); + gen_const_byte_arith_harness!(i16, byte_add, check_const_byte_add_i16); + gen_const_byte_arith_harness!(i32, byte_add, check_const_byte_add_i32); + gen_const_byte_arith_harness!(i64, byte_add, check_const_byte_add_i64); + gen_const_byte_arith_harness!(i128, byte_add, check_const_byte_add_i128); + gen_const_byte_arith_harness!(isize, byte_add, check_const_byte_add_isize); + gen_const_byte_arith_harness!(u8, byte_add, check_const_byte_add_u8); + gen_const_byte_arith_harness!(u16, byte_add, check_const_byte_add_u16); + gen_const_byte_arith_harness!(u32, byte_add, check_const_byte_add_u32); + gen_const_byte_arith_harness!(u64, byte_add, check_const_byte_add_u64); + gen_const_byte_arith_harness!(u128, byte_add, check_const_byte_add_u128); + gen_const_byte_arith_harness!(usize, byte_add, check_const_byte_add_usize); + gen_const_byte_arith_harness!((i8, i8), byte_add, check_const_byte_add_tuple_1); + gen_const_byte_arith_harness!((f64, bool), byte_add, check_const_byte_add_tuple_2); + gen_const_byte_arith_harness!((i32, f64, bool), byte_add, check_const_byte_add_tuple_3); + gen_const_byte_arith_harness!( + (i8, u16, i32, u64, isize), + byte_add, + check_const_byte_add_tuple_4 + ); + + gen_const_byte_arith_harness!(i8, byte_sub, check_const_byte_sub_i8); + gen_const_byte_arith_harness!(i16, byte_sub, check_const_byte_sub_i16); + gen_const_byte_arith_harness!(i32, byte_sub, check_const_byte_sub_i32); + gen_const_byte_arith_harness!(i64, byte_sub, check_const_byte_sub_i64); + gen_const_byte_arith_harness!(i128, byte_sub, check_const_byte_sub_i128); + gen_const_byte_arith_harness!(isize, byte_sub, check_const_byte_sub_isize); + gen_const_byte_arith_harness!(u8, byte_sub, check_const_byte_sub_u8); + gen_const_byte_arith_harness!(u16, byte_sub, check_const_byte_sub_u16); + gen_const_byte_arith_harness!(u32, byte_sub, check_const_byte_sub_u32); + gen_const_byte_arith_harness!(u64, byte_sub, check_const_byte_sub_u64); + gen_const_byte_arith_harness!(u128, byte_sub, check_const_byte_sub_u128); + gen_const_byte_arith_harness!(usize, byte_sub, check_const_byte_sub_usize); + gen_const_byte_arith_harness!((i8, i8), byte_sub, check_const_byte_sub_tuple_1); + gen_const_byte_arith_harness!((f64, bool), byte_sub, check_const_byte_sub_tuple_2); + gen_const_byte_arith_harness!((i32, f64, bool), byte_sub, check_const_byte_sub_tuple_3); + gen_const_byte_arith_harness!( + (i8, u16, i32, u64, isize), + byte_sub, + check_const_byte_sub_tuple_4 + ); + + gen_const_byte_arith_harness!(i8, byte_offset, check_const_byte_offset_i8); + gen_const_byte_arith_harness!(i16, byte_offset, check_const_byte_offset_i16); + gen_const_byte_arith_harness!(i32, byte_offset, check_const_byte_offset_i32); + gen_const_byte_arith_harness!(i64, byte_offset, check_const_byte_offset_i64); + gen_const_byte_arith_harness!(i128, byte_offset, check_const_byte_offset_i128); + gen_const_byte_arith_harness!(isize, byte_offset, check_const_byte_offset_isize); + gen_const_byte_arith_harness!(u8, byte_offset, check_const_byte_offset_u8); + gen_const_byte_arith_harness!(u16, byte_offset, check_const_byte_offset_u16); + gen_const_byte_arith_harness!(u32, byte_offset, check_const_byte_offset_u32); + gen_const_byte_arith_harness!(u64, byte_offset, check_const_byte_offset_u64); + gen_const_byte_arith_harness!(u128, byte_offset, check_const_byte_offset_u128); + gen_const_byte_arith_harness!(usize, byte_offset, check_const_byte_offset_usize); + gen_const_byte_arith_harness!((i8, i8), byte_offset, check_const_byte_offset_tuple_1); + gen_const_byte_arith_harness!((f64, bool), byte_offset, check_const_byte_offset_tuple_2); + gen_const_byte_arith_harness!( + (i32, f64, bool), + byte_offset, + check_const_byte_offset_tuple_3 + ); + gen_const_byte_arith_harness!( + (i8, u16, i32, u64, isize), + byte_offset, + check_const_byte_offset_tuple_4 + ); + + macro_rules! gen_const_byte_arith_harness_for_slice { + ($type:ty, byte_offset, $proof_name:ident) => { + #[kani::proof_for_contract(<*const [$type]>::byte_offset)] + pub fn $proof_name() { + let arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array(); + let slice: &[$type] = kani::slice::any_slice_of_array(&arr); + let ptr: *const [$type] = slice; + + let count: isize = kani::any(); + + unsafe { + ptr.byte_offset(count); + } + } + }; + + ($type:ty, $fn_name: ident, $proof_name:ident) => { + #[kani::proof_for_contract(<*const [$type]>::$fn_name)] + pub fn $proof_name() { + let arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array(); + let slice: &[$type] = kani::slice::any_slice_of_array(&arr); + let ptr: *const [$type] = slice; + + //byte_add and byte_sub need count to be usize unlike byte_offset + let count: usize = kani::any(); + + unsafe { + ptr.$fn_name(count); + } + } + }; + } + + gen_const_byte_arith_harness_for_slice!(i8, byte_add, check_const_byte_add_i8_slice); + gen_const_byte_arith_harness_for_slice!(i16, byte_add, check_const_byte_add_i16_slice); + gen_const_byte_arith_harness_for_slice!(i32, byte_add, check_const_byte_add_i32_slice); + gen_const_byte_arith_harness_for_slice!(i64, byte_add, check_const_byte_add_i64_slice); + gen_const_byte_arith_harness_for_slice!(i128, byte_add, check_const_byte_add_i128_slice); + gen_const_byte_arith_harness_for_slice!(isize, byte_add, check_const_byte_add_isize_slice); + gen_const_byte_arith_harness_for_slice!(u8, byte_add, check_const_byte_add_u8_slice); + gen_const_byte_arith_harness_for_slice!(u16, byte_add, check_const_byte_add_u16_slice); + gen_const_byte_arith_harness_for_slice!(u32, byte_add, check_const_byte_add_u32_slice); + gen_const_byte_arith_harness_for_slice!(u64, byte_add, check_const_byte_add_u64_slice); + gen_const_byte_arith_harness_for_slice!(u128, byte_add, check_const_byte_add_u128_slice); + gen_const_byte_arith_harness_for_slice!(usize, byte_add, check_const_byte_add_usize_slice); + + gen_const_byte_arith_harness_for_slice!(i8, byte_sub, check_const_byte_sub_i8_slice); + gen_const_byte_arith_harness_for_slice!(i16, byte_sub, check_const_byte_sub_i16_slice); + gen_const_byte_arith_harness_for_slice!(i32, byte_sub, check_const_byte_sub_i32_slice); + gen_const_byte_arith_harness_for_slice!(i64, byte_sub, check_const_byte_sub_i64_slice); + gen_const_byte_arith_harness_for_slice!(i128, byte_sub, check_const_byte_sub_i128_slice); + gen_const_byte_arith_harness_for_slice!(isize, byte_sub, check_const_byte_sub_isize_slice); + gen_const_byte_arith_harness_for_slice!(u8, byte_sub, check_const_byte_sub_u8_slice); + gen_const_byte_arith_harness_for_slice!(u16, byte_sub, check_const_byte_sub_u16_slice); + gen_const_byte_arith_harness_for_slice!(u32, byte_sub, check_const_byte_sub_u32_slice); + gen_const_byte_arith_harness_for_slice!(u64, byte_sub, check_const_byte_sub_u64_slice); + gen_const_byte_arith_harness_for_slice!(u128, byte_sub, check_const_byte_sub_u128_slice); + gen_const_byte_arith_harness_for_slice!(usize, byte_sub, check_const_byte_sub_usize_slice); + + gen_const_byte_arith_harness_for_slice!(i8, byte_offset, check_const_byte_offset_i8_slice); + gen_const_byte_arith_harness_for_slice!(i16, byte_offset, check_const_byte_offset_i16_slice); + gen_const_byte_arith_harness_for_slice!(i32, byte_offset, check_const_byte_offset_i32_slice); + gen_const_byte_arith_harness_for_slice!(i64, byte_offset, check_const_byte_offset_i64_slice); + gen_const_byte_arith_harness_for_slice!(i128, byte_offset, check_const_byte_offset_i128_slice); + gen_const_byte_arith_harness_for_slice!( + isize, + byte_offset, + check_const_byte_offset_isize_slice + ); + gen_const_byte_arith_harness_for_slice!(u8, byte_offset, check_const_byte_offset_u8_slice); + gen_const_byte_arith_harness_for_slice!(u16, byte_offset, check_const_byte_offset_u16_slice); + gen_const_byte_arith_harness_for_slice!(u32, byte_offset, check_const_byte_offset_u32_slice); + gen_const_byte_arith_harness_for_slice!(u64, byte_offset, check_const_byte_offset_u64_slice); + gen_const_byte_arith_harness_for_slice!(u128, byte_offset, check_const_byte_offset_u128_slice); + gen_const_byte_arith_harness_for_slice!( + usize, + byte_offset, + check_const_byte_offset_usize_slice + ); } diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 2bfa76a29ab05..aea2df07f19cb 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -7,6 +7,7 @@ use safety::{ensures, requires}; #[cfg(kani)] use crate::kani; +use core::mem; impl *mut T { /// Returns `true` if the pointer is null. @@ -474,6 +475,20 @@ 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( + // If count is zero, any pointer is valid including null pointer. + (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 + ((self.addr() as isize).checked_add(count).is_some() && + core::ub_checks::same_allocation(self, self.wrapping_byte_offset(count))) + )] + #[ensures(|&result| + // The resulting pointer should either be unchanged or still point to the same allocation + (self.addr() == result.addr()) || + (core::ub_checks::same_allocation(self, result)) + )] pub const unsafe fn byte_offset(self, count: isize) -> Self { // SAFETY: the caller must uphold the safety contract for `offset`. unsafe { self.cast::().offset(count).with_metadata_of(self) } @@ -1085,6 +1100,20 @@ 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( + // If count is zero, any pointer is valid including null pointer. + (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 + ((self.addr() as isize).checked_add(count as isize).is_some() && + core::ub_checks::same_allocation(self, self.wrapping_byte_add(count))) + )] + #[ensures(|&result| + // The resulting pointer should either be unchanged or still point to the same allocation + (self.addr() == result.addr()) || + (core::ub_checks::same_allocation(self, result)) + )] pub const unsafe fn byte_add(self, count: usize) -> Self { // SAFETY: the caller must uphold the safety contract for `add`. unsafe { self.cast::().add(count).with_metadata_of(self) } @@ -1217,6 +1246,20 @@ 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( + // If count is zero, any pointer is valid including null pointer. + (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 + ((self.addr() as isize).checked_sub(count as isize).is_some() && + core::ub_checks::same_allocation(self, self.wrapping_byte_sub(count))) + )] + #[ensures(|&result| + // The resulting pointer should either be unchanged or still point to the same allocation + (self.addr() == result.addr()) || + (core::ub_checks::same_allocation(self, result)) + )] pub const unsafe fn byte_sub(self, count: usize) -> Self { // SAFETY: the caller must uphold the safety contract for `sub`. unsafe { self.cast::().sub(count).with_metadata_of(self) } @@ -2177,6 +2220,257 @@ impl PartialOrd for *mut T { #[unstable(feature = "kani", issue = "none")] mod verify { use crate::kani; + 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 does not support dynamic sized arrays. + const ARRAY_LEN: usize = 40; + + #[kani::proof_for_contract(<*mut ()>::byte_offset)] + #[kani::should_panic] + pub fn check_mut_byte_offset_unit_invalid_count() { + let mut val = (); + let ptr: *mut () = &mut val; + let count: isize = kani::any_where(|&x| x > (mem::size_of::<()>() as isize)); + unsafe { + ptr.byte_offset(count); + } + } + + #[kani::proof_for_contract(<*mut ()>::byte_offset)] + pub fn check_mut_byte_offset_cast_unit() { + let mut generator = PointerGenerator::::new(); + let ptr: *mut u8 = generator.any_in_bounds().ptr; + let ptr1: *mut () = ptr as *mut (); + let count: isize = kani::any(); + unsafe { + ptr1.byte_offset(count); + } + } + + // generate proof for contracts of byte_add, byte_sub and byte_offset to verify + // 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 { + (byte_offset, $proof_name:ident) => { + #[kani::proof_for_contract(<*mut ()>::byte_offset)] + pub fn $proof_name() { + let mut val = (); + let ptr: *mut () = &mut val; + let count: isize = mem::size_of::<()>() as isize; + unsafe { + ptr.byte_offset(count); + } + } + }; + + ($fn_name:ident, $proof_name:ident) => { + #[kani::proof_for_contract(<*mut ()>::$fn_name)] + pub fn $proof_name() { + let mut val = (); + let ptr: *mut () = &mut val; + //byte_add and byte_sub need count to be usize unlike byte_offset + let count: usize = mem::size_of::<()>(); + unsafe { + ptr.$fn_name(count); + } + } + }; + } + + gen_mut_byte_arith_harness_for_unit!(byte_add, check_mut_byte_add_unit); + gen_mut_byte_arith_harness_for_unit!(byte_sub, check_mut_byte_sub_unit); + gen_mut_byte_arith_harness_for_unit!(byte_offset, check_mut_byte_offset_unit); + + // generate proof for contracts for byte_add, byte_sub and byte_offset + // - `$type`: 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 { + ($type:ty, byte_offset, $proof_name:ident) => { + #[kani::proof_for_contract(<*mut $type>::byte_offset)] + pub fn $proof_name() { + // generator with space for single element + let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new(); + // generator with space for multiple elements + let mut generator2 = + PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new(); + + let ptr: *mut $type = if kani::any() { + generator1.any_in_bounds().ptr + } else { + generator2.any_in_bounds().ptr + }; + let count: isize = kani::any(); + + unsafe { + ptr.byte_offset(count); + } + } + }; + + ($type:ty, $fn_name:ident, $proof_name:ident) => { + #[kani::proof_for_contract(<*mut $type>::$fn_name)] + pub fn $proof_name() { + // generator with space for single element + let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new(); + // generator with space for multiple elements + let mut generator2 = + PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new(); + + let ptr: *mut $type = if kani::any() { + generator1.any_in_bounds().ptr + } else { + generator2.any_in_bounds().ptr + }; + + //byte_add and byte_sub need count to be usize unlike byte_offset + let count: usize = kani::any(); + + unsafe { + ptr.$fn_name(count); + } + } + }; + } + + gen_mut_byte_arith_harness!(i8, byte_add, check_mut_byte_add_i8); + gen_mut_byte_arith_harness!(i16, byte_add, check_mut_byte_add_i16); + gen_mut_byte_arith_harness!(i32, byte_add, check_mut_byte_add_i32); + gen_mut_byte_arith_harness!(i64, byte_add, check_mut_byte_add_i64); + gen_mut_byte_arith_harness!(i128, byte_add, check_mut_byte_add_i128); + gen_mut_byte_arith_harness!(isize, byte_add, check_mut_byte_add_isize); + gen_mut_byte_arith_harness!(u8, byte_add, check_mut_byte_add_u8); + gen_mut_byte_arith_harness!(u16, byte_add, check_mut_byte_add_u16); + gen_mut_byte_arith_harness!(u32, byte_add, check_mut_byte_add_u32); + gen_mut_byte_arith_harness!(u64, byte_add, check_mut_byte_add_u64); + gen_mut_byte_arith_harness!(u128, byte_add, check_mut_byte_add_u128); + gen_mut_byte_arith_harness!(usize, byte_add, check_mut_byte_add_usize); + gen_mut_byte_arith_harness!((i8, i8), byte_add, check_mut_byte_add_tuple_1); + gen_mut_byte_arith_harness!((f64, bool), byte_add, check_mut_byte_add_tuple_2); + gen_mut_byte_arith_harness!((i32, f64, bool), byte_add, check_mut_byte_add_tuple_3); + gen_mut_byte_arith_harness!( + (i8, u16, i32, u64, isize), + byte_add, + check_mut_byte_add_tuple_4 + ); + + gen_mut_byte_arith_harness!(i8, byte_sub, check_mut_byte_sub_i8); + gen_mut_byte_arith_harness!(i16, byte_sub, check_mut_byte_sub_i16); + gen_mut_byte_arith_harness!(i32, byte_sub, check_mut_byte_sub_i32); + gen_mut_byte_arith_harness!(i64, byte_sub, check_mut_byte_sub_i64); + gen_mut_byte_arith_harness!(i128, byte_sub, check_mut_byte_sub_i128); + gen_mut_byte_arith_harness!(isize, byte_sub, check_mut_byte_sub_isize); + gen_mut_byte_arith_harness!(u8, byte_sub, check_mut_byte_sub_u8); + gen_mut_byte_arith_harness!(u16, byte_sub, check_mut_byte_sub_u16); + gen_mut_byte_arith_harness!(u32, byte_sub, check_mut_byte_sub_u32); + gen_mut_byte_arith_harness!(u64, byte_sub, check_mut_byte_sub_u64); + gen_mut_byte_arith_harness!(u128, byte_sub, check_mut_byte_sub_u128); + gen_mut_byte_arith_harness!(usize, byte_sub, check_mut_byte_sub_usize); + gen_mut_byte_arith_harness!((i8, i8), byte_sub, check_mut_byte_sub_tuple_1); + gen_mut_byte_arith_harness!((f64, bool), byte_sub, check_mut_byte_sub_tuple_2); + gen_mut_byte_arith_harness!((i32, f64, bool), byte_sub, check_mut_byte_sub_tuple_3); + gen_mut_byte_arith_harness!( + (i8, u16, i32, u64, isize), + byte_sub, + check_mut_byte_sub_tuple_4 + ); + + gen_mut_byte_arith_harness!(i8, byte_offset, check_mut_byte_offset_i8); + gen_mut_byte_arith_harness!(i16, byte_offset, check_mut_byte_offset_i16); + gen_mut_byte_arith_harness!(i32, byte_offset, check_mut_byte_offset_i32); + gen_mut_byte_arith_harness!(i64, byte_offset, check_mut_byte_offset_i64); + gen_mut_byte_arith_harness!(i128, byte_offset, check_mut_byte_offset_i128); + gen_mut_byte_arith_harness!(isize, byte_offset, check_mut_byte_offset_isize); + gen_mut_byte_arith_harness!(u8, byte_offset, check_mut_byte_offset_u8); + gen_mut_byte_arith_harness!(u16, byte_offset, check_mut_byte_offset_u16); + gen_mut_byte_arith_harness!(u32, byte_offset, check_mut_byte_offset_u32); + gen_mut_byte_arith_harness!(u64, byte_offset, check_mut_byte_offset_u64); + gen_mut_byte_arith_harness!(u128, byte_offset, check_mut_byte_offset_u128); + gen_mut_byte_arith_harness!(usize, byte_offset, check_mut_byte_offset_usize); + gen_mut_byte_arith_harness!((i8, i8), byte_offset, check_mut_byte_offset_tuple_1); + gen_mut_byte_arith_harness!((f64, bool), byte_offset, check_mut_byte_offset_tuple_2); + gen_mut_byte_arith_harness!((i32, f64, bool), byte_offset, check_mut_byte_offset_tuple_3); + gen_mut_byte_arith_harness!( + (i8, u16, i32, u64, isize), + byte_offset, + check_mut_byte_offset_tuple_4 + ); + + macro_rules! gen_mut_byte_arith_harness_for_slice { + ($type:ty, byte_offset, $proof_name:ident) => { + #[kani::proof_for_contract(<*mut [$type]>::byte_offset)] + pub fn $proof_name() { + let mut arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array(); + let slice: &mut [$type] = kani::slice::any_slice_of_array_mut(&mut arr); + let ptr: *mut [$type] = slice; + + let count: isize = kani::any(); + + unsafe { + ptr.byte_offset(count); + } + } + }; + + ($type:ty, $fn_name: ident, $proof_name:ident) => { + #[kani::proof_for_contract(<*mut [$type]>::$fn_name)] + pub fn $proof_name() { + let mut arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array(); + let slice: &mut [$type] = kani::slice::any_slice_of_array_mut(&mut arr); + let ptr: *mut [$type] = slice; + + //byte_add and byte_sub need count to be usize unlike byte_offset + let count: usize = kani::any(); + + unsafe { + ptr.$fn_name(count); + } + } + }; + } + + gen_mut_byte_arith_harness_for_slice!(i8, byte_add, check_mut_byte_add_i8_slice); + gen_mut_byte_arith_harness_for_slice!(i16, byte_add, check_mut_byte_add_i16_slice); + gen_mut_byte_arith_harness_for_slice!(i32, byte_add, check_mut_byte_add_i32_slice); + gen_mut_byte_arith_harness_for_slice!(i64, byte_add, check_mut_byte_add_i64_slice); + gen_mut_byte_arith_harness_for_slice!(i128, byte_add, check_mut_byte_add_i128_slice); + gen_mut_byte_arith_harness_for_slice!(isize, byte_add, check_mut_byte_add_isize_slice); + gen_mut_byte_arith_harness_for_slice!(u8, byte_add, check_mut_byte_add_u8_slice); + gen_mut_byte_arith_harness_for_slice!(u16, byte_add, check_mut_byte_add_u16_slice); + gen_mut_byte_arith_harness_for_slice!(u32, byte_add, check_mut_byte_add_u32_slice); + gen_mut_byte_arith_harness_for_slice!(u64, byte_add, check_mut_byte_add_u64_slice); + gen_mut_byte_arith_harness_for_slice!(u128, byte_add, check_mut_byte_add_u128_slice); + gen_mut_byte_arith_harness_for_slice!(usize, byte_add, check_mut_byte_add_usize_slice); + + gen_mut_byte_arith_harness_for_slice!(i8, byte_sub, check_mut_byte_sub_i8_slice); + gen_mut_byte_arith_harness_for_slice!(i16, byte_sub, check_mut_byte_sub_i16_slice); + gen_mut_byte_arith_harness_for_slice!(i32, byte_sub, check_mut_byte_sub_i32_slice); + gen_mut_byte_arith_harness_for_slice!(i64, byte_sub, check_mut_byte_sub_i64_slice); + gen_mut_byte_arith_harness_for_slice!(i128, byte_sub, check_mut_byte_sub_i128_slice); + gen_mut_byte_arith_harness_for_slice!(isize, byte_sub, check_mut_byte_sub_isize_slice); + gen_mut_byte_arith_harness_for_slice!(u8, byte_sub, check_mut_byte_sub_u8_slice); + gen_mut_byte_arith_harness_for_slice!(u16, byte_sub, check_mut_byte_sub_u16_slice); + gen_mut_byte_arith_harness_for_slice!(u32, byte_sub, check_mut_byte_sub_u32_slice); + gen_mut_byte_arith_harness_for_slice!(u64, byte_sub, check_mut_byte_sub_u64_slice); + gen_mut_byte_arith_harness_for_slice!(u128, byte_sub, check_mut_byte_sub_u128_slice); + gen_mut_byte_arith_harness_for_slice!(usize, byte_sub, check_mut_byte_sub_usize_slice); + + gen_mut_byte_arith_harness_for_slice!(i8, byte_offset, check_mut_byte_offset_i8_slice); + gen_mut_byte_arith_harness_for_slice!(i16, byte_offset, check_mut_byte_offset_i16_slice); + gen_mut_byte_arith_harness_for_slice!(i32, byte_offset, check_mut_byte_offset_i32_slice); + gen_mut_byte_arith_harness_for_slice!(i64, byte_offset, check_mut_byte_offset_i64_slice); + gen_mut_byte_arith_harness_for_slice!(i128, byte_offset, check_mut_byte_offset_i128_slice); + gen_mut_byte_arith_harness_for_slice!(isize, byte_offset, check_mut_byte_offset_isize_slice); + gen_mut_byte_arith_harness_for_slice!(u8, byte_offset, check_mut_byte_offset_u8_slice); + gen_mut_byte_arith_harness_for_slice!(u16, byte_offset, check_mut_byte_offset_u16_slice); + gen_mut_byte_arith_harness_for_slice!(u32, byte_offset, check_mut_byte_offset_u32_slice); + gen_mut_byte_arith_harness_for_slice!(u64, byte_offset, check_mut_byte_offset_u64_slice); + 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); /// This macro generates a single verification harness for the `offset`, `add`, or `sub` /// pointer operations, supporting integer, composite, or unit types. From a52b65ab8fc304f06b3ac57383b025b1f619762a Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 <60180388+MayureshJoshi25@users.noreply.github.com> Date: Thu, 5 Dec 2024 14:42:59 -0800 Subject: [PATCH 04/14] Contracts and harnesses for <*mut T>::offset_from (#168) - Added contracts for offset_from (mut type); - Accomplished using a macro which generates harnesses; - Verifies: int types, unit, tuples (composite types). Towards #76 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: stogaru <143449212+stogaru@users.noreply.github.com> Co-authored-by: Carolyn Zech Co-authored-by: Felipe R. Monteiro --- library/core/src/ptr/mut_ptr.rs | 207 ++++++++++++-------------------- 1 file changed, 77 insertions(+), 130 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index aea2df07f19cb..fd7e4d80e676d 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -857,11 +857,22 @@ impl *mut T { /// unsafe { /// let one = ptr2_other.offset_from(ptr2); // Undefined Behavior! ⚠️ /// } + /// + /// /// ``` #[stable(feature = "ptr_offset_from", since = "1.47.0")] #[rustc_const_stable(feature = "const_ptr_offset_from", since = "1.65.0")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires( + // Ensuring that subtracting 'origin' from 'self' doesn't result in an overflow + (self as isize).checked_sub(origin as isize).is_some() && + // Ensuring that the distance between 'self' and 'origin' is aligned to `T` + (self as isize - origin as isize) % (mem::size_of::() as isize) == 0 && + // Ensuring that both pointers point to the same address or are in the same allocation + (self as isize == origin as isize || core::ub_checks::same_allocation(self, origin)) + )] + #[ensures(|result| *result == (self as isize - origin as isize) / (mem::size_of::() as isize))] pub const unsafe fn offset_from(self, origin: *const T) -> isize where T: Sized, @@ -2472,143 +2483,79 @@ 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); - /// 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(); + // 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); + } + } + + macro_rules! generate_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 + 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 { - test_ptr.$fn_name(count); + ptr1.offset_from(ptr2); + } + } + + // 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(); + 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.offset_from(ptr2); } } - }; - } - /// 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 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 + 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_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!( + ((), bool, u8, u16, i32, f64, i128, usize), + check_mut_offset_from_tuple_4, + check_mut_offset_from_tuple_4_array ); - // 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 - ); } From bed3267b5f87e1f12676d1555ee51409460e65ab Mon Sep 17 00:00:00 2001 From: Reinier Maas Date: Fri, 6 Dec 2024 08:03:38 +0100 Subject: [PATCH 05/14] Update 0003-pointer-arithmentic.md (#210) --- doc/src/challenges/0003-pointer-arithmentic.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0003-pointer-arithmentic.md b/doc/src/challenges/0003-pointer-arithmentic.md index 902d3a7f55752..b85c4f45e1a78 100644 --- a/doc/src/challenges/0003-pointer-arithmentic.md +++ b/doc/src/challenges/0003-pointer-arithmentic.md @@ -88,7 +88,7 @@ At least 3 of the following usages were proven safe: | Function | Location | |-------------------|---------------| -| \[u8\]::is_asc_ii | core::slice | +| \[u8\]::is_ascii | core::slice | | String::remove | alloc::string | | Vec::swap_remove | alloc::vec | | Option::as_slice | core::option | From e70a892165226dfc06abe2bc9b4473501e223928 Mon Sep 17 00:00:00 2001 From: Yenyun035 <57857379+Yenyun035@users.noreply.github.com> Date: Fri, 6 Dec 2024 05:41:26 -0800 Subject: [PATCH 06/14] Close Challenge 11 (#206) Resolves #59 ### Changes * Marked Challenge 11 as resolved * Changed the end date of the challenge * Added the contributors --- doc/src/challenges/0011-floats-ints.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0011-floats-ints.md b/doc/src/challenges/0011-floats-ints.md index 1a1c872b88f1f..2d80453e25c3c 100644 --- a/doc/src/challenges/0011-floats-ints.md +++ b/doc/src/challenges/0011-floats-ints.md @@ -1,11 +1,12 @@ # Challenge 11: Safety of Methods for Numeric Primitive Types -- **Status:** Open +- **Status:** Resolved - **Tracking Issue:** [#59](https://github.com/model-checking/verify-rust-std/issues/59) - **Start date:** *2024/08/20* -- **End date:** *2025/04/10* +- **End date:** *2024/12/04* - **Reward:** *N/A* +- **Contributors**: [Rajath M Kotyal](https://github.com/rajathkotyal), [Yen-Yun Wu](https://github.com/Yenyun035), [Lanfei Ma](https://github.com/lanfeima), [Junfeng Jin](https://github.com/MWDZ) ------------------- From eae6c8bc2a4393c0c6704603038b00253c83a118 Mon Sep 17 00:00:00 2001 From: Reinier Maas Date: Fri, 6 Dec 2024 20:57:54 +0100 Subject: [PATCH 07/14] Update tools.md (#207) --- doc/src/tools.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/tools.md b/doc/src/tools.md index 1e86d661ccb2e..0eaba7c40d4d8 100644 --- a/doc/src/tools.md +++ b/doc/src/tools.md @@ -4,7 +4,7 @@ The verification tool ecosystem for Rust is rapidly growing, and we welcome the In this chapter, you can find a list of tools that have already been approved for new solutions, what is their CI current status, as well as more details on how to use them. -If the tool you would like to add a new tool to the list of tool applications, +If you would like to add a new tool to the list of tool applications, please see the [Tool Application](general-rules.md#tool-applications) section. ## Approved tools: From ee9b7c311ab494329382b483e35cec622d7e565e Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 6 Dec 2024 14:30:39 -0800 Subject: [PATCH 08/14] Enable harnesses that were blocked by Kani's spurious CEX (#211) In #148 and #122, we had to comment out a few harnesses due to the issue https://github.com/model-checking/kani/issues/3670. But now that the fix has been pushed, we can enable them. --- library/core/src/slice/iter.rs | 22 ++++++++++++++-------- library/core/src/str/pattern.rs | 5 ----- 2 files changed, 14 insertions(+), 13 deletions(-) diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index 5005563233d2d..5ea9204a28fd0 100644 --- a/library/core/src/slice/iter.rs +++ b/library/core/src/slice/iter.rs @@ -3604,18 +3604,24 @@ mod verify { } check_unsafe_contracts!(check_next_back_unchecked, $ty, next_back_unchecked()); - //check_unsafe_contracts!(check_post_inc_start, $ty, post_inc_start(kani::any())); - //check_unsafe_contracts!(check_pre_dec_end, $ty, pre_dec_end(kani::any())); + check_unsafe_contracts!(check_post_inc_start, $ty, post_inc_start(kani::any())); + check_unsafe_contracts!(check_pre_dec_end, $ty, pre_dec_end(kani::any())); // FIXME: The functions that are commented out are currently failing verification. // Debugging the issue is currently blocked by: // https://github.com/model-checking/kani/issues/3670 // // Public functions that call safe abstraction `make_slice`. - // check_safe_abstraction!(check_as_slice, $ty, as_slice); - // check_safe_abstraction!(check_as_ref, $ty, as_ref); + check_safe_abstraction!(check_as_slice, $ty, |iter: &mut Iter<'_, $ty>| { + iter.as_slice(); + }); + check_safe_abstraction!(check_as_ref, $ty, |iter: &mut Iter<'_, $ty>| { + iter.as_ref(); + }); - // check_safe_abstraction!(check_advance_back_by, $ty, advance_back_by, kani::any()); + check_safe_abstraction!(check_advance_back_by, $ty, |iter: &mut Iter<'_, $ty>| { + iter.advance_back_by(kani::any()); + }); check_safe_abstraction!(check_is_empty, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.is_empty(); @@ -3626,12 +3632,12 @@ mod verify { check_safe_abstraction!(check_size_hint, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.size_hint(); }); - //check_safe_abstraction!(check_nth, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth(kani::any()); }); - //check_safe_abstraction!(check_advance_by, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.advance_by(kani::any()); }); + check_safe_abstraction!(check_nth, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth(kani::any()); }); + check_safe_abstraction!(check_advance_by, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.advance_by(kani::any()); }); check_safe_abstraction!(check_next_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.next_back(); }); - //check_safe_abstraction!(check_nth_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth_back(kani::any()); }); + check_safe_abstraction!(check_nth_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth_back(kani::any()); }); check_safe_abstraction!(check_next, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.next(); }); diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index 7792bfbbac718..6540608344fa1 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -2000,10 +2000,6 @@ pub mod verify { } } - /* This harness check `small_slice_eq` with dangling pointer to slice - with zero size. Kani finds safety issue of `small_slice_eq` in this - harness and hence the proof will fail. - #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86 #[kani::proof] #[kani::unwind(4)] @@ -2022,5 +2018,4 @@ pub mod verify { true ); } - */ } From d92a7ea57f9096171354b47b45bd4f6e31baba2a Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 6 Dec 2024 17:44:00 -0800 Subject: [PATCH 09/14] 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 10/14] 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 11/14] 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 12/14] 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: From 16a155ab1091009e8c271b26b588314f8662e140 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 9 Dec 2024 23:43:35 -0500 Subject: [PATCH 13/14] Kani Workflow Updates (#214) Update the `kani list` part of our workflow to: - Be its own step of the workflow so it can run in parallel, which is nice because it finishes much faster than the other jobs in the Kani workflow - Use the new markdown format. This makes the list much more readable (compare [current format](https://github.com/model-checking/verify-rust-std/actions/runs/12199714877/attempts/2#summary-34034201022) to [markdown format](https://github.com/carolynzech/verify-rust-std/actions/runs/12203155221/attempts/1#summary-34045490103)). Also remove the Test Kani workflow step, because it's expensive and duplicates verification work. --- .github/workflows/kani.yml | 37 +++++++++++-------------------------- scripts/run-kani.sh | 2 +- 2 files changed, 12 insertions(+), 27 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 7e0ccfd3551e4..89d9096ec3289 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -38,18 +38,10 @@ jobs: # Step 2: Run Kani on the std library (default configuration) - name: Run Kani Verification run: head/scripts/run-kani.sh --path ${{github.workspace}}/head - - test-kani-script: - name: Test Kani script - runs-on: ${{ matrix.os }} - strategy: - matrix: - os: [ubuntu-latest, macos-latest] - include: - - os: ubuntu-latest - base: ubuntu - - os: macos-latest - base: macos + + run-kani-list: + name: Kani List + runs-on: ubuntu-latest steps: # Step 1: Check out the repository - name: Checkout Repository @@ -58,25 +50,18 @@ jobs: path: head submodules: true - # Step 2: Test Kani verification script with specific arguments - - name: Test Kani script (Custom Args) - run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr --output-format=terse - - # Step 3: Test Kani verification script in the repository directory - - name: Test Kani script (In Repo Directory) - working-directory: ${{github.workspace}}/head - run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse - - # Step 4: Run list on the std library and add output to job summary + # Step 2: Run list on the std library - name: Run Kani List run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head - + + # Step 3: Add output to job summary - name: Add Kani List output to job summary uses: actions/github-script@v6 with: script: | const fs = require('fs'); - const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani_list.txt', 'utf8'); + const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani-list.md', 'utf8'); await core.summary - .addRaw(kaniOutput) - .write(); \ No newline at end of file + .addHeading('Kani List Output', 2) + .addRaw(kaniOutput, false) + .write(); diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index a576717849aca..ceacda86eb2f1 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -221,7 +221,7 @@ main() { --cbmc-args --object-bits 12 elif [[ "$run_command" == "list" ]]; then echo "Running Kani list command..." - "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib ./library --std > $path/kani_list.txt + "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib ./library --std --format markdown fi } From 82893c58ff946945a556df63572e1c7a867bd99b Mon Sep 17 00:00:00 2001 From: stogaru <143449212+stogaru@users.noreply.github.com> Date: Tue, 10 Dec 2024 05:07:48 -0800 Subject: [PATCH 14/14] `dyn Trait` proof for contracts of byte_offset_from (#196) Towards https://github.com/model-checking/verify-rust-std/issues/76 This pull request implements proof for contracts for `byte_offset_from` verifying `dyn Trait` pointee types. Both const and mut versions are included. --- library/core/src/ptr/const_ptr.rs | 29 ++++++++++++++++++++++++++++- library/core/src/ptr/mut_ptr.rs | 31 +++++++++++++++++++++++++++++-- 2 files changed, 57 insertions(+), 3 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 5f818f90904bf..637d9b65af426 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -2536,7 +2536,8 @@ mod verify { // 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 used exclusively for implementing proof for contracts for `dyn Trait` type. + #[cfg_attr(kani, derive(kani::Arbitrary))] struct TestStruct { value: i64, } @@ -2770,4 +2771,30 @@ mod verify { 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); + + // tracking issue: https://github.com/model-checking/kani/issues/3763 + // Workaround: Directly verifying the method `<*const dyn TestTrait>::byte_offset_from` + // 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_from)] + pub fn check_const_byte_offset_from_dyn() { + const gen_size: usize = mem::size_of::(); + // Since the pointer generator cannot directly create pointers to `dyn Trait`, + // we first generate a pointer to the underlying struct and then cast it to a `dyn Trait` pointer. + let mut generator_caller = PointerGenerator::::new(); + let mut generator_input = PointerGenerator::::new(); + let ptr_caller: *const TestStruct = generator_caller.any_in_bounds().ptr; + let ptr_input: *const TestStruct = if kani::any() { + generator_caller.any_alloc_status().ptr + } else { + generator_input.any_alloc_status().ptr + }; + + let ptr_caller = ptr_caller as *const dyn TestTrait; + let ptr_input = ptr_input as *const dyn TestTrait; + + unsafe { + ptr_caller.byte_offset_from(ptr_input); + } + } } diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index af749191f5949..55c8b1b3f5cec 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2763,6 +2763,7 @@ mod verify { trait TestTrait {} // Struct used exclusively for implementing proofs for contracts for `dyn Trait` type. + #[cfg_attr(kani, derive(kani::Arbitrary))] struct TestStruct { value: i64, } @@ -2775,7 +2776,7 @@ mod 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 + // 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. @@ -2793,7 +2794,7 @@ mod verify { } }; ($fn_name: ident, $proof_name:ident) => { - //tracking issue: https://github.com/model-checking/kani/issues/3763 + // 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. @@ -3013,4 +3014,30 @@ mod verify { 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); + + // tracking issue: https://github.com/model-checking/kani/issues/3763 + // Workaround: Directly verifying the method `<*mut dyn TestTrait>::byte_offset_from` + // 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_from)] + pub fn check_mut_byte_offset_from_dyn() { + const gen_size: usize = mem::size_of::(); + // Since the pointer generator cannot directly create pointers to `dyn Trait`, + // we first generate a pointer to the underlying struct and then cast it to a `dyn Trait` pointer. + let mut generator_caller = PointerGenerator::::new(); + let mut generator_input = PointerGenerator::::new(); + let ptr_caller: *mut TestStruct = generator_caller.any_in_bounds().ptr; + let ptr_input: *mut TestStruct = if kani::any() { + generator_caller.any_alloc_status().ptr + } else { + generator_input.any_alloc_status().ptr + }; + + let ptr_caller = ptr_caller as *mut dyn TestTrait; + let ptr_input = ptr_input as *mut dyn TestTrait; + + unsafe { + ptr_caller.byte_offset_from(ptr_input); + } + } }