Skip to content

Commit c4ddf6c

Browse files
fzaiserfzaiser
authored
Implement support for generators (#1378)
1 parent a06136b commit c4ddf6c

36 files changed

+1800
-213
lines changed

‎kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

+1-2
Original file line numberDiff line numberDiff line change
@@ -44,8 +44,7 @@ impl<'tcx> GotocCtx<'tcx> {
4444
/// Get the number of parameters that the current function expects.
4545
fn get_params_size(&self) -> usize {
4646
let sig = self.current_fn().sig();
47-
let sig =
48-
self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig.unwrap());
47+
let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig);
4948
// we don't call [codegen_function_sig] because we want to get a bit more metainformation.
5049
sig.inputs().len()
5150
}

‎kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

+13-3
Original file line numberDiff line numberDiff line change
@@ -313,9 +313,19 @@ impl<'tcx> GotocCtx<'tcx> {
313313
macro_rules! codegen_size_align {
314314
($which: ident) => {{
315315
let tp_ty = instance.substs.type_at(0);
316-
let arg = fargs.remove(0);
317-
let size_align = self.size_and_align_of_dst(tp_ty, arg);
318-
self.codegen_expr_to_place(p, size_align.$which)
316+
if tp_ty.is_generator() {
317+
let e = self.codegen_unimplemented(
318+
"size or alignment of a generator type",
319+
cbmc_ret_ty,
320+
loc,
321+
"https://github.com/model-checking/kani/issues/1395",
322+
);
323+
self.codegen_expr_to_place(p, e)
324+
} else {
325+
let arg = fargs.remove(0);
326+
let size_align = self.size_and_align_of_dst(tp_ty, arg);
327+
self.codegen_expr_to_place(p, size_align.$which)
328+
}
319329
}};
320330
}
321331

‎kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

+2-3
Original file line numberDiff line numberDiff line change
@@ -331,8 +331,7 @@ impl<'tcx> GotocCtx<'tcx> {
331331
let var = tcx.gen_function_local_variable(2, &func_name, cgt.clone()).to_expr();
332332
let body = vec![
333333
Stmt::decl(var.clone(), None, Location::none()),
334-
var.clone()
335-
.member("case", &tcx.symbol_table)
334+
tcx.codegen_discriminant_field(var.clone(), ty)
336335
.assign(param.to_expr(), Location::none()),
337336
var.ret(Location::none()),
338337
];
@@ -641,7 +640,7 @@ impl<'tcx> GotocCtx<'tcx> {
641640
/// This is tracked in <https://github.com/model-checking/kani/issues/1350>.
642641
pub fn codegen_func_symbol(&mut self, instance: Instance<'tcx>) -> (&Symbol, Type) {
643642
let func = self.symbol_name(instance);
644-
let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance).unwrap());
643+
let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance));
645644
// make sure the functions imported from other modules are in the symbol table
646645
let sym = self.ensure(&func, |ctx, _| {
647646
Symbol::function(

‎kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

+55-34
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ use rustc_middle::{
1515
mir::{Field, Local, Place, ProjectionElem},
1616
ty::{self, Ty, TypeAndMut, VariantDef},
1717
};
18-
use rustc_target::abi::{TagEncoding, Variants};
18+
use rustc_target::abi::{TagEncoding, VariantIdx, Variants};
1919
use tracing::{debug, trace, warn};
2020

2121
/// A projection in Kani can either be to a type (the normal case),
@@ -24,6 +24,7 @@ use tracing::{debug, trace, warn};
2424
pub enum TypeOrVariant<'tcx> {
2525
Type(Ty<'tcx>),
2626
Variant(&'tcx VariantDef),
27+
GeneratorVariant(VariantIdx),
2728
}
2829

2930
/// A struct for storing the data for passing to `codegen_unimplemented`
@@ -129,7 +130,7 @@ impl<'tcx> ProjectedPlace<'tcx> {
129130
}
130131
}
131132
// TODO: handle Variant https://github.com/model-checking/kani/issues/448
132-
TypeOrVariant::Variant(_) => None,
133+
TypeOrVariant::Variant(_) | TypeOrVariant::GeneratorVariant(_) => None,
133134
}
134135
}
135136

@@ -197,7 +198,7 @@ impl<'tcx> TypeOrVariant<'tcx> {
197198
pub fn monomorphize(self, ctx: &GotocCtx<'tcx>) -> Self {
198199
match self {
199200
TypeOrVariant::Type(t) => TypeOrVariant::Type(ctx.monomorphize(t)),
200-
TypeOrVariant::Variant(_) => self,
201+
TypeOrVariant::Variant(_) | TypeOrVariant::GeneratorVariant(_) => self,
201202
}
202203
}
203204
}
@@ -207,6 +208,9 @@ impl<'tcx> TypeOrVariant<'tcx> {
207208
match self {
208209
TypeOrVariant::Type(t) => *t,
209210
TypeOrVariant::Variant(v) => panic!("expect a type but variant is found: {:?}", v),
211+
TypeOrVariant::GeneratorVariant(v) => {
212+
panic!("expect a type but generator variant is found: {:?}", v)
213+
}
210214
}
211215
}
212216

@@ -215,6 +219,9 @@ impl<'tcx> TypeOrVariant<'tcx> {
215219
match self {
216220
TypeOrVariant::Type(t) => panic!("expect a variant but type is found: {:?}", t),
217221
TypeOrVariant::Variant(v) => v,
222+
TypeOrVariant::GeneratorVariant(v) => {
223+
panic!("expect a variant but generator variant found {:?}", v)
224+
}
218225
}
219226
}
220227
}
@@ -269,12 +276,12 @@ impl<'tcx> GotocCtx<'tcx> {
269276
Ok(res.member(&field.name.to_string(), &self.symbol_table))
270277
}
271278
ty::Closure(..) => Ok(res.member(&f.index().to_string(), &self.symbol_table)),
272-
ty::Generator(..) => Err(UnimplementedData::new(
273-
"ty::Generator",
274-
"https://github.com/model-checking/kani/issues/416",
275-
Type::code(vec![], Type::empty()),
276-
*res.location(),
277-
)),
279+
ty::Generator(..) => {
280+
let field_name = self.generator_field_name(f.index().into());
281+
Ok(res
282+
.member("direct_fields", &self.symbol_table)
283+
.member(field_name, &self.symbol_table))
284+
}
278285
_ => unimplemented!(),
279286
}
280287
}
@@ -283,6 +290,10 @@ impl<'tcx> GotocCtx<'tcx> {
283290
let field = &v.fields[f.index()];
284291
Ok(res.member(&field.name.to_string(), &self.symbol_table))
285292
}
293+
TypeOrVariant::GeneratorVariant(_var_idx) => {
294+
let field_name = self.generator_field_name(f.index().into());
295+
Ok(res.member(field_name, &self.symbol_table))
296+
}
286297
}
287298
}
288299

