@@ -5,6 +5,7 @@ use super::cbmc::utils::aggr_name;
5
5
use super :: cbmc:: MachineModel ;
6
6
use super :: metadata:: * ;
7
7
use super :: utils:: { dynamic_fat_ptr, slice_fat_ptr} ;
8
+ use crate :: btree_string_map;
8
9
use rustc_ast:: ast:: Mutability ;
9
10
use rustc_middle:: mir:: { AggregateKind , BinOp , CastKind , NullOp , Operand , Place , Rvalue , UnOp } ;
10
11
use rustc_middle:: ty:: adjustment:: PointerCast ;
@@ -98,8 +99,9 @@ impl<'tcx> GotocCtx<'tcx> {
98
99
let pt = self . place_ty ( p) ;
99
100
let place = self . codegen_place ( p) ;
100
101
debug ! ( "codegen_rvalue_ref||{:?}||{:?}||{:?}||{:?}" , p, pt, pt. kind( ) , place) ;
102
+
101
103
match pt. kind ( ) {
102
- ty :: Slice ( _ ) | ty :: Str | ty :: Dynamic ( .. ) => {
104
+ _ if self . is_unsized ( pt ) => {
103
105
let fat_ptr = place. fat_ptr_goto_expr . unwrap ( ) ;
104
106
match place. fat_ptr_mir_typ . unwrap ( ) . kind ( ) {
105
107
ty:: Ref ( _, to, _) | ty:: RawPtr ( ty:: TypeAndMut { ty : to, .. } ) => {
@@ -109,9 +111,23 @@ impl<'tcx> GotocCtx<'tcx> {
109
111
// A user defined DST type needs special handling
110
112
// https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp
111
113
assert ! ( self . is_unsized( to) ) ;
114
+ // In cbmc-reg/Strings/os_str_reduced.rs, we have a flexible array
115
+ // which needs to be decayed to a pointer.
116
+ // In cbmc-reg/Cast/path.rs, we have an ADT, where we need to
117
+ // take its address to get the pointer
118
+ // See the comment in `codegen_projection`.
119
+ let data = if place. goto_expr . typ ( ) . is_pointer ( ) {
120
+ place. goto_expr
121
+ } else if place. goto_expr . typ ( ) . is_array_like ( ) {
122
+ place. goto_expr . array_to_ptr ( )
123
+ } else {
124
+ place. goto_expr . address_of ( )
125
+ } ;
126
+ // TODO: this assumes we have a slice. But it might be dynamic.
112
127
slice_fat_ptr (
113
128
self . codegen_ty ( res_ty) ,
114
- place. goto_expr . array_to_ptr ( ) ,
129
+ // place.goto_expr.decay_to_ptr(),
130
+ data,
115
131
fat_ptr. member ( "len" , & self . symbol_table ) ,
116
132
& self . symbol_table ,
117
133
)
@@ -153,6 +169,7 @@ impl<'tcx> GotocCtx<'tcx> {
153
169
// But I'm not sure that its actually correct for all the match arms.
154
170
place. goto_expr . address_of ( )
155
171
}
172
+ ty:: Slice ( _) | ty:: Str | ty:: Dynamic ( ..) => unreachable ! ( ) ,
156
173
}
157
174
}
158
175
@@ -477,6 +494,42 @@ impl<'tcx> GotocCtx<'tcx> {
477
494
}
478
495
}
479
496
497
+ pub fn codegen_fat_ptr_to_fat_ptr_cast (
498
+ & mut self ,
499
+ src : & Operand < ' tcx > ,
500
+ dst_t : Ty < ' tcx > ,
501
+ ) -> Expr {
502
+ debug ! ( "codegen_fat_ptr_to_fat_ptr_cast |{:?}| |{:?}|" , src, dst_t) ;
503
+ let src_goto_expr = self . codegen_operand ( src) ;
504
+ let dst_goto_typ = self . codegen_ty ( dst_t) ;
505
+ let dst_data_type =
506
+ self . symbol_table . lookup_field_type_in_type ( & dst_goto_typ, "data" ) . unwrap ( ) ;
507
+ let dst_data_field = (
508
+ "data" ,
509
+ src_goto_expr. clone ( ) . member ( "data" , & self . symbol_table ) . cast_to ( dst_data_type. clone ( ) ) ,
510
+ ) ;
511
+
512
+ let dst_metadata_field = if let Some ( vtable_typ) =
513
+ self . symbol_table . lookup_field_type_in_type ( & dst_goto_typ, "vtable" )
514
+ {
515
+ (
516
+ "vtable" ,
517
+ src_goto_expr. member ( "vtable" , & self . symbol_table ) . cast_to ( vtable_typ. clone ( ) ) ,
518
+ )
519
+ } else if let Some ( len_typ) =
520
+ self . symbol_table . lookup_field_type_in_type ( & dst_goto_typ, "len" )
521
+ {
522
+ ( "len" , src_goto_expr. member ( "len" , & self . symbol_table ) . cast_to ( len_typ. clone ( ) ) )
523
+ } else {
524
+ unreachable ! ( "fat pointer with neither vtable nor len. {:?} {:?}" , src, dst_t) ;
525
+ } ;
526
+ Expr :: struct_expr (
527
+ dst_goto_typ,
528
+ btree_string_map ! [ dst_data_field, dst_metadata_field] ,
529
+ & self . symbol_table ,
530
+ )
531
+ }
532
+
480
533
fn codegen_misc_cast ( & mut self , src : & Operand < ' tcx > , dst_t : Ty < ' tcx > ) -> Expr {
481
534
let src_t = self . operand_ty ( src) ;
482
535
debug ! (
@@ -500,6 +553,11 @@ impl<'tcx> GotocCtx<'tcx> {
500
553
return self . codegen_get_discriminant ( operand, src_t, dst_t) ;
501
554
}
502
555
556
+ // Cast between fat pointers
557
+ if self . is_ref_of_unsized ( src_t) && self . is_ref_of_unsized ( dst_t) {
558
+ return self . codegen_fat_ptr_to_fat_ptr_cast ( src, dst_t) ;
559
+ }
560
+
503
561
// pointer casting. from a pointer / reference to another pointer / reference
504
562
// notice that if fat pointer is involved, it cannot be the destination, which is t.
505
563
match dst_t. kind ( ) {
0 commit comments