@@ -10,9 +10,7 @@ use rustc_middle::mir::interpret::{
10
10
} ;
11
11
use rustc_middle:: mir:: { Constant , ConstantKind , Operand } ;
12
12
use rustc_middle:: ty:: layout:: LayoutOf ;
13
- use rustc_middle:: ty:: {
14
- self , Const , ConstKind , FloatTy , Instance , IntTy , ScalarInt , Ty , Uint , UintTy ,
15
- } ;
13
+ use rustc_middle:: ty:: { self , Const , ConstKind , FloatTy , Instance , IntTy , Ty , Uint , UintTy } ;
16
14
use rustc_span:: def_id:: DefId ;
17
15
use rustc_span:: Span ;
18
16
use rustc_target:: abi:: { FieldsShape , Size , TagEncoding , Variants } ;
@@ -78,46 +76,67 @@ impl<'tcx> GotocCtx<'tcx> {
78
76
}
79
77
}
80
78
81
- pub fn codegen_const_value (
79
+ fn codegen_slice_value (
82
80
& mut self ,
83
81
v : ConstValue < ' tcx > ,
84
82
lit_ty : Ty < ' tcx > ,
85
83
span : Option < & Span > ,
84
+ data : & Allocation ,
85
+ start : usize ,
86
+ end : usize ,
86
87
) -> Expr {
87
- match v {
88
- ConstValue :: Scalar ( s) => self . codegen_scalar ( s, lit_ty, span) ,
89
- ConstValue :: Slice { data, start, end } => match lit_ty. kind ( ) {
90
- ty:: Ref ( _, ty:: TyS { kind : ty:: Str , .. } , _) => {
88
+ if let ty:: Ref ( _, ref_ty, _) = lit_ty. kind ( ) {
89
+ match ref_ty. kind ( ) {
90
+ ty:: Str => {
91
91
let slice = data. inspect_with_uninit_and_ptr_outside_interpreter ( start..end) ;
92
92
let s = :: std:: str:: from_utf8 ( slice) . expect ( "non utf8 str from miri" ) ;
93
- Expr :: struct_expr_from_values (
93
+ return Expr :: struct_expr_from_values (
94
94
self . codegen_ty ( lit_ty) ,
95
95
vec ! [ Expr :: string_constant( s) , Expr :: int_constant( s. len( ) , Type :: size_t( ) ) ] ,
96
96
& self . symbol_table ,
97
- )
97
+ ) ;
98
98
}
99
- ty:: Ref (
100
- _,
101
- ty:: TyS { kind : ty:: Slice ( ty:: TyS { kind : Uint ( UintTy :: U8 ) , .. } ) , .. } ,
102
- _,
103
- ) => {
104
- // The case where we have a slice of u8 is easy enough: make an array of u8
105
- // TODO: Handle cases with larger int types by making an array of bytes,
106
- // then using byte-extract on it.
107
- let slice = data. inspect_with_uninit_and_ptr_outside_interpreter ( start..end) ;
108
- let vec_of_bytes: Vec < Expr > = slice
109
- . iter ( )
110
- . map ( |b| Expr :: int_constant ( * b, Type :: unsigned_int ( 8 ) ) )
111
- . collect ( ) ;
112
- let len = vec_of_bytes. len ( ) ;
113
- let array_expr =
114
- Expr :: array_expr ( Type :: unsigned_int ( 8 ) . array_of ( len) , vec_of_bytes) ;
115
- let data_expr = array_expr. array_to_ptr ( ) ;
116
- let len_expr = Expr :: int_constant ( len, Type :: size_t ( ) ) ;
117
- slice_fat_ptr ( self . codegen_ty ( lit_ty) , data_expr, len_expr, & self . symbol_table )
99
+ ty:: Slice ( slice_ty) => {
100
+ if let Uint ( UintTy :: U8 ) = slice_ty. kind ( ) {
101
+ // The case where we have a slice of u8 is easy enough: make an array of u8
102
+ // TODO: Handle cases with larger int types by making an array of bytes,
103
+ // then using byte-extract on it.
104
+ let slice =
105
+ data. inspect_with_uninit_and_ptr_outside_interpreter ( start..end) ;
106
+ let vec_of_bytes: Vec < Expr > = slice
107
+ . iter ( )
108
+ . map ( |b| Expr :: int_constant ( * b, Type :: unsigned_int ( 8 ) ) )
109
+ . collect ( ) ;
110
+ let len = vec_of_bytes. len ( ) ;
111
+ let array_expr =
112
+ Expr :: array_expr ( Type :: unsigned_int ( 8 ) . array_of ( len) , vec_of_bytes) ;
113
+ let data_expr = array_expr. array_to_ptr ( ) ;
114
+ let len_expr = Expr :: int_constant ( len, Type :: size_t ( ) ) ;
115
+ return slice_fat_ptr (
116
+ self . codegen_ty ( lit_ty) ,
117
+ data_expr,
118
+ len_expr,
119
+ & self . symbol_table ,
120
+ ) ;
121
+ }
118
122
}
119
- _ => unimplemented ! ( "\n v {:?}\n lit_ty {:?}\n span {:?}" , v, lit_ty, span) ,
120
- } ,
123
+ _ => { }
124
+ }
125
+ }
126
+ unimplemented ! ( "\n v {:?}\n lit_ty {:?}\n span {:?}" , v, lit_ty, span) ;
127
+ }
128
+
129
+ pub fn codegen_const_value (
130
+ & mut self ,
131
+ v : ConstValue < ' tcx > ,
132
+ lit_ty : Ty < ' tcx > ,
133
+ span : Option < & Span > ,
134
+ ) -> Expr {
135
+ match v {
136
+ ConstValue :: Scalar ( s) => self . codegen_scalar ( s, lit_ty, span) ,
137
+ ConstValue :: Slice { data, start, end } => {
138
+ self . codegen_slice_value ( v, lit_ty, span, & data, start, end)
139
+ }
121
140
ConstValue :: ByRef { alloc, offset } => {
122
141
debug ! ( "ConstValue by ref {:?} {:?}" , alloc, offset) ;
123
142
let mem_var =
@@ -132,31 +151,35 @@ impl<'tcx> GotocCtx<'tcx> {
132
151
}
133
152
134
153
fn codegen_scalar ( & mut self , s : Scalar , ty : Ty < ' tcx > , span : Option < & Span > ) -> Expr {
135
- debug ! { "codegen_scalar\n {:?}\n {:?}\n {:?}\n {:?}" , s, ty, span, & ty. kind} ;
154
+ debug ! { "codegen_scalar\n {:?}\n {:?}\n {:?}\n {:?}" , s, ty, span, & ty. kind( ) } ;
136
155
match ( s, & ty. kind ( ) ) {
137
- ( Scalar :: Int ( ScalarInt { data, .. } ) , ty:: Int ( it) ) => match it {
138
- IntTy :: I8 => Expr :: int_constant ( data, Type :: signed_int ( 8 ) ) ,
139
- IntTy :: I16 => Expr :: int_constant ( data, Type :: signed_int ( 16 ) ) ,
140
- IntTy :: I32 => Expr :: int_constant ( data, Type :: signed_int ( 32 ) ) ,
141
- IntTy :: I64 => Expr :: int_constant ( data, Type :: signed_int ( 64 ) ) ,
142
- IntTy :: I128 => Expr :: int_constant ( data, Type :: signed_int ( 128 ) ) ,
143
- IntTy :: Isize => Expr :: int_constant ( data, Type :: ssize_t ( ) ) ,
156
+ ( Scalar :: Int ( _) , ty:: Int ( it) ) => match it {
157
+ // We treat the data as bit vector. Thus, we extract the value as unsigned and set
158
+ // the type to signed int.
159
+ IntTy :: I8 => Expr :: int_constant ( s. to_u8 ( ) . unwrap ( ) , Type :: signed_int ( 8 ) ) ,
160
+ IntTy :: I16 => Expr :: int_constant ( s. to_u16 ( ) . unwrap ( ) , Type :: signed_int ( 16 ) ) ,
161
+ IntTy :: I32 => Expr :: int_constant ( s. to_u32 ( ) . unwrap ( ) , Type :: signed_int ( 32 ) ) ,
162
+ IntTy :: I64 => Expr :: int_constant ( s. to_u64 ( ) . unwrap ( ) , Type :: signed_int ( 64 ) ) ,
163
+ IntTy :: I128 => Expr :: int_constant ( s. to_u128 ( ) . unwrap ( ) , Type :: signed_int ( 128 ) ) ,
164
+ IntTy :: Isize => {
165
+ Expr :: int_constant ( s. to_machine_usize ( self ) . unwrap ( ) , Type :: ssize_t ( ) )
166
+ }
144
167
} ,
145
- ( Scalar :: Int ( ScalarInt { data, .. } ) , ty:: Uint ( it) ) => match it {
146
- UintTy :: U8 => Expr :: int_constant ( data, Type :: unsigned_int ( 8 ) ) ,
147
- UintTy :: U16 => Expr :: int_constant ( data, Type :: unsigned_int ( 16 ) ) ,
148
- UintTy :: U32 => Expr :: int_constant ( data, Type :: unsigned_int ( 32 ) ) ,
149
- UintTy :: U64 => Expr :: int_constant ( data, Type :: unsigned_int ( 64 ) ) ,
150
- UintTy :: U128 => Expr :: int_constant ( data, Type :: unsigned_int ( 128 ) ) ,
151
- UintTy :: Usize => Expr :: int_constant ( data, Type :: size_t ( ) ) ,
168
+ ( Scalar :: Int ( _) , ty:: Uint ( it) ) => match it {
169
+ UintTy :: U8 => Expr :: int_constant ( s. to_u8 ( ) . unwrap ( ) , Type :: unsigned_int ( 8 ) ) ,
170
+ UintTy :: U16 => Expr :: int_constant ( s. to_u16 ( ) . unwrap ( ) , Type :: unsigned_int ( 16 ) ) ,
171
+ UintTy :: U32 => Expr :: int_constant ( s. to_u32 ( ) . unwrap ( ) , Type :: unsigned_int ( 32 ) ) ,
172
+ UintTy :: U64 => Expr :: int_constant ( s. to_u64 ( ) . unwrap ( ) , Type :: unsigned_int ( 64 ) ) ,
173
+ UintTy :: U128 => Expr :: int_constant ( s. to_u128 ( ) . unwrap ( ) , Type :: unsigned_int ( 128 ) ) ,
174
+ UintTy :: Usize => {
175
+ Expr :: int_constant ( s. to_machine_usize ( self ) . unwrap ( ) , Type :: size_t ( ) )
176
+ }
152
177
} ,
153
- ( Scalar :: Int ( ScalarInt { .. } ) , ty:: Bool ) => {
154
- Expr :: c_bool_constant ( s. to_bool ( ) . unwrap ( ) )
155
- }
156
- ( Scalar :: Int ( ScalarInt { .. } ) , ty:: Char ) => {
178
+ ( Scalar :: Int ( _) , ty:: Bool ) => Expr :: c_bool_constant ( s. to_bool ( ) . unwrap ( ) ) ,
179
+ ( Scalar :: Int ( _) , ty:: Char ) => {
157
180
Expr :: int_constant ( s. to_i32 ( ) . unwrap ( ) , Type :: signed_int ( 32 ) )
158
181
}
159
- ( Scalar :: Int ( ScalarInt { .. } ) , ty:: Float ( k) ) =>
182
+ ( Scalar :: Int ( _ ) , ty:: Float ( k) ) =>
160
183
// rustc uses a sophisticated format for floating points that is hard to get f32/f64 from.
161
184
// Instead, we use integers with the right width to represent the bit pattern.
162
185
{
@@ -165,18 +188,23 @@ impl<'tcx> GotocCtx<'tcx> {
165
188
FloatTy :: F64 => Expr :: double_constant_from_bitpattern ( s. to_u64 ( ) . unwrap ( ) ) ,
166
189
}
167
190
}
168
- ( Scalar :: Int ( ScalarInt { size : 0 , .. } ) , ty:: FnDef ( d, substs) ) => {
191
+ ( Scalar :: Int ( int) , ty:: FnDef ( d, substs) ) => {
192
+ assert_eq ! ( int. size( ) , Size :: ZERO ) ;
169
193
self . codegen_fndef ( * d, substs, span)
170
194
}
171
- ( Scalar :: Int ( ScalarInt { .. } ) , ty:: RawPtr ( tm) ) => {
195
+ ( Scalar :: Int ( _ ) , ty:: RawPtr ( tm) ) => {
172
196
Expr :: pointer_constant ( s. to_u64 ( ) . unwrap ( ) , self . codegen_ty ( tm. ty ) . to_pointer ( ) )
173
197
}
174
198
// TODO: Removing this doesn't cause any regressions to fail.
175
199
// We need a regression for this case.
176
- ( Scalar :: Int ( ScalarInt { data : 0 , .. } ) , ty:: Ref ( _, ty, _) ) => {
177
- self . codegen_ty ( ty) . to_pointer ( ) . null ( )
200
+ ( Scalar :: Int ( int) , ty:: Ref ( _, ty, _) ) => {
201
+ if int. is_null ( ) {
202
+ self . codegen_ty ( ty) . to_pointer ( ) . null ( )
203
+ } else {
204
+ unreachable ! ( )
205
+ }
178
206
}
179
- ( Scalar :: Int ( ScalarInt { .. } ) , ty:: Adt ( adt, subst) ) => {
207
+ ( Scalar :: Int ( _ ) , ty:: Adt ( adt, subst) ) => {
180
208
if adt. is_struct ( ) || adt. is_union ( ) {
181
209
// in this case, we must have a one variant ADT. there are two cases
182
210
let variant = & adt. variants . raw [ 0 ] ;
0 commit comments