From 238b61213f746769853d2cc46033e23d3c33386a Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Thu, 10 Oct 2024 17:19:40 -0700 Subject: [PATCH 1/5] Add wrapping shift macro and wrapping_shl contracts & harnesses --- library/core/src/num/int_macros.rs | 5 ++++ library/core/src/num/mod.rs | 39 +++++++++++++++++++++++++++++ library/core/src/num/uint_macros.rs | 5 ++++ 3 files changed, 49 insertions(+) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index c84087172974a..a018ffaa32413 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -2160,6 +2160,11 @@ macro_rules! int_impl { without modifying the original"] #[inline(always)] #[rustc_allow_const_fn_unstable(unchecked_shifts)] + // Precondition: The right hand side of the shift (rhs) is less than + // the number of bits in the type. This prevents undefined behavior. + // TODO: Is requires needed? It's already specified in `unchecked_shl` + #[requires(rhs < Self::BITS)] + #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))] pub const fn wrapping_shl(self, rhs: u32) -> Self { // SAFETY: the masking by the bitsize of the type ensures that we do not shift // out of bounds diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index e8b7130995831..76c3e8b7e58fe 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1645,6 +1645,19 @@ mod verify { } } + // Verify `wrapping_{shl, shr}` + macro_rules! generate_wrapping_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::(); + + let _ = num1.$method(num2); + } + } + } + macro_rules! generate_unchecked_neg_harness { ($type:ty, $harness_name:ident) => { #[kani::proof_for_contract($type::unchecked_neg)] @@ -1849,4 +1862,30 @@ mod verify { 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); + + // `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: + // #[requires(rhs < Self::BITS)] + // #[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); } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index 0576e087935bb..576c5aa3e8b53 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -2138,6 +2138,11 @@ macro_rules! uint_impl { without modifying the original"] #[inline(always)] #[rustc_allow_const_fn_unstable(unchecked_shifts)] + // Precondition: The right hand side of the shift (rhs) is less than + // the number of bits in the type. This prevents undefined behavior. + // TODO: Is requires needed? It's already specified in `unchecked_shl` + #[requires(rhs < Self::BITS)] + #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))] pub const fn wrapping_shl(self, rhs: u32) -> Self { // SAFETY: the masking by the bitsize of the type ensures that we do not shift // out of bounds From 9e9259cc25088cf17beac00d2cfa6230f1f68e9a Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Thu, 10 Oct 2024 18:46:51 -0700 Subject: [PATCH 2/5] Fix comment --- library/core/src/num/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 76c3e8b7e58fe..1285d647bb8d6 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1645,7 +1645,7 @@ mod verify { } } - // Verify `wrapping_{shl, shr}` + // Verify `wrapping_{shl, shr}` which internally uses `unchecked_{shl,shr}` macro_rules! generate_wrapping_shift_harness { ($type:ty, $method:ident, $harness_name:ident) => { #[kani::proof_for_contract($type::$method)] From d4f8a9c797f13a43090c29a357b2dd61d0040a7d Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Fri, 11 Oct 2024 21:03:12 -0700 Subject: [PATCH 3/5] Remove wrapping_shl requires --- library/core/src/num/int_macros.rs | 4 ---- library/core/src/num/uint_macros.rs | 4 ---- 2 files changed, 8 deletions(-) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index a018ffaa32413..03e1eb0bc5dab 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -2160,10 +2160,6 @@ macro_rules! int_impl { without modifying the original"] #[inline(always)] #[rustc_allow_const_fn_unstable(unchecked_shifts)] - // Precondition: The right hand side of the shift (rhs) is less than - // the number of bits in the type. This prevents undefined behavior. - // TODO: Is requires needed? It's already specified in `unchecked_shl` - #[requires(rhs < Self::BITS)] #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))] pub const fn wrapping_shl(self, rhs: u32) -> Self { // SAFETY: the masking by the bitsize of the type ensures that we do not shift diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index 576c5aa3e8b53..67b8768dea1d0 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -2138,10 +2138,6 @@ macro_rules! uint_impl { without modifying the original"] #[inline(always)] #[rustc_allow_const_fn_unstable(unchecked_shifts)] - // Precondition: The right hand side of the shift (rhs) is less than - // the number of bits in the type. This prevents undefined behavior. - // TODO: Is requires needed? It's already specified in `unchecked_shl` - #[requires(rhs < Self::BITS)] #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))] pub const fn wrapping_shl(self, rhs: u32) -> Self { // SAFETY: the masking by the bitsize of the type ensures that we do not shift From 670997209f5790a4b1b2d823d9c4ad8571f6bf26 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Tue, 15 Oct 2024 15:33:36 -0700 Subject: [PATCH 4/5] Fix wrapping_shl harness comment --- library/core/src/num/mod.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 1285d647bb8d6..2b4b86982747e 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1869,7 +1869,6 @@ mod verify { // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total // // Target contracts: - // #[requires(rhs < Self::BITS)] // #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))] // // Target function: From 890778ddb48bf9239e075fe26e0908b98c16ba37 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Tue, 15 Oct 2024 15:37:30 -0700 Subject: [PATCH 5/5] Fix wrapping_shl harness comment --- library/core/src/num/mod.rs | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 2a789b50eeadd..f84b769bee976 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1645,19 +1645,6 @@ mod verify { } } - // Verify `wrapping_{shl, shr}` which internally uses `unchecked_{shl,shr}` - macro_rules! generate_wrapping_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::(); - - let _ = num1.$method(num2); - } - } - } - macro_rules! generate_unchecked_neg_harness { ($type:ty, $harness_name:ident) => { #[kani::proof_for_contract($type::unchecked_neg)] @@ -1700,6 +1687,19 @@ mod verify { } } + // Verify `wrapping_{shl, shr}` which internally uses `unchecked_{shl,shr}` + macro_rules! generate_wrapping_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::(); + + let _ = num1.$method(num2); + } + } + } + // `unchecked_add` proofs // // Target types: @@ -1928,7 +1928,7 @@ mod verify { // #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))] // // Target function: - // pub const fn wrapping_shl(self, rhs: u32) -> Self { + // 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);