From 96f16035d754d11b428d2a5f1db105c4ecda9ff1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 23 Jul 2024 12:40:14 +0000 Subject: [PATCH] Add harnesses for all public functions of `Layout` Exercise all public member functions of `Layout` and assert properties over the result. Some of those should, perhaps, become `ensures` clauses. --- library/core/src/alloc/layout.rs | 199 +++++++++++++++++++++++++++++++ 1 file changed, 199 insertions(+) diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs index c63db5aa0aa2f..b5074a215645b 100644 --- a/library/core/src/alloc/layout.rs +++ b/library/core/src/alloc/layout.rs @@ -503,6 +503,22 @@ impl fmt::Display for LayoutError { mod verify { use super::*; + // 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::(); + + if let Some(layout) = Layout::from_size_align(s, a) { + assert_eq!(layout.size(), s); + assert_eq!(layout.align(), a); + assert!(a > 0); + assert!(a.is_power_of_two()); + assert!(s <= isize::MAX as usize - (a - 1)); + } + } + + // 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::(); @@ -514,4 +530,187 @@ mod verify { assert_eq!(layout.align(), a); } } + + // pub const fn size(&self) -> usize + #[kani::proof_for_contract(Layout::size)] + pub fn check_size() { + let s = kani::any::(); + let a = kani::any::(); + + unsafe { + let layout = Layout::from_size_align_unchecked(s, a); + assert_eq!(layout.size(), s); + } + } + + // pub const fn align(&self) -> usize + #[kani::proof_for_contract(Layout::align)] + pub fn check_align() { + let s = kani::any::(); + let a = kani::any::(); + + unsafe { + let layout = Layout::from_size_align_unchecked(s, a); + 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 = Layout::new(); + assert_eq!(layout.size(), 4); + assert!(layout.align().is_power_of_two()); + } + + // pub const fn for_value(t: &T) -> Self + #[kani::proof_for_contract(Layout::for_value)] + pub fn check_for_value_i32() { + let array : [i32; 2] = [1, 2]; + let layout = Layout::for_value<&i32>(&array[1 .. 1); + assert!(layout.align().is_power_of_two()); + } + + // 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 layout = Layout::for_value_raw(&[]); + assert!(layout.align().is_power_of_two()); + } + } + + // pub const fn dangling(&self) -> NonNull + #[kani::proof_for_contract(Layout::dangling)] + pub fn check_dangling() { + let s = kani::any::(); + let a = kani::any::(); + + unsafe { + let layout = Layout::from_size_align_unchecked(s, a); + assert!(layout.dangling().is_aligned()); + } + } + + // pub fn align_to(&self, align: usize) -> Result + #[kani::proof_for_contract(Layout::align_to)] + pub fn check_align_to() { + let s = kani::any::(); + let a = kani::any::(); + + unsafe { + let layout = Layout::from_size_align_unchecked(s, a); + let a2 = kani::any::(); + if let Some(layout2) = layout.align_to(a2) { + assert!(layout2.align() > 0); + assert!(layout2.align().is_power_of_two()); + } + } + } + + // 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 s = kani::any::(); + let a = kani::any::(); + + unsafe { + let layout = Layout::from_size_align_unchecked(s, a); + let a2 = kani::any::(); + if(a2.is_power_of_two() && a2 <= a) { + let p = layout.padding_needed_for(a2); + assert!(p <= a2); + } + } + } + + // pub const fn pad_to_align(&self) -> Layout + #[kani::proof_for_contract(Layout::pad_to_align)] + pub fn check_pad_to_align() { + let s = kani::any::(); + let a = kani::any::(); + + unsafe { + let layout = Layout::from_size_align_unchecked(s, a); + let layout2 = layout.pad_to_align(); + assert_eq!(layout2.size() % a, 0); + assert_eq!(layout.size() + layout.padding_needed_for(layout.align()), layout2.size()); + } + } + + // pub fn repeat(&self, n: usize) -> Result<(Self, usize), LayoutError> + #[kani::proof_for_contract(Layout::repeat)] + pub fn check_repeat() { + let s = kani::any::(); + let a = kani::any::(); + + unsafe { + let layout = Layout::from_size_align_unchecked(s, a); + let n = kani::any::(); + if let Some((layout2, padding)) = layout.repeat(n) { + assert!(n == 0 || layout2.size() >= s); + assert!(n == 0 || padding < a); + } + } + } + + // pub fn extend(&self, next: Self) -> Result<(Self, usize), LayoutError> + #[kani::proof_for_contract(Layout::extend)] + pub fn check_extend() { + let s = kani::any::(); + let a = kani::any::(); + + unsafe { + let layout = Layout::from_size_align_unchecked(s, a); + let s2 = kani::any::(); + let a2 = kani::any::(); + let layout2 = Layout::from_size_align_unchecked(s2, a2); + if let Some((layout3, offset)) = layout.extend(layout2) { + assert_eq!(layout3.align(), cmp::max(a, a2)); + assert!(layout3.size() >= s + s2); + assert!(offset >= s); + assert!(offset <= layout3.size()); + } + } + } + + // pub fn repeat_packed(&self, n: usize) -> Result + #[kani::proof_for_contract(Layout::repeat_packed)] + pub fn check_repeat_packed() { + let s = kani::any::(); + let a = kani::any::(); + + unsafe { + let layout = Layout::from_size_align_unchecked(s, a); + let n = kani::any::(); + if let Some(layout2) = layout.repeat_packed(n) { + assert!(n == 0 || layout2.size() >= s); + } + } + } + + // pub fn extend_packed(&self, next: Self) -> Result + #[kani::proof_for_contract(Layout::extend_packed)] + pub fn check_extend_packed() { + let s = kani::any::(); + let a = kani::any::(); + + unsafe { + let layout = Layout::from_size_align_unchecked(s, a); + let s2 = kani::any::(); + let a2 = kani::any::(); + let layout2 = Layout::from_size_align_unchecked(s2, a2); + if let Some(layout3) = layout.extend_packed(layout2) { + assert_eq!(layout3.align(), a); + assert_eq!(layout3.size(), s + s2); + } + } + } + + // pub const fn array(n: usize) -> Result + #[kani::proof_for_contract(Layout::array)] + pub fn check_array_i32() { + let layout = Layout::array(); + assert!(layout.align().is_power_of_two()); + } }