From f8b1afc2864a1798c3cb10f7f1753f0e0ae26448 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 24 Jun 2025 15:22:05 -0600 Subject: [PATCH 1/2] add more patterns now that we have regex support --- .github/workflows/kani.yml | 55 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 72db303578f23..61bc9c2e39284 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -114,6 +114,61 @@ jobs: --include-pattern ascii::ascii_char::AsciiChar::from_u8 \ --include-pattern char::convert::from_u32_unchecked \ --include-pattern core_arch::x86::__m128d::as_f64x2 \ + --include-pattern "convert::num::::unchecked_add" \ + --include-pattern "num::::unchecked_add" \ + --include-pattern "num::::unchecked_add" \ + --include-pattern "num::::unchecked_add" \ + --include-pattern "num::::unchecked_add" \ + --include-pattern "num::::unchecked_add" \ + --include-pattern "num::::unchecked_add" \ + --include-pattern "num::::unchecked_add" \ + --include-pattern "num::::unchecked_add" \ + --include-pattern "num::::unchecked_add" \ + --include-pattern "num::::unchecked_add" \ + --include-pattern "num::::unchecked_add" \ + --include-pattern "num::::unchecked_neg" \ + --include-pattern "num::::unchecked_neg" \ + --include-pattern "num::::unchecked_neg" \ + --include-pattern "num::::unchecked_neg" \ + --include-pattern "num::::unchecked_neg" \ + --include-pattern "num::::unchecked_neg" \ + --include-pattern "num::::unchecked_sh" \ + --include-pattern "num::::unchecked_sh" \ + --include-pattern "num::::unchecked_sh" \ + --include-pattern "num::::unchecked_sh" \ + --include-pattern "num::::unchecked_sh" \ + --include-pattern "num::::unchecked_sh" \ + --include-pattern "num::::unchecked_sh" \ + --include-pattern "num::::unchecked_sh" \ + --include-pattern "num::::unchecked_sh" \ + --include-pattern "num::::unchecked_sh" \ + --include-pattern "num::::unchecked_sh" \ + --include-pattern "num::::unchecked_sh" \ + --include-pattern "num::::unchecked_sub" \ + --include-pattern "num::::unchecked_sub" \ + --include-pattern "num::::unchecked_sub" \ + --include-pattern "num::::unchecked_sub" \ + --include-pattern "num::::unchecked_sub" \ + --include-pattern "num::::unchecked_sub" \ + --include-pattern "num::::unchecked_sub" \ + --include-pattern "num::::unchecked_sub" \ + --include-pattern "num::::unchecked_sub" \ + --include-pattern "num::::unchecked_sub" \ + --include-pattern "num::::unchecked_sub" \ + --include-pattern "num::::unchecked_sub" \ + --include-pattern "num::::wrapping_sh" \ + --include-pattern "num::::wrapping_sh" \ + --include-pattern "num::::wrapping_sh" \ + --include-pattern "num::::wrapping_sh" \ + --include-pattern "num::::wrapping_sh" \ + --include-pattern "num::::wrapping_sh" \ + --include-pattern "num::::wrapping_sh" \ + --include-pattern "num::::wrapping_sh" \ + --include-pattern "num::::wrapping_sh" \ + --include-pattern "num::::wrapping_sh" \ + --include-pattern "num::::wrapping_sh" \ + --include-pattern "num::::wrapping_sh" \ --include-pattern "num::nonzero::NonZero::::count_ones" \ --include-pattern "num::nonzero::NonZero::::count_ones" \ --include-pattern "num::nonzero::NonZero::::count_ones" \ From d1175e0097d6d015389878860764126bc1c49260 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 3 Jul 2025 14:20:53 -0400 Subject: [PATCH 2/2] address PR feedback --- .github/workflows/kani.yml | 7 +- library/core/src/convert/num.rs | 68 ----------- library/core/src/num/mod.rs | 192 -------------------------------- 3 files changed, 2 insertions(+), 265 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 61bc9c2e39284..a49d3c8893156 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -99,16 +99,13 @@ jobs: # explicitly list all functions (or prefixes thereof) the proofs of which # are known to pass. # Notes: - # - We use >::disjoint_bitor (and >::unchecked_disjoint_bitor) as pattern - # as whitespace is not supported, cf. - # https://github.com/model-checking/kani/issues/4046 # - core_arch::x86::__m128d::as_f64x2 is just one example of hundreds of # core_arch::x86:: functions that are known to verify successfully. - name: Run Kani Verification run: | scripts/run-kani.sh --run autoharness --kani-args \ - --include-pattern ">::disjoint_bitor" \ - --include-pattern ">::unchecked_disjoint_bitor" \ + --include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::disjoint_bitor" \ + --include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::unchecked_disjoint_bitor" \ --include-pattern alloc::__default_lib_allocator:: \ --include-pattern alloc::layout::Layout::from_size_align \ --include-pattern ascii::ascii_char::AsciiChar::from_u8 \ diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs index 7fbf3301efe46..6076b33132ff4 100644 --- a/library/core/src/convert/num.rs +++ b/library/core/src/convert/num.rs @@ -600,74 +600,6 @@ impl_nonzero_int_try_from_nonzero_int!(isize => u8, u16, u32, u64, u128, usize); mod verify { use super::*; - // Generate harnesses for `NonZero::::from(NonZero)`. - macro_rules! generate_nonzero_int_from_nonzero_int_harness { - ($Small:ty => $Large:ty, $harness:ident) => { - #[kani::proof] - pub fn $harness() { - let x: NonZero<$Small> = kani::any(); - let _ = NonZero::<$Large>::from(x); - } - }; - } - - // This bundles the calls to `generate_nonzero_int_from_nonzero_int_harness` - // macro into segregated namespaces for better organization and usability. - macro_rules! generate_nonzero_int_from_nonzero_int_harnesses { - ($ns:ident, $Small:ty => $($Large:tt),+ $(,)?) => { - mod $ns { - use super::*; - - $( - mod $Large { - use super::*; - - generate_nonzero_int_from_nonzero_int_harness!( - $Small => $Large, - check_nonzero_int_from_nonzero_int - ); - } - )+ - } - }; - } - - // non-zero unsigned integer -> non-zero integer, infallible - generate_nonzero_int_from_nonzero_int_harnesses!( - check_nonzero_int_from_u8, - u8 => u16, u32, u64, u128, usize, i16, i32, i64, i128, isize, - ); - generate_nonzero_int_from_nonzero_int_harnesses!( - check_nonzero_int_from_u16, - u16 => u32, u64, u128, usize, i32, i64, i128, - ); - generate_nonzero_int_from_nonzero_int_harnesses!( - check_nonzero_int_from_u32, - u32 => u64, u128, i64, i128, - ); - generate_nonzero_int_from_nonzero_int_harnesses!( - check_nonzero_int_from_u64, - u64 => u128, i128, - ); - - // non-zero signed integer -> non-zero signed integer, infallible - generate_nonzero_int_from_nonzero_int_harnesses!( - check_nonzero_int_from_i8, - i8 => i16, i32, i64, i128, isize, - ); - generate_nonzero_int_from_nonzero_int_harnesses!( - check_nonzero_int_from_i16, - i16 => i32, i64, i128, isize, - ); - generate_nonzero_int_from_nonzero_int_harnesses!( - check_nonzero_int_from_i32, - i32 => i64, i128, - ); - generate_nonzero_int_from_nonzero_int_harnesses!( - check_nonzero_int_from_i64, - i64 => i128, - ); - // Generates harnesses for `NonZero::::try_from(NonZero)`. // Since the function may be fallible or infallible depending on `source` and `target`, // this macro supports generating both cases. diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 97c9b1437a700..049bf5dab4f75 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1681,34 +1681,6 @@ mod verify { } } - // Verify `unchecked_{shl, shr}` - macro_rules! generate_unchecked_shift_harness { - ($type:ty, $method:ident, $harness_name:ident) => { - #[kani::proof_for_contract($type::$method)] - pub fn $harness_name() { - let num1: $type = kani::any::<$type>(); - let num2: u32 = kani::any::(); - - unsafe { - num1.$method(num2); - } - } - }; - } - - macro_rules! generate_unchecked_neg_harness { - ($type:ty, $harness_name:ident) => { - #[kani::proof_for_contract($type::unchecked_neg)] - pub fn $harness_name() { - let num1: $type = kani::any::<$type>(); - - unsafe { - num1.unchecked_neg(); - } - } - }; - } - /// A macro to generate Kani proof harnesses for the `carrying_mul` method, /// /// The macro creates multiple harnesses for different ranges of input values, @@ -1810,47 +1782,6 @@ mod verify { } } - // `unchecked_add` proofs - // - // Target types: - // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total - // - // Target contracts: - // Preconditions: No overflow should occur - // #[requires(!self.overflowing_add(rhs).1)] - // - // Target function: - // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self - generate_unchecked_math_harness!(i8, unchecked_add, checked_unchecked_add_i8); - generate_unchecked_math_harness!(i16, unchecked_add, checked_unchecked_add_i16); - generate_unchecked_math_harness!(i32, unchecked_add, checked_unchecked_add_i32); - generate_unchecked_math_harness!(i64, unchecked_add, checked_unchecked_add_i64); - generate_unchecked_math_harness!(i128, unchecked_add, checked_unchecked_add_i128); - generate_unchecked_math_harness!(isize, unchecked_add, checked_unchecked_add_isize); - generate_unchecked_math_harness!(u8, unchecked_add, checked_unchecked_add_u8); - generate_unchecked_math_harness!(u16, unchecked_add, checked_unchecked_add_u16); - generate_unchecked_math_harness!(u32, unchecked_add, checked_unchecked_add_u32); - generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64); - generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128); - generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize); - - // `unchecked_neg` proofs - // - // Target types: - // i{8,16,32,64,128,size} -- 6 types in total - // - // Target contracts: - // #[requires(self != $SelfT::MIN)] - // - // Target function: - // pub const unsafe fn unchecked_neg(self) -> Self - generate_unchecked_neg_harness!(i8, checked_unchecked_neg_i8); - generate_unchecked_neg_harness!(i16, checked_unchecked_neg_i16); - generate_unchecked_neg_harness!(i32, checked_unchecked_neg_i32); - generate_unchecked_neg_harness!(i64, checked_unchecked_neg_i64); - generate_unchecked_neg_harness!(i128, checked_unchecked_neg_i128); - generate_unchecked_neg_harness!(isize, checked_unchecked_neg_isize); - // `unchecked_mul` proofs // // Target types: @@ -2008,80 +1939,6 @@ mod verify { usize::MAX ); - // unchecked_shr proofs - // - // Target types: - // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total - // - // Target contracts: - // #[requires(rhs < <$ActualT>::BITS)] - // - // Target function: - // pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self - generate_unchecked_shift_harness!(i8, unchecked_shr, checked_unchecked_shr_i8); - generate_unchecked_shift_harness!(i16, unchecked_shr, checked_unchecked_shr_i16); - generate_unchecked_shift_harness!(i32, unchecked_shr, checked_unchecked_shr_i32); - generate_unchecked_shift_harness!(i64, unchecked_shr, checked_unchecked_shr_i64); - generate_unchecked_shift_harness!(i128, unchecked_shr, checked_unchecked_shr_i128); - generate_unchecked_shift_harness!(isize, unchecked_shr, checked_unchecked_shr_isize); - generate_unchecked_shift_harness!(u8, unchecked_shr, checked_unchecked_shr_u8); - generate_unchecked_shift_harness!(u16, unchecked_shr, checked_unchecked_shr_u16); - generate_unchecked_shift_harness!(u32, unchecked_shr, checked_unchecked_shr_u32); - generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64); - generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128); - generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize); - - // `unchecked_shl` proofs - // - // Target types: - // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total - // - // Target contracts: - // #[requires(shift < Self::BITS)] - // - // Target function: - // pub const unsafe fn unchecked_shl(self, shift: u32) -> Self - // - // This function performs an unchecked bitwise left shift operation. - generate_unchecked_shift_harness!(i8, unchecked_shl, checked_unchecked_shl_i8); - generate_unchecked_shift_harness!(i16, unchecked_shl, checked_unchecked_shl_i16); - generate_unchecked_shift_harness!(i32, unchecked_shl, checked_unchecked_shl_i32); - generate_unchecked_shift_harness!(i64, unchecked_shl, checked_unchecked_shl_i64); - generate_unchecked_shift_harness!(i128, unchecked_shl, checked_unchecked_shl_i128); - generate_unchecked_shift_harness!(isize, unchecked_shl, checked_unchecked_shl_isize); - generate_unchecked_shift_harness!(u8, unchecked_shl, checked_unchecked_shl_u8); - generate_unchecked_shift_harness!(u16, unchecked_shl, checked_unchecked_shl_u16); - generate_unchecked_shift_harness!(u32, unchecked_shl, checked_unchecked_shl_u32); - generate_unchecked_shift_harness!(u64, unchecked_shl, checked_unchecked_shl_u64); - generate_unchecked_shift_harness!(u128, unchecked_shl, checked_unchecked_shl_u128); - generate_unchecked_shift_harness!(usize, unchecked_shl, checked_unchecked_shl_usize); - - // `unchecked_sub` proofs - // - // Target types: - // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total - // - // Target contracts: - // Preconditions: No overflow should occur - // #[requires(!self.overflowing_sub(rhs).1)] - // - // Target function: - // pub const unsafe fn unchecked_sub(self, rhs: Self) -> Self - // - // This function performs an unchecked subtraction operation. - generate_unchecked_math_harness!(i8, unchecked_sub, checked_unchecked_sub_i8); - generate_unchecked_math_harness!(i16, unchecked_sub, checked_unchecked_sub_i16); - generate_unchecked_math_harness!(i32, unchecked_sub, checked_unchecked_sub_i32); - generate_unchecked_math_harness!(i64, unchecked_sub, checked_unchecked_sub_i64); - generate_unchecked_math_harness!(i128, unchecked_sub, checked_unchecked_sub_i128); - generate_unchecked_math_harness!(isize, unchecked_sub, checked_unchecked_sub_isize); - generate_unchecked_math_harness!(u8, unchecked_sub, checked_unchecked_sub_u8); - generate_unchecked_math_harness!(u16, unchecked_sub, checked_unchecked_sub_u16); - generate_unchecked_math_harness!(u32, unchecked_sub, checked_unchecked_sub_u32); - generate_unchecked_math_harness!(u64, unchecked_sub, checked_unchecked_sub_u64); - generate_unchecked_math_harness!(u128, unchecked_sub, checked_unchecked_sub_u128); - generate_unchecked_math_harness!(usize, unchecked_sub, checked_unchecked_sub_usize); - // Part_2 `carrying_mul` proofs // // ====================== u8 Harnesses ====================== @@ -2172,55 +2029,6 @@ mod verify { (u64::MAX / 2) + 10u64 ); - // Part_2 `wrapping_shl` proofs - // - // Target types: - // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total - // - // Target contracts: - // #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))] - // - // Target function: - // pub const fn wrapping_shl(self, rhs: u32) -> Self - // - // This function performs an panic-free bitwise left shift operation. - generate_wrapping_shift_harness!(i8, wrapping_shl, checked_wrapping_shl_i8); - generate_wrapping_shift_harness!(i16, wrapping_shl, checked_wrapping_shl_i16); - generate_wrapping_shift_harness!(i32, wrapping_shl, checked_wrapping_shl_i32); - generate_wrapping_shift_harness!(i64, wrapping_shl, checked_wrapping_shl_i64); - generate_wrapping_shift_harness!(i128, wrapping_shl, checked_wrapping_shl_i128); - generate_wrapping_shift_harness!(isize, wrapping_shl, checked_wrapping_shl_isize); - generate_wrapping_shift_harness!(u8, wrapping_shl, checked_wrapping_shl_u8); - generate_wrapping_shift_harness!(u16, wrapping_shl, checked_wrapping_shl_u16); - generate_wrapping_shift_harness!(u32, wrapping_shl, checked_wrapping_shl_u32); - generate_wrapping_shift_harness!(u64, wrapping_shl, checked_wrapping_shl_u64); - generate_wrapping_shift_harness!(u128, wrapping_shl, checked_wrapping_shl_u128); - generate_wrapping_shift_harness!(usize, wrapping_shl, checked_wrapping_shl_usize); - - // Part_2 `wrapping_shr` proofs - // - // Target types: - // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total - // - // Target contracts: - // #[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))] - // Target function: - // pub const fn wrapping_shr(self, rhs: u32) -> Self { - // - // This function performs an panic-free bitwise right shift operation. - generate_wrapping_shift_harness!(i8, wrapping_shr, checked_wrapping_shr_i8); - generate_wrapping_shift_harness!(i16, wrapping_shr, checked_wrapping_shr_i16); - generate_wrapping_shift_harness!(i32, wrapping_shr, checked_wrapping_shr_i32); - generate_wrapping_shift_harness!(i64, wrapping_shr, checked_wrapping_shr_i64); - generate_wrapping_shift_harness!(i128, wrapping_shr, checked_wrapping_shr_i128); - generate_wrapping_shift_harness!(isize, wrapping_shr, checked_wrapping_shr_isize); - generate_wrapping_shift_harness!(u8, wrapping_shr, checked_wrapping_shr_u8); - generate_wrapping_shift_harness!(u16, wrapping_shr, checked_wrapping_shr_u16); - generate_wrapping_shift_harness!(u32, wrapping_shr, checked_wrapping_shr_u32); - generate_wrapping_shift_harness!(u64, wrapping_shr, checked_wrapping_shr_u64); - generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128); - generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize); - // `f{16,32,64,128}::to_int_unchecked` proofs // // Target integer types: