Remove proof without contracts for testing

Author: qinheping

library/core/src/alloc/layout.rs

@@ -655,7 +655,7 @@ mod verify {
     }
 
     // pub const fn size(&self) -> usize
-    #[kani::proof]
+    //#[kani::proof]
     pub fn check_size() {
         let s = kani::any::<usize>();
         let a = kani::any::<usize>();
@@ -667,7 +667,7 @@ mod verify {
     }
 
     // pub const fn align(&self) -> usize
-    #[kani::proof]
+    //#[kani::proof]
     pub fn check_align() {
         let layout = kani::any::<Layout>();
         assert!(layout.align().is_power_of_two());

library/core/src/lib.rs

@@ -230,6 +230,7 @@
 #![feature(unboxed_closures)]
 #![feature(unsized_fn_params)]
 #![feature(with_negative_coherence)]
+#![cfg_attr(kani, feature(proc_macro_hygiene))]
 // tidy-alphabetical-end
 //
 // Target features:
@@ -247,7 +248,6 @@
 #![feature(tbm_target_feature)]
 #![feature(wasm_target_feature)]
 #![feature(x86_amx_intrinsics)]
-#![cfg_attr(kani, feature(proc_macro_hygiene))]
 // tidy-alphabetical-end
 
 // allow using `core::` in intra-doc links

library/core/src/num/mod.rs

@@ -1770,7 +1770,7 @@ mod verify {
     macro_rules! generate_carrying_mul_intervals {
         ($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => {
             $(
-                #[kani::proof]
+                //#[kani::proof]
                 pub fn $harness_name() {
                     let lhs: $type = kani::any::<$type>();
                     let rhs: $type = kani::any::<$type>();
@@ -1807,7 +1807,7 @@ mod verify {
     macro_rules! generate_widening_mul_intervals {
         ($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => {
             $(
-                #[kani::proof]
+                //#[kani::proof]
                 pub fn $harness_name() {
                     let lhs: $type = kani::any::<$type>();
                     let rhs: $type = kani::any::<$type>();

library/core/src/ptr/unique.rs

@@ -263,7 +263,7 @@ mod verify {
     }
 
     // pub const unsafe fn as_ref(&self) -> &T
-    #[kani::proof]
+    //#[kani::proof]
     pub fn check_as_ref() {
         let mut x : i32 = kani::any();
         let xptr = &mut x;
@@ -274,7 +274,7 @@ mod verify {
     }
 
     // pub const unsafe fn as_mut(&mut self) -> &mut T
-    #[kani::proof]
+    //#[kani::proof]
     pub fn check_as_mut() {
         let mut x : i32 = kani::any();
         let xptr = &mut x;
@@ -285,7 +285,7 @@ mod verify {
     }
 
     // pub const fn cast<U>(self) -> Unique<U>
-    #[kani::proof]
+    //#[kani::proof]
     pub fn check_cast() {
         let mut x : i32 = kani::any();
         let xptr = &mut x;

library/core/src/str/pattern.rs

@@ -1959,10 +1959,10 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
     unsafe {
         let (mut px, mut py) = (x.as_ptr(), y.as_ptr());
         let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4));
-        #[cfg_attr(kani, kani::loop_invariant(same_allocation(x.as_ptr(), px) && same_allocation(y.as_ptr(), py)
+        #[safety::loop_invariant(same_allocation(x.as_ptr(), px) && same_allocation(y.as_ptr(), py)
         && px as isize >= x.as_ptr() as isize
         && py as isize >= y.as_ptr() as isize
-        && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize)))]
+        && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize))]
         while px < pxend {
             let vx = (px as *const u32).read_unaligned();
             let vy = (py as *const u32).read_unaligned();
@@ -1983,30 +1983,17 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
 pub mod verify {
     use super::*;
 
-    // Copied from https://github.com/model-checking/kani/blob/main/library/kani/src/slice.rs
-    // should be removed when these functions are moved to `kani_core`
-    pub fn any_slice_of_array<T, const LENGTH: usize>(arr: &[T; LENGTH]) -> &[T] {
-        let (from, to) = any_range::<LENGTH>();
-        &arr[from..to]
-    }
-
-    fn any_range<const LENGTH: usize>() -> (usize, usize) {
-        let from: usize = kani::any();
-        let to: usize = kani::any();
-        kani::assume(to <= LENGTH);
-        kani::assume(from <= to);
-        (from, to)
-    }
-
     #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86
     #[kani::proof]
     #[kani::unwind(4)]
     pub fn check_small_slice_eq() {
+        // ARR_SIZE can `std::usize::MAX` with cbmc argument
+        // `--arrays-uf-always`
         const ARR_SIZE: usize = 1000;
         let x: [u8; ARR_SIZE] = kani::any();
         let y: [u8; ARR_SIZE] = kani::any();
-        let xs = any_slice_of_array(&x);
-        let ys = any_slice_of_array(&y);
+        let xs = kani::slice::any_slice_of_array(&x);
+        let ys = kani::slice::any_slice_of_array(&y);
         kani::assume(xs.len() == ys.len());
         unsafe {
             small_slice_eq(xs, ys);

library/core/src/unicode/mod.rs

@@ -38,13 +38,13 @@ mod verify {
     use crate::kani;
 
     /// Checks that `to_upper` does not trigger UB or panics for all valid characters.
-    #[kani::proof]
+    //#[kani::proof]
     fn check_to_upper_safety() {
         let _ = to_upper(kani::any());
     }
 
     /// Checks that `to_lower` does not trigger UB or panics for all valid characters.
-    #[kani::proof]
+    //#[kani::proof]
     fn check_to_lower_safety() {
         let _ = to_lower(kani::any());
     }