Skip to content

Verify/ptr mut refactor harness #12

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Nov 7, 2024
Merged

Verify/ptr mut refactor harness #12

Changes from 3 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
96a8a2e
refactored function contracts for add, sub and offset using the same_…
xsxszab Oct 23, 2024
852e96f
merged macros for add, sub and offset
xsxszab Oct 23, 2024
04bd61e
updated function contracts and proof for contracts for add(), sub() a…
xsxszab Oct 24, 2024
7557fc5
added support for unit type pointers
xsxszab Oct 31, 2024
76b2311
updated function contracts, removed unnecessary kani::assmue
xsxszab Nov 6, 2024
cb6a177
added comments to function contracts
xsxszab Nov 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
207 changes: 118 additions & 89 deletions library/core/src/ptr/mut_ptr.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -407,10 +407,11 @@ impl<T: ?Sized> *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))]
#[requires(
count.checked_mul(core::mem::size_of::<T>() 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,
Expand Down Expand Up @@ -955,10 +956,12 @@ impl<T: ?Sized> *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))]
#[requires(
count.checked_mul(core::mem::size_of::<T>()).is_some() &&
count * core::mem::size_of::<T>() <= 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,
Expand Down Expand Up @@ -1034,10 +1037,12 @@ impl<T: ?Sized> *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))]
#[requires(
count.checked_mul(core::mem::size_of::<T>()).is_some() &&
count * core::mem::size_of::<T>() <= 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,
Expand Down Expand Up @@ -2219,102 +2224,126 @@ impl<T: ?Sized> PartialOrd for *mut T {
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)]
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();
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);
unsafe {
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();
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);
}
}
};
($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();
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);
Copy link
Owner

@stogaru stogaru Nov 6, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

do you think we can use wrapping_byte_add to create and test unaligned pointers?

Copy link
Collaborator Author

@xsxszab xsxszab Nov 7, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just tested it out, actually unaligned pointer worked fine, I think we can use wrapping_byte_add in our next version

unsafe {
test_ptr.$func_name(count);
ptr_with_offset.offset(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);
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_add_and_sub_harness!((), check_mut_add_unit, add);
// generate_mut_arithmetic_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);
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_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);
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_add_and_sub_harness!((), check_mut_sub_unit, sub);
// generate_mut_arithmetic_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) => {
#[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);
}
}
};
}

// 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);
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);
}