From 500f249c90b48f307afe23fb3ed82be8a35f045a Mon Sep 17 00:00:00 2001 From: szlee118 Date: Thu, 12 Sep 2024 18:34:15 -0700 Subject: [PATCH 01/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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