Merge branch 'transmute_unchecked' of https://github.com/AlexLB99/verify-rust-std into transmute_unchecked

Author: AlexLB99

Diff for: .github/pull_requests.toml

@@ -16,5 +16,7 @@ members = [
     "robdockins",
     "HuStmpHrrr",
     "Eh2406",
-    "jswrenn"
+    "jswrenn",
+    "havelund",
+    "jorajeev"
 ]

Diff for: library/core/src/ffi/c_str.rs

@@ -9,6 +9,11 @@ use crate::ptr::NonNull;
 use crate::slice::memchr;
 use crate::{fmt, intrinsics, ops, slice, str};
 
+use crate::ub_checks::Invariant;
+
+#[cfg(kani)]
+use crate::kani;
+
 // FIXME: because this is doc(inline)d, we *have* to use intra-doc links because the actual link
 //   depends on where the item is being documented. however, since this is libcore, we can't
 //   actually reference libstd or liballoc in intra-doc links. so, the best we can do is remove the
@@ -207,6 +212,22 @@ impl fmt::Display for FromBytesWithNulError {
     }
 }
 
+#[unstable(feature = "ub_checks", issue = "none")]
+impl Invariant for &CStr {
+    /**
+     * Safety invariant of a valid CStr:
+     * 1. An empty CStr should have a null byte.
+     * 2. A valid CStr should end with a null-terminator and contains
+     *    no intermediate null bytes.
+     */
+    fn is_safe(&self) -> bool {
+        let bytes: &[c_char] = &self.inner;
+        let len = bytes.len();
+
+        !bytes.is_empty() && bytes[len - 1] == 0 && !bytes[..len-1].contains(&0)
+    }
+}
+
 impl CStr {
     /// Wraps a raw C string with a safe C string wrapper.
     ///
@@ -833,3 +854,91 @@ impl Iterator for Bytes<'_> {
 
 #[unstable(feature = "cstr_bytes", issue = "112115")]
 impl FusedIterator for Bytes<'_> {}
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    
+    // Helper function
+    fn arbitrary_cstr(slice: &[u8]) -> &CStr {
+        let result = CStr::from_bytes_until_nul(&slice);
+        kani::assume(result.is_ok());
+        let c_str = result.unwrap();
+        assert!(c_str.is_safe());
+        c_str
+    }
+
+    // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError>
+    #[kani::proof]
+    #[kani::unwind(32)] // 7.3 seconds when 16; 33.1 seconds when 32
+    fn check_from_bytes_until_nul() {
+        const MAX_SIZE: usize = 32;
+        let string: [u8; MAX_SIZE] = kani::any();
+        // Covers the case of a single null byte at the end, no null bytes, as
+        // well as intermediate null bytes
+        let slice = kani::slice::any_slice_of_array(&string);
+
+        let result = CStr::from_bytes_until_nul(slice);
+        if let Ok(c_str) = result {
+            assert!(c_str.is_safe());
+        }
+    }
+  
+    // pub const fn count_bytes(&self) -> usize
+    #[kani::proof]
+    #[kani::unwind(32)]
+    fn check_count_bytes() {
+        const MAX_SIZE: usize = 32;
+        let mut bytes: [u8; MAX_SIZE] = kani::any();
+        
+        // Non-deterministically generate a length within the valid range [0, MAX_SIZE]
+        let mut len: usize = kani::any_where(|&x| x < MAX_SIZE);
+        
+        // If a null byte exists before the generated length
+        // adjust len to its position
+        if let Some(pos) = bytes[..len].iter().position(|&x| x == 0) {
+            len = pos;
+        } else {
+            // If no null byte, insert one at the chosen length
+            bytes[len] = 0;
+        }
+    
+        let c_str = CStr::from_bytes_until_nul(&bytes).unwrap();
+        // Verify that count_bytes matches the adjusted length
+        assert_eq!(c_str.count_bytes(), len);
+        assert!(c_str.is_safe());
+    }
+
+    // pub const fn to_bytes(&self) -> &[u8]
+    #[kani::proof]
+    #[kani::unwind(32)]
+    fn check_to_bytes() {
+        const MAX_SIZE: usize = 32;
+        let string: [u8; MAX_SIZE] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&string);
+        let c_str = arbitrary_cstr(slice);
+
+        let bytes = c_str.to_bytes();
+        let end_idx = bytes.len();
+        // Comparison does not include the null byte
+        assert_eq!(bytes, &slice[..end_idx]);
+        assert!(c_str.is_safe());
+    }
+
+    // pub const fn to_bytes_with_nul(&self) -> &[u8]
+    #[kani::proof]
+    #[kani::unwind(33)]
+    fn check_to_bytes_with_nul() {
+        const MAX_SIZE: usize = 32;
+        let string: [u8; MAX_SIZE] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&string);
+        let c_str = arbitrary_cstr(slice);
+
+        let bytes = c_str.to_bytes_with_nul();
+        let end_idx = bytes.len();
+        // Comparison includes the null byte
+        assert_eq!(bytes, &slice[..end_idx]);
+        assert!(c_str.is_safe());
+    }
+}

