From a636c052abbcff26ac8f07a16c623ef7cd6fa5b1 Mon Sep 17 00:00:00 2001 From: MWDZ <101102544+MWDZ@users.noreply.github.com> Date: Mon, 21 Oct 2024 18:14:25 -0700 Subject: [PATCH] Contracts & Harnesses for wrapping_shr (#123) Towards https://github.com/model-checking/verify-rust-std/issues/59 Changes Added contracts for wrapping_shr (located in library/core/src/num/int_macros.rs and uint_macros.rs) Added harnesses for wrapping_shr of each integer type i8, i16, i32, i64, i128, isize, u8, u16, u32, u64, u128, usize --- 12 harnesses in total. Revalidation Per the discussion in https://github.com/model-checking/verify-rust-std/issues/59, we have to build and run Kani from feature/verify-rust-std branch. 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 161 failed (1 unreachable) VERIFICATION:- SUCCESSFUL Verification Time: 0.32086188s Complete - 12 successfully verified harnesses, 0 failures, 12 total. ``` Example of the unreachable check: ``` Check 9: num::::wrapping_shr.assertion.1 - Status: UNREACHABLE - Description: "attempt to subtract with overflow" - Location: library/core/src/num/int_macros.rs:2199:42 in function num::::wrapping_shr ``` --------- Co-authored-by: Yenyun035 --- library/core/src/num/int_macros.rs | 1 + library/core/src/num/mod.rs | 24 ++++++++++++++++++++++++ library/core/src/num/uint_macros.rs | 1 + 3 files changed, 26 insertions(+) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index 03e1eb0bc5dab..4ff7f97542d93 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -2191,6 +2191,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_shr(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 f84b769bee976..b123d998a8466 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1943,4 +1943,28 @@ mod verify { 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); + + // `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); } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index 67b8768dea1d0..3220be1d86f30 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -2172,6 +2172,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_shr(self, rhs: u32) -> Self { // SAFETY: the masking by the bitsize of the type ensures that we do not shift // out of bounds