From 1e5ba530923b95a892e7735167e7f45c80865050 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 9 Jul 2024 14:33:05 +0000
Subject: [PATCH 1/2] Add contracts for Layout and Alignment

These contracts seek to capture what is described in documentation and
debug assertions.
---
 library/core/src/alloc/layout.rs  | 30 ++++++++++++++++++++++++++++++
 library/core/src/ptr/alignment.rs |  6 ++++++
 2 files changed, 36 insertions(+)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index 0b92767c93205..87fb5e36091cf 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -4,12 +4,16 @@
 // collections, resulting in having to optimize down excess IR multiple times.
 // Your performance intuition is useless. Run perf.
 
+use safety::requires;
 use crate::cmp;
 use crate::error::Error;
 use crate::fmt;
 use crate::mem;
 use crate::ptr::{Alignment, NonNull};
 
+#[cfg(kani)]
+use crate::kani;
+
 // While this function is used in one place and its implementation
 // could be inlined, the previous attempts to do so made rustc
 // slower:
@@ -117,6 +121,9 @@ impl Layout {
     #[must_use]
     #[inline]
     #[rustc_allow_const_fn_unstable(ptr_alignment_type)]
+    #[requires(align > 0)]
+    #[requires((align & (align - 1)) == 0)]
+    #[requires(size <= isize::MAX as usize - (align - 1))]
     pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self {
         // SAFETY: the caller is required to uphold the preconditions.
         unsafe { Layout { size, align: Alignment::new_unchecked(align) } }
@@ -492,3 +499,26 @@ impl fmt::Display for LayoutError {
         f.write_str("invalid parameters to Layout::from_size_align")
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    #[kani::proof_for_contract(Layout::from_size_align_unchecked)]
+    pub fn check_from_size_align_unchecked() {
+        let shift_index = kani::any::<usize>();
+        kani::assume(shift_index < core::mem::size_of::<usize>() * 8);
+        let a : usize = 1 << shift_index;
+        kani::assume(a > 0);
+
+        let s = kani::any::<usize>();
+        kani::assume(s <= isize::MAX as usize - (a - 1));
+
+        unsafe {
+            let layout = Layout::from_size_align_unchecked(s, a);
+            assert_eq!(layout.size(), s);
+            assert_eq!(layout.align(), a);
+        }
+    }
+}
diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs
index 68fce3960c78c..e5f5bf6a50313 100644
--- a/library/core/src/ptr/alignment.rs
+++ b/library/core/src/ptr/alignment.rs
@@ -1,8 +1,12 @@
+use safety::requires;
 use crate::num::NonZero;
 #[cfg(debug_assertions)]
 use crate::ub_checks::assert_unsafe_precondition;
 use crate::{cmp, fmt, hash, mem, num};
 
+#[cfg(kani)]
+use crate::kani;
+
 /// A type storing a `usize` which is a power of two, and thus
 /// represents a possible alignment in the Rust abstract machine.
 ///
@@ -76,6 +80,8 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[requires(align > 0)]
+    #[requires((align & (align - 1)) == 0)]
     pub const unsafe fn new_unchecked(align: usize) -> Self {
         #[cfg(debug_assertions)]
         assert_unsafe_precondition!(

From 6dbf58e34987928fa429e9481211a63ad35491b1 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 11 Jul 2024 20:56:05 +0000
Subject: [PATCH 2/2] Apply suggestions

---
 library/core/src/alloc/layout.rs | 11 ++---------
 1 file changed, 2 insertions(+), 9 deletions(-)

diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index 87fb5e36091cf..c63db5aa0aa2f 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -121,9 +121,7 @@ impl Layout {
     #[must_use]
     #[inline]
     #[rustc_allow_const_fn_unstable(ptr_alignment_type)]
-    #[requires(align > 0)]
-    #[requires((align & (align - 1)) == 0)]
-    #[requires(size <= isize::MAX as usize - (align - 1))]
+    #[requires(Layout::from_size_align(size, align).is_ok())]
     pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self {
         // SAFETY: the caller is required to uphold the preconditions.
         unsafe { Layout { size, align: Alignment::new_unchecked(align) } }
@@ -507,13 +505,8 @@ mod verify {
 
     #[kani::proof_for_contract(Layout::from_size_align_unchecked)]
     pub fn check_from_size_align_unchecked() {
-        let shift_index = kani::any::<usize>();
-        kani::assume(shift_index < core::mem::size_of::<usize>() * 8);
-        let a : usize = 1 << shift_index;
-        kani::assume(a > 0);
-
         let s = kani::any::<usize>();
-        kani::assume(s <= isize::MAX as usize - (a - 1));
+        let a = kani::any::<usize>();
 
         unsafe {
             let layout = Layout::from_size_align_unchecked(s, a);