From 500f249c90b48f307afe23fb3ed82be8a35f045a Mon Sep 17 00:00:00 2001 From: szlee118 Date: Thu, 12 Sep 2024 18:34:15 -0700 Subject: [PATCH 01/45] Add verification contract for *const T::add and *const T::add --- library/core/src/ptr/verify_const_ptr.rs | 95 ++++++++++++++++++++++++ 1 file changed, 95 insertions(+) create mode 100644 library/core/src/ptr/verify_const_ptr.rs diff --git a/library/core/src/ptr/verify_const_ptr.rs b/library/core/src/ptr/verify_const_ptr.rs new file mode 100644 index 0000000000000..b7d9d8c9687e4 --- /dev/null +++ b/library/core/src/ptr/verify_const_ptr.rs @@ -0,0 +1,95 @@ +extern crate kani; +use kani::mem::can_dereference; + +/// Function that adds an offset to a pointer. +/// +/// The `count` parameter represents the number of elements of type `T` to offset by. +/// The `object_size` parameter represents the total size of the allocated object (in bytes) +/// to ensure we stay within bounds. +/// +/// # Safety +/// This function assumes that: +/// - `ptr` must be valid and dereferenceable. +/// - The computed offset should not exceed the allocated object size. +/// - The entire range between `ptr` and `ptr.add(count)` must remain within bounds. +fn kani_pointer_add(ptr: *const T, count: usize, object_size: usize) { + unsafe { + // Precondition: The pointer must be dereferenceable + kani::assume(can_dereference(ptr)); + + // Precondition: Ensure the pointer's offset does not exceed the object size + let size_of_t = std::mem::size_of::(); + kani::assume(count * size_of_t <= object_size); + + // Perform the pointer arithmetic + let offset_ptr = ptr.add(count); + + // Post-condition: Ensure the result pointer is still within bounds of the allocated object + let end_of_object = (ptr as usize + object_size) as *const T; + + // Assert that the resulting pointer is within bounds, with a detailed message if it fails + kani::assert( + offset_ptr <= end_of_object, + "Pointer offset is out of bounds." + ); + } +} + +/// Verifies the safety of pointer offset operation. +/// +/// The `count` parameter represents the number of elements of type `T` to offset by. +/// The `object_size` parameter represents the total size of the allocated object (in bytes) +/// to ensure we stay within bounds. +/// +/// # Safety +/// This function assumes that: +/// - `ptr` must be valid and dereferenceable. +/// - The computed offset should not exceed the allocated object size. +/// - The entire range between `ptr` and `ptr.offset(count)` must remain within bounds. +fn kani_pointer_offset(ptr: *const T, count: isize, object_size: usize) { + unsafe { + // Precondition: The pointer must be dereferenceable + kani::assume(can_dereference(ptr)); + + // Precondition: Ensure the pointer's offset does not exceed the object size + let size_of_t = std::mem::size_of::(); + let max_offset = (object_size / size_of_t) as isize; + + // The offset should be within valid bounds to prevent overflow + kani::assume(count >= 0 && count <= max_offset); + + // Perform the pointer offset operation + let offset_ptr = ptr.offset(count); + + // Post-condition: Ensure the result pointer is still within bounds of the allocated object + let end_of_object = (ptr as usize + object_size) as *const T; + + // Assert that the resulting pointer is within bounds, with a detailed message if it fails + kani::assert( + offset_ptr <= end_of_object, + "Pointer offset is out of bounds." + ); + } +} + +#[kani::proof] +fn verify_pointer_add() { + let s: &str = "123"; + let ptr: *const u8 = s.as_ptr(); + let object_size = s.len(); // In bytes, the size of the allocated object + + // Test adding offsets within bounds + kani_pointer_add(ptr, 1, object_size); // Adding an offset of 1 + kani_pointer_add(ptr, 2, object_size); // Adding an offset of 2 +} + +#[kani::proof] +fn verify_pointer_offset() { + let s: &str = "123"; + let ptr: *const u8 = s.as_ptr(); + let object_size = s.len(); // In bytes, the size of the allocated object + + // Test offsetting within bounds + kani_pointer_offset(ptr, 1, object_size); // Offset by 1 + kani_pointer_offset(ptr, 2, object_size); // Offset by 2 +} \ No newline at end of file From 99701ff1fee831d3195365ba8ddf52cc75f61b1f Mon Sep 17 00:00:00 2001 From: Yifei Wang <40480373+xsxszab@users.noreply.github.com> Date: Wed, 18 Sep 2024 18:38:18 -0700 Subject: [PATCH 02/45] Update const_ptr.rs --- library/core/src/ptr/const_ptr.rs | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 3b635e2a4aa9e..54042c9d94e18 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -388,6 +388,9 @@ impl *const T { #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[kani::requires(kani::mem::can_dereference(self))] + #[kani::requires(count == 0)] + #[kani::ensures(|result| kani::mem::can_dereference(result))] pub const unsafe fn offset(self, count: isize) -> *const T where T: Sized, @@ -1774,3 +1777,20 @@ impl PartialOrd for *const T { *self >= *other } } + +#[cfg(kani)] +#[unstable(feature="kani", issue="none")] +mod verify { + use super::*; + use crate::kani; + + #[allow(unused)] + #[kani::proof_for_contract(<*const T>::offset)] + fn check_offset_i32() { + let mut test_val: i32 = kani::any(); + let test_ptr: *const i32 = &test_val; + let offset: isize = kani::any(); + unsafe {test_ptr.offset(offset)}; + } +} + From f84b7a6a4937134e7e03174c5da5c1b414aa12b0 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Thu, 19 Sep 2024 01:23:32 -0700 Subject: [PATCH 03/45] Changes generic type to i32 in proof. Refactors by removing unused crates and importing safety crate --- library/core/src/ptr/const_ptr.rs | 36 ++++++++++++++++++++----------- 1 file changed, 24 insertions(+), 12 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 54042c9d94e18..6aae9013bc37f 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -3,6 +3,10 @@ use crate::cmp::Ordering::{Equal, Greater, Less}; use crate::intrinsics::const_eval_select; use crate::mem::SizedTypeProperties; use crate::slice::{self, SliceIndex}; +use safety::{ensures, requires}; + +#[cfg(kani)] +use crate::kani; impl *const T { /// Returns `true` if the pointer is null. @@ -273,7 +277,11 @@ impl *const T { pub const unsafe fn as_ref<'a>(self) -> Option<&'a T> { // SAFETY: the caller must guarantee that `self` is valid // for a reference if it isn't null. - if self.is_null() { None } else { unsafe { Some(&*self) } } + if self.is_null() { + None + } else { + unsafe { Some(&*self) } + } } /// Returns a shared reference to the value behind the pointer. @@ -341,7 +349,11 @@ impl *const T { { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a reference. - if self.is_null() { None } else { Some(unsafe { &*(self as *const MaybeUninit) }) } + if self.is_null() { + None + } else { + Some(unsafe { &*(self as *const MaybeUninit) }) + } } /// Adds an offset to a pointer. @@ -388,9 +400,9 @@ impl *const T { #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - #[kani::requires(kani::mem::can_dereference(self))] - #[kani::requires(count == 0)] - #[kani::ensures(|result| kani::mem::can_dereference(result))] + #[requires(kani::mem::can_dereference(self))] + #[requires(count == 0)] + #[ensures(|result| kani::mem::can_dereference(result))] pub const unsafe fn offset(self, count: isize) -> *const T where T: Sized, @@ -498,7 +510,9 @@ impl *const T { #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")] #[rustc_allow_const_fn_unstable(set_ptr_value)] pub const fn wrapping_byte_offset(self, count: isize) -> Self { - self.cast::().wrapping_offset(count).with_metadata_of(self) + self.cast::() + .wrapping_offset(count) + .with_metadata_of(self) } /// Masks out bits of the pointer according to a mask. @@ -1779,18 +1793,16 @@ impl PartialOrd for *const T { } #[cfg(kani)] -#[unstable(feature="kani", issue="none")] +#[unstable(feature = "kani", issue = "none")] mod verify { - use super::*; use crate::kani; #[allow(unused)] - #[kani::proof_for_contract(<*const T>::offset)] + #[kani::proof_for_contract(<*const i32>::offset)] fn check_offset_i32() { let mut test_val: i32 = kani::any(); let test_ptr: *const i32 = &test_val; let offset: isize = kani::any(); - unsafe {test_ptr.offset(offset)}; - } + unsafe { test_ptr.offset(offset) }; + } } - From a8398201ff010d0f73708626d3b2ddec4862bd0d Mon Sep 17 00:00:00 2001 From: szlee118 Date: Fri, 20 Sep 2024 13:12:04 -0700 Subject: [PATCH 04/45] Remove unneeded file --- library/core/src/ptr/verify_const_ptr.rs | 95 ------------------------ 1 file changed, 95 deletions(-) delete mode 100644 library/core/src/ptr/verify_const_ptr.rs diff --git a/library/core/src/ptr/verify_const_ptr.rs b/library/core/src/ptr/verify_const_ptr.rs deleted file mode 100644 index b7d9d8c9687e4..0000000000000 --- a/library/core/src/ptr/verify_const_ptr.rs +++ /dev/null @@ -1,95 +0,0 @@ -extern crate kani; -use kani::mem::can_dereference; - -/// Function that adds an offset to a pointer. -/// -/// The `count` parameter represents the number of elements of type `T` to offset by. -/// The `object_size` parameter represents the total size of the allocated object (in bytes) -/// to ensure we stay within bounds. -/// -/// # Safety -/// This function assumes that: -/// - `ptr` must be valid and dereferenceable. -/// - The computed offset should not exceed the allocated object size. -/// - The entire range between `ptr` and `ptr.add(count)` must remain within bounds. -fn kani_pointer_add(ptr: *const T, count: usize, object_size: usize) { - unsafe { - // Precondition: The pointer must be dereferenceable - kani::assume(can_dereference(ptr)); - - // Precondition: Ensure the pointer's offset does not exceed the object size - let size_of_t = std::mem::size_of::(); - kani::assume(count * size_of_t <= object_size); - - // Perform the pointer arithmetic - let offset_ptr = ptr.add(count); - - // Post-condition: Ensure the result pointer is still within bounds of the allocated object - let end_of_object = (ptr as usize + object_size) as *const T; - - // Assert that the resulting pointer is within bounds, with a detailed message if it fails - kani::assert( - offset_ptr <= end_of_object, - "Pointer offset is out of bounds." - ); - } -} - -/// Verifies the safety of pointer offset operation. -/// -/// The `count` parameter represents the number of elements of type `T` to offset by. -/// The `object_size` parameter represents the total size of the allocated object (in bytes) -/// to ensure we stay within bounds. -/// -/// # Safety -/// This function assumes that: -/// - `ptr` must be valid and dereferenceable. -/// - The computed offset should not exceed the allocated object size. -/// - The entire range between `ptr` and `ptr.offset(count)` must remain within bounds. -fn kani_pointer_offset(ptr: *const T, count: isize, object_size: usize) { - unsafe { - // Precondition: The pointer must be dereferenceable - kani::assume(can_dereference(ptr)); - - // Precondition: Ensure the pointer's offset does not exceed the object size - let size_of_t = std::mem::size_of::(); - let max_offset = (object_size / size_of_t) as isize; - - // The offset should be within valid bounds to prevent overflow - kani::assume(count >= 0 && count <= max_offset); - - // Perform the pointer offset operation - let offset_ptr = ptr.offset(count); - - // Post-condition: Ensure the result pointer is still within bounds of the allocated object - let end_of_object = (ptr as usize + object_size) as *const T; - - // Assert that the resulting pointer is within bounds, with a detailed message if it fails - kani::assert( - offset_ptr <= end_of_object, - "Pointer offset is out of bounds." - ); - } -} - -#[kani::proof] -fn verify_pointer_add() { - let s: &str = "123"; - let ptr: *const u8 = s.as_ptr(); - let object_size = s.len(); // In bytes, the size of the allocated object - - // Test adding offsets within bounds - kani_pointer_add(ptr, 1, object_size); // Adding an offset of 1 - kani_pointer_add(ptr, 2, object_size); // Adding an offset of 2 -} - -#[kani::proof] -fn verify_pointer_offset() { - let s: &str = "123"; - let ptr: *const u8 = s.as_ptr(); - let object_size = s.len(); // In bytes, the size of the allocated object - - // Test offsetting within bounds - kani_pointer_offset(ptr, 1, object_size); // Offset by 1 - kani_pointer_offset(ptr, 2, object_size); // Offset by 2 -} \ No newline at end of file From 21e0ab8a3a4d3e886289ae906b2d2037a522ad64 Mon Sep 17 00:00:00 2001 From: xsxsz Date: Fri, 20 Sep 2024 14:23:10 -0700 Subject: [PATCH 05/45] added comments for function contracts and harnesses --- library/core/src/ptr/const_ptr.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 6aae9013bc37f..a192ff23548b3 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -401,7 +401,8 @@ impl *const T { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires(kani::mem::can_dereference(self))] - #[requires(count == 0)] + // TODO: Determine the valid value range for 'count' and update the precondition accordingly. + #[requires(count == 0)] // This precondition is currently a placeholder. #[ensures(|result| kani::mem::can_dereference(result))] pub const unsafe fn offset(self, count: isize) -> *const T where @@ -1792,6 +1793,8 @@ impl PartialOrd for *const T { } } +// This module contains all proof harnesses for function contracts. +// Each proof harness verifies the soundness of a function contract for a specific type. #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] mod verify { From 0c0078fc06959f716d773b77a2ce8740a465bd7b Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Mon, 30 Sep 2024 15:29:54 -0700 Subject: [PATCH 06/45] reverted library code format change and removed unnecessary comments --- library/core/src/ptr/const_ptr.rs | 24 ++++++------------------ 1 file changed, 6 insertions(+), 18 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index a192ff23548b3..18e98da6f457d 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -277,11 +277,7 @@ impl *const T { pub const unsafe fn as_ref<'a>(self) -> Option<&'a T> { // SAFETY: the caller must guarantee that `self` is valid // for a reference if it isn't null. - if self.is_null() { - None - } else { - unsafe { Some(&*self) } - } + if self.is_null() { None } else { unsafe { Some(&*self) } } } /// Returns a shared reference to the value behind the pointer. @@ -349,11 +345,7 @@ impl *const T { { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a reference. - if self.is_null() { - None - } else { - Some(unsafe { &*(self as *const MaybeUninit) }) - } + if self.is_null() { None } else { Some(unsafe { &*(self as *const MaybeUninit) }) } } /// Adds an offset to a pointer. @@ -511,9 +503,7 @@ impl *const T { #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")] #[rustc_allow_const_fn_unstable(set_ptr_value)] pub const fn wrapping_byte_offset(self, count: isize) -> Self { - self.cast::() - .wrapping_offset(count) - .with_metadata_of(self) + self.cast::().wrapping_offset(count).with_metadata_of(self) } /// Masks out bits of the pointer according to a mask. @@ -1793,19 +1783,17 @@ impl PartialOrd for *const T { } } -// This module contains all proof harnesses for function contracts. -// Each proof harness verifies the soundness of a function contract for a specific type. #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] mod verify { use crate::kani; - + #[allow(unused)] #[kani::proof_for_contract(<*const i32>::offset)] - fn check_offset_i32() { + fn check_offset_i32() { let mut test_val: i32 = kani::any(); let test_ptr: *const i32 = &test_val; let offset: isize = kani::any(); unsafe { test_ptr.offset(offset) }; - } + } } From a1921292b3dbf7096a2d8224c7b4b9ce5076d322 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Mon, 30 Sep 2024 18:50:53 -0700 Subject: [PATCH 07/45] added macros for verifying all integer types for offset and add --- library/core/src/ptr/const_ptr.rs | 73 +++++++++++++++++++++++++++---- 1 file changed, 64 insertions(+), 9 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 18e98da6f457d..630334fc8fbab 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -857,6 +857,10 @@ impl *const T { #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(kani::mem::can_dereference(self))] + // TODO: Determine the valid value range for 'count' and update the precondition accordingly. + #[requires(count == 0)] // This precondition is currently a placeholder. + #[ensures(|result| kani::mem::can_dereference(result))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -932,6 +936,10 @@ impl *const T { #[rustc_allow_const_fn_unstable(unchecked_neg)] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + // #[requires(kani::mem::can_dereference(self))] + // // TODO: Determine the valid value range for 'count' and update the precondition accordingly. + // #[requires(count == 0)] // This precondition is currently a placeholder. + // #[ensures(|result| kani::mem::can_dereference(result))] pub const unsafe fn sub(self, count: usize) -> Self where T: Sized, @@ -1787,13 +1795,60 @@ impl PartialOrd for *const T { #[unstable(feature = "kani", issue = "none")] mod verify { use crate::kani; - - #[allow(unused)] - #[kani::proof_for_contract(<*const i32>::offset)] - fn check_offset_i32() { - let mut test_val: i32 = kani::any(); - let test_ptr: *const i32 = &test_val; - let offset: isize = kani::any(); - unsafe { test_ptr.offset(offset) }; - } + + macro_rules! generate_offset_harness { + ($type:ty, $proof_name:ident) => { + #[allow(unused)] + #[kani::proof_for_contract(<*const $type>::offset)] + pub fn $proof_name() { + let mut test_val: $type = kani::any::<$type>(); + let test_ptr: *const $type = &test_val; + let count: isize = kani::any(); + unsafe { + test_ptr.offset(count); + } + } + }; + } + + generate_offset_harness!(i8, check_offset_i8); + generate_offset_harness!(i16, check_offset_i16); + generate_offset_harness!(i32, check_offset_i32); + generate_offset_harness!(i64, check_offset_i64); + generate_offset_harness!(i128, check_offset_i128); + generate_offset_harness!(isize, check_offset_isize); + generate_offset_harness!(u8, check_offset_u8); + generate_offset_harness!(u16, check_offset_u16); + generate_offset_harness!(u32, check_offset_u32); + generate_offset_harness!(u64, check_offset_u64); + generate_offset_harness!(u128, check_offset_u128); + generate_offset_harness!(usize, check_offset_usize); + + macro_rules! generate_add_harness { + ($type:ty, $proof_name:ident) => { + #[allow(unused)] + #[kani::proof_for_contract(<*const $type>::add)] + pub fn $proof_name() { + let mut test_val: $type = kani::any::<$type>(); + let test_ptr: *const $type = &test_val; + let count: usize = kani::any(); + unsafe { + test_ptr.add(count); + } + } + }; + } + + generate_add_harness!(i8, check_add_i8); + generate_add_harness!(i16, check_add_i16); + generate_add_harness!(i32, check_add_i32); + generate_add_harness!(i64, check_add_i64); + generate_add_harness!(i128, check_add_i128); + generate_add_harness!(isize, check_add_isize); + generate_add_harness!(u8, check_add_u8); + generate_add_harness!(u16, check_add_u16); + generate_add_harness!(u32, check_add_u32); + generate_add_harness!(u64, check_add_u64); + generate_add_harness!(u128, check_add_u128); + generate_add_harness!(usize, check_add_usize); } From 2ef5923ffc84cb51594fc9bc6aa4d0bac76e8bac Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Tue, 1 Oct 2024 10:03:30 -0700 Subject: [PATCH 08/45] implemented function contract and integer type proofs for fn sub --- library/core/src/ptr/const_ptr.rs | 76 +++++++++++++++++++++++++++++-- 1 file changed, 72 insertions(+), 4 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 630334fc8fbab..3ac0d81c05981 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -885,6 +885,10 @@ impl *const T { #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")] #[rustc_allow_const_fn_unstable(set_ptr_value)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + // #[requires(kani::mem::can_dereference(self))] + // // TODO: Determine the valid value range for 'count' and update the precondition accordingly. + // #[requires(count == 0)] // This precondition is currently a placeholder. + // #[ensures(|result| kani::mem::can_dereference(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) } @@ -936,10 +940,10 @@ impl *const T { #[rustc_allow_const_fn_unstable(unchecked_neg)] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - // #[requires(kani::mem::can_dereference(self))] - // // TODO: Determine the valid value range for 'count' and update the precondition accordingly. - // #[requires(count == 0)] // This precondition is currently a placeholder. - // #[ensures(|result| kani::mem::can_dereference(result))] + #[requires(kani::mem::can_dereference(self))] + // TODO: Determine the valid value range for 'count' and update the precondition accordingly. + #[requires(count == 0)] // This precondition is currently a placeholder. + #[ensures(|result| kani::mem::can_dereference(result))] pub const unsafe fn sub(self, count: usize) -> Self where T: Sized, @@ -1796,6 +1800,7 @@ impl PartialOrd for *const T { mod verify { use crate::kani; + // fn <*const T>::offset verification begin macro_rules! generate_offset_harness { ($type:ty, $proof_name:ident) => { #[allow(unused)] @@ -1823,7 +1828,9 @@ mod verify { generate_offset_harness!(u64, check_offset_u64); generate_offset_harness!(u128, check_offset_u128); generate_offset_harness!(usize, check_offset_usize); + // fn <*const T>::offset verification end + // fn <*const T>::add verification begin macro_rules! generate_add_harness { ($type:ty, $proof_name:ident) => { #[allow(unused)] @@ -1851,4 +1858,65 @@ mod verify { generate_add_harness!(u64, check_add_u64); generate_add_harness!(u128, check_add_u128); generate_add_harness!(usize, check_add_usize); + // fn <*const T>::add verification end + + // fn <*const T>::byte_add verification begin + // macro_rules! generate_byte_add_harness { + // ($type:ty, $proof_name:ident) => { + // #[allow(unused)] + // #[kani::proof_for_contract(<*const $type>::add)] + // pub fn $proof_name() { + // let mut test_val: $type = kani::any::<$type>(); + // let test_ptr: *const $type = &test_val; + // let count: usize = kani::any(); + // unsafe { + // test_ptr.byte_add(count); + // } + // } + // }; + // } + + // generate_byte_add_harness!(i8, check_byte_add_i8); + // generate_byte_add_harness!(i16, check_byte_add_i16); + // generate_byte_add_harness!(i32, check_byte_add_i32); + // generate_byte_add_harness!(i64, check_byte_add_i64); + // generate_byte_add_harness!(i128, check_byte_add_i128); + // generate_byte_add_harness!(isize, check_byte_add_isize); + // generate_byte_add_harness!(u8, check_byte_add_u8); + // generate_byte_add_harness!(u16, check_byte_add_u16); + // generate_byte_add_harness!(u32, check_byte_add_u32); + // generate_byte_add_harness!(u64, check_byte_add_u64); + // generate_byte_add_harness!(u128, check_byte_add_u128); + // generate_byte_add_harness!(usize, check_byte_add_usize); + // fn <*const T>::byte_add verification end + + // fn <*const T>::sub verification begin + macro_rules! generate_sub_harness { + ($type:ty, $proof_name:ident) => { + #[allow(unused)] + #[kani::proof_for_contract(<*const $type>::sub)] + pub fn $proof_name() { + let mut test_val: $type = kani::any::<$type>(); + let test_ptr: *const $type = &test_val; + let count: usize = kani::any(); + unsafe { + test_ptr.sub(count); + } + } + }; + } + + generate_sub_harness!(i8, check_sub_i8); + generate_sub_harness!(i16, check_sub_i16); + generate_sub_harness!(i32, check_sub_i32); + generate_sub_harness!(i64, check_sub_i64); + generate_sub_harness!(i128, check_sub_i128); + generate_sub_harness!(isize, check_sub_isize); + generate_sub_harness!(u8, check_sub_u8); + generate_sub_harness!(u16, check_sub_u16); + generate_sub_harness!(u32, check_sub_u32); + generate_sub_harness!(u64, check_sub_u64); + generate_sub_harness!(u128, check_sub_u128); + generate_sub_harness!(usize, check_sub_usize); + // fn <*const T>::sub verification end } From f1602aa50f2cda77c8cb427f181f5fba7e9253d6 Mon Sep 17 00:00:00 2001 From: szlee118 Date: Tue, 1 Oct 2024 12:03:46 -0700 Subject: [PATCH 09/45] Add verification of slice type proofs for fn offset --- library/core/src/ptr/const_ptr.rs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 6aae9013bc37f..cc1ed69b1b7cb 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1805,4 +1805,17 @@ mod verify { let offset: isize = kani::any(); unsafe { test_ptr.offset(offset) }; } + + #[kani::proof_for_contract(<*const i32>::offset)] + fn check_offset_slice_i32(){ + let mut arr: [i32; 5] = kani::any(); + let test_ptr: *const i32 = arr.as_ptr(); + let offset: isize = kani::any(); + + unsafe{ + let new_ptr = test_ptr.offset(offset); + let _ = * new_ptr; + } + } + } From 1b467d5c2581710df292fb5d4114884e0bb7e6ea Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Tue, 1 Oct 2024 12:50:03 -0700 Subject: [PATCH 10/45] add TODOs for proof for contracts --- library/core/src/ptr/const_ptr.rs | 131 +++++++++++++++++------------- library/core/src/ptr/mut_ptr.rs | 40 +++++++++ 2 files changed, 114 insertions(+), 57 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 3ac0d81c05981..af78520d1ca8d 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1800,6 +1800,66 @@ impl PartialOrd for *const T { mod verify { use crate::kani; + // fn <*const T>::add verification begin + macro_rules! generate_add_harness { + ($type:ty, $proof_name:ident) => { + #[allow(unused)] + #[kani::proof_for_contract(<*const $type>::add)] + pub fn $proof_name() { + let mut test_val: $type = kani::any::<$type>(); + let test_ptr: *const $type = &test_val; + let count: usize = kani::any(); + unsafe { + test_ptr.add(count); + } + } + }; + } + + generate_add_harness!(i8, check_add_i8); + generate_add_harness!(i16, check_add_i16); + generate_add_harness!(i32, check_add_i32); + generate_add_harness!(i64, check_add_i64); + generate_add_harness!(i128, check_add_i128); + generate_add_harness!(isize, check_add_isize); + generate_add_harness!(u8, check_add_u8); + generate_add_harness!(u16, check_add_u16); + generate_add_harness!(u32, check_add_u32); + generate_add_harness!(u64, check_add_u64); + generate_add_harness!(u128, check_add_u128); + generate_add_harness!(usize, check_add_usize); + // fn <*const T>::add verification end + + // fn <*const T>::sub verification begin + macro_rules! generate_sub_harness { + ($type:ty, $proof_name:ident) => { + #[allow(unused)] + #[kani::proof_for_contract(<*const $type>::sub)] + pub fn $proof_name() { + let mut test_val: $type = kani::any::<$type>(); + let test_ptr: *const $type = &test_val; + let count: usize = kani::any(); + unsafe { + test_ptr.sub(count); + } + } + }; + } + + generate_sub_harness!(i8, check_sub_i8); + generate_sub_harness!(i16, check_sub_i16); + generate_sub_harness!(i32, check_sub_i32); + generate_sub_harness!(i64, check_sub_i64); + generate_sub_harness!(i128, check_sub_i128); + generate_sub_harness!(isize, check_sub_isize); + generate_sub_harness!(u8, check_sub_u8); + generate_sub_harness!(u16, check_sub_u16); + generate_sub_harness!(u32, check_sub_u32); + generate_sub_harness!(u64, check_sub_u64); + generate_sub_harness!(u128, check_sub_u128); + generate_sub_harness!(usize, check_sub_usize); + // fn <*const T>::sub verification end + // fn <*const T>::offset verification begin macro_rules! generate_offset_harness { ($type:ty, $proof_name:ident) => { @@ -1830,35 +1890,9 @@ mod verify { generate_offset_harness!(usize, check_offset_usize); // fn <*const T>::offset verification end - // fn <*const T>::add verification begin - macro_rules! generate_add_harness { - ($type:ty, $proof_name:ident) => { - #[allow(unused)] - #[kani::proof_for_contract(<*const $type>::add)] - pub fn $proof_name() { - let mut test_val: $type = kani::any::<$type>(); - let test_ptr: *const $type = &test_val; - let count: usize = kani::any(); - unsafe { - test_ptr.add(count); - } - } - }; - } - - generate_add_harness!(i8, check_add_i8); - generate_add_harness!(i16, check_add_i16); - generate_add_harness!(i32, check_add_i32); - generate_add_harness!(i64, check_add_i64); - generate_add_harness!(i128, check_add_i128); - generate_add_harness!(isize, check_add_isize); - generate_add_harness!(u8, check_add_u8); - generate_add_harness!(u16, check_add_u16); - generate_add_harness!(u32, check_add_u32); - generate_add_harness!(u64, check_add_u64); - generate_add_harness!(u128, check_add_u128); - generate_add_harness!(usize, check_add_usize); - // fn <*const T>::add verification end + // fn <*const T>::offset_from verification begin + // TODO + // fn <*const T>::offset_from verification end // fn <*const T>::byte_add verification begin // macro_rules! generate_byte_add_harness { @@ -1890,33 +1924,16 @@ mod verify { // generate_byte_add_harness!(usize, check_byte_add_usize); // fn <*const T>::byte_add verification end - // fn <*const T>::sub verification begin - macro_rules! generate_sub_harness { - ($type:ty, $proof_name:ident) => { - #[allow(unused)] - #[kani::proof_for_contract(<*const $type>::sub)] - pub fn $proof_name() { - let mut test_val: $type = kani::any::<$type>(); - let test_ptr: *const $type = &test_val; - let count: usize = kani::any(); - unsafe { - test_ptr.sub(count); - } - } - }; - } + // fn <*const T>::byte_sub verification begin + // TODO + // fn <*const T>::byte_sub verification end + + // fn <*const T>::byte_offset verification begin + // TODO + // fn <*const T>::byte_offset verification end + + // fn <*const T>::byte_offset_from verification begin + // TODO + // fn <*const T>::byte_offset_from verification end - generate_sub_harness!(i8, check_sub_i8); - generate_sub_harness!(i16, check_sub_i16); - generate_sub_harness!(i32, check_sub_i32); - generate_sub_harness!(i64, check_sub_i64); - generate_sub_harness!(i128, check_sub_i128); - generate_sub_harness!(isize, check_sub_isize); - generate_sub_harness!(u8, check_sub_u8); - generate_sub_harness!(u16, check_sub_u16); - generate_sub_harness!(u32, check_sub_u32); - generate_sub_harness!(u64, check_sub_u64); - generate_sub_harness!(u128, check_sub_u128); - generate_sub_harness!(usize, check_sub_usize); - // fn <*const T>::sub verification end } diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 42975cc927b8e..4cfdca4deebb2 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2197,3 +2197,43 @@ impl PartialOrd for *mut T { *self >= *other } } + + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use crate::kani; + + // fn <*mut T>::add verification begin + // TODO + // fn <*mut T>::add verification begin + + // fn <*mut T>::sub verification begin + // TODO + // fn <*mut T>::sub verification end + + // fn <*mut T>::offset verification begin + // TODO + // fn <*mut T>::offset verification end + + // fn <*mut T>::offset_from verification begin + // TODO + // fn <*mut T>::offset_from verification end + + // fn <*mut T>::byte_add verification begin + // TODO + // fn <*mut T>::byte_add verification end + + // fn <*mut T>::byte_sub verification begin + // TODO + // fn <*mut T>::byte_sub verification end + + // fn <*mut T>::byte_offset verification begin + // TODO + // fn <*mut T>::byte_offset verification end + + // fn <*mut T>::byte_offset_from verification begin + // TODO + // fn <*mut T>::byte_offset_from verification end + +} \ No newline at end of file From 9461027268852e5c6d4a464ebedf638a6cbf640f Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Tue, 1 Oct 2024 12:59:27 -0700 Subject: [PATCH 11/45] verified *mut T::offset for all integer types --- library/core/src/ptr/mut_ptr.rs | 36 ++++++++++++++++++++++++++++++++- 1 file changed, 35 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 4cfdca4deebb2..180ef13911f0f 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -3,6 +3,10 @@ use crate::cmp::Ordering::{Equal, Greater, Less}; use crate::intrinsics::const_eval_select; use crate::mem::SizedTypeProperties; use crate::slice::{self, SliceIndex}; +use safety::{ensures, requires}; + +#[cfg(kani)] +use crate::kani; impl *mut T { /// Returns `true` if the pointer is null. @@ -947,6 +951,10 @@ impl *mut T { #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(kani::mem::can_dereference(self))] + // TODO: Determine the valid value range for 'count' and update the precondition accordingly. + #[requires(count == 0)] // This precondition is currently a placeholder. + #[ensures(|result| kani::mem::can_dereference(result))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -2205,7 +2213,33 @@ mod verify { use crate::kani; // fn <*mut T>::add verification begin - // TODO + macro_rules! generate_mut_add_harness { + ($type:ty, $proof_name:ident) => { + #[allow(unused)] + #[kani::proof_for_contract(<*mut $type>::add)] + pub fn $proof_name() { + let mut test_val: $type = kani::any::<$type>(); + let test_ptr: *mut $type = &mut test_val; + let count: usize = kani::any(); + unsafe { + test_ptr.add(count); + } + } + }; + } + + generate_mut_add_harness!(i8, check_mut_add_i8); + generate_mut_add_harness!(i16, check_mut_add_i16); + generate_mut_add_harness!(i32, check_mut_add_i32); + generate_mut_add_harness!(i64, check_mut_add_i64); + generate_mut_add_harness!(i128, check_mut_add_i128); + generate_mut_add_harness!(isize, check_mut_add_isize); + generate_mut_add_harness!(u8, check_mut_add_u8); + generate_mut_add_harness!(u16, check_mut_add_u16); + generate_mut_add_harness!(u32, check_mut_add_u32); + generate_mut_add_harness!(u64, check_mut_add_u64); + generate_mut_add_harness!(u128, check_mut_add_u128); + generate_mut_add_harness!(usize, check_mut_add_usize); // fn <*mut T>::add verification begin // fn <*mut T>::sub verification begin From 159137bdcb7c33edf6ab07e7e44e9df093d7e902 Mon Sep 17 00:00:00 2001 From: szlee118 Date: Wed, 2 Oct 2024 17:44:45 -0700 Subject: [PATCH 12/45] Add verification of slice type proofs for fn add and sub --- library/core/src/ptr/const_ptr.rs | 46 +++++++++++++++++++++++++------ 1 file changed, 38 insertions(+), 8 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index cc1ed69b1b7cb..fd2de3ef2acb5 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -866,6 +866,10 @@ impl *const T { #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(kani::mem::can_dereference(self))] + // TODO: Determine the valid value range for 'count' and update the precondition accordingly. + #[requires(count == 0)] // This precondition is currently a placeholder. + #[ensures(|result| kani::mem::can_dereference(result))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -941,6 +945,10 @@ impl *const T { #[rustc_allow_const_fn_unstable(unchecked_neg)] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(kani::mem::can_dereference(self))] + // TODO: Determine the valid value range for 'count' and update the precondition accordingly. + #[requires(count == 0)] // This precondition is currently a placeholder. + #[ensures(|result| kani::mem::can_dereference(result))] pub const unsafe fn sub(self, count: usize) -> Self where T: Sized, @@ -1798,13 +1806,15 @@ mod verify { use crate::kani; #[allow(unused)] - #[kani::proof_for_contract(<*const i32>::offset)] - fn check_offset_i32() { - let mut test_val: i32 = kani::any(); - let test_ptr: *const i32 = &test_val; - let offset: isize = kani::any(); - unsafe { test_ptr.offset(offset) }; - } + // #[kani::proof_for_contract(<*const i32>::offset)] + // fn check_offset_i32() { + // let mut test_val: i32 = kani::any(); + // let test_ptr: *const i32 = &test_val; + // let offset: isize = kani::any(); + // unsafe { + // test_ptr.offset(offset) + // }; + // } #[kani::proof_for_contract(<*const i32>::offset)] fn check_offset_slice_i32(){ @@ -1814,7 +1824,27 @@ mod verify { unsafe{ let new_ptr = test_ptr.offset(offset); - let _ = * new_ptr; + } + } + + #[kani::proof_for_contract(<*const i32>::add)] + fn check_add_slice_i32() { + let mut arr: [i32; 5] = kani::any(); + let test_ptr: *const i32 = arr.as_ptr(); + let count: usize = kani::any(); + unsafe { + let new_ptr = test_ptr.add(count); + } + } + + + #[kani::proof_for_contract(<*const i32>::sub)] + fn check_sub_slice_i32() { + let mut arr: [i32; 5] = kani::any(); + let test_ptr: *const i32 = arr.as_ptr(); + let count: usize = kani::any(); + unsafe { + let new_ptr = test_ptr.sub(count); } } From df56d181f4d742256822842f9bb28e059be69b24 Mon Sep 17 00:00:00 2001 From: szlee118 Date: Wed, 2 Oct 2024 17:47:51 -0700 Subject: [PATCH 13/45] Remove commented code --- library/core/src/ptr/const_ptr.rs | 9 --------- 1 file changed, 9 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index fd2de3ef2acb5..60efad527653c 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1806,15 +1806,6 @@ mod verify { use crate::kani; #[allow(unused)] - // #[kani::proof_for_contract(<*const i32>::offset)] - // fn check_offset_i32() { - // let mut test_val: i32 = kani::any(); - // let test_ptr: *const i32 = &test_val; - // let offset: isize = kani::any(); - // unsafe { - // test_ptr.offset(offset) - // }; - // } #[kani::proof_for_contract(<*const i32>::offset)] fn check_offset_slice_i32(){ From eab0a1537336e71b7b3ac533a47a75239f820ff1 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Wed, 2 Oct 2024 17:58:10 -0700 Subject: [PATCH 14/45] removed unnecessary comments --- library/core/src/ptr/const_ptr.rs | 46 ------------------------------- library/core/src/ptr/mut_ptr.rs | 28 ------------------- 2 files changed, 74 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index af78520d1ca8d..5be79a4f4c68a 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1890,50 +1890,4 @@ mod verify { generate_offset_harness!(usize, check_offset_usize); // fn <*const T>::offset verification end - // fn <*const T>::offset_from verification begin - // TODO - // fn <*const T>::offset_from verification end - - // fn <*const T>::byte_add verification begin - // macro_rules! generate_byte_add_harness { - // ($type:ty, $proof_name:ident) => { - // #[allow(unused)] - // #[kani::proof_for_contract(<*const $type>::add)] - // pub fn $proof_name() { - // let mut test_val: $type = kani::any::<$type>(); - // let test_ptr: *const $type = &test_val; - // let count: usize = kani::any(); - // unsafe { - // test_ptr.byte_add(count); - // } - // } - // }; - // } - - // generate_byte_add_harness!(i8, check_byte_add_i8); - // generate_byte_add_harness!(i16, check_byte_add_i16); - // generate_byte_add_harness!(i32, check_byte_add_i32); - // generate_byte_add_harness!(i64, check_byte_add_i64); - // generate_byte_add_harness!(i128, check_byte_add_i128); - // generate_byte_add_harness!(isize, check_byte_add_isize); - // generate_byte_add_harness!(u8, check_byte_add_u8); - // generate_byte_add_harness!(u16, check_byte_add_u16); - // generate_byte_add_harness!(u32, check_byte_add_u32); - // generate_byte_add_harness!(u64, check_byte_add_u64); - // generate_byte_add_harness!(u128, check_byte_add_u128); - // generate_byte_add_harness!(usize, check_byte_add_usize); - // fn <*const T>::byte_add verification end - - // fn <*const T>::byte_sub verification begin - // TODO - // fn <*const T>::byte_sub verification end - - // fn <*const T>::byte_offset verification begin - // TODO - // fn <*const T>::byte_offset verification end - - // fn <*const T>::byte_offset_from verification begin - // TODO - // fn <*const T>::byte_offset_from verification end - } diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 180ef13911f0f..246a4480548c8 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2242,32 +2242,4 @@ mod verify { generate_mut_add_harness!(usize, check_mut_add_usize); // fn <*mut T>::add verification begin - // fn <*mut T>::sub verification begin - // TODO - // fn <*mut T>::sub verification end - - // fn <*mut T>::offset verification begin - // TODO - // fn <*mut T>::offset verification end - - // fn <*mut T>::offset_from verification begin - // TODO - // fn <*mut T>::offset_from verification end - - // fn <*mut T>::byte_add verification begin - // TODO - // fn <*mut T>::byte_add verification end - - // fn <*mut T>::byte_sub verification begin - // TODO - // fn <*mut T>::byte_sub verification end - - // fn <*mut T>::byte_offset verification begin - // TODO - // fn <*mut T>::byte_offset verification end - - // fn <*mut T>::byte_offset_from verification begin - // TODO - // fn <*mut T>::byte_offset_from verification end - } \ No newline at end of file From e07040ffa96cb3feab97387c770b18ac0f4cd304 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Wed, 2 Oct 2024 18:02:07 -0700 Subject: [PATCH 15/45] reverted changes to mut_ptr.rs --- library/core/src/ptr/mut_ptr.rs | 46 --------------------------------- 1 file changed, 46 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 246a4480548c8..8d8dc7dbab99d 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -3,10 +3,6 @@ use crate::cmp::Ordering::{Equal, Greater, Less}; use crate::intrinsics::const_eval_select; use crate::mem::SizedTypeProperties; use crate::slice::{self, SliceIndex}; -use safety::{ensures, requires}; - -#[cfg(kani)] -use crate::kani; impl *mut T { /// Returns `true` if the pointer is null. @@ -951,10 +947,6 @@ impl *mut T { #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - #[requires(kani::mem::can_dereference(self))] - // TODO: Determine the valid value range for 'count' and update the precondition accordingly. - #[requires(count == 0)] // This precondition is currently a placeholder. - #[ensures(|result| kani::mem::can_dereference(result))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -2204,42 +2196,4 @@ impl PartialOrd for *mut T { fn ge(&self, other: &*mut T) -> bool { *self >= *other } -} - - -#[cfg(kani)] -#[unstable(feature = "kani", issue = "none")] -mod verify { - use crate::kani; - - // fn <*mut T>::add verification begin - macro_rules! generate_mut_add_harness { - ($type:ty, $proof_name:ident) => { - #[allow(unused)] - #[kani::proof_for_contract(<*mut $type>::add)] - pub fn $proof_name() { - let mut test_val: $type = kani::any::<$type>(); - let test_ptr: *mut $type = &mut test_val; - let count: usize = kani::any(); - unsafe { - test_ptr.add(count); - } - } - }; - } - - generate_mut_add_harness!(i8, check_mut_add_i8); - generate_mut_add_harness!(i16, check_mut_add_i16); - generate_mut_add_harness!(i32, check_mut_add_i32); - generate_mut_add_harness!(i64, check_mut_add_i64); - generate_mut_add_harness!(i128, check_mut_add_i128); - generate_mut_add_harness!(isize, check_mut_add_isize); - generate_mut_add_harness!(u8, check_mut_add_u8); - generate_mut_add_harness!(u16, check_mut_add_u16); - generate_mut_add_harness!(u32, check_mut_add_u32); - generate_mut_add_harness!(u64, check_mut_add_u64); - generate_mut_add_harness!(u128, check_mut_add_u128); - generate_mut_add_harness!(usize, check_mut_add_usize); - // fn <*mut T>::add verification begin - } \ No newline at end of file From 0ff52b54b724b71dc0f693abec5969c59b0ed54d Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Wed, 2 Oct 2024 18:10:10 -0700 Subject: [PATCH 16/45] removed necessary comments --- library/core/src/ptr/const_ptr.rs | 4 ---- 1 file changed, 4 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 5be79a4f4c68a..848ed22116daa 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -885,10 +885,6 @@ impl *const T { #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")] #[rustc_allow_const_fn_unstable(set_ptr_value)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - // #[requires(kani::mem::can_dereference(self))] - // // TODO: Determine the valid value range for 'count' and update the precondition accordingly. - // #[requires(count == 0)] // This precondition is currently a placeholder. - // #[ensures(|result| kani::mem::can_dereference(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) } From ccd5c3c52bb9b6794030b7e8f70a07fc11b9e3f5 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Wed, 2 Oct 2024 18:11:13 -0700 Subject: [PATCH 17/45] aligned format for mut_ptr.rs --- library/core/src/ptr/mut_ptr.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 8d8dc7dbab99d..07e1a800698db 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2196,4 +2196,5 @@ impl PartialOrd for *mut T { fn ge(&self, other: &*mut T) -> bool { *self >= *other } + } \ No newline at end of file From 180a27697462e5cbeae103cbac3a5acb4c2d9565 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Wed, 2 Oct 2024 18:14:10 -0700 Subject: [PATCH 18/45] aligned format for mut_ptr.rs --- library/core/src/ptr/mut_ptr.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 07e1a800698db..42975cc927b8e 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2196,5 +2196,4 @@ impl PartialOrd for *mut T { fn ge(&self, other: &*mut T) -> bool { *self >= *other } - -} \ No newline at end of file +} From fb79caf3ec4d0da3341f17bffb5b4c6aae35f40a Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Wed, 2 Oct 2024 18:28:38 -0700 Subject: [PATCH 19/45] Adds proofs for composite type - tuple --- library/core/src/ptr/const_ptr.rs | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 848ed22116daa..87183a3c5b9e7 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1823,7 +1823,11 @@ mod verify { generate_add_harness!(u32, check_add_u32); generate_add_harness!(u64, check_add_u64); generate_add_harness!(u128, check_add_u128); - generate_add_harness!(usize, check_add_usize); + generate_add_harness!(usize, check_add_usize); + generate_add_harness!((i8, i8), check_offset_tuple_1); + generate_add_harness!((f64, bool), check_offset_tuple_2); + generate_add_harness!((i32, f64, bool), check_offset_tuple_3); + generate_add_harness!((i8, u16, i32, u64, isize), check_offset_tuple_4); // fn <*const T>::add verification end // fn <*const T>::sub verification begin @@ -1853,7 +1857,11 @@ mod verify { generate_sub_harness!(u32, check_sub_u32); generate_sub_harness!(u64, check_sub_u64); generate_sub_harness!(u128, check_sub_u128); - generate_sub_harness!(usize, check_sub_usize); + generate_sub_harness!(usize, check_sub_usize); + generate_sub_harness!((i8, i8), check_offset_tuple_1); + generate_sub_harness!((f64, bool), check_offset_tuple_2); + generate_sub_harness!((i32, f64, bool), check_offset_tuple_3); + generate_sub_harness!((i8, u16, i32, u64, isize), check_offset_tuple_4); // fn <*const T>::sub verification end // fn <*const T>::offset verification begin @@ -1884,6 +1892,10 @@ mod verify { generate_offset_harness!(u64, check_offset_u64); generate_offset_harness!(u128, check_offset_u128); generate_offset_harness!(usize, check_offset_usize); + generate_offset_harness!((i8, i8), check_offset_tuple_1); + generate_offset_harness!((f64, bool), check_offset_tuple_2); + generate_offset_harness!((i32, f64, bool), check_offset_tuple_3); + generate_offset_harness!((i8, u16, i32, u64, isize), check_offset_tuple_4); // fn <*const T>::offset verification end } From 7d05c96b6ffcdeb9424b9b3f487bc42a27d304cd Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Wed, 2 Oct 2024 18:32:42 -0700 Subject: [PATCH 20/45] Change function proof names --- library/core/src/ptr/const_ptr.rs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 87183a3c5b9e7..4eadbdf39c679 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1824,10 +1824,10 @@ mod verify { generate_add_harness!(u64, check_add_u64); generate_add_harness!(u128, check_add_u128); generate_add_harness!(usize, check_add_usize); - generate_add_harness!((i8, i8), check_offset_tuple_1); - generate_add_harness!((f64, bool), check_offset_tuple_2); - generate_add_harness!((i32, f64, bool), check_offset_tuple_3); - generate_add_harness!((i8, u16, i32, u64, isize), check_offset_tuple_4); + generate_add_harness!((i8, i8), check_add_tuple_1); + generate_add_harness!((f64, bool), check_add_tuple_2); + generate_add_harness!((i32, f64, bool), check_add_tuple_3); + generate_add_harness!((i8, u16, i32, u64, isize), check_add_tuple_4); // fn <*const T>::add verification end // fn <*const T>::sub verification begin @@ -1858,10 +1858,10 @@ mod verify { generate_sub_harness!(u64, check_sub_u64); generate_sub_harness!(u128, check_sub_u128); generate_sub_harness!(usize, check_sub_usize); - generate_sub_harness!((i8, i8), check_offset_tuple_1); - generate_sub_harness!((f64, bool), check_offset_tuple_2); - generate_sub_harness!((i32, f64, bool), check_offset_tuple_3); - generate_sub_harness!((i8, u16, i32, u64, isize), check_offset_tuple_4); + generate_sub_harness!((i8, i8), check_sub_tuple_1); + generate_sub_harness!((f64, bool), check_sub_tuple_2); + generate_sub_harness!((i32, f64, bool), check_sub_tuple_3); + generate_sub_harness!((i8, u16, i32, u64, isize), check_sub_tuple_4); // fn <*const T>::sub verification end // fn <*const T>::offset verification begin From f9f53713070452340fbc9c0e2d147608f25d11ad Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 Date: Sun, 6 Oct 2024 18:06:26 -0700 Subject: [PATCH 21/45] Added changes for *const T::add & *const::sub verifying unit type --- library/core/src/ptr/const_ptr.rs | 153 ++++++++++++++++++++++++++++-- 1 file changed, 145 insertions(+), 8 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 18e98da6f457d..2c81d50a20a1b 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -857,6 +857,10 @@ impl *const T { #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(kani::mem::can_dereference(self))] + // TODO: Determine the valid value range for 'count' and update the precondition accordingly. + #[requires(count == 0)] // This precondition is currently a placeholder. + #[ensures(|result| kani::mem::can_dereference(result))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -932,6 +936,10 @@ impl *const T { #[rustc_allow_const_fn_unstable(unchecked_neg)] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(kani::mem::can_dereference(self))] + // TODO: Determine the valid value range for 'count' and update the precondition accordingly. + #[requires(count == 0)] // This precondition is currently a placeholder. + #[ensures(|result| kani::mem::can_dereference(result))] pub const unsafe fn sub(self, count: usize) -> Self where T: Sized, @@ -1787,13 +1795,142 @@ impl PartialOrd for *const T { #[unstable(feature = "kani", issue = "none")] mod verify { use crate::kani; - + + // fn <*const T>::add verification begin + macro_rules! generate_add_harness { + ($type:ty, $proof_name:ident) => { + #[allow(unused)] + #[kani::proof_for_contract(<*const $type>::add)] + pub fn $proof_name() { + let mut test_val: $type = kani::any::<$type>(); + let test_ptr: *const $type = &test_val; + let count: usize = kani::any(); + unsafe { + test_ptr.add(count); + } + } + }; + } + + generate_add_harness!(i8, check_add_i8); + generate_add_harness!(i16, check_add_i16); + generate_add_harness!(i32, check_add_i32); + generate_add_harness!(i64, check_add_i64); + generate_add_harness!(i128, check_add_i128); + generate_add_harness!(isize, check_add_isize); + generate_add_harness!(u8, check_add_u8); + generate_add_harness!(u16, check_add_u16); + generate_add_harness!(u32, check_add_u32); + generate_add_harness!(u64, check_add_u64); + generate_add_harness!(u128, check_add_u128); + generate_add_harness!(usize, check_add_usize); + // fn <*const T>::add verification end + + // fn <*const T>::sub verification begin + macro_rules! generate_sub_harness { + ($type:ty, $proof_name:ident) => { + #[allow(unused)] + #[kani::proof_for_contract(<*const $type>::sub)] + pub fn $proof_name() { + let mut test_val: $type = kani::any::<$type>(); + let test_ptr: *const $type = &test_val; + let count: usize = kani::any(); + unsafe { + test_ptr.sub(count); + } + } + }; + } + + generate_sub_harness!(i8, check_sub_i8); + generate_sub_harness!(i16, check_sub_i16); + generate_sub_harness!(i32, check_sub_i32); + generate_sub_harness!(i64, check_sub_i64); + generate_sub_harness!(i128, check_sub_i128); + generate_sub_harness!(isize, check_sub_isize); + generate_sub_harness!(u8, check_sub_u8); + generate_sub_harness!(u16, check_sub_u16); + generate_sub_harness!(u32, check_sub_u32); + generate_sub_harness!(u64, check_sub_u64); + generate_sub_harness!(u128, check_sub_u128); + generate_sub_harness!(usize, check_sub_usize); + // fn <*const T>::sub verification end + + // fn <*const T>::offset verification begin + macro_rules! generate_offset_harness { + ($type:ty, $proof_name:ident) => { + #[allow(unused)] + #[kani::proof_for_contract(<*const $type>::offset)] + pub fn $proof_name() { + let mut test_val: $type = kani::any::<$type>(); + let test_ptr: *const $type = &test_val; + let count: isize = kani::any(); + unsafe { + test_ptr.offset(count); + } + } + }; + } + + generate_offset_harness!(i8, check_offset_i8); + generate_offset_harness!(i16, check_offset_i16); + generate_offset_harness!(i32, check_offset_i32); + generate_offset_harness!(i64, check_offset_i64); + generate_offset_harness!(i128, check_offset_i128); + generate_offset_harness!(isize, check_offset_isize); + generate_offset_harness!(u8, check_offset_u8); + generate_offset_harness!(u16, check_offset_u16); + generate_offset_harness!(u32, check_offset_u32); + generate_offset_harness!(u64, check_offset_u64); + generate_offset_harness!(u128, check_offset_u128); + generate_offset_harness!(usize, check_offset_usize); + // fn <*const T>::offset verification end + + // Unit type proofs start + #[allow(unused)] + #[kani::proof_for_contract(<*const ()>::offset)] + fn verify_offset_unit() { + let base: () = (); + let ptr: *const () = &base; + kani::assume(kani::mem::can_dereference(ptr)); + let result = unsafe { ptr.offset(0) }; + assert!(kani::mem::can_dereference(result)); + assert!(ptr == result); + + } + + #[allow(unused)] + #[kani::proof_for_contract(<*const ()>::add)] + fn verify_add_unit(){ + let unit_val = (); + let unit_ref: &() = &unit_val; + let ptr: *const () = unit_ref; + let count: usize = kani::any(); + + unsafe { + let result = ptr.add(count); + kani::assume(kani::mem::can_dereference(result)); + assert_eq!(result, ptr); + assert_eq!(*result, ()); + } + } + #[allow(unused)] - #[kani::proof_for_contract(<*const i32>::offset)] - fn check_offset_i32() { - let mut test_val: i32 = kani::any(); - let test_ptr: *const i32 = &test_val; - let offset: isize = kani::any(); - unsafe { test_ptr.offset(offset) }; - } + #[kani::proof_for_contract(<*const ()>::sub)] + fn verify_sub_unit(){ + let unit_val = (); + let unit_ref: &() = &unit_val; + let ptr: *const () = unit_ref; + let count: usize = kani::any(); + + unsafe { + let result = ptr.sub(count); + kani::assume(kani::mem::can_dereference(result)); + assert_eq!(result, ptr); + assert_eq!(*result, ()); + } + } + // Unit type proofs end + + } From eab900e2db5996bf5ea30df140243c023542f4a5 Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 Date: Fri, 11 Oct 2024 19:57:52 -0700 Subject: [PATCH 22/45] Updated proofs for const ptr (unit type) --- library/core/src/ptr/const_ptr.rs | 61 ++++++++++++------------------- 1 file changed, 24 insertions(+), 37 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 2c81d50a20a1b..f76527fabbabb 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1887,47 +1887,34 @@ mod verify { // fn <*const T>::offset verification end // Unit type proofs start - #[allow(unused)] - #[kani::proof_for_contract(<*const ()>::offset)] - fn verify_offset_unit() { - let base: () = (); - let ptr: *const () = &base; - kani::assume(kani::mem::can_dereference(ptr)); - let result = unsafe { ptr.offset(0) }; - assert!(kani::mem::can_dereference(result)); - assert!(ptr == result); - - } - - #[allow(unused)] - #[kani::proof_for_contract(<*const ()>::add)] - fn verify_add_unit(){ - let unit_val = (); - let unit_ref: &() = &unit_val; - let ptr: *const () = unit_ref; - let count: usize = kani::any(); - - unsafe { - let result = ptr.add(count); - kani::assume(kani::mem::can_dereference(result)); - assert_eq!(result, ptr); - assert_eq!(*result, ()); - } + + + macro_rules! generate_const_unit_harness { + ($fn_name:ident, $proof_name:ident) => { + #[allow(unused)] + #[kani::proof_for_contract(<*const ()>::$fn_name)] + pub fn $proof_name() { + let test_val: () = (); + let test_ptr: *const () = &test_val; + let count: usize = kani::any(); + unsafe { + test_ptr.$fn_name(count); + } + } + }; } - #[allow(unused)] - #[kani::proof_for_contract(<*const ()>::sub)] - fn verify_sub_unit(){ - let unit_val = (); - let unit_ref: &() = &unit_val; - let ptr: *const () = unit_ref; - let count: usize = kani::any(); + generate_const_unit_harness!(add, check_const_add_unit); + generate_const_unit_harness!(sub, check_const_sub_unit); + #[allow(unused)] + #[kani::proof_for_contract(<*const ()>::offset)] + pub fn check_const_offset_unit() { + let test_val: () = (); + let test_ptr: *const () = &test_val; + let count: isize = kani::any(); unsafe { - let result = ptr.sub(count); - kani::assume(kani::mem::can_dereference(result)); - assert_eq!(result, ptr); - assert_eq!(*result, ()); + test_ptr.offset(count); } } // Unit type proofs end From bd418a455d4674c215e25a9e24d3c34ce2ff6180 Mon Sep 17 00:00:00 2001 From: szlee118 Date: Fri, 25 Oct 2024 09:59:09 -0700 Subject: [PATCH 23/45] Generate slice harness for array --- library/core/src/ptr/const_ptr.rs | 66 +++++++++++++++++++++++++++++++ 1 file changed, 66 insertions(+) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index a96a159d27c38..20d407f9e52f8 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1796,6 +1796,72 @@ impl PartialOrd for *const T { mod verify { use crate::kani; + // Constant for array size used in all tests + const ARRAY_SIZE: usize = 5; + + /// This macro generates verification harnesses for the `offset`, `add`, and `sub` + /// pointer operations for a specific type and function name. + /// - `$ty`: The type of the array (e.g., i32, u32, tuples). + /// - `$offset_fn`: The function name for the `offset` operation. + /// - `$add_fn`: The function name for the `add` operation. + /// - `$sub_fn`: The function name for the `sub` operation. + macro_rules! generate_pointer_harnesses { + ($ty:ty, $offset_fn:ident, $add_fn:ident, $sub_fn:ident) => { + // Generates a harness for the `offset` operation + #[kani::proof_for_contract(<*const $ty>::offset)] + fn $offset_fn() { + let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array(); + let test_ptr: *const $ty = arr.as_ptr(); + let offset: isize = kani::any(); + unsafe { + let new_ptr = test_ptr.offset(offset); + } + } + + // Generates a harness for the `add` operation + #[kani::proof_for_contract(<*const $ty>::add)] + fn $add_fn() { + let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array(); + let test_ptr: *const $ty = arr.as_ptr(); + let count: usize = kani::any(); + unsafe { + let new_ptr = test_ptr.add(count); + } + } + + // Generates a harness for the `sub` operation + #[kani::proof_for_contract(<*const $ty>::sub)] + fn $sub_fn() { + let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array(); + let test_ptr: *const $ty = arr.as_ptr(); + let count: usize = kani::any(); + unsafe { + let new_ptr = test_ptr.sub(count); + } + } + }; + } + + // Generate pointer harnesses for various types (offset, add, sub) + generate_pointer_harnesses!(i8, check_offset_slice_i8, check_add_slice_i8, check_sub_slice_i8); + generate_pointer_harnesses!(i16, check_offset_slice_i16, check_add_slice_i16, check_sub_slice_i16); + generate_pointer_harnesses!(i32, check_offset_slice_i32, check_add_slice_i32, check_sub_slice_i32); + generate_pointer_harnesses!(i64, check_offset_slice_i64, check_add_slice_i64, check_sub_slice_i64); + generate_pointer_harnesses!(i128, check_offset_slice_i128, check_add_slice_i128, check_sub_slice_i128); + generate_pointer_harnesses!(isize, check_offset_slice_isize, check_add_slice_isize, check_sub_slice_isize); + generate_pointer_harnesses!(u8, check_offset_slice_u8, check_add_slice_u8, check_sub_slice_u8); + generate_pointer_harnesses!(u16, check_offset_slice_u16, check_add_slice_u16, check_sub_slice_u16); + generate_pointer_harnesses!(u32, check_offset_slice_u32, check_add_slice_u32, check_sub_slice_u32); + generate_pointer_harnesses!(u64, check_offset_slice_u64, check_add_slice_u64, check_sub_slice_u64); + generate_pointer_harnesses!(u128, check_offset_slice_u128, check_add_slice_u128, check_sub_slice_u128); + generate_pointer_harnesses!(usize, check_offset_slice_usize, check_add_slice_usize, check_sub_slice_usize); + + // Generate pointer harnesses for tuples (offset, add, sub) + generate_pointer_harnesses!((i8, i8), check_offset_slice_tuple_1, check_add_slice_tuple_1, check_sub_slice_tuple_1); + generate_pointer_harnesses!((f64, bool), check_offset_slice_tuple_2, check_add_slice_tuple_2, check_sub_slice_tuple_2); + generate_pointer_harnesses!((i32, f64, bool), check_offset_slice_tuple_3, check_add_slice_tuple_3, check_sub_slice_tuple_3); + generate_pointer_harnesses!((i8, u16, i32, u64, isize), check_offset_slice_tuple_4, check_add_slice_tuple_4, check_sub_slice_tuple_4); + #[kani::proof_for_contract(<*const i32>::offset)] fn check_offset_slice_i32(){ let mut arr: [i32; 5] = kani::any(); From e05b5f8d6d67fc2595d857d8eae14b8682d65442 Mon Sep 17 00:00:00 2001 From: szlee118 Date: Fri, 25 Oct 2024 10:13:41 -0700 Subject: [PATCH 24/45] Remove redundant declaration --- library/core/src/ptr/const_ptr.rs | 32 ------------------------------- 1 file changed, 32 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 20d407f9e52f8..7b93f54f93c69 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1861,38 +1861,6 @@ mod verify { generate_pointer_harnesses!((f64, bool), check_offset_slice_tuple_2, check_add_slice_tuple_2, check_sub_slice_tuple_2); generate_pointer_harnesses!((i32, f64, bool), check_offset_slice_tuple_3, check_add_slice_tuple_3, check_sub_slice_tuple_3); generate_pointer_harnesses!((i8, u16, i32, u64, isize), check_offset_slice_tuple_4, check_add_slice_tuple_4, check_sub_slice_tuple_4); - - #[kani::proof_for_contract(<*const i32>::offset)] - fn check_offset_slice_i32(){ - let mut arr: [i32; 5] = kani::any(); - let test_ptr: *const i32 = arr.as_ptr(); - let offset: isize = kani::any(); - - unsafe{ - let new_ptr = test_ptr.offset(offset); - } - } - - #[kani::proof_for_contract(<*const i32>::add)] - fn check_add_slice_i32() { - let mut arr: [i32; 5] = kani::any(); - let test_ptr: *const i32 = arr.as_ptr(); - let count: usize = kani::any(); - unsafe { - let new_ptr = test_ptr.add(count); - } - } - - - #[kani::proof_for_contract(<*const i32>::sub)] - fn check_sub_slice_i32() { - let mut arr: [i32; 5] = kani::any(); - let test_ptr: *const i32 = arr.as_ptr(); - let count: usize = kani::any(); - unsafe { - let new_ptr = test_ptr.sub(count); - } - } // fn <*const T>::add verification begin macro_rules! generate_add_harness { From b944ec051791435230c9c13676938add05ba7db0 Mon Sep 17 00:00:00 2001 From: szlee118 Date: Wed, 6 Nov 2024 18:12:07 -0800 Subject: [PATCH 25/45] Update to offset test_ptr non-deterministically within the allocated object --- library/core/src/ptr/const_ptr.rs | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 7b93f54f93c69..57d52819fa848 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1812,9 +1812,12 @@ mod verify { fn $offset_fn() { let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array(); let test_ptr: *const $ty = arr.as_ptr(); - let offset: isize = kani::any(); + let offset: usize = kani::any(); + let count: isize = kani::any(); + kani::assume(offset <= ARRAY_SIZE); + let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); unsafe { - let new_ptr = test_ptr.offset(offset); + ptr_with_offset.offset(count); } } @@ -1823,9 +1826,12 @@ mod verify { fn $add_fn() { let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array(); let test_ptr: *const $ty = arr.as_ptr(); + let offset: usize = kani::any(); let count: usize = kani::any(); + kani::assume(offset <= ARRAY_SIZE); + let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); unsafe { - let new_ptr = test_ptr.add(count); + ptr_with_offset.add(count); } } @@ -1834,9 +1840,12 @@ mod verify { fn $sub_fn() { let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array(); let test_ptr: *const $ty = arr.as_ptr(); + let offset: usize = kani::any(); let count: usize = kani::any(); + kani::assume(offset <= ARRAY_SIZE); + let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); unsafe { - let new_ptr = test_ptr.sub(count); + ptr_with_offset.sub(count); } } }; From 054d8875f575bf08cb9abfa69f77e85e47cf0580 Mon Sep 17 00:00:00 2001 From: szlee118 Date: Wed, 6 Nov 2024 18:24:52 -0800 Subject: [PATCH 26/45] Update the precondition for offset in harness --- library/core/src/ptr/const_ptr.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 57d52819fa848..e24024fc6f55e 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1795,7 +1795,7 @@ impl PartialOrd for *const T { #[unstable(feature = "kani", issue = "none")] mod verify { use crate::kani; - + use core::mem; // Constant for array size used in all tests const ARRAY_SIZE: usize = 5; @@ -1814,7 +1814,7 @@ mod verify { let test_ptr: *const $ty = arr.as_ptr(); let offset: usize = kani::any(); let count: isize = kani::any(); - kani::assume(offset <= ARRAY_SIZE); + kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); unsafe { ptr_with_offset.offset(count); @@ -1828,7 +1828,7 @@ mod verify { let test_ptr: *const $ty = arr.as_ptr(); let offset: usize = kani::any(); let count: usize = kani::any(); - kani::assume(offset <= ARRAY_SIZE); + kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); unsafe { ptr_with_offset.add(count); @@ -1842,7 +1842,7 @@ mod verify { let test_ptr: *const $ty = arr.as_ptr(); let offset: usize = kani::any(); let count: usize = kani::any(); - kani::assume(offset <= ARRAY_SIZE); + kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); unsafe { ptr_with_offset.sub(count); From de6ef30c44921c5ce1601a264e377fa7820f3243 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Wed, 6 Nov 2024 18:45:40 -0800 Subject: [PATCH 27/45] updated function contracts and proof for contracts for add(), sub() and offset() --- library/core/src/ptr/const_ptr.rs | 262 ++++++++++++++++-------------- 1 file changed, 142 insertions(+), 120 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index a96a159d27c38..7d6df2beda1e0 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -392,10 +392,20 @@ impl *const T { #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - #[requires(kani::mem::can_dereference(self))] - // TODO: Determine the valid value range for 'count' and update the precondition accordingly. - #[requires(count == 0)] // This precondition is currently a placeholder. - #[ensures(|result| kani::mem::can_dereference(result))] + #[requires( + // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize` + count.checked_mul(core::mem::size_of::() as isize).is_some() && + // Precondition 2: adding the computed offset to `self` does not cause overflow + (self as isize).checked_add((count * core::mem::size_of::() as isize)).is_some() && + // 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)))) + )] + // 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, *result as *const T))] pub const unsafe fn offset(self, count: isize) -> *const T where T: Sized, @@ -857,10 +867,21 @@ impl *const T { #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - #[requires(kani::mem::can_dereference(self))] - // TODO: Determine the valid value range for 'count' and update the precondition accordingly. - #[requires(count == 0)] // This precondition is currently a placeholder. - #[ensures(|result| kani::mem::can_dereference(result))] + #[requires( + // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize` + count.checked_mul(core::mem::size_of::()).is_some() && + count * core::mem::size_of::() <= isize::MAX as usize && + // Precondition 2: adding the computed offset to `self` does not cause overflow + (self as isize).checked_add((count * core::mem::size_of::()) as isize).is_some() && + // 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)))) + )] + // 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, *result as *const T))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -936,10 +957,21 @@ impl *const T { #[rustc_allow_const_fn_unstable(unchecked_neg)] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - #[requires(kani::mem::can_dereference(self))] - // TODO: Determine the valid value range for 'count' and update the precondition accordingly. - #[requires(count == 0)] // This precondition is currently a placeholder. - #[ensures(|result| kani::mem::can_dereference(result))] + #[requires( + // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize` + count.checked_mul(core::mem::size_of::()).is_some() && + count * core::mem::size_of::() <= isize::MAX as usize && + // Precondition 2: subtracting the computed offset from `self` does not cause overflow + (self as isize).checked_sub((count * core::mem::size_of::()) as isize).is_some() && + // 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)))) + )] + // 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, *result as *const T))] pub const unsafe fn sub(self, count: usize) -> Self where T: Sized, @@ -1796,137 +1828,127 @@ impl PartialOrd for *const T { mod verify { use crate::kani; - #[kani::proof_for_contract(<*const i32>::offset)] - fn check_offset_slice_i32(){ - let mut arr: [i32; 5] = kani::any(); - let test_ptr: *const i32 = arr.as_ptr(); - let offset: isize = kani::any(); - - unsafe{ - let new_ptr = test_ptr.offset(offset); - } - } - - #[kani::proof_for_contract(<*const i32>::add)] - fn check_add_slice_i32() { - let mut arr: [i32; 5] = kani::any(); - let test_ptr: *const i32 = arr.as_ptr(); - let count: usize = kani::any(); - unsafe { - let new_ptr = test_ptr.add(count); - } - } - - - #[kani::proof_for_contract(<*const i32>::sub)] - fn check_sub_slice_i32() { - let mut arr: [i32; 5] = kani::any(); - let test_ptr: *const i32 = arr.as_ptr(); - let count: usize = kani::any(); - unsafe { - let new_ptr = test_ptr.sub(count); - } - } - - // fn <*const T>::add verification begin - macro_rules! generate_add_harness { - ($type:ty, $proof_name:ident) => { - #[allow(unused)] + // generate proof for contracts for integer type, composite type and unit type pointers + macro_rules! generate_const_arithmetic_harness { + ($type:ty, $proof_name:ident, add) => { #[kani::proof_for_contract(<*const $type>::add)] pub fn $proof_name() { let mut test_val: $type = kani::any::<$type>(); + let offset: usize = kani::any(); + let count: usize = kani::any(); let test_ptr: *const $type = &test_val; - let count: usize = kani::any(); + + // For integer, composite, and unit types, 1 is the largest offset that + // keeps `ptr_with_offset` within bounds. + kani::assume(offset <= 1); + let ptr_with_offset: *const $type = test_ptr.wrapping_add(offset); unsafe { - test_ptr.add(count); + ptr_with_offset.add(count); } } }; - } - - generate_add_harness!(i8, check_add_i8); - generate_add_harness!(i16, check_add_i16); - generate_add_harness!(i32, check_add_i32); - generate_add_harness!(i64, check_add_i64); - generate_add_harness!(i128, check_add_i128); - generate_add_harness!(isize, check_add_isize); - generate_add_harness!(u8, check_add_u8); - generate_add_harness!(u16, check_add_u16); - generate_add_harness!(u32, check_add_u32); - generate_add_harness!(u64, check_add_u64); - generate_add_harness!(u128, check_add_u128); - generate_add_harness!(usize, check_add_usize); - generate_add_harness!((i8, i8), check_add_tuple_1); - generate_add_harness!((f64, bool), check_add_tuple_2); - generate_add_harness!((i32, f64, bool), check_add_tuple_3); - generate_add_harness!((i8, u16, i32, u64, isize), check_add_tuple_4); - generate_add_harness!((), check_add_unit); - - // fn <*const T>::sub verification begin - macro_rules! generate_sub_harness { - ($type:ty, $proof_name:ident) => { - #[allow(unused)] + ($type:ty, $proof_name:ident, sub) => { #[kani::proof_for_contract(<*const $type>::sub)] pub fn $proof_name() { let mut test_val: $type = kani::any::<$type>(); - let test_ptr: *const $type = &test_val; + let offset: usize = kani::any(); let count: usize = kani::any(); + let test_ptr: *const $type = &test_val; + + // For integer, composite, and unit types, 1 is the largest offset that + // keeps `ptr_with_offset` within bounds. + kani::assume(offset <= 1); + let ptr_with_offset: *const $type = test_ptr.wrapping_add(offset); unsafe { - test_ptr.sub(count); + ptr_with_offset.sub(count); } } }; - } - - generate_sub_harness!(i8, check_sub_i8); - generate_sub_harness!(i16, check_sub_i16); - generate_sub_harness!(i32, check_sub_i32); - generate_sub_harness!(i64, check_sub_i64); - generate_sub_harness!(i128, check_sub_i128); - generate_sub_harness!(isize, check_sub_isize); - generate_sub_harness!(u8, check_sub_u8); - generate_sub_harness!(u16, check_sub_u16); - generate_sub_harness!(u32, check_sub_u32); - generate_sub_harness!(u64, check_sub_u64); - generate_sub_harness!(u128, check_sub_u128); - generate_sub_harness!(usize, check_sub_usize); - generate_sub_harness!((i8, i8), check_sub_tuple_1); - generate_sub_harness!((f64, bool), check_sub_tuple_2); - generate_sub_harness!((i32, f64, bool), check_sub_tuple_3); - generate_sub_harness!((i8, u16, i32, u64, isize), check_sub_tuple_4); - generate_sub_harness!((), check_sub_unit); - - // fn <*const T>::offset verification begin - macro_rules! generate_offset_harness { - ($type:ty, $proof_name:ident) => { - #[allow(unused)] + ($type:ty, $proof_name:ident, offset) => { #[kani::proof_for_contract(<*const $type>::offset)] pub fn $proof_name() { let mut test_val: $type = kani::any::<$type>(); - let test_ptr: *const $type = &test_val; + let offset: usize = kani::any(); let count: isize = kani::any(); + let test_ptr: *const $type = &test_val; + + // For integer, composite, and unit types, 1 is the largest offset that + // keeps `ptr_with_offset` within bounds. + kani::assume(offset <= 1); + let ptr_with_offset: *const $type = test_ptr.wrapping_add(offset); unsafe { - test_ptr.offset(count); + ptr_with_offset.offset(count); } } }; } - generate_offset_harness!(i8, check_offset_i8); - generate_offset_harness!(i16, check_offset_i16); - generate_offset_harness!(i32, check_offset_i32); - generate_offset_harness!(i64, check_offset_i64); - generate_offset_harness!(i128, check_offset_i128); - generate_offset_harness!(isize, check_offset_isize); - generate_offset_harness!(u8, check_offset_u8); - generate_offset_harness!(u16, check_offset_u16); - generate_offset_harness!(u32, check_offset_u32); - generate_offset_harness!(u64, check_offset_u64); - generate_offset_harness!(u128, check_offset_u128); - generate_offset_harness!(usize, check_offset_usize); - generate_offset_harness!((i8, i8), check_offset_tuple_1); - generate_offset_harness!((f64, bool), check_offset_tuple_2); - generate_offset_harness!((i32, f64, bool), check_offset_tuple_3); - generate_offset_harness!((i8, u16, i32, u64, isize), check_offset_tuple_4); - generate_offset_harness!((), check_offset_unit); -} + // <*mut T>:: add() integer types verification + generate_const_arithmetic_harness!(i8, check_const_add_i8, add); + generate_const_arithmetic_harness!(i16, check_const_add_i16, add); + generate_const_arithmetic_harness!(i32, check_const_add_i32, add); + generate_const_arithmetic_harness!(i64, check_const_add_i64, add); + generate_const_arithmetic_harness!(i128, check_const_add_i128, add); + generate_const_arithmetic_harness!(isize, check_const_add_isize, add); + generate_const_arithmetic_harness!(u8, check_const_add_u8, add); + generate_const_arithmetic_harness!(u16, check_const_add_u16, add); + generate_const_arithmetic_harness!(u32, check_const_add_u32, add); + generate_const_arithmetic_harness!(u64, check_const_add_u64, add); + generate_const_arithmetic_harness!(u128, check_const_add_u128, add); + generate_const_arithmetic_harness!(usize, check_const_add_usize, add); + + // <*mut T>:: add() unit type verification + generate_const_arithmetic_harness!((), check_const_add_unit, add); + + // <*mut T>:: add() composite types verification + generate_const_arithmetic_harness!((i8, i8), check_const_add_tuple_1, add); + generate_const_arithmetic_harness!((f64, bool), check_const_add_tuple_2, add); + generate_const_arithmetic_harness!((i32, f64, bool), check_const_add_tuple_3, add); + generate_const_arithmetic_harness!((i8, u16, i32, u64, isize), check_const_add_tuple_4, add); + + // <*mut T>:: sub() integer types verification + generate_const_arithmetic_harness!(i8, check_const_sub_i8, sub); + generate_const_arithmetic_harness!(i16, check_const_sub_i16, sub); + generate_const_arithmetic_harness!(i32, check_const_sub_i32, sub); + generate_const_arithmetic_harness!(i64, check_const_sub_i64, sub); + generate_const_arithmetic_harness!(i128, check_const_sub_i128, sub); + generate_const_arithmetic_harness!(isize, check_const_sub_isize, sub); + generate_const_arithmetic_harness!(u8, check_const_sub_u8, sub); + generate_const_arithmetic_harness!(u16, check_const_sub_u16, sub); + generate_const_arithmetic_harness!(u32, check_const_sub_u32, sub); + generate_const_arithmetic_harness!(u64, check_const_sub_u64, sub); + generate_const_arithmetic_harness!(u128, check_const_sub_u128, sub); + generate_const_arithmetic_harness!(usize, check_const_sub_usize, sub); + + // <*mut T>:: sub() unit type verification + generate_const_arithmetic_harness!((), check_const_sub_unit, sub); + + // <*mut T>:: sub() composite types verification + generate_const_arithmetic_harness!((i8, i8), check_const_sub_tuple_1, sub); + generate_const_arithmetic_harness!((f64, bool), check_const_sub_tuple_2, sub); + generate_const_arithmetic_harness!((i32, f64, bool), check_const_sub_tuple_3, sub); + generate_const_arithmetic_harness!((i8, u16, i32, u64, isize), check_const_sub_tuple_4, sub); + + // fn <*mut T>::offset() integer types verification + generate_const_arithmetic_harness!(i8, check_const_offset_i8, offset); + generate_const_arithmetic_harness!(i16, check_const_offset_i16, offset); + generate_const_arithmetic_harness!(i32, check_const_offset_i32, offset); + generate_const_arithmetic_harness!(i64, check_const_offset_i64, offset); + generate_const_arithmetic_harness!(i128, check_const_offset_i128, offset); + generate_const_arithmetic_harness!(isize, check_const_offset_isize, offset); + generate_const_arithmetic_harness!(u8, check_const_offset_u8, offset); + generate_const_arithmetic_harness!(u16, check_const_offset_u16, offset); + generate_const_arithmetic_harness!(u32, check_const_offset_u32, offset); + generate_const_arithmetic_harness!(u64, check_const_offset_u64, offset); + generate_const_arithmetic_harness!(u128, check_const_offset_u128, offset); + generate_const_arithmetic_harness!(usize, check_const_offset_usize, offset); + + // fn <*mut T>::offset() unit type verification + generate_const_arithmetic_harness!((), check_const_offset_unit, offset); + + // fn <*mut T>::offset() composite type verification + generate_const_arithmetic_harness!((i8, i8), check_const_offset_tuple_1, offset); + generate_const_arithmetic_harness!((f64, bool), check_const_offset_tuple_2, offset); + generate_const_arithmetic_harness!((i32, f64, bool), check_const_offset_tuple_3, offset); + generate_const_arithmetic_harness!((i8, u16, i32, u64, isize), check_const_offset_tuple_4, offset); +} \ No newline at end of file From 554e003e4a888f4c41291eab7848d693beedd974 Mon Sep 17 00:00:00 2001 From: szlee118 Date: Thu, 7 Nov 2024 23:33:19 -0800 Subject: [PATCH 28/45] Modify document --- library/core/src/ptr/const_ptr.rs | 38 +++++++++++++++---------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 60206b7edfa0f..f7560041e3fc8 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1828,16 +1828,16 @@ impl PartialOrd for *const T { mod verify { use crate::kani; use core::mem; - // Constant for array size used in all tests + // Constant for array size used in all tests, for performance reason const ARRAY_SIZE: usize = 5; /// This macro generates verification harnesses for the `offset`, `add`, and `sub` - /// pointer operations for a specific type and function name. + /// pointer operations for a slice type and function name. /// - `$ty`: The type of the array (e.g., i32, u32, tuples). /// - `$offset_fn`: The function name for the `offset` operation. /// - `$add_fn`: The function name for the `add` operation. /// - `$sub_fn`: The function name for the `sub` operation. - macro_rules! generate_pointer_harnesses { + macro_rules! generate_slice_harnesses { ($ty:ty, $offset_fn:ident, $add_fn:ident, $sub_fn:ident) => { // Generates a harness for the `offset` operation #[kani::proof_for_contract(<*const $ty>::offset)] @@ -1884,24 +1884,24 @@ mod verify { } // Generate pointer harnesses for various types (offset, add, sub) - generate_pointer_harnesses!(i8, check_offset_slice_i8, check_add_slice_i8, check_sub_slice_i8); - generate_pointer_harnesses!(i16, check_offset_slice_i16, check_add_slice_i16, check_sub_slice_i16); - generate_pointer_harnesses!(i32, check_offset_slice_i32, check_add_slice_i32, check_sub_slice_i32); - generate_pointer_harnesses!(i64, check_offset_slice_i64, check_add_slice_i64, check_sub_slice_i64); - generate_pointer_harnesses!(i128, check_offset_slice_i128, check_add_slice_i128, check_sub_slice_i128); - generate_pointer_harnesses!(isize, check_offset_slice_isize, check_add_slice_isize, check_sub_slice_isize); - generate_pointer_harnesses!(u8, check_offset_slice_u8, check_add_slice_u8, check_sub_slice_u8); - generate_pointer_harnesses!(u16, check_offset_slice_u16, check_add_slice_u16, check_sub_slice_u16); - generate_pointer_harnesses!(u32, check_offset_slice_u32, check_add_slice_u32, check_sub_slice_u32); - generate_pointer_harnesses!(u64, check_offset_slice_u64, check_add_slice_u64, check_sub_slice_u64); - generate_pointer_harnesses!(u128, check_offset_slice_u128, check_add_slice_u128, check_sub_slice_u128); - generate_pointer_harnesses!(usize, check_offset_slice_usize, check_add_slice_usize, check_sub_slice_usize); + generate_slice_harnesses!(i8, check_offset_slice_i8, check_add_slice_i8, check_sub_slice_i8); + generate_slice_harnesses!(i16, check_offset_slice_i16, check_add_slice_i16, check_sub_slice_i16); + generate_slice_harnesses!(i32, check_offset_slice_i32, check_add_slice_i32, check_sub_slice_i32); + generate_slice_harnesses!(i64, check_offset_slice_i64, check_add_slice_i64, check_sub_slice_i64); + generate_slice_harnesses!(i128, check_offset_slice_i128, check_add_slice_i128, check_sub_slice_i128); + generate_slice_harnesses!(isize, check_offset_slice_isize, check_add_slice_isize, check_sub_slice_isize); + generate_slice_harnesses!(u8, check_offset_slice_u8, check_add_slice_u8, check_sub_slice_u8); + generate_slice_harnesses!(u16, check_offset_slice_u16, check_add_slice_u16, check_sub_slice_u16); + generate_slice_harnesses!(u32, check_offset_slice_u32, check_add_slice_u32, check_sub_slice_u32); + generate_slice_harnesses!(u64, check_offset_slice_u64, check_add_slice_u64, check_sub_slice_u64); + generate_slice_harnesses!(u128, check_offset_slice_u128, check_add_slice_u128, check_sub_slice_u128); + generate_slice_harnesses!(usize, check_offset_slice_usize, check_add_slice_usize, check_sub_slice_usize); // Generate pointer harnesses for tuples (offset, add, sub) - generate_pointer_harnesses!((i8, i8), check_offset_slice_tuple_1, check_add_slice_tuple_1, check_sub_slice_tuple_1); - generate_pointer_harnesses!((f64, bool), check_offset_slice_tuple_2, check_add_slice_tuple_2, check_sub_slice_tuple_2); - generate_pointer_harnesses!((i32, f64, bool), check_offset_slice_tuple_3, check_add_slice_tuple_3, check_sub_slice_tuple_3); - generate_pointer_harnesses!((i8, u16, i32, u64, isize), check_offset_slice_tuple_4, check_add_slice_tuple_4, check_sub_slice_tuple_4); + generate_slice_harnesses!((i8, i8), check_offset_slice_tuple_1, check_add_slice_tuple_1, check_sub_slice_tuple_1); + generate_slice_harnesses!((f64, bool), check_offset_slice_tuple_2, check_add_slice_tuple_2, check_sub_slice_tuple_2); + generate_slice_harnesses!((i32, f64, bool), check_offset_slice_tuple_3, check_add_slice_tuple_3, check_sub_slice_tuple_3); + generate_slice_harnesses!((i8, u16, i32, u64, isize), check_offset_slice_tuple_4, check_add_slice_tuple_4, check_sub_slice_tuple_4); // fn <*const T>::add verification begin macro_rules! generate_add_harness { From a69688f046d2c27b941973460a1509fb9949c9db Mon Sep 17 00:00:00 2001 From: szlee118 Date: Thu, 7 Nov 2024 23:41:26 -0800 Subject: [PATCH 29/45] Fix indentation error --- library/core/src/ptr/const_ptr.rs | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index f7560041e3fc8..9eab11acc1a4f 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1902,12 +1902,7 @@ mod verify { generate_slice_harnesses!((f64, bool), check_offset_slice_tuple_2, check_add_slice_tuple_2, check_sub_slice_tuple_2); generate_slice_harnesses!((i32, f64, bool), check_offset_slice_tuple_3, check_add_slice_tuple_3, check_sub_slice_tuple_3); generate_slice_harnesses!((i8, u16, i32, u64, isize), check_offset_slice_tuple_4, check_add_slice_tuple_4, check_sub_slice_tuple_4); - - // fn <*const T>::add verification begin - macro_rules! generate_add_harness { - ($type:ty, $proof_name:ident) => { - #[allow(unused)] - + // generate proof for contracts for integer type, composite type and unit type pointers macro_rules! generate_const_arithmetic_harness { ($type:ty, $proof_name:ident, add) => { From 3effadde93bfc22d9450ac611cd2c26aad0710f0 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Thu, 14 Nov 2024 10:23:18 -0800 Subject: [PATCH 30/45] improved comments and function naming --- library/core/src/ptr/const_ptr.rs | 81 ++++++++++++++++++++----------- 1 file changed, 52 insertions(+), 29 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 9eab11acc1a4f..60433e821fd5e 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1883,27 +1883,50 @@ mod verify { }; } - // Generate pointer harnesses for various types (offset, add, sub) - generate_slice_harnesses!(i8, check_offset_slice_i8, check_add_slice_i8, check_sub_slice_i8); - generate_slice_harnesses!(i16, check_offset_slice_i16, check_add_slice_i16, check_sub_slice_i16); - generate_slice_harnesses!(i32, check_offset_slice_i32, check_add_slice_i32, check_sub_slice_i32); - generate_slice_harnesses!(i64, check_offset_slice_i64, check_add_slice_i64, check_sub_slice_i64); - generate_slice_harnesses!(i128, check_offset_slice_i128, check_add_slice_i128, check_sub_slice_i128); - generate_slice_harnesses!(isize, check_offset_slice_isize, check_add_slice_isize, check_sub_slice_isize); - generate_slice_harnesses!(u8, check_offset_slice_u8, check_add_slice_u8, check_sub_slice_u8); - generate_slice_harnesses!(u16, check_offset_slice_u16, check_add_slice_u16, check_sub_slice_u16); - generate_slice_harnesses!(u32, check_offset_slice_u32, check_add_slice_u32, check_sub_slice_u32); - generate_slice_harnesses!(u64, check_offset_slice_u64, check_add_slice_u64, check_sub_slice_u64); - generate_slice_harnesses!(u128, check_offset_slice_u128, check_add_slice_u128, check_sub_slice_u128); - generate_slice_harnesses!(usize, check_offset_slice_usize, check_add_slice_usize, check_sub_slice_usize); - - // Generate pointer harnesses for tuples (offset, add, sub) - generate_slice_harnesses!((i8, i8), check_offset_slice_tuple_1, check_add_slice_tuple_1, check_sub_slice_tuple_1); - generate_slice_harnesses!((f64, bool), check_offset_slice_tuple_2, check_add_slice_tuple_2, check_sub_slice_tuple_2); - generate_slice_harnesses!((i32, f64, bool), check_offset_slice_tuple_3, check_add_slice_tuple_3, check_sub_slice_tuple_3); - generate_slice_harnesses!((i8, u16, i32, u64, isize), check_offset_slice_tuple_4, check_add_slice_tuple_4, check_sub_slice_tuple_4); + // Generate slice harnesses for various types (offset, add, sub) + generate_slice_harnesses!(i8, check_const_offset_slice_i8, check_const_add_slice_i8, check_const_sub_slice_i8); + generate_slice_harnesses!(i16, check_const_offset_slice_i16, check_const_add_slice_i16, check_const_sub_slice_i16); + generate_slice_harnesses!(i32, check_const_offset_slice_i32, check_const_add_slice_i32, check_const_sub_slice_i32); + generate_slice_harnesses!(i64, check_const_offset_slice_i64, check_const_add_slice_i64, check_const_sub_slice_i64); + generate_slice_harnesses!(i128, check_const_offset_slice_i128, check_const_add_slice_i128, check_const_sub_slice_i128); + generate_slice_harnesses!(isize, check_const_offset_slice_isize, check_const_add_slice_isize, check_const_sub_slice_isize); + generate_slice_harnesses!(u8, check_const_offset_slice_u8, check_const_add_slice_u8, check_const_sub_slice_u8); + generate_slice_harnesses!(u16, check_const_offset_slice_u16, check_const_add_slice_u16, check_const_sub_slice_u16); + generate_slice_harnesses!(u32, check_const_offset_slice_u32, check_const_add_slice_u32, check_const_sub_slice_u32); + generate_slice_harnesses!(u64, check_const_offset_slice_u64, check_const_add_slice_u64, check_const_sub_slice_u64); + generate_slice_harnesses!(u128, check_const_offset_slice_u128, check_const_add_slice_u128, check_const_sub_slice_u128); + generate_slice_harnesses!(usize, check_const_offset_slice_usize, check_const_add_slice_usize, check_const_sub_slice_usize); + + // Generate slice harnesses for tuples (offset, add, sub) + generate_slice_harnesses!( + (i8, i8), + check_const_offset_slice_tuple_1, + check_const_add_slice_tuple_1, + check_const_sub_slice_tuple_1 + ); + generate_slice_harnesses!( + (f64, bool), + check_const_offset_slice_tuple_2, + check_const_add_slice_tuple_2, + check_const_sub_slice_tuple_2 + ); + generate_slice_harnesses!( + (i32, f64, bool), + check_const_offset_slice_tuple_3, + check_const_add_slice_tuple_3, + check_const_sub_slice_tuple_3 + ); + generate_slice_harnesses!( + (i8, u16, i32, u64, isize), + check_const_offset_slice_tuple_4, + check_const_add_slice_tuple_4, + check_const_sub_slice_tuple_4 + ); - // generate proof for contracts for integer type, composite type and unit type pointers + /// This macro generates proofs for contracts on `add`, `sub`, and `offset` + /// operations for pointers to integer, composite, and unit types. + /// - `$type`: Specifies the pointee type. + /// - `$proof_name`: Specifies the name of the generated proof for the contract. macro_rules! generate_const_arithmetic_harness { ($type:ty, $proof_name:ident, add) => { #[kani::proof_for_contract(<*const $type>::add)] @@ -1958,7 +1981,7 @@ mod verify { }; } - // <*mut T>:: add() integer types verification + // <*const T>:: add() integer types verification generate_const_arithmetic_harness!(i8, check_const_add_i8, add); generate_const_arithmetic_harness!(i16, check_const_add_i16, add); generate_const_arithmetic_harness!(i32, check_const_add_i32, add); @@ -1972,16 +1995,16 @@ mod verify { generate_const_arithmetic_harness!(u128, check_const_add_u128, add); generate_const_arithmetic_harness!(usize, check_const_add_usize, add); - // <*mut T>:: add() unit type verification + // <*const T>:: add() unit type verification generate_const_arithmetic_harness!((), check_const_add_unit, add); - // <*mut T>:: add() composite types verification + // <*const T>:: add() composite types verification generate_const_arithmetic_harness!((i8, i8), check_const_add_tuple_1, add); generate_const_arithmetic_harness!((f64, bool), check_const_add_tuple_2, add); generate_const_arithmetic_harness!((i32, f64, bool), check_const_add_tuple_3, add); generate_const_arithmetic_harness!((i8, u16, i32, u64, isize), check_const_add_tuple_4, add); - // <*mut T>:: sub() integer types verification + // <*const T>:: sub() integer types verification generate_const_arithmetic_harness!(i8, check_const_sub_i8, sub); generate_const_arithmetic_harness!(i16, check_const_sub_i16, sub); generate_const_arithmetic_harness!(i32, check_const_sub_i32, sub); @@ -1995,16 +2018,16 @@ mod verify { generate_const_arithmetic_harness!(u128, check_const_sub_u128, sub); generate_const_arithmetic_harness!(usize, check_const_sub_usize, sub); - // <*mut T>:: sub() unit type verification + // <*const T>:: sub() unit type verification generate_const_arithmetic_harness!((), check_const_sub_unit, sub); - // <*mut T>:: sub() composite types verification + // <*const T>:: sub() composite types verification generate_const_arithmetic_harness!((i8, i8), check_const_sub_tuple_1, sub); generate_const_arithmetic_harness!((f64, bool), check_const_sub_tuple_2, sub); generate_const_arithmetic_harness!((i32, f64, bool), check_const_sub_tuple_3, sub); generate_const_arithmetic_harness!((i8, u16, i32, u64, isize), check_const_sub_tuple_4, sub); - // fn <*mut T>::offset() integer types verification + // fn <*const T>::offset() integer types verification generate_const_arithmetic_harness!(i8, check_const_offset_i8, offset); generate_const_arithmetic_harness!(i16, check_const_offset_i16, offset); generate_const_arithmetic_harness!(i32, check_const_offset_i32, offset); @@ -2018,10 +2041,10 @@ mod verify { generate_const_arithmetic_harness!(u128, check_const_offset_u128, offset); generate_const_arithmetic_harness!(usize, check_const_offset_usize, offset); - // fn <*mut T>::offset() unit type verification + // fn <*const T>::offset() unit type verification generate_const_arithmetic_harness!((), check_const_offset_unit, offset); - // fn <*mut T>::offset() composite type verification + // fn <*const T>::offset() composite type verification generate_const_arithmetic_harness!((i8, i8), check_const_offset_tuple_1, offset); generate_const_arithmetic_harness!((f64, bool), check_const_offset_tuple_2, offset); generate_const_arithmetic_harness!((i32, f64, bool), check_const_offset_tuple_3, offset); From c3cb7fe763aedc6c0c9d44547f15b5a20899c070 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Thu, 14 Nov 2024 10:25:19 -0800 Subject: [PATCH 31/45] fixed a typo --- library/core/src/ptr/const_ptr.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 60433e821fd5e..9d513bbbb2877 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1926,7 +1926,7 @@ mod verify { /// This macro generates proofs for contracts on `add`, `sub`, and `offset` /// operations for pointers to integer, composite, and unit types. /// - `$type`: Specifies the pointee type. - /// - `$proof_name`: Specifies the name of the generated proof for the contract. + /// - `$proof_name`: Specifies the name of the generated proof for contract. macro_rules! generate_const_arithmetic_harness { ($type:ty, $proof_name:ident, add) => { #[kani::proof_for_contract(<*const $type>::add)] From cc5d490416a771f21cc8c9f25af3ca6d8240f7da Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Thu, 14 Nov 2024 20:52:06 -0800 Subject: [PATCH 32/45] updated proofs using pointer generator --- library/core/src/ptr/const_ptr.rs | 44 +++++++++++-------------------- 1 file changed, 16 insertions(+), 28 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 5c10b68584023..32857714913fd 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -2056,51 +2056,39 @@ mod verify { ($type:ty, $proof_name:ident, add) => { #[kani::proof_for_contract(<*const $type>::add)] pub fn $proof_name() { - let mut test_val: $type = kani::any::<$type>(); - let offset: usize = kani::any(); - let count: usize = kani::any(); - let test_ptr: *const $type = &test_val; - - // For integer, composite, and unit types, 1 is the largest offset that - // keeps `ptr_with_offset` within bounds. - kani::assume(offset <= 1); - let ptr_with_offset: *const $type = test_ptr.wrapping_add(offset); + // 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: *const $type = generator.any_in_bounds().ptr; + let count: usize = kani::any(); unsafe { - ptr_with_offset.add(count); + test_ptr.add(count); } } }; ($type:ty, $proof_name:ident, sub) => { #[kani::proof_for_contract(<*const $type>::sub)] pub fn $proof_name() { - let mut test_val: $type = kani::any::<$type>(); - let offset: usize = kani::any(); + // 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: *const $type = generator.any_in_bounds().ptr; let count: usize = kani::any(); - let test_ptr: *const $type = &test_val; - - // For integer, composite, and unit types, 1 is the largest offset that - // keeps `ptr_with_offset` within bounds. - kani::assume(offset <= 1); - let ptr_with_offset: *const $type = test_ptr.wrapping_add(offset); unsafe { - ptr_with_offset.sub(count); + test_ptr.sub(count); } } }; ($type:ty, $proof_name:ident, offset) => { #[kani::proof_for_contract(<*const $type>::offset)] pub fn $proof_name() { - let mut test_val: $type = kani::any::<$type>(); - let offset: usize = kani::any(); + // 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: *const $type = generator.any_in_bounds().ptr; let count: isize = kani::any(); - let test_ptr: *const $type = &test_val; - - // For integer, composite, and unit types, 1 is the largest offset that - // keeps `ptr_with_offset` within bounds. - kani::assume(offset <= 1); - let ptr_with_offset: *const $type = test_ptr.wrapping_add(offset); unsafe { - ptr_with_offset.offset(count); + test_ptr.offset(count); } } }; From 5edd16e67d8301da8bb54d4fb5e668bbc9d3697f Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Tue, 26 Nov 2024 22:49:04 -0800 Subject: [PATCH 33/45] Reformatted code using rustfmt. --- library/core/src/ptr/const_ptr.rs | 33 +++++++++++++++++++------------ 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 32857714913fd..07204000594c2 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -118,7 +118,10 @@ impl *const T { /// println!("{:?}", unsafe { &*bad }); /// ``` #[unstable(feature = "set_ptr_value", issue = "75091")] - #[cfg_attr(bootstrap, rustc_const_stable(feature = "ptr_metadata_const", since = "1.83.0"))] + #[cfg_attr( + bootstrap, + rustc_const_stable(feature = "ptr_metadata_const", since = "1.83.0") + )] #[must_use = "returns a new pointer rather than modifying its argument"] #[inline] pub const fn with_metadata_of(self, meta: *const U) -> *const U @@ -421,7 +424,7 @@ impl *const T { )] // 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`. + // verifying that the result remains within the same allocation as `self`. #[ensures(|result| (core::mem::size_of::() == 0) || kani::mem::same_allocation(self, *result as *const T))] pub const unsafe fn offset(self, count: isize) -> *const T where @@ -949,7 +952,7 @@ impl *const T { )] // 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`. + // verifying that the result remains within the same allocation as `self`. #[ensures(|result| (core::mem::size_of::() == 0) || kani::mem::same_allocation(self, *result as *const T))] pub const unsafe fn add(self, count: usize) -> Self where @@ -1073,7 +1076,7 @@ impl *const T { )] // 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`. + // verifying that the result remains within the same allocation as `self`. #[ensures(|result| (core::mem::size_of::() == 0) || kani::mem::same_allocation(self, *result as *const T))] pub const unsafe fn sub(self, count: usize) -> Self where @@ -1972,7 +1975,7 @@ mod verify { let offset: usize = kani::any(); let count: isize = kani::any(); kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); - let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); + let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); unsafe { ptr_with_offset.offset(count); } @@ -1986,7 +1989,7 @@ mod verify { let offset: usize = kani::any(); let count: usize = kani::any(); kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); - let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); + let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); unsafe { ptr_with_offset.add(count); } @@ -2000,7 +2003,7 @@ mod verify { let offset: usize = kani::any(); let count: usize = kani::any(); kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); - let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); + let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); unsafe { ptr_with_offset.sub(count); } @@ -2028,7 +2031,7 @@ mod verify { check_const_offset_slice_tuple_1, check_const_add_slice_tuple_1, check_const_sub_slice_tuple_1 - ); + ); generate_slice_harnesses!( (f64, bool), check_const_offset_slice_tuple_2, @@ -2047,7 +2050,7 @@ mod verify { check_const_add_slice_tuple_4, check_const_sub_slice_tuple_4 ); - + /// This macro generates proofs for contracts on `add`, `sub`, and `offset` /// operations for pointers to integer, composite, and unit types. /// - `$type`: Specifies the pointee type. @@ -2106,7 +2109,7 @@ mod verify { generate_const_arithmetic_harness!(u32, check_const_add_u32, add); generate_const_arithmetic_harness!(u64, check_const_add_u64, add); generate_const_arithmetic_harness!(u128, check_const_add_u128, add); - generate_const_arithmetic_harness!(usize, check_const_add_usize, add); + generate_const_arithmetic_harness!(usize, check_const_add_usize, add); // <*const T>:: add() unit type verification generate_const_arithmetic_harness!((), check_const_add_unit, add); @@ -2138,7 +2141,7 @@ mod verify { generate_const_arithmetic_harness!((i8, i8), check_const_sub_tuple_1, sub); generate_const_arithmetic_harness!((f64, bool), check_const_sub_tuple_2, sub); generate_const_arithmetic_harness!((i32, f64, bool), check_const_sub_tuple_3, sub); - generate_const_arithmetic_harness!((i8, u16, i32, u64, isize), check_const_sub_tuple_4, sub); + generate_const_arithmetic_harness!((i8, u16, i32, u64, isize), check_const_sub_tuple_4, sub); // fn <*const T>::offset() integer types verification generate_const_arithmetic_harness!(i8, check_const_offset_i8, offset); @@ -2161,5 +2164,9 @@ mod verify { generate_const_arithmetic_harness!((i8, i8), check_const_offset_tuple_1, offset); generate_const_arithmetic_harness!((f64, bool), check_const_offset_tuple_2, offset); generate_const_arithmetic_harness!((i32, f64, bool), check_const_offset_tuple_3, offset); - generate_const_arithmetic_harness!((i8, u16, i32, u64, isize), check_const_offset_tuple_4, offset); -} \ No newline at end of file + generate_const_arithmetic_harness!( + (i8, u16, i32, u64, isize), + check_const_offset_tuple_4, + offset + ); +} From dd2a8eba74dd9e9c334051de99ef1f90fc455a75 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Tue, 26 Nov 2024 22:50:41 -0800 Subject: [PATCH 34/45] Reverted unnecessary rustfmt formatting --- library/core/src/ptr/const_ptr.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 07204000594c2..165d94819935c 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -118,10 +118,7 @@ impl *const T { /// println!("{:?}", unsafe { &*bad }); /// ``` #[unstable(feature = "set_ptr_value", issue = "75091")] - #[cfg_attr( - bootstrap, - rustc_const_stable(feature = "ptr_metadata_const", since = "1.83.0") - )] + #[cfg_attr(bootstrap, rustc_const_stable(feature = "ptr_metadata_const", since = "1.83.0"))] #[must_use = "returns a new pointer rather than modifying its argument"] #[inline] pub const fn with_metadata_of(self, meta: *const U) -> *const U From 576483f85f23c8bfbd6f58e3b9559bc9221df3b2 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Thu, 28 Nov 2024 09:54:18 -0800 Subject: [PATCH 35/45] Resolved compilation error after previous merge. --- library/core/src/ptr/const_ptr.rs | 89 +++++++++++++++++++++++++------ 1 file changed, 74 insertions(+), 15 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 7f2a60682ed6c..8e080cf3eb182 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1963,6 +1963,7 @@ impl PartialOrd for *const T { mod verify { use crate::kani; use core::mem; + use kani::PointerGenerator; // Constant for array size used in all tests const ARRAY_SIZE: usize = 5; @@ -2019,18 +2020,78 @@ mod verify { } // Generate slice harnesses for various types (offset, add, sub) - generate_slice_harnesses!(i8, check_const_offset_slice_i8, check_const_add_slice_i8, check_const_sub_slice_i8); - generate_slice_harnesses!(i16, check_const_offset_slice_i16, check_const_add_slice_i16, check_const_sub_slice_i16); - generate_slice_harnesses!(i32, check_const_offset_slice_i32, check_const_add_slice_i32, check_const_sub_slice_i32); - generate_slice_harnesses!(i64, check_const_offset_slice_i64, check_const_add_slice_i64, check_const_sub_slice_i64); - generate_slice_harnesses!(i128, check_const_offset_slice_i128, check_const_add_slice_i128, check_const_sub_slice_i128); - generate_slice_harnesses!(isize, check_const_offset_slice_isize, check_const_add_slice_isize, check_const_sub_slice_isize); - generate_slice_harnesses!(u8, check_const_offset_slice_u8, check_const_add_slice_u8, check_const_sub_slice_u8); - generate_slice_harnesses!(u16, check_const_offset_slice_u16, check_const_add_slice_u16, check_const_sub_slice_u16); - generate_slice_harnesses!(u32, check_const_offset_slice_u32, check_const_add_slice_u32, check_const_sub_slice_u32); - generate_slice_harnesses!(u64, check_const_offset_slice_u64, check_const_add_slice_u64, check_const_sub_slice_u64); - generate_slice_harnesses!(u128, check_const_offset_slice_u128, check_const_add_slice_u128, check_const_sub_slice_u128); - generate_slice_harnesses!(usize, check_const_offset_slice_usize, check_const_add_slice_usize, check_const_sub_slice_usize); + generate_slice_harnesses!( + i8, + check_const_offset_slice_i8, + check_const_add_slice_i8, + check_const_sub_slice_i8 + ); + generate_slice_harnesses!( + i16, + check_const_offset_slice_i16, + check_const_add_slice_i16, + check_const_sub_slice_i16 + ); + generate_slice_harnesses!( + i32, + check_const_offset_slice_i32, + check_const_add_slice_i32, + check_const_sub_slice_i32 + ); + generate_slice_harnesses!( + i64, + check_const_offset_slice_i64, + check_const_add_slice_i64, + check_const_sub_slice_i64 + ); + generate_slice_harnesses!( + i128, + check_const_offset_slice_i128, + check_const_add_slice_i128, + check_const_sub_slice_i128 + ); + generate_slice_harnesses!( + isize, + check_const_offset_slice_isize, + check_const_add_slice_isize, + check_const_sub_slice_isize + ); + generate_slice_harnesses!( + u8, + check_const_offset_slice_u8, + check_const_add_slice_u8, + check_const_sub_slice_u8 + ); + generate_slice_harnesses!( + u16, + check_const_offset_slice_u16, + check_const_add_slice_u16, + check_const_sub_slice_u16 + ); + generate_slice_harnesses!( + u32, + check_const_offset_slice_u32, + check_const_add_slice_u32, + check_const_sub_slice_u32 + ); + generate_slice_harnesses!( + u64, + check_const_offset_slice_u64, + check_const_add_slice_u64, + check_const_sub_slice_u64 + ); + generate_slice_harnesses!( + u128, + check_const_offset_slice_u128, + check_const_add_slice_u128, + check_const_sub_slice_u128 + ); + generate_slice_harnesses!( + usize, + check_const_offset_slice_usize, + check_const_add_slice_usize, + check_const_sub_slice_usize + ); // Generate slice harnesses for tuples (offset, add, sub) generate_slice_harnesses!( @@ -2175,8 +2236,7 @@ mod verify { (i8, u16, i32, u64, isize), check_const_offset_tuple_4, offset - - use kani::PointerGenerator; + ); // Proof for unit size will panic as offset_from needs the pointee size to be greater then 0 #[kani::proof_for_contract(<*const ()>::offset_from)] @@ -2294,7 +2354,6 @@ mod verify { check_const_offset_from_isize, check_const_offset_from_isize_arr ); - generate_offset_from_harness!( (i8, i8), check_const_offset_from_tuple_1, From 330f06b154c55cd89c8629320907fb0033242bf5 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Thu, 28 Nov 2024 10:04:33 -0800 Subject: [PATCH 36/45] Enhanced comments to clarify proof for contracts. --- library/core/src/ptr/const_ptr.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 8e080cf3eb182..f05e27db58385 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -2293,6 +2293,7 @@ mod verify { }; } + // fn <*const T>::offset_from() integer and integer slice types verification generate_offset_from_harness!( u8, check_const_offset_from_u8, @@ -2323,7 +2324,6 @@ mod verify { check_const_offset_from_usize, check_const_offset_from_usize_arr ); - generate_offset_from_harness!( i8, check_const_offset_from_i8, @@ -2354,6 +2354,8 @@ mod verify { check_const_offset_from_isize, check_const_offset_from_isize_arr ); + + // fn <*const T>::offset_from() typle and tuple slice types verification generate_offset_from_harness!( (i8, i8), check_const_offset_from_tuple_1, From 43a456bdaa246bae41ef5ebe55bafe020af9b525 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Thu, 28 Nov 2024 19:10:09 -0800 Subject: [PATCH 37/45] Refactored macro for generating slice type verifications to reduce duplication. --- library/core/src/ptr/const_ptr.rs | 69 +++++++++++++------------------ 1 file changed, 28 insertions(+), 41 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index f05e27db58385..0c937ef06d43a 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1964,58 +1964,45 @@ mod verify { use crate::kani; use core::mem; use kani::PointerGenerator; + // Constant for array size used in all tests const ARRAY_SIZE: usize = 5; - /// This macro generates verification harnesses for the `offset`, `add`, and `sub` - /// pointer operations for a slice type and function name. - /// - `$ty`: The type of the array (e.g., i32, u32, tuples). - /// - `$offset_fn`: The function name for the `offset` operation. - /// - `$add_fn`: The function name for the `add` operation. - /// - `$sub_fn`: The function name for the `sub` operation. - macro_rules! generate_slice_harnesses { - ($ty:ty, $offset_fn:ident, $add_fn:ident, $sub_fn:ident) => { - // Generates a harness for the `offset` operation - #[kani::proof_for_contract(<*const $ty>::offset)] - fn $offset_fn() { - let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array(); - let test_ptr: *const $ty = arr.as_ptr(); - let offset: usize = kani::any(); - let count: isize = kani::any(); - kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); - let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); - unsafe { - ptr_with_offset.offset(count); - } - } - - // Generates a harness for the `add` operation - #[kani::proof_for_contract(<*const $ty>::add)] - fn $add_fn() { - let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array(); - let test_ptr: *const $ty = arr.as_ptr(); - let offset: usize = kani::any(); - let count: usize = kani::any(); - kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); - let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); - unsafe { - ptr_with_offset.add(count); - } - } - - // Generates a harness for the `sub` operation - #[kani::proof_for_contract(<*const $ty>::sub)] - fn $sub_fn() { + /// This macro generates a single verification harness for the `offset`, `add`, or `sub` + /// pointer operations for a slice type. + /// - `$ty`: The type of the array'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. + macro_rules! generate_single_slice_harness { + ($ty:ty, $proof_name:ident, $fn_name:ident, $count_ty:ty) => { + #[kani::proof_for_contract(<*const $ty>::$fn_name)] + fn $proof_name() { let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array(); let test_ptr: *const $ty = arr.as_ptr(); let offset: usize = kani::any(); - let count: usize = kani::any(); kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); + + let count: $count_ty = kani::any(); unsafe { - ptr_with_offset.sub(count); + ptr_with_offset.$fn_name(count); } } + } + } + + /// This macro generates verification harnesses for the `offset`, `add`, and `sub` + /// pointer operations for a slice type. + /// - `$ty`: The type of the array (e.g., i32, u32, tuples). + /// - `$offset_fn_name`: The function name for the `offset` operation. + /// - `$add_fn_name`: The function name for the `add` operation. + /// - `$sub_fn_name`: The function name for the `sub` operation. + macro_rules! generate_slice_harnesses { + ($ty:ty, $offset_fn_name:ident, $add_fn_name:ident, $sub_fn_name:ident) => { + generate_single_slice_harness!($ty, $add_fn_name, add, usize); + generate_single_slice_harness!($ty, $sub_fn_name, sub, usize); + generate_single_slice_harness!($ty, $offset_fn_name, offset, isize); }; } From 90fc86aad659ba9fd0b85be9b2b1f897ac62937b Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Thu, 28 Nov 2024 19:51:41 -0800 Subject: [PATCH 38/45] Fixed proof naming issue in previous commit; Refactored the macro for integer, composite and unit types verification --- library/core/src/ptr/const_ptr.rs | 321 ++++++++++++++++-------------- 1 file changed, 177 insertions(+), 144 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 0c937ef06d43a..c6c123f63e510 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1974,6 +1974,10 @@ mod verify { /// - `$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_slice_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_slice_harness { ($ty:ty, $proof_name:ident, $fn_name:ident, $count_ty:ty) => { #[kani::proof_for_contract(<*const $ty>::$fn_name)] @@ -1983,15 +1987,15 @@ mod verify { let offset: usize = kani::any(); kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); - + let count: $count_ty = kani::any(); unsafe { ptr_with_offset.$fn_name(count); } } - } + }; } - + /// This macro generates verification harnesses for the `offset`, `add`, and `sub` /// pointer operations for a slice type. /// - `$ty`: The type of the array (e.g., i32, u32, tuples). @@ -2006,223 +2010,252 @@ mod verify { }; } - // Generate slice harnesses for various types (offset, add, sub) + // Generate slice harnesses for various types (add, sub, offset) generate_slice_harnesses!( i8, - check_const_offset_slice_i8, check_const_add_slice_i8, - check_const_sub_slice_i8 + check_const_sub_slice_i8, + check_const_offset_slice_i8 ); generate_slice_harnesses!( i16, - check_const_offset_slice_i16, check_const_add_slice_i16, - check_const_sub_slice_i16 + check_const_sub_slice_i16, + check_const_offset_slice_i16 ); generate_slice_harnesses!( i32, - check_const_offset_slice_i32, check_const_add_slice_i32, - check_const_sub_slice_i32 + check_const_sub_slice_i32, + check_const_offset_slice_i32 ); generate_slice_harnesses!( i64, - check_const_offset_slice_i64, check_const_add_slice_i64, - check_const_sub_slice_i64 + check_const_sub_slice_i64, + check_const_offset_slice_i64 ); generate_slice_harnesses!( i128, - check_const_offset_slice_i128, check_const_add_slice_i128, - check_const_sub_slice_i128 + check_const_sub_slice_i128, + check_const_offset_slice_i128 ); generate_slice_harnesses!( isize, - check_const_offset_slice_isize, check_const_add_slice_isize, - check_const_sub_slice_isize + check_const_sub_slice_isize, + check_const_offset_slice_isize ); generate_slice_harnesses!( u8, - check_const_offset_slice_u8, check_const_add_slice_u8, - check_const_sub_slice_u8 + check_const_sub_slice_u8, + check_const_offset_slice_u8 ); generate_slice_harnesses!( u16, - check_const_offset_slice_u16, check_const_add_slice_u16, - check_const_sub_slice_u16 + check_const_sub_slice_u16, + check_const_offset_slice_u16 ); generate_slice_harnesses!( u32, - check_const_offset_slice_u32, check_const_add_slice_u32, - check_const_sub_slice_u32 + check_const_sub_slice_u32, + check_const_offset_slice_u32 ); generate_slice_harnesses!( u64, - check_const_offset_slice_u64, check_const_add_slice_u64, - check_const_sub_slice_u64 + check_const_sub_slice_u64, + check_const_offset_slice_u64 ); generate_slice_harnesses!( u128, - check_const_offset_slice_u128, check_const_add_slice_u128, - check_const_sub_slice_u128 + check_const_sub_slice_u128, + check_const_offset_slice_u128 ); generate_slice_harnesses!( usize, - check_const_offset_slice_usize, check_const_add_slice_usize, - check_const_sub_slice_usize + check_const_sub_slice_usize, + check_const_offset_slice_usize ); - // Generate slice harnesses for tuples (offset, add, sub) + // Generate slice harnesses for tuples (add, sub, offset) generate_slice_harnesses!( (i8, i8), - check_const_offset_slice_tuple_1, check_const_add_slice_tuple_1, - check_const_sub_slice_tuple_1 + check_const_sub_slice_tuple_1, + check_const_offset_slice_tuple_1 ); generate_slice_harnesses!( (f64, bool), - check_const_offset_slice_tuple_2, check_const_add_slice_tuple_2, - check_const_sub_slice_tuple_2 + check_const_sub_slice_tuple_2, + check_const_offset_slice_tuple_2 ); generate_slice_harnesses!( (i32, f64, bool), - check_const_offset_slice_tuple_3, check_const_add_slice_tuple_3, - check_const_sub_slice_tuple_3 + check_const_sub_slice_tuple_3, + check_const_offset_slice_tuple_3 ); generate_slice_harnesses!( (i8, u16, i32, u64, isize), - check_const_offset_slice_tuple_4, check_const_add_slice_tuple_4, - check_const_sub_slice_tuple_4 + check_const_sub_slice_tuple_4, + check_const_offset_slice_tuple_4 ); - /// This macro generates proofs for contracts on `add`, `sub`, and `offset` - /// operations for pointers to integer, composite, and unit types. - /// - `$type`: Specifies the pointee type. - /// - `$proof_name`: Specifies the name of the generated proof for contract. - macro_rules! generate_const_arithmetic_harness { - ($type:ty, $proof_name:ident, add) => { - #[kani::proof_for_contract(<*const $type>::add)] - 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: *const $type = generator.any_in_bounds().ptr; - let count: usize = kani::any(); - unsafe { - test_ptr.add(count); - } - } - }; - ($type:ty, $proof_name:ident, sub) => { - #[kani::proof_for_contract(<*const $type>::sub)] + /// 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 array'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(<*const $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: *const $type = generator.any_in_bounds().ptr; - let count: usize = kani::any(); + let test_ptr: *const $ty = generator.any_in_bounds().ptr; + let count: $count_ty = kani::any(); unsafe { - test_ptr.sub(count); + test_ptr.$fn_name(count); } } }; - ($type:ty, $proof_name:ident, offset) => { - #[kani::proof_for_contract(<*const $type>::offset)] - 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: *const $type = generator.any_in_bounds().ptr; - let count: isize = kani::any(); - unsafe { - test_ptr.offset(count); - } - } + } + + /// This macro generates verification harnesses for the `offset`, `add`, and `sub` + /// pointer operations, supporting integer, composite, or unit types. + /// - `$ty`: The type of the array (e.g., i32, u32, tuples). + /// - `$offset_fn_name`: The function name for the `offset` contract. + /// - `$add_fn_name`: The function name for the `add` proof for contract. + /// - `$sub_fn_name`: The function name for the `sub` proof for contract. + macro_rules! generate_arithmetic_harnesses { + ($ty:ty, $offset_fn_name:ident, $add_fn_name:ident, $sub_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); }; } - // <*const T>:: add() integer types verification - generate_const_arithmetic_harness!(i8, check_const_add_i8, add); - generate_const_arithmetic_harness!(i16, check_const_add_i16, add); - generate_const_arithmetic_harness!(i32, check_const_add_i32, add); - generate_const_arithmetic_harness!(i64, check_const_add_i64, add); - generate_const_arithmetic_harness!(i128, check_const_add_i128, add); - generate_const_arithmetic_harness!(isize, check_const_add_isize, add); - generate_const_arithmetic_harness!(u8, check_const_add_u8, add); - generate_const_arithmetic_harness!(u16, check_const_add_u16, add); - generate_const_arithmetic_harness!(u32, check_const_add_u32, add); - generate_const_arithmetic_harness!(u64, check_const_add_u64, add); - generate_const_arithmetic_harness!(u128, check_const_add_u128, add); - generate_const_arithmetic_harness!(usize, check_const_add_usize, add); - - // <*const T>:: add() unit type verification - generate_const_arithmetic_harness!((), check_const_add_unit, add); - - // <*const T>:: add() composite types verification - generate_const_arithmetic_harness!((i8, i8), check_const_add_tuple_1, add); - generate_const_arithmetic_harness!((f64, bool), check_const_add_tuple_2, add); - generate_const_arithmetic_harness!((i32, f64, bool), check_const_add_tuple_3, add); - generate_const_arithmetic_harness!((i8, u16, i32, u64, isize), check_const_add_tuple_4, add); - - // <*const T>:: sub() integer types verification - generate_const_arithmetic_harness!(i8, check_const_sub_i8, sub); - generate_const_arithmetic_harness!(i16, check_const_sub_i16, sub); - generate_const_arithmetic_harness!(i32, check_const_sub_i32, sub); - generate_const_arithmetic_harness!(i64, check_const_sub_i64, sub); - generate_const_arithmetic_harness!(i128, check_const_sub_i128, sub); - generate_const_arithmetic_harness!(isize, check_const_sub_isize, sub); - generate_const_arithmetic_harness!(u8, check_const_sub_u8, sub); - generate_const_arithmetic_harness!(u16, check_const_sub_u16, sub); - generate_const_arithmetic_harness!(u32, check_const_sub_u32, sub); - generate_const_arithmetic_harness!(u64, check_const_sub_u64, sub); - generate_const_arithmetic_harness!(u128, check_const_sub_u128, sub); - generate_const_arithmetic_harness!(usize, check_const_sub_usize, sub); - - // <*const T>:: sub() unit type verification - generate_const_arithmetic_harness!((), check_const_sub_unit, sub); - - // <*const T>:: sub() composite types verification - generate_const_arithmetic_harness!((i8, i8), check_const_sub_tuple_1, sub); - generate_const_arithmetic_harness!((f64, bool), check_const_sub_tuple_2, sub); - generate_const_arithmetic_harness!((i32, f64, bool), check_const_sub_tuple_3, sub); - generate_const_arithmetic_harness!((i8, u16, i32, u64, isize), check_const_sub_tuple_4, sub); - - // fn <*const T>::offset() integer types verification - generate_const_arithmetic_harness!(i8, check_const_offset_i8, offset); - generate_const_arithmetic_harness!(i16, check_const_offset_i16, offset); - generate_const_arithmetic_harness!(i32, check_const_offset_i32, offset); - generate_const_arithmetic_harness!(i64, check_const_offset_i64, offset); - generate_const_arithmetic_harness!(i128, check_const_offset_i128, offset); - generate_const_arithmetic_harness!(isize, check_const_offset_isize, offset); - generate_const_arithmetic_harness!(u8, check_const_offset_u8, offset); - generate_const_arithmetic_harness!(u16, check_const_offset_u16, offset); - generate_const_arithmetic_harness!(u32, check_const_offset_u32, offset); - generate_const_arithmetic_harness!(u64, check_const_offset_u64, offset); - generate_const_arithmetic_harness!(u128, check_const_offset_u128, offset); - generate_const_arithmetic_harness!(usize, check_const_offset_usize, offset); - - // fn <*const T>::offset() unit type verification - generate_const_arithmetic_harness!((), check_const_offset_unit, offset); - - // fn <*const T>::offset() composite type verification - generate_const_arithmetic_harness!((i8, i8), check_const_offset_tuple_1, offset); - generate_const_arithmetic_harness!((f64, bool), check_const_offset_tuple_2, offset); - generate_const_arithmetic_harness!((i32, f64, bool), check_const_offset_tuple_3, offset); - generate_const_arithmetic_harness!( + // Generate harnesses for integer types (add, sub, offset) + generate_arithmetic_harnesses!( + i8, + check_const_add_i8, + check_const_sub_i8, + check_const_offset_i8 + ); + generate_arithmetic_harnesses!( + i16, + check_const_add_i16, + check_const_sub_i16, + check_const_offset_i16 + ); + generate_arithmetic_harnesses!( + i32, + check_const_add_i32, + check_const_sub_i32, + check_const_offset_i32 + ); + generate_arithmetic_harnesses!( + i64, + check_const_add_i64, + check_const_sub_i64, + check_const_offset_i64 + ); + generate_arithmetic_harnesses!( + i128, + check_const_add_i128, + check_const_sub_i128, + check_const_offset_i128 + ); + generate_arithmetic_harnesses!( + isize, + check_const_add_isize, + check_const_sub_isize, + check_const_offset_isize + ); + generate_arithmetic_harnesses!( + u8, + check_const_add_u8, + check_const_sub_u8, + check_const_offset_u8 + ); + generate_arithmetic_harnesses!( + u16, + check_const_add_u16, + check_const_sub_u16, + check_const_offset_u16 + ); + generate_arithmetic_harnesses!( + u32, + check_const_add_u32, + check_const_sub_u32, + check_const_offset_u32 + ); + generate_arithmetic_harnesses!( + u64, + check_const_add_u64, + check_const_sub_u64, + check_const_offset_u64 + ); + generate_arithmetic_harnesses!( + u128, + check_const_add_u128, + check_const_sub_u128, + check_const_offset_u128 + ); + generate_arithmetic_harnesses!( + usize, + check_const_add_usize, + check_const_sub_usize, + check_const_offset_usize + ); + + // Generate harnesses for unit type (add, sub, offset) + generate_arithmetic_harnesses!( + (), + check_const_add_unit, + check_const_sub_unit, + check_const_offset_unit + ); + + // Generte harnesses for composite types (add, sub, offset) + generate_arithmetic_harnesses!( + (i8, i8), + check_const_add_tuple_1, + check_const_sub_tuple_1, + check_const_offset_tuple_1 + ); + generate_arithmetic_harnesses!( + (f64, bool), + check_const_add_tuple_2, + check_const_sub_tuple_2, + check_const_offset_tuple_2 + ); + generate_arithmetic_harnesses!( + (i32, f64, bool), + check_const_add_tuple_3, + check_const_sub_tuple_3, + check_const_offset_tuple_3 + ); + generate_arithmetic_harnesses!( (i8, u16, i32, u64, isize), - check_const_offset_tuple_4, - offset + check_const_add_tuple_4, + check_const_sub_tuple_4, + check_const_offset_tuple_4 ); // Proof for unit size will panic as offset_from needs the pointee size to be greater then 0 @@ -2237,7 +2270,7 @@ mod verify { } } - // Array size bound for kani::any_array + // Array size bound for kani::any_array for `offset_from` verification const ARRAY_LEN: usize = 40; macro_rules! generate_offset_from_harness { @@ -2342,7 +2375,7 @@ mod verify { check_const_offset_from_isize_arr ); - // fn <*const T>::offset_from() typle and tuple slice types verification + // fn <*const T>::offset_from() tuple and tuple slice types verification generate_offset_from_harness!( (i8, i8), check_const_offset_from_tuple_1, From 9a2ee76ca21a701fc0bf3880d06e2c565063f013 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Thu, 28 Nov 2024 20:12:26 -0800 Subject: [PATCH 39/45] Formatted code using rustfmt. --- library/core/src/ptr/const_ptr.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index c6c123f63e510..b96e724ee53af 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1974,9 +1974,9 @@ mod verify { /// - `$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_slice_harnesses` macro. Its purpose is to reduce code duplication, + /// + /// Note: This macro is intended for internal use only and should be invoked exclusively + /// by the `generate_slice_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_slice_harness { ($ty:ty, $proof_name:ident, $fn_name:ident, $count_ty:ty) => { @@ -2116,9 +2116,9 @@ mod verify { /// - `$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, + /// + /// 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) => { From d783daccd1bd52c3bd46eb58ef5bf6211f1da3ab Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Thu, 28 Nov 2024 20:24:45 -0800 Subject: [PATCH 40/45] Fixed function naming issues after refactoring. --- library/core/src/ptr/const_ptr.rs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index b96e724ee53af..2bf989ffdce0a 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1999,11 +1999,11 @@ mod verify { /// This macro generates verification harnesses for the `offset`, `add`, and `sub` /// pointer operations for a slice type. /// - `$ty`: The type of the array (e.g., i32, u32, tuples). - /// - `$offset_fn_name`: The function name for the `offset` operation. - /// - `$add_fn_name`: The function name for the `add` operation. - /// - `$sub_fn_name`: The function name for the `sub` operation. + /// - `$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_slice_harnesses { - ($ty:ty, $offset_fn_name:ident, $add_fn_name:ident, $sub_fn_name:ident) => { + ($ty:ty, $add_fn_name:ident, $sub_fn_name:ident, $offset_fn_name:ident) => { generate_single_slice_harness!($ty, $add_fn_name, add, usize); generate_single_slice_harness!($ty, $sub_fn_name, sub, usize); generate_single_slice_harness!($ty, $offset_fn_name, offset, isize); @@ -2139,11 +2139,11 @@ mod verify { /// This macro generates verification harnesses for the `offset`, `add`, and `sub` /// pointer operations, supporting integer, composite, or unit types. /// - `$ty`: The type of the array (e.g., i32, u32, tuples). - /// - `$offset_fn_name`: The function name for the `offset` contract. - /// - `$add_fn_name`: The function name for the `add` proof for contract. - /// - `$sub_fn_name`: The function name for the `sub` proof for contract. + /// - `$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, $offset_fn_name:ident, $add_fn_name:ident, $sub_fn_name:ident) => { + ($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); From d7ee4d0576b1d4fb5cb153b11ed480bbee1b3494 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Fri, 29 Nov 2024 09:48:59 -0800 Subject: [PATCH 41/45] Fixed issues in comments --- library/core/src/ptr/const_ptr.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 2bf989ffdce0a..1d8a773e2390d 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -2112,7 +2112,7 @@ mod verify { /// 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 array's elements (e.g., `i32`, `u32`, tuples). + /// - `$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. @@ -2138,7 +2138,7 @@ mod verify { /// This macro generates verification harnesses for the `offset`, `add`, and `sub` /// pointer operations, supporting integer, composite, or unit types. - /// - `$ty`: The type of the array (e.g., i32, u32, tuples). + /// - `$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. From 6ee79412ea70a8e431243d9c9f27dd6cdf999653 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Mon, 2 Dec 2024 12:43:38 -0800 Subject: [PATCH 42/45] Refactored contracts to improve performance --- library/core/src/ptr/const_ptr.rs | 37 +++++++++++++++++++------------ 1 file changed, 23 insertions(+), 14 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 1d8a773e2390d..40540f464c7c2 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -410,10 +410,13 @@ impl *const T { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires( - // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize` - count.checked_mul(core::mem::size_of::() as isize).is_some() && - // Precondition 2: adding the computed offset to `self` does not cause overflow - (self as isize).checked_add((count * core::mem::size_of::() as isize)).is_some() && + // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize`. + if let Some(computed_offset) = count.checked_mul(core::mem::size_of::() as isize) { + // Precondition 2: adding the computed offset to `self` does not cause overflow. + (self as isize).checked_add(computed_offset).is_some() + } else { + false + } && // 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. @@ -947,11 +950,14 @@ impl *const T { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires( - // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize` - count.checked_mul(core::mem::size_of::()).is_some() && - count * core::mem::size_of::() <= isize::MAX as usize && - // Precondition 2: adding the computed offset to `self` does not cause overflow - (self as isize).checked_add((count * core::mem::size_of::()) as isize).is_some() && + // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize`. + if let Some(computed_offset) = count.checked_mul(core::mem::size_of::()) { + computed_offset <= isize::MAX as usize && + // Precondition 2: adding the computed offset to `self` does not cause overflow. + (self as isize).checked_add(computed_offset as isize).is_some() + } else { + false + } && // 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. @@ -1071,11 +1077,14 @@ impl *const T { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires( - // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize` - count.checked_mul(core::mem::size_of::()).is_some() && - count * core::mem::size_of::() <= isize::MAX as usize && - // Precondition 2: subtracting the computed offset from `self` does not cause overflow - (self as isize).checked_sub((count * core::mem::size_of::()) as isize).is_some() && + // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize`. + if let Some(computed_offset) = count.checked_mul(core::mem::size_of::()) { + computed_offset <= isize::MAX as usize && + // Precondition 2: substracting the computed offset from `self` does not cause overflow. + (self as isize).checked_sub(computed_offset as isize).is_some() + } else { + false + } && // 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. From 0573c74f6038fd0ef6e2bf4d602d86517fd9954d Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Mon, 2 Dec 2024 21:05:30 -0800 Subject: [PATCH 43/45] Replaced kani::mem::same_allocation with core::ub_checks::same_allocation; Rearranged proofs --- library/core/src/ptr/const_ptr.rs | 54 +++++++++++++++---------------- 1 file changed, 27 insertions(+), 27 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 40540f464c7c2..edd080d39b346 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -420,12 +420,12 @@ impl *const 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, *result as *const T))] + #[ensures(|result| (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self, *result as *const T))] pub const unsafe fn offset(self, count: isize) -> *const T where T: Sized, @@ -694,7 +694,7 @@ impl *const T { // Ensure the distance between `self` and `origin` is aligned to `T` (self as isize - origin as isize) % (mem::size_of::() as isize) == 0 && // Ensure both pointers are in the same allocation or are pointing to the same address - (self as isize == origin as isize || kani::mem::same_allocation(self, origin)) + (self as isize == origin as isize || core::ub_checks::same_allocation(self, origin)) )] // The result should equal the distance in terms of elements of type `T` as per the documentation above #[ensures(|result| *result == (self as isize - origin as isize) / (mem::size_of::() as isize))] @@ -961,12 +961,12 @@ impl *const 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, *result as *const T))] + #[ensures(|result| (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self, *result as *const T))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -1088,12 +1088,12 @@ impl *const 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, *result as *const T))] + #[ensures(|result| (core::mem::size_of::() == 0) || core::ub_checks::same_allocation(self, *result as *const T))] pub const unsafe fn sub(self, count: usize) -> Self where T: Sized, @@ -2159,6 +2159,14 @@ mod verify { }; } + // Generate harnesses for unit type (add, sub, offset) + generate_arithmetic_harnesses!( + (), + check_const_add_unit, + check_const_sub_unit, + check_const_offset_unit + ); + // Generate harnesses for integer types (add, sub, offset) generate_arithmetic_harnesses!( i8, @@ -2233,14 +2241,6 @@ mod verify { check_const_offset_usize ); - // Generate harnesses for unit type (add, sub, offset) - generate_arithmetic_harnesses!( - (), - check_const_add_unit, - check_const_sub_unit, - check_const_offset_unit - ); - // Generte harnesses for composite types (add, sub, offset) generate_arithmetic_harnesses!( (i8, i8), @@ -2267,18 +2267,6 @@ mod verify { check_const_offset_tuple_4 ); - // Proof for unit size will panic as offset_from needs the pointee size to be greater then 0 - #[kani::proof_for_contract(<*const ()>::offset_from)] - #[kani::should_panic] - pub fn check_const_offset_from_unit() { - let val: () = (); - let src_ptr: *const () = &val; - let dest_ptr: *const () = &val; - unsafe { - dest_ptr.offset_from(src_ptr); - } - } - // Array size bound for kani::any_array for `offset_from` verification const ARRAY_LEN: usize = 40; @@ -2322,6 +2310,18 @@ mod verify { }; } + // Proof for unit size will panic as offset_from needs the pointee size to be greater then 0 + #[kani::proof_for_contract(<*const ()>::offset_from)] + #[kani::should_panic] + pub fn check_const_offset_from_unit() { + let val: () = (); + let src_ptr: *const () = &val; + let dest_ptr: *const () = &val; + unsafe { + dest_ptr.offset_from(src_ptr); + } + } + // fn <*const T>::offset_from() integer and integer slice types verification generate_offset_from_harness!( u8, From 81afaf92ef50d143886240f2d00e3e8d7bab9b7f Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Mon, 2 Dec 2024 21:36:15 -0800 Subject: [PATCH 44/45] Rearranged proofs, moving the unit type proof to the top --- library/core/src/ptr/const_ptr.rs | 290 +++++++++++++++--------------- 1 file changed, 145 insertions(+), 145 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index edd080d39b346..18124b75856cf 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1974,151 +1974,6 @@ mod verify { use core::mem; use kani::PointerGenerator; - // Constant for array size used in all tests - const ARRAY_SIZE: usize = 5; - - /// This macro generates a single verification harness for the `offset`, `add`, or `sub` - /// pointer operations for a slice type. - /// - `$ty`: The type of the array'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_slice_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_slice_harness { - ($ty:ty, $proof_name:ident, $fn_name:ident, $count_ty:ty) => { - #[kani::proof_for_contract(<*const $ty>::$fn_name)] - fn $proof_name() { - let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array(); - let test_ptr: *const $ty = arr.as_ptr(); - let offset: usize = kani::any(); - kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); - let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); - - let count: $count_ty = kani::any(); - unsafe { - ptr_with_offset.$fn_name(count); - } - } - }; - } - - /// This macro generates verification harnesses for the `offset`, `add`, and `sub` - /// pointer operations for a slice type. - /// - `$ty`: The type of the array (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_slice_harnesses { - ($ty:ty, $add_fn_name:ident, $sub_fn_name:ident, $offset_fn_name:ident) => { - generate_single_slice_harness!($ty, $add_fn_name, add, usize); - generate_single_slice_harness!($ty, $sub_fn_name, sub, usize); - generate_single_slice_harness!($ty, $offset_fn_name, offset, isize); - }; - } - - // Generate slice harnesses for various types (add, sub, offset) - generate_slice_harnesses!( - i8, - check_const_add_slice_i8, - check_const_sub_slice_i8, - check_const_offset_slice_i8 - ); - generate_slice_harnesses!( - i16, - check_const_add_slice_i16, - check_const_sub_slice_i16, - check_const_offset_slice_i16 - ); - generate_slice_harnesses!( - i32, - check_const_add_slice_i32, - check_const_sub_slice_i32, - check_const_offset_slice_i32 - ); - generate_slice_harnesses!( - i64, - check_const_add_slice_i64, - check_const_sub_slice_i64, - check_const_offset_slice_i64 - ); - generate_slice_harnesses!( - i128, - check_const_add_slice_i128, - check_const_sub_slice_i128, - check_const_offset_slice_i128 - ); - generate_slice_harnesses!( - isize, - check_const_add_slice_isize, - check_const_sub_slice_isize, - check_const_offset_slice_isize - ); - generate_slice_harnesses!( - u8, - check_const_add_slice_u8, - check_const_sub_slice_u8, - check_const_offset_slice_u8 - ); - generate_slice_harnesses!( - u16, - check_const_add_slice_u16, - check_const_sub_slice_u16, - check_const_offset_slice_u16 - ); - generate_slice_harnesses!( - u32, - check_const_add_slice_u32, - check_const_sub_slice_u32, - check_const_offset_slice_u32 - ); - generate_slice_harnesses!( - u64, - check_const_add_slice_u64, - check_const_sub_slice_u64, - check_const_offset_slice_u64 - ); - generate_slice_harnesses!( - u128, - check_const_add_slice_u128, - check_const_sub_slice_u128, - check_const_offset_slice_u128 - ); - generate_slice_harnesses!( - usize, - check_const_add_slice_usize, - check_const_sub_slice_usize, - check_const_offset_slice_usize - ); - - // Generate slice harnesses for tuples (add, sub, offset) - generate_slice_harnesses!( - (i8, i8), - check_const_add_slice_tuple_1, - check_const_sub_slice_tuple_1, - check_const_offset_slice_tuple_1 - ); - generate_slice_harnesses!( - (f64, bool), - check_const_add_slice_tuple_2, - check_const_sub_slice_tuple_2, - check_const_offset_slice_tuple_2 - ); - generate_slice_harnesses!( - (i32, f64, bool), - check_const_add_slice_tuple_3, - check_const_sub_slice_tuple_3, - check_const_offset_slice_tuple_3 - ); - generate_slice_harnesses!( - (i8, u16, i32, u64, isize), - check_const_add_slice_tuple_4, - check_const_sub_slice_tuple_4, - check_const_offset_slice_tuple_4 - ); - /// 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). @@ -2267,6 +2122,151 @@ mod verify { check_const_offset_tuple_4 ); + // Constant for array size used in all tests + const ARRAY_SIZE: usize = 5; + + /// This macro generates a single verification harness for the `offset`, `add`, or `sub` + /// pointer operations for a slice type. + /// - `$ty`: The type of the array'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_slice_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_slice_harness { + ($ty:ty, $proof_name:ident, $fn_name:ident, $count_ty:ty) => { + #[kani::proof_for_contract(<*const $ty>::$fn_name)] + fn $proof_name() { + let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array(); + let test_ptr: *const $ty = arr.as_ptr(); + let offset: usize = kani::any(); + kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); + let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset); + + let count: $count_ty = kani::any(); + unsafe { + ptr_with_offset.$fn_name(count); + } + } + }; + } + + /// This macro generates verification harnesses for the `offset`, `add`, and `sub` + /// pointer operations for a slice type. + /// - `$ty`: The type of the array (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_slice_harnesses { + ($ty:ty, $add_fn_name:ident, $sub_fn_name:ident, $offset_fn_name:ident) => { + generate_single_slice_harness!($ty, $add_fn_name, add, usize); + generate_single_slice_harness!($ty, $sub_fn_name, sub, usize); + generate_single_slice_harness!($ty, $offset_fn_name, offset, isize); + }; + } + + // Generate slice harnesses for various types (add, sub, offset) + generate_slice_harnesses!( + i8, + check_const_add_slice_i8, + check_const_sub_slice_i8, + check_const_offset_slice_i8 + ); + generate_slice_harnesses!( + i16, + check_const_add_slice_i16, + check_const_sub_slice_i16, + check_const_offset_slice_i16 + ); + generate_slice_harnesses!( + i32, + check_const_add_slice_i32, + check_const_sub_slice_i32, + check_const_offset_slice_i32 + ); + generate_slice_harnesses!( + i64, + check_const_add_slice_i64, + check_const_sub_slice_i64, + check_const_offset_slice_i64 + ); + generate_slice_harnesses!( + i128, + check_const_add_slice_i128, + check_const_sub_slice_i128, + check_const_offset_slice_i128 + ); + generate_slice_harnesses!( + isize, + check_const_add_slice_isize, + check_const_sub_slice_isize, + check_const_offset_slice_isize + ); + generate_slice_harnesses!( + u8, + check_const_add_slice_u8, + check_const_sub_slice_u8, + check_const_offset_slice_u8 + ); + generate_slice_harnesses!( + u16, + check_const_add_slice_u16, + check_const_sub_slice_u16, + check_const_offset_slice_u16 + ); + generate_slice_harnesses!( + u32, + check_const_add_slice_u32, + check_const_sub_slice_u32, + check_const_offset_slice_u32 + ); + generate_slice_harnesses!( + u64, + check_const_add_slice_u64, + check_const_sub_slice_u64, + check_const_offset_slice_u64 + ); + generate_slice_harnesses!( + u128, + check_const_add_slice_u128, + check_const_sub_slice_u128, + check_const_offset_slice_u128 + ); + generate_slice_harnesses!( + usize, + check_const_add_slice_usize, + check_const_sub_slice_usize, + check_const_offset_slice_usize + ); + + // Generate slice harnesses for tuples (add, sub, offset) + generate_slice_harnesses!( + (i8, i8), + check_const_add_slice_tuple_1, + check_const_sub_slice_tuple_1, + check_const_offset_slice_tuple_1 + ); + generate_slice_harnesses!( + (f64, bool), + check_const_add_slice_tuple_2, + check_const_sub_slice_tuple_2, + check_const_offset_slice_tuple_2 + ); + generate_slice_harnesses!( + (i32, f64, bool), + check_const_add_slice_tuple_3, + check_const_sub_slice_tuple_3, + check_const_offset_slice_tuple_3 + ); + generate_slice_harnesses!( + (i8, u16, i32, u64, isize), + check_const_add_slice_tuple_4, + check_const_sub_slice_tuple_4, + check_const_offset_slice_tuple_4 + ); + // Array size bound for kani::any_array for `offset_from` verification const ARRAY_LEN: usize = 40; From 36ef49498aab329d74a16cd469b1fb373ea4c2ce Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Mon, 2 Dec 2024 21:42:06 -0800 Subject: [PATCH 45/45] Refactored function contracts for better readability. --- library/core/src/ptr/const_ptr.rs | 36 ++++++++++++++----------------- 1 file changed, 16 insertions(+), 20 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 18124b75856cf..dc6cee50b86c0 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -411,12 +411,10 @@ impl *const T { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires( // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize`. - if let Some(computed_offset) = count.checked_mul(core::mem::size_of::() as isize) { - // Precondition 2: adding the computed offset to `self` does not cause overflow. - (self as isize).checked_add(computed_offset).is_some() - } else { - false - } && + // Precondition 2: adding the computed offset to `self` does not cause overflow. + // These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani. + count.checked_mul(core::mem::size_of::() as isize) + .map_or(false, |computed_offset| (self as isize).checked_add(computed_offset).is_some()) && // 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. @@ -951,13 +949,12 @@ impl *const T { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires( // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize`. - if let Some(computed_offset) = count.checked_mul(core::mem::size_of::()) { - computed_offset <= isize::MAX as usize && - // Precondition 2: adding the computed offset to `self` does not cause overflow. - (self as isize).checked_add(computed_offset as isize).is_some() - } else { - false - } && + // Precondition 2: adding the computed offset to `self` does not cause overflow. + // These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani. + count.checked_mul(core::mem::size_of::()) + .map_or(false, |computed_offset| { + computed_offset <= isize::MAX as usize && (self as isize).checked_add(computed_offset as isize).is_some() + }) && // 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. @@ -1078,13 +1075,12 @@ impl *const T { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires( // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize`. - if let Some(computed_offset) = count.checked_mul(core::mem::size_of::()) { - computed_offset <= isize::MAX as usize && - // Precondition 2: substracting the computed offset from `self` does not cause overflow. - (self as isize).checked_sub(computed_offset as isize).is_some() - } else { - false - } && + // Precondition 2: substracting the computed offset from `self` does not cause overflow. + // These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani. + count.checked_mul(core::mem::size_of::()) + .map_or(false, |computed_offset| { + computed_offset <= isize::MAX as usize && (self as isize).checked_sub(computed_offset as isize).is_some() + }) && // 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.