Add autoharness to run-kani script and use in CI

.github/workflows/kani-metrics.yml

@@ -26,7 +26,7 @@ jobs:
         python-version: '3.x'
 
     - name: Compute Kani Metrics
-      run: ./scripts/run-kani.sh --run metrics --path ${{github.workspace}}
+      run: ./scripts/run-kani.sh --run metrics --with-autoharness --path ${{github.workspace}}
 
     - name: Create Pull Request
       uses: peter-evans/create-pull-request@v7

.github/workflows/kani.yml

@@ -53,6 +53,79 @@ jobs:
       - name: Run Kani Verification
         run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
 
+  kani-autoharness:
+    name: Verify std library using autoharness
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+        include:
+          - os: ubuntu-latest
+            base: ubuntu
+          - os: macos-latest
+            base: macos
+      fail-fast: false
+
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      # Step 2: Run Kani autoharness on the std library for selected functions.
+      # Uses "--include-pattern" to make sure we do not try to run across all
+      # possible functions as that may take a lot longer than expected. Instead,
+      # explicitly list all functions (or prefixes thereof) the proofs of which
+      # are known to pass.
+      - name: Run Kani Verification
+        run: |
+          scripts/run-kani.sh --run autoharness --kani-args \
+            --include-pattern alloc::layout::Layout::from_size_align \
+            --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
+            --include-pattern char::convert::from_u32_unchecked \
+            --include-pattern "num::nonzero::NonZero::<i8>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i16>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i32>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i64>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i128>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<isize>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u8>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u16>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u32>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u64>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u128>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<usize>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i8>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<i16>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<i32>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<i64>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<i128>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<isize>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<u8>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<u16>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<u32>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<u64>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<u128>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<usize>::rotate_" \
+            --include-pattern ptr::align_offset::mod_inv \
+            --include-pattern ptr::alignment::Alignment::as_nonzero \
+            --include-pattern ptr::alignment::Alignment::as_usize \
+            --include-pattern ptr::alignment::Alignment::log2 \
+            --include-pattern ptr::alignment::Alignment::mask \
+            --include-pattern ptr::alignment::Alignment::new \
+            --include-pattern ptr::alignment::Alignment::new_unchecked \
+            --include-pattern time::Duration::from_micros \
+            --include-pattern time::Duration::from_millis \
+            --include-pattern time::Duration::from_nanos \
+            --include-pattern time::Duration::from_secs \
+            --exclude-pattern time::Duration::from_secs_f \
+            --include-pattern unicode::unicode_data::conversions::to_ \
+            --exclude-pattern ::precondition_check \
+            --harness-timeout 5m \
+            --default-unwind 1000 \
+            --jobs=3 --output-format=terse
+
   run-kani-list:
     name: Kani List
     runs-on: ubuntu-latest
@@ -66,8 +139,14 @@ jobs:
 
       # Step 2: Run list on the std library
       - name: Run Kani List
-        run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head
-
+        run: |
+          head/scripts/run-kani.sh --run list --with-autoharness --path ${{github.workspace}}/head
+          # remove duplicate white space to reduce file size (GitHub permits at
+          # most one 1MB)
+          ls -l ${{github.workspace}}/head/kani-list.md
+          perl -p -i -e 's/ +/ /g' ${{github.workspace}}/head/kani-list.md
+          ls -l ${{github.workspace}}/head/kani-list.md
+
       # Step 3: Add output to job summary
       - name: Add Kani List output to job summary
         uses: actions/github-script@v6

library/core/src/alloc/layout.rs

@@ -637,24 +637,6 @@ mod verify {
         }
     }
 
-    // pub const fn from_size_align(size: usize, align: usize) -> Result<Self, LayoutError>
-    #[kani::proof_for_contract(Layout::from_size_align)]
-    pub fn check_from_size_align() {
-        let s = kani::any::<usize>();
-        let a = kani::any::<usize>();
-        let _ = Layout::from_size_align(s, a);
-    }
-
-    // pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self
-    #[kani::proof_for_contract(Layout::from_size_align_unchecked)]
-    pub fn check_from_size_align_unchecked() {
-        let s = kani::any::<usize>();
-        let a = kani::any::<usize>();
-        unsafe {
-            let _ = Layout::from_size_align_unchecked(s, a);
-        }
-    }
-
     // pub const fn size(&self) -> usize
     #[kani::proof]
     pub fn check_size() {

library/core/src/ascii/ascii_char.rs

@@ -621,23 +621,3 @@ impl fmt::Debug for AsciiChar {
         f.write_str(buf[..len].as_str())
     }
 }
