Added <dyn Trait> Proof for Contracts for byte_add, byte_sub, and byte_offset

library/core/src/ptr/const_ptr.rs

@@ -7,6 +7,7 @@ use safety::{ensures, requires};
 
 #[cfg(kani)]
 use crate::kani;
+use core::mem;
 
 impl<T: ?Sized> *const T {
     /// Returns `true` if the pointer is null.
@@ -463,6 +464,21 @@ impl<T: ?Sized> *const T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // If count is zero, any pointer is valid including null pointer.
+        (count == 0) ||
+        // Else if count is not zero, then ensure that adding `count` doesn't cause 
+        // overflow and that both pointers `self` and the result are in the same 
+        // allocation 
+        (mem::size_of_val_raw(self) != 0 &&
+            (self.addr() as isize).checked_add(count).is_some() &&
+            kani::mem::same_allocation(self, self.wrapping_byte_offset(count)))
+    )]
+    #[ensures(|result|
+        // The resulting pointer should either be unchanged or still point to the same allocation
+        (self.addr() == (*result).addr()) ||
+        (kani::mem::same_allocation(self, *result))
+    )]
     pub const unsafe fn byte_offset(self, count: isize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `offset`.
         unsafe { self.cast::<u8>().offset(count).with_metadata_of(self) }
@@ -986,6 +1002,21 @@ impl<T: ?Sized> *const T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // If count is zero, any pointer is valid including null pointer.
+        (count == 0) || 
+        // Else if count is not zero, then ensure that adding `count` doesn't cause 
+        // overflow and that both pointers `self` and the result are in the same 
+        // allocation 
+        (mem::size_of_val_raw(self) != 0 &&
+            (self.addr() as isize).checked_add(count as isize).is_some() && 
+            kani::mem::same_allocation(self, self.wrapping_byte_add(count)))
+    )]
+    #[ensures(|result|
+        // The resulting pointer should either be unchanged or still point to the same allocation
+        (self.addr() == (*result).addr()) ||
+        (kani::mem::same_allocation(self, *result))
+    )]
     pub const unsafe fn byte_add(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `add`.
         unsafe { self.cast::<u8>().add(count).with_metadata_of(self) }
@@ -1101,6 +1132,21 @@ impl<T: ?Sized> *const T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // If count is zero, any pointer is valid including null pointer.
+        (count == 0) || 
+        // Else if count is not zero, then ensure that subtracting `count` doesn't 
+        // cause overflow and that both pointers `self` and the result are in the 
+        // same allocation 
+        (mem::size_of_val_raw(self) != 0 &&
+            (self.addr() as isize).checked_sub(count as isize).is_some() && 
+            kani::mem::same_allocation(self, self.wrapping_byte_sub(count)))
+    )]
+    #[ensures(|result|
+        // The resulting pointer should either be unchanged or still point to the same allocation
+        (self.addr() == (*result).addr()) ||
+        (kani::mem::same_allocation(self, *result))
+    )]
     pub const unsafe fn byte_sub(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `sub`.
         unsafe { self.cast::<u8>().sub(count).with_metadata_of(self) }
@@ -1916,7 +1962,7 @@ impl<T: ?Sized> PartialOrd for *const T {
 
 #[cfg(kani)]
 #[unstable(feature = "kani", issue = "none")]
-mod verify {
+pub mod verify {
     use crate::kani;
     use core::mem;
     use kani::PointerGenerator;
@@ -2058,4 +2104,57 @@ mod verify {
         check_const_offset_from_tuple_4,
         check_const_offset_from_tuple_4_arr
     );
+
+    trait TestTrait {}
+
+    struct TestStruct {
+        value: i64,
+    }
+
+    impl TestTrait for TestStruct {}
+
+    macro_rules! gen_const_byte_arith_harness_for_dyn {
+        (byte_offset, $proof_name:ident) => {
+            // Workaround: Directly verifying the method `<*const dyn TestTrait>::byte_offset`
+            // causes a compilation error: "Failed to resolve checking function <*const dyn TestTrait>::byte_offset
+            // because Expected a type, but found trait object paths `dyn TestTrait`".
+            // As a result, the proof is annotated for the underlying struct type instead.
+            #[kani::proof_for_contract(<*const TestStruct>::byte_offset)]
+            pub fn $proof_name() {
+                let test_struct = TestStruct { value: 42 };
+                let trait_object: &dyn TestTrait = &test_struct;
+                let test_ptr: *const dyn TestTrait = trait_object;
+
+                let count: isize = kani::any();
+
+                unsafe {
+                    test_ptr.byte_offset(count);
+                }
+            }
+        };
+
+        ($fn_name: ident, $proof_name:ident) => {
+            // Workaround: Directly verifying the method `<*const dyn TestTrait>::$fn_name`
+            // causes a compilation error: "Failed to resolve checking function <*const dyn TestTrait>::byte_offset
+            // because Expected a type, but found trait object paths `dyn TestTrait`".
+            // As a result, the proof is annotated for the underlying struct type instead.
+            #[kani::proof_for_contract(<*const TestStruct>::$fn_name)]
+            pub fn $proof_name() {
+                let test_struct = TestStruct { value: 42 };
+                let trait_object: &dyn TestTrait = &test_struct;
+                let test_ptr: *const dyn TestTrait = trait_object;
+
+                //byte_add and byte_sub need count to be usize unlike byte_offset
+                let count: usize = kani::any();
+
+                unsafe {
+                    test_ptr.$fn_name(count);
+                }
+            }
+        };
+    }
+
+    gen_const_byte_arith_harness_for_dyn!(byte_add, check_const_byte_add_dyn);
+    gen_const_byte_arith_harness_for_dyn!(byte_sub, check_const_byte_sub_dyn);
+    gen_const_byte_arith_harness_for_dyn!(byte_offset, check_const_byte_offset_dyn);
 }

library/core/src/ptr/mut_ptr.rs

@@ -7,6 +7,7 @@ use safety::{ensures, requires};
 
 #[cfg(kani)]
 use crate::kani;
+use core::mem;
 
 impl<T: ?Sized> *mut T {
     /// Returns `true` if the pointer is null.
@@ -477,6 +478,21 @@ impl<T: ?Sized> *mut T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // If count is zero, any pointer is valid including null pointer.
+        (count == 0) || 
+        // Else if count is not zero, then ensure that subtracting `count` doesn't 
+        // cause overflow and that both pointers `self` and the result are in the 
+        // same allocation 
+        (mem::size_of_val_raw(self) != 0 &&
+            (self.addr() as isize).checked_add(count).is_some() && 
+            kani::mem::same_allocation(self as *const T, self.wrapping_byte_offset(count) as *const T))
+    )]
+    #[ensures(|result|
+        // The resulting pointer should either be unchanged or still point to the same allocation
+        (self.addr() == (*result).addr()) ||
+        (kani::mem::same_allocation(self as *const T, *result as *const T))
+    )]
     pub const unsafe fn byte_offset(self, count: isize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `offset`.
         unsafe { self.cast::<u8>().offset(count).with_metadata_of(self) }
@@ -1089,6 +1105,21 @@ impl<T: ?Sized> *mut T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // If count is zero, any pointer is valid including null pointer.
+        (count == 0) || 
+        // Else if count is not zero, then ensure that subtracting `count` doesn't 
+        // cause overflow and that both pointers `self` and the result are in the 
+        // same allocation 
+        (mem::size_of_val_raw(self) != 0 &&
+            (self.addr() as isize).checked_add(count as isize).is_some() && 
+            kani::mem::same_allocation(self as *const T, self.wrapping_byte_add(count) as *const T))
+    )]
+    #[ensures(|result|
+        // The resulting pointer should either be unchanged or still point to the same allocation
+        (self.addr() == (*result).addr()) ||
+        (kani::mem::same_allocation(self as *const T, *result as *const T))
+    )]
     pub const unsafe fn byte_add(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `add`.
         unsafe { self.cast::<u8>().add(count).with_metadata_of(self) }
@@ -1221,6 +1252,21 @@ impl<T: ?Sized> *mut T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // If count is zero, any pointer is valid including null pointer.
+        (count == 0) || 
+        // Else if count is not zero, then ensure that subtracting `count` doesn't 
+        // cause overflow and that both pointers `self` and the result are in the 
+        // same allocation 
+        (mem::size_of_val_raw(self) != 0 &&
+            (self.addr() as isize).checked_sub(count as isize).is_some() && 
+            kani::mem::same_allocation(self as *const T, self.wrapping_byte_sub(count) as *const T))
+    )]
+    #[ensures(|result|
+        // The resulting pointer should either be unchanged or still point to the same allocation
+        (self.addr() == (*result).addr()) ||
+        (kani::mem::same_allocation(self as *const T, *result as *const T))
+    )]
     pub const unsafe fn byte_sub(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `sub`.
         unsafe { self.cast::<u8>().sub(count).with_metadata_of(self) }
@@ -2359,8 +2405,10 @@ impl<T: ?Sized> PartialOrd for *mut T {
 
 #[cfg(kani)]
 #[unstable(feature = "kani", issue = "none")]
-mod verify {
+pub mod verify {
     use crate::kani;
+    use core::mem;
+    use kani::PointerGenerator;
 
     /// This macro generates proofs for contracts on `add`, `sub`, and `offset`
     /// operations for pointers to integer, composite, and unit types.
@@ -2478,4 +2526,61 @@ mod verify {
     generate_mut_arithmetic_harness!((f64, bool), check_mut_offset_tuple_2, offset);
     generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_offset_tuple_3, offset);
     generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_offset_tuple_4, offset);
+
+    trait TestTrait {}
+
+    struct TestStruct {
+        value: i64,
+    }
+
+    impl TestTrait for TestStruct {}
+
+    /// This macro generates proofs for contracts on `byte_add`, `byte_sub`, and `byte_offset`
+    /// operations for pointers to dyn Trait.
+    /// - `$fn_name`: Specifies the arithmetic operation to verify.
+    /// - `$proof_name`: Specifies the name of the generated proof for contract.
+    macro_rules! gen_mut_byte_arith_harness_for_dyn {
+        (byte_offset, $proof_name:ident) => {
+            // Workaround: Directly verifying the method `<*mut dyn TestTrait>::byte_offset`
+            // causes a compilation error: "Failed to resolve checking function <*mut dyn TestTrait>::byte_offset
+            // because Expected a type, but found trait object paths `dyn TestTrait`".
+            // As a result, the proof is annotated for the underlying struct type instead.
+            #[kani::proof_for_contract(<*mut TestStruct>::byte_offset)]
+            pub fn $proof_name() {
+                let mut test_struct = TestStruct { value: 42 };
+                let trait_object: &mut dyn TestTrait = &mut test_struct;
+                let test_ptr: *mut dyn TestTrait = trait_object;
+
+                let count: isize = kani::any();
+
+                unsafe {
+                    test_ptr.byte_offset(count);
+                }
+            }
+        };
+        ($fn_name: ident, $proof_name:ident) => {
+            // Workaround: Directly verifying the method `<*mut dyn TestTrait>::$fn_name`
+            // causes a compilation error: "Failed to resolve checking function <*mut dyn TestTrait>::byte_offset
+            // because Expected a type, but found trait object paths `dyn TestTrait`".
+            // As a result, the proof is annotated for the underlying struct type instead.
+            #[kani::proof_for_contract(<*mut TestStruct>::$fn_name)]
+            pub fn $proof_name() {
+                let mut test_struct = TestStruct { value: 42 };
+                let trait_object: &mut dyn TestTrait = &mut test_struct;
+                let test_ptr: *mut dyn TestTrait = trait_object;
+
+                //byte_add and byte_sub need count to be usize unlike byte_offset
+                let count: usize = kani::any();
+
+                unsafe {
+                    test_ptr.$fn_name(count);
+                }
+            }
+        };
+    }
+
+    // fn <*mut T>::add(), <*mut T>::sub() and <*mut T>::offset() dyn Trait verification
+    gen_mut_byte_arith_harness_for_dyn!(byte_add, check_mut_byte_add_dyn);
+    gen_mut_byte_arith_harness_for_dyn!(byte_sub, check_mut_byte_sub_dyn);
+    gen_mut_byte_arith_harness_for_dyn!(byte_offset, check_mut_byte_offset_dyn);
 }