@@ -6,10 +6,8 @@ use crate::unwrap_or_return_codegen_unimplemented;
6
6
use cbmc:: btree_string_map;
7
7
use cbmc:: goto_program:: { DatatypeComponent , Expr , ExprValue , Location , Stmt , Symbol , Type } ;
8
8
use rustc_ast:: ast:: Mutability ;
9
- use rustc_middle:: mir:: interpret:: {
10
- read_target_uint, AllocId , Allocation , ConstValue , GlobalAlloc , Scalar ,
11
- } ;
12
- use rustc_middle:: mir:: { Constant , ConstantKind , Operand , UnevaluatedConst } ;
9
+ use rustc_middle:: mir:: interpret:: { read_target_uint, AllocId , Allocation , GlobalAlloc , Scalar } ;
10
+ use rustc_middle:: mir:: { Const as mirConst, ConstOperand , ConstValue , Operand , UnevaluatedConst } ;
13
11
use rustc_middle:: ty:: layout:: LayoutOf ;
14
12
use rustc_middle:: ty:: { self , Const , ConstKind , FloatTy , Instance , IntTy , Ty , Uint , UintTy } ;
15
13
use rustc_span:: def_id:: DefId ;
@@ -56,13 +54,13 @@ impl<'tcx> GotocCtx<'tcx> {
56
54
/// 1. `Ty` means e.g. that it's a const generic parameter. (See `codegen_const`)
57
55
/// 2. `Val` means it's a constant value of various kinds. (See `codegen_const_value`)
58
56
/// 3. `Unevaluated` means we need to run the interpreter, to get a `ConstValue`. (See `codegen_const_unevaluated`)
59
- fn codegen_constant ( & mut self , c : & Constant < ' tcx > ) -> Expr {
57
+ fn codegen_constant ( & mut self , c : & ConstOperand < ' tcx > ) -> Expr {
60
58
trace ! ( constant=?c, "codegen_constant" ) ;
61
59
let span = Some ( & c. span ) ;
62
- match self . monomorphize ( c. literal ) {
63
- ConstantKind :: Ty ( ct) => self . codegen_const ( ct, span) ,
64
- ConstantKind :: Val ( val, ty) => self . codegen_const_value ( val, ty, span) ,
65
- ConstantKind :: Unevaluated ( unevaluated, ty) => {
60
+ match self . monomorphize ( c. const_ ) {
61
+ mirConst :: Ty ( ct) => self . codegen_const ( ct, span) ,
62
+ mirConst :: Val ( val, ty) => self . codegen_const_value ( val, ty, span) ,
63
+ mirConst :: Unevaluated ( unevaluated, ty) => {
66
64
self . codegen_const_unevaluated ( unevaluated, ty, span)
67
65
}
68
66
}
@@ -125,8 +123,8 @@ impl<'tcx> GotocCtx<'tcx> {
125
123
trace ! ( val=?v, ?lit_ty, "codegen_const_value" ) ;
126
124
match v {
127
125
ConstValue :: Scalar ( s) => self . codegen_scalar ( s, lit_ty, span) ,
128
- ConstValue :: Slice { data, start , end } => {
129
- self . codegen_slice_value ( v, lit_ty, span, data. inner ( ) , start , end )
126
+ ConstValue :: Slice { data, meta } => {
127
+ self . codegen_slice_value ( v, lit_ty, span, data. inner ( ) , meta . try_into ( ) . unwrap ( ) )
130
128
}
131
129
ConstValue :: Indirect { alloc_id, offset } => {
132
130
let alloc = self . tcx . global_alloc ( alloc_id) . unwrap_memory ( ) ;
@@ -155,15 +153,12 @@ impl<'tcx> GotocCtx<'tcx> {
155
153
lit_ty : Ty < ' tcx > ,
156
154
span : Option < & Span > ,
157
155
data : & ' tcx Allocation ,
158
- start : usize ,
159
- end : usize ,
156
+ size : usize ,
160
157
) -> Expr {
161
158
if let ty:: Ref ( _, ref_ty, _) = lit_ty. kind ( ) {
162
159
match ref_ty. kind ( ) {
163
160
ty:: Str => {
164
161
// a string literal
165
- // These seem to always start at 0
166
- assert_eq ! ( start, 0 ) ;
167
162
// Create a static variable that holds its value
168
163
let mem_var = self . codegen_const_allocation ( data, None ) ;
169
164
@@ -179,15 +174,15 @@ impl<'tcx> GotocCtx<'tcx> {
179
174
} ;
180
175
181
176
// Extract the actual string literal
182
- let slice = data. inspect_with_uninit_and_ptr_outside_interpreter ( start..end ) ;
177
+ let slice = data. inspect_with_uninit_and_ptr_outside_interpreter ( 0 ..size ) ;
183
178
let s = :: std:: str:: from_utf8 ( slice) . expect ( "non utf8 str from miri" ) ;
184
179
185
180
// Store the identifier to the string literal in the goto context
186
181
self . str_literals . insert ( * ident, s. into ( ) ) ;
187
182
188
183
// Codegen as a fat pointer
189
184
let data_expr = mem_var. cast_to ( Type :: unsigned_int ( 8 ) . to_pointer ( ) ) ;
190
- let len_expr = Expr :: int_constant ( end - start , Type :: size_t ( ) ) ;
185
+ let len_expr = Expr :: int_constant ( size , Type :: size_t ( ) ) ;
191
186
return slice_fat_ptr (
192
187
self . codegen_ty ( lit_ty) ,
193
188
data_expr,
@@ -198,8 +193,7 @@ impl<'tcx> GotocCtx<'tcx> {
198
193
ty:: Slice ( slice_ty) => {
199
194
if let Uint ( UintTy :: U8 ) = slice_ty. kind ( ) {
200
195
let mem_var = self . codegen_const_allocation ( data, None ) ;
201
- let slice =
202
- data. inspect_with_uninit_and_ptr_outside_interpreter ( start..end) ;
196
+ let slice = data. inspect_with_uninit_and_ptr_outside_interpreter ( 0 ..size) ;
203
197
let len = slice. len ( ) ;
204
198
let data_expr = mem_var. cast_to ( Type :: unsigned_int ( 8 ) . to_pointer ( ) ) ;
205
199
let len_expr = Expr :: int_constant ( len, Type :: size_t ( ) ) ;
0 commit comments