From 89f56e096f4089a623b284e55eee98943caf474a Mon Sep 17 00:00:00 2001 From: JimmyYang Date: Mon, 21 Oct 2024 22:02:41 -0700 Subject: [PATCH 1/8] complete Alignment and Size Checks --- library/core/src/ptr/non_null.rs | 70 +++++++++++++++++++++++++++++++- 1 file changed, 69 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 4d6e484915dbf..0a888736e0005 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -9,7 +9,7 @@ use crate::slice::{self, SliceIndex}; use crate::ub_checks::assert_unsafe_precondition; use crate::{fmt, hash, intrinsics, ptr}; use safety::{ensures, requires}; - +use crate::{ub_checks}; #[cfg(kani)] use crate::kani; @@ -1301,6 +1301,8 @@ impl NonNull { #[must_use] #[stable(feature = "pointer_is_aligned", since = "1.79.0")] #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")] + #[requires(ub_checks::can_dereference(self.as_ptr()))] + #[kani::ensures(|result: &bool| *result == (self.as_ptr() as usize % core::mem::align_of::() == 0))] // Ensure the returned value is correct for alignment check pub const fn is_aligned(self) -> bool where T: Sized, @@ -1416,6 +1418,8 @@ impl NonNull { #[must_use] #[unstable(feature = "pointer_is_aligned_to", issue = "96284")] #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")] + #[kani::requires(align.is_power_of_two() && align > 0)] // Ensure alignment is a power of two and not zero + #[kani::ensures(|result: &bool| *result == ((self.as_ptr() as *const u8) as usize % align == 0))] // Ensure the returned value is correct based on the given alignment pub const fn is_aligned_to(self, align: usize) -> bool { self.pointer.is_aligned_to(align) } @@ -1471,6 +1475,7 @@ impl NonNull<[T]> { #[rustc_const_stable(feature = "const_slice_ptr_len_nonnull", since = "1.63.0")] #[must_use] #[inline] + #[kani::ensures(|result: &usize| *result >= 0)] pub const fn len(self) -> usize { self.as_ptr().len() } @@ -1489,6 +1494,7 @@ impl NonNull<[T]> { #[rustc_const_stable(feature = "const_slice_ptr_is_empty_nonnull", since = "1.79.0")] #[must_use] #[inline] + #[kani::ensures(|result: &bool| (*result && self.len() == 0) || (!*result && self.len() > 0))] // Ensure the returned value correctly indicates whether the slice is empty pub const fn is_empty(self) -> bool { self.len() == 0 } @@ -1803,4 +1809,66 @@ mod verify { let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() }; let _ = NonNull::new(maybe_null_ptr); } + + #[kani::proof_for_contract(NonNull::len)] + pub fn non_null_check_len() { + const SIZE: usize = 20000; + // Create a non-deterministic array of size SIZE + let arr: [i8; SIZE] = kani::any(); + // Get a raw pointer to the array + let raw_ptr: *const i8 = arr.as_ptr(); + // Create a NonNull slice from the raw pointer + let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(NonNull::new(raw_ptr as *mut i8).unwrap(), SIZE) }; + + // Perform the length check + let len = non_null_slice.len(); + assert!(len == SIZE); + } + + #[kani::proof_for_contract(NonNull::is_empty)] + pub fn non_null_check_is_empty() { + const SIZE: usize = 0; + // Create a non-deterministic array of size SIZE + let arr: [i8; SIZE] = kani::any(); + // Get a raw pointer to the array + let raw_ptr: *const i8 = arr.as_ptr(); + // Create a NonNull slice from the raw pointer + let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(NonNull::new(raw_ptr as *mut i8).unwrap(), SIZE) }; + + // Perform the is_empty check + let is_empty = non_null_slice.is_empty(); + assert!(is_empty); + } + + #[kani::proof_for_contract(NonNull::is_aligned)] + pub fn non_null_slice_is_aligned_check() { + // Create a non-deterministic integer + let mut data: i32 = kani::any(); + // Get a raw pointer to the integer + let raw_ptr: *mut i32 = &mut data; + // NonNull pointer to the integer + let ptr = unsafe { NonNull::new(raw_ptr).unwrap() }; + + // Perform the alignment check + let result = ptr.is_aligned(); + assert!(result); + } + + #[kani::proof_for_contract(NonNull::is_aligned_to)] + pub fn non_null_check_is_aligned_to() { + const SIZE: usize = 10; + const ALIGN: usize = 4; + // Create a non-deterministic array of size SIZE + let arr: [i32; SIZE] = kani::any(); + // Get a raw pointer to the array + let raw_ptr: *mut i32 = arr.as_ptr() as *mut i32; + // Randomize pointer offset within array bounds + let offset = kani::any_where(|x| *x <= SIZE); + // NonNull pointer to the random offset + let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() }; + + // Perform the alignment to check if it matches the given alignment + let result = ptr.is_aligned_to(ALIGN); + assert!(result == (ptr.as_ptr() as usize % ALIGN == 0)); + } } From f6b715aa60bd8e8cccd69b65bc1621d8cee0d796 Mon Sep 17 00:00:00 2001 From: JimmyYang Date: Thu, 31 Oct 2024 08:48:37 -0700 Subject: [PATCH 2/8] change kani:requires to requires --- library/core/src/ptr/non_null.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 0a888736e0005..fa3ac0ae64cad 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1302,7 +1302,7 @@ impl NonNull { #[stable(feature = "pointer_is_aligned", since = "1.79.0")] #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")] #[requires(ub_checks::can_dereference(self.as_ptr()))] - #[kani::ensures(|result: &bool| *result == (self.as_ptr() as usize % core::mem::align_of::() == 0))] // Ensure the returned value is correct for alignment check + #[ensures(|result: &bool| *result == (self.as_ptr() as usize % core::mem::align_of::() == 0))] // Ensure the returned value is correct for alignment check pub const fn is_aligned(self) -> bool where T: Sized, @@ -1418,8 +1418,8 @@ impl NonNull { #[must_use] #[unstable(feature = "pointer_is_aligned_to", issue = "96284")] #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")] - #[kani::requires(align.is_power_of_two() && align > 0)] // Ensure alignment is a power of two and not zero - #[kani::ensures(|result: &bool| *result == ((self.as_ptr() as *const u8) as usize % align == 0))] // Ensure the returned value is correct based on the given alignment + #[requires(align.is_power_of_two() && align > 0)] // Ensure alignment is a power of two and not zero + #[ensures(|result: &bool| *result == ((self.as_ptr() as *const u8) as usize % align == 0))] // Ensure the returned value is correct based on the given alignment pub const fn is_aligned_to(self, align: usize) -> bool { self.pointer.is_aligned_to(align) } @@ -1475,7 +1475,7 @@ impl NonNull<[T]> { #[rustc_const_stable(feature = "const_slice_ptr_len_nonnull", since = "1.63.0")] #[must_use] #[inline] - #[kani::ensures(|result: &usize| *result >= 0)] + #[ensures(|result: &usize| *result >= 0)] pub const fn len(self) -> usize { self.as_ptr().len() } @@ -1494,7 +1494,7 @@ impl NonNull<[T]> { #[rustc_const_stable(feature = "const_slice_ptr_is_empty_nonnull", since = "1.79.0")] #[must_use] #[inline] - #[kani::ensures(|result: &bool| (*result && self.len() == 0) || (!*result && self.len() > 0))] // Ensure the returned value correctly indicates whether the slice is empty + #[ensures(|result: &bool| (*result && self.len() == 0) || (!*result && self.len() > 0))] // Ensure the returned value correctly indicates whether the slice is empty pub const fn is_empty(self) -> bool { self.len() == 0 } From 570bbf30baf26af8815216100b22ad369160620c Mon Sep 17 00:00:00 2001 From: JimmyYang Date: Mon, 11 Nov 2024 10:08:28 -0800 Subject: [PATCH 3/8] modify the len func --- library/core/src/ptr/non_null.rs | 41 +++++++++++++++++++++++--------- 1 file changed, 30 insertions(+), 11 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index fa3ac0ae64cad..bc9e5ff18ac87 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1301,7 +1301,6 @@ impl NonNull { #[must_use] #[stable(feature = "pointer_is_aligned", since = "1.79.0")] #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")] - #[requires(ub_checks::can_dereference(self.as_ptr()))] #[ensures(|result: &bool| *result == (self.as_ptr() as usize % core::mem::align_of::() == 0))] // Ensure the returned value is correct for alignment check pub const fn is_aligned(self) -> bool where @@ -1418,7 +1417,6 @@ impl NonNull { #[must_use] #[unstable(feature = "pointer_is_aligned_to", issue = "96284")] #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")] - #[requires(align.is_power_of_two() && align > 0)] // Ensure alignment is a power of two and not zero #[ensures(|result: &bool| *result == ((self.as_ptr() as *const u8) as usize % align == 0))] // Ensure the returned value is correct based on the given alignment pub const fn is_aligned_to(self, align: usize) -> bool { self.pointer.is_aligned_to(align) @@ -1494,7 +1492,7 @@ impl NonNull<[T]> { #[rustc_const_stable(feature = "const_slice_ptr_is_empty_nonnull", since = "1.79.0")] #[must_use] #[inline] - #[ensures(|result: &bool| (*result && self.len() == 0) || (!*result && self.len() > 0))] // Ensure the returned value correctly indicates whether the slice is empty + #[ensures(|result: &bool| *result == (self.len() == 0))] pub const fn is_empty(self) -> bool { self.len() == 0 } @@ -1792,6 +1790,13 @@ mod verify { use super::*; use crate::ptr::null_mut; + impl kani::Arbitrary for NonNull { + fn any() -> Self { + let ptr: *mut T = kani::any(); + NonNull::new(ptr).expect("Non-null pointer expected") + } + } + // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self #[kani::proof_for_contract(NonNull::new_unchecked)] pub fn non_null_check_new_unchecked() { @@ -1810,19 +1815,33 @@ mod verify { let _ = NonNull::new(maybe_null_ptr); } + // #[kani::proof_for_contract(NonNull::len)] + // pub fn non_null_check_len() { + // const SIZE: usize = 20000; + // // Create a non-deterministic array of size SIZE + // let arr: [i8; SIZE] = kani::any(); + // // Get a raw pointer to the array + // let raw_ptr: *const i8 = arr.as_ptr(); + // // Create a NonNull slice from the raw pointer + // let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(NonNull::new(raw_ptr as *mut i8).unwrap(), SIZE) }; + + // // Perform the length check + // let len = non_null_slice.len(); + // assert!(len == SIZE); + // } + #[kani::proof_for_contract(NonNull::len)] pub fn non_null_check_len() { - const SIZE: usize = 20000; - // Create a non-deterministic array of size SIZE - let arr: [i8; SIZE] = kani::any(); - // Get a raw pointer to the array - let raw_ptr: *const i8 = arr.as_ptr(); - // Create a NonNull slice from the raw pointer - let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(NonNull::new(raw_ptr as *mut i8).unwrap(), SIZE) }; + // Create a non-deterministic NonNull pointer using kani::any() + let non_null_ptr: NonNull = kani::any(); + // Create a non-deterministic size using kani::any() + let size: usize = kani::any(); + // Create a NonNull slice from the non-null pointer and size + let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(non_null_ptr, size) }; // Perform the length check let len = non_null_slice.len(); - assert!(len == SIZE); + assert!(len == size); } #[kani::proof_for_contract(NonNull::is_empty)] From 21491e80f80d33cbf3dd60288b4955a8237afafa Mon Sep 17 00:00:00 2001 From: JimmyYang Date: Tue, 12 Nov 2024 10:24:51 -0800 Subject: [PATCH 4/8] fix the len problem --- library/core/src/ptr/non_null.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index bc9e5ff18ac87..f737e5ef3c6c9 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1792,7 +1792,8 @@ mod verify { impl kani::Arbitrary for NonNull { fn any() -> Self { - let ptr: *mut T = kani::any(); + let ptr: *mut T = kani::any::() as *mut T; + kani::assume(!ptr.is_null()); NonNull::new(ptr).expect("Non-null pointer expected") } } From 06cf552bf0f478e2d61b93b541feb2aba07b2200 Mon Sep 17 00:00:00 2001 From: JimmyYang Date: Wed, 13 Nov 2024 23:03:55 -0800 Subject: [PATCH 5/8] improve the proof based on the suggestions --- library/core/src/ptr/non_null.rs | 31 +++++++------------------------ 1 file changed, 7 insertions(+), 24 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index f737e5ef3c6c9..8d02ae329c60b 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1301,7 +1301,7 @@ impl NonNull { #[must_use] #[stable(feature = "pointer_is_aligned", since = "1.79.0")] #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")] - #[ensures(|result: &bool| *result == (self.as_ptr() as usize % core::mem::align_of::() == 0))] // Ensure the returned value is correct for alignment check + #[ensures(|result: &bool| *result == (self.as_ptr().addr() % core::mem::align_of::() == 0))] pub const fn is_aligned(self) -> bool where T: Sized, @@ -1417,7 +1417,8 @@ impl NonNull { #[must_use] #[unstable(feature = "pointer_is_aligned_to", issue = "96284")] #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")] - #[ensures(|result: &bool| *result == ((self.as_ptr() as *const u8) as usize % align == 0))] // Ensure the returned value is correct based on the given alignment + #[requires(align.is_power_of_two())] + #[ensures(|result: &bool| *result == (self.as_ptr().addr() % align == 0))] // Ensure the returned value is correct based on the given alignment pub const fn is_aligned_to(self, align: usize) -> bool { self.pointer.is_aligned_to(align) } @@ -1473,7 +1474,6 @@ impl NonNull<[T]> { #[rustc_const_stable(feature = "const_slice_ptr_len_nonnull", since = "1.63.0")] #[must_use] #[inline] - #[ensures(|result: &usize| *result >= 0)] pub const fn len(self) -> usize { self.as_ptr().len() } @@ -1492,7 +1492,6 @@ impl NonNull<[T]> { #[rustc_const_stable(feature = "const_slice_ptr_is_empty_nonnull", since = "1.79.0")] #[must_use] #[inline] - #[ensures(|result: &bool| *result == (self.len() == 0))] pub const fn is_empty(self) -> bool { self.len() == 0 } @@ -1816,36 +1815,21 @@ mod verify { let _ = NonNull::new(maybe_null_ptr); } - // #[kani::proof_for_contract(NonNull::len)] - // pub fn non_null_check_len() { - // const SIZE: usize = 20000; - // // Create a non-deterministic array of size SIZE - // let arr: [i8; SIZE] = kani::any(); - // // Get a raw pointer to the array - // let raw_ptr: *const i8 = arr.as_ptr(); - // // Create a NonNull slice from the raw pointer - // let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(NonNull::new(raw_ptr as *mut i8).unwrap(), SIZE) }; - - // // Perform the length check - // let len = non_null_slice.len(); - // assert!(len == SIZE); - // } - - #[kani::proof_for_contract(NonNull::len)] + #[kani::proof] pub fn non_null_check_len() { // Create a non-deterministic NonNull pointer using kani::any() let non_null_ptr: NonNull = kani::any(); // Create a non-deterministic size using kani::any() let size: usize = kani::any(); // Create a NonNull slice from the non-null pointer and size - let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(non_null_ptr, size) }; + let non_null_slice: NonNull<[i8]> = NonNull::slice_from_raw_parts(non_null_ptr, size); // Perform the length check let len = non_null_slice.len(); assert!(len == size); } - #[kani::proof_for_contract(NonNull::is_empty)] + #[kani::proof] pub fn non_null_check_is_empty() { const SIZE: usize = 0; // Create a non-deterministic array of size SIZE @@ -1871,7 +1855,6 @@ mod verify { // Perform the alignment check let result = ptr.is_aligned(); - assert!(result); } #[kani::proof_for_contract(NonNull::is_aligned_to)] @@ -1889,6 +1872,6 @@ mod verify { // Perform the alignment to check if it matches the given alignment let result = ptr.is_aligned_to(ALIGN); - assert!(result == (ptr.as_ptr() as usize % ALIGN == 0)); + } } From 30d63fe5420ddf5d6b10adecf25c805bbc2f78ca Mon Sep 17 00:00:00 2001 From: JimmyYang Date: Sat, 16 Nov 2024 22:11:43 -0800 Subject: [PATCH 6/8] refine the proof based on the suggestions --- library/core/src/ptr/non_null.rs | 49 ++++++++++++++------------------ 1 file changed, 21 insertions(+), 28 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 8d02ae329c60b..032961b1d3f4d 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1831,13 +1831,13 @@ mod verify { #[kani::proof] pub fn non_null_check_is_empty() { - const SIZE: usize = 0; - // Create a non-deterministic array of size SIZE - let arr: [i8; SIZE] = kani::any(); - // Get a raw pointer to the array - let raw_ptr: *const i8 = arr.as_ptr(); - // Create a NonNull slice from the raw pointer - let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(NonNull::new(raw_ptr as *mut i8).unwrap(), SIZE) }; + // Create a non-deterministic NonNull pointer using kani::any() + let non_null_ptr: NonNull = kani::any(); + // Create a non-deterministic size using kani::any(), constrained to zero + let size: usize = 0; + + // Create a NonNull slice from the non-null pointer and size + let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(non_null_ptr, size) }; // Perform the is_empty check let is_empty = non_null_slice.is_empty(); @@ -1846,32 +1846,25 @@ mod verify { #[kani::proof_for_contract(NonNull::is_aligned)] pub fn non_null_slice_is_aligned_check() { - // Create a non-deterministic integer - let mut data: i32 = kani::any(); - // Get a raw pointer to the integer - let raw_ptr: *mut i32 = &mut data; - // NonNull pointer to the integer - let ptr = unsafe { NonNull::new(raw_ptr).unwrap() }; + // Create a non-deterministic NonNull pointer using kani::any() + let non_null_ptr: NonNull = kani::any(); // Perform the alignment check - let result = ptr.is_aligned(); + let result = non_null_ptr.is_aligned(); + } #[kani::proof_for_contract(NonNull::is_aligned_to)] pub fn non_null_check_is_aligned_to() { - const SIZE: usize = 10; - const ALIGN: usize = 4; - // Create a non-deterministic array of size SIZE - let arr: [i32; SIZE] = kani::any(); - // Get a raw pointer to the array - let raw_ptr: *mut i32 = arr.as_ptr() as *mut i32; - // Randomize pointer offset within array bounds - let offset = kani::any_where(|x| *x <= SIZE); - // NonNull pointer to the random offset - let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() }; - - // Perform the alignment to check if it matches the given alignment - let result = ptr.is_aligned_to(ALIGN); - + // Create a non-deterministic NonNull pointer using kani::any() + let non_null_ptr: NonNull = kani::any(); + + // Create a non-deterministic alignment using kani::any() + let align: usize = kani::any(); + kani::assume(align > 0); // Ensure alignment is greater than zero + + // Perform the alignment check + let result = non_null_ptr.is_aligned_to(align); + } } From bc5dc9e6e2e09a01aa0a9511fe7da99a4ac47463 Mon Sep 17 00:00:00 2001 From: JimmyYang Date: Tue, 19 Nov 2024 16:22:30 -0800 Subject: [PATCH 7/8] refine the code based on suggestions --- library/core/src/ptr/non_null.rs | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 032961b1d3f4d..cba1faa158559 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1867,4 +1867,18 @@ mod verify { let result = non_null_ptr.is_aligned_to(align); } + + #[kani::proof] + #[kani::should_panic] // Add this if we expect a panic when the alignment is invalid + pub fn non_null_check_is_aligned_to_no_power_two() { + // Create a non-deterministic NonNull pointer using kani::any() + let non_null_ptr: NonNull = kani::any(); + + // Create a non-deterministic alignment value using kani::any() + let align: usize = kani::any(); + + // Perform the alignment check + let result = non_null_ptr.is_aligned_to(align); + + } } From 9e9d50e3c8e7e95a00e3433413301cc279f089da Mon Sep 17 00:00:00 2001 From: JY <53210261+Jimmycreative@users.noreply.github.com> Date: Fri, 22 Nov 2024 09:51:02 -0800 Subject: [PATCH 8/8] Update library/core/src/ptr/non_null.rs Co-authored-by: Carolyn Zech --- library/core/src/ptr/non_null.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index cba1faa158559..3bc84601b4448 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -9,7 +9,7 @@ use crate::slice::{self, SliceIndex}; use crate::ub_checks::assert_unsafe_precondition; use crate::{fmt, hash, intrinsics, ptr}; use safety::{ensures, requires}; -use crate::{ub_checks}; +use crate::ub_checks; #[cfg(kani)] use crate::kani;