diff --git a/src/layout.rs b/src/layout.rs index 9e4611c4c9..97f94587e9 100644 --- a/src/layout.rs +++ b/src/layout.rs @@ -1429,3 +1429,244 @@ mod tests { validate_against_rust!(4, 16, 4); } } + +#[cfg(kani)] +mod proofs { + use core::alloc::Layout; + + use super::*; + + impl kani::Arbitrary for DstLayout { + fn any() -> Self { + let align: NonZeroUsize = kani::any(); + let size_info: SizeInfo = kani::any(); + + kani::assume(align.is_power_of_two()); + kani::assume(align < DstLayout::THEORETICAL_MAX_ALIGN); + + // For testing purposes, we most care about instantiations of + // `DstLayout` that can correspond to actual Rust types. We use + // `Layout` to verify that our `DstLayout` satisfies the validity + // conditions of Rust layouts. + kani::assume( + match size_info { + SizeInfo::Sized { size } => Layout::from_size_align(size, align.get()), + SizeInfo::SliceDst(TrailingSliceLayout { offset, elem_size: _ }) => { + // `SliceDst`` cannot encode an exact size, but we know + // it is at least `offset` bytes. + Layout::from_size_align(offset, align.get()) + } + } + .is_ok(), + ); + + Self { align: align, size_info: size_info } + } + } + + impl kani::Arbitrary for SizeInfo { + fn any() -> Self { + let is_sized: bool = kani::any(); + + match is_sized { + true => { + let size: usize = kani::any(); + + kani::assume(size <= isize::MAX as _); + + SizeInfo::Sized { size } + } + false => SizeInfo::SliceDst(kani::any()), + } + } + } + + impl kani::Arbitrary for TrailingSliceLayout { + fn any() -> Self { + let elem_size: usize = kani::any(); + let offset: usize = kani::any(); + + kani::assume(elem_size < isize::MAX as _); + kani::assume(offset < isize::MAX as _); + + TrailingSliceLayout { elem_size, offset } + } + } + + #[kani::proof] + fn prove_dst_layout_extend() { + use crate::util::{max, min, padding_needed_for}; + + let base: DstLayout = kani::any(); + let field: DstLayout = kani::any(); + let packed: Option = kani::any(); + + if let Some(max_align) = packed { + kani::assume(max_align.is_power_of_two()); + kani::assume(base.align <= max_align); + } + + // The base can only be extended if it's sized. + kani::assume(matches!(base.size_info, SizeInfo::Sized { .. })); + let base_size = if let SizeInfo::Sized { size } = base.size_info { + size + } else { + unreachable!(); + }; + + // Under the above conditions, `DstLayout::extend` will not panic. + let composite = base.extend(field, packed); + + // The field's alignment is clamped by `max_align` (i.e., the + // `packed` attribute, if any) [1]. + // + // [1] Per https://doc.rust-lang.org/reference/type-layout.html#the-alignment-modifiers: + // + // The alignments of each field, for the purpose of positioning + // fields, is the smaller of the specified alignment and the + // alignment of the field's type. + let field_align = min(field.align, packed.unwrap_or(DstLayout::THEORETICAL_MAX_ALIGN)); + + // The struct's alignment is the maximum of its previous alignment and + // `field_align`. + assert_eq!(composite.align, max(base.align, field_align)); + + // Compute the minimum amount of inter-field padding needed to + // satisfy the field's alignment, and offset of the trailing field. + // [1] + // + // [1] Per https://doc.rust-lang.org/reference/type-layout.html#the-alignment-modifiers: + // + // Inter-field padding is guaranteed to be the minimum required in + // order to satisfy each field's (possibly altered) alignment. + let padding = padding_needed_for(base_size, field_align); + let offset = base_size + padding; + + // For testing purposes, we'll also construct `alloc::Layout` + // stand-ins for `DstLayout`, and show that `extend` behaves + // comparably on both types. + let base_analog = Layout::from_size_align(base_size, base.align.get()).unwrap(); + + match field.size_info { + SizeInfo::Sized { size: field_size } => { + if let SizeInfo::Sized { size: composite_size } = composite.size_info { + // If the trailing field is sized, the resulting layout will + // be sized. Its size will be the sum of the preceding + // layout, the size of the new field, and the size of + // inter-field padding between the two. + assert_eq!(composite_size, offset + field_size); + + let field_analog = + Layout::from_size_align(field_size, field_align.get()).unwrap(); + + if let Ok((actual_composite, actual_offset)) = base_analog.extend(field_analog) + { + assert_eq!(actual_offset, offset); + assert_eq!(actual_composite.size(), composite_size); + assert_eq!(actual_composite.align(), composite.align.get()); + } else { + // An error here reflects that composite of `base` + // and `field` cannot correspond to a real Rust type + // fragment, because such a fragment would violate + // the basic invariants of a valid Rust layout. At + // the time of writing, `DstLayout` is a little more + // permissive than `Layout`, so we don't assert + // anything in this branch (e.g., unreachability). + } + } else { + panic!("The composite of two sized layouts must be sized.") + } + } + SizeInfo::SliceDst(TrailingSliceLayout { + offset: field_offset, + elem_size: field_elem_size, + }) => { + if let SizeInfo::SliceDst(TrailingSliceLayout { + offset: composite_offset, + elem_size: composite_elem_size, + }) = composite.size_info + { + // The offset of the trailing slice component is the sum + // of the offset of the trailing field and the trailing + // slice offset within that field. + assert_eq!(composite_offset, offset + field_offset); + // The elem size is unchanged. + assert_eq!(composite_elem_size, field_elem_size); + + let field_analog = + Layout::from_size_align(field_offset, field_align.get()).unwrap(); + + if let Ok((actual_composite, actual_offset)) = base_analog.extend(field_analog) + { + assert_eq!(actual_offset, offset); + assert_eq!(actual_composite.size(), composite_offset); + assert_eq!(actual_composite.align(), composite.align.get()); + } else { + // An error here reflects that composite of `base` + // and `field` cannot correspond to a real Rust type + // fragment, because such a fragment would violate + // the basic invariants of a valid Rust layout. At + // the time of writing, `DstLayout` is a little more + // permissive than `Layout`, so we don't assert + // anything in this branch (e.g., unreachability). + } + } else { + panic!("The extension of a layout with a DST must result in a DST.") + } + } + } + } + + #[kani::proof] + #[kani::should_panic] + fn prove_dst_layout_extend_dst_panics() { + let base: DstLayout = kani::any(); + let field: DstLayout = kani::any(); + let packed: Option = kani::any(); + + if let Some(max_align) = packed { + kani::assume(max_align.is_power_of_two()); + kani::assume(base.align <= max_align); + } + + kani::assume(matches!(base.size_info, SizeInfo::SliceDst(..))); + + let _ = base.extend(field, packed); + } + + #[kani::proof] + fn prove_dst_layout_pad_to_align() { + use crate::util::padding_needed_for; + + let layout: DstLayout = kani::any(); + + let padded: DstLayout = layout.pad_to_align(); + + // Calling `pad_to_align` does not alter the `DstLayout`'s alignment. + assert_eq!(padded.align, layout.align); + + if let SizeInfo::Sized { size: unpadded_size } = layout.size_info { + if let SizeInfo::Sized { size: padded_size } = padded.size_info { + // If the layout is sized, it will remain sized after padding is + // added. Its sum will be its unpadded size and the size of the + // trailing padding needed to satisfy its alignment + // requirements. + let padding = padding_needed_for(unpadded_size, layout.align); + assert_eq!(padded_size, unpadded_size + padding); + + // Prove that calling `DstLayout::pad_to_align` behaves + // identically to `Layout::pad_to_align`. + let layout_analog = + Layout::from_size_align(unpadded_size, layout.align.get()).unwrap(); + let padded_analog = layout_analog.pad_to_align(); + assert_eq!(padded_analog.align(), layout.align.get()); + assert_eq!(padded_analog.size(), padded_size); + } else { + panic!("The padding of a sized layout must result in a sized layout.") + } + } else { + // If the layout is a DST, padding cannot be statically added. + assert_eq!(padded.size_info, layout.size_info); + } + } +} diff --git a/src/lib.rs b/src/lib.rs index 7458b72038..709d09c37d 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -6640,242 +6640,3 @@ mod tests { } } } - -#[cfg(kani)] -mod proofs { - use super::*; - - impl kani::Arbitrary for DstLayout { - fn any() -> Self { - let align: NonZeroUsize = kani::any(); - let size_info: SizeInfo = kani::any(); - - kani::assume(align.is_power_of_two()); - kani::assume(align < DstLayout::THEORETICAL_MAX_ALIGN); - - // For testing purposes, we most care about instantiations of - // `DstLayout` that can correspond to actual Rust types. We use - // `Layout` to verify that our `DstLayout` satisfies the validity - // conditions of Rust layouts. - kani::assume( - match size_info { - SizeInfo::Sized { size } => Layout::from_size_align(size, align.get()), - SizeInfo::SliceDst(TrailingSliceLayout { offset, elem_size: _ }) => { - // `SliceDst`` cannot encode an exact size, but we know - // it is at least `offset` bytes. - Layout::from_size_align(offset, align.get()) - } - } - .is_ok(), - ); - - Self { align: align, size_info: size_info } - } - } - - impl kani::Arbitrary for SizeInfo { - fn any() -> Self { - let is_sized: bool = kani::any(); - - match is_sized { - true => { - let size: usize = kani::any(); - - kani::assume(size <= isize::MAX as _); - - SizeInfo::Sized { size } - } - false => SizeInfo::SliceDst(kani::any()), - } - } - } - - impl kani::Arbitrary for TrailingSliceLayout { - fn any() -> Self { - let elem_size: usize = kani::any(); - let offset: usize = kani::any(); - - kani::assume(elem_size < isize::MAX as _); - kani::assume(offset < isize::MAX as _); - - TrailingSliceLayout { elem_size, offset } - } - } - - #[kani::proof] - fn prove_dst_layout_extend() { - use crate::util::{max, min, padding_needed_for}; - - let base: DstLayout = kani::any(); - let field: DstLayout = kani::any(); - let packed: Option = kani::any(); - - if let Some(max_align) = packed { - kani::assume(max_align.is_power_of_two()); - kani::assume(base.align <= max_align); - } - - // The base can only be extended if it's sized. - kani::assume(matches!(base.size_info, SizeInfo::Sized { .. })); - let base_size = if let SizeInfo::Sized { size } = base.size_info { - size - } else { - unreachable!(); - }; - - // Under the above conditions, `DstLayout::extend` will not panic. - let composite = base.extend(field, packed); - - // The field's alignment is clamped by `max_align` (i.e., the - // `packed` attribute, if any) [1]. - // - // [1] Per https://doc.rust-lang.org/reference/type-layout.html#the-alignment-modifiers: - // - // The alignments of each field, for the purpose of positioning - // fields, is the smaller of the specified alignment and the - // alignment of the field's type. - let field_align = min(field.align, packed.unwrap_or(DstLayout::THEORETICAL_MAX_ALIGN)); - - // The struct's alignment is the maximum of its previous alignment and - // `field_align`. - assert_eq!(composite.align, max(base.align, field_align)); - - // Compute the minimum amount of inter-field padding needed to - // satisfy the field's alignment, and offset of the trailing field. - // [1] - // - // [1] Per https://doc.rust-lang.org/reference/type-layout.html#the-alignment-modifiers: - // - // Inter-field padding is guaranteed to be the minimum required in - // order to satisfy each field's (possibly altered) alignment. - let padding = padding_needed_for(base_size, field_align); - let offset = base_size + padding; - - // For testing purposes, we'll also construct `alloc::Layout` - // stand-ins for `DstLayout`, and show that `extend` behaves - // comparably on both types. - let base_analog = Layout::from_size_align(base_size, base.align.get()).unwrap(); - - match field.size_info { - SizeInfo::Sized { size: field_size } => { - if let SizeInfo::Sized { size: composite_size } = composite.size_info { - // If the trailing field is sized, the resulting layout will - // be sized. Its size will be the sum of the preceding - // layout, the size of the new field, and the size of - // inter-field padding between the two. - assert_eq!(composite_size, offset + field_size); - - let field_analog = - Layout::from_size_align(field_size, field_align.get()).unwrap(); - - if let Ok((actual_composite, actual_offset)) = base_analog.extend(field_analog) - { - assert_eq!(actual_offset, offset); - assert_eq!(actual_composite.size(), composite_size); - assert_eq!(actual_composite.align(), composite.align.get()); - } else { - // An error here reflects that composite of `base` - // and `field` cannot correspond to a real Rust type - // fragment, because such a fragment would violate - // the basic invariants of a valid Rust layout. At - // the time of writing, `DstLayout` is a little more - // permissive than `Layout`, so we don't assert - // anything in this branch (e.g., unreachability). - } - } else { - panic!("The composite of two sized layouts must be sized.") - } - } - SizeInfo::SliceDst(TrailingSliceLayout { - offset: field_offset, - elem_size: field_elem_size, - }) => { - if let SizeInfo::SliceDst(TrailingSliceLayout { - offset: composite_offset, - elem_size: composite_elem_size, - }) = composite.size_info - { - // The offset of the trailing slice component is the sum - // of the offset of the trailing field and the trailing - // slice offset within that field. - assert_eq!(composite_offset, offset + field_offset); - // The elem size is unchanged. - assert_eq!(composite_elem_size, field_elem_size); - - let field_analog = - Layout::from_size_align(field_offset, field_align.get()).unwrap(); - - if let Ok((actual_composite, actual_offset)) = base_analog.extend(field_analog) - { - assert_eq!(actual_offset, offset); - assert_eq!(actual_composite.size(), composite_offset); - assert_eq!(actual_composite.align(), composite.align.get()); - } else { - // An error here reflects that composite of `base` - // and `field` cannot correspond to a real Rust type - // fragment, because such a fragment would violate - // the basic invariants of a valid Rust layout. At - // the time of writing, `DstLayout` is a little more - // permissive than `Layout`, so we don't assert - // anything in this branch (e.g., unreachability). - } - } else { - panic!("The extension of a layout with a DST must result in a DST.") - } - } - } - } - - #[kani::proof] - #[kani::should_panic] - fn prove_dst_layout_extend_dst_panics() { - let base: DstLayout = kani::any(); - let field: DstLayout = kani::any(); - let packed: Option = kani::any(); - - if let Some(max_align) = packed { - kani::assume(max_align.is_power_of_two()); - kani::assume(base.align <= max_align); - } - - kani::assume(matches!(base.size_info, SizeInfo::SliceDst(..))); - - let _ = base.extend(field, packed); - } - - #[kani::proof] - fn prove_dst_layout_pad_to_align() { - use crate::util::padding_needed_for; - - let layout: DstLayout = kani::any(); - - let padded: DstLayout = layout.pad_to_align(); - - // Calling `pad_to_align` does not alter the `DstLayout`'s alignment. - assert_eq!(padded.align, layout.align); - - if let SizeInfo::Sized { size: unpadded_size } = layout.size_info { - if let SizeInfo::Sized { size: padded_size } = padded.size_info { - // If the layout is sized, it will remain sized after padding is - // added. Its sum will be its unpadded size and the size of the - // trailing padding needed to satisfy its alignment - // requirements. - let padding = padding_needed_for(unpadded_size, layout.align); - assert_eq!(padded_size, unpadded_size + padding); - - // Prove that calling `DstLayout::pad_to_align` behaves - // identically to `Layout::pad_to_align`. - let layout_analog = - Layout::from_size_align(unpadded_size, layout.align.get()).unwrap(); - let padded_analog = layout_analog.pad_to_align(); - assert_eq!(padded_analog.align(), layout.align.get()); - assert_eq!(padded_analog.size(), padded_size); - } else { - panic!("The padding of a sized layout must result in a sized layout.") - } - } else { - // If the layout is a DST, padding cannot be statically added. - assert_eq!(padded.size_info, layout.size_info); - } - } -}