@@ -498,33 +509,43 @@ impl<'tcx> GotocCtx<'tcx> {
498509
ProjectionElem::Downcast(_, idx) => {
499510
// downcast converts a variable of an enum type to one of its discriminated cases
500511
let t = before.mir_typ();
501-
match t.kind() {
512+
let (case_name, type_or_variant) = match t.kind() {
502513
ty::Adt(def, _) => {
503-
let variant = def.variants().get(idx).unwrap();
504-
let case_name = variant.name.to_string();
505-
let typ = TypeOrVariant::Variant(variant);
506-
let expr = match &self.layout_of(t).variants {
507-
Variants::Single { .. } => before.goto_expr,
508-
Variants::Multiple { tag_encoding, .. } => match tag_encoding {
509-
TagEncoding::Direct => before
510-
.goto_expr
511-
.member("cases", &self.symbol_table)
512-
.member(&case_name, &self.symbol_table),
513-
TagEncoding::Niche { .. } => {
514-
before.goto_expr.member(&case_name, &self.symbol_table)
515-
}
516-
},
517-
};
518-
ProjectedPlace::try_new(
519-
expr,
520-
typ,
521-
before.fat_ptr_goto_expr,
522-
before.fat_ptr_mir_typ,
523-
self,
524-
)
514+
let variant = def.variant(idx);
515+
(variant.name.as_str().into(), TypeOrVariant::Variant(variant))
525516
}
526-
_ => unreachable!("it's a bug to reach here!"),
527-
}
517+
ty::Generator(..) => {
518+
(self.generator_variant_name(idx), TypeOrVariant::GeneratorVariant(idx))
519+
}
520+
_ => unreachable!(
521+
"cannot downcast {:?} to a variant (only enums and generators can)",
522+
&t.kind()
523+
),
524+
};
525+
let layout = self.layout_of(t);
526+
let expr = match &layout.variants {
527+
Variants::Single { .. } => before.goto_expr,
528+
Variants::Multiple { tag_encoding, .. } => match tag_encoding {
529+
TagEncoding::Direct => {
530+
let cases = if t.is_generator() {
531+
before.goto_expr
532+
} else {
533+
before.goto_expr.member("cases", &self.symbol_table)
534+
};
535+
cases.member(case_name, &self.symbol_table)
536+
}
537+
TagEncoding::Niche { .. } => {
538+
before.goto_expr.member(case_name, &self.symbol_table)
539+
}
540+
},
541+
};
542+
ProjectedPlace::try_new(
543+
expr,
544+
type_or_variant,
545+
before.fat_ptr_goto_expr,
546+
before.fat_ptr_mir_typ,
547+
self,
548+
)
528549
}
529550
ProjectionElem::OpaqueCast(ty) => ProjectedPlace::try_new(
530551
before.goto_expr.cast_to(self.codegen_ty(ty)),

‎kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

+20-1
Original file line numberDiff line numberDiff line change
@@ -502,6 +502,25 @@ impl<'tcx> GotocCtx<'tcx> {
502502
}
503503
}
504504

505+
pub fn codegen_discriminant_field(&self, place: Expr, ty: Ty<'tcx>) -> Expr {
506+
let layout = self.layout_of(ty);
507+
assert!(
508+
matches!(
509+
&layout.variants,
510+
Variants::Multiple { tag_encoding: TagEncoding::Direct, .. }
511+
),
512+
"discriminant field (`case`) only exists for multiple variants and direct encoding"
513+
);
514+
let expr = if ty.is_generator() {
515+
// Generators are translated somewhat differently from enums (see [`GotoCtx::codegen_ty_generator`]).
516+
// As a consequence, the discriminant is accessed as `.direct_fields.case` instead of just `.case`.
517+
place.member("direct_fields", &self.symbol_table)
518+
} else {
519+
place
520+
};
521+
expr.member("case", &self.symbol_table)
522+
}
523+
505524
/// e: ty
506525
/// get the discriminant of e, of type res_ty
507526
pub fn codegen_get_discriminant(&mut self, e: Expr, ty: Ty<'tcx>, res_ty: Ty<'tcx>) -> Expr {
@@ -516,7 +535,7 @@ impl<'tcx> GotocCtx<'tcx> {
516535
}
517536
Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding {
518537
TagEncoding::Direct => {
519-
e.member("case", &self.symbol_table).cast_to(self.codegen_ty(res_ty))
538+
self.codegen_discriminant_field(e, ty).cast_to(self.codegen_ty(res_ty))
520539
}
521540
TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
522541
// This code follows the logic in the cranelift codegen backend:

‎kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

+11-30
Original file line numberDiff line numberDiff line change
@@ -65,8 +65,6 @@ impl<'tcx> GotocCtx<'tcx> {
6565
let layout = self.layout_of(dst_mir_ty);
6666
if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 {
6767
// We ignore assignment for all zero size types
68-
// Ignore generators too for now:
69-
// https://github.com/model-checking/kani/issues/416
7068
Stmt::skip(location)
7169
} else {
7270
unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place))
@@ -77,26 +75,13 @@ impl<'tcx> GotocCtx<'tcx> {
7775
StatementKind::SetDiscriminant { place, variant_index } => {
7876
// this requires place points to an enum type.
7977
let pt = self.place_ty(place);
80-
let (def, _) = match pt.kind() {
81-
ty::Adt(def, substs) => (def, substs),
82-
ty::Generator(..) => {
83-
return self
84-
.codegen_unimplemented(
85-
"ty::Generator",
86-
Type::code(vec![], Type::empty()),
87-
location,
88-
"https://github.com/model-checking/kani/issues/416",
89-
)
90-
.as_stmt(location);
91-
}
92-
_ => unreachable!(),
93-
};
9478
let layout = self.layout_of(pt);
9579
match &layout.variants {
9680
Variants::Single { .. } => Stmt::skip(location),
9781
Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding {
9882
TagEncoding::Direct => {
99-
let discr = def.discriminant_for_variant(self.tcx, *variant_index);
83+
let discr =
84+
pt.discriminant_for_variant(self.tcx, *variant_index).unwrap();
10085
let discr_t = self.codegen_enum_discr_typ(pt);
10186
// The constant created below may not fit into the type.
10287
// https://github.com/model-checking/kani/issues/996
@@ -111,13 +96,13 @@ impl<'tcx> GotocCtx<'tcx> {
11196
// DISCRIMINANT - val:0 ty:i8
11297
// DISCRIMINANT - val:1 ty:i8
11398
let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t));
114-
unwrap_or_return_codegen_unimplemented_stmt!(
99+
let place_goto_expr = unwrap_or_return_codegen_unimplemented_stmt!(
115100
self,
116101
self.codegen_place(place)
117102
)
118-
.goto_expr
119-
.member("case", &self.symbol_table)
120-
.assign(discr, location)
103+
.goto_expr;
104+
self.codegen_discriminant_field(place_goto_expr, pt)
105+
.assign(discr, location)
121106
}
122107
TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
123108
if dataful_variant != variant_index {
@@ -206,7 +191,7 @@ impl<'tcx> GotocCtx<'tcx> {
206191
loc,
207192
),
208193
TerminatorKind::Return => {
209-
let rty = self.current_fn().sig().unwrap().skip_binder().output();
194+
let rty = self.current_fn().sig().skip_binder().output();
210195
if rty.is_unit() {
211196
self.codegen_ret_unit()
212197
} else {
@@ -534,15 +519,11 @@ impl<'tcx> GotocCtx<'tcx> {
534519
/// N.B. public only because instrinsics use this directly, too.
535520
pub(crate) fn codegen_funcall_args(&mut self, args: &[Operand<'tcx>]) -> Vec<Expr> {
536521
args.iter()
537-
.filter_map(|o| {
538-
let ot = self.operand_ty(o);
539-
if self.ignore_var_ty(ot) {
540-
trace!(operand=?o, typ=?ot, "codegen_funcall_args ignore");
541-
None
542-
} else if ot.is_bool() {
543-
Some(self.codegen_operand(o).cast_to(Type::c_bool()))
522+
.map(|o| {
523+
if self.operand_ty(o).is_bool() {
524+
self.codegen_operand(o).cast_to(Type::c_bool())
544525
} else {
545-
Some(self.codegen_operand(o))
526+
self.codegen_operand(o)
546527
}
547528
})
548529
.collect()

0 commit comments

Comments
 (0)