Skip to content

Commit

Permalink
Contract and Harnesses for byte_add, byte_sub and byte_offset (#…
Browse files Browse the repository at this point in the history 
…169)

Towards #76

### Changes
* Adds contracts for `<*mut T>::byte_add`, `<*mut T>::byte_sub` and
`<*mut T>::byte_offset`.
* Adds harnesses for the function verifying the following pointee types:
    * All integer types
    * Tuples (composite types)
    * Unit Type
    * Slices
* Accomplishes this using a few macros.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Yifei Wang <[email protected]>
Co-authored-by: Yifei Wang <[email protected]>
  • Loading branch information
@stogaru @xsxszab
3 people authored Dec 5, 2024
1 parent 30c756d commit dd75225
Show file tree
Hide file tree
Showing 2 changed files with 597 additions and 1 deletion.
304 changes: 303 additions & 1 deletion library/core/src/ptr/const_ptr.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ 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 @@ -474,6 +475,20 @@ 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 count is zero, any pointer is valid including null pointer.
(count == 0) ||
// Else if count is not zero, then ensure that adding `count` doesn't cause
// overflow and that both pointers `self` and the result are in the same
// allocation
((self.addr() as isize).checked_add(count).is_some() &&
core::ub_checks::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.addr() == result.addr()) ||
(core::ub_checks::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 @@ -1012,6 +1027,20 @@ 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 count is zero, any pointer is valid including null pointer.
(count == 0) ||
// Else if count is not zero, then ensure that adding `count` doesn't cause
// overflow and that both pointers `self` and the result are in the same
// allocation
((self.addr() as isize).checked_add(count as isize).is_some() &&
core::ub_checks::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.addr() == result.addr()) ||
(core::ub_checks::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 @@ -1142,6 +1171,20 @@ 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 count is zero, any pointer is valid including null pointer.
(count == 0) ||
// Else if count is not zero, then ensure that subtracting `count` doesn't
// cause overflow and that both pointers `self` and the result are in the
// same allocation
((self.addr() as isize).checked_sub(count as isize).is_some() &&
core::ub_checks::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.addr() == result.addr()) ||
(core::ub_checks::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 @@ -2068,7 +2111,9 @@ mod verify {
check_const_offset_slice_tuple_4
);

// Array size bound for kani::any_array for `offset_from` verification
// 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 does not support dynamic sized arrays.
const ARRAY_LEN: usize = 40;

macro_rules! generate_offset_from_harness {
Expand Down Expand Up @@ -2206,4 +2251,261 @@ mod verify {
check_const_offset_from_tuple_4,
check_const_offset_from_tuple_4_arr
);

#[kani::proof_for_contract(<*const ()>::byte_offset)]
#[kani::should_panic]
pub fn check_const_byte_offset_unit_invalid_count() {
let val = ();
let ptr: *const () = &val;
let count: isize = kani::any_where(|&x| x != (mem::size_of::<()>() as isize));
unsafe {
ptr.byte_offset(count);
}
}

#[kani::proof_for_contract(<*const ()>::byte_offset)]
pub fn check_const_byte_offset_cast_unit() {
let mut generator = PointerGenerator::<ARRAY_LEN>::new();
let ptr: *const u8 = generator.any_in_bounds().ptr;
let ptr1: *const () = ptr as *const ();
let count: isize = kani::any();
unsafe {
ptr1.byte_offset(count);
}
}

// 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 = mem::size_of::<()>() as isize;
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 = mem::size_of::<()>();
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);

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

0 comments on commit dd75225

Please sign in to comment.