From ec6d00fa1dab471414ee97fc059077402796e928 Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 Date: Fri, 8 Nov 2024 01:21:26 -0800 Subject: [PATCH 01/12] Added contracts for (mut) offset_from v2 --- library/core/src/ptr/mut_ptr.rs | 74 ++++++++++++++++++++++++++++++++- 1 file changed, 73 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 42975cc927b8e..ca665f09698f0 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -3,6 +3,9 @@ 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)] impl *mut T { /// Returns `true` if the pointer is null. @@ -798,11 +801,19 @@ impl *mut T { /// unsafe { /// let one = ptr2_other.offset_from(ptr2); // Undefined Behavior! ⚠️ /// } - /// ``` + /// ```S #[stable(feature = "ptr_offset_from", since = "1.47.0")] #[rustc_const_stable(feature = "const_ptr_offset_from", since = "1.65.0")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires( + + (mem::size_of::() != 0) && + (self as isize).checked_sub(origin as isize).is_some() && + (self as isize - origin as isize) % (mem::size_of::() as isize) == 0 && + kani::mem::same_allocation(self, origin) + )] + #[ensures(|result| *result == (self as isize - origin as isize) / (mem::size_of::() as isize))] pub const unsafe fn offset_from(self, origin: *const T) -> isize where T: Sized, @@ -2197,3 +2208,64 @@ impl PartialOrd for *mut T { *self >= *other } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use crate::kani; + use kani::{PointerGenerator}; + + #[kani::proof_for_contract(<*mut ()>::offset_from)] + pub fn check_mut_offset_from_unit() { + let mut val: () = (); + let src_ptr: *mut () = &mut val; + let dest_ptr: *mut () = &mut val; + unsafe { + dest_ptr.offset_from(src_ptr); + } + } + + macro_rules! generate_offset_from_harness { + ($type: ty, $proof_name: ident) => { + #[kani::proof_for_contract(<*mut $type>::offset_from)] + pub fn $proof_name() { + let mut val: $type = kani::any::<$type>(); + let ptr: *mut $type = &mut val; + + let offset: usize = kani::any_where(|x| *x <= 1); + let src_ptr: *mut $type = unsafe { ptr.add(offset) }; + let offset: usize = kani::any_where(|x| *x <= 1); + let dest_ptr: *mut $type = unsafe { ptr.add(offset) }; + + unsafe { + dest_ptr.offset_from(src_ptr); + } + + + } + }; + } + + generate_offset_from_harness!(u8, check_mut_offset_from_u8); + generate_offset_from_harness!(u16, check_mut_offset_from_u16); + generate_offset_from_harness!(u32, check_mut_offset_from_u32); + generate_offset_from_harness!(u64, check_mut_offset_from_u64); + generate_offset_from_harness!(u128, check_mut_offset_from_u128); + generate_offset_from_harness!(usize, check_mut_offset_from_usize); + + generate_offset_from_harness!(i8, check_mut_offset_from_i8); + generate_offset_from_harness!(i16, check_mut_offset_from_i16); + generate_offset_from_harness!(i32, check_mut_offset_from_i32); + generate_offset_from_harness!(i64, check_mut_offset_from_i64); + generate_offset_from_harness!(i128, check_mut_offset_from_i128); + generate_offset_from_harness!(isize, check_mut_offset_from_isize); + + generate_offset_from_harness!((i8, i8), check_mut_offset_from_tuple_1); + generate_offset_from_harness!((f64, bool), check_mut_offset_from_tuple_2); + generate_offset_from_harness!((u32, i16, f32), check_mut_offset_from_tuple_3); + generate_offset_from_harness!( + ((), bool, u8, u16, i32, f64, i128, usize), + check_mut_offset_from_tuple_4 + ); + +} From a16423e3ced6be913af269380a077045e778c599 Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 Date: Fri, 8 Nov 2024 11:40:19 -0800 Subject: [PATCH 02/12] Changes made to macro --- library/core/src/ptr/mut_ptr.rs | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index ca665f09698f0..28b6a9520b085 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2214,6 +2214,7 @@ impl PartialOrd for *mut T { mod verify { use crate::kani; use kani::{PointerGenerator}; + use core::mem; #[kani::proof_for_contract(<*mut ()>::offset_from)] pub fn check_mut_offset_from_unit() { @@ -2232,13 +2233,19 @@ mod verify { let mut val: $type = kani::any::<$type>(); let ptr: *mut $type = &mut val; - let offset: usize = kani::any_where(|x| *x <= 1); - let src_ptr: *mut $type = unsafe { ptr.add(offset) }; - let offset: usize = kani::any_where(|x| *x <= 1); - let dest_ptr: *mut $type = unsafe { ptr.add(offset) }; + let offset: usize = kani::any_where(|x| *x <= mem::size_of::<$type>()); + let src_ptr: *mut $type = unsafe { ptr.byte_add(offset) }; + let offset: usize = kani::any_where(|x| *x <= mem::size_of::<$type>()); + let dest_ptr: *mut $type = if kani::any() { + let offset: usize = kani::any_where(|x| *x <= mem::size_of::<$type>()); + unsafe { ptr.byte_add(offset) } + } else { + let mut val2: $type = kani::any::<$type>(); + &mut val2 + }; unsafe { - dest_ptr.offset_from(src_ptr); + src_ptr.offset_from(dest_ptr); } From ff72e0b9e3d27d4dc700008753c2c81aca0fac78 Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 Date: Fri, 15 Nov 2024 01:00:58 -0800 Subject: [PATCH 03/12] Updated offset_from (mut) --- library/core/src/ptr/mut_ptr.rs | 94 +++++++++++++++++++++------------ 1 file changed, 59 insertions(+), 35 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 28b6a9520b085..266faab5c5ed0 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -804,14 +804,15 @@ impl *mut T { /// ```S #[stable(feature = "ptr_offset_from", since = "1.47.0")] #[rustc_const_stable(feature = "const_ptr_offset_from", since = "1.65.0")] - #[inline(always)] + #[inline] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires( - - (mem::size_of::() != 0) && + // Ensuring that subtracting 'origin' from 'self' doesnt result in an overflow (self as isize).checked_sub(origin as isize).is_some() && + // Ensuring that sthe distance between 'self' & 'origin' is aligned to T (self as isize - origin as isize) % (mem::size_of::() as isize) == 0 && - kani::mem::same_allocation(self, origin) + // Ensuring that both pointers point to the same address or are in the same allocation + (self as isize == origin as isize || kani::mem::same_allocation(self, origin)) )] #[ensures(|result| *result == (self as isize - origin as isize) / (mem::size_of::() as isize))] pub const unsafe fn offset_from(self, origin: *const T) -> isize @@ -2216,7 +2217,9 @@ mod verify { use kani::{PointerGenerator}; use core::mem; + // The proof for a unit type panics as offset_from needs the pointee size > 0 #[kani::proof_for_contract(<*mut ()>::offset_from)] + #[kani::should_panic] pub fn check_mut_offset_from_unit() { let mut val: () = (); let src_ptr: *mut () = &mut val; @@ -2226,53 +2229,74 @@ mod verify { } } + // Array size is bound for kani::any_array + const ARRAY_LEN: usize = 40; + macro_rules! generate_offset_from_harness { - ($type: ty, $proof_name: ident) => { + ($type: ty, $proof_name1: ident, $proof_name2: ident) => { #[kani::proof_for_contract(<*mut $type>::offset_from)] - pub fn $proof_name() { - let mut val: $type = kani::any::<$type>(); - let ptr: *mut $type = &mut val; - - let offset: usize = kani::any_where(|x| *x <= mem::size_of::<$type>()); - let src_ptr: *mut $type = unsafe { ptr.byte_add(offset) }; - let offset: usize = kani::any_where(|x| *x <= mem::size_of::<$type>()); - let dest_ptr: *mut $type = if kani::any() { - let offset: usize = kani::any_where(|x| *x <= mem::size_of::<$type>()); - unsafe { ptr.byte_add(offset) } + // Below function is for a single element + pub fn $proof_name1() { + const gen_size: usize = mem::size_of::<$type>(); + let mut generator1 = PointerGenerator::::new(); + let mut generator2 = PointerGenerator::::new(); + let ptr1: *mut $type = generator1.any_in_bounds().ptr; + let ptr2: *mut $type = if kani::any() { + generator1.any_alloc_status().ptr } else { - let mut val2: $type = kani::any::<$type>(); - &mut val2 - }; + generator2.any_alloc_status().ptr + }; + + unsafe { + ptr1.offset_from(ptr2); + } + + } + + // Below function is for large arrays + pub fn $proof_name2() { + const gen_size: usize = mem::size_of::<$type>(); + let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let ptr1: *mut $type = generator1.any_in_bounds().ptr; + let ptr2: *mut $type = if kani::any() { + generator1.any_alloc_status().ptr + } else { + generator2.any_alloc_status().ptr + }; + unsafe { - src_ptr.offset_from(dest_ptr); + ptr1.offset_from(ptr2); } } + }; } - generate_offset_from_harness!(u8, check_mut_offset_from_u8); - generate_offset_from_harness!(u16, check_mut_offset_from_u16); - generate_offset_from_harness!(u32, check_mut_offset_from_u32); - generate_offset_from_harness!(u64, check_mut_offset_from_u64); - generate_offset_from_harness!(u128, check_mut_offset_from_u128); - generate_offset_from_harness!(usize, check_mut_offset_from_usize); + generate_offset_from_harness!(u8, check_mut_offset_from_u8, check_mut_offset_from_u8_array); + generate_offset_from_harness!(u16, check_mut_offset_from_u16, check_mut_offset_from_u16_array); + generate_offset_from_harness!(u32, check_mut_offset_from_u32, check_mut_offset_from_u32_array); + generate_offset_from_harness!(u64, check_mut_offset_from_u64, check_mut_offset_from_u64_array); + generate_offset_from_harness!(u128, check_mut_offset_from_u128, check_mut_offset_from_u128_array); + generate_offset_from_harness!(usize, check_mut_offset_from_usize, check_mut_offset_from_usize_array); - generate_offset_from_harness!(i8, check_mut_offset_from_i8); - generate_offset_from_harness!(i16, check_mut_offset_from_i16); - generate_offset_from_harness!(i32, check_mut_offset_from_i32); - generate_offset_from_harness!(i64, check_mut_offset_from_i64); - generate_offset_from_harness!(i128, check_mut_offset_from_i128); - generate_offset_from_harness!(isize, check_mut_offset_from_isize); + generate_offset_from_harness!(i8, check_mut_offset_from_i8, check_mut_offset_from_i8_array); + generate_offset_from_harness!(i16, check_mut_offset_from_i16, check_mut_offset_from_i16_array); + generate_offset_from_harness!(i32, check_mut_offset_from_i32, check_mut_offset_from_i32_array); + generate_offset_from_harness!(i64, check_mut_offset_from_i64, check_mut_offset_from_i64_array); + generate_offset_from_harness!(i128, check_mut_offset_from_i128, check_mut_offset_from_i128_array); + generate_offset_from_harness!(isize, check_mut_offset_from_isize, check_mut_offset_from_isize_array); - generate_offset_from_harness!((i8, i8), check_mut_offset_from_tuple_1); - generate_offset_from_harness!((f64, bool), check_mut_offset_from_tuple_2); - generate_offset_from_harness!((u32, i16, f32), check_mut_offset_from_tuple_3); + generate_offset_from_harness!((i8, i8), check_mut_offset_from_tuple_1, check_mut_offset_from_tuple_1_array); + generate_offset_from_harness!((f64, bool), check_mut_offset_from_tuple_2, check_mut_offset_from_tuple_2_array); + generate_offset_from_harness!((u32, i16, f32), check_mut_offset_from_tuple_3, check_mut_offset_from_tuple_3_array); generate_offset_from_harness!( ((), bool, u8, u16, i32, f64, i128, usize), - check_mut_offset_from_tuple_4 + check_mut_offset_from_tuple_4, + check_mut_offset_from_tuple_4_array ); } From ec50021fb9001c2f99b4b2b1b3163393ecf990e2 Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 <60180388+MayureshJoshi25@users.noreply.github.com> Date: Sat, 23 Nov 2024 19:42:11 -0800 Subject: [PATCH 04/12] Update library/core/src/ptr/mut_ptr.rs Minor change Co-authored-by: Carolyn Zech --- 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 32ed7d73115f4..3c375cb362e31 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -4,8 +4,8 @@ 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. From f7c7553b8bdf7a7991a2ddfb68bf2b85b725555c Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 <60180388+MayureshJoshi25@users.noreply.github.com> Date: Sat, 23 Nov 2024 19:42:29 -0800 Subject: [PATCH 05/12] Update library/core/src/ptr/mut_ptr.rs Minor change 2 Co-authored-by: Carolyn Zech --- 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 3c375cb362e31..de4bbd62cdc6e 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -832,7 +832,7 @@ impl *mut T { /// ```S #[stable(feature = "ptr_offset_from", since = "1.47.0")] #[rustc_const_stable(feature = "const_ptr_offset_from", since = "1.65.0")] - #[inline] + #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires( // Ensuring that subtracting 'origin' from 'self' doesnt result in an overflow From f2aec122251f710531ac5aea00e61ce5e471c484 Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 <60180388+MayureshJoshi25@users.noreply.github.com> Date: Sat, 23 Nov 2024 19:42:43 -0800 Subject: [PATCH 06/12] Update library/core/src/ptr/mut_ptr.rs Minor change 3 Co-authored-by: Carolyn Zech --- 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 de4bbd62cdc6e..6d63f8d28854a 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2319,7 +2319,7 @@ impl PartialOrd for *mut T { #[unstable(feature = "kani", issue = "none")] mod verify { use crate::kani; - use kani::{PointerGenerator}; + use kani::PointerGenerator; use core::mem; // The proof for a unit type panics as offset_from needs the pointee size > 0 From 56e30eafa4b1008aec3abfc2df70ead5ca53544f Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 <60180388+MayureshJoshi25@users.noreply.github.com> Date: Sat, 23 Nov 2024 19:43:09 -0800 Subject: [PATCH 07/12] Update library/core/src/ptr/mut_ptr.rs Co-authored-by: Carolyn Zech --- library/core/src/ptr/mut_ptr.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 6d63f8d28854a..0fd022492a6f5 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2355,8 +2355,6 @@ mod verify { unsafe { ptr1.offset_from(ptr2); } - - } // Below function is for large arrays From cf06518d730f7ef7310ad0bc397d4054802fa0a5 Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 <60180388+MayureshJoshi25@users.noreply.github.com> Date: Sat, 23 Nov 2024 19:43:40 -0800 Subject: [PATCH 08/12] Update library/core/src/ptr/mut_ptr.rs Co-authored-by: Carolyn Zech --- library/core/src/ptr/mut_ptr.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 0fd022492a6f5..72680cbb2cbb7 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2372,8 +2372,6 @@ mod verify { unsafe { ptr1.offset_from(ptr2); } - - } }; From c9428c66acb56436ac54f013b4c40c343e6a5859 Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 <60180388+MayureshJoshi25@users.noreply.github.com> Date: Wed, 27 Nov 2024 17:52:20 -0800 Subject: [PATCH 09/12] Update library/core/src/ptr/mut_ptr.rs minor comment change Co-authored-by: Felipe R. Monteiro --- 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 72680cbb2cbb7..44d97ba70b44c 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -837,7 +837,7 @@ impl *mut T { #[requires( // Ensuring that subtracting 'origin' from 'self' doesnt result in an overflow (self as isize).checked_sub(origin as isize).is_some() && - // Ensuring that sthe distance between 'self' & 'origin' is aligned to T + // Ensuring that the distance between 'self' & 'origin' is aligned to `T` (self as isize - origin as isize) % (mem::size_of::() as isize) == 0 && // Ensuring that both pointers point to the same address or are in the same allocation (self as isize == origin as isize || kani::mem::same_allocation(self, origin)) From e115ec007cc8481132cb9c16b25781fd4f9389bf Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 Date: Sun, 1 Dec 2024 19:02:10 -0800 Subject: [PATCH 10/12] Latest changes --- library/core/src/ptr/mut_ptr.rs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 44d97ba70b44c..74890b7c37553 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -829,7 +829,9 @@ impl *mut T { /// unsafe { /// let one = ptr2_other.offset_from(ptr2); // Undefined Behavior! ⚠️ /// } - /// ```S + /// + /// + /// ``` #[stable(feature = "ptr_offset_from", since = "1.47.0")] #[rustc_const_stable(feature = "const_ptr_offset_from", since = "1.65.0")] #[inline(always)] @@ -2336,6 +2338,9 @@ mod verify { // Array size is bound for kani::any_array const ARRAY_LEN: usize = 40; + // The array's length is set to a random value, which defines its size. + // This is necessary because implementing a dynamic array is not possible. + // Size can be changed. macro_rules! generate_offset_from_harness { ($type: ty, $proof_name1: ident, $proof_name2: ident) => { From 55496a17be7dc2c66050b3e257413a6c6cab1fac Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 <60180388+MayureshJoshi25@users.noreply.github.com> Date: Mon, 2 Dec 2024 16:05:54 -0800 Subject: [PATCH 11/12] Update library/core/src/ptr/mut_ptr.rs Co-authored-by: Felipe R. Monteiro --- 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 74890b7c37553..67115d167d25e 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -837,7 +837,7 @@ impl *mut T { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires( - // Ensuring that subtracting 'origin' from 'self' doesnt result in an overflow + // Ensuring that subtracting 'origin' from 'self' doesn't result in an overflow (self as isize).checked_sub(origin as isize).is_some() && // Ensuring that the distance between 'self' & 'origin' is aligned to `T` (self as isize - origin as isize) % (mem::size_of::() as isize) == 0 && From 33c1882440483a937441ab4c361d5aad9238cbfd Mon Sep 17 00:00:00 2001 From: MayureshJoshi25 <60180388+MayureshJoshi25@users.noreply.github.com> Date: Mon, 2 Dec 2024 16:06:05 -0800 Subject: [PATCH 12/12] Update library/core/src/ptr/mut_ptr.rs Co-authored-by: Felipe R. Monteiro --- 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 67115d167d25e..0362f67a4aab9 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -839,7 +839,7 @@ impl *mut T { #[requires( // Ensuring that subtracting 'origin' from 'self' doesn't result in an overflow (self as isize).checked_sub(origin as isize).is_some() && - // Ensuring that the distance between 'self' & 'origin' is aligned to `T` + // Ensuring that the distance between 'self' and 'origin' is aligned to `T` (self as isize - origin as isize) % (mem::size_of::() as isize) == 0 && // Ensuring that both pointers point to the same address or are in the same allocation (self as isize == origin as isize || kani::mem::same_allocation(self, origin))