Skip to content

Commit c841a12

Browse files
Dhvani-Kapadiazhassan-awstautschnigQinyuanWu
authored
Contract and harness for as_ptr, cast, as_mut_ptr, and as_non_null_ptr (#126)
### Description This PR includes contracts and proof harnesses for the four APIs as_ptr, cast, as_mut_ptr, and as_non_null_ptr which are part of the NonNull library in Rust. ### Changes Overview: Covered APIs: NonNull::as_ptr: Acquires the underlying *mut pointer NonNull::cast: Casts to a pointer of another type NonNull:: as_mut_ptr: Returns raw pointer to array's buffer NonNull::as_non_null_ptr: Returns a non-null pointer to slice's buffer Proof harness: non_null_check_as_ptr non_null_check_cast non_null_check_as_mut_ptr non_null_check_as_non_null_ptr Revalidation To revalidate the verification results, run kani verify-std -Z unstable-options "path/to/library" -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify. This will run all four harnesses in the module. All default checks should pass: ``` SUMMARY: ** 0 of 128 failed VERIFICATION:- SUCCESSFUL Verification Time: 0.8232234s Complete - 4 successfully verified harnesses, 0 failures, 4 total. ``` Towards issue #53 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Zyad Hassan <[email protected]> Co-authored-by: Zyad Hassan <[email protected]> Co-authored-by: Michael Tautschnig <[email protected]> Co-authored-by: Qinyuan Wu <[email protected]>
1 parent 2338dad commit c841a12

File tree

1 file changed

+44
-0
lines changed

1 file changed

+44
-0
lines changed

library/core/src/ptr/non_null.rs

+44
Original file line numberDiff line numberDiff line change
@@ -353,6 +353,8 @@ impl<T: ?Sized> NonNull<T> {
353353
#[rustc_never_returns_null_ptr]
354354
#[must_use]
355355
#[inline(always)]
356+
//Ensures address of resulting pointer is same as original
357+
#[ensures(|result: &*mut T| *result == self.pointer as *mut T)]
356358
pub const fn as_ptr(self) -> *mut T {
357359
self.pointer as *mut T
358360
}
@@ -454,6 +456,8 @@ impl<T: ?Sized> NonNull<T> {
454456
#[must_use = "this returns the result of the operation, \
455457
without modifying the original"]
456458
#[inline]
459+
// Address preservation
460+
#[ensures(|result: &NonNull<U>| result.as_ptr().addr() == self.as_ptr().addr())]
457461
pub const fn cast<U>(self) -> NonNull<U> {
458462
// SAFETY: `self` is a `NonNull` pointer which is necessarily non-null
459463
unsafe { NonNull { pointer: self.as_ptr() as *mut U } }
@@ -1470,6 +1474,8 @@ impl<T> NonNull<[T]> {
14701474
#[inline]
14711475
#[must_use]
14721476
#[unstable(feature = "slice_ptr_get", issue = "74265")]
1477+
// Address preservation
1478+
#[ensures(|result: &NonNull<T>| result.as_ptr().addr() == self.as_ptr().addr())]
14731479
pub const fn as_non_null_ptr(self) -> NonNull<T> {
14741480
self.cast()
14751481
}
@@ -1489,6 +1495,8 @@ impl<T> NonNull<[T]> {
14891495
#[must_use]
14901496
#[unstable(feature = "slice_ptr_get", issue = "74265")]
14911497
#[rustc_never_returns_null_ptr]
1498+
// Address preservation
1499+
#[ensures(|result: &*mut T| *result == self.pointer as *mut T)]
14921500
pub const fn as_mut_ptr(self) -> *mut T {
14931501
self.as_non_null_ptr().as_ptr()
14941502
}
@@ -2186,6 +2194,42 @@ mod verify {
21862194
}
21872195
}
21882196

2197+
#[kani::proof_for_contract(NonNull::as_ptr)]
2198+
pub fn non_null_check_as_ptr() {
2199+
// Create a non-null pointer to a random value
2200+
let non_null_ptr: *mut i32 = kani::any::<usize>() as *mut i32;
2201+
if let Some(ptr) = NonNull::new(non_null_ptr) {
2202+
let result = ptr.as_ptr();
2203+
}
2204+
2205+
}
2206+
2207+
#[kani::proof_for_contract(NonNull::<[T]>::as_mut_ptr)]
2208+
pub fn non_null_check_as_mut_ptr() {
2209+
const ARR_LEN: usize = 100;
2210+
let mut values: [i32; ARR_LEN] = kani::any();
2211+
let slice = kani::slice::any_slice_of_array_mut(&mut values);
2212+
let non_null_ptr = NonNull::new(slice as *mut [i32]).unwrap();
2213+
let result = non_null_ptr.as_mut_ptr();
2214+
}
2215+
#[kani::proof_for_contract(NonNull::<T>::cast)]
2216+
pub fn non_null_check_cast() {
2217+
// Create a non-null pointer to a random value
2218+
let non_null_ptr: *mut i32 = kani::any::<usize>() as *mut i32;
2219+
if let Some(ptr) = NonNull::new(non_null_ptr) {
2220+
let result: NonNull<u8> = ptr.cast();
2221+
}
2222+
}
2223+
2224+
#[kani::proof_for_contract(NonNull::<[T]>::as_non_null_ptr)]
2225+
pub fn non_null_check_as_non_null_ptr() {
2226+
const ARR_LEN: usize = 100;
2227+
let mut values: [i32; ARR_LEN] = kani::any();
2228+
let slice = kani::slice::any_slice_of_array_mut(&mut values);
2229+
let non_null_ptr = NonNull::new(slice as *mut [i32]).unwrap();
2230+
let result = non_null_ptr.as_non_null_ptr();
2231+
}
2232+
21892233
#[kani::proof]
21902234
pub fn non_null_check_len() {
21912235
// Create a non-deterministic NonNull pointer using kani::any()

0 commit comments

Comments
 (0)