From 3a967e316ab90736da81b75789dca9763a306f1e Mon Sep 17 00:00:00 2001 From: Yenyun035 <57857379+Yenyun035@users.noreply.github.com> Date: Thu, 17 Oct 2024 06:29:26 -0700 Subject: [PATCH] Contracts & Harnesses for `wrapping_shl` (#112) Towards #59 ### Changes * Added contracts for `wrapping_shl` (located in `library/core/src/num/int_macros.rs` and `uint_macros.rs`) * Added a macro for generating wrapping_{shl, shr} harnesses * Added harnesses for `wrapping_shl` of each integer type * `i8`, `i16`, `i32`, `i64`, `i128`, `isize`, `u8`, `u16`, `u32`, `u64`, `u128`, `usize` --- 12 harnesses in total. ### Revalidation 1. Per the discussion in #59, we have to **build and run Kani from `feature/verify-rust-std` branch**. 2. To revalidate the verification results, run the following command. `` can be either `num::verify` to run all harnesses or `num::verify::` (e.g. `checked_wrapping_shl_i8`) to run a specific harness. ``` kani verify-std "path/to/library" \ --harness \ -Z unstable-options \ -Z function-contracts \ -Z mem-predicates ``` All harnesses should pass the default checks (1251 checks where 1 unreachable). ``` SUMMARY: ** 0 of 1251 failed (1 unreachable) VERIFICATION:- SUCCESSFUL Verification Time: 2.4682913s Complete - 1 successfully verified harnesses, 0 failures, 1 total. ``` Example of the unreachable check: ``` Check 123: num::::wrapping_shl.assertion.1 - Status: UNREACHABLE - Description: "attempt to subtract with overflow" - Location: library/core/src/num/int_macros.rs:2172:42 in function num::::wrapping_shl ``` ### Questions 1. Should we add `requires` (and `ensures`) for `wrapping_shl` given that `unchecked_shl` already has a `requires`? By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- library/core/src/num/int_macros.rs | 1 + library/core/src/num/mod.rs | 38 +++++++++++++++++++++++++++++ library/core/src/num/uint_macros.rs | 1 + 3 files changed, 40 insertions(+) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index c84087172974a..03e1eb0bc5dab 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -2160,6 +2160,7 @@ macro_rules! int_impl { without modifying the original"] #[inline(always)] #[rustc_allow_const_fn_unstable(unchecked_shifts)] + #[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 91c1ccb708613..f84b769bee976 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1687,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: @@ -1905,4 +1918,29 @@ mod verify { widening_mul_u64_large, u64::MAX - 10u64, u64::MAX, widening_mul_u64_mid_edge, (u64::MAX / 2) - 10u64, (u64::MAX / 2) + 10u64 ); + + // `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); } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index 0576e087935bb..67b8768dea1d0 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -2138,6 +2138,7 @@ macro_rules! uint_impl { without modifying the original"] #[inline(always)] #[rustc_allow_const_fn_unstable(unchecked_shifts)] + #[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