2
2
// SPDX-License-Identifier: Apache-2.0 OR MIT
3
3
4
4
use super :: typ:: pointee_type;
5
+ use crate :: codegen_cprover_gotoc:: codegen:: place:: { ProjectedPlace , TypeOrVariant } ;
5
6
use crate :: codegen_cprover_gotoc:: codegen:: PropertyClass ;
6
7
use crate :: codegen_cprover_gotoc:: utils:: { dynamic_fat_ptr, slice_fat_ptr} ;
7
8
use crate :: codegen_cprover_gotoc:: { GotocCtx , VtableCtx } ;
@@ -17,9 +18,9 @@ use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place,
17
18
use rustc_middle:: ty:: adjustment:: PointerCast ;
18
19
use rustc_middle:: ty:: layout:: LayoutOf ;
19
20
use rustc_middle:: ty:: { self , Instance , IntTy , Ty , TyCtxt , UintTy , VtblEntry } ;
20
- use rustc_target:: abi:: { FieldsShape , Size , TagEncoding , Variants } ;
21
+ use rustc_target:: abi:: { FieldsShape , Size , TagEncoding , VariantIdx , Variants } ;
21
22
use std:: collections:: BTreeMap ;
22
- use tracing:: { debug, warn} ;
23
+ use tracing:: { debug, trace , warn} ;
23
24
24
25
impl < ' tcx > GotocCtx < ' tcx > {
25
26
fn codegen_comparison ( & mut self , op : & BinOp , e1 : & Operand < ' tcx > , e2 : & Operand < ' tcx > ) -> Expr {
@@ -279,13 +280,112 @@ impl<'tcx> GotocCtx<'tcx> {
279
280
}
280
281
}
281
282
283
+ /// Create an initializer for a generator struct.
284
+ fn codegen_rvalue_generator ( & mut self , operands : & [ Operand < ' tcx > ] , ty : Ty < ' tcx > ) -> Expr {
285
+ let layout = self . layout_of ( ty) ;
286
+ let discriminant_field = match & layout. variants {
287
+ Variants :: Multiple { tag_encoding : TagEncoding :: Direct , tag_field, .. } => tag_field,
288
+ _ => unreachable ! (
289
+ "Expected generators to have multiple variants and direct encoding, but found: {layout:?}"
290
+ ) ,
291
+ } ;
292
+ let overall_t = self . codegen_ty ( ty) ;
293
+ let direct_fields = overall_t. lookup_field ( "direct_fields" , & self . symbol_table ) . unwrap ( ) ;
294
+ let mut operands_iter = operands. iter ( ) ;
295
+ let direct_fields_expr = Expr :: struct_expr_from_values (
296
+ direct_fields. typ ( ) ,
297
+ layout
298
+ . fields
299
+ . index_by_increasing_offset ( )
300
+ . map ( |idx| {
301
+ let field_ty = layout. field ( self , idx) . ty ;
302
+ if idx == * discriminant_field {
303
+ Expr :: int_constant ( 0 , self . codegen_ty ( field_ty) )
304
+ } else {
305
+ self . codegen_operand ( operands_iter. next ( ) . unwrap ( ) )
306
+ }
307
+ } )
308
+ . collect ( ) ,
309
+ & self . symbol_table ,
310
+ ) ;
311
+ assert ! ( operands_iter. next( ) . is_none( ) ) ;
312
+ Expr :: union_expr ( overall_t, "direct_fields" , direct_fields_expr, & self . symbol_table )
313
+ }
314
+
315
+ /// This code will generate an expression that initializes an enumeration.
316
+ ///
317
+ /// It will first create a temporary variant with the same enum type.
318
+ /// Initialize the case structure and set its discriminant.
319
+ /// Finally, it will return the temporary value.
320
+ fn codegen_rvalue_enum_aggregate (
321
+ & mut self ,
322
+ variant_index : VariantIdx ,
323
+ operands : & [ Operand < ' tcx > ] ,
324
+ res_ty : Ty < ' tcx > ,
325
+ loc : Location ,
326
+ ) -> Expr {
327
+ let mut stmts = vec ! [ ] ;
328
+ let typ = self . codegen_ty ( res_ty) ;
329
+ // 1- Create a temporary value of the enum type.
330
+ tracing:: debug!( ?typ, ?res_ty, "aggregate_enum" ) ;
331
+ let ( temp_var, decl) = self . decl_temp_variable ( typ. clone ( ) , None , loc) ;
332
+ stmts. push ( decl) ;
333
+ if !operands. is_empty ( ) {
334
+ // 2- Initialize the members of the temporary variant.
335
+ let initial_projection = ProjectedPlace :: try_new (
336
+ temp_var. clone ( ) ,
337
+ TypeOrVariant :: Type ( res_ty) ,
338
+ None ,
339
+ None ,
340
+ self ,
341
+ )
342
+ . unwrap ( ) ;
343
+ let variant_proj = self . codegen_variant_lvalue ( initial_projection, variant_index) ;
344
+ let variant_expr = variant_proj. goto_expr . clone ( ) ;
345
+ let layout = self . layout_of ( res_ty) ;
346
+ let fields = match & layout. variants {
347
+ Variants :: Single { index } => {
348
+ if * index != variant_index {
349
+ // This may occur if all variants except for the one pointed by
350
+ // index can never be constructed. Generic code might still try
351
+ // to initialize the non-existing invariant.
352
+ trace ! ( ?res_ty, ?variant_index, "Unreachable invariant" ) ;
353
+ return Expr :: nondet ( typ) ;
354
+ }
355
+ & layout. fields
356
+ }
357
+ Variants :: Multiple { variants, .. } => & variants[ variant_index] . fields ,
358
+ } ;
359
+
360
+ trace ! ( ?variant_expr, ?fields, ?operands, "codegen_aggregate enum" ) ;
361
+ let init_struct = Expr :: struct_expr_from_values (
362
+ variant_expr. typ ( ) . clone ( ) ,
363
+ fields
364
+ . index_by_increasing_offset ( )
365
+ . map ( |idx| self . codegen_operand ( & operands[ idx] ) )
366
+ . collect ( ) ,
367
+ & self . symbol_table ,
368
+ ) ;
369
+ let assign_case = variant_proj. goto_expr . assign ( init_struct, loc) ;
370
+ stmts. push ( assign_case) ;
371
+ }
372
+ // 3- Set discriminant.
373
+ let set_discriminant =
374
+ self . codegen_set_discriminant ( res_ty, temp_var. clone ( ) , variant_index, loc) ;
375
+ stmts. push ( set_discriminant) ;
376
+ // 4- Return temporary variable.
377
+ stmts. push ( temp_var. as_stmt ( loc) ) ;
378
+ Expr :: statement_expression ( stmts, typ)
379
+ }
380
+
282
381
fn codegen_rvalue_aggregate (
283
382
& mut self ,
284
- k : & AggregateKind < ' tcx > ,
383
+ aggregate : & AggregateKind < ' tcx > ,
285
384
operands : & [ Operand < ' tcx > ] ,
286
385
res_ty : Ty < ' tcx > ,
386
+ loc : Location ,
287
387
) -> Expr {
288
- match * k {
388
+ match * aggregate {
289
389
AggregateKind :: Array ( et) => {
290
390
if et. is_unit ( ) {
291
391
Expr :: struct_expr_from_values (
@@ -304,7 +404,44 @@ impl<'tcx> GotocCtx<'tcx> {
304
404
)
305
405
}
306
406
}
307
- AggregateKind :: Tuple => {
407
+ AggregateKind :: Adt ( _, _, _, _, Some ( active_field_index) ) => {
408
+ assert ! ( res_ty. is_union( ) ) ;
409
+ assert_eq ! ( operands. len( ) , 1 ) ;
410
+ let typ = self . codegen_ty ( res_ty) ;
411
+ let components = typ. lookup_components ( & self . symbol_table ) . unwrap ( ) ;
412
+ Expr :: union_expr (
413
+ typ,
414
+ components[ active_field_index] . name ( ) ,
415
+ self . codegen_operand ( & operands[ 0 ] ) ,
416
+ & self . symbol_table ,
417
+ )
418
+ }
419
+ AggregateKind :: Adt ( _, _, _, _, _) if res_ty. is_simd ( ) => {
420
+ let typ = self . codegen_ty ( res_ty) ;
421
+ let layout = self . layout_of ( res_ty) ;
422
+ let vector_element_type = typ. base_type ( ) . unwrap ( ) . clone ( ) ;
423
+ Expr :: vector_expr (
424
+ typ,
425
+ layout
426
+ . fields
427
+ . index_by_increasing_offset ( )
428
+ . map ( |idx| {
429
+ let cgo = self . codegen_operand ( & operands[ idx] ) ;
430
+ // The input operand might actually be a one-element array, as seen
431
+ // when running assess on firecracker.
432
+ if * cgo. typ ( ) == vector_element_type {
433
+ cgo
434
+ } else {
435
+ cgo. transmute_to ( vector_element_type. clone ( ) , & self . symbol_table )
436
+ }
437
+ } )
438
+ . collect ( ) ,
439
+ )
440
+ }
441
+ AggregateKind :: Adt ( _, variant_index, ..) if res_ty. is_enum ( ) => {
442
+ self . codegen_rvalue_enum_aggregate ( variant_index, operands, res_ty, loc)
443
+ }
444
+ AggregateKind :: Adt ( ..) | AggregateKind :: Closure ( ..) | AggregateKind :: Tuple => {
308
445
let typ = self . codegen_ty ( res_ty) ;
309
446
let layout = self . layout_of ( res_ty) ;
310
447
Expr :: struct_expr_from_values (
@@ -317,9 +454,7 @@ impl<'tcx> GotocCtx<'tcx> {
317
454
& self . symbol_table ,
318
455
)
319
456
}
320
- AggregateKind :: Adt ( _, _, _, _, _) => unimplemented ! ( ) ,
321
- AggregateKind :: Closure ( _, _) => unimplemented ! ( ) ,
322
- AggregateKind :: Generator ( _, _, _) => unimplemented ! ( ) ,
457
+ AggregateKind :: Generator ( _, _, _) => self . codegen_rvalue_generator ( & operands, res_ty) ,
323
458
}
324
459
}
325
460
@@ -406,7 +541,7 @@ impl<'tcx> GotocCtx<'tcx> {
406
541
self . codegen_get_discriminant ( place, pt, res_ty)
407
542
}
408
543
Rvalue :: Aggregate ( ref k, operands) => {
409
- self . codegen_rvalue_aggregate ( k, operands, res_ty)
544
+ self . codegen_rvalue_aggregate ( k, operands, res_ty, loc )
410
545
}
411
546
Rvalue :: ThreadLocalRef ( def_id) => {
412
547
// Since Kani is single-threaded, we treat a thread local like a static variable:
0 commit comments