From 1bc79060fe4a4d415983658357bacda867e6ee34 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 1 Nov 2024 18:30:38 -0700
Subject: [PATCH 1/5] Start the verification of slice::Iter

There are a few harnesses failing that needs further debugging.
I commented them out for now.
---
 library/core/src/slice/iter.rs        | 160 ++++++++++++++++++++++++++
 library/core/src/slice/iter/macros.rs |  11 ++
 library/core/src/ub_checks.rs         |  10 +-
 3 files changed, 180 insertions(+), 1 deletion(-)

diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs
index c5746157d01b2..04f4fd591c3b6 100644
--- a/library/core/src/slice/iter.rs
+++ b/library/core/src/slice/iter.rs
@@ -14,6 +14,11 @@ use crate::num::NonZero;
 use crate::ptr::{NonNull, without_provenance, without_provenance_mut};
 use crate::{cmp, fmt};
 
+#[cfg(kani)]
+use crate::kani;
+
+use crate::ub_checks::Invariant;
+
 #[stable(feature = "boxed_slice_into_iter", since = "1.80.0")]
 impl<T> !Iterator for [T] {}
 
@@ -157,6 +162,23 @@ impl<T> AsRef<[T]> for Iter<'_, T> {
     }
 }
 
+#[unstable(feature = "ub_checks", issue = "none")]
+impl<T> crate::ub_checks::Invariant for Iter<'_, T> {
+    fn is_safe(&self) -> bool {
+        let ty_size = crate::mem::size_of::<T>();
+        let distance = self.ptr.addr().get().abs_diff(self.end_or_len as usize);
+        if ty_size == 0 || distance == 0 {
+            self.ptr.is_aligned()
+        } else {
+            let slice_ptr: *const [T] = crate::ptr::from_raw_parts(self.ptr.as_ptr(), distance / ty_size);
+            crate::ub_checks::same_allocation(self.ptr.as_ptr(), self.end_or_len)
+                && self.ptr.addr().get() <= self.end_or_len as usize
+                && distance % ty_size == 0
+                && crate::ub_checks::can_dereference(slice_ptr)
+        }
+    }
+}
+
 /// Mutable slice iterator.
 ///
 /// This struct is created by the [`iter_mut`] method on [slices].
@@ -196,6 +218,24 @@ pub struct IterMut<'a, T: 'a> {
     _marker: PhantomData<&'a mut T>,
 }
 
+#[unstable(feature = "ub_checks", issue = "none")]
+impl<T> crate::ub_checks::Invariant for IterMut<'_, T> {
+    fn is_safe(&self) -> bool {
+        let size = crate::mem::size_of::<T>();
+        if size == 0 {
+            self.ptr.is_aligned()
+        } else {
+            let distance = self.ptr.addr().get().abs_diff(self.end_or_len as usize);
+            let slice_ptr: *mut [T] = crate::ptr::from_raw_parts_mut(self.ptr.as_ptr(), distance / size);
+            crate::ub_checks::same_allocation(self.ptr.as_ptr(), self.end_or_len)
+                && self.ptr.addr().get() <= self.end_or_len as usize
+                && distance % size == 0
+                && crate::ub_checks::can_dereference(slice_ptr)
+                && crate::ub_checks::can_write(slice_ptr)
+        }
+    }
+}
+
 #[stable(feature = "core_impl_debug", since = "1.9.0")]
 impl<T: fmt::Debug> fmt::Debug for IterMut<'_, T> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
@@ -3464,3 +3504,123 @@ impl<'a, T: 'a + fmt::Debug, P> fmt::Debug for ChunkByMut<'a, T, P> {
         f.debug_struct("ChunkByMut").field("slice", &self.slice).finish()
     }
 }
+
+/// Verify the safety of the code implemented in this module (including generated code from macros).
+#[unstable(feature = "kani", issue="none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig_slice: &[T]) -> &[T] {
+        if kani::any() {
+            let first = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let last = kani::any_where(|idx: &usize| *idx >= first && *idx <= orig_slice.len());
+            &orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    fn any_iter<'a, T>(orig_slice: &'a [T]) -> Iter<'a, T> {
+        let slice = any_slice(orig_slice);
+        Iter::new(slice)
+    }
+
+    /// Macro that generates a harness for a given `Iter` method.
+    ///
+    /// Takes the name of the harness, the element type, and an expression to check.
+    macro_rules! check_safe_abstraction {
+        ($harness:ident, $elem_ty:ty, $call:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut iter = any_iter::<$elem_ty>(&array);
+                let target = $call;
+                target(&mut iter);
+                kani::assert(iter.is_safe(), "Iter is safe");
+            }
+        };
+    }
+
+    /// Macro that generates a harness for a given unsafe `Iter` method.
+    ///
+    /// Takes:
+    /// 1. The name of the harness
+    /// 2. the element type
+    /// 3. the target function
+    /// 4. the optional arguments.
+    macro_rules! check_unsafe_contracts {
+        ($harness:ident, $elem_ty:ty, $func:ident($($args:expr),*)) => {
+            #[kani::proof_for_contract(Iter::$func)]
+            fn $harness() {
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut iter = any_iter::<$elem_ty>(&array);
+                let _ = unsafe { iter.$func($($args),*) };
+            }
+        };
+    }
+
+    macro_rules! check_iter_with_ty {
+        ($module:ident, $ty:ty, $max:expr) => {
+            mod $module {
+                use super::*;
+                const MAX_LEN: usize = $max;
+
+                #[kani::proof]
+                fn check_new_iter() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_slice::<$ty>(&array);
+                    let mut iter = Iter::new(slice);
+                    kani::assert(iter.is_safe(), "Iter is safe");
+                }
+
+                /// Count consumes the value, thus, invoke it directly.
+                #[kani::proof]
+                fn check_count() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let mut iter = any_iter::<$ty>(&array);
+                    iter.count();
+                }
+
+                #[kani::proof]
+                fn check_default() {
+                    let iter: Iter<'_, $ty> = Iter::default();
+                    kani::assert(iter.is_safe(), "Iter is safe");
+                }
+
+                check_unsafe_contracts!(check_next_back_unchecked, $ty, next_back_unchecked());
+                //check_unsafe_contracts!(check_post_inc_start, $ty, post_inc_start(kani::any()));
+                //check_unsafe_contracts!(check_pre_dec_end, $ty, pre_dec_end(kani::any()));
+
+                // FIXME: The functions that are commented out are currently failing verification.
+                // Debugging the issue is currently blocked by:
+                // https://github.com/model-checking/kani/issues/3670
+                //
+                // Public functions that call safe abstraction `make_slice`.
+                // check_safe_abstraction!(check_as_slice, $ty, as_slice);
+                // check_safe_abstraction!(check_as_ref, $ty, as_ref);
+
+                // check_safe_abstraction!(check_advance_back_by, $ty, advance_back_by, kani::any());
+
+                check_safe_abstraction!(check_is_empty, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.is_empty(); });
+                check_safe_abstraction!(check_len, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.len(); });
+                check_safe_abstraction!(check_size_hint, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.size_hint(); });
+                //check_safe_abstraction!(check_nth, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth(kani::any()); });
+                //check_safe_abstraction!(check_advance_by, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.advance_by(kani::any()); });
+                //check_safe_abstraction!(check_next_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.next_back(); });
+                //check_safe_abstraction!(check_nth_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth_back(kani::any()); });
+                check_safe_abstraction!(check_next, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.next(); });
+
+                // Ensure that clone always generates a safe object.
+                check_safe_abstraction!(check_clone, $ty, |iter: &mut Iter<'_, $ty>| { kani::assert(iter.clone().is_safe(), "Clone is safe"); });
+            }
+        };
+    }
+
+    check_iter_with_ty!(verify_unit, (), isize::MAX as usize);
+    check_iter_with_ty!(verify_u8, u8, u32::MAX as usize);
+    check_iter_with_ty!(verify_char, char, 50);
+    check_iter_with_ty!(verify_tup, (char, u8), 50);
+}
\ No newline at end of file
diff --git a/library/core/src/slice/iter/macros.rs b/library/core/src/slice/iter/macros.rs
index 830debe02ea2b..29438921d6690 100644
--- a/library/core/src/slice/iter/macros.rs
+++ b/library/core/src/slice/iter/macros.rs
@@ -77,6 +77,9 @@ macro_rules! iterator {
             ///
             /// The iterator must not be empty
             #[inline]
+            #[cfg_attr(kani, kani::modifies(self))]
+            #[safety::requires(!is_empty!(self))]
+            #[safety::ensures(|_| self.is_safe())]
             unsafe fn next_back_unchecked(&mut self) -> $elem {
                 // SAFETY: the caller promised it's not empty, so
                 // the offsetting is in-bounds and there's an element to return.
@@ -96,6 +99,9 @@ macro_rules! iterator {
             // returning the old start.
             // Unsafe because the offset must not exceed `self.len()`.
             #[inline(always)]
+            #[cfg_attr(kani, kani::modifies(self))]
+            #[safety::requires(offset <= len!(self))]
+            #[safety::ensures(|_| self.is_safe())]
             unsafe fn post_inc_start(&mut self, offset: usize) -> NonNull<T> {
                 let old = self.ptr;
 
@@ -115,6 +121,9 @@ macro_rules! iterator {
             // returning the new end.
             // Unsafe because the offset must not exceed `self.len()`.
             #[inline(always)]
+            #[cfg_attr(kani, kani::modifies(self))]
+            #[safety::requires(offset <= len!(self))]
+            #[safety::ensures(|_| self.is_safe())]
             unsafe fn pre_dec_end(&mut self, offset: usize) -> NonNull<T> {
                 if_zst!(mut self,
                     // SAFETY: By our precondition, `offset` can be at most the
@@ -369,6 +378,7 @@ macro_rules! iterator {
             }
 
             #[inline]
+            #[safety::requires(idx < len!(self))]
             unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item {
                 // SAFETY: the caller must guarantee that `i` is in bounds of
                 // the underlying slice, so `i` cannot overflow an `isize`, and
@@ -437,6 +447,7 @@ macro_rules! iterator {
 
         impl<'a, T> UncheckedIterator for $name<'a, T> {
             #[inline]
+            #[safety::requires(!is_empty!(self))]
             unsafe fn next_unchecked(&mut self) -> $elem {
                 // SAFETY: The caller promised there's at least one more item.
                 unsafe {
diff --git a/library/core/src/ub_checks.rs b/library/core/src/ub_checks.rs
index 64b7c11b38cd5..fd0d3c64e2619 100644
--- a/library/core/src/ub_checks.rs
+++ b/library/core/src/ub_checks.rs
@@ -171,6 +171,7 @@ pub use predicates::*;
 /// Provide a few predicates to be used in safety contracts.
 ///
 /// At runtime, they are no-op, and always return true.
+/// FIXME: In some cases, we could do better, for example check if not null and aligned.
 #[cfg(not(kani))]
 mod predicates {
     /// Checks if a pointer can be dereferenced, ensuring:
@@ -207,11 +208,18 @@ mod predicates {
         let _ = dst;
         true
     }
+
+    /// Checks if two pointers point to the same allocation.
+    pub fn same_allocation<T>(src: *const T, dst: *const T) -> bool {
+        let _ = (src, dst);
+        true
+    }
 }
 
 #[cfg(kani)]
 mod predicates {
-    pub use crate::kani::mem::{can_dereference, can_write, can_read_unaligned, can_write_unaligned};
+    pub use crate::kani::mem::{can_dereference, can_write, can_read_unaligned, can_write_unaligned,
+    same_allocation};
 }
 
 /// This trait should be used to specify and check type safety invariants for a

From 0a70327820e82248ae016791fa10469098a0b5bb Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Sat, 2 Nov 2024 17:20:01 -0700
Subject: [PATCH 2/5] Fix rustc compilation and code format

---
 library/core/src/slice/iter.rs | 45 ++++++++++++++++++++++------------
 library/core/src/ub_checks.rs  | 10 ++++----
 2 files changed, 34 insertions(+), 21 deletions(-)

diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs
index 04f4fd591c3b6..1daa074162f26 100644
--- a/library/core/src/slice/iter.rs
+++ b/library/core/src/slice/iter.rs
@@ -8,15 +8,13 @@ use crate::hint::assert_unchecked;
 use crate::iter::{
     FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce, UncheckedIterator,
 };
+#[cfg(kani)]
+use crate::kani;
 use crate::marker::PhantomData;
 use crate::mem::{self, SizedTypeProperties};
 use crate::num::NonZero;
 use crate::ptr::{NonNull, without_provenance, without_provenance_mut};
 use crate::{cmp, fmt};
-
-#[cfg(kani)]
-use crate::kani;
-
 use crate::ub_checks::Invariant;
 
 #[stable(feature = "boxed_slice_into_iter", since = "1.80.0")]
@@ -163,14 +161,15 @@ impl<T> AsRef<[T]> for Iter<'_, T> {
 }
 
 #[unstable(feature = "ub_checks", issue = "none")]
-impl<T> crate::ub_checks::Invariant for Iter<'_, T> {
+impl<T> Invariant for Iter<'_, T> {
     fn is_safe(&self) -> bool {
         let ty_size = crate::mem::size_of::<T>();
         let distance = self.ptr.addr().get().abs_diff(self.end_or_len as usize);
         if ty_size == 0 || distance == 0 {
             self.ptr.is_aligned()
         } else {
-            let slice_ptr: *const [T] = crate::ptr::from_raw_parts(self.ptr.as_ptr(), distance / ty_size);
+            let slice_ptr: *const [T] =
+                crate::ptr::from_raw_parts(self.ptr.as_ptr(), distance / ty_size);
             crate::ub_checks::same_allocation(self.ptr.as_ptr(), self.end_or_len)
                 && self.ptr.addr().get() <= self.end_or_len as usize
                 && distance % ty_size == 0
@@ -219,14 +218,15 @@ pub struct IterMut<'a, T: 'a> {
 }
 
 #[unstable(feature = "ub_checks", issue = "none")]
-impl<T> crate::ub_checks::Invariant for IterMut<'_, T> {
+impl<T> Invariant for IterMut<'_, T> {
     fn is_safe(&self) -> bool {
         let size = crate::mem::size_of::<T>();
         if size == 0 {
             self.ptr.is_aligned()
         } else {
             let distance = self.ptr.addr().get().abs_diff(self.end_or_len as usize);
-            let slice_ptr: *mut [T] = crate::ptr::from_raw_parts_mut(self.ptr.as_ptr(), distance / size);
+            let slice_ptr: *mut [T] =
+                crate::ptr::from_raw_parts_mut(self.ptr.as_ptr(), distance / size);
             crate::ub_checks::same_allocation(self.ptr.as_ptr(), self.end_or_len)
                 && self.ptr.addr().get() <= self.end_or_len as usize
                 && distance % size == 0
@@ -3506,7 +3506,8 @@ impl<'a, T: 'a + fmt::Debug, P> fmt::Debug for ChunkByMut<'a, T, P> {
 }
 
 /// Verify the safety of the code implemented in this module (including generated code from macros).
-#[unstable(feature = "kani", issue="none")]
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
 mod verify {
     use super::*;
     use crate::kani;
@@ -3604,17 +3605,29 @@ mod verify {
 
                 // check_safe_abstraction!(check_advance_back_by, $ty, advance_back_by, kani::any());
 
-                check_safe_abstraction!(check_is_empty, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.is_empty(); });
-                check_safe_abstraction!(check_len, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.len(); });
-                check_safe_abstraction!(check_size_hint, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.size_hint(); });
+                check_safe_abstraction!(check_is_empty, $ty, |iter: &mut Iter<'_, $ty>| {
+                    let _ = iter.is_empty();
+                });
+                check_safe_abstraction!(check_len, $ty, |iter: &mut Iter<'_, $ty>| {
+                    let _ = iter.len();
+                });
+                check_safe_abstraction!(check_size_hint, $ty, |iter: &mut Iter<'_, $ty>| {
+                    let _ = iter.size_hint();
+                });
                 //check_safe_abstraction!(check_nth, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth(kani::any()); });
                 //check_safe_abstraction!(check_advance_by, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.advance_by(kani::any()); });
-                //check_safe_abstraction!(check_next_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.next_back(); });
+                check_safe_abstraction!(check_next_back, $ty, |iter: &mut Iter<'_, $ty>| {
+                    let _ = iter.next_back();
+                });
                 //check_safe_abstraction!(check_nth_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth_back(kani::any()); });
-                check_safe_abstraction!(check_next, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.next(); });
+                check_safe_abstraction!(check_next, $ty, |iter: &mut Iter<'_, $ty>| {
+                    let _ = iter.next();
+                });
 
                 // Ensure that clone always generates a safe object.
-                check_safe_abstraction!(check_clone, $ty, |iter: &mut Iter<'_, $ty>| { kani::assert(iter.clone().is_safe(), "Clone is safe"); });
+                check_safe_abstraction!(check_clone, $ty, |iter: &mut Iter<'_, $ty>| {
+                    kani::assert(iter.clone().is_safe(), "Clone is safe");
+                });
             }
         };
     }
@@ -3623,4 +3636,4 @@ mod verify {
     check_iter_with_ty!(verify_u8, u8, u32::MAX as usize);
     check_iter_with_ty!(verify_char, char, 50);
     check_iter_with_ty!(verify_tup, (char, u8), 50);
-}
\ No newline at end of file
+}
diff --git a/library/core/src/ub_checks.rs b/library/core/src/ub_checks.rs
index fd0d3c64e2619..d3e4ee4bda8d2 100644
--- a/library/core/src/ub_checks.rs
+++ b/library/core/src/ub_checks.rs
@@ -180,7 +180,7 @@ mod predicates {
     ///   * `src` points to a properly initialized value of type `T`.
     ///
     /// [`crate::ptr`]: https://doc.rust-lang.org/std/ptr/index.html
-    pub fn can_dereference<T>(src: *const T) -> bool {
+    pub fn can_dereference<T: ?Sized>(src: *const T) -> bool {
         let _ = src;
         true
     }
@@ -189,7 +189,7 @@ mod predicates {
     /// * `dst` must be valid for writes.
     /// * `dst` must be properly aligned. Use `write_unaligned` if this is not the
     ///    case.
-    pub fn can_write<T>(dst: *mut T) -> bool {
+    pub fn can_write<T: ?Sized>(dst: *mut T) -> bool {
         let _ = dst;
         true
     }
@@ -197,20 +197,20 @@ mod predicates {
     /// Check if a pointer can be the target of unaligned reads.
     /// * `src` must be valid for reads.
     /// * `src` must point to a properly initialized value of type `T`.
-    pub fn can_read_unaligned<T>(src: *const T) -> bool {
+    pub fn can_read_unaligned<T: ?Sized>(src: *const T) -> bool {
         let _ = src;
         true
     }
 
     /// Check if a pointer can be the target of unaligned writes.
     /// * `dst` must be valid for writes.
-    pub fn can_write_unaligned<T>(dst: *mut T) -> bool {
+    pub fn can_write_unaligned<T: ?Sized>(dst: *mut T) -> bool {
         let _ = dst;
         true
     }
 
     /// Checks if two pointers point to the same allocation.
-    pub fn same_allocation<T>(src: *const T, dst: *const T) -> bool {
+    pub fn same_allocation<T: ?Sized>(src: *const T, dst: *const T) -> bool {
         let _ = (src, dst);
         true
     }

From 85ea71edd6b43317245c3ea1d62b0eaa021b4c52 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Mon, 4 Nov 2024 11:27:13 -0800
Subject: [PATCH 3/5] Add comments to the `Invariant` implementation

---
 library/core/src/slice/iter.rs | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs
index 1daa074162f26..4a6e2abf48587 100644
--- a/library/core/src/slice/iter.rs
+++ b/library/core/src/slice/iter.rs
@@ -162,11 +162,19 @@ impl<T> AsRef<[T]> for Iter<'_, T> {
 
 #[unstable(feature = "ub_checks", issue = "none")]
 impl<T> Invariant for Iter<'_, T> {
+    /// An iterator can be safely used if its pointer can be read for its current length.
+    ///
+    /// If the type is a ZST or the encoded length is `0`, the only safety requirement is that
+    /// its pointer is aligned (since zero-size access is always safe for aligned pointers),
+    /// and that `self.ptr` value is less or equal to `self.end_or_len`.
+    ///
+    /// For other cases, we need to ensure that it is safe to read the memory between
+    /// `self.ptr` and `self.end_or_len`.
     fn is_safe(&self) -> bool {
         let ty_size = crate::mem::size_of::<T>();
         let distance = self.ptr.addr().get().abs_diff(self.end_or_len as usize);
         if ty_size == 0 || distance == 0 {
-            self.ptr.is_aligned()
+            self.ptr.is_aligned() && self.ptr.addr().get() <= self.end_or_len as usize
         } else {
             let slice_ptr: *const [T] =
                 crate::ptr::from_raw_parts(self.ptr.as_ptr(), distance / ty_size);
@@ -219,10 +227,14 @@ pub struct IterMut<'a, T: 'a> {
 
 #[unstable(feature = "ub_checks", issue = "none")]
 impl<T> Invariant for IterMut<'_, T> {
+    /// This is similar to [Iter] with an extra write requirement.
+    ///
+    /// It must be safe to write in the memory interval between `self.ptr`
+    /// and `self.end_or_len`.
     fn is_safe(&self) -> bool {
         let size = crate::mem::size_of::<T>();
         if size == 0 {
-            self.ptr.is_aligned()
+            self.ptr.is_aligned() && self.ptr.addr().get() <= self.end_or_len as usize
         } else {
             let distance = self.ptr.addr().get().abs_diff(self.end_or_len as usize);
             let slice_ptr: *mut [T] =
@@ -3632,6 +3644,7 @@ mod verify {
         };
     }
 
+    // FIXME: Add harnesses for ZST with alignment > 1.
     check_iter_with_ty!(verify_unit, (), isize::MAX as usize);
     check_iter_with_ty!(verify_u8, u8, u32::MAX as usize);
     check_iter_with_ty!(verify_char, char, 50);

From 07af6fb70b7c49c20aa4b93480a377480b215570 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Mon, 4 Nov 2024 18:11:27 -0800
Subject: [PATCH 4/5] Fix invariant for Iter/IterMut

---
 library/core/src/slice/iter.rs | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs
index 4a6e2abf48587..ad6c0aac09448 100644
--- a/library/core/src/slice/iter.rs
+++ b/library/core/src/slice/iter.rs
@@ -165,8 +165,7 @@ impl<T> Invariant for Iter<'_, T> {
     /// An iterator can be safely used if its pointer can be read for its current length.
     ///
     /// If the type is a ZST or the encoded length is `0`, the only safety requirement is that
-    /// its pointer is aligned (since zero-size access is always safe for aligned pointers),
-    /// and that `self.ptr` value is less or equal to `self.end_or_len`.
+    /// its pointer is aligned (since zero-size access is always safe for aligned pointers).
     ///
     /// For other cases, we need to ensure that it is safe to read the memory between
     /// `self.ptr` and `self.end_or_len`.
@@ -174,7 +173,7 @@ impl<T> Invariant for Iter<'_, T> {
         let ty_size = crate::mem::size_of::<T>();
         let distance = self.ptr.addr().get().abs_diff(self.end_or_len as usize);
         if ty_size == 0 || distance == 0 {
-            self.ptr.is_aligned() && self.ptr.addr().get() <= self.end_or_len as usize
+            self.ptr.is_aligned()
         } else {
             let slice_ptr: *const [T] =
                 crate::ptr::from_raw_parts(self.ptr.as_ptr(), distance / ty_size);
@@ -232,16 +231,16 @@ impl<T> Invariant for IterMut<'_, T> {
     /// It must be safe to write in the memory interval between `self.ptr`
     /// and `self.end_or_len`.
     fn is_safe(&self) -> bool {
-        let size = crate::mem::size_of::<T>();
-        if size == 0 {
-            self.ptr.is_aligned() && self.ptr.addr().get() <= self.end_or_len as usize
+        let ty_size = crate::mem::size_of::<T>();
+        let distance = self.ptr.addr().get().abs_diff(self.end_or_len as usize);
+        if ty_size == 0 || distance == 0 {
+            self.ptr.is_aligned()
         } else {
-            let distance = self.ptr.addr().get().abs_diff(self.end_or_len as usize);
-            let slice_ptr: *mut [T] =
-                crate::ptr::from_raw_parts_mut(self.ptr.as_ptr(), distance / size);
+            let slice_ptr: *const [T] =
+                crate::ptr::from_raw_parts(self.ptr.as_ptr(), distance / ty_size);
             crate::ub_checks::same_allocation(self.ptr.as_ptr(), self.end_or_len)
                 && self.ptr.addr().get() <= self.end_or_len as usize
-                && distance % size == 0
+                && distance % ty_size == 0
                 && crate::ub_checks::can_dereference(slice_ptr)
                 && crate::ub_checks::can_write(slice_ptr)
         }

From 432145c1134961a8ff85f9767addfec1c6aacdc2 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 5 Nov 2024 11:22:44 -0800
Subject: [PATCH 5/5] Address PR feedback

  - Improve first / last logic
  - Add comment to invariant
  - Fix IterMut invariant
---
 library/core/src/slice/iter.rs | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs
index ad6c0aac09448..5005563233d2d 100644
--- a/library/core/src/slice/iter.rs
+++ b/library/core/src/slice/iter.rs
@@ -171,6 +171,7 @@ impl<T> Invariant for Iter<'_, T> {
     /// `self.ptr` and `self.end_or_len`.
     fn is_safe(&self) -> bool {
         let ty_size = crate::mem::size_of::<T>();
+        // Use `abs_diff` since `end_or_len` may be smaller than `ptr` if `T` is a ZST.
         let distance = self.ptr.addr().get().abs_diff(self.end_or_len as usize);
         if ty_size == 0 || distance == 0 {
             self.ptr.is_aligned()
@@ -236,8 +237,8 @@ impl<T> Invariant for IterMut<'_, T> {
         if ty_size == 0 || distance == 0 {
             self.ptr.is_aligned()
         } else {
-            let slice_ptr: *const [T] =
-                crate::ptr::from_raw_parts(self.ptr.as_ptr(), distance / ty_size);
+            let slice_ptr: *mut [T] =
+                crate::ptr::from_raw_parts_mut(self.ptr.as_ptr(), distance / ty_size);
             crate::ub_checks::same_allocation(self.ptr.as_ptr(), self.end_or_len)
                 && self.ptr.addr().get() <= self.end_or_len as usize
                 && distance % ty_size == 0
@@ -3525,8 +3526,8 @@ mod verify {
 
     fn any_slice<T>(orig_slice: &[T]) -> &[T] {
         if kani::any() {
-            let first = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
-            let last = kani::any_where(|idx: &usize| *idx >= first && *idx <= orig_slice.len());
+            let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let first = kani::any_where(|idx: &usize| *idx <= last);
             &orig_slice[first..last]
         } else {
             let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;