Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement support for generators #1378

Merged
merged 21 commits into from
Jul 25, 2022
Merged

Implement support for generators #1378

Show file tree
Hide file tree
Changes from 12 commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
ac34884
Implement support for generators
fzaiser Jul 14, 2022
798af91
Fix tests
fzaiser Jul 14, 2022
9ca6263
Fix generator codegen (different approach than enums)
fzaiser Jul 18, 2022
f8c06bb
Add tests (mostly taken from rustc)
fzaiser Jul 18, 2022
229cf4d
Fix copyright headers
fzaiser Jul 18, 2022
b9838c0
Merge branch 'main' into generators
fzaiser Jul 18, 2022
1443b5c
Small code simplification
fzaiser Jul 18, 2022
ca0c21f
Merge branch 'generators' of https://github.com/fzaiser/kani into gen…
fzaiser Jul 18, 2022
1cabf67
Refactor: remove unnecessary Option
fzaiser Jul 19, 2022
3005cca
Update comments
fzaiser Jul 19, 2022
f818b34
Merge branch 'main' into generators
fzaiser Jul 19, 2022
e269f4f
Fix merge issue
fzaiser Jul 19, 2022
1826b5b
Address reviewer comments
fzaiser Jul 20, 2022
dd728ec
Merge branch 'main' into generators
fzaiser Jul 20, 2022
db2263c
Fix comment test
fzaiser Jul 20, 2022
72d5d10
Improve tests
fzaiser Jul 20, 2022
de87147
Merge branch 'main' into generators
fzaiser Jul 20, 2022
64f7af1
Address reviewer comments
fzaiser Jul 20, 2022
88eaf1f
Check generator layout assumption only in one place
fzaiser Jul 25, 2022
daecbbf
Merge branch 'main' into generators
fzaiser Jul 25, 2022
5864e9f
Make size_of or align_of fail for generators (because they are curren…
fzaiser Jul 25, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,7 @@ impl<'tcx> GotocCtx<'tcx> {
/// Get the number of parameters that the current function expects.
fn get_params_size(&self) -> usize {
let sig = self.current_fn().sig();
let sig =
self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig.unwrap());
let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig);
// we don't call [codegen_function_sig] because we want to get a bit more metainformation.
sig.inputs().len()
}
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -634,7 +634,7 @@ impl<'tcx> GotocCtx<'tcx> {
/// This is tracked in <https://github.com/model-checking/kani/issues/1350>.
pub fn codegen_func_symbol(&mut self, instance: Instance<'tcx>) -> (&Symbol, Type) {
let func = self.symbol_name(instance);
let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance).unwrap());
let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance));
// make sure the functions imported from other modules are in the symbol table
let sym = self.ensure(&func, |ctx, _| {
Symbol::function(
Expand Down
86 changes: 52 additions & 34 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ use rustc_middle::{
mir::{Field, Local, Place, ProjectionElem},
ty::{self, Ty, TypeAndMut, VariantDef},
};
use rustc_target::abi::{TagEncoding, Variants};
use rustc_target::abi::{TagEncoding, VariantIdx, Variants};
use tracing::{debug, trace, warn};

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

/// A struct for storing the data for passing to `codegen_unimplemented`
Expand Down Expand Up @@ -129,7 +130,7 @@ impl<'tcx> ProjectedPlace<'tcx> {
}
}
// TODO: handle Variant https://github.com/model-checking/kani/issues/448
TypeOrVariant::Variant(_) => None,
TypeOrVariant::Variant(_) | TypeOrVariant::GeneratorVariant(_) => None,
fzaiser marked this conversation as resolved.
Show resolved Hide resolved
}
}

Expand Down Expand Up @@ -197,7 +198,7 @@ impl<'tcx> TypeOrVariant<'tcx> {
pub fn monomorphize(self, ctx: &GotocCtx<'tcx>) -> Self {
match self {
TypeOrVariant::Type(t) => TypeOrVariant::Type(ctx.monomorphize(t)),
TypeOrVariant::Variant(_) => self,
TypeOrVariant::Variant(_) | TypeOrVariant::GeneratorVariant(_) => self,
}
}
}
Expand All @@ -207,6 +208,9 @@ impl<'tcx> TypeOrVariant<'tcx> {
match self {
TypeOrVariant::Type(t) => *t,
TypeOrVariant::Variant(v) => panic!("expect a type but variant is found: {:?}", v),
TypeOrVariant::GeneratorVariant(v) => {
panic!("expect a type but generator variant is found: {:?}", v)
}
}
}