Diff for: library/core/src/ptr/mut_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> *mut T {
     /// Returns `true` if the pointer is null.
@@ -400,6 +404,22 @@ impl<T: ?Sized> *mut 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
+    // Note: It is the caller's responsibility to ensure that `self` is non-null and properly aligned.
+    // These conditions are not verified as part of the preconditions.
+    #[requires(
+        // Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`
+        count.checked_mul(core::mem::size_of::<T>() as isize).is_some() &&
+        // Precondition 2: adding the computed offset to `self` does not cause overflow
+        (self as isize).checked_add((count * core::mem::size_of::<T>() as isize)).is_some() &&
+        // Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
+        // Otherwise, for non-unit types, `self` and `self.wrapping_offset(count)` should point to the same allocated object,
+        // restricting `count` to prevent crossing allocation boundaries.
+        ((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_offset(count))))
+    )]
+    // Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
+    // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
+    // verifying that the result remains within the same allocation as `self`.
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn offset(self, count: isize) -> *mut T
     where
         T: Sized,
@@ -998,6 +1018,23 @@ impl<T: ?Sized> *mut 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
+    // Note: It is the caller's responsibility to ensure that `self` is non-null and properly aligned.
+    // These conditions are not verified as part of the preconditions.
+    #[requires(
+        // Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`
+        count.checked_mul(core::mem::size_of::<T>()).is_some() &&
+        count * core::mem::size_of::<T>() <= isize::MAX as usize &&
+        // Precondition 2: adding the computed offset to `self` does not cause overflow
+        (self as isize).checked_add((count * core::mem::size_of::<T>()) as isize).is_some() &&
+        // Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
+        // Otherwise, for non-unit types, `self` and `self.wrapping_add(count)` should point to the same allocated object,
+        // restricting `count` to prevent crossing allocation boundaries.
+        ((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_add(count))))
+    )]
+    // Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
+    // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
+    // verifying that the result remains within the same allocation as `self`.
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn add(self, count: usize) -> Self
     where
         T: Sized,
@@ -1107,6 +1144,23 @@ impl<T: ?Sized> *mut T {
     #[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_neg))]
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    // Note: It is the caller's responsibility to ensure that `self` is non-null and properly aligned.
+    // These conditions are not verified as part of the preconditions.
+    #[requires(
+        // Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`
+        count.checked_mul(core::mem::size_of::<T>()).is_some() &&
+        count * core::mem::size_of::<T>() <= isize::MAX as usize &&
+        // Precondition 2: subtracting the computed offset from `self` does not cause overflow
+        (self as isize).checked_sub((count * core::mem::size_of::<T>()) as isize).is_some() &&
+        // Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
+        // Otherwise, for non-unit types, `self` and `self.wrapping_sub(count)` should point to the same allocated object,
+        // restricting `count` to prevent crossing allocation boundaries.
+        ((core::mem::size_of::<T>() == 0) || (kani::mem::same_allocation(self, self.wrapping_sub(count))))
+    )]
+    // Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
+    // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
+    // verifying that the result remains within the same allocation as `self`.
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || kani::mem::same_allocation(self as *const T, *result as *const T))]
     pub const unsafe fn sub(self, count: usize) -> Self
     where
         T: Sized,
@@ -2302,3 +2356,126 @@ impl<T: ?Sized> PartialOrd for *mut T {
         *self >= *other
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use crate::kani;
+
+    /// This macro generates proofs for contracts on `add`, `sub`, and `offset`
+    /// operations for pointers to integer, composite, and unit types.
+    /// - `$type`: Specifies the pointee type.
+    /// - `$proof_name`: Specifies the name of the generated proof for contract.
+    macro_rules! generate_mut_arithmetic_harness {
+        ($type:ty, $proof_name:ident, add) => {
+            #[kani::proof_for_contract(<*mut $type>::add)]
+            pub fn $proof_name() {
+                // 200 bytes are large enough to cover all pointee types used for testing
+                const BUF_SIZE: usize = 200;
+                let mut generator = kani::PointerGenerator::<BUF_SIZE>::new();
+                let test_ptr: *mut $type = generator.any_in_bounds().ptr;
+                let count: usize = kani::any();
+                unsafe {
+                    test_ptr.add(count);
+                }
+            }
+        };
+        ($type:ty, $proof_name:ident, sub) => {
+            #[kani::proof_for_contract(<*mut $type>::sub)]
+            pub fn $proof_name() {
+                // 200 bytes are large enough to cover all pointee types used for testing
+                const BUF_SIZE: usize = 200;
+                let mut generator = kani::PointerGenerator::<BUF_SIZE>::new();
+                let test_ptr: *mut $type = generator.any_in_bounds().ptr;
+                let count: usize = kani::any();
+                unsafe {
+                    test_ptr.sub(count);
+                }
+            }
+        };
+        ($type:ty, $proof_name:ident, offset) => {
+            #[kani::proof_for_contract(<*mut $type>::offset)]
+            pub fn $proof_name() {
+                // 200 bytes are large enough to cover all pointee types used for testing
+                const BUF_SIZE: usize = 200;
+                let mut generator = kani::PointerGenerator::<BUF_SIZE>::new();
+                let test_ptr: *mut $type = generator.any_in_bounds().ptr;
+                let count: isize = kani::any();
+                unsafe {
+                    test_ptr.offset(count);
+                }
+            }
+        };
+    }
+
+    // <*mut T>:: add() integer types verification
+    generate_mut_arithmetic_harness!(i8, check_mut_add_i8, add);
+    generate_mut_arithmetic_harness!(i16, check_mut_add_i16, add);
+    generate_mut_arithmetic_harness!(i32, check_mut_add_i32, add);
+    generate_mut_arithmetic_harness!(i64, check_mut_add_i64, add);
+    generate_mut_arithmetic_harness!(i128, check_mut_add_i128, add);
+    generate_mut_arithmetic_harness!(isize, check_mut_add_isize, add);
+    // Due to a bug of kani this test case is malfunctioning for now.
+    // Tracking issue: https://github.com/model-checking/kani/issues/3743
+    // generate_mut_arithmetic_harness!(u8, check_mut_add_u8, add);
+    generate_mut_arithmetic_harness!(u16, check_mut_add_u16, add);
+    generate_mut_arithmetic_harness!(u32, check_mut_add_u32, add);
+    generate_mut_arithmetic_harness!(u64, check_mut_add_u64, add);
+    generate_mut_arithmetic_harness!(u128, check_mut_add_u128, add);
+    generate_mut_arithmetic_harness!(usize, check_mut_add_usize, add);
+
+    // <*mut T>:: add() unit type verification
+    generate_mut_arithmetic_harness!((), check_mut_add_unit, add);
+
+    // <*mut T>:: add() composite types verification
+    generate_mut_arithmetic_harness!((i8, i8), check_mut_add_tuple_1, add);
+    generate_mut_arithmetic_harness!((f64, bool), check_mut_add_tuple_2, add);
+    generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_add_tuple_3, add);
+    generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_add_tuple_4, add);
+
+    // <*mut T>:: sub() integer types verification
+    generate_mut_arithmetic_harness!(i8, check_mut_sub_i8, sub);
+    generate_mut_arithmetic_harness!(i16, check_mut_sub_i16, sub);
+    generate_mut_arithmetic_harness!(i32, check_mut_sub_i32, sub);
+    generate_mut_arithmetic_harness!(i64, check_mut_sub_i64, sub);
+    generate_mut_arithmetic_harness!(i128, check_mut_sub_i128, sub);
+    generate_mut_arithmetic_harness!(isize, check_mut_sub_isize, sub);
+    generate_mut_arithmetic_harness!(u8, check_mut_sub_u8, sub);
+    generate_mut_arithmetic_harness!(u16, check_mut_sub_u16, sub);
+    generate_mut_arithmetic_harness!(u32, check_mut_sub_u32, sub);
+    generate_mut_arithmetic_harness!(u64, check_mut_sub_u64, sub);
+    generate_mut_arithmetic_harness!(u128, check_mut_sub_u128, sub);
+    generate_mut_arithmetic_harness!(usize, check_mut_sub_usize, sub);
+
+    // <*mut T>:: sub() unit type verification
+    generate_mut_arithmetic_harness!((), check_mut_sub_unit, sub);
+
+    // <*mut T>:: sub() composite types verification
+    generate_mut_arithmetic_harness!((i8, i8), check_mut_sub_tuple_1, sub);
+    generate_mut_arithmetic_harness!((f64, bool), check_mut_sub_tuple_2, sub);
+    generate_mut_arithmetic_harness!((i32, f64, bool), check_mut_sub_tuple_3, sub);
+    generate_mut_arithmetic_harness!((i8, u16, i32, u64, isize), check_mut_sub_tuple_4, sub);
+
+    // fn <*mut T>::offset() integer types verification
+    generate_mut_arithmetic_harness!(i8, check_mut_offset_i8, offset);
+    generate_mut_arithmetic_harness!(i16, check_mut_offset_i16, offset);
+    generate_mut_arithmetic_harness!(i32, check_mut_offset_i32, offset);
+    generate_mut_arithmetic_harness!(i64, check_mut_offset_i64, offset);
+    generate_mut_arithmetic_harness!(i128, check_mut_offset_i128, offset);
+    generate_mut_arithmetic_harness!(isize, check_mut_offset_isize, offset);
+    generate_mut_arithmetic_harness!(u8, check_mut_offset_u8, offset);
+    generate_mut_arithmetic_harness!(u16, check_mut_offset_u16, offset);
+    generate_mut_arithmetic_harness!(u32, check_mut_offset_u32, offset);
+    generate_mut_arithmetic_harness!(u64, check_mut_offset_u64, offset);
+    generate_mut_arithmetic_harness!(u128, check_mut_offset_u128, offset);
+    generate_mut_arithmetic_harness!(usize, check_mut_offset_usize, offset);
+
+    // fn <*mut T>::offset() unit type verification
+    generate_mut_arithmetic_harness!((), check_mut_offset_unit, offset);
+
+    // fn <*mut T>::offset() composite type verification
+    generate_mut_arithmetic_harness!((i8, i8), check_mut_offset_tuple_1, offset);
+    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);
+}