diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index fa3e4cef9bcb4..a46e653de2bd0 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -816,6 +816,7 @@ macro_rules! int_impl { without modifying the original"] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(!self.overflowing_mul(rhs).1)] pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, @@ -1424,6 +1425,7 @@ macro_rules! int_impl { #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(rhs < <$ActualT>::BITS)] // i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior. pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self { assert_unsafe_precondition!( check_language_ub, diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 51bc33b7b47a4..54e90d1bff0ff 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1605,19 +1605,39 @@ mod verify { } } + macro_rules! generate_unchecked_mul_harness { + ($type:ty, $method:ident, $harness_name:ident, $min:expr, $max:expr) => { + #[kani::proof_for_contract($type::$method)] + pub fn $harness_name() { + let num1: $type = kani::any(); + let num2: $type = kani::any(); + + // Limit the values of num1 and num2 to the specified range for multiplication + kani::assume(num1 >= $min && num1 <= $max); + kani::assume(num2 >= $min && num2 <= $max); + + unsafe { + num1.$method(num2); + } + } + } + } + + 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, $method:ident, $harness_name:ident) => { @@ -1654,4 +1674,54 @@ mod verify { 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_mul 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(!self.overflowing_mul(rhs).1)] + // + // Target function: + // pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self + // exponential state spaces for 32,64 and 128, hence provided limited range for verification. + generate_unchecked_math_harness!(i8, unchecked_mul, checked_unchecked_mul_i8); + generate_unchecked_math_harness!(i16, unchecked_mul, checked_unchecked_mul_i16); + generate_unchecked_mul_harness!(i32, unchecked_mul, checked_unchecked_mul_i32, -10_000i32, 10_000i32); + generate_unchecked_mul_harness!(i64, unchecked_mul, checked_unchecked_mul_i64, -1_000i64, 1_000i64); + generate_unchecked_mul_harness!(i128, unchecked_mul, checked_unchecked_mul_i128, -1_000_000_000_000_000i128, 1_000_000_000_000_000i128); + generate_unchecked_mul_harness!(isize, unchecked_mul, checked_unchecked_mul_isize, -100_000isize, 100_000isize); + generate_unchecked_math_harness!(u8, unchecked_mul, checked_unchecked_mul_u8); + generate_unchecked_math_harness!(u16, unchecked_mul, checked_unchecked_mul_u16); + generate_unchecked_mul_harness!(u32, unchecked_mul, checked_unchecked_mul_u32, 0u32, 20_000u32); + generate_unchecked_mul_harness!(u64, unchecked_mul, checked_unchecked_mul_u64, 0u64, 2_000u64); + generate_unchecked_mul_harness!(u128, unchecked_mul, checked_unchecked_mul_u128, 0u128, 1_000_000_000_000_000u128); + generate_unchecked_mul_harness!(usize, unchecked_mul, checked_unchecked_mul_usize, 0usize, 100_000usize); + + + // 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); + } + } } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index b12d82bdc720c..8706ed8bd6d5f 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -908,6 +908,7 @@ macro_rules! uint_impl { without modifying the original"] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(!self.overflowing_mul(rhs).1)] pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, @@ -1613,6 +1614,7 @@ macro_rules! uint_impl { #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(rhs < <$ActualT>::BITS)]// i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior. pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self { assert_unsafe_precondition!( check_language_ub,