Skip to content

Commit 024d84b

Browse files
tautschnigcelinval
tautschnig
and
celinval
authored
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 <[email protected]>
1 parent 85a59bc commit 024d84b

File tree

1 file changed

+191
-2
lines changed

1 file changed

+191
-2
lines changed

‎library/core/src/alloc/layout.rs

+191-2
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
// collections, resulting in having to optimize down excess IR multiple times.
55
// Your performance intuition is useless. Run perf.
66

7-
use safety::requires;
7+
use safety::{ensures, requires};
88
use crate::error::Error;
99
use crate::ptr::{Alignment, NonNull};
1010
use crate::{assert_unsafe_precondition, cmp, fmt, mem};
@@ -69,6 +69,10 @@ impl Layout {
6969
#[rustc_const_stable(feature = "const_alloc_layout_size_align", since = "1.50.0")]
7070
#[inline]
7171
#[rustc_allow_const_fn_unstable(ptr_alignment_type)]
72+
#[ensures(|result| result.is_err() || align.is_power_of_two())]
73+
#[ensures(|result| result.is_err() || size <= isize::MAX as usize - (align - 1))]
74+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == size)]
75+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == align)]
7276
pub const fn from_size_align(size: usize, align: usize) -> Result<Self, LayoutError> {
7377
if Layout::is_size_align_valid(size, align) {
7478
// SAFETY: Layout::is_size_align_valid checks the preconditions for this call.
@@ -128,6 +132,8 @@ impl Layout {
128132
#[inline]
129133
#[rustc_allow_const_fn_unstable(ptr_alignment_type)]
130134
#[requires(Layout::from_size_align(size, align).is_ok())]
135+
#[ensures(|result| result.size() == size)]
136+
#[ensures(|result| result.align() == align)]
131137
pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self {
132138
assert_unsafe_precondition!(
133139
check_library_ub,
@@ -169,6 +175,8 @@ impl Layout {
169175
#[rustc_const_stable(feature = "alloc_layout_const_new", since = "1.42.0")]
170176
#[must_use]
171177
#[inline]
178+
#[ensures(|result| result.size() == mem::size_of::<T>())]
179+
#[ensures(|result| result.align() == mem::align_of::<T>())]
172180
pub const fn new<T>() -> Self {
173181
let (size, align) = size_align::<T>();
174182
// SAFETY: if the type is instantiated, rustc already ensures that its
@@ -184,6 +192,8 @@ impl Layout {
184192
#[rustc_const_unstable(feature = "const_alloc_layout", issue = "67521")]
185193
#[must_use]
186194
#[inline]
195+
#[requires(mem::align_of_val(t).is_power_of_two())]
196+
#[ensures(|result| result.align() == mem::align_of_val(t))]
187197
pub const fn for_value<T: ?Sized>(t: &T) -> Self {
188198
let (size, align) = (mem::size_of_val(t), mem::align_of_val(t));
189199
// SAFETY: see rationale in `new` for why this is using the unsafe variant
@@ -220,6 +230,10 @@ impl Layout {
220230
#[unstable(feature = "layout_for_ptr", issue = "69835")]
221231
#[rustc_const_unstable(feature = "const_alloc_layout", issue = "67521")]
222232
#[must_use]
233+
// TODO: we should try to capture the above constraints on T in a `requires` clause, and the
234+
// metadata helpers from https://github.com/model-checking/verify-rust-std/pull/37 may be able
235+
// to accomplish this.
236+
#[ensures(|result| result.align().is_power_of_two())]
223237
pub const unsafe fn for_value_raw<T: ?Sized>(t: *const T) -> Self {
224238
// SAFETY: we pass along the prerequisites of these functions to the caller
225239
let (size, align) = unsafe { (mem::size_of_val_raw(t), mem::align_of_val_raw(t)) };
@@ -237,6 +251,7 @@ impl Layout {
237251
#[rustc_const_unstable(feature = "alloc_layout_extra", issue = "55724")]
238252
#[must_use]
239253
#[inline]
254+
#[ensures(|result| result.is_aligned())]
240255
pub const fn dangling(&self) -> NonNull<u8> {
241256
// SAFETY: align is guaranteed to be non-zero
242257
unsafe { NonNull::new_unchecked(crate::ptr::without_provenance_mut::<u8>(self.align())) }
@@ -258,6 +273,8 @@ impl Layout {
258273
/// `align` violates the conditions listed in [`Layout::from_size_align`].
259274
#[stable(feature = "alloc_layout_manipulation", since = "1.44.0")]
260275
#[inline]
276+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().align() >= align)]
277+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().align().is_power_of_two())]
261278
pub fn align_to(&self, align: usize) -> Result<Self, LayoutError> {
262279
Layout::from_size_align(self.size(), cmp::max(self.align(), align))
263280
}
@@ -283,6 +300,7 @@ impl Layout {
283300
#[must_use = "this returns the padding needed, \
284301
without modifying the `Layout`"]
285302
#[inline]
303+
#[ensures(|result| *result <= align)]
286304
pub const fn padding_needed_for(&self, align: usize) -> usize {
287305
let len = self.size();
288306

@@ -319,6 +337,10 @@ impl Layout {
319337
#[must_use = "this returns a new `Layout`, \
320338
without modifying the original"]
321339
#[inline]
340+
#[ensures(|result| result.size() >= self.size())]
341+
#[ensures(|result| result.align() == self.align())]
342+
#[ensures(|result| result.size() % result.align() == 0)]
343+
#[ensures(|result| self.size() + self.padding_needed_for(self.align()) == result.size())]
322344
pub const fn pad_to_align(&self) -> Layout {
323345
let pad = self.padding_needed_for(self.align());
324346
// This cannot overflow. Quoting from the invariant of Layout:
@@ -341,6 +363,20 @@ impl Layout {
341363
/// On arithmetic overflow, returns `LayoutError`.
342364
#[unstable(feature = "alloc_layout_extra", issue = "55724")]
343365
#[inline]
366+
// for Kani (v0.54.0), the below modulo operation is too costly to prove (running into the
367+
// 6-hours timeout on GitHub); we use a weaker postcondition instead
368+
#[cfg_attr(not(kani),
369+
ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() % n == 0))]
370+
#[cfg_attr(kani,
371+
ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= self.size()))]
372+
// for Kani (v0.54.0), the below multiplication is too costly to prove (running into the
373+
// 6-hours timeout on GitHub); we use a weaker postcondition instead
374+
#[cfg_attr(not(kani),
375+
ensures(|result| result.is_err() ||
376+
result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1))]
377+
#[cfg_attr(kani,
378+
ensures(|result| result.is_err() || n == 0 ||
379+
result.as_ref().unwrap().0.size() >= result.as_ref().unwrap().1))]
344380
pub fn repeat(&self, n: usize) -> Result<(Self, usize), LayoutError> {
345381
// This cannot overflow. Quoting from the invariant of Layout:
346382
// > `size`, when rounded up to the nearest multiple of `align`,
@@ -401,6 +437,10 @@ impl Layout {
401437
/// ```
402438
#[stable(feature = "alloc_layout_manipulation", since = "1.44.0")]
403439
#[inline]
440+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().0.align() == cmp::max(self.align(), next.align()))]
441+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().0.size() >= self.size() + next.size())]
442+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().1 >= self.size())]
443+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().1 <= result.as_ref().unwrap().0.size())]
404444
pub fn extend(&self, next: Self) -> Result<(Self, usize), LayoutError> {
405445
let new_align = cmp::max(self.align, next.align);
406446
let pad = self.padding_needed_for(next.align());
@@ -427,6 +467,13 @@ impl Layout {
427467
/// On arithmetic overflow, returns `LayoutError`.
428468
#[unstable(feature = "alloc_layout_extra", issue = "55724")]
429469
#[inline]
470+
// for Kani (v0.54.0), the below multiplication is too costly to prove (running into the
471+
// 6-hours timeout on GitHub); we use a weaker postcondition instead
472+
#[cfg_attr(not(kani),
473+
ensures(|result| result.is_err() || result.as_ref().unwrap().size() == n * self.size()))]
474+
#[cfg_attr(kani,
475+
ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().size() >= self.size()))]
476+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == self.align())]
430477
pub fn repeat_packed(&self, n: usize) -> Result<Self, LayoutError> {
431478
let size = self.size().checked_mul(n).ok_or(LayoutError)?;
432479
// The safe constructor is called here to enforce the isize size limit.
@@ -441,6 +488,8 @@ impl Layout {
441488
/// On arithmetic overflow, returns `LayoutError`.
442489
#[unstable(feature = "alloc_layout_extra", issue = "55724")]
443490
#[inline]
491+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == self.size() + next.size())]
492+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == self.align())]
444493
pub fn extend_packed(&self, next: Self) -> Result<Self, LayoutError> {
445494
let new_size = self.size().checked_add(next.size()).ok_or(LayoutError)?;
446495
// The safe constructor is called here to enforce the isize size limit.
@@ -454,6 +503,8 @@ impl Layout {
454503
#[stable(feature = "alloc_layout_manipulation", since = "1.44.0")]
455504
#[rustc_const_unstable(feature = "const_alloc_layout", issue = "67521")]
456505
#[inline]
506+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == n * mem::size_of::<T>())]
507+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == mem::align_of::<T>())]
457508
pub const fn array<T>(n: usize) -> Result<Self, LayoutError> {
458509
// Reduce the amount of code we need to monomorphize per `T`.
459510
return inner(mem::size_of::<T>(), Alignment::of::<T>(), n);
@@ -520,15 +571,153 @@ impl fmt::Display for LayoutError {
520571
mod verify {
521572
use super::*;
522573

574+
impl kani::Arbitrary for Layout {
575+
fn any() -> Self {
576+
let align = kani::any::<Alignment>();
577+
let size = kani::any_where(|s: &usize| *s <= isize::MAX as usize - (align.as_usize() - 1));
578+
unsafe { Layout { size, align } }
579+
}
580+
}
581+
582+
// pub const fn from_size_align(size: usize, align: usize) -> Result<Self, LayoutError>
583+
#[kani::proof_for_contract(Layout::from_size_align)]
584+
pub fn check_from_size_align() {
585+
let s = kani::any::<usize>();
586+
let a = kani::any::<usize>();
587+
let _ = Layout::from_size_align(s, a);
588+
}
589+
590+
// pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self
523591
#[kani::proof_for_contract(Layout::from_size_align_unchecked)]
524592
pub fn check_from_size_align_unchecked() {
525593
let s = kani::any::<usize>();
526594
let a = kani::any::<usize>();
595+
unsafe {
596+
let _ = Layout::from_size_align_unchecked(s, a);
597+
}
598+
}
527599

600+
// pub const fn size(&self) -> usize
601+
#[kani::proof]
602+
pub fn check_size() {
603+
let s = kani::any::<usize>();
604+
let a = kani::any::<usize>();
605+
kani::assume(Layout::from_size_align(s, a).is_ok());
528606
unsafe {
529607
let layout = Layout::from_size_align_unchecked(s, a);
530608
assert_eq!(layout.size(), s);
531-
assert_eq!(layout.align(), a);
609+
}
610+
}
611+
612+
// pub const fn align(&self) -> usize
613+
#[kani::proof]
614+
pub fn check_align() {
615+
let layout = kani::any::<Layout>();
616+
assert!(layout.align().is_power_of_two());
617+
}
618+
619+
// pub const fn new<T>() -> Self
620+
#[kani::proof_for_contract(Layout::new)]
621+
pub fn check_new_i32() {
622+
let _ = Layout::new::<i32>();
623+
}
624+
625+
// pub const fn for_value<T: ?Sized>(t: &T) -> Self
626+
#[kani::proof_for_contract(Layout::for_value)]
627+
pub fn check_for_value_i32() {
628+
let x = kani::any::<i32>();
629+
let _ = Layout::for_value::<i32>(&x);
630+
let array : [i32; 2] = [1, 2];
631+
let _ = Layout::for_value::<[i32]>(&array[1 .. 1]);
632+
let trait_ref: &dyn core::fmt::Debug = &x;
633+
let _ = Layout::for_value::<dyn core::fmt::Debug>(trait_ref);
634+
// TODO: the case of an extern type as unsized tail is not yet covered
635+
}
636+
637+
// pub const unsafe fn for_value_raw<T: ?Sized>(t: *const T) -> Self
638+
#[kani::proof_for_contract(Layout::for_value_raw)]
639+
pub fn check_for_value_raw_i32() {
640+
unsafe {
641+
let x = kani::any::<i32>();
642+
let _ = Layout::for_value_raw::<i32>(&x as *const i32);
643+
let _ = Layout::for_value_raw::<[i32]>(&[] as *const [i32]);
644+
let trait_ref: &dyn core::fmt::Debug = &x;
645+
let _ = Layout::for_value_raw::<dyn core::fmt::Debug>(trait_ref);
646+
// TODO: the case of an extern type as unsized tail is not yet covered
647+
}
648+
}
649+
650+
// pub const fn dangling(&self) -> NonNull<u8>
651+
#[kani::proof_for_contract(Layout::dangling)]
652+
pub fn check_dangling() {
653+
let layout = kani::any::<Layout>();
654+
let _ = layout.dangling();
655+
}
656+
657+
// pub fn align_to(&self, align: usize) -> Result<Self, LayoutError>
658+
#[kani::proof_for_contract(Layout::align_to)]
659+
pub fn check_align_to() {
660+
let layout = kani::any::<Layout>();
661+
let a2 = kani::any::<usize>();
662+
let _ = layout.align_to(a2);
663+
}
664+
665+
// pub const fn padding_needed_for(&self, align: usize) -> usize
666+
#[kani::proof_for_contract(Layout::padding_needed_for)]
667+
pub fn check_padding_needed_for() {
668+
let layout = kani::any::<Layout>();
669+
let a2 = kani::any::<usize>();
670+
if(a2.is_power_of_two() && a2 <= layout.align()) {
671+
let _ = layout.padding_needed_for(a2);
672+
}
673+
}
674+
675+
// pub const fn pad_to_align(&self) -> Layout
676+
#[kani::proof_for_contract(Layout::pad_to_align)]
677+
pub fn check_pad_to_align() {
678+
let layout = kani::any::<Layout>();
679+
let _ = layout.pad_to_align();
680+
}
681+
682+
// pub fn repeat(&self, n: usize) -> Result<(Self, usize), LayoutError>
683+
#[kani::proof_for_contract(Layout::repeat)]
684+
pub fn check_repeat() {
685+
let layout = kani::any::<Layout>();
686+
let n = kani::any::<usize>();
687+
let _ = layout.repeat(n);
688+
}
689+
690+
// pub fn extend(&self, next: Self) -> Result<(Self, usize), LayoutError>
691+
#[kani::proof_for_contract(Layout::extend)]
692+
pub fn check_extend() {
693+
let layout = kani::any::<Layout>();
694+
let layout2 = kani::any::<Layout>();
695+
let _ = layout.extend(layout2);
696+
}
697+
698+
// pub fn repeat_packed(&self, n: usize) -> Result<Self, LayoutError>
699+
#[kani::proof_for_contract(Layout::repeat_packed)]
700+
pub fn check_repeat_packed() {
701+
let layout = kani::any::<Layout>();
702+
let n = kani::any::<usize>();
703+
let _ = layout.repeat_packed(n);
704+
}
705+
706+
// pub fn extend_packed(&self, next: Self) -> Result<Self, LayoutError>
707+
#[kani::proof_for_contract(Layout::extend_packed)]
708+
pub fn check_extend_packed() {
709+
let layout = kani::any::<Layout>();
710+
let layout2 = kani::any::<Layout>();
711+
let _ = layout.extend_packed(layout2);
712+
}
713+
714+
// pub const fn array<T>(n: usize) -> Result<Self, LayoutError>
715+
#[kani::proof_for_contract(Layout::array)]
716+
pub fn check_array_i32() {
717+
let n = kani::any::<usize>();
718+
if let Ok(layout) = Layout::array::<i32>(n) {
719+
assert!(layout.size() >= n * 4);
720+
assert!(layout.align().is_power_of_two());
532721
}
533722
}
534723
}

0 commit comments

Comments
 (0)