Skip to content

Contracts and Harnesses for <*const T>::byte_add, byte_sub and byte_offset #177

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

Closed
wants to merge 4 commits into from
Closed

Contracts and Harnesses for <*const T>::byte_add, byte_sub and byte_offset #177

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2fdebd6
Adds contracts for byte_offset, byte_add and byte_sub
stogaru Nov 16, 2024
cd0a134
Runs rustfmt
stogaru Nov 16, 2024
81fe7c9
Refactors the function contracts
stogaru Nov 21, 2024
bee4503
Merge branch 'main' into verify/ptr_const_byte
stogaru Nov 22, 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
299 changes: 299 additions & 0 deletions library/core/src/ptr/const_ptr.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<T: ?Sized> *const T {
/// Returns `true` if the pointer is null.
Expand Down Expand Up @@ -459,6 +464,22 @@ impl<T: ?Sized> *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(
// If the size of the pointee is zero, then `count` must also be zero
(mem::size_of_val_raw(self) == 0 && count == 0) ||
// If the size of the pointee is not zero, then ensure that adding `count`
// bytes doesn't cause overflow and that both pointers `self` and the result
// are pointing to the same address or in the same allocation
(mem::size_of_val_raw(self) != 0 &&
(self as *const u8 as isize).checked_add(count).is_some() &&
((self as *const u8 as usize) == (self.wrapping_byte_offset(count) as *const u8 as usize) ||
kani::mem::same_allocation(self, self.wrapping_byte_offset(count))))
)]
#[ensures(|result|
// The resulting pointer should either be unchanged or still point to the same allocation
((self as *const u8 as usize) == (*result as *const u8 as usize)) ||
(kani::mem::same_allocation(self, *result))
)]
pub const unsafe fn byte_offset(self, count: isize) -> Self {
// SAFETY: the caller must uphold the safety contract for `offset`.
unsafe { self.cast::<u8>().offset(count).with_metadata_of(self) }
Expand Down Expand Up @@ -972,6 +993,22 @@ impl<T: ?Sized> *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(
// If the size of the pointee is zero, then `count` must also be zero
(mem::size_of_val_raw(self) == 0 && count == 0) ||
// If the size of the pointee is not zero, then ensure that adding `count`
// bytes doesn't cause overflow and that both pointers `self` and the result
// are pointing to the same address or in the same allocation
(mem::size_of_val_raw(self) != 0 &&
(self as *const u8 as isize).checked_add(count as isize).is_some() &&
((self as *const u8 as usize) == (self.wrapping_byte_add(count) as *const u8 as usize) ||
kani::mem::same_allocation(self, self.wrapping_byte_add(count))))
)]
#[ensures(|result|
// The resulting pointer should either be unchanged or still point to the same allocation
((self as *const u8 as usize) == (*result as *const u8 as usize)) ||
(kani::mem::same_allocation(self, *result))
)]
pub const unsafe fn byte_add(self, count: usize) -> Self {
// SAFETY: the caller must uphold the safety contract for `add`.
unsafe { self.cast::<u8>().add(count).with_metadata_of(self) }
Expand Down Expand Up @@ -1087,6 +1124,22 @@ impl<T: ?Sized> *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(
// If the size of the pointee is zero, then `count` must also be zero
(mem::size_of_val_raw(self) == 0 && count == 0) ||
// If the size of the pointee is not zero then ensure that adding `count`
// bytes doesn't cause overflow and that both pointers `self` and the result
// would be pointing to the same address or in the same allocation
(mem::size_of_val_raw(self) != 0 &&
(self as *const u8 as isize).checked_sub(count as isize).is_some() &&
((self as *const u8 as usize) == (self.wrapping_byte_sub(count) as *const u8 as usize) ||
kani::mem::same_allocation(self, self.wrapping_byte_sub(count))))
)]
#[ensures(|result|
// The resulting pointer should either be unchanged or still point to the same allocation
((self as *const u8 as isize) == (*result as *const u8 as isize)) ||
(kani::mem::same_allocation(self, *result))
)]
pub const unsafe fn byte_sub(self, count: usize) -> Self {
// SAFETY: the caller must uphold the safety contract for `sub`.
unsafe { self.cast::<u8>().sub(count).with_metadata_of(self) }
Expand Down Expand Up @@ -1899,3 +1952,249 @@ impl<T: ?Sized> 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;

// generate proof for contracts of byte_add, byte_sub and byte_offset to verify
// unit pointee type
// - `$fn_name`: function for which the contract must be verified
// - `$proof_name`: name of the harness generated
macro_rules! gen_const_byte_arith_harness_for_unit {
(byte_offset, $proof_name:ident) => {
#[kani::proof_for_contract(<*const ()>::byte_offset)]
pub fn $proof_name() {
let val = ();
let ptr: *const () = &val;
let count: isize = kani::any();
unsafe {
ptr.byte_offset(count);
}
}
};

($fn_name:ident, $proof_name:ident) => {
#[kani::proof_for_contract(<*const ()>::$fn_name)]
pub fn $proof_name() {
let val = ();
let ptr: *const () = &val;
//byte_add and byte_sub need count to be usize unlike byte_offset
let count: usize = kani::any();
unsafe {
ptr.$fn_name(count);
}
}
};
}

gen_const_byte_arith_harness_for_unit!(byte_add, check_const_byte_add_unit);
gen_const_byte_arith_harness_for_unit!(byte_sub, check_const_byte_sub_unit);
gen_const_byte_arith_harness_for_unit!(byte_offset, check_const_byte_offset_unit);

// bounding space for PointerGenerator to accommodate 40 elements.
const ARRAY_LEN: usize = 40;

// generate proof for contracts for byte_add, byte_sub and byte_offset
// - `$type`: pointee type
// - `$fn_name`: function for which the contract must be verified
// - `$proof_name`: name of the harness generated
macro_rules! gen_const_byte_arith_harness {
($type:ty, byte_offset, $proof_name:ident) => {
#[kani::proof_for_contract(<*const $type>::byte_offset)]
pub fn $proof_name() {
// generator with space for single element
let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new();
// generator with space for multiple elements
let mut generator2 =
PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new();

let ptr: *const $type = if kani::any() {
generator1.any_in_bounds().ptr
} else {
generator2.any_in_bounds().ptr
};

let count: isize = kani::any();

unsafe {
ptr.byte_offset(count);
}
}
};

($type:ty, $fn_name:ident, $proof_name:ident) => {
#[kani::proof_for_contract(<*const $type>::$fn_name)]
pub fn $proof_name() {
// generator with space for single element
let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new();
// generator with space for multiple elements
let mut generator2 =
PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new();

let ptr: *const $type = if kani::any() {
generator1.any_in_bounds().ptr
} else {
generator2.any_in_bounds().ptr
};

//byte_add and byte_sub need count to be usize unlike byte_offset
let count: usize = kani::any();

unsafe {
ptr.$fn_name(count);
}
}
};
}

gen_const_byte_arith_harness!(i8, byte_add, check_const_byte_add_i8);
gen_const_byte_arith_harness!(i16, byte_add, check_const_byte_add_i16);
gen_const_byte_arith_harness!(i32, byte_add, check_const_byte_add_i32);
gen_const_byte_arith_harness!(i64, byte_add, check_const_byte_add_i64);
gen_const_byte_arith_harness!(i128, byte_add, check_const_byte_add_i128);
gen_const_byte_arith_harness!(isize, byte_add, check_const_byte_add_isize);
gen_const_byte_arith_harness!(u8, byte_add, check_const_byte_add_u8);
gen_const_byte_arith_harness!(u16, byte_add, check_const_byte_add_u16);
gen_const_byte_arith_harness!(u32, byte_add, check_const_byte_add_u32);
gen_const_byte_arith_harness!(u64, byte_add, check_const_byte_add_u64);
gen_const_byte_arith_harness!(u128, byte_add, check_const_byte_add_u128);
gen_const_byte_arith_harness!(usize, byte_add, check_const_byte_add_usize);
gen_const_byte_arith_harness!((i8, i8), byte_add, check_const_byte_add_tuple_1);
gen_const_byte_arith_harness!((f64, bool), byte_add, check_const_byte_add_tuple_2);
gen_const_byte_arith_harness!((i32, f64, bool), byte_add, check_const_byte_add_tuple_3);
gen_const_byte_arith_harness!(
(i8, u16, i32, u64, isize),
byte_add,
check_const_byte_add_tuple_4
);

gen_const_byte_arith_harness!(i8, byte_sub, check_const_byte_sub_i8);
gen_const_byte_arith_harness!(i16, byte_sub, check_const_byte_sub_i16);
gen_const_byte_arith_harness!(i32, byte_sub, check_const_byte_sub_i32);
gen_const_byte_arith_harness!(i64, byte_sub, check_const_byte_sub_i64);
gen_const_byte_arith_harness!(i128, byte_sub, check_const_byte_sub_i128);
gen_const_byte_arith_harness!(isize, byte_sub, check_const_byte_sub_isize);
gen_const_byte_arith_harness!(u8, byte_sub, check_const_byte_sub_u8);
gen_const_byte_arith_harness!(u16, byte_sub, check_const_byte_sub_u16);
gen_const_byte_arith_harness!(u32, byte_sub, check_const_byte_sub_u32);
gen_const_byte_arith_harness!(u64, byte_sub, check_const_byte_sub_u64);
gen_const_byte_arith_harness!(u128, byte_sub, check_const_byte_sub_u128);
gen_const_byte_arith_harness!(usize, byte_sub, check_const_byte_sub_usize);
gen_const_byte_arith_harness!((i8, i8), byte_sub, check_const_byte_sub_tuple_1);
gen_const_byte_arith_harness!((f64, bool), byte_sub, check_const_byte_sub_tuple_2);
gen_const_byte_arith_harness!((i32, f64, bool), byte_sub, check_const_byte_sub_tuple_3);
gen_const_byte_arith_harness!(
(i8, u16, i32, u64, isize),
byte_sub,
check_const_byte_sub_tuple_4
);

gen_const_byte_arith_harness!(i8, byte_offset, check_const_byte_offset_i8);
gen_const_byte_arith_harness!(i16, byte_offset, check_const_byte_offset_i16);
gen_const_byte_arith_harness!(i32, byte_offset, check_const_byte_offset_i32);
gen_const_byte_arith_harness!(i64, byte_offset, check_const_byte_offset_i64);
gen_const_byte_arith_harness!(i128, byte_offset, check_const_byte_offset_i128);
gen_const_byte_arith_harness!(isize, byte_offset, check_const_byte_offset_isize);
gen_const_byte_arith_harness!(u8, byte_offset, check_const_byte_offset_u8);
gen_const_byte_arith_harness!(u16, byte_offset, check_const_byte_offset_u16);
gen_const_byte_arith_harness!(u32, byte_offset, check_const_byte_offset_u32);
gen_const_byte_arith_harness!(u64, byte_offset, check_const_byte_offset_u64);
gen_const_byte_arith_harness!(u128, byte_offset, check_const_byte_offset_u128);
gen_const_byte_arith_harness!(usize, byte_offset, check_const_byte_offset_usize);
gen_const_byte_arith_harness!((i8, i8), byte_offset, check_const_byte_offset_tuple_1);
gen_const_byte_arith_harness!((f64, bool), byte_offset, check_const_byte_offset_tuple_2);
gen_const_byte_arith_harness!(
(i32, f64, bool),
byte_offset,
check_const_byte_offset_tuple_3
);
gen_const_byte_arith_harness!(
(i8, u16, i32, u64, isize),
byte_offset,
check_const_byte_offset_tuple_4
);

macro_rules! gen_const_byte_arith_harness_for_slice {
($type:ty, byte_offset, $proof_name:ident) => {
#[kani::proof_for_contract(<*const [$type]>::byte_offset)]
pub fn $proof_name() {
let arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array();
let slice: &[$type] = kani::slice::any_slice_of_array(&arr);
let ptr: *const [$type] = slice;

let count: isize = kani::any();

unsafe {
ptr.byte_offset(count);
}
}
};

($type:ty, $fn_name: ident, $proof_name:ident) => {
#[kani::proof_for_contract(<*const [$type]>::$fn_name)]
pub fn $proof_name() {
let arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array();
let slice: &[$type] = kani::slice::any_slice_of_array(&arr);
let ptr: *const [$type] = slice;

//byte_add and byte_sub need count to be usize unlike byte_offset
let count: usize = kani::any();

unsafe {
ptr.$fn_name(count);
}
}
};
}

gen_const_byte_arith_harness_for_slice!(i8, byte_add, check_const_byte_add_i8_slice);
gen_const_byte_arith_harness_for_slice!(i16, byte_add, check_const_byte_add_i16_slice);
gen_const_byte_arith_harness_for_slice!(i32, byte_add, check_const_byte_add_i32_slice);
gen_const_byte_arith_harness_for_slice!(i64, byte_add, check_const_byte_add_i64_slice);
gen_const_byte_arith_harness_for_slice!(i128, byte_add, check_const_byte_add_i128_slice);
gen_const_byte_arith_harness_for_slice!(isize, byte_add, check_const_byte_add_isize_slice);
gen_const_byte_arith_harness_for_slice!(u8, byte_add, check_const_byte_add_u8_slice);
gen_const_byte_arith_harness_for_slice!(u16, byte_add, check_const_byte_add_u16_slice);
gen_const_byte_arith_harness_for_slice!(u32, byte_add, check_const_byte_add_u32_slice);
gen_const_byte_arith_harness_for_slice!(u64, byte_add, check_const_byte_add_u64_slice);
gen_const_byte_arith_harness_for_slice!(u128, byte_add, check_const_byte_add_u128_slice);
gen_const_byte_arith_harness_for_slice!(usize, byte_add, check_const_byte_add_usize_slice);

gen_const_byte_arith_harness_for_slice!(i8, byte_sub, check_const_byte_sub_i8_slice);
gen_const_byte_arith_harness_for_slice!(i16, byte_sub, check_const_byte_sub_i16_slice);
gen_const_byte_arith_harness_for_slice!(i32, byte_sub, check_const_byte_sub_i32_slice);
gen_const_byte_arith_harness_for_slice!(i64, byte_sub, check_const_byte_sub_i64_slice);
gen_const_byte_arith_harness_for_slice!(i128, byte_sub, check_const_byte_sub_i128_slice);
gen_const_byte_arith_harness_for_slice!(isize, byte_sub, check_const_byte_sub_isize_slice);
gen_const_byte_arith_harness_for_slice!(u8, byte_sub, check_const_byte_sub_u8_slice);
gen_const_byte_arith_harness_for_slice!(u16, byte_sub, check_const_byte_sub_u16_slice);
gen_const_byte_arith_harness_for_slice!(u32, byte_sub, check_const_byte_sub_u32_slice);
gen_const_byte_arith_harness_for_slice!(u64, byte_sub, check_const_byte_sub_u64_slice);
gen_const_byte_arith_harness_for_slice!(u128, byte_sub, check_const_byte_sub_u128_slice);
gen_const_byte_arith_harness_for_slice!(usize, byte_sub, check_const_byte_sub_usize_slice);

gen_const_byte_arith_harness_for_slice!(i8, byte_offset, check_const_byte_offset_i8_slice);
gen_const_byte_arith_harness_for_slice!(i16, byte_offset, check_const_byte_offset_i16_slice);
gen_const_byte_arith_harness_for_slice!(i32, byte_offset, check_const_byte_offset_i32_slice);
gen_const_byte_arith_harness_for_slice!(i64, byte_offset, check_const_byte_offset_i64_slice);
gen_const_byte_arith_harness_for_slice!(i128, byte_offset, check_const_byte_offset_i128_slice);
gen_const_byte_arith_harness_for_slice!(
isize,
byte_offset,
check_const_byte_offset_isize_slice
);
gen_const_byte_arith_harness_for_slice!(u8, byte_offset, check_const_byte_offset_u8_slice);
gen_const_byte_arith_harness_for_slice!(u16, byte_offset, check_const_byte_offset_u16_slice);
gen_const_byte_arith_harness_for_slice!(u32, byte_offset, check_const_byte_offset_u32_slice);
gen_const_byte_arith_harness_for_slice!(u64, byte_offset, check_const_byte_offset_u64_slice);
gen_const_byte_arith_harness_for_slice!(u128, byte_offset, check_const_byte_offset_u128_slice);
gen_const_byte_arith_harness_for_slice!(
usize,
byte_offset,
check_const_byte_offset_usize_slice
);
}