Skip to content

Commit 8c21272

Browse files
tautschnigtautschnig
committed
Add more ensures clauses
1 parent ac03385 commit 8c21272

File tree

1 file changed

+34
-56
lines changed

1 file changed

+34
-56
lines changed

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

Lines changed: 34 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,9 @@ impl Layout {
7272
#[inline]
7373
#[rustc_allow_const_fn_unstable(ptr_alignment_type)]
7474
#[ensures(|result| result.is_err() || align.is_power_of_two())]
75+
#[ensures(|result| result.is_err() || size <= isize::MAX as usize - (align - 1))]
76+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == size)]
77+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == align)]
7578
pub const fn from_size_align(size: usize, align: usize) -> Result<Self, LayoutError> {
7679
if !align.is_power_of_two() {
7780
return Err(LayoutError);
@@ -123,6 +126,8 @@ impl Layout {
123126
#[inline]
124127
#[rustc_allow_const_fn_unstable(ptr_alignment_type)]
125128
#[requires(Layout::from_size_align(size, align).is_ok())]
129+
#[ensures(|result| result.size() == size)]
130+
#[ensures(|result| result.align() == align)]
126131
pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self {
127132
// SAFETY: the caller is required to uphold the preconditions.
128133
unsafe { Layout { size, align: Alignment::new_unchecked(align) } }
@@ -247,6 +252,7 @@ impl Layout {
247252
#[stable(feature = "alloc_layout_manipulation", since = "1.44.0")]
248253
#[inline]
249254
#[ensures(|result| result.is_err() || result.as_ref().unwrap().align() >= align)]
255+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().align().is_power_of_two())]
250256
pub fn align_to(&self, align: usize) -> Result<Self, LayoutError> {
251257
Layout::from_size_align(self.size(), cmp::max(self.align(), align))
252258
}
@@ -309,7 +315,10 @@ impl Layout {
309315
#[must_use = "this returns a new `Layout`, \
310316
without modifying the original"]
311317
#[inline]
318+
#[ensures(|result| result.size() >= self.size())]
319+
#[ensures(|result| result.align() == self.align())]
312320
#[ensures(|result| result.size() % result.align() == 0)]
321+
#[ensures(|result| self.size() + self.padding_needed_for(self.align()) == result.size())]
313322
pub const fn pad_to_align(&self) -> Layout {
314323
let pad = self.padding_needed_for(self.align());
315324
// This cannot overflow. Quoting from the invariant of Layout:
@@ -332,7 +341,9 @@ impl Layout {
332341
/// On arithmetic overflow, returns `LayoutError`.
333342
#[unstable(feature = "alloc_layout_extra", issue = "55724")]
334343
#[inline]
335-
#[ensures(|result| result.is_err() || result.as_ref().unwrap().1 % n == 0)]
344+
#[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().1 % n == 0)]
345+
#[ensures(|result| result.is_err() || n == 0 || result.as_ref().unwrap().0.size() >= self.size())]
346+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().0.size() == n * result.as_ref().unwrap().1)]
336347
pub fn repeat(&self, n: usize) -> Result<(Self, usize), LayoutError> {
337348
// This cannot overflow. Quoting from the invariant of Layout:
338349
// > `size`, when rounded up to the nearest multiple of `align`,
@@ -393,6 +404,9 @@ impl Layout {
393404
/// ```
394405
#[stable(feature = "alloc_layout_manipulation", since = "1.44.0")]
395406
#[inline]
407+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().0.align() == cmp::max(self.align(), next.align()))]
408+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().0.size() >= self.size() + next.size())]
409+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().1 >= self.size())]
396410
#[ensures(|result| result.is_err() || result.as_ref().unwrap().1 <= result.as_ref().unwrap().0.size())]
397411
pub fn extend(&self, next: Self) -> Result<(Self, usize), LayoutError> {
398412
let new_align = cmp::max(self.align, next.align);
@@ -420,7 +434,8 @@ impl Layout {
420434
/// On arithmetic overflow, returns `LayoutError`.
421435
#[unstable(feature = "alloc_layout_extra", issue = "55724")]
422436
#[inline]
423-
#[ensures(|result| result.is_err() || result.as_ref().unwrap().size() % n == 0)]
437+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == n * self.size())]
438+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == self.align())]
424439
pub fn repeat_packed(&self, n: usize) -> Result<Self, LayoutError> {
425440
let size = self.size().checked_mul(n).ok_or(LayoutError)?;
426441
// The safe constructor is called here to enforce the isize size limit.
@@ -435,7 +450,11 @@ impl Layout {
435450
/// On arithmetic overflow, returns `LayoutError`.
436451
#[unstable(feature = "alloc_layout_extra", issue = "55724")]
437452
#[inline]
453+
// the below is wrong but was written in a previous commit; keeping it for now to confirm that
454+
// this is caught
438455
#[ensures(|result| result.is_err() || result.as_ref().unwrap().size() <= next.size())]
456+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().size() == self.size() + next.size())]
457+
#[ensures(|result| result.is_err() || result.as_ref().unwrap().align() == self.align())]
439458
pub fn extend_packed(&self, next: Self) -> Result<Self, LayoutError> {
440459
let new_size = self.size().checked_add(next.size()).ok_or(LayoutError)?;
441460
// The safe constructor is called here to enforce the isize size limit.
@@ -520,26 +539,16 @@ mod verify {
520539
pub fn check_from_size_align() {
521540
let s = kani::any::<usize>();
522541
let a = kani::any::<usize>();
523-
524-
if let Ok(layout) = Layout::from_size_align(s, a) {
525-
assert_eq!(layout.size(), s);
526-
assert_eq!(layout.align(), a);
527-
assert!(a > 0);
528-
assert!(a.is_power_of_two());
529-
assert!(s <= isize::MAX as usize - (a - 1));
530-
}
542+
let _ = Layout::from_size_align(s, a);
531543
}
532544

533545
// pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self
534546
#[kani::proof_for_contract(Layout::from_size_align_unchecked)]
535547
pub fn check_from_size_align_unchecked() {
536548
let s = kani::any::<usize>();
537549
let a = kani::any::<usize>();
538-
539550
unsafe {
540-
let layout = Layout::from_size_align_unchecked(s, a);
541-
assert_eq!(layout.size(), s);
542-
assert_eq!(layout.align(), a);
551+
let _ = Layout::from_size_align_unchecked(s, a);
543552
}
544553
}
545554

@@ -548,7 +557,6 @@ mod verify {
548557
pub fn check_size() {
549558
let s = kani::any::<usize>();
550559
let a = kani::any::<usize>();
551-
552560
unsafe {
553561
let layout = Layout::from_size_align_unchecked(s, a);
554562
assert_eq!(layout.size(), s);
@@ -560,10 +568,9 @@ mod verify {
560568
pub fn check_align() {
561569
let s = kani::any::<usize>();
562570
let a = kani::any::<usize>();
563-
564571
unsafe {
565572
let layout = Layout::from_size_align_unchecked(s, a);
566-
assert!(layout.align().is_power_of_two());
573+
let _ = layout.align();
567574
}
568575
}
569576

@@ -579,16 +586,14 @@ mod verify {
579586
#[kani::proof_for_contract(Layout::for_value)]
580587
pub fn check_for_value_i32() {
581588
let array : [i32; 2] = [1, 2];
582-
let layout = Layout::for_value::<[i32]>(&array[1 .. 1]);
583-
assert!(layout.align().is_power_of_two());
589+
let _ = Layout::for_value::<[i32]>(&array[1 .. 1]);
584590
}
585591

586592
// pub const unsafe fn for_value_raw<T: ?Sized>(t: *const T) -> Self
587593
#[kani::proof_for_contract(Layout::for_value_raw)]
588594
pub fn check_for_value_raw_i32() {
589595
unsafe {
590-
let layout = Layout::for_value_raw::<[i32]>(&[] as *const [i32]);
591-
assert!(layout.align().is_power_of_two());
596+
let _ = Layout::for_value_raw::<[i32]>(&[] as *const [i32]);
592597
}
593598
}
594599

@@ -597,10 +602,9 @@ mod verify {
597602
pub fn check_dangling() {
598603
let s = kani::any::<usize>();
599604
let a = kani::any::<usize>();
600-
601605
unsafe {
602606
let layout = Layout::from_size_align_unchecked(s, a);
603-
assert!(layout.dangling().is_aligned());
607+
let _ = layout.dangling();
604608
}
605609
}
606610

@@ -609,14 +613,10 @@ mod verify {
609613
pub fn check_align_to() {
610614
let s = kani::any::<usize>();
611615
let a = kani::any::<usize>();
612-
613616
unsafe {
614617
let layout = Layout::from_size_align_unchecked(s, a);
615618
let a2 = kani::any::<usize>();
616-
if let Ok(layout2) = layout.align_to(a2) {
617-
assert!(layout2.align() > 0);
618-
assert!(layout2.align().is_power_of_two());
619-
}
619+
let _ = layout.align_to(a2);
620620
}
621621
}
622622

@@ -625,13 +625,11 @@ mod verify {
625625
pub fn check_padding_needed_for() {
626626
let s = kani::any::<usize>();
627627
let a = kani::any::<usize>();
628-
629628
unsafe {
630629
let layout = Layout::from_size_align_unchecked(s, a);
631630
let a2 = kani::any::<usize>();
632631
if(a2.is_power_of_two() && a2 <= a) {
633-
let p = layout.padding_needed_for(a2);
634-
assert!(p <= a2);
632+
let _ = layout.padding_needed_for(a2);
635633
}
636634
}
637635
}
@@ -641,12 +639,9 @@ mod verify {
641639
pub fn check_pad_to_align() {
642640
let s = kani::any::<usize>();
643641
let a = kani::any::<usize>();
644-
645642
unsafe {
646643
let layout = Layout::from_size_align_unchecked(s, a);
647-
let layout2 = layout.pad_to_align();
648-
assert_eq!(layout2.size() % a, 0);
649-
assert_eq!(layout.size() + layout.padding_needed_for(layout.align()), layout2.size());
644+
let _ = layout.pad_to_align();
650645
}
651646
}
652647

@@ -655,14 +650,10 @@ mod verify {
655650
pub fn check_repeat() {
656651
let s = kani::any::<usize>();
657652
let a = kani::any::<usize>();
658-
659653
unsafe {
660654
let layout = Layout::from_size_align_unchecked(s, a);
661655
let n = kani::any::<usize>();
662-
if let Ok((layout2, padded_size)) = layout.repeat(n) {
663-
assert!(n == 0 || layout2.size() >= s);
664-
assert_eq!(layout2.size(), n * padded_size);
665-
}
656+
let _ = layout.repeat(n);
666657
}
667658
}
668659

@@ -671,18 +662,12 @@ mod verify {
671662
pub fn check_extend() {
672663
let s = kani::any::<usize>();
673664
let a = kani::any::<usize>();
674-
675665
unsafe {
676666
let layout = Layout::from_size_align_unchecked(s, a);
677667
let s2 = kani::any::<usize>();
678668
let a2 = kani::any::<usize>();
679669
let layout2 = Layout::from_size_align_unchecked(s2, a2);
680-
if let Ok((layout3, offset)) = layout.extend(layout2) {
681-
assert_eq!(layout3.align(), cmp::max(a, a2));
682-
assert!(layout3.size() >= s + s2);
683-
assert!(offset >= s);
684-
assert!(offset <= layout3.size());
685-
}
670+
let _ = layout.extend(layout2);
686671
}
687672
}
688673

@@ -691,13 +676,10 @@ mod verify {
691676
pub fn check_repeat_packed() {
692677
let s = kani::any::<usize>();
693678
let a = kani::any::<usize>();
694-
695679
unsafe {
696680
let layout = Layout::from_size_align_unchecked(s, a);
697681
let n = kani::any::<usize>();
698-
if let Ok(layout2) = layout.repeat_packed(n) {
699-
assert!(n == 0 || layout2.size() >= s);
700-
}
682+
let _ = layout.repeat_packed(n);
701683
}
702684
}
703685

@@ -706,16 +688,12 @@ mod verify {
706688
pub fn check_extend_packed() {
707689
let s = kani::any::<usize>();
708690
let a = kani::any::<usize>();
709-
710691
unsafe {
711692
let layout = Layout::from_size_align_unchecked(s, a);
712693
let s2 = kani::any::<usize>();
713694
let a2 = kani::any::<usize>();
714695
let layout2 = Layout::from_size_align_unchecked(s2, a2);
715-
if let Ok(layout3) = layout.extend_packed(layout2) {
716-
assert_eq!(layout3.align(), a);
717-
assert_eq!(layout3.size(), s + s2);
718-
}
696+
let _ = layout.extend_packed(layout2);
719697
}
720698
}
721699

0 commit comments

Comments
 (0)