From 17658b34a597d14c9356d2351afa9fa373d045a8 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Tue, 26 Nov 2024 01:46:02 -0800 Subject: [PATCH 1/6] Contracts and harnesses for byte_offset_from verifying int, unit, slice, and composite types --- library/core/src/ptr/const_ptr.rs | 198 ++++++++++++++++++++++++++++++ library/core/src/ptr/mut_ptr.rs | 198 ++++++++++++++++++++++++++++++ 2 files changed, 396 insertions(+) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 57a7c0fc0925c..2a320aed1de07 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -3,6 +3,11 @@ 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; +use core::mem; impl *const T { /// Returns `true` if the pointer is null. @@ -690,6 +695,16 @@ impl *const T { #[stable(feature = "pointer_byte_offsets", since = "1.75.0")] #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires( + (mem::size_of_val_raw(self) != 0) && + // Ensures subtracting `origin` from `self` doesn't overflow + (self.addr() as isize).checked_sub(origin.addr() as isize).is_some() && + // Ensure both pointers are in the same allocation or are pointing to the same address + (self.addr() == origin.addr() || + kani::mem::same_allocation(self as *const u8, origin as *const u8)) + )] + // The result should equal the distance in terms of bytes + #[ensures(|result| *result == (self.addr() as isize - origin.addr() as isize))] pub const unsafe fn byte_offset_from(self, origin: *const U) -> isize { // SAFETY: the caller must uphold the safety contract for `offset_from`. unsafe { self.cast::().offset_from(origin.cast::()) } @@ -1899,3 +1914,186 @@ impl PartialOrd for *const T { *self >= *other } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod verify { + use crate::kani; + use core::mem; + use kani::PointerGenerator; + + const ARRAY_LEN: usize = 40; + + // Proof for unit size + #[kani::proof_for_contract(<*const ()>::byte_offset_from)] + pub fn check_const_byte_offset_from_unit() { + let val: () = (); + let src_ptr: *const () = &val; + let dest_ptr: *const () = &val; + unsafe { + dest_ptr.byte_offset_from(src_ptr); + } + } + + macro_rules! generate_const_byte_offset_from_harness { + ($type: ty, $proof_name1: ident, $proof_name2: ident) => { + // Proof for a single element + #[kani::proof_for_contract(<*const $type>::byte_offset_from)] + pub fn $proof_name1() { + 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 { + generator2.any_alloc_status().ptr + }; + + unsafe { + ptr1.byte_offset_from(ptr2); + } + } + + // Proof for large arrays + #[kani::proof_for_contract(<*const $type>::byte_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 ptr1: *const $type = generator1.any_in_bounds().ptr; + let ptr2: *const $type = if kani::any() { + generator1.any_alloc_status().ptr + } else { + generator2.any_alloc_status().ptr + }; + + unsafe { + ptr1.byte_offset_from(ptr2); + } + } + }; + } + + generate_const_byte_offset_from_harness!( + u8, + check_const_byte_offset_from_u8, + check_const_byte_offset_from_u8_arr + ); + generate_const_byte_offset_from_harness!( + u16, + check_const_byte_offset_from_u16, + check_const_byte_offset_from_u16_arr + ); + generate_const_byte_offset_from_harness!( + u32, + check_const_byte_offset_from_u32, + check_const_byte_offset_from_u32_arr + ); + generate_const_byte_offset_from_harness!( + u64, + check_const_byte_offset_from_u64, + check_const_byte_offset_from_u64_arr + ); + generate_const_byte_offset_from_harness!( + u128, + check_const_byte_offset_from_u128, + check_const_byte_offset_from_u128_arr + ); + generate_const_byte_offset_from_harness!( + usize, + check_const_byte_offset_from_usize, + check_const_byte_offset_from_usize_arr + ); + + generate_const_byte_offset_from_harness!( + i8, + check_const_byte_offset_from_i8, + check_const_byte_offset_from_i8_arr + ); + generate_const_byte_offset_from_harness!( + i16, + check_const_byte_offset_from_i16, + check_const_byte_offset_from_i16_arr + ); + generate_const_byte_offset_from_harness!( + i32, + check_const_byte_offset_from_i32, + check_const_byte_offset_from_i32_arr + ); + generate_const_byte_offset_from_harness!( + i64, + check_const_byte_offset_from_i64, + check_const_byte_offset_from_i64_arr + ); + generate_const_byte_offset_from_harness!( + i128, + check_const_byte_offset_from_i128, + check_const_byte_offset_from_i128_arr + ); + generate_const_byte_offset_from_harness!( + isize, + check_const_byte_offset_from_isize, + check_const_byte_offset_from_isize_arr + ); + + generate_const_byte_offset_from_harness!( + (i8, i8), + check_const_byte_offset_from_tuple_1, + check_const_byte_offset_from_tuple_1_arr + ); + generate_const_byte_offset_from_harness!( + (f64, bool), + check_const_byte_offset_from_tuple_2, + check_const_byte_offset_from_tuple_2_arr + ); + generate_const_byte_offset_from_harness!( + (u32, i16, f32), + check_const_byte_offset_from_tuple_3, + check_const_byte_offset_from_tuple_3_arr + ); + generate_const_byte_offset_from_harness!( + ((), bool, u8, u16, i32, f64, i128, usize), + check_const_byte_offset_from_tuple_4, + check_const_byte_offset_from_tuple_4_arr + ); + + const SLICE_LEN: usize = 10; + + macro_rules! generate_const_byte_offset_from_slice_harness { + ($type: ty, $proof_name: ident) => { + + // Proof for large arrays + #[kani::proof_for_contract(<*const [$type]>::byte_offset_from)] + pub fn $proof_name() { + 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 as *const [$type; SLICE_LEN]; + let ptr2: *const [$type] = if kani::any() { + generator1.any_alloc_status().ptr as *const [$type; SLICE_LEN] + } else { + generator2.any_alloc_status().ptr as *const [$type; SLICE_LEN] + }; + + unsafe { + ptr1.byte_offset_from(ptr2); + } + } + }; + } + + generate_const_byte_offset_from_slice_harness!(u8, check_const_byte_offset_from_u8_slice); + generate_const_byte_offset_from_slice_harness!(u16, check_const_byte_offset_from_u16_slice); + generate_const_byte_offset_from_slice_harness!(u32, check_const_byte_offset_from_u32_slice); + generate_const_byte_offset_from_slice_harness!(u64, check_const_byte_offset_from_u64_slice); + generate_const_byte_offset_from_slice_harness!(u128, check_const_byte_offset_from_u128_slice); + generate_const_byte_offset_from_slice_harness!(usize, check_const_byte_offset_from_usize_slice); + generate_const_byte_offset_from_slice_harness!(i8, check_const_byte_offset_from_i8_slice); + generate_const_byte_offset_from_slice_harness!(i16, check_const_byte_offset_from_i16_slice); + generate_const_byte_offset_from_slice_harness!(i32, check_const_byte_offset_from_i32_slice); + generate_const_byte_offset_from_slice_harness!(i64, check_const_byte_offset_from_i64_slice); + generate_const_byte_offset_from_slice_harness!(i128, check_const_byte_offset_from_i128_slice); + generate_const_byte_offset_from_slice_harness!(isize, check_const_byte_offset_from_isize_slice); + +} diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 7aa6a309a06b5..23cb9bc21d2ef 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -3,6 +3,11 @@ 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; +use core::mem; impl *mut T { /// Returns `true` if the pointer is null. @@ -852,6 +857,16 @@ impl *mut T { #[stable(feature = "pointer_byte_offsets", since = "1.75.0")] #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires( + (mem::size_of_val_raw(self) != 0) && + // Ensures subtracting `origin` from `self` doesn't overflow + (self.addr() as isize).checked_sub(origin.addr() as isize).is_some() && + // Ensure both pointers are in the same allocation or are pointing to the same address + (self.addr() == origin.addr() || + kani::mem::same_allocation(self as *const u8, origin as *const u8)) + )] + // The result should equal the distance in terms of bytes + #[ensures(|result| *result == (self.addr() as isize - origin.addr() as isize))] pub const unsafe fn byte_offset_from(self, origin: *const U) -> isize { // SAFETY: the caller must uphold the safety contract for `offset_from`. unsafe { self.cast::().offset_from(origin.cast::()) } @@ -2302,3 +2317,186 @@ impl PartialOrd for *mut T { *self >= *other } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod verify { + use crate::kani; + use core::mem; + use kani::PointerGenerator; + + const ARRAY_LEN: usize = 40; + + // Proof for unit size + #[kani::proof_for_contract(<*mut ()>::byte_offset_from)] + pub fn check_mut_byte_offset_from_unit() { + let mut val: () = (); + let src_ptr: *mut () = &mut val; + let dest_ptr: *mut () = &mut val; + unsafe { + dest_ptr.byte_offset_from(src_ptr); + } + } + + macro_rules! generate_mut_byte_offset_from_harness { + ($type: ty, $proof_name1: ident, $proof_name2: ident) => { + // Proof for a single element + #[kani::proof_for_contract(<*mut $type>::byte_offset_from)] + 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 { + generator2.any_alloc_status().ptr + }; + + unsafe { + ptr1.byte_offset_from(ptr2); + } + } + + // Proof for large arrays + #[kani::proof_for_contract(<*mut $type>::byte_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 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 { + ptr1.byte_offset_from(ptr2); + } + } + }; + } + + generate_mut_byte_offset_from_harness!( + u8, + check_mut_byte_offset_from_u8, + check_mut_byte_offset_from_u8_arr + ); + generate_mut_byte_offset_from_harness!( + u16, + check_mut_byte_offset_from_u16, + check_mut_byte_offset_from_u16_arr + ); + generate_mut_byte_offset_from_harness!( + u32, + check_mut_byte_offset_from_u32, + check_mut_byte_offset_from_u32_arr + ); + generate_mut_byte_offset_from_harness!( + u64, + check_mut_byte_offset_from_u64, + check_mut_byte_offset_from_u64_arr + ); + generate_mut_byte_offset_from_harness!( + u128, + check_mut_byte_offset_from_u128, + check_mut_byte_offset_from_u128_arr + ); + generate_mut_byte_offset_from_harness!( + usize, + check_mut_byte_offset_from_usize, + check_mut_byte_offset_from_usize_arr + ); + + generate_mut_byte_offset_from_harness!( + i8, + check_mut_byte_offset_from_i8, + check_mut_byte_offset_from_i8_arr + ); + generate_mut_byte_offset_from_harness!( + i16, + check_mut_byte_offset_from_i16, + check_mut_byte_offset_from_i16_arr + ); + generate_mut_byte_offset_from_harness!( + i32, + check_mut_byte_offset_from_i32, + check_mut_byte_offset_from_i32_arr + ); + generate_mut_byte_offset_from_harness!( + i64, + check_mut_byte_offset_from_i64, + check_mut_byte_offset_from_i64_arr + ); + generate_mut_byte_offset_from_harness!( + i128, + check_mut_byte_offset_from_i128, + check_mut_byte_offset_from_i128_arr + ); + generate_mut_byte_offset_from_harness!( + isize, + check_mut_byte_offset_from_isize, + check_mut_byte_offset_from_isize_arr + ); + + generate_mut_byte_offset_from_harness!( + (i8, i8), + check_mut_byte_offset_from_tuple_1, + check_mut_byte_offset_from_tuple_1_arr + ); + generate_mut_byte_offset_from_harness!( + (f64, bool), + check_mut_byte_offset_from_tuple_2, + check_mut_byte_offset_from_tuple_2_arr + ); + generate_mut_byte_offset_from_harness!( + (u32, i16, f32), + check_mut_byte_offset_from_tuple_3, + check_mut_byte_offset_from_tuple_3_arr + ); + generate_mut_byte_offset_from_harness!( + ((), bool, u8, u16, i32, f64, i128, usize), + check_mut_byte_offset_from_tuple_4, + check_mut_byte_offset_from_tuple_4_arr + ); + + const SLICE_LEN: usize = 10; + + macro_rules! generate_mut_byte_offset_from_slice_harness { + ($type: ty, $proof_name: ident) => { + + // Proof for large arrays + #[kani::proof_for_contract(<*mut [$type]>::byte_offset_from)] + pub fn $proof_name() { + 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 as *mut [$type; SLICE_LEN]; + let ptr2: *mut [$type] = if kani::any() { + generator1.any_alloc_status().ptr as *mut [$type; SLICE_LEN] + } else { + generator2.any_alloc_status().ptr as *mut [$type; SLICE_LEN] + }; + + unsafe { + ptr1.byte_offset_from(ptr2); + } + } + }; + } + + generate_mut_byte_offset_from_slice_harness!(u8, check_mut_byte_offset_from_u8_slice); + generate_mut_byte_offset_from_slice_harness!(u16, check_mut_byte_offset_from_u16_slice); + generate_mut_byte_offset_from_slice_harness!(u32, check_mut_byte_offset_from_u32_slice); + generate_mut_byte_offset_from_slice_harness!(u64, check_mut_byte_offset_from_u64_slice); + generate_mut_byte_offset_from_slice_harness!(u128, check_mut_byte_offset_from_u128_slice); + generate_mut_byte_offset_from_slice_harness!(usize, check_mut_byte_offset_from_usize_slice); + generate_mut_byte_offset_from_slice_harness!(i8, check_mut_byte_offset_from_i8_slice); + generate_mut_byte_offset_from_slice_harness!(i16, check_mut_byte_offset_from_i16_slice); + generate_mut_byte_offset_from_slice_harness!(i32, check_mut_byte_offset_from_i32_slice); + generate_mut_byte_offset_from_slice_harness!(i64, check_mut_byte_offset_from_i64_slice); + generate_mut_byte_offset_from_slice_harness!(i128, check_mut_byte_offset_from_i128_slice); + generate_mut_byte_offset_from_slice_harness!(isize, check_mut_byte_offset_from_isize_slice); + +} From 660429109ebd21b5ed0825f44ffa36d2031072f6 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Tue, 26 Nov 2024 01:53:30 -0800 Subject: [PATCH 2/6] Adds comments --- library/core/src/ptr/const_ptr.rs | 11 +++++++++-- library/core/src/ptr/mut_ptr.rs | 12 ++++++++++-- 2 files changed, 19 insertions(+), 4 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 2a320aed1de07..ac6c90da72134 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1935,6 +1935,11 @@ pub mod verify { } } + // generate proofs for contracts for byte_offset_from to verify int and composite + // types + // - `$type`: pointee type + // - `$proof_name1`: name of the harness for single element + // - `$proof_name2`: name of the harness for array of elements macro_rules! generate_const_byte_offset_from_harness { ($type: ty, $proof_name1: ident, $proof_name2: ident) => { // Proof for a single element @@ -2058,12 +2063,14 @@ pub mod verify { check_const_byte_offset_from_tuple_4_arr ); + // length of the slice generated from PointerGenerator const SLICE_LEN: usize = 10; + // generate proofs for contracts for byte_offset_from to verify slices + // - `$type`: type of the underlyign element within the slice pointer + // - `$proof_name`: name of the harness macro_rules! generate_const_byte_offset_from_slice_harness { ($type: ty, $proof_name: ident) => { - - // Proof for large arrays #[kani::proof_for_contract(<*const [$type]>::byte_offset_from)] pub fn $proof_name() { const gen_size: usize = mem::size_of::<$type>(); diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 23cb9bc21d2ef..45e1530a92269 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2325,6 +2325,7 @@ pub mod verify { use core::mem; use kani::PointerGenerator; + // bound space for PointerGenerator const ARRAY_LEN: usize = 40; // Proof for unit size @@ -2338,6 +2339,11 @@ pub mod verify { } } + // generate proofs for contracts for byte_offset_from to verify int and composite + // types + // - `$type`: pointee type + // - `$proof_name1`: name of the harness for single element + // - `$proof_name2`: name of the harness for array of elements macro_rules! generate_mut_byte_offset_from_harness { ($type: ty, $proof_name1: ident, $proof_name2: ident) => { // Proof for a single element @@ -2461,12 +2467,14 @@ pub mod verify { check_mut_byte_offset_from_tuple_4_arr ); + // length of the slice generated from PointerGenerator const SLICE_LEN: usize = 10; + // generate proofs for contracts for byte_offset_from to verify slices + // - `$type`: type of the underlyign element within the slice pointer + // - `$proof_name`: name of the harness macro_rules! generate_mut_byte_offset_from_slice_harness { ($type: ty, $proof_name: ident) => { - - // Proof for large arrays #[kani::proof_for_contract(<*mut [$type]>::byte_offset_from)] pub fn $proof_name() { const gen_size: usize = mem::size_of::<$type>(); From 6aacbb852d05e649b1a0171c1a99875b882f08a9 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Wed, 27 Nov 2024 23:07:10 -0800 Subject: [PATCH 3/6] Runs rust format on the file --- library/core/src/ptr/const_ptr.rs | 10 +++++----- library/core/src/ptr/mut_ptr.rs | 4 ++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index cf041e2149ec1..d1397547d0415 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -2070,7 +2070,7 @@ mod verify { check_const_offset_from_tuple_4_arr ); - // Proof for contact of byte_offset_from to verify unit type + // Proof for contact of byte_offset_from to verify unit type #[kani::proof_for_contract(<*const ()>::byte_offset_from)] pub fn check_const_byte_offset_from_unit() { let val: () = (); @@ -2081,7 +2081,7 @@ mod verify { } } - // generate proofs for contracts for byte_offset_from to verify int and composite + // generate proofs for contracts for byte_offset_from to verify int and composite // types // - `$type`: pointee type // - `$proof_name1`: name of the harness for single element @@ -2222,7 +2222,8 @@ mod verify { 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 as *const [$type; SLICE_LEN]; + let ptr1: *const [$type] = + generator1.any_in_bounds().ptr as *const [$type; SLICE_LEN]; let ptr2: *const [$type] = if kani::any() { generator1.any_alloc_status().ptr as *const [$type; SLICE_LEN] } else { @@ -2235,7 +2236,7 @@ mod verify { } }; } - + generate_const_byte_offset_from_slice_harness!(u8, check_const_byte_offset_from_u8_slice); generate_const_byte_offset_from_slice_harness!(u16, check_const_byte_offset_from_u16_slice); generate_const_byte_offset_from_slice_harness!(u32, check_const_byte_offset_from_u32_slice); @@ -2248,5 +2249,4 @@ mod verify { generate_const_byte_offset_from_slice_harness!(i64, check_const_byte_offset_from_i64_slice); generate_const_byte_offset_from_slice_harness!(i128, check_const_byte_offset_from_i128_slice); generate_const_byte_offset_from_slice_harness!(isize, check_const_byte_offset_from_isize_slice); - } diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 5c85a59cbb55f..c64fc286223ba 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2389,7 +2389,7 @@ pub mod verify { } } - // generate proofs for contracts for byte_offset_from to verify int and composite + // generate proofs for contracts for byte_offset_from to verify int and composite // types // - `$type`: pointee type // - `$proof_name1`: name of the harness for single element @@ -2543,7 +2543,7 @@ pub mod verify { } }; } - + generate_mut_byte_offset_from_slice_harness!(u8, check_mut_byte_offset_from_u8_slice); generate_mut_byte_offset_from_slice_harness!(u16, check_mut_byte_offset_from_u16_slice); generate_mut_byte_offset_from_slice_harness!(u32, check_mut_byte_offset_from_u32_slice); From 30ab88dd362a2f5ff20e0b1f97f7181a6df9e4c4 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Thu, 28 Nov 2024 01:56:07 -0800 Subject: [PATCH 4/6] Removes unnecessary `pub` visibility specifier --- 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 c64fc286223ba..5bf08bdb7535e 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2370,7 +2370,7 @@ impl PartialOrd for *mut T { #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] -pub mod verify { +mod verify { use crate::kani; use core::mem; use kani::PointerGenerator; From dbf29ae6fa3f0b10f1f198b32b27d3cf06230c66 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Thu, 28 Nov 2024 18:47:30 -0800 Subject: [PATCH 5/6] Verify byte_offset_from postcondition with a harness --- library/core/src/ptr/const_ptr.rs | 11 +++++++++++ library/core/src/ptr/mut_ptr.rs | 13 ++++++++++++- 2 files changed, 23 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index d1397547d0415..6ac58b12d47fb 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1947,6 +1947,17 @@ mod verify { // Array size bound for PointerGenerator const ARRAY_LEN: usize = 40; + #[kani::proof] + pub fn check_const_byte_offset_from_fixed_offset() { + let arr: [u32; ARRAY_LEN] = kani::Arbitrary::any_array(); + let offset: usize = kani::any_where(|&x| x <= ARRAY_LEN); + let origin_ptr: *const u32 = arr.as_ptr(); + let self_ptr: *const u32 = unsafe { origin_ptr.byte_offset(offset as isize) }; + let result: isize = unsafe { self_ptr.byte_offset_from(origin_ptr) }; + assert_eq!(result, offset as isize); + assert_eq!(result, (self_ptr.addr() as isize - origin_ptr.addr() as isize)); + } + macro_rules! generate_offset_from_harness { ($type: ty, $proof_name1: ident, $proof_name2: ident) => { // Proof for a single element diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 5bf08bdb7535e..603f82bb5acf6 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2375,9 +2375,20 @@ mod verify { use core::mem; use kani::PointerGenerator; - // bound space for PointerGenerator + // bound space for PointerGenerator and arrays const ARRAY_LEN: usize = 40; + #[kani::proof] + pub fn check_mut_byte_offset_from_fixed_offset() { + let mut arr: [u32; ARRAY_LEN] = kani::Arbitrary::any_array(); + let offset: usize = kani::any_where(|&x| x <= ARRAY_LEN); + let origin_ptr: *mut u32 = arr.as_mut_ptr(); + let self_ptr: *mut u32 = unsafe { origin_ptr.byte_offset(offset as isize) }; + let result: isize = unsafe { self_ptr.byte_offset_from(origin_ptr) }; + assert_eq!(result, offset as isize); + assert_eq!(result, (self_ptr.addr() as isize - origin_ptr.addr() as isize)); + } + // Proof for unit size #[kani::proof_for_contract(<*mut ()>::byte_offset_from)] pub fn check_mut_byte_offset_from_unit() { From f7448a670645a5e994379e66c2a5f978fcc672a1 Mon Sep 17 00:00:00 2001 From: Surya Togaru Date: Thu, 5 Dec 2024 00:12:05 -0800 Subject: [PATCH 6/6] Refactors contracts to be tool agnostic --- library/core/src/ptr/const_ptr.rs | 6 ++++-- library/core/src/ptr/mut_ptr.rs | 11 ++++++++--- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index c5abc07c6c826..cd20e6be9121f 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -722,7 +722,7 @@ impl *const T { (self.addr() as isize).checked_sub(origin.addr() as isize).is_some() && // Ensure both pointers are in the same allocation or are pointing to the same address (self.addr() == origin.addr() || - kani::mem::same_allocation(self as *const u8, origin as *const u8)) + core::ub_checks::same_allocation(self as *const u8, origin as *const u8)) )] // The result should equal the distance in terms of bytes #[ensures(|result| *result == (self.addr() as isize - origin.addr() as isize))] @@ -2079,7 +2079,9 @@ mod verify { check_const_offset_slice_tuple_4 ); - // Array size bound for PointerGenerator + // The array's length is set to an arbitrary value, which defines its size. + // In this case, implementing a dynamic array is not possible, because + // PointerGenerator or any_array() do not support dynamic sized arrays. const ARRAY_LEN: usize = 40; #[kani::proof] diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index c7bee9e908665..4d5cc2e4f5dc8 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -875,7 +875,7 @@ impl *mut T { (self.addr() as isize).checked_sub(origin.addr() as isize).is_some() && // Ensure both pointers are in the same allocation or are pointing to the same address (self.addr() == origin.addr() || - kani::mem::same_allocation(self as *const u8, origin as *const u8)) + core::ub_checks::same_allocation(self as *const u8, origin as *const u8)) )] // The result should equal the distance in terms of bytes #[ensures(|result| *result == (self.addr() as isize - origin.addr() as isize))] @@ -2191,7 +2191,9 @@ mod verify { use core::mem; use kani::PointerGenerator; - // bound space for PointerGenerator and arrays + // The array's length is set to an arbitrary value, which defines its size. + // In this case, implementing a dynamic array is not possible, because + // PointerGenerator or any_array() do not support dynamic sized arrays. const ARRAY_LEN: usize = 40; #[kani::proof] @@ -2344,7 +2346,10 @@ mod verify { check_mut_byte_offset_from_tuple_4_arr ); - // length of the slice generated from PointerGenerator + // The length of a slice is set to an arbitrary value, which defines its size. + // In this case, implementing a slice with a dynamic size set using kani::any() + // is not possible, because PointerGenerator does not support non-deterministic + // slice pointers. const SLICE_LEN: usize = 10; // generate proofs for contracts for byte_offset_from to verify slices