-
-#[cfg(kani)]
-#[unstable(feature = "kani", issue = "none")]
-mod verify {
-    use AsciiChar;
-
-    use super::*;
-
-    #[kani::proof_for_contract(AsciiChar::from_u8)]
-    fn check_from_u8() {
-        let b: u8 = kani::any();
-        AsciiChar::from_u8(b);
-    }
-
-    #[kani::proof_for_contract(AsciiChar::from_u8_unchecked)]
-    fn check_from_u8_unchecked() {
-        let b: u8 = kani::any();
-        unsafe { AsciiChar::from_u8_unchecked(b) };
-    }
-}

library/core/src/char/convert.rs

@@ -288,15 +288,3 @@ pub(super) const fn from_digit(num: u32, radix: u32) -> Option<char> {
         None
     }
 }
-
-#[cfg(kani)]
-#[unstable(feature = "kani", issue = "none")]
-mod verify {
-    use super::*;
-
-    #[kani::proof_for_contract(from_u32_unchecked)]
-    fn check_from_u32_unchecked() {
-        let i: u32 = kani::any();
-        unsafe { from_u32_unchecked(i) };
-    }
-}

library/core/src/num/nonzero.rs

@@ -721,6 +721,7 @@ macro_rules! nonzero_integer {
             #[must_use = "this returns the result of the operation, \
                         without modifying the original"]
             #[inline(always)]
+            #[ensures(|result| result.get() > 0)]
             pub const fn count_ones(self) -> NonZero<u32> {
                 // SAFETY:
                 // `self` is non-zero, which means it has at least one bit set, which means
@@ -754,6 +755,8 @@ macro_rules! nonzero_integer {
             #[must_use = "this returns the result of the operation, \
                         without modifying the original"]
             #[inline(always)]
+            #[ensures(|result| result.get() > 0)]
+            #[ensures(|result| result.rotate_right(n).get() == old(self).get())]
             pub const fn rotate_left(self, n: u32) -> Self {
                 let result = self.get().rotate_left(n);
                 // SAFETY: Rotating bits preserves the property int > 0.
@@ -787,6 +790,8 @@ macro_rules! nonzero_integer {
             #[must_use = "this returns the result of the operation, \
                         without modifying the original"]
             #[inline(always)]
+            #[ensures(|result| result.get() > 0)]
+            #[ensures(|result| result.rotate_left(n).get() == old(self).get())]
             pub const fn rotate_right(self, n: u32) -> Self {
                 let result = self.get().rotate_right(n);
                 // SAFETY: Rotating bits preserves the property int > 0.
@@ -2571,56 +2576,4 @@ mod verify {
     nonzero_check_clamp_panic!(core::num::NonZeroU64, nonzero_check_clamp_panic_for_u64);
     nonzero_check_clamp_panic!(core::num::NonZeroU128, nonzero_check_clamp_panic_for_u128);
     nonzero_check_clamp_panic!(core::num::NonZeroUsize, nonzero_check_clamp_panic_for_usize);
-
-    macro_rules! nonzero_check_count_ones {
-        ($nonzero_type:ty, $nonzero_check_count_ones_for:ident) => {
-            #[kani::proof]
-            pub fn $nonzero_check_count_ones_for() {
-                let x: $nonzero_type = kani::any();
-                let result = x.count_ones();
-                // Since x is non-zero, count_ones should never return 0
-                assert!(result.get() > 0);
-            }
-        };
-    }
-
-    // Use the macro to generate different versions of the function for multiple types
-    nonzero_check_count_ones!(core::num::NonZeroI8, nonzero_check_count_ones_for_i8);
-    nonzero_check_count_ones!(core::num::NonZeroI16, nonzero_check_count_ones_for_i16);
-    nonzero_check_count_ones!(core::num::NonZeroI32, nonzero_check_count_ones_for_i32);
-    nonzero_check_count_ones!(core::num::NonZeroI64, nonzero_check_count_ones_for_i64);
-    nonzero_check_count_ones!(core::num::NonZeroI128, nonzero_check_count_ones_for_i128);
-    nonzero_check_count_ones!(core::num::NonZeroIsize, nonzero_check_count_ones_for_isize);
-    nonzero_check_count_ones!(core::num::NonZeroU8, nonzero_check_count_ones_for_u8);
-    nonzero_check_count_ones!(core::num::NonZeroU16, nonzero_check_count_ones_for_u16);
-    nonzero_check_count_ones!(core::num::NonZeroU32, nonzero_check_count_ones_for_u32);
-    nonzero_check_count_ones!(core::num::NonZeroU64, nonzero_check_count_ones_for_u64);
-    nonzero_check_count_ones!(core::num::NonZeroU128, nonzero_check_count_ones_for_u128);
-    nonzero_check_count_ones!(core::num::NonZeroUsize, nonzero_check_count_ones_for_usize);
-
-    macro_rules! nonzero_check_rotate_left_and_right {
-        ($nonzero_type:ty, $nonzero_check_rotate_for:ident) => {
-            #[kani::proof]
-            pub fn $nonzero_check_rotate_for() {
-                let x: $nonzero_type = kani::any();
-                let n: u32 = kani::any();
-                let result = x.rotate_left(n).rotate_right(n);
-                assert!(result == x);
-            }
-        };
-    }
-
-    // Use the macro to generate different versions of the function for multiple types
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroI8, nonzero_check_rotate_for_i8);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroI16, nonzero_check_rotate_for_i16);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroI32, nonzero_check_rotate_for_i32);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroI64, nonzero_check_rotate_for_i64);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroI128, nonzero_check_rotate_for_i128);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroIsize, nonzero_check_rotate_for_isize);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroU8, nonzero_check_rotate_for_u8);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroU16, nonzero_check_rotate_for_u16);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroU32, nonzero_check_rotate_for_u32);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroU64, nonzero_check_rotate_for_u64);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroU128, nonzero_check_rotate_for_u128);
-    nonzero_check_rotate_left_and_right!(core::num::NonZeroUsize, nonzero_check_rotate_for_usize);
 }

