From 9c8905e5508ed1b991887922625da4c02aa5f0eb Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Wed, 2 Oct 2024 16:34:28 -0700 Subject: [PATCH 01/19] contract and harness for add --- library/core/src/ptr/non_null.rs | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 4d6e484915dbf..350be00271a1e 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -552,6 +552,9 @@ impl NonNull { #[must_use = "returns a new pointer rather than modifying its argument"] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] + #[requires(count.checked_mul(core::mem::size_of::()).is_some())] // Prevent offset overflow + #[requires(count * core::mem::size_of::() <= isize::MAX as usize)] // SAFETY: count * size_of::() does not overflow isize + #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(count as isize))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -1803,4 +1806,28 @@ mod verify { let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() }; let _ = NonNull::new(maybe_null_ptr); } + + // pub const unsafe fn add(self, count: usize) -> Self + #[kani::proof_for_contract(NonNull::add)] + pub fn non_null_check_add() { + const SIZE: usize = 10; + // Randomiz pointer offset within array bound + let offset = kani::any_where(|x| *x < SIZE); + // Create a non-deterministic array of size SIZE + let arr: [i8; SIZE] = kani::any(); + // Get a raw pointer to the array + let raw_ptr: *mut i8 = arr.as_ptr() as *mut i8; + // NonNUll pointer to the random offset + let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() }; + // Create a non-deterministic count value + let count: usize = kani::any(); + + // SAFETY: Ensure that the pointer operation does not go out of the bounds of the array + //kani::assume(count < SIZE - offset); + + unsafe { + // Add a positive offset to pointer + let result = ptr.add(count); + } + } } From 5ea1ddc600bf893cb77e1af43ecb75c0f9081302 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Wed, 2 Oct 2024 17:05:42 -0700 Subject: [PATCH 02/19] add contract and harness to addr --- library/core/src/ptr/non_null.rs | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 350be00271a1e..e9eb817bcf621 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -279,6 +279,8 @@ impl NonNull { #[must_use] #[inline] #[unstable(feature = "strict_provenance", issue = "95228")] + #[requires(!self.as_ptr().is_null())] + #[ensures(|result| result.get() != 0)] pub fn addr(self) -> NonZero { // SAFETY: The pointer is guaranteed by the type to be non-null, // meaning that the address will be non-zero. @@ -1818,7 +1820,7 @@ mod verify { // Get a raw pointer to the array let raw_ptr: *mut i8 = arr.as_ptr() as *mut i8; // NonNUll pointer to the random offset - let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap() }; + let ptr = NonNull::new(raw_ptr.add(offset)).unwrap(); // Create a non-deterministic count value let count: usize = kani::any(); @@ -1830,4 +1832,13 @@ mod verify { let result = ptr.add(count); } } + + // pub const unsafe fn addr(self) -> NonZero + #[kani::proof_for_contract(NonNull::addr)] + pub fn non_null_check_addr() { + let mut x: i32 = kani::any(); + let xptr = &mut x as *mut i32; + let nonnull_xptr = NonNull::new(xptr); + let address = nonnull_xptr.addr(); + } } From ca6813f0a944d6282e01977bef8c3123e77f4a2b Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Wed, 2 Oct 2024 17:40:30 -0700 Subject: [PATCH 03/19] use can_write --- library/core/src/ptr/non_null.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index e9eb817bcf621..789518ebd1e25 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -9,6 +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)] @@ -556,6 +557,7 @@ impl NonNull { #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] #[requires(count.checked_mul(core::mem::size_of::()).is_some())] // Prevent offset overflow #[requires(count * core::mem::size_of::() <= isize::MAX as usize)] // SAFETY: count * size_of::() does not overflow isize + #[requires(ub_checks::can_write(self.as_ptr()))] #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(count as isize))] pub const unsafe fn add(self, count: usize) -> Self where @@ -1820,7 +1822,7 @@ mod verify { // Get a raw pointer to the array let raw_ptr: *mut i8 = arr.as_ptr() as *mut i8; // NonNUll pointer to the random offset - let ptr = NonNull::new(raw_ptr.add(offset)).unwrap(); + let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap()}; // Create a non-deterministic count value let count: usize = kani::any(); @@ -1838,7 +1840,7 @@ mod verify { pub fn non_null_check_addr() { let mut x: i32 = kani::any(); let xptr = &mut x as *mut i32; - let nonnull_xptr = NonNull::new(xptr); + let nonnull_xptr = NonNull::new(xptr).unwrap(); let address = nonnull_xptr.addr(); } } From 2c0dcbe851390a8e2fe2ecd2b7d704575505632c Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Wed, 2 Oct 2024 23:30:54 -0700 Subject: [PATCH 04/19] add harness for align_offset --- library/core/src/ptr/non_null.rs | 46 ++++++++++++++++++++++++++++---- 1 file changed, 41 insertions(+), 5 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 789518ebd1e25..a80c3c5950ced 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -9,7 +9,6 @@ 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)] @@ -557,7 +556,7 @@ impl NonNull { #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] #[requires(count.checked_mul(core::mem::size_of::()).is_some())] // Prevent offset overflow #[requires(count * core::mem::size_of::() <= isize::MAX as usize)] // SAFETY: count * size_of::() does not overflow isize - #[requires(ub_checks::can_write(self.as_ptr()))] + #[requires(ub_checks::can_write(self.as_ptr().offset(count as isize)))] #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(count as isize))] pub const unsafe fn add(self, count: usize) -> Self where @@ -1792,6 +1791,8 @@ impl From<&T> for NonNull { mod verify { use super::*; use crate::ptr::null_mut; + use crate::ub_checks; + use crate::mem::align_of; // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self #[kani::proof_for_contract(NonNull::new_unchecked)] @@ -1802,7 +1803,7 @@ mod verify { } } - // pub const unsafe fn new(ptr: *mut T) -> Option + // pub const fn new(ptr: *mut T) -> Option #[kani::proof_for_contract(NonNull::new)] pub fn non_null_check_new() { let mut x: i32 = kani::any(); @@ -1814,7 +1815,7 @@ mod verify { // pub const unsafe fn add(self, count: usize) -> Self #[kani::proof_for_contract(NonNull::add)] pub fn non_null_check_add() { - const SIZE: usize = 10; + const SIZE: usize = 100000; // Randomiz pointer offset within array bound let offset = kani::any_where(|x| *x < SIZE); // Create a non-deterministic array of size SIZE @@ -1835,7 +1836,7 @@ mod verify { } } - // pub const unsafe fn addr(self) -> NonZero + // pub fn addr(self) -> NonZero #[kani::proof_for_contract(NonNull::addr)] pub fn non_null_check_addr() { let mut x: i32 = kani::any(); @@ -1843,4 +1844,39 @@ mod verify { let nonnull_xptr = NonNull::new(xptr).unwrap(); let address = nonnull_xptr.addr(); } + + // pub fn align_offset(self, align: usize) -> usize + #[kani::proof_for_contract(NonNull::align_offset)] + pub fn non_null_check_align_offset() { + const SIZE: usize = 10; + // Non-deterministic input array of i8 (signed 8-bit integers) + let x: [i8; SIZE] = kani::any(); + + // Non-null pointer to the start of the array + let ptr = NonNull::new(x.as_ptr() as *mut i8).unwrap(); + + // Calculate the offset needed to align the pointer to u16 alignment + let offset = ptr.align_offset(align_of::()); + + // Ensure that the offset is within bounds (must be able to read at least two i8 values as u16) + if offset < SIZE - 1 { + // Cast the aligned pointer to u16 + let u16_ptr = unsafe { ptr.add(offset).cast::() }; + + // Read the u16 value at the aligned pointer + let value = unsafe { u16_ptr.read() }; + + // Convert the corresponding adjacent i8 values to u16 using native-endian conversion + let byte1 = x[offset] as u8; + let byte2 = x[offset + 1] as u8; + let expected_value = u16::from_ne_bytes([byte1, byte2]); + + // Verify that the read value matches the expected value + kani::assert!( + value == expected_value, + "Read value {} did not match expected u16 value {} from adjacent i8 values.", + value, expected_value + ); + } + } } From df2e65861d72273eab898fd87a2f5ed5ee237d26 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Wed, 2 Oct 2024 23:49:15 -0700 Subject: [PATCH 05/19] minor fix --- library/core/src/ptr/non_null.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index a80c3c5950ced..808cad4ad6144 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -9,6 +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::can_write; #[cfg(kani)] @@ -1791,7 +1792,6 @@ impl From<&T> for NonNull { mod verify { use super::*; use crate::ptr::null_mut; - use crate::ub_checks; use crate::mem::align_of; // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self @@ -1872,7 +1872,7 @@ mod verify { let expected_value = u16::from_ne_bytes([byte1, byte2]); // Verify that the read value matches the expected value - kani::assert!( + kani::assert( value == expected_value, "Read value {} did not match expected u16 value {} from adjacent i8 values.", value, expected_value From 6c341e83f79b6545aae1fb411d21878513e980f9 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Wed, 2 Oct 2024 23:57:52 -0700 Subject: [PATCH 06/19] minor fix --- library/core/src/ptr/non_null.rs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 808cad4ad6144..30791304ee35b 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::can_write; +use crate::ub_checks; #[cfg(kani)] @@ -1874,8 +1874,7 @@ mod verify { // Verify that the read value matches the expected value kani::assert( value == expected_value, - "Read value {} did not match expected u16 value {} from adjacent i8 values.", - value, expected_value + "Read value {} did not match expected u16 value {} from adjacent i8 values." ); } } From 319a002c116e8ed3b1282d8b4b016d04c522b4f8 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Thu, 3 Oct 2024 00:06:01 -0700 Subject: [PATCH 07/19] minor fix --- 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 30791304ee35b..6e4aac2db5ea7 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1846,7 +1846,7 @@ mod verify { } // pub fn align_offset(self, align: usize) -> usize - #[kani::proof_for_contract(NonNull::align_offset)] + #[kani::proof] pub fn non_null_check_align_offset() { const SIZE: usize = 10; // Non-deterministic input array of i8 (signed 8-bit integers) From 64568b787a39f8ab7325ecdbcd173b6d92793ab2 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Thu, 3 Oct 2024 11:55:08 -0700 Subject: [PATCH 08/19] add contract and negative proof for align_offset --- library/core/src/ptr/non_null.rs | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 6e4aac2db5ea7..04d75d981729d 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1184,6 +1184,8 @@ impl NonNull { #[must_use] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_unstable(feature = "const_align_offset", issue = "90962")] + #[requires(!self.pointer.is_null())] + #[ensures(!self.pointer.is_null())] pub const fn align_offset(self, align: usize) -> usize where T: Sized, @@ -1846,7 +1848,7 @@ mod verify { } // pub fn align_offset(self, align: usize) -> usize - #[kani::proof] + #[kani::proof_for_contract(NonNull::align_offset)] pub fn non_null_check_align_offset() { const SIZE: usize = 10; // Non-deterministic input array of i8 (signed 8-bit integers) @@ -1874,8 +1876,27 @@ mod verify { // Verify that the read value matches the expected value kani::assert( value == expected_value, - "Read value {} did not match expected u16 value {} from adjacent i8 values." + "Read value did not match expected u16 value from adjacent i8 values." ); } } + + // pub fn align_offset(self, align: usize) -> usize + #[kani::should_panic] + #[kani::proof_for_contract(NonNull::align_offset)] + pub fn non_null_check_align_offset_negative() { + const SIZE: usize = 10; + // Non-deterministic input array of i8 (signed 8-bit integers) + let x: [i8; SIZE] = kani::any(); + + // Non-null pointer to the start of the array + let ptr = NonNull::new(x.as_ptr() as *mut i8).unwrap(); + + // Generate align value that is not a power of two + let invald_align: usize = kani::any(); + kani::assume(!invalid_align.is_power_of_two()) + + // Trigger panic + let offset = ptr.align_offset(invalid_align); + } } From 2c3a17f351a3da943bc0fd8e871305a2723a316e Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Thu, 3 Oct 2024 11:57:41 -0700 Subject: [PATCH 09/19] add comments for addr --- library/core/src/ptr/non_null.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 04d75d981729d..c1ae51b6bea83 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1841,9 +1841,13 @@ mod verify { // pub fn addr(self) -> NonZero #[kani::proof_for_contract(NonNull::addr)] pub fn non_null_check_addr() { + + // Create NonNull pointer let mut x: i32 = kani::any(); let xptr = &mut x as *mut i32; let nonnull_xptr = NonNull::new(xptr).unwrap(); + + // Get pointer address let address = nonnull_xptr.addr(); } From 288abda6a6952a11fb961f296c403486628c0c4c Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Sat, 5 Oct 2024 12:48:17 -0700 Subject: [PATCH 10/19] add requires clause for align_offset and tidy up harnesses --- library/core/src/ptr/non_null.rs | 101 ++++++++++++++++--------------- 1 file changed, 53 insertions(+), 48 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index c1ae51b6bea83..f49d72fad77b3 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1,15 +1,14 @@ use crate::cmp::Ordering; use crate::marker::Unsize; -use crate::mem::{MaybeUninit, SizedTypeProperties}; +use crate::mem::{self, MaybeUninit, SizedTypeProperties}; use crate::num::NonZero; use crate::ops::{CoerceUnsized, DispatchFromDyn}; use crate::pin::PinCoerceUnsized; use crate::ptr::Unique; use crate::slice::{self, SliceIndex}; use crate::ub_checks::assert_unsafe_precondition; -use crate::{fmt, hash, intrinsics, ptr}; +use crate::{fmt, hash, intrinsics, ptr, ub_checks}; use safety::{ensures, requires}; -use crate::ub_checks; #[cfg(kani)] @@ -557,7 +556,7 @@ impl NonNull { #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] #[requires(count.checked_mul(core::mem::size_of::()).is_some())] // Prevent offset overflow #[requires(count * core::mem::size_of::() <= isize::MAX as usize)] // SAFETY: count * size_of::() does not overflow isize - #[requires(ub_checks::can_write(self.as_ptr().offset(count as isize)))] + //#[requires(ub_checks::can_write(self.as_ptr().offset(count as isize)))] // not working #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(count as isize))] pub const unsafe fn add(self, count: usize) -> Self where @@ -567,6 +566,8 @@ impl NonNull { // Additionally safety contract of `offset` guarantees that the resulting pointer is // pointing to an allocation, there can't be an allocation at null, thus it's safe to // construct `NonNull`. + assert!(core::mem::size_of::() == 1, "element size is 1"); + assert!(count * core::mem::size_of::() <= isize::MAX as usize, "count should not overflow"); unsafe { NonNull { pointer: intrinsics::offset(self.pointer, count) } } } @@ -1185,7 +1186,36 @@ impl NonNull { #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_unstable(feature = "const_align_offset", issue = "90962")] #[requires(!self.pointer.is_null())] - #[ensures(!self.pointer.is_null())] + #[ensures(|result| { + // Post-condition reference: https://github.com/model-checking/verify-rust-std/pull/69/files + let stride = mem::size_of::(); + // ZSTs + if stride == 0 { + if self.pointer.addr() % align == 0 { + return *result == 0; + } else { + return *result == usize::MAX; + } + } + // In this case, the pointer cannot be aligned + if (align % stride == 0) && (self.pointer.addr() % stride != 0) { + return *result == usize::MAX; + } + // Checking if the answer should indeed be usize::MAX when align % stride != 0 + // requires computing gcd(a, stride), which is too expensive without + // quantifiers (https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html). + // This should be updated once quantifiers are available. + if (align % stride != 0 && *result == usize::MAX) { + return true; + } + // If we reach this case, either: + // - align % stride == 0 and self.pointer.addr() % stride == 0, so it is definitely possible to align the pointer + // - align % stride != 0 and result != usize::MAX, so align_offset is claiming that it's possible to align the pointer + // Check that applying the returned result does indeed produce an aligned address + let product = usize::wrapping_mul(*result, stride); + let new_addr = usize::wrapping_add(product, self.pointer.addr()); + *result != usize::MAX && new_addr % align == 0 + })] pub const fn align_offset(self, align: usize) -> usize where T: Sized, @@ -1829,8 +1859,8 @@ mod verify { // Create a non-deterministic count value let count: usize = kani::any(); - // SAFETY: Ensure that the pointer operation does not go out of the bounds of the array - //kani::assume(count < SIZE - offset); + // Workaround: SAFETY: Ensure that the pointer operation does not go out of the bounds of the array + kani::assume(count < SIZE - offset); unsafe { // Add a positive offset to pointer @@ -1840,67 +1870,42 @@ mod verify { // pub fn addr(self) -> NonZero #[kani::proof_for_contract(NonNull::addr)] - pub fn non_null_check_addr() { - - // Create NonNull pointer + pub fn non_null_check_addr() { + // Create NonNull pointer & get pointer address let mut x: i32 = kani::any(); - let xptr = &mut x as *mut i32; - let nonnull_xptr = NonNull::new(xptr).unwrap(); - - // Get pointer address + let nonnull_xptr = NonNull::new(&mut x as *mut i32).unwrap(); let address = nonnull_xptr.addr(); } // pub fn align_offset(self, align: usize) -> usize #[kani::proof_for_contract(NonNull::align_offset)] pub fn non_null_check_align_offset() { - const SIZE: usize = 10; - // Non-deterministic input array of i8 (signed 8-bit integers) - let x: [i8; SIZE] = kani::any(); - - // Non-null pointer to the start of the array - let ptr = NonNull::new(x.as_ptr() as *mut i8).unwrap(); - - // Calculate the offset needed to align the pointer to u16 alignment - let offset = ptr.align_offset(align_of::()); - - // Ensure that the offset is within bounds (must be able to read at least two i8 values as u16) - if offset < SIZE - 1 { - // Cast the aligned pointer to u16 - let u16_ptr = unsafe { ptr.add(offset).cast::() }; - - // Read the u16 value at the aligned pointer - let value = unsafe { u16_ptr.read() }; - - // Convert the corresponding adjacent i8 values to u16 using native-endian conversion - let byte1 = x[offset] as u8; - let byte2 = x[offset + 1] as u8; - let expected_value = u16::from_ne_bytes([byte1, byte2]); + // Create NonNull pointer + let mut x: i8 = kani::any(); + let nonnull_xptr = NonNull::new(&mut x as *mut i8).unwrap(); - // Verify that the read value matches the expected value - kani::assert( - value == expected_value, - "Read value did not match expected u16 value from adjacent i8 values." - ); - } + // Call align_offset with valid align value + let align: usize = kani::any(); + kani::assume(align.is_power_of_two()); + nonnull_xptr.align_offset(align); } // pub fn align_offset(self, align: usize) -> usize #[kani::should_panic] #[kani::proof_for_contract(NonNull::align_offset)] pub fn non_null_check_align_offset_negative() { - const SIZE: usize = 10; // Non-deterministic input array of i8 (signed 8-bit integers) - let x: [i8; SIZE] = kani::any(); + let mut x: i8 = kani::any(); + let xptr = &mut x as *mut i8; // Non-null pointer to the start of the array - let ptr = NonNull::new(x.as_ptr() as *mut i8).unwrap(); + let nonnull_xptr = NonNull::new(xptr).unwrap(); // Generate align value that is not a power of two - let invald_align: usize = kani::any(); - kani::assume(!invalid_align.is_power_of_two()) + let invalid_align: usize = kani::any(); + kani::assume(!invalid_align.is_power_of_two()); // Trigger panic - let offset = ptr.align_offset(invalid_align); + let offset = nonnull_xptr.align_offset(invalid_align); } } From c7406c166da1231f03bc5d61d41c2fe4e4ed0bd9 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Mon, 21 Oct 2024 17:04:31 -0400 Subject: [PATCH 11/19] incorporate pr suggestions --- library/core/src/ptr/non_null.rs | 27 +++++++++++---------------- 1 file changed, 11 insertions(+), 16 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index f49d72fad77b3..518baf4c2471c 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1,6 +1,6 @@ use crate::cmp::Ordering; use crate::marker::Unsize; -use crate::mem::{self, MaybeUninit, SizedTypeProperties}; +use crate::mem::{MaybeUninit, SizedTypeProperties}; use crate::num::NonZero; use crate::ops::{CoerceUnsized, DispatchFromDyn}; use crate::pin::PinCoerceUnsized; @@ -279,8 +279,7 @@ impl NonNull { #[must_use] #[inline] #[unstable(feature = "strict_provenance", issue = "95228")] - #[requires(!self.as_ptr().is_null())] - #[ensures(|result| result.get() != 0)] + #[ensures(|result| result.get() != 0 && result.get() == self.as_ptr() as *const() as usize)] pub fn addr(self) -> NonZero { // SAFETY: The pointer is guaranteed by the type to be non-null, // meaning that the address will be non-zero. @@ -554,10 +553,9 @@ impl NonNull { #[must_use = "returns a new pointer rather than modifying its argument"] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] - #[requires(count.checked_mul(core::mem::size_of::()).is_some())] // Prevent offset overflow - #[requires(count * core::mem::size_of::() <= isize::MAX as usize)] // SAFETY: count * size_of::() does not overflow isize - //#[requires(ub_checks::can_write(self.as_ptr().offset(count as isize)))] // not working - #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(count as isize))] + #[requires(count.checked_mul(core::mem::size_of::()).is_some() + && count * core::mem::size_of::() <= isize::MAX as usize)] + #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(count as isize))] //TODO: use same_allocation to check pointer pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -566,8 +564,6 @@ impl NonNull { // Additionally safety contract of `offset` guarantees that the resulting pointer is // pointing to an allocation, there can't be an allocation at null, thus it's safe to // construct `NonNull`. - assert!(core::mem::size_of::() == 1, "element size is 1"); - assert!(count * core::mem::size_of::() <= isize::MAX as usize, "count should not overflow"); unsafe { NonNull { pointer: intrinsics::offset(self.pointer, count) } } } @@ -1185,10 +1181,9 @@ impl NonNull { #[must_use] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_unstable(feature = "const_align_offset", issue = "90962")] - #[requires(!self.pointer.is_null())] #[ensures(|result| { // Post-condition reference: https://github.com/model-checking/verify-rust-std/pull/69/files - let stride = mem::size_of::(); + let stride = crate::mem::size_of::(); // ZSTs if stride == 0 { if self.pointer.addr() % align == 0 { @@ -1824,7 +1819,6 @@ impl From<&T> for NonNull { mod verify { use super::*; use crate::ptr::null_mut; - use crate::mem::align_of; // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self #[kani::proof_for_contract(NonNull::new_unchecked)] @@ -1848,19 +1842,20 @@ mod verify { #[kani::proof_for_contract(NonNull::add)] pub fn non_null_check_add() { const SIZE: usize = 100000; - // Randomiz pointer offset within array bound - let offset = kani::any_where(|x| *x < SIZE); + // Randomize pointer offset within array bound + let offset = kani::any_where(|x| * x <= SIZE as isize); + kani::assume(offset >= 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: *mut i8 = arr.as_ptr() as *mut i8; // NonNUll pointer to the random offset - let ptr = unsafe { NonNull::new(raw_ptr.add(offset)).unwrap()}; + let ptr = unsafe { NonNull::new(raw_ptr.offset(offset)).unwrap()}; // Create a non-deterministic count value let count: usize = kani::any(); // Workaround: SAFETY: Ensure that the pointer operation does not go out of the bounds of the array - kani::assume(count < SIZE - offset); + kani::assume(count < SIZE - offset as usize); unsafe { // Add a positive offset to pointer From 4e7e3a5463cd7c716580ad37f879e87df173e68e Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Fri, 25 Oct 2024 15:29:38 -0400 Subject: [PATCH 12/19] using same_allocation for add --- library/core/src/ptr/non_null.rs | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 518baf4c2471c..8b062c9c74791 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -554,8 +554,11 @@ impl NonNull { #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] #[requires(count.checked_mul(core::mem::size_of::()).is_some() - && count * core::mem::size_of::() <= isize::MAX as usize)] - #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(count as isize))] //TODO: use same_allocation to check pointer + && count * core::mem::size_of::() <= isize::MAX as usize + && (self.pointer as isize).checked_add(count as isize * core::mem::size_of::() as isize).is_some() + && kani::mem::same_allocation(self.pointer, self.pointer.wrapping_offset(count as isize)))] //overflowing pointer.offset + #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(count as isize) + && kani::mem::same_allocation(result.pointer, self.pointer))] //TODO: use same_allocation to check pointer pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -1855,7 +1858,7 @@ mod verify { let count: usize = kani::any(); // Workaround: SAFETY: Ensure that the pointer operation does not go out of the bounds of the array - kani::assume(count < SIZE - offset as usize); + //kani::assume(count < SIZE - offset as usize); unsafe { // Add a positive offset to pointer From 6cfad82b4a360f2f5d3ff755c925798877f42cb1 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Mon, 28 Oct 2024 12:26:54 -0400 Subject: [PATCH 13/19] misc: remove todo --- library/core/src/ptr/non_null.rs | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 8b062c9c74791..2e893378daefb 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -555,10 +555,10 @@ impl NonNull { #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] #[requires(count.checked_mul(core::mem::size_of::()).is_some() && count * core::mem::size_of::() <= isize::MAX as usize - && (self.pointer as isize).checked_add(count as isize * core::mem::size_of::() as isize).is_some() - && kani::mem::same_allocation(self.pointer, self.pointer.wrapping_offset(count as isize)))] //overflowing pointer.offset + && (self.pointer as isize).checked_add(count as isize * core::mem::size_of::() as isize).is_some() // check wrapping add + && kani::mem::same_allocation(self.pointer, self.pointer.wrapping_offset(count as isize)))] #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(count as isize) - && kani::mem::same_allocation(result.pointer, self.pointer))] //TODO: use same_allocation to check pointer + && kani::mem::same_allocation(result.pointer, self.pointer))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -1852,14 +1852,11 @@ mod verify { let arr: [i8; SIZE] = kani::any(); // Get a raw pointer to the array let raw_ptr: *mut i8 = arr.as_ptr() as *mut i8; - // NonNUll pointer to the random offset + // NonNull pointer to the random offset let ptr = unsafe { NonNull::new(raw_ptr.offset(offset)).unwrap()}; // Create a non-deterministic count value let count: usize = kani::any(); - - // Workaround: SAFETY: Ensure that the pointer operation does not go out of the bounds of the array - //kani::assume(count < SIZE - offset as usize); - + unsafe { // Add a positive offset to pointer let result = ptr.add(count); From 22ac1a94af4241d735f49d4b403251c7ed770dff Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Thu, 7 Nov 2024 15:39:26 -0800 Subject: [PATCH 14/19] address PR comments --- library/core/src/ptr/non_null.rs | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 2e893378daefb..90e1da2164834 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -279,7 +279,7 @@ impl NonNull { #[must_use] #[inline] #[unstable(feature = "strict_provenance", issue = "95228")] - #[ensures(|result| result.get() != 0 && result.get() == self.as_ptr() as *const() as usize)] + #[ensures(|result| result.get() == self.as_ptr() as *const() as usize)] pub fn addr(self) -> NonZero { // SAFETY: The pointer is guaranteed by the type to be non-null, // meaning that the address will be non-zero. @@ -1846,8 +1846,8 @@ mod verify { pub fn non_null_check_add() { const SIZE: usize = 100000; // Randomize pointer offset within array bound - let offset = kani::any_where(|x| * x <= SIZE as isize); - kani::assume(offset >= 0); + let offset = kani::any_where(|x| *x <= SIZE as isize && *x >=0); + //kani::assume(offset >= 0); // Create a non-deterministic array of size SIZE let arr: [i8; SIZE] = kani::any(); // Get a raw pointer to the array @@ -1867,8 +1867,9 @@ mod verify { #[kani::proof_for_contract(NonNull::addr)] pub fn non_null_check_addr() { // Create NonNull pointer & get pointer address - let mut x: i32 = kani::any(); - let nonnull_xptr = NonNull::new(&mut x as *mut i32).unwrap(); + let x = kani::any::() as *mut i32; + kani::assume(!x.is_null()); + let nonnull_xptr = NonNull::new(x).unwrap(); let address = nonnull_xptr.addr(); } @@ -1876,8 +1877,9 @@ mod verify { #[kani::proof_for_contract(NonNull::align_offset)] pub fn non_null_check_align_offset() { // Create NonNull pointer - let mut x: i8 = kani::any(); - let nonnull_xptr = NonNull::new(&mut x as *mut i8).unwrap(); + let x = kani::any::() as *mut i32; + kani::assume(!x.is_null()); + let nonnull_xptr = NonNull::new(x).unwrap(); // Call align_offset with valid align value let align: usize = kani::any(); @@ -1889,12 +1891,11 @@ mod verify { #[kani::should_panic] #[kani::proof_for_contract(NonNull::align_offset)] pub fn non_null_check_align_offset_negative() { - // Non-deterministic input array of i8 (signed 8-bit integers) - let mut x: i8 = kani::any(); - let xptr = &mut x as *mut i8; - - // Non-null pointer to the start of the array - let nonnull_xptr = NonNull::new(xptr).unwrap(); + // Create NonNull pointer + let x = kani::any::() as *mut i8; + kani::assume(!x.is_null()); + + let nonnull_xptr = NonNull::new(x).unwrap(); // Generate align value that is not a power of two let invalid_align: usize = kani::any(); From 355c67221c627fbc7fb5c2cb7bac3995f1eaecb3 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Fri, 8 Nov 2024 12:05:15 -0800 Subject: [PATCH 15/19] address PR comment --- library/core/src/ptr/non_null.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index e9af39428dfe7..33be56646ae85 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -572,8 +572,7 @@ impl NonNull { && count * core::mem::size_of::() <= isize::MAX as usize && (self.pointer as isize).checked_add(count as isize * core::mem::size_of::() as isize).is_some() // check wrapping add && kani::mem::same_allocation(self.pointer, self.pointer.wrapping_offset(count as isize)))] - #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(count as isize) - && kani::mem::same_allocation(result.pointer, self.pointer))] + #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(count as isize))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, From b3839789744146246b44cc2fd42f7d4f8cfcaf78 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Mon, 11 Nov 2024 23:07:43 -0800 Subject: [PATCH 16/19] revert stdarch changes --- library/stdarch | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/stdarch b/library/stdarch index d9466edb4c53c..ff9a4445038ea 160000 --- a/library/stdarch +++ b/library/stdarch @@ -1 +1 @@ -Subproject commit d9466edb4c53cece8686ee6e17b028436ddf4151 +Subproject commit ff9a4445038eae46fd095188740946808581bc0e From 7e2eee337299f9888a8152a64a1ce7b2c2b6514c Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Wed, 13 Nov 2024 15:09:24 -0800 Subject: [PATCH 17/19] simplify expressions --- library/core/src/ptr/non_null.rs | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 33be56646ae85..5f63afd1270b2 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1872,7 +1872,6 @@ mod verify { const SIZE: usize = 100000; // Randomize pointer offset within array bound let offset = kani::any_where(|x| *x <= SIZE as isize && *x >=0); - //kani::assume(offset >= 0); // Create a non-deterministic array of size SIZE let arr: [i8; SIZE] = kani::any(); // Get a raw pointer to the array @@ -1893,8 +1892,9 @@ mod verify { pub fn non_null_check_addr() { // Create NonNull pointer & get pointer address let x = kani::any::() as *mut i32; - kani::assume(!x.is_null()); - let nonnull_xptr = NonNull::new(x).unwrap(); + //kani::assume(!x.is_null()); + //let nonnull_xptr = NonNull::new(x).unwrap(); + let Some(nonnull_xptr) = NonNull::new(x) else { return; }; let address = nonnull_xptr.addr(); } @@ -1903,8 +1903,7 @@ mod verify { pub fn non_null_check_align_offset() { // Create NonNull pointer let x = kani::any::() as *mut i32; - kani::assume(!x.is_null()); - let nonnull_xptr = NonNull::new(x).unwrap(); + let Some(nonnull_xptr) = NonNull::new(x) else { return; }; // Call align_offset with valid align value let align: usize = kani::any(); @@ -1918,13 +1917,10 @@ mod verify { pub fn non_null_check_align_offset_negative() { // Create NonNull pointer let x = kani::any::() as *mut i8; - kani::assume(!x.is_null()); + let Some(nonnull_xptr) = NonNull::new(x) else { return; }; - let nonnull_xptr = NonNull::new(x).unwrap(); - - // Generate align value that is not a power of two + // Generate align value that is not necessarily a power of two let invalid_align: usize = kani::any(); - kani::assume(!invalid_align.is_power_of_two()); // Trigger panic let offset = nonnull_xptr.align_offset(invalid_align); From dc9e9e0b3494433619071e3958f882275d66ac0e Mon Sep 17 00:00:00 2001 From: Qinyuan Wu Date: Wed, 13 Nov 2024 15:20:20 -0800 Subject: [PATCH 18/19] use PointerGenerator for add --- library/core/src/ptr/non_null.rs | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 5f63afd1270b2..2f9a8848c3dfe 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1847,6 +1847,7 @@ impl From<&T> for NonNull { mod verify { use super::*; use crate::ptr::null_mut; + use kani::PointerGenerator; // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self #[kani::proof_for_contract(NonNull::new_unchecked)] @@ -1870,19 +1871,13 @@ mod verify { #[kani::proof_for_contract(NonNull::add)] pub fn non_null_check_add() { const SIZE: usize = 100000; - // Randomize pointer offset within array bound - let offset = kani::any_where(|x| *x <= SIZE as isize && *x >=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: *mut i8 = arr.as_ptr() as *mut i8; - // NonNull pointer to the random offset - let ptr = unsafe { NonNull::new(raw_ptr.offset(offset)).unwrap()}; + let mut generator = PointerGenerator::<100000>::new(); + let raw_ptr: *mut i8 = generator.any_in_bounds().ptr; + let ptr = unsafe { NonNull::new(raw_ptr).unwrap()}; // Create a non-deterministic count value let count: usize = kani::any(); unsafe { - // Add a positive offset to pointer let result = ptr.add(count); } } @@ -1892,8 +1887,6 @@ mod verify { pub fn non_null_check_addr() { // Create NonNull pointer & get pointer address let x = kani::any::() as *mut i32; - //kani::assume(!x.is_null()); - //let nonnull_xptr = NonNull::new(x).unwrap(); let Some(nonnull_xptr) = NonNull::new(x) else { return; }; let address = nonnull_xptr.addr(); } From 25317fdff89a4ba9aa3e37196f1e40f0e4108ff1 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 14 Nov 2024 09:45:14 -0500 Subject: [PATCH 19/19] Remove unused import --- 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 2f9a8848c3dfe..b805c8e3b55ac 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -7,7 +7,7 @@ use crate::pin::PinCoerceUnsized; use crate::ptr::Unique; use crate::slice::{self, SliceIndex}; use crate::ub_checks::assert_unsafe_precondition; -use crate::{fmt, hash, intrinsics, ptr, ub_checks}; +use crate::{fmt, hash, intrinsics, ptr}; use safety::{ensures, requires};