@@ -4020,9 +4020,8 @@ impl<T> [T] {
40204020 offset > self . len( ) || {
40214021 let ( _, rest) = self . split_at( offset) ;
40224022 let ( us_len, _) = rest. align_to_offsets:: <U >( ) ;
4023- let middle = crate :: ptr:: slice_from_raw_parts( rest. as_ptr( ) as * const U , us_len)
4024- ;
4025- ub_checks:: can_dereference( middle)
4023+ let middle = crate :: ptr:: slice_from_raw_parts( rest. as_ptr( ) as * const U , us_len) ;
4024+ crate :: ub_checks:: can_dereference( middle)
40264025 }
40274026 }
40284027 ) ]
@@ -4147,6 +4146,44 @@ impl<T> [T] {
41474146 }
41484147 }
41494148
4149+ //We need the following wrapper because it is not currently possible to write
4150+ //contracts for functions that return mut refs to input arguments
4151+ //see https://github.com/model-checking/kani/issues/3764
4152+ //----------------------------
4153+ //Checks if the part that will be transmuted from type T to U is valid for type U
4154+ //reuses most function logic up to use of from_raw_parts,
4155+ //where the potentially unsafe transmute occurs
4156+ #[ requires(
4157+ U :: IS_ZST || T :: IS_ZST || {
4158+ let ptr = self . as_ptr( ) ;
4159+ let offset = crate :: ptr:: align_offset( ptr, align_of:: <U >( ) ) ;
4160+ offset > self . len( ) || {
4161+ let ( _, rest) = self . split_at( offset) ;
4162+ let ( us_len, _) = rest. align_to_offsets:: <U >( ) ;
4163+ let middle = crate :: ptr:: slice_from_raw_parts( rest. as_ptr( ) as * const U , us_len) ;
4164+ crate :: ub_checks:: can_dereference( middle)
4165+ }
4166+ }
4167+ ) ]
4168+ //The following two ensures clauses guarantee that middle is of maximum size within self
4169+ #[ ensures( |( prefix, _, _) : & ( * const [ T ] , * const [ U ] , * const [ T ] ) | prefix. len( ) * size_of:: <T >( )
4170+ < align_of:: <U >( ) ) ]
4171+ #[ ensures( |( _, _, suffix) : & ( * const [ T ] , * const [ U ] , * const [ T ] ) | suffix. len( ) * size_of:: <T >( ) < size_of:: <U >( ) ) ]
4172+ //Either align_to just returns self in the prefix, or the 3 returned slices
4173+ //should be sequential, contiguous, and have same total length as self
4174+ #[ ensures( |( prefix, middle, suffix) : & ( * const [ T ] , * const [ U ] , * const [ T ] ) |
4175+ prefix. as_ptr( ) == self . as_ptr( ) &&
4176+ ( prefix. len( ) == self . len( ) || (
4177+ ( ( prefix. as_ptr( ) ) . add( prefix. len( ) ) as * const u8 == middle. as_ptr( ) as * const u8 ) &&
4178+ ( ( middle. as_ptr( ) ) . add( middle. len( ) ) as * const u8 == suffix. as_ptr( ) as * const u8 ) &&
4179+ ( ( suffix. as_ptr( ) ) . add( suffix. len( ) ) == ( self . as_ptr( ) ) . add( self . len( ) ) ) )
4180+ )
4181+ ) ]
4182+ unsafe fn align_to_mut_wrapper < U > ( & mut self ) -> ( * const [ T ] , * const [ U ] , * const [ T ] ) {
4183+ let ( prefix_mut, mid_mut, suffix_mut) = self . align_to_mut :: < U > ( ) ;
4184+ ( prefix_mut as * const [ T ] , mid_mut as * const [ U ] , suffix_mut as * const [ T ] )
4185+ }
4186+
41504187 /// Splits a slice into a prefix, a middle of aligned SIMD types, and a suffix.
41514188 ///
41524189 /// This is a safe wrapper around [`slice::align_to`], so inherits the same
@@ -5368,50 +5405,6 @@ mod verify {
53685405 gen_align_to_harnesses ! ( align_to_from_char, char ) ;
53695406 gen_align_to_harnesses ! ( align_to_from_unit, ( ) ) ;
53705407
5371- trait wrap_align_to_mut < T > {
5372- unsafe fn align_to_mut_wrapper < U > ( & mut self ) -> ( * const [ T ] , * const [ U ] , * const [ T ] ) ;
5373- }
5374-
5375- //We write this as an impl so that we can refer to "self"
5376- impl < T > wrap_align_to_mut < T > for [ T ] {
5377- //We need the following wrapper because it is not currently possible to write
5378- //contracts for functions that return mut refs to input arguments
5379- //see https://github.com/model-checking/kani/issues/3764
5380- //----------------------------
5381- //Checks if the part that will be transmuted from type T to U is valid for type U
5382- //reuses most function logic up to use of from_raw_parts,
5383- //where the potentially unsafe transmute occurs
5384- #[ requires(
5385- U :: IS_ZST || T :: IS_ZST || {
5386- let ptr = self . as_ptr( ) ;
5387- let offset = crate :: ptr:: align_offset( ptr, align_of:: <U >( ) ) ;
5388- offset > self . len( ) || {
5389- let ( _, rest) = self . split_at( offset) ;
5390- let ( us_len, _) = rest. align_to_offsets:: <U >( ) ;
5391- let middle = crate :: ptr:: slice_from_raw_parts( rest. as_ptr( ) as * const U , us_len) ;
5392- ub_checks:: can_dereference( middle)
5393- }
5394- }
5395- ) ]
5396- //The following two ensures clauses guarantee that middle is of maximum size within self
5397- #[ ensures( |( prefix, _, _) : & ( * const [ T ] , * const [ U ] , * const [ T ] ) | prefix. len( ) * size_of:: <T >( ) < align_of:: <U >( ) ) ]
5398- #[ ensures( |( _, _, suffix) : & ( * const [ T ] , * const [ U ] , * const [ T ] ) | suffix. len( ) * size_of:: <T >( ) < size_of:: <U >( ) ) ]
5399- //Either align_to just returns self in the prefix, or the 3 returned slices
5400- //should be sequential, contiguous, and have same total length as self
5401- #[ ensures( |( prefix, middle, suffix) : & ( * const [ T ] , * const [ U ] , * const [ T ] ) |
5402- prefix. as_ptr( ) == self . as_ptr( ) &&
5403- ( prefix. len( ) == self . len( ) || (
5404- ( ( prefix. as_ptr( ) ) . add( prefix. len( ) ) as * const u8 == middle. as_ptr( ) as * const u8 ) &&
5405- ( ( middle. as_ptr( ) ) . add( middle. len( ) ) as * const u8 == suffix. as_ptr( ) as * const u8 ) &&
5406- ( ( suffix. as_ptr( ) ) . add( suffix. len( ) ) == ( self . as_ptr( ) ) . add( self . len( ) ) ) )
5407- )
5408- ) ]
5409- unsafe fn align_to_mut_wrapper < U > ( & mut self ) -> ( * const [ T ] , * const [ U ] , * const [ T ] ) {
5410- let ( prefix_mut, mid_mut, suffix_mut) = self . align_to_mut :: < U > ( ) ;
5411- ( prefix_mut as * const [ T ] , mid_mut as * const [ U ] , suffix_mut as * const [ T ] )
5412- }
5413- }
5414-
54155408 macro_rules! proof_of_contract_for_align_to_mut {
54165409 ( $harness: ident, $src: ty, $dst: ty) => {
54175410 #[ kani:: proof_for_contract( <[ $src] >:: align_to_mut_wrapper) ]
0 commit comments