Skip to content

Commit

Permalink
Contracts and Harnesses for core::ptr::byte_offset_from (#186)
Browse files Browse the repository at this point in the history
  • Loading branch information
@stogaru
stogaru authored Dec 8, 2024
1 parent d92a7ea commit 8a0d0ce
Show file tree
Hide file tree
Showing 2 changed files with 407 additions and 3 deletions.
205 changes: 203 additions & 2 deletions library/core/src/ptr/const_ptr.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -730,6 +730,16 @@ 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(
(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() ||
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))]
pub const unsafe fn byte_offset_from<U: ?Sized>(self, origin: *const U) -> isize {
// SAFETY: the caller must uphold the safety contract for `offset_from`.
unsafe { self.cast::<u8>().offset_from(origin.cast::<u8>()) }
Expand Down Expand Up @@ -1940,7 +1950,7 @@ mod verify {
check_const_offset_usize
);

// Generte harnesses for composite types (add, sub, offset)
// Generate harnesses for composite types (add, sub, offset)
generate_arithmetic_harnesses!(
(i8, i8),
check_const_add_tuple_1,
Expand Down Expand Up @@ -2116,6 +2126,17 @@ mod verify {
// PointerGenerator does not support dynamic sized arrays.
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
Expand Down Expand Up @@ -2156,7 +2177,7 @@ mod verify {
};
}

// Proof for unit size will panic as offset_from needs the pointee size to be greater then 0
// Proof for unit size will panic as offset_from needs the pointee size to be greater than 0
#[kani::proof_for_contract(<*const ()>::offset_from)]
#[kani::should_panic]
pub fn check_const_offset_from_unit() {
Expand Down Expand Up @@ -2252,6 +2273,186 @@ mod verify {
check_const_offset_from_tuple_4_arr
);

// 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: () = ();
let src_ptr: *const () = &val;
let dest_ptr: *const () = &val;
unsafe {
dest_ptr.byte_offset_from(src_ptr);
}
}

// 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
#[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::<gen_size>::new();
let mut generator2 = PointerGenerator::<gen_size>::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
);

// 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) => {
#[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);

#[kani::proof_for_contract(<*const ()>::byte_offset)]
#[kani::should_panic]
pub fn check_const_byte_offset_unit_invalid_count() {
Expand Down
Loading

0 comments on commit 8a0d0ce

Please sign in to comment.