Expand All @@ -215,6 +219,9 @@ impl<'tcx> TypeOrVariant<'tcx> {
match self {
TypeOrVariant::Type(t) => panic!("expect a variant but type is found: {:?}", t),
TypeOrVariant::Variant(v) => v,
TypeOrVariant::GeneratorVariant(v) => {
panic!("expect a variant but generator variant found {:?}", v)
}
}
}
}
Expand Down Expand Up @@ -269,12 +276,12 @@ impl<'tcx> GotocCtx<'tcx> {
Ok(res.member(&field.name.to_string(), &self.symbol_table))
}
ty::Closure(..) => Ok(res.member(&f.index().to_string(), &self.symbol_table)),
ty::Generator(..) => Err(UnimplementedData::new(
"ty::Generator",
"https://github.com/model-checking/kani/issues/416",
Type::code(vec![], Type::empty()),
*res.location(),
)),
ty::Generator(..) => {
let field_name = self.generator_field_name(f.index().into());
Ok(res
.member("direct_fields", &self.symbol_table)
fzaiser marked this conversation as resolved.
Show resolved Hide resolved
.member(field_name, &self.symbol_table))
}
_ => unimplemented!(),
}
}
Expand All @@ -283,6 +290,10 @@ impl<'tcx> GotocCtx<'tcx> {
let field = &v.fields[f.index()];
Ok(res.member(&field.name.to_string(), &self.symbol_table))
}
TypeOrVariant::GeneratorVariant(_var_idx) => {
let field_name = self.generator_field_name(f.index().into());
Ok(res.member(field_name, &self.symbol_table))
}
}
}

