From bbd75f7189ba5bae71febf02a94db85a6f037928 Mon Sep 17 00:00:00 2001 From: Rajath Date: Mon, 23 Sep 2024 13:01:33 -0700 Subject: [PATCH 1/3] unchecked multiplication and shift right --- library/core/src/num/int_macros.rs | 6 +- library/core/src/num/mod.rs | 228 ++++++++++++++++++++++++++++ library/core/src/num/uint_macros.rs | 4 + 3 files changed, 237 insertions(+), 1 deletion(-) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index fa0c9c98dde74..1f82f24c6bf27 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -817,6 +817,8 @@ 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)] + #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, @@ -1423,8 +1425,10 @@ macro_rules! int_impl { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")] - #[inline(always)] + #[inline(always)]0 #[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. + #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // ensures result is within range after bit shift 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 4dbce78394d9e..661c3f11cd3b6 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1703,4 +1703,232 @@ mod verify { num1.unchecked_add(num2); } } + + // `unchecked_mul` proofs + // + // Target types: + // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total + // + // Target Files : src/num/int_macros.rs , src/num/uint_macros.rs + // + // Target contracts : + // #[requires(!self.overflowing_mul(rhs).1)] + // #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] + // + // Target function definition: + // pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self + + #[kani::proof_for_contract(i8::unchecked_mul)] + pub fn check_unchecked_mul_i8() { + let num1: i8 = kani::any::(); + let num2: i8 = kani::any::(); + + unsafe { + num1.unchecked_mul(num2); + } + } + + #[kani::proof_for_contract(i16::unchecked_mul)] + pub fn check_unchecked_mul_i16() { + let num1: i16 = kani::any::(); + let num2: i16 = kani::any::(); + + unsafe { + num1.unchecked_mul(num2); + } + } + + #[kani::proof_for_contract(i32::unchecked_mul)] + pub fn check_unchecked_mul_i32() { + let num1: i32 = kani::any::(); + let num2: i32 = kani::any::(); + + unsafe { + num1.unchecked_mul(num2); + } + } + + #[kani::proof_for_contract(i64::unchecked_mul)] + pub fn check_unchecked_mul_i64() { + let num1: i64 = kani::any::(); + let num2: i64 = kani::any::(); + + unsafe { + num1.unchecked_mul(num2); + } + } + + #[kani::proof_for_contract(i128::unchecked_mul)] + pub fn check_unchecked_mul_i128() { + let num1: i128 = kani::any::(); + let num2: i128 = kani::any::(); + + unsafe { + num1.unchecked_mul(num2); + } + } + + #[kani::proof_for_contract(u8::unchecked_mul)] + pub fn check_unchecked_mul_u8() { + let num1: u8 = kani::any::(); + let num2: u8 = kani::any::(); + + unsafe { + num1.unchecked_mul(num2); + } + } + + #[kani::proof_for_contract(u16::unchecked_mul)] + pub fn check_unchecked_mul_u16() { + let num1: u16 = kani::any::(); + let num2: u16 = kani::any::(); + + unsafe { + num1.unchecked_mul(num2); + } + } + + #[kani::proof_for_contract(u32::unchecked_mul)] + pub fn check_unchecked_mul_u32() { + let num1: u32 = kani::any::(); + let num2: u32 = kani::any::(); + + unsafe { + num1.unchecked_mul(num2); + } + } + + #[kani::proof_for_contract(u64::unchecked_mul)] + pub fn check_unchecked_mul_u64() { + let num1: u64 = kani::any::(); + let num2: u64 = kani::any::(); + + unsafe { + num1.unchecked_mul(num2); + } + } + + #[kani::proof_for_contract(u128::unchecked_mul)] + pub fn check_unchecked_mul_u128() { + let num1: u128 = kani::any::(); + let num2: u128 = kani::any::(); + + unsafe { + num1.unchecked_mul(num2); + } + } + + // `unchecked_shr` proofs + // + // Target types: + // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total + // + // Target Files : src/num/int_macros.rs , src/num/uint_macros.rs + // + // Target contracts: + // #[requires(rhs < <$ActualT>::BITS)] + // #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] + // + // Target function: + // pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self + + #[kani::proof_for_contract(i8::unchecked_shr)] + pub fn check_unchecked_shr_i8() { + let num: i8 = kani::any::(); + let shift: u32 = kani::any::() % i8::BITS; + + unsafe { + num.unchecked_shr(shift); + } + } + + #[kani::proof_for_contract(i16::unchecked_shr)] + pub fn check_unchecked_shr_i16() { + let num: i16 = kani::any::(); + let shift: u32 = kani::any::() % i16::BITS; + + unsafe { + num.unchecked_shr(shift); + } + } + + #[kani::proof_for_contract(i32::unchecked_shr)] + pub fn check_unchecked_shr_i32() { + let num: i32 = kani::any::(); + let shift: u32 = kani::any::() % i32::BITS; + + unsafe { + num.unchecked_shr(shift); + } + } + + #[kani::proof_for_contract(i64::unchecked_shr)] + pub fn check_unchecked_shr_i64() { + let num: i64 = kani::any::(); + let shift: u32 = kani::any::() % i64::BITS; + + unsafe { + num.unchecked_shr(shift); + } + } + + #[kani::proof_for_contract(i128::unchecked_shr)] + pub fn check_unchecked_shr_i128() { + let num: i128 = kani::any::(); + let shift: u32 = kani::any::() % i128::BITS; + + unsafe { + num.unchecked_shr(shift); + } + } + + #[kani::proof_for_contract(u8::unchecked_shr)] + pub fn check_unchecked_shr_u8() { + let num: u8 = kani::any::(); + let shift: u32 = kani::any::() % u8::BITS; + + unsafe { + num.unchecked_shr(shift); + } + } + + #[kani::proof_for_contract(u16::unchecked_shr)] + pub fn check_unchecked_shr_u16() { + let num: u16 = kani::any::(); + let shift: u32 = kani::any::() % u16::BITS; + + unsafe { + num.unchecked_shr(shift); + } + } + + #[kani::proof_for_contract(u32::unchecked_shr)] + pub fn check_unchecked_shr_u32() { + let num: u32 = kani::any::(); + let shift: u32 = kani::any::() % u32::BITS; + + unsafe { + num.unchecked_shr(shift); + } + } + + #[kani::proof_for_contract(u64::unchecked_shr)] + pub fn check_unchecked_shr_u64() { + let num: u64 = kani::any::(); + let shift: u32 = kani::any::() % u64::BITS; + + unsafe { + num.unchecked_shr(shift); + } + } + + #[kani::proof_for_contract(u128::unchecked_shr)] + pub fn check_unchecked_shr_u128() { + let num: u128 = kani::any::(); + let shift: u32 = kani::any::() % u128::BITS; + + unsafe { + num.unchecked_shr(shift); + } + } } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index 48f0e2d4dc24b..4ca4e2bcb08b7 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -909,6 +909,8 @@ 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)] + #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, @@ -1614,6 +1616,8 @@ 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. + #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // ensures result is within range after bit shift pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self { assert_unsafe_precondition!( check_language_ub, From 864afa684013af8608c43740099e75c655d83060 Mon Sep 17 00:00:00 2001 From: Rajath Kotyal <53811196+rajathkotyal@users.noreply.github.com> Date: Wed, 25 Sep 2024 03:04:12 -0700 Subject: [PATCH 2/3] Small fix typo --- library/core/src/num/int_macros.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index 1f82f24c6bf27..07715ddaa3b70 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -1425,7 +1425,7 @@ macro_rules! int_impl { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")] - #[inline(always)]0 + #[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. #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // ensures result is within range after bit shift From ae678de8bda63673540fd1c5a2bbb5fb776bff94 Mon Sep 17 00:00:00 2001 From: rajathkotyal Date: Sun, 29 Sep 2024 04:32:21 -0700 Subject: [PATCH 3/3] added limits to multiplication proofs, reduced duplicacy in code by using macros to generate proof harnesses --- library/core/src/num/int_macros.rs | 3 - library/core/src/num/mod.rs | 412 +++++++--------------------- library/core/src/num/uint_macros.rs | 3 - 3 files changed, 103 insertions(+), 315 deletions(-) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index 07715ddaa3b70..a46e653de2bd0 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -512,7 +512,6 @@ macro_rules! int_impl { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires(!self.overflowing_add(rhs).1)] - #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] pub const unsafe fn unchecked_add(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, @@ -818,7 +817,6 @@ macro_rules! int_impl { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires(!self.overflowing_mul(rhs).1)] - #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, @@ -1428,7 +1426,6 @@ macro_rules! int_impl { #[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. - #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // ensures result is within range after bit shift 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 661c3f11cd3b6..186d05eda5a98 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1401,10 +1401,7 @@ const fn from_str_radix_panic_ct(_radix: u32) -> ! { #[track_caller] fn from_str_radix_panic_rt(radix: u32) -> ! { - panic!( - "from_str_radix_int: must lie in the range `[2, 36]` - found {}", - radix - ); + panic!("from_str_radix_int: must lie in the range `[2, 36]` - found {}", radix); } #[cfg_attr(not(feature = "panic_immediate_abort"), inline(never))] @@ -1589,346 +1586,143 @@ from_str_radix_size_impl! { i32 isize, u32 usize } #[cfg(target_pointer_width = "64")] from_str_radix_size_impl! { i64 isize, u64 usize } +#[cfg(kani)] #[unstable(feature = "kani", issue = "none")] mod verify { use super::*; - // `unchecked_add` proofs - // - // Target types: - // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total - // - // Target contracts: - // #[requires(!self.overflowing_add(rhs).1)] - // #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] - // - // Target function: - // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self - #[kani::proof_for_contract(i8::unchecked_add)] - pub fn check_unchecked_add_i8() { - let num1: i8 = kani::any::(); - let num2: i8 = kani::any::(); - - unsafe { - num1.unchecked_add(num2); - } - } - - #[kani::proof_for_contract(i16::unchecked_add)] - pub fn check_unchecked_add_i16() { - let num1: i16 = kani::any::(); - let num2: i16 = kani::any::(); - - unsafe { - num1.unchecked_add(num2); - } - } - - #[kani::proof_for_contract(i32::unchecked_add)] - pub fn check_unchecked_add_i32() { - let num1: i32 = kani::any::(); - let num2: i32 = kani::any::(); - - unsafe { - num1.unchecked_add(num2); - } - } - - #[kani::proof_for_contract(i64::unchecked_add)] - pub fn check_unchecked_add_i64() { - let num1: i64 = kani::any::(); - let num2: i64 = kani::any::(); - - unsafe { - num1.unchecked_add(num2); - } - } - - #[kani::proof_for_contract(i128::unchecked_add)] - pub fn check_unchecked_add_i128() { - let num1: i128 = kani::any::(); - let num2: i128 = kani::any::(); - - unsafe { - num1.unchecked_add(num2); - } - } - - #[kani::proof_for_contract(u8::unchecked_add)] - pub fn check_unchecked_add_u8() { - let num1: u8 = kani::any::(); - let num2: u8 = kani::any::(); - - unsafe { - num1.unchecked_add(num2); - } - } - - #[kani::proof_for_contract(u16::unchecked_add)] - pub fn check_unchecked_add_u16() { - let num1: u16 = kani::any::(); - let num2: u16 = kani::any::(); + macro_rules! generate_unchecked_math_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: $type = kani::any::<$type>(); - unsafe { - num1.unchecked_add(num2); + unsafe { + num1.$method(num2); + } + } } } - #[kani::proof_for_contract(u32::unchecked_add)] - pub fn check_unchecked_add_u32() { - let num1: u32 = kani::any::(); - let num2: u32 = kani::any::(); - - unsafe { - num1.unchecked_add(num2); + 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); + } + } } } - - #[kani::proof_for_contract(u64::unchecked_add)] - pub fn check_unchecked_add_u64() { - let num1: u64 = kani::any::(); - let num2: u64 = kani::any::(); - - unsafe { - num1.unchecked_add(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); + } + } } } + - #[kani::proof_for_contract(u128::unchecked_add)] - pub fn check_unchecked_add_u128() { - let num1: u128 = kani::any::(); - let num2: u128 = kani::any::(); + macro_rules! generate_unchecked_neg_harness { + ($type:ty, $method:ident, $harness_name:ident) => { + #[kani::proof_for_contract($type::$method)] + pub fn $harness_name() { + let num1: $type = kani::any::<$type>(); - unsafe { - num1.unchecked_add(num2); + unsafe { + num1.$method(); + } + } } } - // `unchecked_mul` proofs + // `unchecked_add` proofs // // Target types: - // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total + // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total // - // Target Files : src/num/int_macros.rs , src/num/uint_macros.rs + // Target contracts: + // #[requires(!self.overflowing_add(rhs).1)] // - // Target contracts : + // 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_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)] - // #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // - // Target function definition: + // 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); - #[kani::proof_for_contract(i8::unchecked_mul)] - pub fn check_unchecked_mul_i8() { - let num1: i8 = kani::any::(); - let num2: i8 = kani::any::(); - - unsafe { - num1.unchecked_mul(num2); - } - } - - #[kani::proof_for_contract(i16::unchecked_mul)] - pub fn check_unchecked_mul_i16() { - let num1: i16 = kani::any::(); - let num2: i16 = kani::any::(); - - unsafe { - num1.unchecked_mul(num2); - } - } - - #[kani::proof_for_contract(i32::unchecked_mul)] - pub fn check_unchecked_mul_i32() { - let num1: i32 = kani::any::(); - let num2: i32 = kani::any::(); - - unsafe { - num1.unchecked_mul(num2); - } - } - - #[kani::proof_for_contract(i64::unchecked_mul)] - pub fn check_unchecked_mul_i64() { - let num1: i64 = kani::any::(); - let num2: i64 = kani::any::(); - unsafe { - num1.unchecked_mul(num2); - } - } + 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); - #[kani::proof_for_contract(i128::unchecked_mul)] - pub fn check_unchecked_mul_i128() { - let num1: i128 = kani::any::(); - let num2: i128 = kani::any::(); - unsafe { - num1.unchecked_mul(num2); - } - } - - #[kani::proof_for_contract(u8::unchecked_mul)] - pub fn check_unchecked_mul_u8() { - let num1: u8 = kani::any::(); - let num2: u8 = kani::any::(); - - unsafe { - num1.unchecked_mul(num2); - } - } - - #[kani::proof_for_contract(u16::unchecked_mul)] - pub fn check_unchecked_mul_u16() { - let num1: u16 = kani::any::(); - let num2: u16 = kani::any::(); - - unsafe { - num1.unchecked_mul(num2); - } - } - - #[kani::proof_for_contract(u32::unchecked_mul)] - pub fn check_unchecked_mul_u32() { - let num1: u32 = kani::any::(); - let num2: u32 = kani::any::(); - - unsafe { - num1.unchecked_mul(num2); - } - } - - #[kani::proof_for_contract(u64::unchecked_mul)] - pub fn check_unchecked_mul_u64() { - let num1: u64 = kani::any::(); - let num2: u64 = kani::any::(); - - unsafe { - num1.unchecked_mul(num2); - } - } - - #[kani::proof_for_contract(u128::unchecked_mul)] - pub fn check_unchecked_mul_u128() { - let num1: u128 = kani::any::(); - let num2: u128 = kani::any::(); - - unsafe { - num1.unchecked_mul(num2); - } - } - - // `unchecked_shr` proofs + // unchecked_shr proofs // // Target types: - // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total - // - // Target Files : src/num/int_macros.rs , src/num/uint_macros.rs + // 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)] - // #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // // 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); - #[kani::proof_for_contract(i8::unchecked_shr)] - pub fn check_unchecked_shr_i8() { - let num: i8 = kani::any::(); - let shift: u32 = kani::any::() % i8::BITS; - - unsafe { - num.unchecked_shr(shift); - } - } - - #[kani::proof_for_contract(i16::unchecked_shr)] - pub fn check_unchecked_shr_i16() { - let num: i16 = kani::any::(); - let shift: u32 = kani::any::() % i16::BITS; - - unsafe { - num.unchecked_shr(shift); - } - } - - #[kani::proof_for_contract(i32::unchecked_shr)] - pub fn check_unchecked_shr_i32() { - let num: i32 = kani::any::(); - let shift: u32 = kani::any::() % i32::BITS; - - unsafe { - num.unchecked_shr(shift); - } - } - - #[kani::proof_for_contract(i64::unchecked_shr)] - pub fn check_unchecked_shr_i64() { - let num: i64 = kani::any::(); - let shift: u32 = kani::any::() % i64::BITS; - - unsafe { - num.unchecked_shr(shift); - } - } - - #[kani::proof_for_contract(i128::unchecked_shr)] - pub fn check_unchecked_shr_i128() { - let num: i128 = kani::any::(); - let shift: u32 = kani::any::() % i128::BITS; - - unsafe { - num.unchecked_shr(shift); - } - } - - #[kani::proof_for_contract(u8::unchecked_shr)] - pub fn check_unchecked_shr_u8() { - let num: u8 = kani::any::(); - let shift: u32 = kani::any::() % u8::BITS; - - unsafe { - num.unchecked_shr(shift); - } - } - - #[kani::proof_for_contract(u16::unchecked_shr)] - pub fn check_unchecked_shr_u16() { - let num: u16 = kani::any::(); - let shift: u32 = kani::any::() % u16::BITS; - - unsafe { - num.unchecked_shr(shift); - } - } - - #[kani::proof_for_contract(u32::unchecked_shr)] - pub fn check_unchecked_shr_u32() { - let num: u32 = kani::any::(); - let shift: u32 = kani::any::() % u32::BITS; - - unsafe { - num.unchecked_shr(shift); - } - } - - #[kani::proof_for_contract(u64::unchecked_shr)] - pub fn check_unchecked_shr_u64() { - let num: u64 = kani::any::(); - let shift: u32 = kani::any::() % u64::BITS; - - unsafe { - num.unchecked_shr(shift); - } - } - - #[kani::proof_for_contract(u128::unchecked_shr)] - pub fn check_unchecked_shr_u128() { - let num: u128 = kani::any::(); - let shift: u32 = kani::any::() % u128::BITS; - - unsafe { - num.unchecked_shr(shift); - } - } } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index 4ca4e2bcb08b7..8706ed8bd6d5f 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -559,7 +559,6 @@ macro_rules! uint_impl { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires(!self.overflowing_add(rhs).1)] - #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] pub const unsafe fn unchecked_add(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, @@ -910,7 +909,6 @@ macro_rules! uint_impl { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires(!self.overflowing_mul(rhs).1)] - #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, @@ -1617,7 +1615,6 @@ macro_rules! uint_impl { #[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. - #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // ensures result is within range after bit shift pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self { assert_unsafe_precondition!( check_language_ub,