Add loop contracts and harness for ptr::swap_nonoverlapping_simple_untyped

Author: qinheping

library/alloc/src/lib.rs

@@ -193,6 +193,7 @@
 #![feature(unboxed_closures)]
 #![feature(unsized_fn_params)]
 #![feature(with_negative_coherence)]
+#![cfg_attr(kani, feature(proc_macro_hygiene))]
 #![rustc_preserve_ub_checks]
 // tidy-alphabetical-end
 //

library/core/src/ptr/mod.rs

@@ -1202,6 +1202,7 @@ const unsafe fn swap_nonoverlapping_simple_untyped<T>(x: *mut T, y: *mut T, coun
     let x = x.cast::<MaybeUninit<T>>();
     let y = y.cast::<MaybeUninit<T>>();
     let mut i = 0;
+    #[safety::loop_invariant(i <= count)]
     while i < count {
         // SAFETY: By precondition, `i` is in-bounds because it's below `n`
         let x = unsafe { x.add(i) };
@@ -2623,4 +2624,18 @@ mod verify {
         let m = kani::any::<usize>();
         unsafe { mod_inv_copy(x, m) };
     }
+
+    #[kani::proof]
+    pub fn check_swap_nonoverlapping_simple_untyped() {
+        const ARR_SIZE: usize = (2 << 32) -1;
+        let mut x: [u8; ARR_SIZE] = kani::any();
+        let mut xs = kani::slice::any_slice_of_array_mut(&mut x);
+        let mut y: [u8; ARR_SIZE] = kani::any();
+        let mut ys = kani::slice::any_slice_of_array_mut(&mut y);
+        let s: usize = kani::any_where(|v| *v <= xs.len() && *v <= ys.len());
+        unsafe {
+            swap_nonoverlapping_simple_untyped(xs.as_mut_ptr(), ys.as_mut_ptr(), s);
+        }
+}
+
 }