library/core/src/ptr/alignment.rs

@@ -16,7 +16,9 @@ use crate::{cmp, fmt, hash, mem, num};
 #[unstable(feature = "ptr_alignment_type", issue = "102070")]
 #[derive(Copy, Clone, PartialEq, Eq)]
 #[repr(transparent)]
-#[invariant(self.as_usize().is_power_of_two())]
+// uses .0 instead of .as_usize() to permit proving as_usize so that its proof does not itself use
+// as_usize
+#[invariant((self.0 as usize).is_power_of_two())]
 pub struct Alignment(AlignmentEnum);
 
 // Alignment is `repr(usize)`, but via extra steps.
@@ -404,56 +406,10 @@ mod verify {
         }
     }
 
-    /// FIXME, c.f. https://github.com/model-checking/kani/issues/3905
+    // FIXME, c.f. https://github.com/model-checking/kani/issues/3905
     // // pub const fn of<T>() -> Self
     // #[kani::proof_for_contract(Alignment::of)]
     // pub fn check_of_i32() {
     //     let _ = Alignment::of::<i32>();
     // }
-
-    // pub const fn new(align: usize) -> Option<Self>
-    #[kani::proof_for_contract(Alignment::new)]
-    pub fn check_new() {
-        let a = kani::any::<usize>();
-        let _ = Alignment::new(a);
-    }
-
-    // pub const unsafe fn new_unchecked(align: usize) -> Self
-    #[kani::proof_for_contract(Alignment::new_unchecked)]
-    pub fn check_new_unchecked() {
-        let a = kani::any::<usize>();
-        unsafe {
-            let _ = Alignment::new_unchecked(a);
-        }
-    }
-
-    // pub const fn as_usize(self) -> usize
-    #[kani::proof_for_contract(Alignment::as_usize)]
-    pub fn check_as_usize() {
-        let a = kani::any::<usize>();
-        if let Some(alignment) = Alignment::new(a) {
-            assert_eq!(alignment.as_usize(), a);
-        }
-    }
-
-    // pub const fn as_nonzero(self) -> NonZero<usize>
-    #[kani::proof_for_contract(Alignment::as_nonzero)]
-    pub fn check_as_nonzero() {
-        let alignment = kani::any::<Alignment>();
-        let _ = alignment.as_nonzero();
-    }
-
-    // pub const fn log2(self) -> u32
-    #[kani::proof_for_contract(Alignment::log2)]
-    pub fn check_log2() {
-        let alignment = kani::any::<Alignment>();
-        let _ = alignment.log2();
-    }
-
-    // pub const fn mask(self) -> usize
-    #[kani::proof_for_contract(Alignment::mask)]
-    pub fn check_mask() {
-        let alignment = kani::any::<Alignment>();
-        let _ = alignment.mask();
-    }
 }