contract and harness for byte_sub and offset

Author: Dhvani-Kapadia

library/core/src/num/mod.rs

@@ -5,11 +5,11 @@
 use crate::str::FromStr;
 use crate::ub_checks::assert_unsafe_precondition;
 use crate::{ascii, intrinsics, mem};
-use safety::requires;
+/*use safety::requires;
 
 #[cfg(kani)]
 use crate::kani;
-
+*/
 // Used because the `?` operator is not allowed in a const context.
 macro_rules! try_opt {
     ($e:expr) => {
@@ -1585,7 +1585,6 @@ from_str_radix_size_impl! { i16 isize, u16 usize }
 from_str_radix_size_impl! { i32 isize, u32 usize }
 #[cfg(target_pointer_width = "64")]
 from_str_radix_size_impl! { i64 isize, u64 usize }
-
 #[cfg(kani)]
 #[unstable(feature = "kani", issue = "none")]
 mod verify {

library/core/src/ptr/non_null.rs

@@ -1,5 +1,6 @@
 use crate::cmp::Ordering;
 use crate::marker::Unsize;
+//use crate::num::NonZeroUsize;
 use crate::mem::{MaybeUninit, SizedTypeProperties};
 use crate::num::NonZero;
 use crate::ops::{CoerceUnsized, DispatchFromDyn};
@@ -476,11 +477,12 @@ impl<T: ?Sized> NonNull<T> {
     #[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")]
-    #[kani::requires(!self.as_ptr().is_null())]// Ensures that the input pointer is not null, which is a requirement for NonNull
-    #[kani::requires(count.checked_mul(std::mem::size_of::<T>() as isize).is_some())]// Checks that multiplying count by the size of T doesn't overflow isize
-    #[kani::ensures(|result: &NonNull<T>| !result.as_ptr().is_null())] // Guarantees that the resulting pointer is also not null
-    #[kani::ensures(|result: &NonNull<T>| (result.as_ptr() as isize) == (self.as_ptr() as isize) + count * (std::mem::size_of::<T>() as isize))]
-    // It checks that the resulting pointer address is equal to the original address plus the offset
+    // Requires that the input pointer is not null
+    #[kani::requires(!self.as_ptr().is_null())]
+    // Requires that multiplying count by the size of T doesn't overflow isize
+    #[kani::requires(count.checked_mul(core::mem::size_of::<T>() as isize).is_some())]
+    //Two conditions for postconditions: 1.Resulting pointer is not null 2.Safe operation of pointer arithmetic
+    #[kani::ensures(|result: &NonNull<T>|  !result.as_ptr().is_null() && (result.as_ptr() as isize) == (self.as_ptr() as isize).wrapping_add(count.wrapping_mul(core::mem::size_of::<T>() as isize)))]
     pub const unsafe fn offset(self, count: isize) -> Self
     where
         T: Sized,
@@ -668,11 +670,12 @@ impl<T: ?Sized> NonNull<T> {
     #[rustc_allow_const_fn_unstable(set_ptr_value)]
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
-    #[kani::requires(!self.as_ptr().is_null())] //precondition to ensures that pointer is not null
-    #[kani::requires(count <= isize::MAX as usize)] //precondition to ensure count doesn't exceed max
-    #[kani::ensures(|result: &NonNull<T>| !result.as_ptr().is_null())] //postcondition that result is not null
-    #[kani::ensures(|result: &NonNull<T>| result.as_ptr() as usize == self.as_ptr() as usize - count)] //postcondition that verifies correctness of pointer arithmetic
-
+    //Requires that the input pointer is not null
+    #[kani::requires(!self.as_ptr().is_null())]
+    // Requires that count doesnt exceed Max
+    #[kani::requires(count <= isize::MAX as usize)] 
+    //Ensures that result is not null
+    #[kani::ensures(|result: &NonNull<T>| !result.as_ptr().is_null())] 
     pub const unsafe fn byte_sub(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `sub` and `byte_sub` has the same
         // safety contract.
@@ -1814,43 +1817,43 @@ mod verify {
         let _ = NonNull::new(maybe_null_ptr);
     }
    #[kani::proof_for_contract(NonNull::byte_sub)]
-    pub fn non_null_byte_sub() {
-    // Create an array to work with
+    pub fn non_null_check_byte_sub() {
+    // Initializing array of size 10000
     const ARR_SIZE: usize = 100000;
     let arr: [i32; ARR_SIZE] = kani::any();
-    //Randomizing the start
+    //Randomizing start pointer within array
     let offset = kani::any_where(|x| *x <= ARR_SIZE);
     // Create a NonNull pointer to the end of the array
     let raw_ptr: *mut i32 = unsafe { arr.as_ptr().add(offset) as *mut i32 };
     let ptr = unsafe { NonNull::new(raw_ptr).unwrap() };
     // Choose an arbitrary count to subtract
     let count: usize = kani::any();
-        // Assume preconditions
-        kani::assume(!ptr.as_ptr().is_null());
-        kani::assume(count <= isize::MAX as usize);
-        kani::assume(count <= offset);
-        // Ensure that the subtraction doesnt go out of bounds of array
-        kani::assume(count < ARR_SIZE - offset);
+    // Ensure that the subtraction doesnt go out of bounds of array
+     kani::assume(count < ARR_SIZE - offset);
   unsafe {
      // Perform the byte_sub operation
      let result = ptr.byte_sub(count);
   }}
 
   #[kani::proof_for_contract(NonNull::offset)]
-  pub fun non_null_offset(){
-    const ARR_SIZE: usize = 10000;
-    let arr: [i32; ARR_SIZE] = kani::any(); 
-    // Randomizing start pointer within array
-   let start_offset = kani::any_where(|x| *x < ARR_SIZE);
-   let ptr = unsafe { NonNull::new(arr.as_ptr().add(start_offset) as *mut i32).unwrap() };
-
-    // Choose an arbitrary count to offset
-    let count: isize = kani::any();
-    kani::assume(!ptr.as_ptr().is_null()); // NonNull guarantee
-    kani::assume(count.checked_mul(std::mem::size_of::<i32>() as isize).is_some()); // Prevent overflow
-    unsafe {
-        let result = ptr.offset(count);
+   pub fn non_null_check_offset(){
+        //Initializing array of size 10000
+        const ARR_SIZE: usize = 10000;
+        let arr: [i32; ARR_SIZE] = kani::any(); 
+         // Randomizing start pointer within array
+        let start_offset = kani::any_where(|x| *x < ARR_SIZE);
+        // Creating a NonNull pointer to a random position within the array
+        let ptr = unsafe { NonNull::new(arr.as_ptr().add(start_offset) as *mut i32).unwrap() };
+        // Choose an arbitrary count to offset
+        let count: isize = kani::any();
+        // Constraining the count to ensure it doesn't go out of bounds
+        kani::assume(
+            (count >= 0 && (count as usize) < ARR_SIZE - start_offset) ||
+            (count < 0 && count.unsigned_abs() <= start_offset)
+        );
+        unsafe {
+            // Perform the offset operation
+            let result = ptr.offset(count);
+        }
     }
-
-  }
 }