diff --git a/.github/workflows/kani-metrics.yml b/.github/workflows/kani-metrics.yml index 84945e236a4ed..106ed3e160b4b 100644 --- a/.github/workflows/kani-metrics.yml +++ b/.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 diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 7ca0ca81b8ea8..fd949f8eef552 100644 --- a/.github/workflows/kani.yml +++ b/.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::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::count_ones" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::rotate_" \ + --include-pattern "num::nonzero::NonZero::::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 diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs index f3df9c6916812..17871634b0ad4 100644 --- a/library/core/src/alloc/layout.rs +++ b/library/core/src/alloc/layout.rs @@ -637,24 +637,6 @@ mod verify { } } - // pub const fn from_size_align(size: usize, align: usize) -> Result - #[kani::proof_for_contract(Layout::from_size_align)] - pub fn check_from_size_align() { - let s = kani::any::(); - let a = kani::any::(); - 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::(); - let a = kani::any::(); - unsafe { - let _ = Layout::from_size_align_unchecked(s, a); - } - } - // pub const fn size(&self) -> usize #[kani::proof] pub fn check_size() { diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs index aca4503f5a6c0..6fce682b33dbb 100644 --- a/library/core/src/ascii/ascii_char.rs +++ b/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) }; - } -} diff --git a/library/core/src/char/convert.rs b/library/core/src/char/convert.rs index cc1632182b231..ff4ff38290e63 100644 --- a/library/core/src/char/convert.rs +++ b/library/core/src/char/convert.rs @@ -288,15 +288,3 @@ pub(super) const fn from_digit(num: u32, radix: u32) -> Option { 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) }; - } -} diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index d11e729c2b520..83ebd7fbe1922 100644 --- a/library/core/src/num/nonzero.rs +++ b/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 { // 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); } diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs index c14c2b67c3ddf..6095e408ff71e 100644 --- a/library/core/src/ptr/alignment.rs +++ b/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() -> Self // #[kani::proof_for_contract(Alignment::of)] // pub fn check_of_i32() { // let _ = Alignment::of::(); // } - - // pub const fn new(align: usize) -> Option - #[kani::proof_for_contract(Alignment::new)] - pub fn check_new() { - let a = kani::any::(); - 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::(); - 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::(); - if let Some(alignment) = Alignment::new(a) { - assert_eq!(alignment.as_usize(), a); - } - } - - // pub const fn as_nonzero(self) -> NonZero - #[kani::proof_for_contract(Alignment::as_nonzero)] - pub fn check_as_nonzero() { - let alignment = kani::any::(); - let _ = alignment.as_nonzero(); - } - - // pub const fn log2(self) -> u32 - #[kani::proof_for_contract(Alignment::log2)] - pub fn check_log2() { - let alignment = kani::any::(); - let _ = alignment.log2(); - } - - // pub const fn mask(self) -> usize - #[kani::proof_for_contract(Alignment::mask)] - pub fn check_mask() { - let alignment = kani::any::(); - let _ = alignment.mask(); - } } diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index 6ea47e6a6f517..e87cbb027cd8c 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -1941,6 +1941,14 @@ pub(crate) unsafe fn align_offset(p: *const T, a: usize) -> usize { /// * `x < m`; (if `x ≥ m`, pass in `x % m` instead) /// /// Implementation of this function shall not panic. Ever. + #[safety::requires(m.is_power_of_two())] + #[safety::requires(x < m)] + // TODO: add ensures contract to check that the answer is indeed correct + // This will require quantifiers (https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html) + // so that we can add a precondition that gcd(x, m) = 1 like so: + // ∀d, d > 0 ∧ x % d = 0 ∧ m % d = 0 → d = 1 + // With this precondition, we can then write this postcondition to check the correctness of the answer: + // #[safety::ensures(|result| wrapping_mul(*result, x) % m == 1)] #[inline] const unsafe fn mod_inv(x: usize, m: usize) -> usize { /// Multiplicative modular inverse table modulo 2⁴ = 16. @@ -2549,67 +2557,4 @@ mod verify { let p = kani::any::() as *const [char; 5]; check_align_offset(p); } - - // This function lives inside align_offset, so it is not publicly accessible (hence this copy). - #[safety::requires(m.is_power_of_two())] - #[safety::requires(x < m)] - // TODO: add ensures contract to check that the answer is indeed correct - // This will require quantifiers (https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html) - // so that we can add a precondition that gcd(x, m) = 1 like so: - // ∀d, d > 0 ∧ x % d = 0 ∧ m % d = 0 → d = 1 - // With this precondition, we can then write this postcondition to check the correctness of the answer: - // #[safety::ensures(|result| wrapping_mul(*result, x) % m == 1)] - const unsafe fn mod_inv_copy(x: usize, m: usize) -> usize { - /// Multiplicative modular inverse table modulo 2⁴ = 16. - /// - /// Note, that this table does not contain values where inverse does not exist (i.e., for - /// `0⁻¹ mod 16`, `2⁻¹ mod 16`, etc.) - const INV_TABLE_MOD_16: [u8; 8] = [1, 11, 13, 7, 9, 3, 5, 15]; - /// Modulo for which the `INV_TABLE_MOD_16` is intended. - const INV_TABLE_MOD: usize = 16; - - // SAFETY: `m` is required to be a power-of-two, hence non-zero. - let m_minus_one = unsafe { unchecked_sub(m, 1) }; - let mut inverse = INV_TABLE_MOD_16[(x & (INV_TABLE_MOD - 1)) >> 1] as usize; - let mut mod_gate = INV_TABLE_MOD; - // We iterate "up" using the following formula: - // - // $$ xy ≡ 1 (mod 2ⁿ) → xy (2 - xy) ≡ 1 (mod 2²ⁿ) $$ - // - // This application needs to be applied at least until `2²ⁿ ≥ m`, at which point we can - // finally reduce the computation to our desired `m` by taking `inverse mod m`. - // - // This computation is `O(log log m)`, which is to say, that on 64-bit machines this loop - // will always finish in at most 4 iterations. - loop { - // y = y * (2 - xy) mod n - // - // Note, that we use wrapping operations here intentionally – the original formula - // uses e.g., subtraction `mod n`. It is entirely fine to do them `mod - // usize::MAX` instead, because we take the result `mod n` at the end - // anyway. - if mod_gate >= m { - break; - } - inverse = wrapping_mul(inverse, wrapping_sub(2usize, wrapping_mul(x, inverse))); - let (new_gate, overflow) = mul_with_overflow(mod_gate, mod_gate); - if overflow { - break; - } - mod_gate = new_gate; - } - inverse & m_minus_one - } - - // The specification for mod_inv states that it cannot ever panic. - // Verify that is the case, given that the function's safety preconditions are met. - - // TODO: Once https://github.com/model-checking/kani/issues/3467 is fixed, - // move this harness inside `align_offset` and delete `mod_inv_copy` - #[kani::proof_for_contract(mod_inv_copy)] - fn check_mod_inv() { - let x = kani::any::(); - let m = kani::any::(); - unsafe { mod_inv_copy(x, m) }; - } } diff --git a/library/core/src/time.rs b/library/core/src/time.rs index c0d67cc51edf5..f0a7e36fd4b0f 100644 --- a/library/core/src/time.rs +++ b/library/core/src/time.rs @@ -1756,30 +1756,6 @@ pub mod duration_verify { let _ = Duration::new(secs, nanos); } - #[kani::proof_for_contract(Duration::from_secs)] - fn duration_from_secs() { - let secs = kani::any::(); - let _ = Duration::from_secs(secs); - } - - #[kani::proof_for_contract(Duration::from_millis)] - fn duration_from_millis() { - let ms = kani::any::(); - let _ = Duration::from_millis(ms); - } - - #[kani::proof_for_contract(Duration::from_micros)] - fn duration_from_micros() { - let micros = kani::any::(); - let _ = Duration::from_micros(micros); - } - - #[kani::proof_for_contract(Duration::from_nanos)] - fn duration_from_nanos() { - let nanos = kani::any::(); - let _ = Duration::from_nanos(nanos); - } - #[kani::proof_for_contract(Duration::as_secs)] fn duration_as_secs() { let dur = safe_duration(); diff --git a/library/core/src/unicode/mod.rs b/library/core/src/unicode/mod.rs index 92394340152d0..49dbdeb1a6d1c 100644 --- a/library/core/src/unicode/mod.rs +++ b/library/core/src/unicode/mod.rs @@ -33,21 +33,3 @@ mod unicode_data; /// [Unicode 11.0 or later, Section 3.1 Versions of the Unicode Standard](https://www.unicode.org/versions/Unicode11.0.0/ch03.pdf#page=4). #[stable(feature = "unicode_version", since = "1.45.0")] pub const UNICODE_VERSION: (u8, u8, u8) = unicode_data::UNICODE_VERSION; - -#[cfg(kani)] -mod verify { - use super::conversions::{to_lower, to_upper}; - use crate::kani; - - /// Checks that `to_upper` does not trigger UB or panics for all valid characters. - #[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] - fn check_to_lower_safety() { - let _ = to_lower(kani::any()); - } -} diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index d3edc34bc064a..1abe73df88b12 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -7,15 +7,17 @@ usage() { echo "Options:" echo " -h, --help Show this help message" echo " -p, --path Optional: Specify a path to a copy of the std library. For example, if you want to run the script from an outside directory." - echo " --run Optional: Specify whether to run the 'kani verify-std' command, 'kani list' command, collect Kani-specific metrics, or summarize autoharness failure reasons. Defaults to 'verify-std' if not specified." + echo " --run Optional: Specify whether to run the 'kani verify-std' command, 'kani list' command, collect Kani-specific metrics, run verification with autoharness support, or summarize autoharness failure reasons. Defaults to 'verify-std' if not specified." + echo " --with-autoharness Include autoharness information in list or metrics commands." echo " --kani-args Optional: Arguments to pass to the command. Simply pass them in the same way you would to the Kani binary. This should be the last argument." exit 1 } # Initialize variables -command_args="" +declare -a command_args path="" run_command="verify-std" +with_autoharness="false" # Parse command line arguments # TODO: Improve parsing with getopts @@ -34,7 +36,7 @@ while [[ $# -gt 0 ]]; do fi ;; --run) - if [[ -n $2 && ($2 == "verify-std" || $2 == "list" || $2 == "metrics" || $2 == "autoharness-analyzer") ]]; then + if [[ -n $2 && ($2 == "verify-std" || $2 == "list" || $2 == "metrics" || $2 == "autoharness" || $2 == "autoharness-analyzer") ]]; then run_command=$2 shift 2 else @@ -42,9 +44,13 @@ while [[ $# -gt 0 ]]; do usage fi ;; + --with-autoharness) + with_autoharness="true" + shift + ;; --kani-args) shift - command_args="$@" + command_args=("$@") break ;; *) @@ -145,7 +151,7 @@ build_kani() { source "kani-dependencies" # Check if installed versions are correct. if ./scripts/check-cbmc-version.py \ - --major ${CBMC_MAJOR} --minor ${CBMC_MINOR} --patch ${CBMC_PATCH} \ + --major ${CBMC_MAJOR} --minor ${CBMC_MINOR} \ && ./scripts/check_kissat_version.sh; then echo "Dependencies are up-to-date" else @@ -211,7 +217,7 @@ run_verification_subset() { $harness_args --exact \ -j \ --output-format=terse \ - $command_args \ + "${command_args[@]}" \ --enable-unstable \ --cbmc-args --object-bits 12 } @@ -293,17 +299,35 @@ main() { "$kani_path" verify-std -Z unstable-options ./library \ $unstable_args \ --no-assert-contracts \ - $command_args \ + "${command_args[@]}" \ --enable-unstable \ --cbmc-args --object-bits 12 fi + elif [[ "$run_command" == "autoharness" ]]; then + # Run verification for a subset of automatically generated harnesses + # (not in parallel) + echo "Running Kani autoharness command..." + "$kani_path" autoharness -Z autoharness -Z unstable-options --std ./library \ + $unstable_args \ + --no-assert-contracts \ + "${command_args[@]}" \ + --enable-unstable \ + --cbmc-args --object-bits 12 elif [[ "$run_command" == "list" ]]; then echo "Running Kani list command..." - "$kani_path" list -Z list $unstable_args ./library --std --format markdown + if [[ "$with_autoharness" == "true" ]]; then + "$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format markdown + else + "$kani_path" list -Z list $unstable_args ./library --std --format markdown + fi elif [[ "$run_command" == "metrics" ]]; then local current_dir=$(pwd) echo "Running Kani list command..." - "$kani_path" list -Z list $unstable_args ./library --std --format json + if [[ "$with_autoharness" == "true" ]]; then + "$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format json + else + "$kani_path" list -Z list $unstable_args ./library --std --format json + fi pushd scripts/kani-std-analysis echo "Running Kani's std-analysis command..." ./std-analysis.sh $build_dir @@ -323,7 +347,7 @@ main() { --only-codegen -j --output-format=terse \ $unstable_args \ --no-assert-contracts \ - $command_args \ + "${command_args[@]}" \ --enable-unstable \ --cbmc-args --object-bits 12 # remove metadata file for Kani-generated "dummy" crate that we won't