From d07cf9cd577dcbe2904aba917a4d95fd9146af02 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Thu, 24 Oct 2024 00:21:57 +0000 Subject: [PATCH 01/11] Writes contracts for offset_from and adds a harness for u32 --- library/core/src/ptr/const_ptr.rs | 42 +++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 3b635e2a4aa9e..d0ede9cf306d3 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -3,6 +3,10 @@ use crate::cmp::Ordering::{Equal, Greater, Less}; use crate::intrinsics::const_eval_select; use crate::mem::SizedTypeProperties; use crate::slice::{self, SliceIndex}; +use safety::{ensures, requires}; + +#[cfg(kani)] +use crate::kani; impl *const T { /// Returns `true` if the pointer is null. @@ -621,6 +625,14 @@ impl *const T { #[rustc_const_stable(feature = "const_ptr_offset_from", since = "1.65.0")] #[inline] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(kani::mem::same_allocation(self, origin))] + #[requires( + (self as usize).checked_sub(origin as usize).is_some() && + (self as usize - origin as usize) % (mem::size_of::() as usize) == 0 + )] + #[ensures(|result| + *result == ((self as usize - origin as usize) / (mem::size_of::() as usize)) as isize + )] pub const unsafe fn offset_from(self, origin: *const T) -> isize where T: Sized, @@ -1774,3 +1786,33 @@ impl PartialOrd for *const T { *self >= *other } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use crate::kani; + use kani::{PointerGenerator}; + + #[kani::proof_for_contract(<*const u32>::offset_from)] + pub fn check_const_offset_from_u32() { + let mut val: u32 = kani::any::(); + let ptr: *const u32 = &mut val; + let offset = kani::any_where(|b: &usize| *b <= size_of::()); + let src_ptr: *const u32 = unsafe { ptr.add(offset) }; + let offset = kani::any_where(|b: &usize| *b <= size_of::()); + let dest_ptr: *const u32 = unsafe { ptr.add(offset) }; + unsafe { + dest_ptr.offset_from(src_ptr); + } + } + + #[kani::proof_for_contract(<*const u32>::offset_from)] + pub fn check_const_offset_from_u32_pg() { + let mut generator = PointerGenerator::<4>::new(); + let origin_ptr: *const u32 = generator.any_alloc_status::().ptr; + let dest_ptr: *const u32 = generator.any_alloc_status::().ptr; + unsafe { + origin_ptr.offset_from(dest_ptr); + } + } +} From c778d36add033f235bb38e9cdf4dff8884c3f371 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Mon, 28 Oct 2024 19:25:32 -0700 Subject: [PATCH 02/11] Removes PointerGenerator proof and corrects the contract for offset_from --- library/core/src/ptr/const_ptr.rs | 17 +++-------------- 1 file changed, 3 insertions(+), 14 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index d0ede9cf306d3..b8e6559eb7672 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -627,11 +627,11 @@ impl *const T { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires(kani::mem::same_allocation(self, origin))] #[requires( - (self as usize).checked_sub(origin as usize).is_some() && - (self as usize - origin as usize) % (mem::size_of::() as usize) == 0 + (self as isize).checked_sub(origin as isize).is_some() && + (self as isize - origin as isize) % (mem::size_of::() as isize) == 0 )] #[ensures(|result| - *result == ((self as usize - origin as usize) / (mem::size_of::() as usize)) as isize + *result == ((self as isize - origin as isize) / (mem::size_of::() as isize)) )] pub const unsafe fn offset_from(self, origin: *const T) -> isize where @@ -1791,7 +1791,6 @@ impl PartialOrd for *const T { #[unstable(feature = "kani", issue = "none")] mod verify { use crate::kani; - use kani::{PointerGenerator}; #[kani::proof_for_contract(<*const u32>::offset_from)] pub fn check_const_offset_from_u32() { @@ -1805,14 +1804,4 @@ mod verify { dest_ptr.offset_from(src_ptr); } } - - #[kani::proof_for_contract(<*const u32>::offset_from)] - pub fn check_const_offset_from_u32_pg() { - let mut generator = PointerGenerator::<4>::new(); - let origin_ptr: *const u32 = generator.any_alloc_status::().ptr; - let dest_ptr: *const u32 = generator.any_alloc_status::().ptr; - unsafe { - origin_ptr.offset_from(dest_ptr); - } - } } From 0434a3ed3187066c644b1a681784195432eb16d1 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Thu, 31 Oct 2024 20:37:58 -0700 Subject: [PATCH 03/11] Corrects fonctracts and adds amacro for offset_from proofs --- library/core/src/ptr/const_ptr.rs | 64 ++++++++++++++++++++++++------- 1 file changed, 51 insertions(+), 13 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index b8e6559eb7672..b3ad2c6137194 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -625,14 +625,13 @@ impl *const T { #[rustc_const_stable(feature = "const_ptr_offset_from", since = "1.65.0")] #[inline] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - #[requires(kani::mem::same_allocation(self, origin))] #[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 - )] - #[ensures(|result| - *result == ((self as isize - origin as isize) / (mem::size_of::() as isize)) + (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, @@ -1792,16 +1791,55 @@ impl PartialOrd for *const T { mod verify { use crate::kani; - #[kani::proof_for_contract(<*const u32>::offset_from)] - pub fn check_const_offset_from_u32() { - let mut val: u32 = kani::any::(); - let ptr: *const u32 = &mut val; - let offset = kani::any_where(|b: &usize| *b <= size_of::()); - let src_ptr: *const u32 = unsafe { ptr.add(offset) }; - let offset = kani::any_where(|b: &usize| *b <= size_of::()); - let dest_ptr: *const u32 = unsafe { ptr.add(offset) }; + #[kani::proof_for_contract(<*const ()>::offset_from)] + pub fn check_const_offset_from_unit() { + let val: () = (); + let src_ptr: *const () = &val; + let dest_ptr: *const () = &val; unsafe { dest_ptr.offset_from(src_ptr); } } + + macro_rules! generate_offset_from_harness { + ($type: ty, $proof_name: ident) => { + #[kani::proof_for_contract(<*const $type>::offset_from)] + pub fn $proof_name() { + let val: $type = kani::any::<$type>(); + let ptr: *const $type = &val; + + let offset: usize = kani::any_where(|x| *x <= 1); + let src_ptr: *const $type = unsafe { ptr.add(offset) }; + + let offset: usize = kani::any_where(|x| *x <= 1); + let dest_ptr: *const $type = unsafe { ptr.add(offset) }; + + unsafe { + dest_ptr.offset_from(src_ptr); + } + } + }; + } + + generate_offset_from_harness!(u8, check_const_offset_from_u8); + generate_offset_from_harness!(u16, check_const_offset_from_u16); + generate_offset_from_harness!(u32, check_const_offset_from_u32); + generate_offset_from_harness!(u64, check_const_offset_from_u64); + generate_offset_from_harness!(u128, check_const_offset_from_u128); + generate_offset_from_harness!(usize, check_const_offset_from_usize); + + generate_offset_from_harness!(i8, check_const_offset_from_i8); + generate_offset_from_harness!(i16, check_const_offset_from_i16); + generate_offset_from_harness!(i32, check_const_offset_from_i32); + generate_offset_from_harness!(i64, check_const_offset_from_i64); + generate_offset_from_harness!(i128, check_const_offset_from_i128); + generate_offset_from_harness!(isize, check_const_offset_from_isize); + + generate_offset_from_harness!((i8, i8), check_const_offset_from_tuple_1); + generate_offset_from_harness!((f64, bool), check_const_offset_from_tuple_2); + generate_offset_from_harness!((u32, i16, f32), check_const_offset_from_tuple_3); + generate_offset_from_harness!( + ((), bool, u8, u16, i32, f64, i128, usize), + check_const_offset_from_tuple_4 + ); } From ba808485c67f40a2503b2fbb635fa05876279bc8 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Fri, 1 Nov 2024 06:08:31 -0700 Subject: [PATCH 04/11] Improves the harness to have ptrs from same and diff allocation objects --- library/core/src/ptr/const_ptr.rs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index b3ad2c6137194..e4a301fb98def 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1811,8 +1811,13 @@ mod verify { let offset: usize = kani::any_where(|x| *x <= 1); let src_ptr: *const $type = unsafe { ptr.add(offset) }; - let offset: usize = kani::any_where(|x| *x <= 1); - let dest_ptr: *const $type = unsafe { ptr.add(offset) }; + let dest_ptr: *const $type = if kani::any() { + let offset: usize = kani::any_where(|x| *x <= 1); + unsafe { ptr.add(offset) } + } else { + let val2: $type = kani::any::<$type>(); + &val2 + }; unsafe { dest_ptr.offset_from(src_ptr); From df35ec7230d6e58470d697a9dd92151fbea3b15a Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Tue, 5 Nov 2024 23:46:48 -0800 Subject: [PATCH 05/11] Moves the ptr within the object using byte_Add intead of add --- library/core/src/ptr/const_ptr.rs | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index e4a301fb98def..04df44ac15917 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -626,7 +626,7 @@ impl *const T { #[inline] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires( - (mem::size_of::() != 0) && + (mem::size_of::() != 0) && // offset_from requires pointee size to be greater than 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) @@ -1790,6 +1790,7 @@ impl PartialOrd for *const T { #[unstable(feature = "kani", issue = "none")] mod verify { use crate::kani; + use core::mem; #[kani::proof_for_contract(<*const ()>::offset_from)] pub fn check_const_offset_from_unit() { @@ -1808,19 +1809,21 @@ mod verify { let val: $type = kani::any::<$type>(); let ptr: *const $type = &val; - let offset: usize = kani::any_where(|x| *x <= 1); - let src_ptr: *const $type = unsafe { ptr.add(offset) }; - + // offset the src pointer within the allocation bounds non-deterministically + let offset: usize = kani::any_where(|x| *x <= mem::size_of::<$type>()); + let src_ptr: *const $type = unsafe { ptr.byte_add(offset) }; + + // generate the dest ptr non-deterministically with same or different provenance. let dest_ptr: *const $type = if kani::any() { - let offset: usize = kani::any_where(|x| *x <= 1); - unsafe { ptr.add(offset) } + let offset: usize = kani::any_where(|x| *x <= mem::size_of::<$type>()); + unsafe { ptr.byte_add(offset) } } else { let val2: $type = kani::any::<$type>(); &val2 }; unsafe { - dest_ptr.offset_from(src_ptr); + src_ptr.offset_from(dest_ptr); } } }; From 93fded6b6b9f9105d710b13191a21c40f0fce705 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Wed, 6 Nov 2024 22:32:24 -0800 Subject: [PATCH 06/11] Write harnesses to verify slices --- library/core/src/ptr/const_ptr.rs | 64 +++++++++++++++++++++++++++++++ 1 file changed, 64 insertions(+) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 3b635e2a4aa9e..d51afdade9d06 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -3,6 +3,10 @@ use crate::cmp::Ordering::{Equal, Greater, Less}; use crate::intrinsics::const_eval_select; use crate::mem::SizedTypeProperties; use crate::slice::{self, SliceIndex}; +use safety::{ensures, requires}; + +#[cfg(kani)] +use crate::kani; impl *const T { /// Returns `true` if the pointer is null. @@ -621,6 +625,13 @@ impl *const T { #[rustc_const_stable(feature = "const_ptr_offset_from", since = "1.65.0")] #[inline] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires( + (mem::size_of::() != 0) && // offset_from requires pointee size to be greater than 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, @@ -1774,3 +1785,56 @@ impl PartialOrd for *const T { *self >= *other } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use crate::kani; + use core::mem; + + const ARRAY_SIZE: usize = 5; + + macro_rules! generate_offset_from_harnesses_for_slices { + + ($type:ty, $proof_name:ident) => { + #[kani::proof_for_contract(<*const $type>::offset_from)] + fn $proof_name() { + let arr1: [$type; ARRAY_SIZE] = kani::Arbitrary::any_array(); + let arr2: [$type; ARRAY_SIZE] = kani::Arbitrary::any_array(); + let len_arr_bytes: usize = mem::size_of::<$type>() * ARRAY_SIZE; + + let ptr_arr1: *const $type = arr1.as_ptr(); + let mut offset: usize = kani::any_where(|x| *x <= len_arr_bytes ); + let src_ptr: *const $type = ptr_arr1.wrapping_byte_add(offset); + + offset = kani::any_where(|x| *x <= len_arr_bytes); + + let dest_ptr: *const $type = if kani::any() { + ptr_arr1.wrapping_byte_add(offset) + } else { + arr2.as_ptr().wrapping_byte_add(offset) as *const $type + }; + + unsafe { + src_ptr.offset_from(dest_ptr); + } + } + } + + } + + generate_offset_from_harnesses_for_slices!(i8, check_offset_from_slice_i8); + generate_offset_from_harnesses_for_slices!(i16, check_offset_from_slice_i16); + generate_offset_from_harnesses_for_slices!(i32, check_offset_from_slice_i32); + generate_offset_from_harnesses_for_slices!(i64, check_offset_from_slice_i64); + generate_offset_from_harnesses_for_slices!(i128, check_offset_from_slice_i128); + generate_offset_from_harnesses_for_slices!(isize, check_offset_from_slice_isize); + generate_offset_from_harnesses_for_slices!(u8, check_offset_from_slice_u8); + generate_offset_from_harnesses_for_slices!(u16, check_offset_from_slice_u16); + generate_offset_from_harnesses_for_slices!(u32, check_offset_from_slice_u32); + generate_offset_from_harnesses_for_slices!(u64, check_offset_from_slice_u64); + generate_offset_from_harnesses_for_slices!(u128, check_offset_from_slice_u128); + generate_offset_from_harnesses_for_slices!(usize, check_offset_from_slice_usize); + generate_offset_from_harnesses_for_slices!(bool, check_offset_from_slice_bool); + generate_offset_from_harnesses_for_slices!((), check_offset_from_slice_unit); +} From 401dd87520bd6ceee7f039afe40d616909532cf2 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Thu, 7 Nov 2024 21:38:52 -0800 Subject: [PATCH 07/11] Add comments --- library/core/src/ptr/const_ptr.rs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index d51afdade9d06..d30b2b461ae31 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1792,7 +1792,8 @@ mod verify { use crate::kani; use core::mem; - const ARRAY_SIZE: usize = 5; + // Array size bound for kani::any_array + const ARRAY_SIZE: usize = 40; macro_rules! generate_offset_from_harnesses_for_slices { @@ -1804,11 +1805,14 @@ mod verify { let len_arr_bytes: usize = mem::size_of::<$type>() * ARRAY_SIZE; let ptr_arr1: *const $type = arr1.as_ptr(); + + // Non-deterministically offset the pointer within the allocated object let mut offset: usize = kani::any_where(|x| *x <= len_arr_bytes ); let src_ptr: *const $type = ptr_arr1.wrapping_byte_add(offset); offset = kani::any_where(|x| *x <= len_arr_bytes); - + + // Non-deterministically generate pointer of same or different provenance let dest_ptr: *const $type = if kani::any() { ptr_arr1.wrapping_byte_add(offset) } else { From 9d6c0fb19a02366f51a9c607dc99cd83a7aaab9b Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Fri, 8 Nov 2024 00:16:40 -0800 Subject: [PATCH 08/11] Adds slices harnesses --- library/core/src/ptr/const_ptr.rs | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 28bb7a525b0a5..00f45e9ad02c9 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -675,7 +675,7 @@ impl *const T { (mem::size_of::() != 0) && // offset_from requires pointee size to be greater than 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) + (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 @@ -1931,21 +1931,21 @@ mod verify { ($type: ty, $proof_name: ident) => { #[kani::proof_for_contract(<*const $type>::offset_from)] pub fn $proof_name() { - let val: $type = kani::any::<$type>(); - let ptr: *const $type = &val; + let val1: $type = kani::any::<$type>(); + let val2: $type = kani::any::<$type>(); + let ptr1: *const $type = &val1; + let ptr2: *const $type = &val2; // offset the src pointer within the allocation bounds non-deterministically - let offset: usize = kani::any_where(|x| *x <= mem::size_of::<$type>()); - let src_ptr: *const $type = unsafe { ptr.byte_add(offset) }; - - // generate the dest ptr non-deterministically with same or different provenance. + let mut offset: usize = kani::any_where(|x| *x <= mem::size_of::<$type>()); + let src_ptr: *const $type = ptr1.wrapping_byte_add(offset); + + offset = kani::any_where(|x| *x <= mem::size_of::<$type>()); + // generate the dest ptr non-deterministically with same or different provenance let dest_ptr: *const $type = if kani::any() { - let offset: usize = kani::any_where(|x| *x <= mem::size_of::<$type>()); - unsafe { ptr.byte_add(offset) } + ptr1.wrapping_byte_add(offset) } else { - let val2: $type = kani::any::<$type>(); - &val2 - + ptr2.wrapping_byte_add(offset) }; unsafe { From d7294eaa26d5231ae1e07deb1258fac691417155 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Fri, 8 Nov 2024 11:31:20 -0800 Subject: [PATCH 09/11] Uses PointerGenerator for integer and composite, write harnesses for slice types --- library/core/src/ptr/const_ptr.rs | 72 +++++++++++++++---------------- 1 file changed, 34 insertions(+), 38 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 00f45e9ad02c9..3cd465140bc39 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -672,7 +672,6 @@ impl *const T { #[inline] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires( - (mem::size_of::() != 0) && // offset_from requires pointee size to be greater than 0 (self as isize).checked_sub(origin as isize).is_some() && (self as isize - origin as isize) % (mem::size_of::() as isize) == 0 && (self as isize == origin as isize || kani::mem::same_allocation(self, origin)) @@ -1915,9 +1914,11 @@ impl PartialOrd for *const T { #[unstable(feature = "kani", issue = "none")] mod verify { use crate::kani; + use kani::PointerGenerator; use core::mem; #[kani::proof_for_contract(<*const ()>::offset_from)] + #[kani::should_panic] pub fn check_const_offset_from_unit() { let val: () = (); let src_ptr: *const () = &val; @@ -1931,25 +1932,18 @@ mod verify { ($type: ty, $proof_name: ident) => { #[kani::proof_for_contract(<*const $type>::offset_from)] pub fn $proof_name() { - let val1: $type = kani::any::<$type>(); - let val2: $type = kani::any::<$type>(); - let ptr1: *const $type = &val1; - let ptr2: *const $type = &val2; - - // offset the src pointer within the allocation bounds non-deterministically - let mut offset: usize = kani::any_where(|x| *x <= mem::size_of::<$type>()); - let src_ptr: *const $type = ptr1.wrapping_byte_add(offset); - - offset = kani::any_where(|x| *x <= mem::size_of::<$type>()); - // generate the dest ptr non-deterministically with same or different provenance - let dest_ptr: *const $type = if kani::any() { - ptr1.wrapping_byte_add(offset) + const gen_size: usize = mem::size_of::<$type>(); + let mut generator1 = PointerGenerator::::new(); + let mut generator2 = PointerGenerator::::new(); + let ptr1: *const $type = generator1.any_in_bounds().ptr; + let ptr2: *const $type = if kani::any() { + generator1.any_alloc_status().ptr } else { - ptr2.wrapping_byte_add(offset) + generator2.any_alloc_status().ptr }; unsafe { - src_ptr.offset_from(dest_ptr); + ptr1.offset_from(ptr2); } } }; @@ -1986,21 +1980,24 @@ mod verify { fn $proof_name() { let arr1: [$type; ARRAY_SIZE] = kani::Arbitrary::any_array(); let arr2: [$type; ARRAY_SIZE] = kani::Arbitrary::any_array(); - let len_arr_bytes: usize = mem::size_of::<$type>() * ARRAY_SIZE; - let ptr_arr1: *const $type = arr1.as_ptr(); + let slice1 = kani::slice::any_slice_of_array(&arr1); + let slice2 = kani::slice::any_slice_of_array(&arr2); + + let ptr1: *const $type = slice1.as_ptr(); + let ptr2: *const $type = slice2.as_ptr(); // Non-deterministically offset the pointer within the allocated object - let mut offset: usize = kani::any_where(|x| *x <= len_arr_bytes ); - let src_ptr: *const $type = ptr_arr1.wrapping_byte_add(offset); + let mut offset: usize = kani::any_where(|x| *x <= slice1.len() * mem::size_of::<$type>()); + let src_ptr: *const $type = ptr1.wrapping_byte_add(offset); - offset = kani::any_where(|x| *x <= len_arr_bytes); - // Non-deterministically generate pointer of same or different provenance let dest_ptr: *const $type = if kani::any() { - ptr_arr1.wrapping_byte_add(offset) + offset = kani::any_where(|x| *x <= slice1.len() * mem::size_of::<$type>()); + ptr1.wrapping_byte_add(offset) } else { - arr2.as_ptr().wrapping_byte_add(offset) as *const $type + offset = kani::any_where(|x| *x <= slice2.len() * mem::size_of::<$type>()); + ptr2.wrapping_byte_add(offset) }; unsafe { @@ -2010,18 +2007,17 @@ mod verify { } } - generate_offset_from_harnesses_for_slices!(i8, check_offset_from_slice_i8); - generate_offset_from_harnesses_for_slices!(i16, check_offset_from_slice_i16); - generate_offset_from_harnesses_for_slices!(i32, check_offset_from_slice_i32); - generate_offset_from_harnesses_for_slices!(i64, check_offset_from_slice_i64); - generate_offset_from_harnesses_for_slices!(i128, check_offset_from_slice_i128); - generate_offset_from_harnesses_for_slices!(isize, check_offset_from_slice_isize); - generate_offset_from_harnesses_for_slices!(u8, check_offset_from_slice_u8); - generate_offset_from_harnesses_for_slices!(u16, check_offset_from_slice_u16); - generate_offset_from_harnesses_for_slices!(u32, check_offset_from_slice_u32); - generate_offset_from_harnesses_for_slices!(u64, check_offset_from_slice_u64); - generate_offset_from_harnesses_for_slices!(u128, check_offset_from_slice_u128); - generate_offset_from_harnesses_for_slices!(usize, check_offset_from_slice_usize); - generate_offset_from_harnesses_for_slices!(bool, check_offset_from_slice_bool); - generate_offset_from_harnesses_for_slices!((), check_offset_from_slice_unit); + generate_offset_from_harnesses_for_slices!(i8, check_const_offset_from_slice_i8); + generate_offset_from_harnesses_for_slices!(i16, check_const_offset_from_slice_i16); + generate_offset_from_harnesses_for_slices!(i32, check_const_offset_from_slice_i32); + generate_offset_from_harnesses_for_slices!(i64, check_const_offset_from_slice_i64); + generate_offset_from_harnesses_for_slices!(i128, check_const_offset_from_slice_i128); + generate_offset_from_harnesses_for_slices!(isize, check_const_offset_from_slice_isize); + generate_offset_from_harnesses_for_slices!(u8, check_const_offset_from_slice_u8); + generate_offset_from_harnesses_for_slices!(u16, check_const_offset_from_slice_u16); + generate_offset_from_harnesses_for_slices!(u32, check_const_offset_from_slice_u32); + generate_offset_from_harnesses_for_slices!(u64, check_const_offset_from_slice_u64); + generate_offset_from_harnesses_for_slices!(u128, check_const_offset_from_slice_u128); + generate_offset_from_harnesses_for_slices!(usize, check_const_offset_from_slice_usize); + generate_offset_from_harnesses_for_slices!(bool, check_const_offset_from_slice_bool); } From d46714e6e6c67578e5fe718782be35483aadde3c Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Thu, 14 Nov 2024 11:57:12 -0800 Subject: [PATCH 10/11] Uses PointerGeenrator to suppot proofs with large arrays --- library/core/src/ptr/const_ptr.rs | 106 +++++++++++------------------- 1 file changed, 40 insertions(+), 66 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 3cd465140bc39..c35df18882bb6 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1917,6 +1917,7 @@ mod verify { use kani::PointerGenerator; use core::mem; + // Proof for unit size will panic as offset_from needs the pointee size to be greater then 0 #[kani::proof_for_contract(<*const ()>::offset_from)] #[kani::should_panic] pub fn check_const_offset_from_unit() { @@ -1928,10 +1929,14 @@ mod verify { } } + // Array size 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) => { + // Proof for a single element #[kani::proof_for_contract(<*const $type>::offset_from)] - pub fn $proof_name() { + pub fn $proof_name1() { const gen_size: usize = mem::size_of::<$type>(); let mut generator1 = PointerGenerator::::new(); let mut generator2 = PointerGenerator::::new(); @@ -1946,78 +1951,47 @@ mod verify { ptr1.offset_from(ptr2); } } - }; - } - - generate_offset_from_harness!(u8, check_const_offset_from_u8); - generate_offset_from_harness!(u16, check_const_offset_from_u16); - generate_offset_from_harness!(u32, check_const_offset_from_u32); - generate_offset_from_harness!(u64, check_const_offset_from_u64); - generate_offset_from_harness!(u128, check_const_offset_from_u128); - generate_offset_from_harness!(usize, check_const_offset_from_usize); - - generate_offset_from_harness!(i8, check_const_offset_from_i8); - generate_offset_from_harness!(i16, check_const_offset_from_i16); - generate_offset_from_harness!(i32, check_const_offset_from_i32); - generate_offset_from_harness!(i64, check_const_offset_from_i64); - generate_offset_from_harness!(i128, check_const_offset_from_i128); - generate_offset_from_harness!(isize, check_const_offset_from_isize); - - generate_offset_from_harness!((i8, i8), check_const_offset_from_tuple_1); - generate_offset_from_harness!((f64, bool), check_const_offset_from_tuple_2); - generate_offset_from_harness!((u32, i16, f32), check_const_offset_from_tuple_3); - generate_offset_from_harness!( - ((), bool, u8, u16, i32, f64, i128, usize), - check_const_offset_from_tuple_4 - ); - - // Array size bound for kani::any_array - const ARRAY_SIZE: usize = 40; - macro_rules! generate_offset_from_harnesses_for_slices { - ($type:ty, $proof_name:ident) => { + // Proof for large arrays #[kani::proof_for_contract(<*const $type>::offset_from)] - fn $proof_name() { - let arr1: [$type; ARRAY_SIZE] = kani::Arbitrary::any_array(); - let arr2: [$type; ARRAY_SIZE] = kani::Arbitrary::any_array(); - - let slice1 = kani::slice::any_slice_of_array(&arr1); - let slice2 = kani::slice::any_slice_of_array(&arr2); - - let ptr1: *const $type = slice1.as_ptr(); - let ptr2: *const $type = slice2.as_ptr(); - - // Non-deterministically offset the pointer within the allocated object - let mut offset: usize = kani::any_where(|x| *x <= slice1.len() * mem::size_of::<$type>()); - let src_ptr: *const $type = ptr1.wrapping_byte_add(offset); - - // Non-deterministically generate pointer of same or different provenance - let dest_ptr: *const $type = if kani::any() { - offset = kani::any_where(|x| *x <= slice1.len() * mem::size_of::<$type>()); - ptr1.wrapping_byte_add(offset) + 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: *const $type = generator1.any_in_bounds().ptr; + let ptr2: *const $type = if kani::any() { + generator1.any_alloc_status().ptr } else { - offset = kani::any_where(|x| *x <= slice2.len() * mem::size_of::<$type>()); - ptr2.wrapping_byte_add(offset) + generator2.any_alloc_status().ptr }; unsafe { - src_ptr.offset_from(dest_ptr); + ptr1.offset_from(ptr2); } } - } + }; } - generate_offset_from_harnesses_for_slices!(i8, check_const_offset_from_slice_i8); - generate_offset_from_harnesses_for_slices!(i16, check_const_offset_from_slice_i16); - generate_offset_from_harnesses_for_slices!(i32, check_const_offset_from_slice_i32); - generate_offset_from_harnesses_for_slices!(i64, check_const_offset_from_slice_i64); - generate_offset_from_harnesses_for_slices!(i128, check_const_offset_from_slice_i128); - generate_offset_from_harnesses_for_slices!(isize, check_const_offset_from_slice_isize); - generate_offset_from_harnesses_for_slices!(u8, check_const_offset_from_slice_u8); - generate_offset_from_harnesses_for_slices!(u16, check_const_offset_from_slice_u16); - generate_offset_from_harnesses_for_slices!(u32, check_const_offset_from_slice_u32); - generate_offset_from_harnesses_for_slices!(u64, check_const_offset_from_slice_u64); - generate_offset_from_harnesses_for_slices!(u128, check_const_offset_from_slice_u128); - generate_offset_from_harnesses_for_slices!(usize, check_const_offset_from_slice_usize); - generate_offset_from_harnesses_for_slices!(bool, check_const_offset_from_slice_bool); + generate_offset_from_harness!(u8, check_const_offset_from_u8, check_const_offset_from_u8_arr); + generate_offset_from_harness!(u16, check_const_offset_from_u16, check_const_offset_from_u16_arr); + generate_offset_from_harness!(u32, check_const_offset_from_u32, check_const_offset_from_u32_arr); + generate_offset_from_harness!(u64, check_const_offset_from_u64, check_const_offset_from_u64_arr); + generate_offset_from_harness!(u128, check_const_offset_from_u128, check_const_offset_from_u128_arr); + generate_offset_from_harness!(usize, check_const_offset_from_usize, check_const_offset_from_usize_arr); + + generate_offset_from_harness!(i8, check_const_offset_from_i8, check_const_offset_from_i8_arr); + generate_offset_from_harness!(i16, check_const_offset_from_i16, check_const_offset_from_i16_arr); + generate_offset_from_harness!(i32, check_const_offset_from_i32, check_const_offset_from_i32_arr); + generate_offset_from_harness!(i64, check_const_offset_from_i64, check_const_offset_from_i64_arr); + generate_offset_from_harness!(i128, check_const_offset_from_i128, check_const_offset_from_i128_arr); + generate_offset_from_harness!(isize, check_const_offset_from_isize, check_const_offset_from_isize_arr); + + generate_offset_from_harness!((i8, i8), check_const_offset_from_tuple_1, check_const_offset_from_tuple_1_arr); + generate_offset_from_harness!((f64, bool), check_const_offset_from_tuple_2, check_const_offset_from_tuple_2_arr); + generate_offset_from_harness!((u32, i16, f32), check_const_offset_from_tuple_3, check_const_offset_from_tuple_3_arr); + generate_offset_from_harness!( + ((), bool, u8, u16, i32, f64, i128, usize), + check_const_offset_from_tuple_4, + check_const_offset_from_tuple_4_arr + ); } From b05ceb3a567e6284f692afaab018ed8844ae432b Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Thu, 14 Nov 2024 12:00:50 -0800 Subject: [PATCH 11/11] Runs rustfmt --- library/core/src/ptr/const_ptr.rs | 104 ++++++++++++++++++++++++------ 1 file changed, 84 insertions(+), 20 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index c35df18882bb6..c7f762dabe3d3 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -672,10 +672,14 @@ impl *const T { #[inline] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires( + // Ensures subtracting `origin` from `self` doesn't overflow (self as isize).checked_sub(origin as isize).is_some() && + // Ensure the distance between `self` and `origin` is aligned to `T` (self as isize - origin as isize) % (mem::size_of::() as isize) == 0 && + // Ensure both pointers are in the same allocation or are pointing to the same address (self as isize == origin as isize || kani::mem::same_allocation(self, origin)) )] + // The result should equal the distance in terms of elements of type `T` as per the documentation above #[ensures(|result| *result == (self as isize - origin as isize) / (mem::size_of::() as isize))] pub const unsafe fn offset_from(self, origin: *const T) -> isize where @@ -1914,8 +1918,8 @@ impl PartialOrd for *const T { #[unstable(feature = "kani", issue = "none")] mod verify { use crate::kani; - use kani::PointerGenerator; use core::mem; + use kani::PointerGenerator; // Proof for unit size will panic as offset_from needs the pointee size to be greater then 0 #[kani::proof_for_contract(<*const ()>::offset_from)] @@ -1956,8 +1960,8 @@ mod verify { #[kani::proof_for_contract(<*const $type>::offset_from)] 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 mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); let ptr1: *const $type = generator1.any_in_bounds().ptr; let ptr2: *const $type = if kani::any() { generator1.any_alloc_status().ptr @@ -1972,23 +1976,83 @@ mod verify { }; } - generate_offset_from_harness!(u8, check_const_offset_from_u8, check_const_offset_from_u8_arr); - generate_offset_from_harness!(u16, check_const_offset_from_u16, check_const_offset_from_u16_arr); - generate_offset_from_harness!(u32, check_const_offset_from_u32, check_const_offset_from_u32_arr); - generate_offset_from_harness!(u64, check_const_offset_from_u64, check_const_offset_from_u64_arr); - generate_offset_from_harness!(u128, check_const_offset_from_u128, check_const_offset_from_u128_arr); - generate_offset_from_harness!(usize, check_const_offset_from_usize, check_const_offset_from_usize_arr); - - generate_offset_from_harness!(i8, check_const_offset_from_i8, check_const_offset_from_i8_arr); - generate_offset_from_harness!(i16, check_const_offset_from_i16, check_const_offset_from_i16_arr); - generate_offset_from_harness!(i32, check_const_offset_from_i32, check_const_offset_from_i32_arr); - generate_offset_from_harness!(i64, check_const_offset_from_i64, check_const_offset_from_i64_arr); - generate_offset_from_harness!(i128, check_const_offset_from_i128, check_const_offset_from_i128_arr); - generate_offset_from_harness!(isize, check_const_offset_from_isize, check_const_offset_from_isize_arr); - - generate_offset_from_harness!((i8, i8), check_const_offset_from_tuple_1, check_const_offset_from_tuple_1_arr); - generate_offset_from_harness!((f64, bool), check_const_offset_from_tuple_2, check_const_offset_from_tuple_2_arr); - generate_offset_from_harness!((u32, i16, f32), check_const_offset_from_tuple_3, check_const_offset_from_tuple_3_arr); + generate_offset_from_harness!( + u8, + check_const_offset_from_u8, + check_const_offset_from_u8_arr + ); + generate_offset_from_harness!( + u16, + check_const_offset_from_u16, + check_const_offset_from_u16_arr + ); + generate_offset_from_harness!( + u32, + check_const_offset_from_u32, + check_const_offset_from_u32_arr + ); + generate_offset_from_harness!( + u64, + check_const_offset_from_u64, + check_const_offset_from_u64_arr + ); + generate_offset_from_harness!( + u128, + check_const_offset_from_u128, + check_const_offset_from_u128_arr + ); + generate_offset_from_harness!( + usize, + check_const_offset_from_usize, + check_const_offset_from_usize_arr + ); + + generate_offset_from_harness!( + i8, + check_const_offset_from_i8, + check_const_offset_from_i8_arr + ); + generate_offset_from_harness!( + i16, + check_const_offset_from_i16, + check_const_offset_from_i16_arr + ); + generate_offset_from_harness!( + i32, + check_const_offset_from_i32, + check_const_offset_from_i32_arr + ); + generate_offset_from_harness!( + i64, + check_const_offset_from_i64, + check_const_offset_from_i64_arr + ); + generate_offset_from_harness!( + i128, + check_const_offset_from_i128, + check_const_offset_from_i128_arr + ); + generate_offset_from_harness!( + isize, + check_const_offset_from_isize, + check_const_offset_from_isize_arr + ); + + generate_offset_from_harness!( + (i8, i8), + check_const_offset_from_tuple_1, + check_const_offset_from_tuple_1_arr + ); + generate_offset_from_harness!( + (f64, bool), + check_const_offset_from_tuple_2, + check_const_offset_from_tuple_2_arr + ); + generate_offset_from_harness!( + (u32, i16, f32), + check_const_offset_from_tuple_3, + check_const_offset_from_tuple_3_arr + ); generate_offset_from_harness!( ((), bool, u8, u16, i32, f64, i128, usize), check_const_offset_from_tuple_4,