From 9a8993d24bd5a5f7f757afa14a47e84886a94b9c Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Mon, 7 Oct 2024 12:44:18 -0700 Subject: [PATCH 01/22] added common codes for all proof of contracts --- library/core/src/ptr/mut_ptr.rs | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 42975cc927b8e..2a5d44a5eae1c 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. @@ -403,6 +407,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 offset(self, count: isize) -> *mut T where T: Sized, @@ -947,6 +955,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, @@ -1022,6 +1034,10 @@ impl *mut 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, @@ -2197,3 +2213,10 @@ impl PartialOrd for *mut T { *self >= *other } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use crate::kani; + +} \ No newline at end of file From 55950bbfb9e8ad39bb2fd1d59dc9ac135e0bac5f Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Mon, 7 Oct 2024 12:57:46 -0700 Subject: [PATCH 02/22] implemented integer type proof for contract for fn add, sub and offset --- library/core/src/ptr/mut_ptr.rs | 92 ++++++++++++++++++++++++++++++++- 1 file changed, 91 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 2a5d44a5eae1c..4c5a98f8ffea0 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2218,5 +2218,95 @@ impl PartialOrd for *mut T { #[unstable(feature = "kani", issue = "none")] mod verify { use crate::kani; - + + // fn <*mut T>::add verification begin + macro_rules! generate_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_add_harness!(i8, check_mut_add_i8); + generate_add_harness!(i16, check_mut_add_i16); + generate_add_harness!(i32, check_mut_add_i32); + generate_add_harness!(i64, check_mut_add_i64); + generate_add_harness!(i128, check_mut_add_i128); + generate_add_harness!(isize, check_mut_add_isize); + generate_add_harness!(u8, check_mut_add_u8); + generate_add_harness!(u16, check_mut_add_u16); + generate_add_harness!(u32, check_mut_add_u32); + generate_add_harness!(u64, check_mut_add_u64); + generate_add_harness!(u128, check_mut_add_u128); + generate_add_harness!(usize, check_mut_add_usize); + // fn <*mut T>::add verification end + + // fn <*mut T>::sub verification begin + macro_rules! generate_sub_harness { + ($type:ty, $proof_name:ident) => { + #[allow(unused)] + #[kani::proof_for_contract(<*mut $type>::sub)] + 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.sub(count); + } + } + }; + } + + generate_sub_harness!(i8, check_mut_sub_i8); + generate_sub_harness!(i16, check_mut_sub_i16); + generate_sub_harness!(i32, check_mut_sub_i32); + generate_sub_harness!(i64, check_mut_sub_i64); + generate_sub_harness!(i128, check_mut_sub_i128); + generate_sub_harness!(isize, check_mut_sub_isize); + generate_sub_harness!(u8, check_mut_sub_u8); + generate_sub_harness!(u16, check_mut_sub_u16); + generate_sub_harness!(u32, check_mut_sub_u32); + generate_sub_harness!(u64, check_mut_sub_u64); + generate_sub_harness!(u128, check_mut_sub_u128); + generate_sub_harness!(usize, check_mut_sub_usize); + // fn <*mut T>::sub verification end + + // fn <*mut T>::offset verification begin + macro_rules! generate_offset_harness { + ($type:ty, $proof_name:ident) => { + #[allow(unused)] + #[kani::proof_for_contract(<*mut $type>::offset)] + pub fn $proof_name() { + let mut test_val: $type = kani::any::<$type>(); + let test_ptr: *mut $type = &mut test_val; + let count: isize = kani::any(); + unsafe { + test_ptr.offset(count); + } + } + }; + } + + generate_offset_harness!(i8, check_mut_offset_i8); + generate_offset_harness!(i16, check_mut_offset_i16); + generate_offset_harness!(i32, check_mut_offset_i32); + generate_offset_harness!(i64, check_mut_offset_i64); + generate_offset_harness!(i128, check_mut_offset_i128); + generate_offset_harness!(isize, check_mut_offset_isize); + generate_offset_harness!(u8, check_mut_offset_u8); + generate_offset_harness!(u16, check_mut_offset_u16); + generate_offset_harness!(u32, check_mut_offset_u32); + generate_offset_harness!(u64, check_mut_offset_u64); + generate_offset_harness!(u128, check_mut_offset_u128); + generate_offset_harness!(usize, check_mut_offset_usize); + // fn <*mut T>::offset verification end + } \ No newline at end of file From 36828583f364bb822af61749594785d7b9b472a9 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Wed, 9 Oct 2024 00:50:07 +0000 Subject: [PATCH 03/22] Adds proofs for tuple types --- library/core/src/ptr/mut_ptr.rs | 46 ++++++++++++++++++++++++++++++++- 1 file changed, 45 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 2a5d44a5eae1c..4a74ef5738aec 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2218,5 +2218,49 @@ impl PartialOrd for *mut T { #[unstable(feature = "kani", issue = "none")] mod verify { use crate::kani; - + + macro_rules! generate_mut_add_and_sub_harness { + ($type:ty, $proof_name:ident, $func_name:ident) => { + #[allow(unused)] + #[kani::proof_for_contract(<*mut $type>::$func_name)] + 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.$func_name(count); + } + } + }; + } + + generate_mut_add_and_sub_harness!((i8, i8), check_add_tuple_1, add); + generate_mut_add_and_sub_harness!((f64, bool), check_add_tuple_2, add); + generate_mut_add_and_sub_harness!((i32, f64, bool), check_add_tuple_3, add); + generate_mut_add_and_sub_harness!((i8, u16, i32, u64, isize), check_add_tuple_4, add); + generate_mut_add_and_sub_harness!((i8, i8), check_add_tuple_1, sub); + generate_mut_add_and_sub_harness!((f64, bool), check_add_tuple_2, sub); + generate_mut_add_and_sub_harness!((i32, f64, bool), check_add_tuple_3, sub); + generate_mut_add_and_sub_harness!((i8, u16, i32, u64, isize), check_add_tuple_4, sub); + + // fn <*mut T>::offset verification begin + macro_rules! generate_mut_offset_harness { + ($type:ty, $proof_name:ident) => { + #[allow(unused)] + #[kani::proof_for_contract(<*mut $type>::offset)] + pub fn $proof_name() { + let mut test_val: $type = kani::any::<$type>(); + let test_ptr: *mut $type = &test_val; + let count: isize = kani::any(); + unsafe { + test_ptr.offset(count); + } + } + }; + } + + generate_mut_offset_harness!((i8, i8), check_offset_tuple_1); + generate_mut_offset_harness!((f64, bool), check_offset_tuple_2); + generate_mut_offset_harness!((i32, f64, bool), check_offset_tuple_3); + generate_mut_offset_harness!((i8, u16, i32, u64, isize), check_offset_tuple_4); } \ No newline at end of file From a6d4d62dc9ba46f9a59d864c354e00966bcfd0ea Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Wed, 9 Oct 2024 01:04:40 +0000 Subject: [PATCH 04/22] Renames harnesses --- library/core/src/ptr/mut_ptr.rs | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 4a74ef5738aec..c211039ae7527 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2234,14 +2234,14 @@ mod verify { }; } - generate_mut_add_and_sub_harness!((i8, i8), check_add_tuple_1, add); - generate_mut_add_and_sub_harness!((f64, bool), check_add_tuple_2, add); - generate_mut_add_and_sub_harness!((i32, f64, bool), check_add_tuple_3, add); - generate_mut_add_and_sub_harness!((i8, u16, i32, u64, isize), check_add_tuple_4, add); - generate_mut_add_and_sub_harness!((i8, i8), check_add_tuple_1, sub); - generate_mut_add_and_sub_harness!((f64, bool), check_add_tuple_2, sub); - generate_mut_add_and_sub_harness!((i32, f64, bool), check_add_tuple_3, sub); - generate_mut_add_and_sub_harness!((i8, u16, i32, u64, isize), check_add_tuple_4, sub); + generate_mut_add_and_sub_harness!((i8, i8), check_mut_add_tuple_1, add); + generate_mut_add_and_sub_harness!((f64, bool), check_mut_add_tuple_2, add); + generate_mut_add_and_sub_harness!((i32, f64, bool), check_mut_add_tuple_3, add); + generate_mut_add_and_sub_harness!((i8, u16, i32, u64, isize), check_mut_add_tuple_4, add); + generate_mut_add_and_sub_harness!((i8, i8), check_mut_sub_tuple_1, sub); + generate_mut_add_and_sub_harness!((f64, bool), check_mut_sub_tuple_2, sub); + generate_mut_add_and_sub_harness!((i32, f64, bool), check_mut_sub_tuple_3, sub); + generate_mut_add_and_sub_harness!((i8, u16, i32, u64, isize), check_mut_sub_tuple_4, sub); // fn <*mut T>::offset verification begin macro_rules! generate_mut_offset_harness { @@ -2259,8 +2259,8 @@ mod verify { }; } - generate_mut_offset_harness!((i8, i8), check_offset_tuple_1); - generate_mut_offset_harness!((f64, bool), check_offset_tuple_2); - generate_mut_offset_harness!((i32, f64, bool), check_offset_tuple_3); - generate_mut_offset_harness!((i8, u16, i32, u64, isize), check_offset_tuple_4); + generate_mut_offset_harness!((i8, i8), check_mut_offset_tuple_1); + generate_mut_offset_harness!((f64, bool), check_mut_offset_tuple_2); + generate_mut_offset_harness!((i32, f64, bool), check_mut_offset_tuple_3); + generate_mut_offset_harness!((i8, u16, i32, u64, isize), check_omut_ffset_tuple_4); } \ No newline at end of file From dec8c30d0c901d75ab803529b2bda631950b8936 Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 Date: Wed, 9 Oct 2024 11:45:09 -0700 Subject: [PATCH 05/22] Added unit type proofs for mut ptr --- library/core/src/ptr/mut_ptr.rs | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 2a5d44a5eae1c..a4ec2bacda680 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2218,5 +2218,31 @@ impl PartialOrd for *mut T { #[unstable(feature = "kani", issue = "none")] mod verify { use crate::kani; - + macro_rules! generate_unit_harness { + ($fn_name:ident, $proof_name:ident) => { + #[allow(unused)] + #[kani::proof_for_contract(<*mut ()>::$fn_name)] + pub fn $proof_name() { + let mut test_val: () = (); + let test_ptr: *mut () = &mut test_val; + let count: usize = kani::any(); + unsafe { + test_ptr.$fn_name(count); + } + } + }; + } + generate_unit_harness!(add, check_mut_add_unit); + generate_unit_harness!(sub, check_mut_sub_unit); + + #[allow(unused)] + #[kani::proof_for_contract(<*mut ()>::offset)] + pub fn check_mut_offset_unit() { + let mut test_val: () = (); + let test_ptr: *mut () = &mut test_val; + let count: isize = kani::any(); + unsafe { + test_ptr.offset(count); + } + } } \ No newline at end of file From 0faac468d2fff9656ab9d84c3f3cefc57e7ecea8 Mon Sep 17 00:00:00 2001 From: stogaru <143449212+stogaru@users.noreply.github.com> Date: Fri, 11 Oct 2024 19:47:11 -0400 Subject: [PATCH 06/22] Combined macros --- library/core/src/ptr/mut_ptr.rs | 177 +++++++++++--------------------- 1 file changed, 59 insertions(+), 118 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 1dbd6dabfe22f..6843b1769e193 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2234,43 +2234,51 @@ mod verify { }; } + // <*mut T>:: add() integer types verification + generate_mut_add_and_sub_harness!(i8, check_mut_add_i8, add); + generate_mut_add_and_sub_harness!(i16, check_mut_add_i16, add); + generate_mut_add_and_sub_harness!(i32, check_mut_add_i32, add); + generate_mut_add_and_sub_harness!(i64, check_mut_add_i64, add); + generate_mut_add_and_sub_harness!(i128, check_mut_add_i128, add); + generate_mut_add_and_sub_harness!(isize, check_mut_add_isize, add); + generate_mut_add_and_sub_harness!(u8, check_mut_add_u8, add); + generate_mut_add_and_sub_harness!(u16, check_mut_add_u16, add); + generate_mut_add_and_sub_harness!(u32, check_mut_add_u32, add); + generate_mut_add_and_sub_harness!(u64, check_mut_add_u64, add); + generate_mut_add_and_sub_harness!(u128, check_mut_add_u128, add); + generate_mut_add_and_sub_harness!(usize, check_mut_add_usize, add); + + // <*mut T>:: add() unit type verification + generate_mut_add_and_sub_harness!((), check_mut_add_unit, add); + + // <*mut T>:: add() composite types verification generate_mut_add_and_sub_harness!((i8, i8), check_mut_add_tuple_1, add); generate_mut_add_and_sub_harness!((f64, bool), check_mut_add_tuple_2, add); generate_mut_add_and_sub_harness!((i32, f64, bool), check_mut_add_tuple_3, add); generate_mut_add_and_sub_harness!((i8, u16, i32, u64, isize), check_mut_add_tuple_4, add); + + // <*mut T>:: sub() integer types verification + generate_mut_add_and_sub_harness!(i8, check_mut_sub_i8, sub); + generate_mut_add_and_sub_harness!(i16, check_mut_sub_i16, sub); + generate_mut_add_and_sub_harness!(i32, check_mut_sub_i32, sub); + generate_mut_add_and_sub_harness!(i64, check_mut_sub_i64, sub); + generate_mut_add_and_sub_harness!(i128, check_mut_sub_i128, sub); + generate_mut_add_and_sub_harness!(isize, check_mut_sub_isize, sub); + generate_mut_add_and_sub_harness!(u8, check_mut_sub_u8, sub); + generate_mut_add_and_sub_harness!(u16, check_mut_sub_u16, sub); + generate_mut_add_and_sub_harness!(u32, check_mut_sub_u32, sub); + generate_mut_add_and_sub_harness!(u64, check_mut_sub_u64, sub); + generate_mut_add_and_sub_harness!(u128, check_mut_sub_u128, sub); + generate_mut_add_and_sub_harness!(usize, check_mut_sub_usize, sub); + + // <*mut T>:: sub() unit type verification + generate_mut_add_and_sub_harness!((), check_mut_sub_unit, sub); + + // <*mut T>:: sub() composite types verification generate_mut_add_and_sub_harness!((i8, i8), check_mut_sub_tuple_1, sub); generate_mut_add_and_sub_harness!((f64, bool), check_mut_sub_tuple_2, sub); generate_mut_add_and_sub_harness!((i32, f64, bool), check_mut_sub_tuple_3, sub); generate_mut_add_and_sub_harness!((i8, u16, i32, u64, isize), check_mut_sub_tuple_4, sub); - - // fn <*mut T>::add verification begin - macro_rules! generate_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_add_harness!(i8, check_mut_add_i8); - generate_add_harness!(i16, check_mut_add_i16); - generate_add_harness!(i32, check_mut_add_i32); - generate_add_harness!(i64, check_mut_add_i64); - generate_add_harness!(i128, check_mut_add_i128); - generate_add_harness!(isize, check_mut_add_isize); - generate_add_harness!(u8, check_mut_add_u8); - generate_add_harness!(u16, check_mut_add_u16); - generate_add_harness!(u32, check_mut_add_u32); - generate_add_harness!(u64, check_mut_add_u64); - generate_add_harness!(u128, check_mut_add_u128); - generate_add_harness!(usize, check_mut_add_usize); // fn <*mut T>::offset verification begin @@ -2280,7 +2288,7 @@ mod verify { #[kani::proof_for_contract(<*mut $type>::offset)] pub fn $proof_name() { let mut test_val: $type = kani::any::<$type>(); - let test_ptr: *mut $type = &test_val; + let test_ptr: *mut $type = &mut test_val; let count: isize = kani::any(); unsafe { test_ptr.offset(count); @@ -2288,94 +2296,27 @@ mod verify { } }; } - + + // fn <*mut T>::offset integer types verification + generate_mut_offset_harness!(i8, check_mut_offset_i8); + generate_mut_offset_harness!(i16, check_mut_offset_i16); + generate_mut_offset_harness!(i32, check_mut_offset_i32); + generate_mut_offset_harness!(i64, check_mut_offset_i64); + generate_mut_offset_harness!(i128, check_mut_offset_i128); + generate_mut_offset_harness!(isize, check_mut_offset_isize); + generate_mut_offset_harness!(u8, check_mut_offset_u8); + generate_mut_offset_harness!(u16, check_mut_offset_u16); + generate_mut_offset_harness!(u32, check_mut_offset_u32); + generate_mut_offset_harness!(u64, check_mut_offset_u64); + generate_mut_offset_harness!(u128, check_mut_offset_u128); + generate_mut_offset_harness!(usize, check_mut_offset_usize); + + // fn <*mut T>::offset unit type verification + generate_mut_offset_harness!((), check_mut_offset_unit); + + // fn <*mut T>::offset composite type verification generate_mut_offset_harness!((i8, i8), check_mut_offset_tuple_1); generate_mut_offset_harness!((f64, bool), check_mut_offset_tuple_2); generate_mut_offset_harness!((i32, f64, bool), check_mut_offset_tuple_3); - generate_mut_offset_harness!((i8, u16, i32, u64, isize), check_omut_ffset_tuple_4); - - // fn <*mut T>::sub verification begin - macro_rules! generate_sub_harness { - ($type:ty, $proof_name:ident) => { - #[allow(unused)] - #[kani::proof_for_contract(<*mut $type>::sub)] - 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.sub(count); - } - } - }; - } - - generate_sub_harness!(i8, check_mut_sub_i8); - generate_sub_harness!(i16, check_mut_sub_i16); - generate_sub_harness!(i32, check_mut_sub_i32); - generate_sub_harness!(i64, check_mut_sub_i64); - generate_sub_harness!(i128, check_mut_sub_i128); - generate_sub_harness!(isize, check_mut_sub_isize); - generate_sub_harness!(u8, check_mut_sub_u8); - generate_sub_harness!(u16, check_mut_sub_u16); - generate_sub_harness!(u32, check_mut_sub_u32); - generate_sub_harness!(u64, check_mut_sub_u64); - generate_sub_harness!(u128, check_mut_sub_u128); - generate_sub_harness!(usize, check_mut_sub_usize); - - // fn <*mut T>::offset verification begin - macro_rules! generate_offset_harness { - ($type:ty, $proof_name:ident) => { - #[allow(unused)] - #[kani::proof_for_contract(<*mut $type>::offset)] - pub fn $proof_name() { - let mut test_val: $type = kani::any::<$type>(); - let test_ptr: *mut $type = &mut test_val; - let count: isize = kani::any(); - unsafe { - test_ptr.offset(count); - } - } - }; - } - generate_offset_harness!(i8, check_mut_offset_i8); - generate_offset_harness!(i16, check_mut_offset_i16); - generate_offset_harness!(i32, check_mut_offset_i32); - generate_offset_harness!(i64, check_mut_offset_i64); - generate_offset_harness!(i128, check_mut_offset_i128); - generate_offset_harness!(isize, check_mut_offset_isize); - generate_offset_harness!(u8, check_mut_offset_u8); - generate_offset_harness!(u16, check_mut_offset_u16); - generate_offset_harness!(u32, check_mut_offset_u32); - generate_offset_harness!(u64, check_mut_offset_u64); - generate_offset_harness!(u128, check_mut_offset_u128); - generate_offset_harness!(usize, check_mut_offset_usize); - - macro_rules! generate_unit_harness { - ($fn_name:ident, $proof_name:ident) => { - #[allow(unused)] - #[kani::proof_for_contract(<*mut ()>::$fn_name)] - pub fn $proof_name() { - let mut test_val: () = (); - let test_ptr: *mut () = &mut test_val; - let count: usize = kani::any(); - unsafe { - test_ptr.$fn_name(count); - } - } - }; - } - generate_unit_harness!(add, check_mut_add_unit); - generate_unit_harness!(sub, check_mut_sub_unit); - - #[allow(unused)] - #[kani::proof_for_contract(<*mut ()>::offset)] - pub fn check_mut_offset_unit() { - let mut test_val: () = (); - let test_ptr: *mut () = &mut test_val; - let count: isize = kani::any(); - unsafe { - test_ptr.offset(count); - } - } -} \ No newline at end of file + generate_mut_offset_harness!((i8, u16, i32, u64, isize), check_mut_offset_tuple_4); +} From 82345de2d57a732fd8c410347ce67188def42322 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Sat, 12 Oct 2024 00:01:13 +0000 Subject: [PATCH 07/22] Fixes a typo --- 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 6843b1769e193..b2d9a5fb67c6c 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2218,10 +2218,10 @@ impl PartialOrd for *mut T { #[unstable(feature = "kani", issue = "none")] mod verify { use crate::kani; + #[allow(unused)] macro_rules! generate_mut_add_and_sub_harness { ($type:ty, $proof_name:ident, $func_name:ident) => { - #[allow(unused)] #[kani::proof_for_contract(<*mut $type>::$func_name)] pub fn $proof_name() { let mut test_val: $type = kani::any::<$type>(); @@ -2284,7 +2284,6 @@ mod verify { // fn <*mut T>::offset verification begin macro_rules! generate_mut_offset_harness { ($type:ty, $proof_name:ident) => { - #[allow(unused)] #[kani::proof_for_contract(<*mut $type>::offset)] pub fn $proof_name() { let mut test_val: $type = kani::any::<$type>(); From 656209b56da81d4f2afbf302edd315fd8644e346 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Sat, 12 Oct 2024 00:06:20 +0000 Subject: [PATCH 08/22] Removes an unnecessary attribute --- library/core/src/ptr/mut_ptr.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index b2d9a5fb67c6c..83d30e0c01375 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2218,7 +2218,6 @@ impl PartialOrd for *mut T { #[unstable(feature = "kani", issue = "none")] mod verify { use crate::kani; - #[allow(unused)] macro_rules! generate_mut_add_and_sub_harness { ($type:ty, $proof_name:ident, $func_name:ident) => { From 96a8a2e79428ab08ccb06315fceae00ffaa04234 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Wed, 23 Oct 2024 12:58:18 -0700 Subject: [PATCH 09/22] refactored function contracts for add, sub and offset using the same_allocation api, modified their proof for harness accordingly --- library/core/src/ptr/mut_ptr.rs | 73 ++++++++++++++++++++++++++------- 1 file changed, 59 insertions(+), 14 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 83d30e0c01375..0252c9656a255 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -408,9 +408,8 @@ impl *mut T { #[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(count.checked_mul(core::mem::size_of::() as isize).is_some())] + #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T) && kani::mem::can_dereference(result))] pub const unsafe fn offset(self, count: isize) -> *mut T where T: Sized, @@ -956,9 +955,9 @@ impl *mut T { #[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(count.checked_mul(core::mem::size_of::()).is_some() + && count * core::mem::size_of::() <= isize::MAX as usize)] + #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T) && kani::mem::can_dereference(result))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -1035,9 +1034,9 @@ impl *mut T { #[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(count.checked_mul(core::mem::size_of::()).is_some() + && count * core::mem::size_of::() <= isize::MAX as usize)] + #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T) && kani::mem::can_dereference(result))] pub const unsafe fn sub(self, count: usize) -> Self where T: Sized, @@ -2220,17 +2219,52 @@ mod verify { use crate::kani; macro_rules! generate_mut_add_and_sub_harness { - ($type:ty, $proof_name:ident, $func_name:ident) => { - #[kani::proof_for_contract(<*mut $type>::$func_name)] + ($type:ty, $proof_name:ident, add) => { + #[kani::proof_for_contract(<*mut $type>::add)] pub fn $proof_name() { let mut test_val: $type = kani::any::<$type>(); + let offset: usize = kani::any(); + let count: usize = kani::any(); + if(core::mem::size_of::<$type>() == 0) { // unit type + kani::assume(offset == 0); + kani::assume(count == 0); + } else { + kani::assume(offset == 0 || offset == 1); + kani::assume(count == 0 || count == 1); + kani::assume(offset + count <= 1); + } + let test_ptr: *mut $type = &mut test_val; - let count: usize = kani::any(); + let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset); + unsafe { - test_ptr.$func_name(count); + ptr_with_offset.add(count); } } }; + ($type:ty, $proof_name:ident, sub) => { + #[kani::proof_for_contract(<*mut $type>::sub)] + pub fn $proof_name() { + let mut test_val: $type = kani::any::<$type>(); + let offset: usize = kani::any(); + let count: usize = kani::any(); + if(core::mem::size_of::<$type>() == 0) { // unit type + kani::assume(offset == 0); + kani::assume(count == 0); + } else { + kani::assume(offset == 0 || offset == 1); + kani::assume(count == 0 || count == 1); + kani::assume(count <= offset); + } + + let test_ptr: *mut $type = &mut test_val; + let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset); + + unsafe { + ptr_with_offset.sub(count); + } + } + } } // <*mut T>:: add() integer types verification @@ -2287,9 +2321,20 @@ mod verify { pub fn $proof_name() { let mut test_val: $type = kani::any::<$type>(); let test_ptr: *mut $type = &mut test_val; + let offset: usize = kani::any(); let count: isize = kani::any(); + if(core::mem::size_of::<$type>() == 0) { // unit type + kani::assume(offset == 0); + kani::assume(count == 0); + } else { + kani::assume(offset == 0 || offset == 1); + kani::assume(count == 0 || count == 1); + kani::assume(offset as isize + count == 0 || offset as isize + count == 1); + } + let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset); + unsafe { - test_ptr.offset(count); + ptr_with_offset.offset(count); } } }; From 852e96f4c20540bbfb9b1807f3eec8da8825594a Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Wed, 23 Oct 2024 13:11:23 -0700 Subject: [PATCH 10/22] merged macros for add, sub and offset --- library/core/src/ptr/mut_ptr.rs | 147 +++++++++++++++----------------- 1 file changed, 71 insertions(+), 76 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 0252c9656a255..df97e30bcbe3e 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2218,7 +2218,7 @@ impl PartialOrd for *mut T { mod verify { use crate::kani; - macro_rules! generate_mut_add_and_sub_harness { + macro_rules! generate_mut_arithmetic_harness { ($type:ty, $proof_name:ident, add) => { #[kani::proof_for_contract(<*mut $type>::add)] pub fn $proof_name() { @@ -2264,59 +2264,8 @@ mod verify { ptr_with_offset.sub(count); } } - } - } - - // <*mut T>:: add() integer types verification - generate_mut_add_and_sub_harness!(i8, check_mut_add_i8, add); - generate_mut_add_and_sub_harness!(i16, check_mut_add_i16, add); - generate_mut_add_and_sub_harness!(i32, check_mut_add_i32, add); - generate_mut_add_and_sub_harness!(i64, check_mut_add_i64, add); - generate_mut_add_and_sub_harness!(i128, check_mut_add_i128, add); - generate_mut_add_and_sub_harness!(isize, check_mut_add_isize, add); - generate_mut_add_and_sub_harness!(u8, check_mut_add_u8, add); - generate_mut_add_and_sub_harness!(u16, check_mut_add_u16, add); - generate_mut_add_and_sub_harness!(u32, check_mut_add_u32, add); - generate_mut_add_and_sub_harness!(u64, check_mut_add_u64, add); - generate_mut_add_and_sub_harness!(u128, check_mut_add_u128, add); - generate_mut_add_and_sub_harness!(usize, check_mut_add_usize, add); - - // <*mut T>:: add() unit type verification - generate_mut_add_and_sub_harness!((), check_mut_add_unit, add); - - // <*mut T>:: add() composite types verification - generate_mut_add_and_sub_harness!((i8, i8), check_mut_add_tuple_1, add); - generate_mut_add_and_sub_harness!((f64, bool), check_mut_add_tuple_2, add); - generate_mut_add_and_sub_harness!((i32, f64, bool), check_mut_add_tuple_3, add); - generate_mut_add_and_sub_harness!((i8, u16, i32, u64, isize), check_mut_add_tuple_4, add); - - // <*mut T>:: sub() integer types verification - generate_mut_add_and_sub_harness!(i8, check_mut_sub_i8, sub); - generate_mut_add_and_sub_harness!(i16, check_mut_sub_i16, sub); - generate_mut_add_and_sub_harness!(i32, check_mut_sub_i32, sub); - generate_mut_add_and_sub_harness!(i64, check_mut_sub_i64, sub); - generate_mut_add_and_sub_harness!(i128, check_mut_sub_i128, sub); - generate_mut_add_and_sub_harness!(isize, check_mut_sub_isize, sub); - generate_mut_add_and_sub_harness!(u8, check_mut_sub_u8, sub); - generate_mut_add_and_sub_harness!(u16, check_mut_sub_u16, sub); - generate_mut_add_and_sub_harness!(u32, check_mut_sub_u32, sub); - generate_mut_add_and_sub_harness!(u64, check_mut_sub_u64, sub); - generate_mut_add_and_sub_harness!(u128, check_mut_sub_u128, sub); - generate_mut_add_and_sub_harness!(usize, check_mut_sub_usize, sub); - - // <*mut T>:: sub() unit type verification - generate_mut_add_and_sub_harness!((), check_mut_sub_unit, sub); - - // <*mut T>:: sub() composite types verification - generate_mut_add_and_sub_harness!((i8, i8), check_mut_sub_tuple_1, sub); - generate_mut_add_and_sub_harness!((f64, bool), check_mut_sub_tuple_2, sub); - generate_mut_add_and_sub_harness!((i32, f64, bool), check_mut_sub_tuple_3, sub); - generate_mut_add_and_sub_harness!((i8, u16, i32, u64, isize), check_mut_sub_tuple_4, sub); - - - // fn <*mut T>::offset verification begin - macro_rules! generate_mut_offset_harness { - ($type:ty, $proof_name:ident) => { + }; + ($type:ty, $proof_name:ident, offset) => { #[kani::proof_for_contract(<*mut $type>::offset)] pub fn $proof_name() { let mut test_val: $type = kani::any::<$type>(); @@ -2340,26 +2289,72 @@ mod verify { }; } - // fn <*mut T>::offset integer types verification - generate_mut_offset_harness!(i8, check_mut_offset_i8); - generate_mut_offset_harness!(i16, check_mut_offset_i16); - generate_mut_offset_harness!(i32, check_mut_offset_i32); - generate_mut_offset_harness!(i64, check_mut_offset_i64); - generate_mut_offset_harness!(i128, check_mut_offset_i128); - generate_mut_offset_harness!(isize, check_mut_offset_isize); - generate_mut_offset_harness!(u8, check_mut_offset_u8); - generate_mut_offset_harness!(u16, check_mut_offset_u16); - generate_mut_offset_harness!(u32, check_mut_offset_u32); - generate_mut_offset_harness!(u64, check_mut_offset_u64); - generate_mut_offset_harness!(u128, check_mut_offset_u128); - generate_mut_offset_harness!(usize, check_mut_offset_usize); - - // fn <*mut T>::offset unit type verification - generate_mut_offset_harness!((), check_mut_offset_unit); - - // fn <*mut T>::offset composite type verification - generate_mut_offset_harness!((i8, i8), check_mut_offset_tuple_1); - generate_mut_offset_harness!((f64, bool), check_mut_offset_tuple_2); - generate_mut_offset_harness!((i32, f64, bool), check_mut_offset_tuple_3); - generate_mut_offset_harness!((i8, u16, i32, u64, isize), check_mut_offset_tuple_4); + // <*mut T>:: add() integer types verification + generate_mut_arithmetic_harness!(i8, check_mut_add_i8, add); + generate_mut_arithmetic_harness!(i16, check_mut_add_i16, add); + generate_mut_arithmetic_harness!(i32, check_mut_add_i32, add); + generate_mut_arithmetic_harness!(i64, check_mut_add_i64, add); + generate_mut_arithmetic_harness!(i128, check_mut_add_i128, add); + generate_mut_arithmetic_harness!(isize, check_mut_add_isize, add); + generate_mut_arithmetic_harness!(u8, check_mut_add_u8, add); + generate_mut_arithmetic_harness!(u16, check_mut_add_u16, add); + generate_mut_arithmetic_harness!(u32, check_mut_add_u32, add); + generate_mut_arithmetic_harness!(u64, check_mut_add_u64, add); + generate_mut_arithmetic_harness!(u128, check_mut_add_u128, add); + generate_mut_arithmetic_harness!(usize, check_mut_add_usize, add); + + // <*mut T>:: add() unit type verification + generate_mut_arithmetic_harness!((), check_mut_add_unit, add); + + // <*mut T>:: add() composite types verification + generate_mut_arithmetic_harness!((i8, i8), check_mut_add_tuple_1, add); + generate_mut_arithmetic_harness!((f64, bool), check_mut_add_tuple_2, add); + generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_add_tuple_3, add); + generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_add_tuple_4, add); + + // <*mut T>:: sub() integer types verification + generate_mut_arithmetic_harness!(i8, check_mut_sub_i8, sub); + generate_mut_arithmetic_harness!(i16, check_mut_sub_i16, sub); + generate_mut_arithmetic_harness!(i32, check_mut_sub_i32, sub); + generate_mut_arithmetic_harness!(i64, check_mut_sub_i64, sub); + generate_mut_arithmetic_harness!(i128, check_mut_sub_i128, sub); + generate_mut_arithmetic_harness!(isize, check_mut_sub_isize, sub); + generate_mut_arithmetic_harness!(u8, check_mut_sub_u8, sub); + generate_mut_arithmetic_harness!(u16, check_mut_sub_u16, sub); + generate_mut_arithmetic_harness!(u32, check_mut_sub_u32, sub); + generate_mut_arithmetic_harness!(u64, check_mut_sub_u64, sub); + generate_mut_arithmetic_harness!(u128, check_mut_sub_u128, sub); + generate_mut_arithmetic_harness!(usize, check_mut_sub_usize, sub); + + // <*mut T>:: sub() unit type verification + generate_mut_arithmetic_harness!((), check_mut_sub_unit, sub); + + // <*mut T>:: sub() composite types verification + generate_mut_arithmetic_harness!((i8, i8), check_mut_sub_tuple_1, sub); + generate_mut_arithmetic_harness!((f64, bool), check_mut_sub_tuple_2, sub); + generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_sub_tuple_3, sub); + generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_sub_tuple_4, sub); + + // fn <*mut T>::offset() integer types verification + generate_mut_arithmetic_harness!(i8, check_mut_offset_i8, offset); + generate_mut_arithmetic_harness!(i16, check_mut_offset_i16, offset); + generate_mut_arithmetic_harness!(i32, check_mut_offset_i32, offset); + generate_mut_arithmetic_harness!(i64, check_mut_offset_i64, offset); + generate_mut_arithmetic_harness!(i128, check_mut_offset_i128, offset); + generate_mut_arithmetic_harness!(isize, check_mut_offset_isize, offset); + generate_mut_arithmetic_harness!(u8, check_mut_offset_u8, offset); + generate_mut_arithmetic_harness!(u16, check_mut_offset_u16, offset); + generate_mut_arithmetic_harness!(u32, check_mut_offset_u32, offset); + generate_mut_arithmetic_harness!(u64, check_mut_offset_u64, offset); + generate_mut_arithmetic_harness!(u128, check_mut_offset_u128, offset); + generate_mut_arithmetic_harness!(usize, check_mut_offset_usize, offset); + + // fn <*mut T>::offset() unit type verification + generate_mut_arithmetic_harness!((), check_mut_offset_unit, offset); + + // fn <*mut T>::offset() composite type verification + generate_mut_arithmetic_harness!((i8, i8), check_mut_offset_tuple_1, offset); + generate_mut_arithmetic_harness!((f64, bool), check_mut_offset_tuple_2, offset); + generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_offset_tuple_3, offset); + generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_offset_tuple_4, offset); } From 04bd61e55faa37f4256b7ced3b4bc1fc1c529f7f Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Wed, 23 Oct 2024 19:32:34 -0700 Subject: [PATCH 11/22] updated function contracts and proof for contracts for add(), sub() and offset() --- library/core/src/ptr/mut_ptr.rs | 77 ++++++++++++++------------------- 1 file changed, 33 insertions(+), 44 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index df97e30bcbe3e..4dce768cef784 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -407,9 +407,11 @@ 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))] - #[requires(count.checked_mul(core::mem::size_of::() as isize).is_some())] - #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T) && kani::mem::can_dereference(result))] + #[requires( + count.checked_mul(core::mem::size_of::() as isize).is_some() && + kani::mem::same_allocation(self, self.wrapping_offset(count)) + )] + #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T))] pub const unsafe fn offset(self, count: isize) -> *mut T where T: Sized, @@ -954,10 +956,12 @@ 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))] - #[requires(count.checked_mul(core::mem::size_of::()).is_some() - && count * core::mem::size_of::() <= isize::MAX as usize)] - #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T) && kani::mem::can_dereference(result))] + #[requires( + count.checked_mul(core::mem::size_of::()).is_some() && + count * core::mem::size_of::() <= isize::MAX as usize && + kani::mem::same_allocation(self, self.wrapping_add(count)) + )] + #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -1033,10 +1037,12 @@ impl *mut 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))] - #[requires(count.checked_mul(core::mem::size_of::()).is_some() - && count * core::mem::size_of::() <= isize::MAX as usize)] - #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T) && kani::mem::can_dereference(result))] + #[requires( + count.checked_mul(core::mem::size_of::()).is_some() && + count * core::mem::size_of::() <= isize::MAX as usize && + kani::mem::same_allocation(self, self.wrapping_sub(count)) + )] + #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T))] pub const unsafe fn sub(self, count: usize) -> Self where T: Sized, @@ -2225,18 +2231,12 @@ mod verify { let mut test_val: $type = kani::any::<$type>(); let offset: usize = kani::any(); let count: usize = kani::any(); - if(core::mem::size_of::<$type>() == 0) { // unit type - kani::assume(offset == 0); - kani::assume(count == 0); - } else { - kani::assume(offset == 0 || offset == 1); - kani::assume(count == 0 || count == 1); - kani::assume(offset + count <= 1); - } + kani::assume(offset <= 1); + kani::assume(count <= 1); + kani::assume(offset + count <= 1); let test_ptr: *mut $type = &mut test_val; - let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset); - + let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset); unsafe { ptr_with_offset.add(count); } @@ -2248,18 +2248,12 @@ mod verify { let mut test_val: $type = kani::any::<$type>(); let offset: usize = kani::any(); let count: usize = kani::any(); - if(core::mem::size_of::<$type>() == 0) { // unit type - kani::assume(offset == 0); - kani::assume(count == 0); - } else { - kani::assume(offset == 0 || offset == 1); - kani::assume(count == 0 || count == 1); - kani::assume(count <= offset); - } + kani::assume(offset <= 1); + kani::assume(count <= 1); + kani::assume(count <= offset); let test_ptr: *mut $type = &mut test_val; let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset); - unsafe { ptr_with_offset.sub(count); } @@ -2269,19 +2263,14 @@ mod verify { #[kani::proof_for_contract(<*mut $type>::offset)] pub fn $proof_name() { let mut test_val: $type = kani::any::<$type>(); - let test_ptr: *mut $type = &mut test_val; let offset: usize = kani::any(); let count: isize = kani::any(); - if(core::mem::size_of::<$type>() == 0) { // unit type - kani::assume(offset == 0); - kani::assume(count == 0); - } else { - kani::assume(offset == 0 || offset == 1); - kani::assume(count == 0 || count == 1); - kani::assume(offset as isize + count == 0 || offset as isize + count == 1); - } - let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset); - + kani::assume(offset <= 1); + kani::assume(count >= -1 && count <= 1); + kani::assume(offset as isize + count >= 0 && offset as isize + count <= 1); + + let test_ptr: *mut $type = &mut test_val; + let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset); unsafe { ptr_with_offset.offset(count); } @@ -2304,7 +2293,7 @@ mod verify { generate_mut_arithmetic_harness!(usize, check_mut_add_usize, add); // <*mut T>:: add() unit type verification - generate_mut_arithmetic_harness!((), check_mut_add_unit, add); + // generate_mut_arithmetic_harness!((), check_mut_add_unit, add); // <*mut T>:: add() composite types verification generate_mut_arithmetic_harness!((i8, i8), check_mut_add_tuple_1, add); @@ -2327,7 +2316,7 @@ mod verify { generate_mut_arithmetic_harness!(usize, check_mut_sub_usize, sub); // <*mut T>:: sub() unit type verification - generate_mut_arithmetic_harness!((), check_mut_sub_unit, sub); + // generate_mut_arithmetic_harness!((), check_mut_sub_unit, sub); // <*mut T>:: sub() composite types verification generate_mut_arithmetic_harness!((i8, i8), check_mut_sub_tuple_1, sub); @@ -2350,7 +2339,7 @@ mod verify { generate_mut_arithmetic_harness!(usize, check_mut_offset_usize, offset); // fn <*mut T>::offset() unit type verification - generate_mut_arithmetic_harness!((), check_mut_offset_unit, offset); + // generate_mut_arithmetic_harness!((), check_mut_offset_unit, offset); // fn <*mut T>::offset() composite type verification generate_mut_arithmetic_harness!((i8, i8), check_mut_offset_tuple_1, offset); From 7557fc557da59fee7c2e8397466e0bdec84bb600 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Wed, 30 Oct 2024 18:02:43 -0700 Subject: [PATCH 12/22] added support for unit type pointers --- library/core/src/ptr/mut_ptr.rs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 4dce768cef784..c35458c8f91f3 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -409,9 +409,9 @@ impl *mut T { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires( count.checked_mul(core::mem::size_of::() as isize).is_some() && - kani::mem::same_allocation(self, self.wrapping_offset(count)) + ((core::mem::size_of::() == 0) || (kani::mem::same_allocation(self, self.wrapping_offset(count)))) )] - #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T))] + #[ensures(|result| (core::mem::size_of::() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))] pub const unsafe fn offset(self, count: isize) -> *mut T where T: Sized, @@ -959,9 +959,9 @@ impl *mut T { #[requires( count.checked_mul(core::mem::size_of::()).is_some() && count * core::mem::size_of::() <= isize::MAX as usize && - kani::mem::same_allocation(self, self.wrapping_add(count)) + ((core::mem::size_of::() == 0) || (kani::mem::same_allocation(self, self.wrapping_add(count)))) )] - #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T))] + #[ensures(|result| (core::mem::size_of::() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -1040,9 +1040,9 @@ impl *mut T { #[requires( count.checked_mul(core::mem::size_of::()).is_some() && count * core::mem::size_of::() <= isize::MAX as usize && - kani::mem::same_allocation(self, self.wrapping_sub(count)) + ((core::mem::size_of::() == 0) || (kani::mem::same_allocation(self, self.wrapping_sub(count)))) )] - #[ensures(|result| kani::mem::same_allocation(self as *const T, *result as *const T))] + #[ensures(|result| (core::mem::size_of::() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))] pub const unsafe fn sub(self, count: usize) -> Self where T: Sized, @@ -2293,7 +2293,7 @@ mod verify { generate_mut_arithmetic_harness!(usize, check_mut_add_usize, add); // <*mut T>:: add() unit type verification - // generate_mut_arithmetic_harness!((), check_mut_add_unit, add); + generate_mut_arithmetic_harness!((), check_mut_add_unit, add); // <*mut T>:: add() composite types verification generate_mut_arithmetic_harness!((i8, i8), check_mut_add_tuple_1, add); @@ -2316,7 +2316,7 @@ mod verify { generate_mut_arithmetic_harness!(usize, check_mut_sub_usize, sub); // <*mut T>:: sub() unit type verification - // generate_mut_arithmetic_harness!((), check_mut_sub_unit, sub); + generate_mut_arithmetic_harness!((), check_mut_sub_unit, sub); // <*mut T>:: sub() composite types verification generate_mut_arithmetic_harness!((i8, i8), check_mut_sub_tuple_1, sub); @@ -2339,7 +2339,7 @@ mod verify { generate_mut_arithmetic_harness!(usize, check_mut_offset_usize, offset); // fn <*mut T>::offset() unit type verification - // generate_mut_arithmetic_harness!((), check_mut_offset_unit, offset); + generate_mut_arithmetic_harness!((), check_mut_offset_unit, offset); // fn <*mut T>::offset() composite type verification generate_mut_arithmetic_harness!((i8, i8), check_mut_offset_tuple_1, offset); From 76b231170608507847b56f21c954e424b01c76b6 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Wed, 6 Nov 2024 09:45:25 -0800 Subject: [PATCH 13/22] updated function contracts, removed unnecessary kani::assmue --- library/core/src/ptr/mut_ptr.rs | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index c35458c8f91f3..efc9e9095eb84 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -409,6 +409,7 @@ impl *mut T { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires( count.checked_mul(core::mem::size_of::() as isize).is_some() && + (self as isize).checked_add((count * core::mem::size_of::() as isize)).is_some() && ((core::mem::size_of::() == 0) || (kani::mem::same_allocation(self, self.wrapping_offset(count)))) )] #[ensures(|result| (core::mem::size_of::() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))] @@ -959,6 +960,7 @@ impl *mut T { #[requires( count.checked_mul(core::mem::size_of::()).is_some() && count * core::mem::size_of::() <= isize::MAX as usize && + (self as isize).checked_add((count * core::mem::size_of::()) as isize).is_some() && ((core::mem::size_of::() == 0) || (kani::mem::same_allocation(self, self.wrapping_add(count)))) )] #[ensures(|result| (core::mem::size_of::() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))] @@ -1040,6 +1042,7 @@ impl *mut T { #[requires( count.checked_mul(core::mem::size_of::()).is_some() && count * core::mem::size_of::() <= isize::MAX as usize && + (self as isize).checked_sub((count * core::mem::size_of::()) as isize).is_some() && ((core::mem::size_of::() == 0) || (kani::mem::same_allocation(self, self.wrapping_sub(count)))) )] #[ensures(|result| (core::mem::size_of::() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))] @@ -2232,8 +2235,8 @@ mod verify { let offset: usize = kani::any(); let count: usize = kani::any(); kani::assume(offset <= 1); - kani::assume(count <= 1); - kani::assume(offset + count <= 1); + // kani::assume(count <= 1); + // kani::assume(offset + count <= 1); let test_ptr: *mut $type = &mut test_val; let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset); @@ -2249,8 +2252,8 @@ mod verify { let offset: usize = kani::any(); let count: usize = kani::any(); kani::assume(offset <= 1); - kani::assume(count <= 1); - kani::assume(count <= offset); + // kani::assume(count <= 1); + // kani::assume(count <= offset); let test_ptr: *mut $type = &mut test_val; let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset); @@ -2266,8 +2269,8 @@ mod verify { let offset: usize = kani::any(); let count: isize = kani::any(); kani::assume(offset <= 1); - kani::assume(count >= -1 && count <= 1); - kani::assume(offset as isize + count >= 0 && offset as isize + count <= 1); + // kani::assume(count >= -1 && count <= 1); + // kani::assume(offset as isize + count >= 0 && offset as isize + count <= 1); let test_ptr: *mut $type = &mut test_val; let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset); From cb6a17713edc486417a8b7e7e1c2f76eb70424fa Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Wed, 6 Nov 2024 10:18:16 -0800 Subject: [PATCH 14/22] added comments to function contracts --- library/core/src/ptr/mut_ptr.rs | 38 ++++++++++++++++++++++++--------- 1 file changed, 28 insertions(+), 10 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index efc9e9095eb84..faef82ffb343a 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -408,10 +408,18 @@ impl *mut 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 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 as *const T, *result as *const T))] pub const unsafe fn offset(self, count: isize) -> *mut T where @@ -958,11 +966,19 @@ impl *mut T { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires( - count.checked_mul(core::mem::size_of::()).is_some() && - count * core::mem::size_of::() <= isize::MAX as usize && - (self as isize).checked_add((count * core::mem::size_of::()) as isize).is_some() && - ((core::mem::size_of::() == 0) || (kani::mem::same_allocation(self, self.wrapping_add(count)))) + // 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 as *const T, *result as *const T))] pub const unsafe fn add(self, count: usize) -> Self where @@ -1040,11 +1056,19 @@ impl *mut 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 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 as *const T, *result as *const T))] pub const unsafe fn sub(self, count: usize) -> Self where @@ -2235,8 +2259,6 @@ mod verify { let offset: usize = kani::any(); let count: usize = kani::any(); kani::assume(offset <= 1); - // kani::assume(count <= 1); - // kani::assume(offset + count <= 1); let test_ptr: *mut $type = &mut test_val; let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset); @@ -2252,8 +2274,6 @@ mod verify { let offset: usize = kani::any(); let count: usize = kani::any(); kani::assume(offset <= 1); - // kani::assume(count <= 1); - // kani::assume(count <= offset); let test_ptr: *mut $type = &mut test_val; let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset); @@ -2269,8 +2289,6 @@ mod verify { let offset: usize = kani::any(); let count: isize = kani::any(); kani::assume(offset <= 1); - // kani::assume(count >= -1 && count <= 1); - // kani::assume(offset as isize + count >= 0 && offset as isize + count <= 1); let test_ptr: *mut $type = &mut test_val; let ptr_with_offset: *mut $type = test_ptr.wrapping_add(offset); From a079a7aff712202235ff7200de998149fe4e4728 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Wed, 6 Nov 2024 18:18:34 -0800 Subject: [PATCH 15/22] added comments for magic numbers --- library/core/src/ptr/mut_ptr.rs | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index faef82ffb343a..d06166d4c6255 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2251,6 +2251,7 @@ impl PartialOrd for *mut T { mod verify { use crate::kani; + // generate proof for contracts for integer type, composite type and unit type pointers macro_rules! generate_mut_arithmetic_harness { ($type:ty, $proof_name:ident, add) => { #[kani::proof_for_contract(<*mut $type>::add)] @@ -2258,9 +2259,11 @@ mod verify { let mut test_val: $type = kani::any::<$type>(); let offset: usize = kani::any(); let count: usize = kani::any(); - kani::assume(offset <= 1); - let test_ptr: *mut $type = &mut 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: *mut $type = test_ptr.wrapping_add(offset); unsafe { ptr_with_offset.add(count); @@ -2273,9 +2276,11 @@ mod verify { let mut test_val: $type = kani::any::<$type>(); let offset: usize = kani::any(); let count: usize = kani::any(); - kani::assume(offset <= 1); - let test_ptr: *mut $type = &mut 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: *mut $type = test_ptr.wrapping_add(offset); unsafe { ptr_with_offset.sub(count); @@ -2288,9 +2293,11 @@ mod verify { let mut test_val: $type = kani::any::<$type>(); let offset: usize = kani::any(); let count: isize = kani::any(); - kani::assume(offset <= 1); - let test_ptr: *mut $type = &mut 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: *mut $type = test_ptr.wrapping_add(offset); unsafe { ptr_with_offset.offset(count); From 51ded418fdcf72432e984591edabd013ce7132af Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Thu, 14 Nov 2024 18:43:26 -0800 Subject: [PATCH 16/22] updated proofs using pointer generator --- library/core/src/ptr/mut_ptr.rs | 52 ++++++++++++++------------------- 1 file changed, 22 insertions(+), 30 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 7b56a4e9eedc8..294c1f271a170 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2356,56 +2356,47 @@ impl PartialOrd for *mut T { mod verify { use crate::kani; - // 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 contract. macro_rules! generate_mut_arithmetic_harness { ($type:ty, $proof_name:ident, add) => { #[kani::proof_for_contract(<*mut $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: *mut $type = &mut 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: *mut $type = test_ptr.wrapping_add(offset); + // 200 bytes is large enough to cover all pointee types used for testing + const BUF_SIZE: usize = 200; + let mut generator = kani::PointerGenerator::< BUF_SIZE >::new(); + let test_ptr: *mut $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(<*mut $type>::sub)] pub fn $proof_name() { - let mut test_val: $type = kani::any::<$type>(); - let offset: usize = kani::any(); + // 200 bytes is large enough to cover all pointee types used for testing + const BUF_SIZE: usize = 200; + let mut generator = kani::PointerGenerator::< BUF_SIZE >::new(); + let test_ptr: *mut $type = generator.any_in_bounds().ptr; let count: usize = kani::any(); - let test_ptr: *mut $type = &mut 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: *mut $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(<*mut $type>::offset)] pub fn $proof_name() { - let mut test_val: $type = kani::any::<$type>(); - let offset: usize = kani::any(); + // 200 bytes is large enough to cover all pointee types used for testing + const BUF_SIZE: usize = 200; + let mut generator = kani::PointerGenerator::< BUF_SIZE >::new(); + let test_ptr: *mut $type = generator.any_in_bounds().ptr; let count: isize = kani::any(); - let test_ptr: *mut $type = &mut 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: *mut $type = test_ptr.wrapping_add(offset); unsafe { - ptr_with_offset.offset(count); + test_ptr.offset(count); } } }; @@ -2418,7 +2409,8 @@ mod verify { generate_mut_arithmetic_harness!(i64, check_mut_add_i64, add); generate_mut_arithmetic_harness!(i128, check_mut_add_i128, add); generate_mut_arithmetic_harness!(isize, check_mut_add_isize, add); - generate_mut_arithmetic_harness!(u8, check_mut_add_u8, add); + // Encountered a bug after using the pointer generator; will uncomment once resolved. + // generate_mut_arithmetic_harness!(u8, check_mut_add_u8, add); generate_mut_arithmetic_harness!(u16, check_mut_add_u16, add); generate_mut_arithmetic_harness!(u32, check_mut_add_u32, add); generate_mut_arithmetic_harness!(u64, check_mut_add_u64, add); From fb6215e8f149dcb7c5347147c051a9dd5779bf63 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Thu, 14 Nov 2024 18:57:33 -0800 Subject: [PATCH 17/22] fixed typos in comments --- library/core/src/ptr/mut_ptr.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 294c1f271a170..5b6b61d606e2f 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2364,7 +2364,7 @@ mod verify { ($type:ty, $proof_name:ident, add) => { #[kani::proof_for_contract(<*mut $type>::add)] pub fn $proof_name() { - // 200 bytes is large enough to cover all pointee types used for testing + // 200 bytes are large enough to cover all pointee types used for testing const BUF_SIZE: usize = 200; let mut generator = kani::PointerGenerator::< BUF_SIZE >::new(); let test_ptr: *mut $type = generator.any_in_bounds().ptr; @@ -2377,7 +2377,7 @@ mod verify { ($type:ty, $proof_name:ident, sub) => { #[kani::proof_for_contract(<*mut $type>::sub)] pub fn $proof_name() { - // 200 bytes is large enough to cover all pointee types used for testing + // 200 bytes are large enough to cover all pointee types used for testing const BUF_SIZE: usize = 200; let mut generator = kani::PointerGenerator::< BUF_SIZE >::new(); let test_ptr: *mut $type = generator.any_in_bounds().ptr; @@ -2390,7 +2390,7 @@ mod verify { ($type:ty, $proof_name:ident, offset) => { #[kani::proof_for_contract(<*mut $type>::offset)] pub fn $proof_name() { - // 200 bytes is large enough to cover all pointee types used for testing + // 200 bytes are large enough to cover all pointee types used for testing const BUF_SIZE: usize = 200; let mut generator = kani::PointerGenerator::< BUF_SIZE >::new(); let test_ptr: *mut $type = generator.any_in_bounds().ptr; @@ -2410,7 +2410,7 @@ mod verify { generate_mut_arithmetic_harness!(i128, check_mut_add_i128, add); generate_mut_arithmetic_harness!(isize, check_mut_add_isize, add); // Encountered a bug after using the pointer generator; will uncomment once resolved. - // generate_mut_arithmetic_harness!(u8, check_mut_add_u8, add); + generate_mut_arithmetic_harness!(u8, check_mut_add_u8, add); generate_mut_arithmetic_harness!(u16, check_mut_add_u16, add); generate_mut_arithmetic_harness!(u32, check_mut_add_u32, add); generate_mut_arithmetic_harness!(u64, check_mut_add_u64, add); From f229fd99b8f8f6bc86f0f142404d66b54904cfee Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Thu, 14 Nov 2024 18:59:48 -0800 Subject: [PATCH 18/22] rustfmt formatting --- library/core/src/ptr/mut_ptr.rs | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 5b6b61d606e2f..4aed8bed44bc9 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -98,7 +98,10 @@ impl *mut T { /// // This dereference is UB. The pointer only has provenance for `x` but points to `y`. /// 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) -> *mut U @@ -416,7 +419,7 @@ impl *mut 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 as *const T, *result as *const T))] pub const unsafe fn offset(self, count: isize) -> *mut T where @@ -1029,7 +1032,7 @@ impl *mut 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 as *const T, *result as *const T))] pub const unsafe fn add(self, count: usize) -> Self where @@ -1153,7 +1156,7 @@ impl *mut 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 as *const T, *result as *const T))] pub const unsafe fn sub(self, count: usize) -> Self where @@ -2365,8 +2368,8 @@ mod verify { #[kani::proof_for_contract(<*mut $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::< BUF_SIZE >::new(); + const BUF_SIZE: usize = 200; + let mut generator = kani::PointerGenerator::::new(); let test_ptr: *mut $type = generator.any_in_bounds().ptr; let count: usize = kani::any(); unsafe { @@ -2378,8 +2381,8 @@ mod verify { #[kani::proof_for_contract(<*mut $type>::sub)] 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::< BUF_SIZE >::new(); + const BUF_SIZE: usize = 200; + let mut generator = kani::PointerGenerator::::new(); let test_ptr: *mut $type = generator.any_in_bounds().ptr; let count: usize = kani::any(); unsafe { @@ -2391,8 +2394,8 @@ mod verify { #[kani::proof_for_contract(<*mut $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::< BUF_SIZE >::new(); + const BUF_SIZE: usize = 200; + let mut generator = kani::PointerGenerator::::new(); let test_ptr: *mut $type = generator.any_in_bounds().ptr; let count: isize = kani::any(); unsafe { @@ -2415,7 +2418,7 @@ mod verify { generate_mut_arithmetic_harness!(u32, check_mut_add_u32, add); generate_mut_arithmetic_harness!(u64, check_mut_add_u64, add); generate_mut_arithmetic_harness!(u128, check_mut_add_u128, add); - generate_mut_arithmetic_harness!(usize, check_mut_add_usize, add); + generate_mut_arithmetic_harness!(usize, check_mut_add_usize, add); // <*mut T>:: add() unit type verification generate_mut_arithmetic_harness!((), check_mut_add_unit, add); @@ -2447,7 +2450,7 @@ mod verify { generate_mut_arithmetic_harness!((i8, i8), check_mut_sub_tuple_1, sub); generate_mut_arithmetic_harness!((f64, bool), check_mut_sub_tuple_2, sub); generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_sub_tuple_3, sub); - generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_sub_tuple_4, sub); + generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_sub_tuple_4, sub); // fn <*mut T>::offset() integer types verification generate_mut_arithmetic_harness!(i8, check_mut_offset_i8, offset); From 20fffa3fb11abbadbb9621f1d00f1120248ed5ff Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Thu, 14 Nov 2024 19:01:56 -0800 Subject: [PATCH 19/22] reverse unnecessary rustfmt formatting --- library/core/src/ptr/mut_ptr.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 4aed8bed44bc9..03a6ef9f5604c 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -98,10 +98,7 @@ impl *mut T { /// // This dereference is UB. The pointer only has provenance for `x` but points to `y`. /// 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) -> *mut U From b9054a8a17c314c2a7d1c48b7fa09a0876f9648d Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Fri, 15 Nov 2024 16:26:44 -0800 Subject: [PATCH 20/22] temporary disabled check_mut_add_u8 test --- library/core/src/ptr/mut_ptr.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 03a6ef9f5604c..86fd8ee7f76a8 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2409,8 +2409,8 @@ mod verify { generate_mut_arithmetic_harness!(i64, check_mut_add_i64, add); generate_mut_arithmetic_harness!(i128, check_mut_add_i128, add); generate_mut_arithmetic_harness!(isize, check_mut_add_isize, add); - // Encountered a bug after using the pointer generator; will uncomment once resolved. - generate_mut_arithmetic_harness!(u8, check_mut_add_u8, add); + // Due to a bug of kani this test case is malfunctioning for now + // generate_mut_arithmetic_harness!(u8, check_mut_add_u8, add); generate_mut_arithmetic_harness!(u16, check_mut_add_u16, add); generate_mut_arithmetic_harness!(u32, check_mut_add_u32, add); generate_mut_arithmetic_harness!(u64, check_mut_add_u64, add); From b528b0e28c8bc41a51dc3e43240e5d2fc4722b76 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Tue, 26 Nov 2024 22:13:09 -0800 Subject: [PATCH 21/22] Clarified preconditions with additional notes --- library/core/src/ptr/mut_ptr.rs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 86fd8ee7f76a8..82234bad672be 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -404,6 +404,8 @@ 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 + // Note: It is the caller's responsibility to ensure that `self` is non-null and properly aligned. + // These conditions are not verified as part of the preconditions. #[requires( // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize` count.checked_mul(core::mem::size_of::() as isize).is_some() && @@ -1016,6 +1018,8 @@ 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 + // Note: It is the caller's responsibility to ensure that `self` is non-null and properly aligned. + // These conditions are not verified as part of the preconditions. #[requires( // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize` count.checked_mul(core::mem::size_of::()).is_some() && @@ -1140,6 +1144,8 @@ impl *mut T { #[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_neg))] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + // Note: It is the caller's responsibility to ensure that `self` is non-null and properly aligned. + // These conditions are not verified as part of the preconditions. #[requires( // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize` count.checked_mul(core::mem::size_of::()).is_some() && From 9b90b233437b789f14ead0fc96e707d446997f92 Mon Sep 17 00:00:00 2001 From: Yifei Wang <1277495324@qq.com> Date: Tue, 26 Nov 2024 22:40:36 -0800 Subject: [PATCH 22/22] added tracking issue info for the pointer generator bug --- library/core/src/ptr/mut_ptr.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 82234bad672be..34ab472735915 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2415,7 +2415,8 @@ mod verify { generate_mut_arithmetic_harness!(i64, check_mut_add_i64, add); generate_mut_arithmetic_harness!(i128, check_mut_add_i128, add); generate_mut_arithmetic_harness!(isize, check_mut_add_isize, add); - // Due to a bug of kani this test case is malfunctioning for now + // Due to a bug of kani this test case is malfunctioning for now. + // Tracking issue: https://github.com/model-checking/kani/issues/3743 // generate_mut_arithmetic_harness!(u8, check_mut_add_u8, add); generate_mut_arithmetic_harness!(u16, check_mut_add_u16, add); generate_mut_arithmetic_harness!(u32, check_mut_add_u32, add);