diff --git a/doc/src/challenges/0006-nonnull.md b/doc/src/challenges/0006-nonnull.md index 86cb8366a36a2..4b1b73b75ccf5 100644 --- a/doc/src/challenges/0006-nonnull.md +++ b/doc/src/challenges/0006-nonnull.md @@ -1,11 +1,11 @@ # Challenge 6: Safety of NonNull -- **Status:** Open +- **Status:** Resolved - **Tracking Issue:** [#53](https://github.com/model-checking/verify-rust-std/issues/53) - **Start date:** *2024/08/16* - **End date:** *2025/04/10* - **Reward:** *N/A* - +- **Contributors**: [Quinyuan Wu](https://github.com/QinyuanWu), [Daniel Tu](https://github.com/danielhumanmod), [Dhvani Kapadia](https://github.com/Dhvani-Kapadia) and [Jiun Chi Yang](https://github.com/Jimmycreative) ------------------- diff --git a/doc/src/challenges/0008-smallsort.md b/doc/src/challenges/0008-smallsort.md index 1052031506517..ea4e90caa94dc 100644 --- a/doc/src/challenges/0008-smallsort.md +++ b/doc/src/challenges/0008-smallsort.md @@ -11,8 +11,7 @@ ## Goal -The implementations of the traits `StableSmallSortTypeImpl`, `UnstableSmallSortTypeImpl`, and `UnstableSmallSortFreezeTypeImpl` in the `smallsort` [module](https://github.com/rust-lang/rust/blob/master/library/core/src/slice/sort/shared/smallsort.rs) of the Rust standard library are the sorting -algorithms optimized for slices with small lengths. +The implementations of the traits `StableSmallSortTypeImpl`, `UnstableSmallSortTypeImpl`, and `UnstableSmallSortFreezeTypeImpl` in the `smallsort` [module](https://github.com/rust-lang/rust/blob/master/library/core/src/slice/sort/shared/smallsort.rs) of the Rust standard library are the sorting algorithms with optimized implementations for slices with small lengths. In this challenge, the goal is to, first prove the memory safety of the public functions in the `smallsort` module, and, second, write contracts for them to show that the sorting algorithms actually sort the slices. diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md index d5252cd939da7..7a42360bca183 100644 --- a/doc/src/challenges/0012-nonzero.md +++ b/doc/src/challenges/0012-nonzero.md @@ -73,7 +73,6 @@ Verify the safety of the following functions and methods (all located within `co | `from_mut` | | `from_mut_unchecked` | -You are not required to write correctness contracts for these methods (e.g., for `max`, ensuring that the `result` is indeed the maximum of the inputs), but it would be great to do so! ### List of UBs diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md index e6dc78666718d..fb15d0395bff2 100644 --- a/doc/src/challenges/0014-convert-num.md +++ b/doc/src/challenges/0014-convert-num.md @@ -1,11 +1,11 @@ # Challenge 14: Safety of Primitive Conversions -- **Status:** Open +- **Status:** Resolved - **Tracking Issue:** https://github.com/model-checking/verify-rust-std/issues/220 - **Start date:** 2024/12/15 - **End date:** 2025/2/28 - **Prize:** *TBD* - +- **Contributors**: [Shoyu Vanilla](https://github.com/ShoyuVanilla) ------------------- ## Goal diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index d2ffae1082495..625db457f5261 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1213,6 +1213,8 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")] + #[cfg_attr(kani, kani::modifies(self.as_ptr()))] + #[requires(ub_checks::can_write(self.as_ptr()))] pub const unsafe fn write(self, val: T) where T: Sized, @@ -1232,6 +1234,13 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")] + #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(self.as_ptr(), count)))] + #[requires( + count.checked_mul(core::mem::size_of::() as usize).is_some_and(|byte_count| byte_count.wrapping_add(self.as_ptr() as usize) <= isize::MAX as usize) && + ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(self.as_ptr(), count)) + )] + #[ensures(|_| + ub_checks::can_dereference(crate::ptr::slice_from_raw_parts(self.as_ptr() as *const u8, count * size_of::())))] pub const unsafe fn write_bytes(self, val: u8, count: usize) where T: Sized, @@ -1275,6 +1284,8 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")] + #[cfg_attr(kani, kani::modifies(self.as_ptr()))] + #[requires(ub_checks::can_write_unaligned(self.as_ptr()))] pub const unsafe fn write_unaligned(self, val: T) where T: Sized, @@ -2535,12 +2546,143 @@ mod verify { } } + macro_rules! generate_write_harness { + ($type:ty, $harness_name:ident) => { + #[kani::proof_for_contract(NonNull::write)] + pub fn $harness_name() { + // Create a pointer generator for the given type with appropriate byte size + const ARR_SIZE: usize = mem::size_of::<$type>() * 100; + let mut generator = kani::PointerGenerator::::new(); + + // Get a raw pointer from the generator + let raw_ptr: *mut $type = generator.any_in_bounds().ptr; + + // Create a non-null pointer from the raw pointer + let ptr = NonNull::new(raw_ptr).unwrap(); + + // Create a non-deterministic value to write + let new_value: $type = kani::any(); + + unsafe { + // Perform the volatile write operation + ptr.write(new_value); + + // Read back the value and assert it's correct + assert_eq!(ptr.as_ptr().read(), new_value); + } + } + }; + } + + #[kani::proof_for_contract(NonNull::write)] + pub fn non_null_check_write_unit() { + // Create a pointer generator for the given type with appropriate byte size + let mut generator = kani::PointerGenerator::<1>::new(); + + // Get a raw pointer from the generator + let raw_ptr: *mut () = generator.any_in_bounds().ptr; + + // Create a non-null pointer from the raw pointer + let ptr = NonNull::new(raw_ptr).unwrap(); + + // Create a non-deterministic value to write + let new_value: () = kani::any(); + + unsafe { + // Perform the volatile write operation + ptr.write(new_value); + + // Read back the value and assert it's correct + assert_eq!(ptr.as_ptr().read(), new_value); + } + } + + // Generate proof harnesses for multiple types with appropriate byte sizes + generate_write_harness!(i8, non_null_check_write_i8); + generate_write_harness!(i16, non_null_check_write_i16); + generate_write_harness!(i32, non_null_check_write_i32); + generate_write_harness!(i64, non_null_check_write_i64); + generate_write_harness!(i128, non_null_check_write_i128); + generate_write_harness!(isize, non_null_check_write_isize); + generate_write_harness!(u8, non_null_check_write_u8); + generate_write_harness!(u16, non_null_check_write_u16); + generate_write_harness!(u32, non_null_check_write_u32); + generate_write_harness!(u64, non_null_check_write_u64); + generate_write_harness!(u128, non_null_check_write_u128); + generate_write_harness!(usize, non_null_check_write_usize); + + macro_rules! generate_write_unaligned_harness { + ($type:ty, $harness_name:ident) => { + #[kani::proof_for_contract(NonNull::write_unaligned)] + pub fn $harness_name() { + // Create a pointer generator for the given type with appropriate byte size + const ARR_SIZE: usize = mem::size_of::<$type>() * 100; + let mut generator = kani::PointerGenerator::::new(); + + // Get a raw pointer from the generator + let raw_ptr: *mut $type = generator.any_in_bounds().ptr; + + // Create a non-null pointer from the raw pointer + let ptr = NonNull::new(raw_ptr).unwrap(); + + // Create a non-deterministic value to write + let new_value: $type = kani::any(); + + unsafe { + // Perform the volatile write operation + ptr.write_unaligned(new_value); + + // Read back the value and assert it's correct + assert_eq!(ptr.as_ptr().read_unaligned(), new_value); + } + } + }; + } + + #[kani::proof_for_contract(NonNull::write_unaligned)] + pub fn non_null_check_write_unaligned_unit() { + // Create a pointer generator for the given type with appropriate byte size + let mut generator = kani::PointerGenerator::<1>::new(); + + // Get a raw pointer from the generator + let raw_ptr: *mut () = generator.any_in_bounds().ptr; + + // Create a non-null pointer from the raw pointer + let ptr = NonNull::new(raw_ptr).unwrap(); + + // Create a non-deterministic value to write + let new_value: () = kani::any(); + + unsafe { + // Perform the volatile write operation + ptr.write_unaligned(new_value); + + // Read back the value and assert it's correct + assert_eq!(ptr.as_ptr().read_unaligned(), new_value); + } + } + + // Generate proof harnesses for multiple types with appropriate byte sizes + generate_write_unaligned_harness!(i8, non_null_check_write_unaligned_i8); + generate_write_unaligned_harness!(i16, non_null_check_write_unaligned_i16); + generate_write_unaligned_harness!(i32, non_null_check_write_unaligned_i32); + generate_write_unaligned_harness!(i64, non_null_check_write_unaligned_i64); + generate_write_unaligned_harness!(i128, non_null_check_write_unaligned_i128); + generate_write_unaligned_harness!(isize, non_null_check_write_unaligned_isize); + generate_write_unaligned_harness!(u8, non_null_check_write_unaligned_u8); + generate_write_unaligned_harness!(u16, non_null_check_write_unaligned_u16); + generate_write_unaligned_harness!(u32, non_null_check_write_unaligned_u32); + generate_write_unaligned_harness!(u64, non_null_check_write_unaligned_u64); + generate_write_unaligned_harness!(u128, non_null_check_write_unaligned_u128); + generate_write_unaligned_harness!(usize, non_null_check_write_unaligned_usize); + macro_rules! generate_write_volatile_harness { - ($type:ty, $byte_size:expr, $harness_name:ident) => { + ($type:ty, $harness_name:ident) => { #[kani::proof_for_contract(NonNull::write_volatile)] pub fn $harness_name() { // Create a pointer generator for the given type with appropriate byte size - let mut generator = kani::PointerGenerator::<$byte_size>::new(); + const ARR_SIZE: usize = mem::size_of::<$type>() * 100; + let mut generator = kani::PointerGenerator::::new(); // Get a raw pointer from the generator let raw_ptr: *mut $type = generator.any_in_bounds().ptr; @@ -2562,28 +2704,114 @@ mod verify { }; } + #[kani::proof_for_contract(NonNull::write_volatile)] + pub fn non_null_check_write_volatile_unit() { + // Create a pointer generator for the given type with appropriate byte size + let mut generator = kani::PointerGenerator::<1>::new(); + + // Get a raw pointer from the generator + let raw_ptr: *mut () = generator.any_in_bounds().ptr; + + // Create a non-null pointer from the raw pointer + let ptr = NonNull::new(raw_ptr).unwrap(); + + // Create a non-deterministic value to write + let new_value: () = kani::any(); + + unsafe { + // Perform the volatile write operation + ptr.write_volatile(new_value); + + // Read back the value and assert it's correct + assert_eq!(ptr.as_ptr().read_volatile(), new_value); + } + } + + // Generate proof harnesses for multiple types with appropriate byte sizes + generate_write_volatile_harness!(i8, non_null_check_write_volatile_i8); + generate_write_volatile_harness!(i16, non_null_check_write_volatile_i16); + generate_write_volatile_harness!(i32, non_null_check_write_volatile_i32); + generate_write_volatile_harness!(i64, non_null_check_write_volatile_i64); + generate_write_volatile_harness!(i128, non_null_check_write_volatile_i128); + generate_write_volatile_harness!(isize, non_null_check_write_volatile_isize); + generate_write_volatile_harness!(u8, non_null_check_write_volatile_u8); + generate_write_volatile_harness!(u16, non_null_check_write_volatile_u16); + generate_write_volatile_harness!(u32, non_null_check_write_volatile_u32); + generate_write_volatile_harness!(u64, non_null_check_write_volatile_u64); + generate_write_volatile_harness!(u128, non_null_check_write_volatile_u128); + generate_write_volatile_harness!(usize, non_null_check_write_volatile_usize); + + macro_rules! generate_write_bytes_harness { + ($type:ty, $harness_name:ident) => { + #[kani::proof_for_contract(NonNull::write_bytes)] + pub fn $harness_name() { + // Create a pointer generator for the given type with appropriate byte size + const ARR_SIZE: usize = mem::size_of::<$type>() * 10; + let mut generator = kani::PointerGenerator::::new(); + + // Get a raw pointer from the generator + let raw_ptr: *mut $type = generator.any_in_bounds().ptr; + + // Create a non-null pointer from the raw pointer + let ptr = NonNull::new(raw_ptr).unwrap(); + + // Create a non-deterministic value to write + let val: u8 = kani::any(); + + // Create a non-deterministic count + let count: usize = kani::any(); + + unsafe { + // Perform the volatile write operation + ptr.write_bytes(val, count); + + // Create a non-deterministic count + let i: usize = kani::any_where(|&x| x < count * mem::size_of::<$type>()); + let ptr_byte = ptr.as_ptr() as *const u8; + + // Read back the value and assert it's correct + assert_eq!(*ptr_byte.add(i), val); + } + } + }; + } + + #[kani::proof_for_contract(NonNull::write_bytes)] + pub fn non_null_check_write_bytes_unit() { + // Create a pointer generator for the given type with appropriate byte size + let mut generator = kani::PointerGenerator::<1>::new(); + + // Get a raw pointer from the generator + let raw_ptr: *mut () = generator.any_in_bounds().ptr; + + // Create a non-null pointer from the raw pointer + let ptr = NonNull::new(raw_ptr).unwrap(); + + // Create a non-deterministic value to write + let val: u8 = kani::any(); + + // Create a non-deterministic count + let count: usize = kani::any(); + + unsafe { + // Perform the volatile write operation + ptr.write_bytes(val, count); + } + } + // Generate proof harnesses for multiple types with appropriate byte sizes - generate_write_volatile_harness!(i8, 1, non_null_check_write_volatile_i8); - generate_write_volatile_harness!(i16, 2, non_null_check_write_volatile_i16); - generate_write_volatile_harness!(i32, 4, non_null_check_write_volatile_i32); - generate_write_volatile_harness!(i64, 8, non_null_check_write_volatile_i64); - generate_write_volatile_harness!(i128, 16, non_null_check_write_volatile_i128); - generate_write_volatile_harness!( - isize, - { core::mem::size_of::() }, - non_null_check_write_volatile_isize - ); - generate_write_volatile_harness!(u8, 1, non_null_check_write_volatile_u8); - generate_write_volatile_harness!(u16, 2, non_null_check_write_volatile_u16); - generate_write_volatile_harness!(u32, 4, non_null_check_write_volatile_u32); - generate_write_volatile_harness!(u64, 8, non_null_check_write_volatile_u64); - generate_write_volatile_harness!(u128, 16, non_null_check_write_volatile_u128); - generate_write_volatile_harness!( - usize, - { core::mem::size_of::() }, - non_null_check_write_volatile_usize - ); - generate_write_volatile_harness!((), 1, non_null_check_write_volatile_unit); + generate_write_bytes_harness!(i8, non_null_check_write_bytes_i8); + generate_write_bytes_harness!(i16, non_null_check_write_bytes_i16); + generate_write_bytes_harness!(i32, non_null_check_write_bytes_i32); + generate_write_bytes_harness!(i64, non_null_check_write_bytes_i64); + generate_write_bytes_harness!(i128, non_null_check_write_bytes_i128); + generate_write_bytes_harness!(isize, non_null_check_write_bytes_isize); + generate_write_bytes_harness!(u8, non_null_check_write_bytes_u8); + generate_write_bytes_harness!(u16, non_null_check_write_bytes_u16); + generate_write_bytes_harness!(u32, non_null_check_write_bytes_u32); + generate_write_bytes_harness!(u64, non_null_check_write_bytes_u64); + generate_write_bytes_harness!(u128, non_null_check_write_bytes_u128); + generate_write_bytes_harness!(usize, non_null_check_write_bytes_usize); #[kani::proof_for_contract(NonNull::byte_add)] pub fn non_null_byte_add_proof() {