8
8
use super :: cbmc:: goto_program:: { Expr , Type } ;
9
9
use super :: metadata:: * ;
10
10
use super :: typ:: tuple_fld;
11
- use rustc_middle :: mir :: { Field , Local , Place , ProjectionElem } ;
11
+ use rustc_ast :: ast :: Mutability ;
12
12
use rustc_middle:: ty:: { self , Ty , TyS , VariantDef } ;
13
+ use rustc_middle:: {
14
+ mir:: { Field , Local , Place , ProjectionElem } ,
15
+ ty:: layout:: HasTyCtxt ,
16
+ } ;
13
17
use rustc_target:: abi:: { LayoutOf , TagEncoding , Variants } ;
14
18
use tracing:: debug;
15
19
@@ -95,13 +99,18 @@ impl<'tcx> ProjectedPlace<'tcx> {
95
99
}
96
100
// TODO: these assertions fail on a few regressions. Figure out why.
97
101
// I think it may have to do with boxed fat pointers.
98
- // assert!(Self::check_expr_typ(&expr, &typ, ctx), "\n{:?}\n{:?}", &expr, &typ);
99
102
// assert!(
100
- // Self::check_fat_ptr_typ(&fat_ptr , &fat_ptr_typ , ctx),
103
+ // Self::check_expr_typ(&goto_expr , &mir_typ_or_variant , ctx),
101
104
// "\n{:?}\n{:?}",
102
- // &fat_ptr ,
103
- // &fat_ptr_typ
105
+ // &goto_expr ,
106
+ // &mir_typ_or_variant
104
107
// );
108
+ assert ! (
109
+ Self :: check_fat_ptr_typ( & fat_ptr_goto_expr, & fat_ptr_mir_typ, ctx) ,
110
+ "\n {:?}\n {:?}" ,
111
+ & fat_ptr_goto_expr,
112
+ & fat_ptr_mir_typ
113
+ ) ;
105
114
ProjectedPlace { goto_expr, mir_typ_or_variant, fat_ptr_goto_expr, fat_ptr_mir_typ }
106
115
}
107
116
}
@@ -219,12 +228,12 @@ impl<'tcx> GotocCtx<'tcx> {
219
228
} else {
220
229
before. goto_expr
221
230
} ;
222
- let inner_mir_typ = base_type. builtin_deref ( true ) . unwrap ( ) . ty ;
223
231
232
+ let inner_mir_typ_and_mut = base_type. builtin_deref ( true ) . unwrap ( ) ;
224
233
let fat_ptr_mir_typ = if self . is_box_of_unsized ( base_type) {
225
234
assert ! ( before. fat_ptr_mir_typ. is_none( ) ) ;
226
- //TODO, not sure this is correct
227
- Some ( base_type . boxed_ty ( ) )
235
+ // If we have a box, its fat pointer typ is a pointer to the boxes inner type.
236
+ Some ( self . tcx . mk_ptr ( inner_mir_typ_and_mut ) )
228
237
} else if self . is_ref_of_unsized ( base_type) {
229
238
assert ! ( before. fat_ptr_mir_typ. is_none( ) ) ;
230
239
Some ( before. mir_typ_or_variant . expect_type ( ) )
@@ -240,6 +249,7 @@ impl<'tcx> GotocCtx<'tcx> {
240
249
before. fat_ptr_goto_expr
241
250
} ;
242
251
252
+ let inner_mir_typ = inner_mir_typ_and_mut. ty ;
243
253
let expr = match inner_mir_typ. kind ( ) {
244
254
ty:: Slice ( _) | ty:: Str | ty:: Dynamic ( ..) => {
245
255
inner_goto_expr. member ( "data" , & self . symbol_table )
0 commit comments