Expand Down Expand Up @@ -498,33 +509,40 @@ impl<'tcx> GotocCtx<'tcx> {
ProjectionElem::Downcast(_, idx) => {
// downcast converts a variable of an enum type to one of its discriminated cases
let t = before.mir_typ();
match t.kind() {
let (case_name, type_or_variant) = match t.kind() {
ty::Adt(def, _) => {
let variant = def.variants().get(idx).unwrap();
let case_name = variant.name.to_string();
let typ = TypeOrVariant::Variant(variant);
let expr = match &self.layout_of(t).variants {
Variants::Single { .. } => before.goto_expr,
Variants::Multiple { tag_encoding, .. } => match tag_encoding {
TagEncoding::Direct => before
.goto_expr
.member("cases", &self.symbol_table)
.member(&case_name, &self.symbol_table),
TagEncoding::Niche { .. } => {
before.goto_expr.member(&case_name, &self.symbol_table)
}
},
};
ProjectedPlace::try_new(
expr,
typ,
before.fat_ptr_goto_expr,
before.fat_ptr_mir_typ,
self,
)
let variant = def.variant(idx);
(variant.name.as_str().into(), TypeOrVariant::Variant(variant))
}
_ => unreachable!("it's a bug to reach here!"),
}
ty::Generator(..) => {
(self.generator_variant_name(idx), TypeOrVariant::GeneratorVariant(idx))
}
_ => unreachable!("it's a bug to reach here! {:?}", &t.kind()),
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ error message could be more informative

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Improved

};
let layout = self.layout_of(t);
let expr = match &layout.variants {
fzaiser marked this conversation as resolved.
Show resolved Hide resolved
Variants::Single { .. } => before.goto_expr,
Variants::Multiple { tag_encoding, .. } => match tag_encoding {
TagEncoding::Direct => {
let cases = if t.is_generator() {
before.goto_expr
} else {
before.goto_expr.member("cases", &self.symbol_table)
};
cases.member(case_name, &self.symbol_table)
}
TagEncoding::Niche { .. } => {
before.goto_expr.member(case_name, &self.symbol_table)
}
},
};
ProjectedPlace::try_new(
expr,
type_or_variant,
before.fat_ptr_goto_expr,
before.fat_ptr_mir_typ,
self,
)
}
}
}
Expand Down
5 changes: 5 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -510,6 +510,11 @@ impl<'tcx> GotocCtx<'tcx> {
}
Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding {
TagEncoding::Direct => {
let e = if ty.is_generator() {
fzaiser marked this conversation as resolved.
Show resolved Hide resolved
e.member("direct_fields", &&self.symbol_table)
fzaiser marked this conversation as resolved.
Show resolved Hide resolved
} else {
e
};
e.member("case", &self.symbol_table).cast_to(self.codegen_ty(res_ty))
}
TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
Expand Down
45 changes: 17 additions & 28 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ impl<'tcx> GotocCtx<'tcx> {
loc,
),
TerminatorKind::Return => {
let rty = self.current_fn().sig().unwrap().skip_binder().output();
let rty = self.current_fn().sig().skip_binder().output();
if rty.is_unit() {
self.codegen_ret_unit()
} else {
Expand Down Expand Up @@ -358,14 +358,12 @@ impl<'tcx> GotocCtx<'tcx> {

pub fn codegen_funcall_args(&mut self, args: &[Operand<'tcx>]) -> Vec<Expr> {
args.iter()
.filter_map(|o| {
.map(|o| {
let ot = self.operand_ty(o);
if self.ignore_var_ty(ot) {
None
} else if ot.is_bool() {
Some(self.codegen_operand(o).cast_to(Type::c_bool()))
if ot.is_bool() {
fzaiser marked this conversation as resolved.
Show resolved Hide resolved
self.codegen_operand(o).cast_to(Type::c_bool())
} else {
Some(self.codegen_operand(o))
self.codegen_operand(o)
}
})
.collect()
Expand Down Expand Up @@ -653,8 +651,6 @@ impl<'tcx> GotocCtx<'tcx> {
let layout = self.layout_of(dst_mir_ty);
if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 {
// We ignore assignment for all zero size types
// Ignore generators too for now:
// https://github.com/model-checking/kani/issues/416
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe this comment was outdated because the if condition only checks for ZST.

Stmt::skip(location)
} else {
unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place))
Expand All @@ -665,26 +661,13 @@ impl<'tcx> GotocCtx<'tcx> {
StatementKind::SetDiscriminant { place, variant_index } => {
// this requires place points to an enum type.
let pt = self.place_ty(place);
let (def, _) = match pt.kind() {
ty::Adt(def, substs) => (def, substs),
ty::Generator(..) => {
return self
.codegen_unimplemented(
"ty::Generator",
Type::code(vec![], Type::empty()),
location,
"https://github.com/model-checking/kani/issues/416",
)
.as_stmt(location);
}
_ => unreachable!(),
};
let layout = self.layout_of(pt);
match &layout.variants {
Variants::Single { .. } => Stmt::skip(location),
Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding {
TagEncoding::Direct => {
let discr = def.discriminant_for_variant(self.tcx, *variant_index);
let discr =
pt.discriminant_for_variant(self.tcx, *variant_index).unwrap();
fzaiser marked this conversation as resolved.
Show resolved Hide resolved
let discr_t = self.codegen_enum_discr_typ(pt);
// The constant created below may not fit into the type.
// https://github.com/model-checking/kani/issues/996
Expand All @@ -699,13 +682,19 @@ impl<'tcx> GotocCtx<'tcx> {
// DISCRIMINANT - val:0 ty:i8
// DISCRIMINANT - val:1 ty:i8
let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t));
unwrap_or_return_codegen_unimplemented_stmt!(
let place_goto_expr = unwrap_or_return_codegen_unimplemented_stmt!(
self,
self.codegen_place(place)
)
.goto_expr
.member("case", &self.symbol_table)
.assign(discr, location)
.goto_expr;
let place_goto_expr = if pt.is_generator() {
place_goto_expr.member("direct_fields", &self.symbol_table)
} else {
place_goto_expr
};
fzaiser marked this conversation as resolved.
Show resolved Hide resolved
place_goto_expr
.member("case", &self.symbol_table)
.assign(discr, location)
}
TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
if dataful_variant != variant_index {
Expand Down
Loading