Merge branch 'main' into sift_up

qinheping · Oct 22, 2024 · 521394a · 521394a
2 parents eed4094 + 38d490c
commit 521394a
Show file tree

Hide file tree

Showing 8 changed files with 31 additions and 1 deletion.
diff --git a/README.md b/README.md
@@ -47,4 +47,4 @@ See [the Rust repository](https://github.com/rust-lang/rust) for details.
 
 ## Introducing a New Tool
 
-Please use the [template available in this repository](.github/TOOL_REQUEST_TEMPLATE.md) to introduce a new verification tool.
+Please use the [template available in this repository](./doc/src/tool_template.md) to introduce a new verification tool.
diff --git a/library/alloc/Cargo.toml b/library/alloc/Cargo.toml
@@ -12,6 +12,7 @@ edition = "2021"
 core = { path = "../core" }
 safety = { path = "../contracts/safety" }
 compiler_builtins = { version = "0.1.123", features = ['rustc-dep-of-std'] }
+safety = { path = "../contracts/safety" }
 
 [dev-dependencies]
 rand = { version = "0.8.5", default-features = false, features = ["alloc"] }

diff --git a/library/alloc/src/lib.rs b/library/alloc/src/lib.rs
@@ -91,6 +91,7 @@
 //
 // Library features:
 // tidy-alphabetical-start
+#![cfg_attr(kani, feature(kani))]
 #![cfg_attr(not(no_global_oom_handling), feature(const_alloc_error))]
 #![cfg_attr(not(no_global_oom_handling), feature(const_btree_len))]
 #![feature(alloc_layout_extra)]

diff --git 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
@@ -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
@@ -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

diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml
@@ -26,6 +26,7 @@ hashbrown = { version = "0.14", default-features = false, features = [
 std_detect = { path = "../stdarch/crates/std_detect", default-features = false, features = [
     'rustc-dep-of-std',
 ] }
+safety = { path = "../contracts/safety" }
 
 # Dependencies of the `backtrace` crate
 rustc-demangle = { version = "0.1.24", features = ['rustc-dep-of-std'] }

diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs
@@ -269,6 +269,7 @@
 #![cfg_attr(any(windows, target_os = "uefi"), feature(round_char_boundary))]
 #![cfg_attr(target_family = "wasm", feature(stdarch_wasm_atomic_wait))]
 #![cfg_attr(target_arch = "wasm64", feature(simd_wasm64))]
+#![cfg_attr(kani, feature(kani))]
 //
 // Language features:
 // tidy-alphabetical-start