From b6552b80c95a9edc7414aa3ff95e7e63f8b0bf97 Mon Sep 17 00:00:00 2001 From: szlee118 <33711285+szlee118@users.noreply.github.com> Date: Tue, 10 Dec 2024 09:57:04 -0800 Subject: [PATCH] Harnesses verifying slice types for add, sub and offset (#179) Towards https://github.com/model-checking/verify-rust-std/issues/76 ## Changes ### Contracts Added: - Added contracts for <*mut T>::add, <*mut T>::sub, and <*mut T>::offset operations for raw pointers to slices. ### Proofs Implemented: - Added proofs for the above contracts, verifying safety for the following slice pointee types using arrays: - All integer types (i8, i16, i32, etc.). - Tuples (composite types) (e.g., (i8, i8), (i32, f64, bool)). - Unit type (()). ### Macro Definitions: - Introduced macros to simplify and automate harness generation: - One macro for add and sub operations on slices. - Another macro for offset operations on slices. ### Array-Based Implementation for Slice Verification: - Arrays are used as a proxy for slices (as slices do not have a known length at compile time) to enable proper bounds checking and assumptions during verification. --- library/core/src/ptr/mut_ptr.rs | 76 +++++++++++++++++++++++++++++++++ 1 file changed, 76 insertions(+) diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 55c8b1b3f5cec..8f3ae4f746b9f 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -2242,6 +2242,82 @@ impl PartialOrd for *mut T { mod verify { use crate::kani; use core::mem; + + // Chosen for simplicity and sufficient size to test edge cases effectively + // Represents the number of elements in the slice or array being tested. + // Doesn't need to be large because all possible values for the slice are explored, + // including edge cases like pointers at the start, middle, and end of the slice. + // Symbolic execution generalizes across all possible elements, regardless of the actual array size. + const ARRAY_SIZE: usize = 5; + + /// This macro generates verification harnesses for the `offset`, `add`, and `sub` + /// pointer operations for a slice type and function name. + macro_rules! generate_mut_slice_harnesses { + ($ty:ty, $offset_fn:ident, $add_fn:ident, $sub_fn:ident) => { + // Generates a harness for the `offset` operation + #[kani::proof_for_contract(<*mut $ty>::offset)] + fn $offset_fn() { + let mut arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array(); + let test_ptr: *mut $ty = arr.as_mut_ptr(); + let offset: usize = kani::any(); + let count: isize = kani::any(); + kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); + let ptr_with_offset: *mut $ty = test_ptr.wrapping_byte_add(offset); + unsafe { + ptr_with_offset.offset(count); + } + } + + // Generates a harness for the `add` operation + #[kani::proof_for_contract(<*mut $ty>::add)] + fn $add_fn() { + let mut arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array(); + let test_ptr: *mut $ty = arr.as_mut_ptr(); + let offset: usize = kani::any(); + let count: usize = kani::any(); + kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); + let ptr_with_offset: *mut $ty = test_ptr.wrapping_byte_add(offset); + unsafe { + ptr_with_offset.add(count); + } + } + + // Generates a harness for the `sub` operation + #[kani::proof_for_contract(<*mut $ty>::sub)] + fn $sub_fn() { + let mut arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array(); + let test_ptr: *mut $ty = arr.as_mut_ptr(); + let offset: usize = kani::any(); + let count: usize = kani::any(); + kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); + let ptr_with_offset: *mut $ty = test_ptr.wrapping_byte_add(offset); + unsafe { + ptr_with_offset.sub(count); + } + } + }; + } + + // Generate pointer harnesses for various types (offset, add, sub) + generate_mut_slice_harnesses!(i8, check_mut_offset_slice_i8, check_mut_add_slice_i8, check_mut_sub_slice_i8); + generate_mut_slice_harnesses!(i16, check_mut_offset_slice_i16, check_mut_add_slice_i16, check_mut_sub_slice_i16); + generate_mut_slice_harnesses!(i32, check_mut_offset_slice_i32, check_mut_add_slice_i32, check_mut_sub_slice_i32); + generate_mut_slice_harnesses!(i64, check_mut_offset_slice_i64, check_mut_add_slice_i64, check_mut_sub_slice_i64); + generate_mut_slice_harnesses!(i128, check_mut_offset_slice_i128, check_mut_add_slice_i128, check_mut_sub_slice_i128); + generate_mut_slice_harnesses!(isize, check_mut_offset_slice_isize, check_mut_add_slice_isize, check_mut_sub_slice_isize); + generate_mut_slice_harnesses!(u8, check_mut_offset_slice_u8, check_mut_add_slice_u8, check_mut_sub_slice_u8); + generate_mut_slice_harnesses!(u16, check_mut_offset_slice_u16, check_mut_add_slice_u16, check_mut_sub_slice_u16); + generate_mut_slice_harnesses!(u32, check_mut_offset_slice_u32, check_mut_add_slice_u32, check_mut_sub_slice_u32); + generate_mut_slice_harnesses!(u64, check_mut_offset_slice_u64, check_mut_add_slice_u64, check_mut_sub_slice_u64); + generate_mut_slice_harnesses!(u128, check_mut_offset_slice_u128, check_mut_add_slice_u128, check_mut_sub_slice_u128); + generate_mut_slice_harnesses!(usize, check_mut_offset_slice_usize, check_mut_add_slice_usize, check_mut_sub_slice_usize); + + // Generate pointer harnesses for tuples (offset, add, sub) + generate_mut_slice_harnesses!((i8, i8), check_mut_offset_slice_tuple_1, check_mut_add_slice_tuple_1, check_mut_sub_slice_tuple_1); + generate_mut_slice_harnesses!((f64, bool), check_mut_offset_slice_tuple_2, check_mut_add_slice_tuple_2, check_mut_sub_slice_tuple_2); + generate_mut_slice_harnesses!((i32, f64, bool), check_mut_offset_slice_tuple_3, check_mut_add_slice_tuple_3, check_mut_sub_slice_tuple_3); + generate_mut_slice_harnesses!((i8, u16, i32, u64, isize), check_mut_offset_slice_tuple_4, check_mut_add_slice_tuple_4, check_mut_sub_slice_tuple_4); + use kani::PointerGenerator; /// This macro generates a single verification harness for the `offset`, `add`, or `sub`