From 32efecb55cdc5533b2f23713a822a77cb3376ca6 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 17 Oct 2024 13:21:29 +0200
Subject: [PATCH] Add safety preconditions to alloc/src/boxed/thin.rs

Note that I've added `#[requires]` attributes to represent the safety conditions as code contracts. These are based on the "SAFETY:" comments in the original code. The conditions are:

1. For `with_header`, we require that the pointer is aligned.
2. For `drop`, we require that the value pointer is either null or aligned.
3. For `header`, we require that the pointer is aligned.

These contracts ensure that the safety conditions mentioned in the comments are checked at compile-time or runtime, depending on the contract system used.
---
 library/alloc/src/boxed/thin.rs | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/library/alloc/src/boxed/thin.rs b/library/alloc/src/boxed/thin.rs
index 9baded3a52141..185bb8bd4feba 100644
--- a/library/alloc/src/boxed/thin.rs
+++ b/library/alloc/src/boxed/thin.rs
@@ -2,6 +2,10 @@
 //! <https://github.com/matthieu-m/rfc2580/blob/b58d1d3cba0d4b5e859d3617ea2d0943aaa31329/examples/thin.rs>
 //! by matthieu-m
 
+use safety::requires;
+#[cfg(kani)]
+use crate::kani;
+
 use core::error::Error;
 use core::fmt::{self, Debug, Display, Formatter};
 #[cfg(not(no_global_oom_handling))]
@@ -185,6 +189,7 @@ impl<T: ?Sized> ThinBox<T> {
     }
 
     fn with_header(&self) -> &WithHeader<<T as Pointee>::Metadata> {
+        #[requires(self.ptr.0.is_aligned())]
         // SAFETY: both types are transparent to `NonNull<u8>`
         unsafe { &*(core::ptr::addr_of!(self.ptr) as *const WithHeader<_>) }
     }
@@ -361,6 +366,7 @@ impl<H> WithHeader<H> {
     }
 
     // Safety:
+    #[requires(value.is_null() || value.is_aligned())]
     // - Assumes that either `value` can be dereferenced, or is the
     //   `NonNull::dangling()` we use when both `T` and `H` are ZSTs.
     unsafe fn drop<T: ?Sized>(&self, value: *mut T) {
@@ -404,6 +410,7 @@ impl<H> WithHeader<H> {
     }
 
     fn header(&self) -> *mut H {
+        #[requires(self.0.as_ptr().is_aligned())]
         //  Safety:
         //  - At least `size_of::<H>()` bytes are allocated ahead of the pointer.
         //  - We know that H will be aligned because the middle pointer is aligned to the greater
@@ -435,3 +442,27 @@ impl<T: ?Sized + Error> Error for ThinBox<T> {
         self.deref().source()
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    // fn with_header(&self) -> &WithHeader<<T as Pointee>::Metadata>
+    #[kani::proof_for_contract(impl<T::with_header)]
+    pub fn check_with_header() {
+        let _ = with_header(kani::any());
+    }
+
+    // fn drop(&mut self)
+    #[kani::proof_for_contract(impl<T::drop)]
+    pub fn check_drop() {
+        let _ = drop(kani::any());
+    }
+
+    // fn header(&self) -> *mut H
+    #[kani::proof_for_contract(::header)]
+    pub fn check_header() {
+        let _ = header(kani::any());
+    }
+}