@@ -92,6 +92,140 @@ pub(crate) enum MetadataCastError {
92
92
Size ,
93
93
}
94
94
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
+
95
229
impl DstLayout {
96
230
/// The minimum possible alignment of a type.
97
231
const MIN_ALIGN : NonZeroUsize = match NonZeroUsize :: new ( 1 ) {
@@ -202,6 +336,57 @@ impl DstLayout {
202
336
}
203
337
}
204
338
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
+
205
390
/// Like `Layout::extend`, this creates a layout that describes a record
206
391
/// whose layout consists of `self` followed by `next` that includes the
207
392
/// necessary inter-field padding, but not any trailing padding.
@@ -1432,7 +1617,9 @@ mod tests {
1432
1617
1433
1618
#[ cfg( kani) ]
1434
1619
mod proofs {
1435
- use core:: alloc:: Layout ;
1620
+ use core:: { alloc:: Layout , f32:: consts:: E } ;
1621
+
1622
+ use crate :: util:: padding_needed_for;
1436
1623
1437
1624
use super :: * ;
1438
1625
@@ -1452,7 +1639,7 @@ mod proofs {
1452
1639
match size_info {
1453
1640
SizeInfo :: Sized { size } => Layout :: from_size_align ( size, align. get ( ) ) ,
1454
1641
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
1456
1643
// it is at least `offset` bytes.
1457
1644
Layout :: from_size_align ( offset, align. get ( ) )
1458
1645
}
@@ -1493,6 +1680,75 @@ mod proofs {
1493
1680
}
1494
1681
}
1495
1682
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
+
1496
1752
#[ kani:: proof]
1497
1753
fn prove_dst_layout_extend ( ) {
1498
1754
use crate :: util:: { max, min, padding_needed_for} ;
0 commit comments