@@ -92,6 +92,140 @@ pub(crate) enum MetadataCastError {
9292 Size ,
9393}
9494
95+ /// Parameters necessary to perform an infallible reference cast on slice DSTs.
96+ ///
97+ /// # Safety
98+ ///
99+ /// Given `Src: KnownLayout` and `Dst: KnownLayout`, it is only possible to
100+ /// produce `CastParams` via
101+ /// `Src::LAYOUT.try_compute_cast_params(&Dst::LAYOUT)`, and that method will
102+ /// only return `Some` if it is possible to perform an infallible reference cast
103+ /// from `&Src` to `&Dst`.
104+ pub ( crate ) struct CastParams {
105+ // TODO: Also need the invariant that `Src`'s alignment is not smaller than
106+ // `Dst`'s alignment, or else, once unsized locals are supported, a
107+ // conversion could permit `*dst = ...` to write padding past the end of
108+ // `*src`.
109+ /// Given `sl: TrailingSliceLayout` (source layout) and `dl:
110+ /// TrailingSliceLayout` (destination layout), this is computed as:
111+ ///
112+ /// `(sl.offset - dl.offset) / dl.elem_size`
113+ ///
114+ /// INVARIANT: `CastParams` can only be constructed if `sl.offset -
115+ /// dl.offset` is an integer multiple of `dl.elem_size`.
116+ offset_delta_elems : usize ,
117+ /// `sl.elem_size / dl.elem_size`
118+ ///
119+ /// INVARIANT: `CastParams` can only be constructed if `sl.elem_size` is an
120+ /// integer multiple of `dl.elem_size`, and if `dl.elem_size > 0`.
121+ elem_multiple : usize ,
122+ }
123+
124+ impl CastParams {
125+ /// Given the metadata from `src: &Src`, computes the metadata required in
126+ /// order for `dst: &Dst` with the same address to reference the same number
127+ /// of bytes as `src`.
128+ ///
129+ /// # Safety
130+ ///
131+ /// If `Src: KnownLayout` and `Dst: KnownLayout`, and if `self` was computed
132+ /// as `Src::LAYOUT.try_compute_cast_params(&Dst::LAYOUT)`, then the
133+ /// following is guaranteed:
134+ ///
135+ /// Let `src_meta` be the pointer metadata from a `src: &Src`, and compute
136+ /// `let dst_meta = self.compute_cast(src_meta)`. If `dst: &Dst` is
137+ /// constructed using the address of `src` and using `dst_meta` as its
138+ /// pointer metadata, then `dst` will address the same bytes as `src`.
139+ ///
140+ /// TODO: Mention that post-padding may not be preserved.
141+ ///
142+ /// # Panics
143+ ///
144+ /// If the safety preconditions do not hold, then `compute_cast` may panic
145+ /// due to arithmetic overflow. Note that, as `compute_cast` is a safe
146+ /// function, failing to uphold the safety preconditions cannot cause
147+ /// immediate undefined behavior.
148+ pub ( crate ) const fn compute_cast ( self , src_meta : usize ) -> usize {
149+ // PANICS: This function is permitted to panic if its safety
150+ // preconditions are not upheld.
151+ //
152+ // SAFETY/PANICS: If `Src: KnownLayout`, `Dst: KnownLayout`, and `self`
153+ // was computed as `Src::LAYOUT.try_compute_cast_params(&Dst::LAYOUT)`,
154+ // then `self` is a witness to the infallibility of casts from `&Src` to
155+ // `&Dst`, and the internal invariants hold with respect to `Src` and
156+ // `Dst`. Given `sl: Src::LAYOUT` and `dl: Dst::LAYOUT`, these
157+ // invariants guarantee that:
158+ //
159+ // (1) `self.offset_delta_elems = (sl.offset - dl.offset) /
160+ // dl.elem_size`
161+ //
162+ // (2) `self.elem_multiple = sl.elem_size / dl.elem_size` where
163+ // `sl.elem_size` is an integer multiple of `dl.elem_size`
164+ //
165+ // If the safety preconditions are upheld, then the caller has promised
166+ // that `src_meta` is the pointer metadata from some `src: &Src`. By
167+ // invariant on `&Src`, `src` cannot address more than `isize::MAX`
168+ // bytes [1]. Thus:
169+ //
170+ // (3) `sl.offset + (sl.elem_size * src_meta) = src_len <= isize::MAX`
171+ //
172+ // (4) `self.offset_delta_elems * dl.elem_size = sl.offset - dl.offset`
173+ // (rearranging (1))
174+ //
175+ // (5) `sl.offset = (self.offset_delta_elems * dl.elem_size) +
176+ // dl.offset`
177+ //
178+ // (6) `(self.offset_delta_elems * dl.elem_size) + dl.offset +
179+ // (sl.elem_size * src_meta) = src_len <= isize::MAX` (substituting
180+ // (5) into (3))
181+ //
182+ // (7) `sl.elem_size = self.elem_multiple * dl.elem_size` (rearranging
183+ // (2))
184+ //
185+ // (8) `(self.offset_delta_elems * dl.elem_size) + dl.offset +
186+ // (self.elem_multiple * dl.elem_size * src_meta) = src_len <=
187+ // isize::MAX` (substituting (7) into (6))
188+ //
189+ // (9) `(self.offset_delta_elems * dl.elem_size) + (self.elem_multiple
190+ // * dl.elem_size * src_meta) = src_len - dl.offset <= isize::MAX -
191+ // dl.offset`
192+ //
193+ // (10) `self.offset_delta_elems + (self.elem_multiple * src_meta) =
194+ // (src_len - dl.offset) / dl.elem_size <= (isize::MAX - dl.offset)
195+ // / dl.elem_size`
196+ //
197+ // The left-hand side of (10) is the expression we compute and return
198+ // from this method. Since `dl.offset >= 0` and `dl.elem_size > 1`, the
199+ // right-hand side is not greater than `usize::MAX`, and thus this
200+ // computation will not overflow, and thus it will not panic.
201+ //
202+ // We further need to prove that, if the caller takes this resulting
203+ // value as `dst_meta` and uses it to synthesize a `dst &Dst`, this will
204+ // be address the same number of bytes as `src`. The number of bytes is
205+ // given by:
206+ //
207+ // (11) `dst_len = dl.offset + (dl.elem_size * dst_meta)`
208+ //
209+ // (12) `dst_len = dl.offset + (dl.elem_size * (self.offset_delta_elems
210+ // + (self.elem_multiple * src_meta)))` (substituing this method's
211+ // return value)
212+ //
213+ // (13) `dst_len = dl.offset + (dl.elem_size * ((src_len - dl.offset) /
214+ // dl.elem_size))` (substituting (10))
215+ //
216+ // (14) `dst_len = dl.offset + (src_len - dl.offset)`
217+ //
218+ // (15) `dst_len = src_len`
219+ //
220+ // [1] TODO
221+ //
222+ // TODO: Clarify that this algorithm is agnostic to post-padding, and
223+ // justify that this is acceptable.
224+ #[ allow( clippy:: arithmetic_side_effects) ]
225+ return self . offset_delta_elems + ( self . elem_multiple * src_meta) ;
226+ }
227+ }
228+
95229impl DstLayout {
96230 /// The minimum possible alignment of a type.
97231 const MIN_ALIGN : NonZeroUsize = match NonZeroUsize :: new ( 1 ) {
@@ -202,6 +336,57 @@ impl DstLayout {
202336 }
203337 }
204338
339+ pub ( crate ) const fn try_compute_cast_params ( self , dst : & DstLayout ) -> Option < CastParams > {
340+ // TODO: Check alignment in order to guarantee that a `&Src` to `&Dst`
341+ // conversion will never result in a larger referent (including trailing
342+ // padding).
343+ let src = self ;
344+
345+ if src. align . get ( ) < dst. align . get ( ) {
346+ return None ;
347+ }
348+
349+ let ( src, dst) = if let ( SizeInfo :: SliceDst ( src) , SizeInfo :: SliceDst ( dst) ) =
350+ ( src. size_info , dst. size_info )
351+ {
352+ ( src, dst)
353+ } else {
354+ return None ;
355+ } ;
356+
357+ let offset_delta = if let Some ( od) = src. offset . checked_sub ( dst. offset ) {
358+ od
359+ } else {
360+ return None ;
361+ } ;
362+
363+ let delta_mod_other_elem = offset_delta. checked_rem ( dst. elem_size ) ;
364+ let elem_remainder = src. elem_size . checked_rem ( dst. elem_size ) ;
365+
366+ let ( delta_mod_other_elem, elem_remainder) =
367+ if let ( Some ( dmoe) , Some ( em) ) = ( delta_mod_other_elem, elem_remainder) {
368+ ( dmoe, em)
369+ } else {
370+ return None ;
371+ } ;
372+
373+ if delta_mod_other_elem != 0 || src. elem_size < dst. elem_size || elem_remainder != 0 {
374+ return None ;
375+ }
376+
377+ // PANICS: The preceding `src.elem_size.checked_rem(dst.elem_size)`
378+ // could only return `Some` if `dst.elem_size > 0`, so this division
379+ // will not divide by zero.
380+ #[ allow( clippy:: arithmetic_side_effects) ]
381+ let offset_delta_elems = offset_delta / dst. elem_size ;
382+ // PANICS: See previous panics comment.
383+ #[ allow( clippy:: arithmetic_side_effects) ]
384+ let elem_multiple = src. elem_size / dst. elem_size ;
385+
386+ // INVARIANTS: TODO
387+ Some ( CastParams { offset_delta_elems, elem_multiple } )
388+ }
389+
205390 /// Like `Layout::extend`, this creates a layout that describes a record
206391 /// whose layout consists of `self` followed by `next` that includes the
207392 /// necessary inter-field padding, but not any trailing padding.
@@ -1432,7 +1617,9 @@ mod tests {
14321617
14331618#[ cfg( kani) ]
14341619mod proofs {
1435- use core:: alloc:: Layout ;
1620+ use core:: { alloc:: Layout , f32:: consts:: E } ;
1621+
1622+ use crate :: util:: padding_needed_for;
14361623
14371624 use super :: * ;
14381625
@@ -1452,7 +1639,7 @@ mod proofs {
14521639 match size_info {
14531640 SizeInfo :: Sized { size } => Layout :: from_size_align ( size, align. get ( ) ) ,
14541641 SizeInfo :: SliceDst ( TrailingSliceLayout { offset, elem_size : _ } ) => {
1455- // `SliceDst`` cannot encode an exact size, but we know
1642+ // `SliceDst` cannot encode an exact size, but we know
14561643 // it is at least `offset` bytes.
14571644 Layout :: from_size_align ( offset, align. get ( ) )
14581645 }
@@ -1493,6 +1680,75 @@ mod proofs {
14931680 }
14941681 }
14951682
1683+ #[ kani:: proof]
1684+ fn prove_try_compute_cast_params ( ) {
1685+ let src: DstLayout = kani:: any ( ) ;
1686+ let dst: DstLayout = kani:: any ( ) ;
1687+
1688+ let Some ( params) = src. try_compute_cast_params ( & dst) else {
1689+ // TODO: Is there a better way to say "assume that this branch is
1690+ // unreachable"?
1691+ kani:: assume ( false ) ;
1692+ return ;
1693+ } ;
1694+
1695+ let SizeInfo :: SliceDst ( src_size_info) = src. size_info else {
1696+ kani:: assume ( false ) ;
1697+ return ;
1698+ } ;
1699+
1700+ let SizeInfo :: SliceDst ( dst_size_info) = dst. size_info else {
1701+ kani:: assume ( false ) ;
1702+ return ;
1703+ } ;
1704+
1705+ // Returns `Some(size)` only if `meta` is valid metadata for the given
1706+ // type layout - it describes an object which would fit in a valid Rust
1707+ // allocation.
1708+ fn size_for_meta (
1709+ size_info : TrailingSliceLayout ,
1710+ align : NonZeroUsize ,
1711+ meta : usize ,
1712+ ) -> Option < usize > {
1713+ let Some ( slice_bytes) = size_info. elem_size . checked_mul ( meta) else {
1714+ kani:: assume ( false ) ;
1715+ return None ;
1716+ } ;
1717+
1718+ let Some ( size_no_trailing_padding) = size_info. offset . checked_add ( slice_bytes) else {
1719+ kani:: assume ( false ) ;
1720+ return None ;
1721+ } ;
1722+
1723+ let padding = padding_needed_for ( size_no_trailing_padding, align) ;
1724+
1725+ let Some ( src_size) = size_no_trailing_padding. checked_add ( padding) else {
1726+ kani:: assume ( false ) ;
1727+ return None ;
1728+ } ;
1729+
1730+ if src_size > isize:: MAX as usize {
1731+ kani:: assume ( false ) ;
1732+ return None ;
1733+ }
1734+
1735+ Some ( src_size)
1736+ }
1737+
1738+ let src_meta: usize = kani:: any ( ) ;
1739+
1740+ let Some ( src_size) = size_for_meta ( src_size_info, src. align , src_meta) else {
1741+ kani:: assume ( false ) ;
1742+ return ;
1743+ } ;
1744+
1745+ let dst_meta = params. compute_cast ( src_meta) ;
1746+
1747+ let dst_size = size_for_meta ( dst_size_info, dst. align , dst_meta) . unwrap ( ) ;
1748+
1749+ assert ! ( dst_size <= src_size) ;
1750+ }
1751+
14961752 #[ kani:: proof]
14971753 fn prove_dst_layout_extend ( ) {
14981754 use crate :: util:: { max, min, padding_needed_for} ;
0 commit comments