AWS Team 3: Verifying <*const T>::offset

library/core/src/ptr/const_ptr.rs

@@ -3,6 +3,10 @@ use crate::cmp::Ordering::{Equal, Greater, Less};
 use crate::intrinsics::const_eval_select;
 use crate::mem::SizedTypeProperties;
 use crate::slice::{self, SliceIndex};
+use safety::{ensures, requires};
+
+#[cfg(kani)]
+use crate::kani;
 
 impl<T: ?Sized> *const T {
  /// Returns `true` if the pointer is null.
@@ -273,7 +277,11 @@ impl<T: ?Sized> *const T {
  pub const unsafe fn as_ref<'a>(self) -> Option<&'a T> {
  // SAFETY: the caller must guarantee that `self` is valid
  // for a reference if it isn't null.
- if self.is_null() { None } else { unsafe { Some(&*self) } }
+ if self.is_null() {
+ None
+ } else {
+ unsafe { Some(&*self) }
+ }
  }
 
  /// Returns a shared reference to the value behind the pointer.
@@ -341,7 +349,11 @@ impl<T: ?Sized> *const T {
  {
  // SAFETY: the caller must guarantee that `self` meets all the
  // requirements for a reference.
- if self.is_null() { None } else { Some(unsafe { &*(self as *const MaybeUninit<T>) }) }
+ if self.is_null() {
+ None
+ } else {
+ Some(unsafe { &*(self as *const MaybeUninit<T>) })
+ }
  }
 
  /// Adds an offset to a pointer.
@@ -388,6 +400,10 @@ impl<T: ?Sized> *const T {
  #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")]
  #[inline(always)]
  #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+ #[requires(kani::mem::can_dereference(self))]
+ // TODO: Determine the valid value range for 'count' and update the precondition accordingly.
+ #[requires(count == 0)] // This precondition is currently a placeholder.
+ #[ensures(|result| kani::mem::can_dereference(result))]
  pub const unsafe fn offset(self, count: isize) -> *const T
  where
  T: Sized,
@@ -495,7 +511,9 @@ impl<T: ?Sized> *const T {
  #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
  #[rustc_allow_const_fn_unstable(set_ptr_value)]
  pub const fn wrapping_byte_offset(self, count: isize) -> Self {
- self.cast::<u8>().wrapping_offset(count).with_metadata_of(self)
+ self.cast::<u8>()
+ .wrapping_offset(count)
+ .with_metadata_of(self)
  }
 
  /// Masks out bits of the pointer according to a mask.
@@ -1774,3 +1792,20 @@ impl<T: ?Sized> PartialOrd for *const T {
  *self >= *other
  }
 }
+
+// This module contains all proof harnesses for function contracts.
+// Each proof harness verifies the soundness of a function contract for a specific type.
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+ use crate::kani;
+
+ #[allow(unused)]
+ #[kani::proof_for_contract(<*const i32>::offset)]
+ fn check_offset_i32() {
+ let mut test_val: i32 = kani::any();
+ let test_ptr: *const i32 = &test_val;
+ let offset: isize = kani::any();
+ unsafe { test_ptr.offset(offset) };
+ }
+}