Add safety preconditions to alloc/src/boxed/thin.rs

library/alloc/Cargo.toml

@@ -11,6 +11,7 @@ edition = "2021"
 [dependencies]
 core = { path = "../core" }
 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"] }

library/alloc/src/boxed/thin.rs

@@ -2,6 +2,12 @@
 //! <https://github.com/matthieu-m/rfc2580/blob/b58d1d3cba0d4b5e859d3617ea2d0943aaa31329/examples/thin.rs>
 //! by matthieu-m
 
+use safety::requires;
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+use core::kani;
+use core::ub_checks;
+
 use core::error::Error;
 use core::fmt::{self, Debug, Display, Formatter};
 #[cfg(not(no_global_oom_handling))]
@@ -363,6 +369,8 @@ impl<H> WithHeader<H> {
     // Safety:
     // - Assumes that either `value` can be dereferenced, or is the
     //   `NonNull::dangling()` we use when both `T` and `H` are ZSTs.
+    #[requires((mem::size_of_val_raw(value) == 0 && size_of::<H>() == 0) ||
+        ub_checks::can_dereference(value))]
     unsafe fn drop<T: ?Sized>(&self, value: *mut T) {
         struct DropGuard<H> {
             ptr: NonNull<u8>,
@@ -435,3 +443,20 @@ impl<T: ?Sized + Error> Error for ThinBox<T> {
         self.deref().source()
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    // unsafe fn drop<T: ?Sized>(&self, value: *mut T)
+    #[kani::proof_for_contract(WithHeader<T>::drop)]
+    pub fn check_drop() {
+        let w = WithHeader::new(kani::any::<usize>(), kani::any::<usize>());
+        let mut x : usize = kani::any();
+        let xptr = &mut x;
+        unsafe {
+            let _ = w.drop(xptr);
+        }
+    }
+}

library/alloc/src/lib.rs

@@ -91,6 +91,8 @@
 //
 // Library features:
 // tidy-alphabetical-start
+#![cfg_attr(kani, feature(kani))]
+#![cfg_attr(kani, feature(ub_checks))]
 #![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)]

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'] }

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