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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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/30] 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); From afe1b165ac68d581f3493dffe6f06760a3b899c8 Mon Sep 17 00:00:00 2001 From: szlee118 Date: Mon, 2 Dec 2024 00:23:40 -0800 Subject: [PATCH 23/30] Add proof for String:remove --- library/alloc/src/string.rs | 40 +++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs index b042720933b6d..55c9e135cda84 100644 --- a/library/alloc/src/string.rs +++ b/library/alloc/src/string.rs @@ -67,6 +67,7 @@ use crate::str::{self, Chars, Utf8Error, from_utf8_unchecked_mut}; use crate::str::{FromStr, from_boxed_utf8_unchecked}; use crate::vec::Vec; + /// A UTF-8–encoded, growable string. /// /// `String` is the most common string type. It has ownership over the contents @@ -3217,3 +3218,42 @@ impl From for String { c.to_string() } } + + + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use core::kani; + use crate::string::String; + + #[kani::proof] + #[kani::unwind(9)] + fn check_remove() { + // Use a small fixed-length ASCII string to avoid UTF-8 complexity + let arr: [u8; 8] = kani::any(); + for &byte in &arr { + kani::assume(byte.is_ascii()); // Constrain to ASCII characters + } + + // Convert byte array to a String directly (safe since all are ASCII) + let mut s = unsafe { String::from_utf8_unchecked(arr.to_vec()) }; + + // Ensure the string is not empty + kani::assume(!s.is_empty()); + + // Generate a valid index within the bounds of the string + let idx: usize = kani::any(); + kani::assume(idx < s.len()); + + // Call the `remove` function + let removed_char = s.remove(idx); + + // Verify the string length decreases correctly + assert_eq!(s.len(), arr.len() - 1); + + // Verify the removed character is a valid ASCII character + assert!(removed_char.is_ascii()); + } +} + From 80b3f912eb9e8a73115b7e7cdb2d4e4d78ea1f45 Mon Sep 17 00:00:00 2001 From: szlee118 Date: Mon, 2 Dec 2024 20:11:58 -0800 Subject: [PATCH 24/30] Use any_array at creation --- library/alloc/src/string.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs index 55c9e135cda84..8657c642a7af1 100644 --- a/library/alloc/src/string.rs +++ b/library/alloc/src/string.rs @@ -3230,8 +3230,8 @@ mod verify { #[kani::proof] #[kani::unwind(9)] fn check_remove() { - // Use a small fixed-length ASCII string to avoid UTF-8 complexity - let arr: [u8; 8] = kani::any(); + + let arr: [u8; 8] = kani::Arbitrary::any_array(); for &byte in &arr { kani::assume(byte.is_ascii()); // Constrain to ASCII characters } From 6e974384cfcaa7e2789ebfb94eaaa04d188b8a82 Mon Sep 17 00:00:00 2001 From: szlee118 Date: Wed, 4 Dec 2024 22:34:12 -0800 Subject: [PATCH 25/30] align mut_ptr with usage_proofs branch --- library/core/src/ptr/mut_ptr.rs | 543 +++++++++++--------------------- 1 file changed, 191 insertions(+), 352 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 34ab472735915..7225169b93ddc 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -33,7 +33,7 @@ impl *mut T { /// assert!(!ptr.is_null()); /// ``` #[stable(feature = "rust1", since = "1.0.0")] - #[rustc_const_unstable(feature = "const_ptr_is_null", issue = "74939")] + #[rustc_const_stable(feature = "const_ptr_is_null", since = "CURRENT_RUSTC_VERSION")] #[rustc_diagnostic_item = "ptr_is_null"] #[inline] pub const fn is_null(self) -> bool { @@ -229,7 +229,6 @@ impl *mut T { /// /// The pointer can be later reconstructed with [`from_raw_parts_mut`]. #[unstable(feature = "ptr_metadata", issue = "81513")] - #[rustc_const_unstable(feature = "ptr_metadata", issue = "81513")] #[inline] pub const fn to_raw_parts(self) -> (*mut (), ::Metadata) { (self.cast(), super::metadata(self)) @@ -276,7 +275,7 @@ impl *mut T { /// } /// ``` #[stable(feature = "ptr_as_ref", since = "1.9.0")] - #[rustc_const_unstable(feature = "const_ptr_is_null", issue = "74939")] + #[rustc_const_stable(feature = "const_ptr_is_null", since = "CURRENT_RUSTC_VERSION")] #[inline] pub const unsafe fn as_ref<'a>(self) -> Option<&'a T> { // SAFETY: the caller must guarantee that `self` is valid for a @@ -310,7 +309,6 @@ impl *mut T { /// ``` // FIXME: mention it in the docs for `as_ref` and `as_uninit_ref` once stabilized. #[unstable(feature = "ptr_as_ref_unchecked", issue = "122034")] - #[rustc_const_unstable(feature = "ptr_as_ref_unchecked", issue = "122034")] #[inline] #[must_use] pub const unsafe fn as_ref_unchecked<'a>(self) -> &'a T { @@ -407,10 +405,11 @@ impl *mut T { // 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() && - // Precondition 2: adding the computed offset to `self` does not cause overflow - (self as isize).checked_add((count * core::mem::size_of::() as isize)).is_some() && + // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize`. + // Precondition 2: adding the computed offset to `self` does not cause overflow. + // These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani. + count.checked_mul(core::mem::size_of::() as isize) + .map_or(false, |computed_offset| (self as isize).checked_add(computed_offset).is_some()) && // Precondition 3: If `T` is a unit type (`size_of::() == 0`), this check is unnecessary as it has no allocated memory. // Otherwise, for non-unit types, `self` and `self.wrapping_offset(count)` should point to the same allocated object, // restricting `count` to prevent crossing allocation boundaries. @@ -427,23 +426,21 @@ impl *mut T { #[inline] #[rustc_allow_const_fn_unstable(const_eval_select)] const fn runtime_offset_nowrap(this: *const (), count: isize, size: usize) -> bool { - #[inline] - fn runtime(this: *const (), count: isize, size: usize) -> bool { - // `size` is the size of a Rust type, so we know that - // `size <= isize::MAX` and thus `as` cast here is not lossy. - let Some(byte_offset) = count.checked_mul(size as isize) else { - return false; - }; - let (_, overflow) = this.addr().overflowing_add_signed(byte_offset); - !overflow - } - - const fn comptime(_: *const (), _: isize, _: usize) -> bool { - true - } - // We can use const_eval_select here because this is only for UB checks. - intrinsics::const_eval_select((this, count, size), comptime, runtime) + const_eval_select!( + @capture { this: *const (), count: isize, size: usize } -> bool: + if const { + true + } else { + // `size` is the size of a Rust type, so we know that + // `size <= isize::MAX` and thus `as` cast here is not lossy. + let Some(byte_offset) = count.checked_mul(size as isize) else { + return false; + }; + let (_, overflow) = this.addr().overflowing_add_signed(byte_offset); + !overflow + } + ) } ub_checks::assert_unsafe_precondition!( @@ -643,7 +640,7 @@ impl *mut T { /// println!("{s:?}"); // It'll print: "[4, 2, 3]". /// ``` #[stable(feature = "ptr_as_ref", since = "1.9.0")] - #[rustc_const_unstable(feature = "const_ptr_is_null", issue = "74939")] + #[rustc_const_stable(feature = "const_ptr_is_null", since = "CURRENT_RUSTC_VERSION")] #[inline] pub const unsafe fn as_mut<'a>(self) -> Option<&'a mut T> { // SAFETY: the caller must guarantee that `self` is be valid for @@ -679,7 +676,6 @@ impl *mut T { /// ``` // FIXME: mention it in the docs for `as_mut` and `as_uninit_mut` once stabilized. #[unstable(feature = "ptr_as_ref_unchecked", issue = "122034")] - #[rustc_const_unstable(feature = "ptr_as_ref_unchecked", issue = "122034")] #[inline] #[must_use] pub const unsafe fn as_mut_unchecked<'a>(self) -> &'a mut T { @@ -1021,11 +1017,13 @@ impl *mut T { // 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() && - count * core::mem::size_of::() <= isize::MAX as usize && - // Precondition 2: adding the computed offset to `self` does not cause overflow - (self as isize).checked_add((count * core::mem::size_of::()) as isize).is_some() && + // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize`. + // Precondition 2: adding the computed offset to `self` does not cause overflow. + // These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani. + count.checked_mul(core::mem::size_of::()) + .map_or(false, |computed_offset| { + computed_offset <= isize::MAX as usize && (self as isize).checked_add(computed_offset as isize).is_some() + }) && // Precondition 3: If `T` is a unit type (`size_of::() == 0`), this check is unnecessary as it has no allocated memory. // Otherwise, for non-unit types, `self` and `self.wrapping_add(count)` should point to the same allocated object, // restricting `count` to prevent crossing allocation boundaries. @@ -1043,20 +1041,18 @@ impl *mut T { #[inline] #[rustc_allow_const_fn_unstable(const_eval_select)] const fn runtime_add_nowrap(this: *const (), count: usize, size: usize) -> bool { - #[inline] - fn runtime(this: *const (), count: usize, size: usize) -> bool { - let Some(byte_offset) = count.checked_mul(size) else { - return false; - }; - let (_, overflow) = this.addr().overflowing_add(byte_offset); - byte_offset <= (isize::MAX as usize) && !overflow - } - - const fn comptime(_: *const (), _: usize, _: usize) -> bool { - true - } - - intrinsics::const_eval_select((this, count, size), comptime, runtime) + const_eval_select!( + @capture { this: *const (), count: usize, size: usize } -> bool: + if const { + true + } else { + let Some(byte_offset) = count.checked_mul(size) else { + return false; + }; + let (_, overflow) = this.addr().overflowing_add(byte_offset); + byte_offset <= (isize::MAX as usize) && !overflow + } + ) } #[cfg(debug_assertions)] // Expensive, and doesn't catch much in the wild. @@ -1147,11 +1143,13 @@ impl *mut T { // 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() && - count * core::mem::size_of::() <= isize::MAX as usize && - // Precondition 2: subtracting the computed offset from `self` does not cause overflow - (self as isize).checked_sub((count * core::mem::size_of::()) as isize).is_some() && + // Precondition 1: the computed offset `count * size_of::()` does not overflow `isize`. + // Precondition 2: substracting the computed offset from `self` does not cause overflow. + // These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani. + count.checked_mul(core::mem::size_of::()) + .map_or(false, |computed_offset| { + computed_offset <= isize::MAX as usize && (self as isize).checked_sub(computed_offset as isize).is_some() + }) && // Precondition 3: If `T` is a unit type (`size_of::() == 0`), this check is unnecessary as it has no allocated memory. // Otherwise, for non-unit types, `self` and `self.wrapping_sub(count)` should point to the same allocated object, // restricting `count` to prevent crossing allocation boundaries. @@ -1169,19 +1167,17 @@ impl *mut T { #[inline] #[rustc_allow_const_fn_unstable(const_eval_select)] const fn runtime_sub_nowrap(this: *const (), count: usize, size: usize) -> bool { - #[inline] - fn runtime(this: *const (), count: usize, size: usize) -> bool { - let Some(byte_offset) = count.checked_mul(size) else { - return false; - }; - byte_offset <= (isize::MAX as usize) && this.addr() >= byte_offset - } - - const fn comptime(_: *const (), _: usize, _: usize) -> bool { - true - } - - intrinsics::const_eval_select((this, count, size), comptime, runtime) + const_eval_select!( + @capture { this: *const (), count: usize, size: usize } -> bool: + if const { + true + } else { + let Some(byte_offset) = count.checked_mul(size) else { + return false; + }; + byte_offset <= (isize::MAX as usize) && this.addr() >= byte_offset + } + ) } #[cfg(debug_assertions)] // Expensive, and doesn't catch much in the wild. @@ -1693,8 +1689,7 @@ impl *mut T { #[must_use] #[inline] #[stable(feature = "align_offset", since = "1.36.0")] - #[rustc_const_unstable(feature = "const_align_offset", issue = "90962")] - pub const fn align_offset(self, align: usize) -> usize + pub fn align_offset(self, align: usize) -> usize where T: Sized, { @@ -1732,95 +1727,10 @@ impl *mut T { /// assert!(ptr.is_aligned()); /// assert!(!ptr.wrapping_byte_add(1).is_aligned()); /// ``` - /// - /// # At compiletime - /// **Note: Alignment at compiletime is experimental and subject to change. See the - /// [tracking issue] for details.** - /// - /// At compiletime, the compiler may not know where a value will end up in memory. - /// Calling this function on a pointer created from a reference at compiletime will only - /// return `true` if the pointer is guaranteed to be aligned. This means that the pointer - /// is never aligned if cast to a type with a stricter alignment than the reference's - /// underlying allocation. - /// - /// ``` - /// #![feature(const_pointer_is_aligned)] - /// - /// // On some platforms, the alignment of primitives is less than their size. - /// #[repr(align(4))] - /// struct AlignedI32(i32); - /// #[repr(align(8))] - /// struct AlignedI64(i64); - /// - /// const _: () = { - /// let mut data = AlignedI32(42); - /// let ptr = &mut data as *mut AlignedI32; - /// assert!(ptr.is_aligned()); - /// - /// // At runtime either `ptr1` or `ptr2` would be aligned, but at compiletime neither is aligned. - /// let ptr1 = ptr.cast::(); - /// let ptr2 = ptr.wrapping_add(1).cast::(); - /// assert!(!ptr1.is_aligned()); - /// assert!(!ptr2.is_aligned()); - /// }; - /// ``` - /// - /// Due to this behavior, it is possible that a runtime pointer derived from a compiletime - /// pointer is aligned, even if the compiletime pointer wasn't aligned. - /// - /// ``` - /// #![feature(const_pointer_is_aligned)] - /// - /// // On some platforms, the alignment of primitives is less than their size. - /// #[repr(align(4))] - /// struct AlignedI32(i32); - /// #[repr(align(8))] - /// struct AlignedI64(i64); - /// - /// // At compiletime, neither `COMPTIME_PTR` nor `COMPTIME_PTR + 1` is aligned. - /// // Also, note that mutable references are not allowed in the final value of constants. - /// const COMPTIME_PTR: *mut AlignedI32 = (&AlignedI32(42) as *const AlignedI32).cast_mut(); - /// const _: () = assert!(!COMPTIME_PTR.cast::().is_aligned()); - /// const _: () = assert!(!COMPTIME_PTR.wrapping_add(1).cast::().is_aligned()); - /// - /// // At runtime, either `runtime_ptr` or `runtime_ptr + 1` is aligned. - /// let runtime_ptr = COMPTIME_PTR; - /// assert_ne!( - /// runtime_ptr.cast::().is_aligned(), - /// runtime_ptr.wrapping_add(1).cast::().is_aligned(), - /// ); - /// ``` - /// - /// If a pointer is created from a fixed address, this function behaves the same during - /// runtime and compiletime. - /// - /// ``` - /// #![feature(const_pointer_is_aligned)] - /// - /// // On some platforms, the alignment of primitives is less than their size. - /// #[repr(align(4))] - /// struct AlignedI32(i32); - /// #[repr(align(8))] - /// struct AlignedI64(i64); - /// - /// const _: () = { - /// let ptr = 40 as *mut AlignedI32; - /// assert!(ptr.is_aligned()); - /// - /// // For pointers with a known address, runtime and compiletime behavior are identical. - /// let ptr1 = ptr.cast::(); - /// let ptr2 = ptr.wrapping_add(1).cast::(); - /// assert!(ptr1.is_aligned()); - /// assert!(!ptr2.is_aligned()); - /// }; - /// ``` - /// - /// [tracking issue]: https://github.com/rust-lang/rust/issues/104203 #[must_use] #[inline] #[stable(feature = "pointer_is_aligned", since = "1.79.0")] - #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")] - pub const fn is_aligned(self) -> bool + pub fn is_aligned(self) -> bool where T: Sized, { @@ -1857,106 +1767,15 @@ impl *mut T { /// /// assert_ne!(ptr.is_aligned_to(8), ptr.wrapping_add(1).is_aligned_to(8)); /// ``` - /// - /// # At compiletime - /// **Note: Alignment at compiletime is experimental and subject to change. See the - /// [tracking issue] for details.** - /// - /// At compiletime, the compiler may not know where a value will end up in memory. - /// Calling this function on a pointer created from a reference at compiletime will only - /// return `true` if the pointer is guaranteed to be aligned. This means that the pointer - /// cannot be stricter aligned than the reference's underlying allocation. - /// - /// ``` - /// #![feature(pointer_is_aligned_to)] - /// #![feature(const_pointer_is_aligned)] - /// - /// // On some platforms, the alignment of i32 is less than 4. - /// #[repr(align(4))] - /// struct AlignedI32(i32); - /// - /// const _: () = { - /// let mut data = AlignedI32(42); - /// let ptr = &mut data as *mut AlignedI32; - /// - /// assert!(ptr.is_aligned_to(1)); - /// assert!(ptr.is_aligned_to(2)); - /// assert!(ptr.is_aligned_to(4)); - /// - /// // At compiletime, we know for sure that the pointer isn't aligned to 8. - /// assert!(!ptr.is_aligned_to(8)); - /// assert!(!ptr.wrapping_add(1).is_aligned_to(8)); - /// }; - /// ``` - /// - /// Due to this behavior, it is possible that a runtime pointer derived from a compiletime - /// pointer is aligned, even if the compiletime pointer wasn't aligned. - /// - /// ``` - /// #![feature(pointer_is_aligned_to)] - /// #![feature(const_pointer_is_aligned)] - /// - /// // On some platforms, the alignment of i32 is less than 4. - /// #[repr(align(4))] - /// struct AlignedI32(i32); - /// - /// // At compiletime, neither `COMPTIME_PTR` nor `COMPTIME_PTR + 1` is aligned. - /// // Also, note that mutable references are not allowed in the final value of constants. - /// const COMPTIME_PTR: *mut AlignedI32 = (&AlignedI32(42) as *const AlignedI32).cast_mut(); - /// const _: () = assert!(!COMPTIME_PTR.is_aligned_to(8)); - /// const _: () = assert!(!COMPTIME_PTR.wrapping_add(1).is_aligned_to(8)); - /// - /// // At runtime, either `runtime_ptr` or `runtime_ptr + 1` is aligned. - /// let runtime_ptr = COMPTIME_PTR; - /// assert_ne!( - /// runtime_ptr.is_aligned_to(8), - /// runtime_ptr.wrapping_add(1).is_aligned_to(8), - /// ); - /// ``` - /// - /// If a pointer is created from a fixed address, this function behaves the same during - /// runtime and compiletime. - /// - /// ``` - /// #![feature(pointer_is_aligned_to)] - /// #![feature(const_pointer_is_aligned)] - /// - /// const _: () = { - /// let ptr = 40 as *mut u8; - /// assert!(ptr.is_aligned_to(1)); - /// assert!(ptr.is_aligned_to(2)); - /// assert!(ptr.is_aligned_to(4)); - /// assert!(ptr.is_aligned_to(8)); - /// assert!(!ptr.is_aligned_to(16)); - /// }; - /// ``` - /// - /// [tracking issue]: https://github.com/rust-lang/rust/issues/104203 #[must_use] #[inline] #[unstable(feature = "pointer_is_aligned_to", issue = "96284")] - #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")] - pub const fn is_aligned_to(self, align: usize) -> bool { + pub fn is_aligned_to(self, align: usize) -> bool { if !align.is_power_of_two() { panic!("is_aligned_to: align is not a power-of-two"); } - #[inline] - fn runtime_impl(ptr: *mut (), align: usize) -> bool { - ptr.addr() & (align - 1) == 0 - } - - #[inline] - #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")] - const fn const_impl(ptr: *mut (), align: usize) -> bool { - // We can't use the address of `self` in a `const fn`, so we use `align_offset` instead. - ptr.align_offset(align) == 0 - } - - // The cast to `()` is used to - // 1. deal with fat pointers; and - // 2. ensure that `align_offset` (in `const_impl`) doesn't actually try to compute an offset. - const_eval_select((self.cast::<()>(), align), const_impl, runtime_impl) + self.addr() & (align - 1) == 0 } } @@ -2113,7 +1932,6 @@ impl *mut [T] { /// ``` #[inline(always)] #[unstable(feature = "slice_ptr_get", issue = "74265")] - #[rustc_const_unstable(feature = "slice_ptr_get", issue = "74265")] pub const fn as_mut_ptr(self) -> *mut T { self as *mut T } @@ -2269,7 +2087,6 @@ impl *mut [T; N] { /// ``` #[inline] #[unstable(feature = "array_ptr_get", issue = "119834")] - #[rustc_const_unstable(feature = "array_ptr_get", issue = "119834")] pub const fn as_mut_ptr(self) -> *mut T { self as *mut T } @@ -2290,7 +2107,6 @@ impl *mut [T; N] { /// ``` #[inline] #[unstable(feature = "array_ptr_get", issue = "119834")] - #[rustc_const_unstable(feature = "array_ptr_get", issue = "119834")] pub const fn as_mut_slice(self) -> *mut [T] { self } @@ -2362,120 +2178,143 @@ impl PartialOrd for *mut T { mod verify { use crate::kani; - /// 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() { - // 200 bytes are large enough to cover all pointee types used for testing - const BUF_SIZE: usize = 200; - let mut generator = kani::PointerGenerator::::new(); - let test_ptr: *mut $type = generator.any_in_bounds().ptr; - let count: usize = kani::any(); - unsafe { - test_ptr.add(count); - } - } - }; - ($type:ty, $proof_name:ident, sub) => { - #[kani::proof_for_contract(<*mut $type>::sub)] + /// This macro generates a single verification harness for the `offset`, `add`, or `sub` + /// pointer operations, supporting integer, composite, or unit types. + /// - `$ty`: The type of the slice's elements (e.g., `i32`, `u32`, tuples). + /// - `$fn_name`: The name of the function being checked (`add`, `sub`, or `offset`). + /// - `$proof_name`: The name assigned to the generated proof for the contract. + /// - `$count_ty:ty`: The type of the input variable passed to the method being invoked. + /// + /// Note: This macro is intended for internal use only and should be invoked exclusively + /// by the `generate_arithmetic_harnesses` macro. Its purpose is to reduce code duplication, + /// and it is not meant to be used directly elsewhere in the codebase. + macro_rules! generate_single_arithmetic_harness { + ($ty:ty, $proof_name:ident, $fn_name:ident, $count_ty:ty) => { + #[kani::proof_for_contract(<*mut $ty>::$fn_name)] pub fn $proof_name() { // 200 bytes are large enough to cover all pointee types used for testing const BUF_SIZE: usize = 200; let mut generator = kani::PointerGenerator::::new(); - let test_ptr: *mut $type = generator.any_in_bounds().ptr; - let count: usize = kani::any(); + let test_ptr: *mut $ty = generator.any_in_bounds().ptr; + let count: $count_ty = kani::any(); unsafe { - test_ptr.sub(count); + test_ptr.$fn_name(count); } } }; - ($type:ty, $proof_name:ident, offset) => { - #[kani::proof_for_contract(<*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::::new(); - let test_ptr: *mut $type = generator.any_in_bounds().ptr; - let count: isize = kani::any(); - unsafe { - test_ptr.offset(count); - } - } + } + + /// This macro generates verification harnesses for the `offset`, `add`, and `sub` + /// pointer operations, supporting integer, composite, and unit types. + /// - `$ty`: The pointee type (e.g., i32, u32, tuples). + /// - `$offset_fn_name`: The name for the `offset` proof for contract. + /// - `$add_fn_name`: The name for the `add` proof for contract. + /// - `$sub_fn_name`: The name for the `sub` proof for contract. + macro_rules! generate_arithmetic_harnesses { + ($ty:ty, $add_fn_name:ident, $sub_fn_name:ident, $offset_fn_name:ident) => { + generate_single_arithmetic_harness!($ty, $add_fn_name, add, usize); + generate_single_arithmetic_harness!($ty, $sub_fn_name, sub, usize); + generate_single_arithmetic_harness!($ty, $offset_fn_name, offset, isize); }; } - // <*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); - // Due to a bug of kani this test case is malfunctioning for now. + // Generate harnesses for unit type (add, sub, offset) + generate_arithmetic_harnesses!( + (), + check_mut_add_unit, + check_mut_sub_unit, + check_mut_offset_unit + ); + + // Generate harnesses for integer types (add, sub, offset) + generate_arithmetic_harnesses!(i8, check_mut_add_i8, check_mut_sub_i8, check_mut_offset_i8); + generate_arithmetic_harnesses!( + i16, + check_mut_add_i16, + check_mut_sub_i16, + check_mut_offset_i16 + ); + generate_arithmetic_harnesses!( + i32, + check_mut_add_i32, + check_mut_sub_i32, + check_mut_offset_i32 + ); + generate_arithmetic_harnesses!( + i64, + check_mut_add_i64, + check_mut_sub_i64, + check_mut_offset_i64 + ); + generate_arithmetic_harnesses!( + i128, + check_mut_add_i128, + check_mut_sub_i128, + check_mut_offset_i128 + ); + generate_arithmetic_harnesses!( + isize, + check_mut_add_isize, + check_mut_sub_isize, + check_mut_offset_isize + ); + // Due to a bug of kani the test `check_mut_add_u8` is malfunctioning for now. // Tracking issue: https://github.com/model-checking/kani/issues/3743 - // generate_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); -} + // generate_arithmetic_harnesses!(u8, check_mut_add_u8, check_mut_sub_u8, check_mut_offset_u8); + generate_arithmetic_harnesses!( + u16, + check_mut_add_u16, + check_mut_sub_u16, + check_mut_offset_u16 + ); + generate_arithmetic_harnesses!( + u32, + check_mut_add_u32, + check_mut_sub_u32, + check_mut_offset_u32 + ); + generate_arithmetic_harnesses!( + u64, + check_mut_add_u64, + check_mut_sub_u64, + check_mut_offset_u64 + ); + generate_arithmetic_harnesses!( + u128, + check_mut_add_u128, + check_mut_sub_u128, + check_mut_offset_u128 + ); + generate_arithmetic_harnesses!( + usize, + check_mut_add_usize, + check_mut_sub_usize, + check_mut_offset_usize + ); + + // Generte harnesses for composite types (add, sub, offset) + generate_arithmetic_harnesses!( + (i8, i8), + check_mut_add_tuple_1, + check_mut_sub_tuple_1, + check_mut_offset_tuple_1 + ); + generate_arithmetic_harnesses!( + (f64, bool), + check_mut_add_tuple_2, + check_mut_sub_tuple_2, + check_mut_offset_tuple_2 + ); + generate_arithmetic_harnesses!( + (i32, f64, bool), + check_mut_add_tuple_3, + check_mut_sub_tuple_3, + check_mut_offset_tuple_3 + ); + generate_arithmetic_harnesses!( + (i8, u16, i32, u64, isize), + check_mut_add_tuple_4, + check_mut_sub_tuple_4, + check_mut_offset_tuple_4 + ); +} \ No newline at end of file From f5817590151ad1acae03177742a204632ed835c6 Mon Sep 17 00:00:00 2001 From: szlee118 Date: Wed, 4 Dec 2024 22:48:12 -0800 Subject: [PATCH 26/30] Copied file from usage_proofs to verify/string_remove --- library/core/src/ptr/mut_ptr.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 7225169b93ddc..2bfa76a29ab05 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2317,4 +2317,4 @@ mod verify { check_mut_sub_tuple_4, check_mut_offset_tuple_4 ); -} \ No newline at end of file +} From 081474ef91e9819468f7aa146c8d00197496e390 Mon Sep 17 00:00:00 2001 From: szlee118 Date: Wed, 4 Dec 2024 23:45:25 -0800 Subject: [PATCH 27/30] Fix of any_where usage, hardcode constant --- library/alloc/src/string.rs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs index eff2a67693219..13f51263fe7d3 100644 --- a/library/alloc/src/string.rs +++ b/library/alloc/src/string.rs @@ -3226,12 +3226,13 @@ impl From for String { mod verify { use core::kani; use crate::string::String; - + #[kani::proof] #[kani::unwind(9)] fn check_remove() { - - let arr: [u8; 8] = kani::Arbitrary::any_array(); + // array size is chosen because it is small enough to be feasible to check exhaustively + const ARRAY_SIZE: usize = 8; + let arr: [u8; ARRAY_SIZE] = kani::Arbitrary::any_array(); for &byte in &arr { kani::assume(byte.is_ascii()); // Constrain to ASCII characters } @@ -3243,7 +3244,7 @@ mod verify { kani::assume(!s.is_empty()); // Generate a valid index within the bounds of the string - let idx: usize = kani::any(); + let idx: usize = kani::any_where(|&x| x < s.len()); kani::assume(idx < s.len()); // Call the `remove` function From 51e903df1b2983cadefcd3aa4be6ddd7f4bfc932 Mon Sep 17 00:00:00 2001 From: szlee118 Date: Thu, 5 Dec 2024 21:43:01 -0800 Subject: [PATCH 28/30] Add extra assertion and remove redundant assume --- library/alloc/src/string.rs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs index 13f51263fe7d3..790ff4e51f431 100644 --- a/library/alloc/src/string.rs +++ b/library/alloc/src/string.rs @@ -3245,7 +3245,9 @@ mod verify { // Generate a valid index within the bounds of the string let idx: usize = kani::any_where(|&x| x < s.len()); - kani::assume(idx < s.len()); + + // Store the character at the index `idx` before calling `remove` + let original_char = s.chars().nth(idx).expect("Index out of bounds"); // Call the `remove` function let removed_char = s.remove(idx); @@ -3255,6 +3257,9 @@ mod verify { // Verify the removed character is a valid ASCII character assert!(removed_char.is_ascii()); + + // Assert that the removed character matches the original character at `idx` + assert_eq!(removed_char, original_char); } } From 8ec384e40b596d3824250d28ce305ad84ecbe9ab Mon Sep 17 00:00:00 2001 From: szlee118 Date: Thu, 5 Dec 2024 21:47:12 -0800 Subject: [PATCH 29/30] Add description --- library/alloc/src/string.rs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs index 790ff4e51f431..8d23e778f5228 100644 --- a/library/alloc/src/string.rs +++ b/library/alloc/src/string.rs @@ -3228,7 +3228,15 @@ mod verify { use crate::string::String; #[kani::proof] - #[kani::unwind(9)] + #[kani::unwind(9)] // Unwind up to 9 times + /// This proof harness verifies the correctness and safety of the `String::remove` + /// + /// The harness checks: + /// 1. The string length decreases by one after the `remove` operation. + /// 2. The removed character is valid ASCII. + /// 3. The removed character matches the character at the specified index in the original string. + /// + /// This ensures the `remove` function behaves as expected for constrained inputs. fn check_remove() { // array size is chosen because it is small enough to be feasible to check exhaustively const ARRAY_SIZE: usize = 8; From ee063134b8718091db8030197a94cb4517a314e3 Mon Sep 17 00:00:00 2001 From: szlee118 Date: Thu, 5 Dec 2024 21:48:08 -0800 Subject: [PATCH 30/30] Remove redundant white line --- library/alloc/src/string.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs index 8d23e778f5228..c286da44ea750 100644 --- a/library/alloc/src/string.rs +++ b/library/alloc/src/string.rs @@ -67,7 +67,6 @@ use crate::str::{self, Chars, Utf8Error, from_utf8_unchecked_mut}; use crate::str::{FromStr, from_boxed_utf8_unchecked}; use crate::vec::Vec; - /// A UTF-8–encoded, growable string. /// /// `String` is the most common string type. It has ownership over the contents