From 024d84bf13d05afea968ef47d82c7c0c0e7781a7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 2 Oct 2024 23:20:07 +0200 Subject: [PATCH] Add harnesses for all public functions of `Layout` (#43) Exercise all public member functions of `Layout` and assert properties over the result. Some of those should, perhaps, become `ensures` clauses. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Celina G. Val --- library/core/src/alloc/layout.rs | 193 ++++++++++++++++++++++++++++++- 1 file changed, 191 insertions(+), 2 deletions(-) diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs index 789f9248e7fab..666c5be7c29b5 100644 --- a/library/core/src/alloc/layout.rs +++ b/library/core/src/alloc/layout.rs @@ -4,7 +4,7 @@ // collections, resulting in having to optimize down excess IR multiple times. // Your performance intuition is useless. Run perf. -use safety::requires; +use safety::{ensures, requires}; use crate::error::Error; use crate::ptr::{Alignment, NonNull}; use crate::{assert_unsafe_precondition, cmp, fmt, mem}; @@ -69,6 +69,10 @@ impl Layout { #[rustc_const_stable(feature = "const_alloc_layout_size_align", since = "1.50.0")] #[inline] #[rustc_allow_const_fn_unstable(ptr_alignment_type)] + #[ensures(|result| result.is_err() || align.is_power_of_two())] + #[ensures(|result| result.is_err() || size <= isize::MAX as usize - (align - 1))] + #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == size)] + #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == align)] pub const fn from_size_align(size: usize, align: usize) -> Result { if Layout::is_size_align_valid(size, align) { // SAFETY: Layout::is_size_align_valid checks the preconditions for this call. @@ -128,6 +132,8 @@ impl Layout { #[inline] #[rustc_allow_const_fn_unstable(ptr_alignment_type)] #[requires(Layout::from_size_align(size, align).is_ok())] + #[ensures(|result| result.size() == size)] + #[ensures(|result| result.align() == align)] pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self { assert_unsafe_precondition!( check_library_ub, @@ -169,6 +175,8 @@ impl Layout { #[rustc_const_stable(feature = "alloc_layout_const_new", since = "1.42.0")] #[must_use] #[inline] + #[ensures(|result| result.size() == mem::size_of::())] + #[ensures(|result| result.align() == mem::align_of::())] pub const fn new() -> Self { let (size, align) = size_align::(); // SAFETY: if the type is instantiated, rustc already ensures that its @@ -184,6 +192,8 @@ impl Layout { #[rustc_const_unstable(feature = "const_alloc_layout", issue = "67521")] #[must_use] #[inline] + #[requires(mem::align_of_val(t).is_power_of_two())] + #[ensures(|result| result.align() == mem::align_of_val(t))] pub const fn for_value(t: &T) -> Self { let (size, align) = (mem::size_of_val(t), mem::align_of_val(t)); // SAFETY: see rationale in `new` for why this is using the unsafe variant @@ -220,6 +230,10 @@ impl Layout { #[unstable(feature = "layout_for_ptr", issue = "69835")] #[rustc_const_unstable(feature = "const_alloc_layout", issue = "67521")] #[must_use] + // TODO: we should try to capture the above constraints on T in a `requires` clause, and the + // metadata helpers from https://github.com/model-checking/verify-rust-std/pull/37 may be able + // to accomplish this. + #[ensures(|result| result.align().is_power_of_two())] pub const unsafe fn for_value_raw(t: *const T) -> Self { // SAFETY: we pass along the prerequisites of these functions to the caller let (size, align) = unsafe { (mem::size_of_val_raw(t), mem::align_of_val_raw(t)) }; @@ -237,6 +251,7 @@ impl Layout { #[rustc_const_unstable(feature = "alloc_layout_extra", issue = "55724")] #[must_use] #[inline] + #[ensures(|result| result.is_aligned())] pub const fn dangling(&self) -> NonNull { // SAFETY: align is guaranteed to be non-zero unsafe { NonNull::new_unchecked(crate::ptr::without_provenance_mut::(self.align())) } @@ -258,6 +273,8 @@ impl Layout { /// `align` violates the conditions listed in [`Layout::from_size_align`]. #[stable(feature = "alloc_layout_manipulation", since = "1.44.0")] #[inline] + #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() >= align)] + #[ensures(|result| result.is_err() || result.as_ref().unwrap().align().is_power_of_two())] pub fn align_to(&self, align: usize) -> Result { Layout::from_size_align(self.size(), cmp::max(self.align(), align)) } @@ -283,6 +300,7 @@ impl Layout { #[must_use = "this returns the padding needed, \ without modifying the `Layout`"] #[inline] + #[ensures(|result| *result <= align)] pub const fn padding_needed_for(&self, align: usize) -> usize { let len = self.size(); @@ -319,6 +337,10 @@ impl Layout { #[must_use = "this returns a new `Layout`, \ without modifying the original"] #[inline] + #[ensures(|result| result.size() >= self.size())] + #[ensures(|result| result.align() == self.align())] + #[ensures(|result| result.size() % result.align() == 0)] + #[ensures(|result| self.size() + self.padding_needed_for(self.align()) == result.size())] pub const fn pad_to_align(&self) -> Layout { let pad = self.padding_needed_for(self.align()); // This cannot overflow. Quoting from the invariant of Layout: @@ -341,6 +363,20 @@ impl Layout { /// On arithmetic overflow, returns `LayoutError`. #[unstable(feature = "alloc_layout_extra", issue = "55724")] #[inline] + // for Kani (v0.54.0), the below modulo operation is too costly to prove (running into the + // 6-hours timeout on GitHub); we use a weaker postcondition instead + #[cfg_attr(not(kani), + ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() % n == 0))] + #[cfg_attr(kani, + ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= self.size()))] + // for Kani (v0.54.0), the below multiplication is too costly to prove (running into the + // 6-hours timeout on GitHub); we use a weaker postcondition instead + #[cfg_attr(not(kani), + ensures(|result| result.is_err() || + result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1))] + #[cfg_attr(kani, + ensures(|result| result.is_err() || n == 0 || + result.as_ref().unwrap().0.size() >= result.as_ref().unwrap().1))] pub fn repeat(&self, n: usize) -> Result<(Self, usize), LayoutError> { // This cannot overflow. Quoting from the invariant of Layout: // > `size`, when rounded up to the nearest multiple of `align`, @@ -401,6 +437,10 @@ impl Layout { /// ``` #[stable(feature = "alloc_layout_manipulation", since = "1.44.0")] #[inline] + #[ensures(|result| result.is_err() || result.as_ref().unwrap().0.align() == cmp::max(self.align(), next.align()))] + #[ensures(|result| result.is_err() || result.as_ref().unwrap().0.size() >= self.size() + next.size())] + #[ensures(|result| result.is_err() || result.as_ref().unwrap().1 >= self.size())] + #[ensures(|result| result.is_err() || result.as_ref().unwrap().1 <= result.as_ref().unwrap().0.size())] pub fn extend(&self, next: Self) -> Result<(Self, usize), LayoutError> { let new_align = cmp::max(self.align, next.align); let pad = self.padding_needed_for(next.align()); @@ -427,6 +467,13 @@ impl Layout { /// On arithmetic overflow, returns `LayoutError`. #[unstable(feature = "alloc_layout_extra", issue = "55724")] #[inline] + // for Kani (v0.54.0), the below multiplication is too costly to prove (running into the + // 6-hours timeout on GitHub); we use a weaker postcondition instead + #[cfg_attr(not(kani), + ensures(|result| result.is_err() || result.as_ref().unwrap().size() == n * self.size()))] + #[cfg_attr(kani, + ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().size() >= self.size()))] + #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == self.align())] pub fn repeat_packed(&self, n: usize) -> Result { let size = self.size().checked_mul(n).ok_or(LayoutError)?; // The safe constructor is called here to enforce the isize size limit. @@ -441,6 +488,8 @@ impl Layout { /// On arithmetic overflow, returns `LayoutError`. #[unstable(feature = "alloc_layout_extra", issue = "55724")] #[inline] + #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == self.size() + next.size())] + #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == self.align())] pub fn extend_packed(&self, next: Self) -> Result { let new_size = self.size().checked_add(next.size()).ok_or(LayoutError)?; // The safe constructor is called here to enforce the isize size limit. @@ -454,6 +503,8 @@ impl Layout { #[stable(feature = "alloc_layout_manipulation", since = "1.44.0")] #[rustc_const_unstable(feature = "const_alloc_layout", issue = "67521")] #[inline] + #[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == n * mem::size_of::())] + #[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == mem::align_of::())] pub const fn array(n: usize) -> Result { // Reduce the amount of code we need to monomorphize per `T`. return inner(mem::size_of::(), Alignment::of::(), n); @@ -520,15 +571,153 @@ impl fmt::Display for LayoutError { mod verify { use super::*; + impl kani::Arbitrary for Layout { + fn any() -> Self { + let align = kani::any::(); + let size = kani::any_where(|s: &usize| *s <= isize::MAX as usize - (align.as_usize() - 1)); + unsafe { Layout { size, align } } + } + } + + // pub const fn from_size_align(size: usize, align: usize) -> Result + #[kani::proof_for_contract(Layout::from_size_align)] + pub fn check_from_size_align() { + let s = kani::any::(); + let a = kani::any::(); + let _ = Layout::from_size_align(s, a); + } + + // pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self #[kani::proof_for_contract(Layout::from_size_align_unchecked)] pub fn check_from_size_align_unchecked() { let s = kani::any::(); let a = kani::any::(); + unsafe { + let _ = Layout::from_size_align_unchecked(s, a); + } + } + // pub const fn size(&self) -> usize + #[kani::proof] + pub fn check_size() { + let s = kani::any::(); + let a = kani::any::(); + kani::assume(Layout::from_size_align(s, a).is_ok()); unsafe { let layout = Layout::from_size_align_unchecked(s, a); assert_eq!(layout.size(), s); - assert_eq!(layout.align(), a); + } + } + + // pub const fn align(&self) -> usize + #[kani::proof] + pub fn check_align() { + let layout = kani::any::(); + assert!(layout.align().is_power_of_two()); + } + + // pub const fn new() -> Self + #[kani::proof_for_contract(Layout::new)] + pub fn check_new_i32() { + let _ = Layout::new::(); + } + + // pub const fn for_value(t: &T) -> Self + #[kani::proof_for_contract(Layout::for_value)] + pub fn check_for_value_i32() { + let x = kani::any::(); + let _ = Layout::for_value::(&x); + let array : [i32; 2] = [1, 2]; + let _ = Layout::for_value::<[i32]>(&array[1 .. 1]); + let trait_ref: &dyn core::fmt::Debug = &x; + let _ = Layout::for_value::(trait_ref); + // TODO: the case of an extern type as unsized tail is not yet covered + } + + // pub const unsafe fn for_value_raw(t: *const T) -> Self + #[kani::proof_for_contract(Layout::for_value_raw)] + pub fn check_for_value_raw_i32() { + unsafe { + let x = kani::any::(); + let _ = Layout::for_value_raw::(&x as *const i32); + let _ = Layout::for_value_raw::<[i32]>(&[] as *const [i32]); + let trait_ref: &dyn core::fmt::Debug = &x; + let _ = Layout::for_value_raw::(trait_ref); + // TODO: the case of an extern type as unsized tail is not yet covered + } + } + + // pub const fn dangling(&self) -> NonNull + #[kani::proof_for_contract(Layout::dangling)] + pub fn check_dangling() { + let layout = kani::any::(); + let _ = layout.dangling(); + } + + // pub fn align_to(&self, align: usize) -> Result + #[kani::proof_for_contract(Layout::align_to)] + pub fn check_align_to() { + let layout = kani::any::(); + let a2 = kani::any::(); + let _ = layout.align_to(a2); + } + + // pub const fn padding_needed_for(&self, align: usize) -> usize + #[kani::proof_for_contract(Layout::padding_needed_for)] + pub fn check_padding_needed_for() { + let layout = kani::any::(); + let a2 = kani::any::(); + if(a2.is_power_of_two() && a2 <= layout.align()) { + let _ = layout.padding_needed_for(a2); + } + } + + // pub const fn pad_to_align(&self) -> Layout + #[kani::proof_for_contract(Layout::pad_to_align)] + pub fn check_pad_to_align() { + let layout = kani::any::(); + let _ = layout.pad_to_align(); + } + + // pub fn repeat(&self, n: usize) -> Result<(Self, usize), LayoutError> + #[kani::proof_for_contract(Layout::repeat)] + pub fn check_repeat() { + let layout = kani::any::(); + let n = kani::any::(); + let _ = layout.repeat(n); + } + + // pub fn extend(&self, next: Self) -> Result<(Self, usize), LayoutError> + #[kani::proof_for_contract(Layout::extend)] + pub fn check_extend() { + let layout = kani::any::(); + let layout2 = kani::any::(); + let _ = layout.extend(layout2); + } + + // pub fn repeat_packed(&self, n: usize) -> Result + #[kani::proof_for_contract(Layout::repeat_packed)] + pub fn check_repeat_packed() { + let layout = kani::any::(); + let n = kani::any::(); + let _ = layout.repeat_packed(n); + } + + // pub fn extend_packed(&self, next: Self) -> Result + #[kani::proof_for_contract(Layout::extend_packed)] + pub fn check_extend_packed() { + let layout = kani::any::(); + let layout2 = kani::any::(); + let _ = layout.extend_packed(layout2); + } + + // pub const fn array(n: usize) -> Result + #[kani::proof_for_contract(Layout::array)] + pub fn check_array_i32() { + let n = kani::any::(); + if let Ok(layout) = Layout::array::(n) { + assert!(layout.size() >= n * 4); + assert!(layout.align().is_power_of_two()); } } }