@@ -77,6 +77,29 @@ impl SizeInfo {
7777 }
7878}
7979
80+ #[ cfg( kani) ]
81+ impl TrailingSliceLayout < usize > {
82+ fn is_valid_metadata ( self , align : NonZeroUsize , meta : usize ) -> bool {
83+ let Some ( trailing_slice_size) = self . elem_size . checked_mul ( meta) else {
84+ return false ;
85+ } ;
86+
87+ let Some ( unpadded_size) = self . offset . checked_add ( trailing_slice_size) else {
88+ return false ;
89+ } ;
90+
91+ if unpadded_size >= isize:: MAX as usize {
92+ return false ;
93+ }
94+
95+ let trailing_padding = util:: padding_needed_for ( unpadded_size, align) ;
96+
97+ let Some ( size) = unpadded_size. checked_add ( trailing_padding) else { return false } ;
98+
99+ size <= isize:: MAX as usize
100+ }
101+ }
102+
80103#[ doc( hidden) ]
81104#[ derive( Copy , Clone ) ]
82105#[ cfg_attr( test, derive( Debug ) ) ]
@@ -612,6 +635,34 @@ pub(crate) use cast_from_raw::cast_from_raw;
612635mod cast_from_raw {
613636 use crate :: { pointer:: PtrInner , * } ;
614637
638+ #[ cfg_attr( kani, kani:: ensures( |& gcd|
639+ offset_delta % gcd == 0
640+ && src_elem_size % gcd == 0
641+ && dst_elem_size. get( ) % gcd == 0
642+ ) ) ]
643+ #[ cfg_attr( kani, kani:: recursion) ]
644+ const fn gcd (
645+ offset_delta : usize ,
646+ src_elem_size : usize ,
647+ dst_elem_size : NonZeroUsize ,
648+ ) -> NonZeroUsize {
649+ const fn gcd ( a : usize , b : usize ) -> usize {
650+ if a == 0 {
651+ b
652+ } else {
653+ #[ allow( clippy:: arithmetic_side_effects) ]
654+ gcd ( b % a, a)
655+ }
656+ }
657+
658+ let gcd = gcd ( gcd ( offset_delta, src_elem_size) , dst_elem_size. get ( ) ) ;
659+
660+ match NonZeroUsize :: new ( gcd) {
661+ Some ( gcd) => gcd,
662+ None => const_panic ! ( "gcd should be non-zero, because dst_elem_size is non-zero" ) ,
663+ }
664+ }
665+
615666 /// Implements [`<Dst as SizeFrom<Src>>::cast_from_raw`][cast_from_raw].
616667 ///
617668 /// # PME
@@ -623,11 +674,15 @@ mod cast_from_raw {
623674 /// [cast_from_raw]: crate::pointer::SizeFrom::cast_from_raw
624675 //
625676 // FIXME(#1817): Support Sized->Unsized and Unsized->Sized casts
626- pub ( crate ) fn cast_from_raw < Src , Dst > ( src : PtrInner < ' _ , Src > ) -> PtrInner < ' _ , Dst >
677+ pub ( crate ) fn cast_from_raw < Src , Dst , const ALLOW_SHRINK : bool > (
678+ src : PtrInner < ' _ , Src > ,
679+ ) -> PtrInner < ' _ , Dst >
627680 where
628681 Src : KnownLayout < PointerMetadata = usize > + ?Sized ,
629682 Dst : KnownLayout < PointerMetadata = usize > + ?Sized ,
630683 {
684+ // TODO: Update this comment.
685+ //
631686 // At compile time (specifically, post-monomorphization time), we need
632687 // to compute two things:
633688 // - Whether, given *any* `*Src`, it is possible to construct a `*Dst`
@@ -693,13 +748,20 @@ mod cast_from_raw {
693748 ///
694749 /// `Src`'s alignment must not be smaller than `Dst`'s alignment.
695750 #[ derive( Copy , Clone ) ]
696- struct CastParams {
697- offset_delta_elems : usize ,
698- elem_multiple : usize ,
751+ pub ( super ) struct CastParams {
752+ // `offset_delta / dst.elem_size = offset_delta_elems_num / denom`
753+ offset_delta_elems_num : usize ,
754+ // `src.elem_size / dst.elem_size = elem_multiple_num / denom`
755+ elem_multiple_num : usize ,
756+ denom : NonZeroUsize ,
699757 }
700758
701759 impl CastParams {
702- const fn try_compute ( src : & DstLayout , dst : & DstLayout ) -> Option < CastParams > {
760+ const fn try_compute (
761+ src : & DstLayout ,
762+ dst : & DstLayout ,
763+ allow_shrink : bool ,
764+ ) -> Option < CastParams > {
703765 if src. align . get ( ) < dst. align . get ( ) {
704766 return None ;
705767 }
@@ -724,33 +786,35 @@ mod cast_from_raw {
724786 return None ;
725787 } ;
726788
727- // PANICS: `dst_elem_size: NonZeroUsize`, so this won't div by zero.
728- #[ allow( clippy:: arithmetic_side_effects) ]
729- let delta_mod_other_elem = offset_delta % dst_elem_size. get ( ) ;
789+ let gcd = gcd ( offset_delta, src. elem_size , dst_elem_size) . get ( ) ;
730790
731- // PANICS: `dst_elem_size: NonZeroUsize`, so this won't div by zero.
791+ // PANICS: `gcd` is non- zero.
732792 #[ allow( clippy:: arithmetic_side_effects) ]
733- let elem_remainder = src. elem_size % dst_elem_size. get ( ) ;
734-
735- if delta_mod_other_elem != 0 || src. elem_size < dst. elem_size || elem_remainder != 0
736- {
737- return None ;
738- }
793+ let offset_delta_elems_num = offset_delta / gcd;
739794
740- // PANICS: `dst_elem_size: NonZeroUsize`, so this won't div by zero.
795+ // PANICS: `gcd` is non- zero.
741796 #[ allow( clippy:: arithmetic_side_effects) ]
742- let offset_delta_elems = offset_delta / dst_elem_size . get ( ) ;
797+ let elem_multiple_num = src . elem_size / gcd ;
743798
744- // PANICS: `dst_elem_size: NonZeroUsize`, so this won't div by zero.
799+ // PANICS: `dst_elem_size` is non-zero, and `gcd` is no greater
800+ // than it by construction. Thus, this should be at least 1.
745801 #[ allow( clippy:: arithmetic_side_effects) ]
746- let elem_multiple = src. elem_size / dst_elem_size. get ( ) ;
802+ let denom = match NonZeroUsize :: new ( dst_elem_size. get ( ) / gcd) {
803+ Some ( d) => d,
804+ None => const_panic ! ( "CastParams::try_compute: denom should be non-zero" ) ,
805+ } ;
806+
807+ if denom. get ( ) != 1 && !allow_shrink {
808+ return None ;
809+ }
747810
748811 // SAFETY: We checked above that `src.align >= dst.align`.
749812 Some ( CastParams {
750813 // SAFETY: We checked above that this is an exact ratio.
751- offset_delta_elems ,
814+ offset_delta_elems_num ,
752815 // SAFETY: We checked above that this is an exact ratio.
753- elem_multiple,
816+ elem_multiple_num,
817+ denom,
754818 } )
755819 }
756820
@@ -759,12 +823,17 @@ mod cast_from_raw {
759823 /// `src_meta` describes a `Src` whose size is no larger than
760824 /// `isize::MAX`.
761825 ///
762- /// The returned metadata describes a `Dst` of the same size as the
763- /// original `Src`.
826+ /// If `self.denom == 1`, then the returned metadata describes a
827+ /// `Dst` of the same size as the original `Src`. Otherwise, the
828+ /// returned metadata describes a `Dst` whose size is no greater
829+ /// than the size of the original `Src`.
764830 unsafe fn cast_metadata ( self , src_meta : usize ) -> usize {
765831 #[ allow( unused) ]
766832 use crate :: util:: polyfills:: * ;
767833
834+ // TODO: Update this safety comment. Make sure that even if
835+ // `denom > 1`, these arithmetic operations will not overflow.
836+ //
768837 // SAFETY: `self` is a witness that the following equation
769838 // holds:
770839 //
@@ -774,24 +843,61 @@ mod cast_from_raw {
774843 // metadata, this math will not overflow, and the returned value
775844 // will describe a `Dst` of the same size.
776845 #[ allow( unstable_name_collisions) ]
777- unsafe {
778- self . offset_delta_elems
779- . unchecked_add ( src_meta. unchecked_mul ( self . elem_multiple ) )
780- }
846+ let num = unsafe {
847+ self . offset_delta_elems_num
848+ . unchecked_add ( src_meta. unchecked_mul ( self . elem_multiple_num ) )
849+ } ;
850+ num / self . denom
851+ }
852+ }
853+
854+ // Prove that `CastParams::try_compute` does not panic, and that
855+ // `CastParams::cast_metadata` does not exhibit UB. Ideally, we would
856+ // also prove that that a `dst` with `dst_metadata` is no larger than a
857+ // `src` with `src_metadata`, but this is beyond kani's ability to prove
858+ // in a reasonable time.
859+ #[ cfg_attr( kani, kani:: proof) ]
860+ #[ cfg_attr( kani, kani:: stub_verified( gcd) ) ]
861+ fn proof ( ) {
862+ let src: DstLayout = kani:: any ( ) ;
863+ let dst: DstLayout = kani:: any ( ) ;
864+ let allow_shrink: bool = true ;
865+
866+ let SizeInfo :: SliceDst ( src_size_info) = src. size_info else {
867+ kani:: assume ( false ) ;
868+ loop { }
869+ } ;
870+
871+ let SizeInfo :: SliceDst ( _) = dst. size_info else {
872+ kani:: assume ( false ) ;
873+ loop { }
874+ } ;
875+
876+ let params = CastParams :: try_compute ( & src, & dst, allow_shrink) ;
877+
878+ if let Some ( params) = params {
879+ let src_meta = {
880+ let meta: usize = kani:: any ( ) ;
881+ kani:: assume ( src_size_info. is_valid_metadata ( src. align , meta) ) ;
882+ meta
883+ } ;
884+
885+ // SAFETY: Kani will reject the proof if this invocation is unsound.
886+ let _dst_meta = unsafe { params. cast_metadata ( src_meta) } ;
781887 }
782888 }
783889
784- trait Params < Src : ?Sized > {
890+ trait Params < Src : ?Sized , const ALLOW_SHRINK : bool > {
785891 const CAST_PARAMS : CastParams ;
786892 }
787893
788- impl < Src , Dst > Params < Src > for Dst
894+ impl < Src , Dst , const ALLOW_SHRINK : bool > Params < Src , ALLOW_SHRINK > for Dst
789895 where
790896 Src : KnownLayout + ?Sized ,
791897 Dst : KnownLayout < PointerMetadata = usize > + ?Sized ,
792898 {
793899 const CAST_PARAMS : CastParams =
794- match CastParams :: try_compute ( & Src :: LAYOUT , & Dst :: LAYOUT ) {
900+ match CastParams :: try_compute ( & Src :: LAYOUT , & Dst :: LAYOUT , ALLOW_SHRINK ) {
795901 Some ( params) => params,
796902 None => const_panic ! (
797903 "cannot `transmute_ref!` or `transmute_mut!` between incompatible types"
@@ -800,7 +906,7 @@ mod cast_from_raw {
800906 }
801907
802908 let src_meta = <Src as KnownLayout >:: pointer_to_metadata ( src. as_non_null ( ) . as_ptr ( ) ) ;
803- let params = <Dst as Params < Src > >:: CAST_PARAMS ;
909+ let params = <Dst as Params < Src , ALLOW_SHRINK > >:: CAST_PARAMS ;
804910
805911 // SAFETY: `src: PtrInner`, and so by invariant on `PtrInner`, `src`'s
806912 // referent is no larger than `isize::MAX`.
@@ -809,11 +915,11 @@ mod cast_from_raw {
809915 let dst = <Dst as KnownLayout >:: raw_from_ptr_len ( src. as_non_null ( ) . cast ( ) , dst_meta) ;
810916
811917 // SAFETY: By post-condition on `params.cast_metadata`, `dst` addresses
812- // the same number of bytes as `src`. Since `src: PtrInner`, `src` has
813- // provenance for its entire referent, which lives inside of a single
814- // allocation. Since `dst` has the same address as `src` and was
815- // constructed using provenance-preserving operations, it addresses a
816- // subset of those bytes, and has provenance for those bytes.
918+ // no more bytes than `src`. Since `src: PtrInner`, `src` has provenance
919+ // for its entire referent, which lives inside of a single allocation.
920+ // Since `dst` has the same address as `src` and was constructed using
921+ // provenance-preserving operations, it addresses a subset of those
922+ // bytes, and has provenance for those bytes.
817923 unsafe { PtrInner :: new ( dst) }
818924 }
819925}
@@ -823,7 +929,6 @@ mod cast_from_raw {
823929// putting it here works. Once our MSRV is high enough that this bug has been
824930// fixed, remove this `allow`.
825931#[ allow( unknown_lints) ]
826- #[ cfg( test) ]
827932mod tests {
828933 use super :: * ;
829934
0 commit comments