Add safety preconditions to alloc/src/alloc.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/alloc.rs

@@ -10,6 +10,11 @@ use core::hint;
 #[cfg(not(test))]
 use core::ptr::{self, NonNull};
 
+use safety::requires;
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+use core::kani;
+
 #[cfg(test)]
 mod tests;
 
@@ -172,6 +177,7 @@ pub unsafe fn alloc_zeroed(layout: Layout) -> *mut u8 {
 
 #[cfg(not(test))]
 impl Global {
+    #[requires(layout.size() == 0 || layout.align() != 0)]
     #[inline]
     fn alloc_impl(&self, layout: Layout, zeroed: bool) -> Result<NonNull<[u8]>, AllocError> {
         match layout.size() {
@@ -186,6 +192,10 @@ impl Global {
     }
 
     // SAFETY: Same as `Allocator::grow`
+    #[requires(new_layout.size() >= old_layout.size())]
+    #[requires(old_layout.size() == 0 || old_layout.align() != 0)]
+    #[requires(new_layout.size() == 0 || new_layout.align() != 0)]
+    #[requires(ptr.as_ptr() as usize % old_layout.align() == 0)]
     #[inline]
     unsafe fn grow_impl(
         &self,
@@ -247,6 +257,8 @@ unsafe impl Allocator for Global {
     }
 
     #[inline]
+    #[requires(layout.size() == 0 || layout.align() != 0)]
+    #[requires(ptr.as_ptr() as usize % layout.align() == 0)]
     unsafe fn deallocate(&self, ptr: NonNull<u8>, layout: Layout) {
         if layout.size() != 0 {
             // SAFETY: `layout` is non-zero in size,
@@ -256,6 +268,10 @@ unsafe impl Allocator for Global {
     }
 
     #[inline]
+    #[requires(new_layout.size() >= old_layout.size())]
+    #[requires(old_layout.size() == 0 || old_layout.align() != 0)]
+    #[requires(new_layout.size() == 0 || new_layout.align() != 0)]
+    #[requires(ptr.as_ptr() as usize % old_layout.align() == 0)]
     unsafe fn grow(
         &self,
         ptr: NonNull<u8>,
@@ -267,6 +283,10 @@ unsafe impl Allocator for Global {
     }
 
     #[inline]
+    #[requires(new_layout.size() >= old_layout.size())]
+    #[requires(old_layout.size() == 0 || old_layout.align() != 0)]
+    #[requires(new_layout.size() == 0 || new_layout.align() != 0)]
+    #[requires(ptr.as_ptr() as usize % old_layout.align() == 0)]
     unsafe fn grow_zeroed(
         &self,
         ptr: NonNull<u8>,
@@ -278,6 +298,10 @@ unsafe impl Allocator for Global {
     }
 
     #[inline]
+    #[requires(new_layout.size() <= old_layout.size())]
+    #[requires(old_layout.size() == 0 || old_layout.align() != 0)]
+    #[requires(new_layout.size() == 0 || new_layout.align() != 0)]
+    #[requires(ptr.as_ptr() as usize % old_layout.align() == 0)]
     unsafe fn shrink(
         &self,
         ptr: NonNull<u8>,
@@ -423,3 +447,69 @@ pub mod __alloc_error_handler {
         }
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    // fn alloc_impl(&self, layout: Layout, zeroed: bool) -> Result<NonNull<[u8]>, AllocError>
+    #[kani::proof_for_contract(Global::alloc_impl)]
+    pub fn check_alloc_impl() {
+        let _ = Global.alloc_impl(kani::any(), kani::any());
+    }
+
+    // unsafe fn grow_impl(&self, ptr: NonNull<u8>, old_layout: Layout, new_layout: Layout, zeroed: bool) -> Result<NonNull<[u8]>, AllocError>
+    #[kani::proof_for_contract(Global::grow_impl)]
+    pub fn check_grow_impl() {
+        let raw_ptr = kani::any::<usize>() as *mut u8;
+        unsafe {
+            let n = NonNull::new_unchecked(raw_ptr);
+            let _ = Global.grow_impl(n, kani::any(), kani::any(), kani::any());
+        }
+    }
+
+    // unsafe fn deallocate(&self, ptr: NonNull<u8>, layout: Layout)
+    #[kani::proof_for_contract(Allocator::deallocate)]
+    pub fn check_deallocate() {
+        let obj : &dyn Allocator = &Global;
+        let raw_ptr = kani::any::<usize>() as *mut u8;
+        unsafe {
+            let n = NonNull::new_unchecked(raw_ptr);
+            let _ = obj.deallocate(n, kani::any());
+        }
+    }
+
+    // unsafe fn grow(&self, ptr: NonNull<u8>, old_layout: Layout, new_layout: Layout) -> Result<NonNull<[u8]>, AllocError>
+    #[kani::proof_for_contract(Allocator::grow)]
+    pub fn check_grow() {
+        let obj : &dyn Allocator = &Global;
+        let raw_ptr = kani::any::<usize>() as *mut u8;
+        unsafe {
+            let n = NonNull::new_unchecked(raw_ptr);
+            let _ = obj.grow(n, kani::any(), kani::any());
+        }
+    }
+
+    // unsafe fn grow_zeroed(&self, ptr: NonNull<u8>, old_layout: Layout, new_layout: Layout) -> Result<NonNull<[u8]>, AllocError>
+    #[kani::proof_for_contract(Allocator::grow_zeroed)]
+    pub fn check_grow_zeroed() {
+        let obj : &dyn Allocator = &Global;
+        let raw_ptr = kani::any::<usize>() as *mut u8;
+        unsafe {
+            let n = NonNull::new_unchecked(raw_ptr);
+            let _ = obj.grow_zeroed(n, kani::any(), kani::any());
+        }
+    }
+
+    // unsafe fn shrink(&self, ptr: NonNull<u8>, old_layout: Layout, new_layout: Layout) -> Result<NonNull<[u8]>, AllocError>
+    #[kani::proof_for_contract(Allocator::shrink)]
+    pub fn check_shrink() {
+        let obj : &dyn Allocator = &Global;
+        let raw_ptr = kani::any::<usize>() as *mut u8;
+        unsafe {
+            let n = NonNull::new_unchecked(raw_ptr);
+            let _ = obj.shrink(n, kani::any(), kani::any());
+        }
+    }
+}

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)]

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