Skip to content

Commit

Permalink
Contract and harness for as_ptr, cast, as_mut_ptr, and as_non_null_ptr (
Browse files Browse the repository at this point in the history
rust-lang#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 rust-lang#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]>
  • Loading branch information
5 people authored Dec 5, 2024
1 parent 2338dad commit c841a12
Showing 1 changed file with 44 additions and 0 deletions.
44 changes: 44 additions & 0 deletions library/core/src/ptr/non_null.rs
Original file line number Diff line number Diff line change
Expand Up @@ -353,6 +353,8 @@ impl<T: ?Sized> NonNull<T> {
#[rustc_never_returns_null_ptr]
#[must_use]
#[inline(always)]
//Ensures address of resulting pointer is same as original
#[ensures(|result: &*mut T| *result == self.pointer as *mut T)]
pub const fn as_ptr(self) -> *mut T {
self.pointer as *mut T
}
Expand Down Expand Up @@ -454,6 +456,8 @@ impl<T: ?Sized> NonNull<T> {
#[must_use = "this returns the result of the operation, \
without modifying the original"]
#[inline]
// Address preservation
#[ensures(|result: &NonNull<U>| result.as_ptr().addr() == self.as_ptr().addr())]
pub const fn cast<U>(self) -> NonNull<U> {
// SAFETY: `self` is a `NonNull` pointer which is necessarily non-null
unsafe { NonNull { pointer: self.as_ptr() as *mut U } }
Expand Down Expand Up @@ -1470,6 +1474,8 @@ impl<T> NonNull<[T]> {
#[inline]
#[must_use]
#[unstable(feature = "slice_ptr_get", issue = "74265")]
// Address preservation
#[ensures(|result: &NonNull<T>| result.as_ptr().addr() == self.as_ptr().addr())]
pub const fn as_non_null_ptr(self) -> NonNull<T> {
self.cast()
}
Expand All @@ -1489,6 +1495,8 @@ impl<T> NonNull<[T]> {
#[must_use]
#[unstable(feature = "slice_ptr_get", issue = "74265")]
#[rustc_never_returns_null_ptr]
// Address preservation
#[ensures(|result: &*mut T| *result == self.pointer as *mut T)]
pub const fn as_mut_ptr(self) -> *mut T {
self.as_non_null_ptr().as_ptr()
}
Expand Down Expand Up @@ -2186,6 +2194,42 @@ mod verify {
}
}

#[kani::proof_for_contract(NonNull::as_ptr)]
pub fn non_null_check_as_ptr() {
// Create a non-null pointer to a random value
let non_null_ptr: *mut i32 = kani::any::<usize>() as *mut i32;
if let Some(ptr) = NonNull::new(non_null_ptr) {
let result = ptr.as_ptr();
}

}

#[kani::proof_for_contract(NonNull::<[T]>::as_mut_ptr)]
pub fn non_null_check_as_mut_ptr() {
const ARR_LEN: usize = 100;
let mut values: [i32; ARR_LEN] = kani::any();
let slice = kani::slice::any_slice_of_array_mut(&mut values);
let non_null_ptr = NonNull::new(slice as *mut [i32]).unwrap();
let result = non_null_ptr.as_mut_ptr();
}
#[kani::proof_for_contract(NonNull::<T>::cast)]
pub fn non_null_check_cast() {
// Create a non-null pointer to a random value
let non_null_ptr: *mut i32 = kani::any::<usize>() as *mut i32;
if let Some(ptr) = NonNull::new(non_null_ptr) {
let result: NonNull<u8> = ptr.cast();
}
}

#[kani::proof_for_contract(NonNull::<[T]>::as_non_null_ptr)]
pub fn non_null_check_as_non_null_ptr() {
const ARR_LEN: usize = 100;
let mut values: [i32; ARR_LEN] = kani::any();
let slice = kani::slice::any_slice_of_array_mut(&mut values);
let non_null_ptr = NonNull::new(slice as *mut [i32]).unwrap();
let result = non_null_ptr.as_non_null_ptr();
}

#[kani::proof]
pub fn non_null_check_len() {
// Create a non-deterministic NonNull pointer using kani::any()
Expand Down

0 comments on commit c841a12

Please sign in to comment.