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

Jump to bottom

Fix issues and Update toolchain 10-26 #2843

Merged
merged 5 commits into from
Oct 31, 2023
Merged

Fix issues and Update toolchain 10-26 #2843

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
4d68b45
Rename Generators to Coroutines
jaisnan Oct 27, 2023
dce6524
Fix printer rustc change
jaisnan Oct 27, 2023
a025bc9
Merge branch 'main' into Update-toolchain-10-25
jaisnan Oct 27, 2023
4dfc327
update w/ clippy recommendation
jaisnan Oct 27, 2023
9eeb624
Merge branch 'main' into Update-toolchain-10-25
jaisnan Oct 31, 2023
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
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 @@ -383,7 +383,7 @@ impl<'tcx> GotocCtx<'tcx> {
assert_eq!(
fields[0].name().to_string(),
"case",
"Unexpected field in enum/generator. Please report your failing case at https://github.com/model-checking/kani/issues/1465"
"Unexpected field in enum/coroutine. Please report your failing case at https://github.com/model-checking/kani/issues/1465"
);
Expr::struct_expr_with_nondet_fields(
cgt,
Expand Down
34 changes: 17 additions & 17 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 @@ -26,7 +26,7 @@ use tracing::{debug, trace, warn};
pub enum TypeOrVariant<'tcx> {
Type(Ty<'tcx>),
Variant(&'tcx VariantDef),
GeneratorVariant(VariantIdx),
CoroutineVariant(VariantIdx),
}

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

Expand Down Expand Up @@ -205,7 +205,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(_) | TypeOrVariant::GeneratorVariant(_) => self,
TypeOrVariant::Variant(_) | TypeOrVariant::CoroutineVariant(_) => self,
}
}
}
Expand All @@ -215,8 +215,8 @@ 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:?}")
TypeOrVariant::CoroutineVariant(v) => {
panic!("expect a type but coroutine variant is found: {v:?}")
}
}
}
Expand All @@ -226,8 +226,8 @@ 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:?}")
TypeOrVariant::CoroutineVariant(v) => {
panic!("expect a variant but coroutine variant found {v:?}")
}
}
}
Expand All @@ -236,7 +236,7 @@ impl<'tcx> TypeOrVariant<'tcx> {
impl<'tcx> GotocCtx<'tcx> {
/// Codegen field access for types that allow direct field projection.
///
/// I.e.: Algebraic data types, closures, and generators.
/// I.e.: Algebraic data types, closures, and coroutines.
///
/// Other composite types such as array only support index projection.
fn codegen_field(
Expand All @@ -258,7 +258,7 @@ impl<'tcx> GotocCtx<'tcx> {
| ty::FnPtr(_)
| ty::Never
| ty::FnDef(..)
| ty::GeneratorWitness(..)
| ty::CoroutineWitness(..)
| ty::Foreign(..)
| ty::Dynamic(..)
| ty::Bound(..)
Expand All @@ -283,8 +283,8 @@ impl<'tcx> GotocCtx<'tcx> {
ty::Closure(..) => {
Ok(parent_expr.member(field.index().to_string(), &self.symbol_table))
}
ty::Generator(..) => {
let field_name = self.generator_field_name(field.as_usize());
ty::Coroutine(..) => {
let field_name = self.coroutine_field_name(field.as_usize());
Ok(parent_expr
.member("direct_fields", &self.symbol_table)
.member(field_name, &self.symbol_table))
Expand All @@ -301,8 +301,8 @@ impl<'tcx> GotocCtx<'tcx> {
let field = &parent_var.fields[*field];
Ok(parent_expr.member(field.name.to_string(), &self.symbol_table))
}
TypeOrVariant::GeneratorVariant(_var_idx) => {
let field_name = self.generator_field_name(field.index());
TypeOrVariant::CoroutineVariant(_var_idx) => {
let field_name = self.coroutine_field_name(field.index());
Ok(parent_expr.member(field_name, &self.symbol_table))
}
}
Expand Down Expand Up @@ -570,11 +570,11 @@ impl<'tcx> GotocCtx<'tcx> {
let variant = def.variant(idx);
(variant.name.as_str().into(), TypeOrVariant::Variant(variant))
}
ty::Generator(..) => {
(self.generator_variant_name(idx), TypeOrVariant::GeneratorVariant(idx))
ty::Coroutine(..) => {
(self.coroutine_variant_name(idx), TypeOrVariant::CoroutineVariant(idx))
}
_ => unreachable!(
"cannot downcast {:?} to a variant (only enums and generators can)",
"cannot downcast {:?} to a variant (only enums and coroutines can)",
&t.kind()
),
};
Expand All @@ -583,7 +583,7 @@ impl<'tcx> GotocCtx<'tcx> {
Variants::Single { .. } => before.goto_expr,
Variants::Multiple { tag_encoding, .. } => match tag_encoding {
TagEncoding::Direct => {
let cases = if t.is_generator() {
let cases = if t.is_coroutine() {
before.goto_expr
} else {
before.goto_expr.member("cases", &self.symbol_table)
Expand Down
12 changes: 6 additions & 6 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 @@ -498,8 +498,8 @@ impl<'tcx> GotocCtx<'tcx> {
}
}

/// Create an initializer for a generator struct.
fn codegen_rvalue_generator(
/// Create an initializer for a coroutine struct.
fn codegen_rvalue_coroutine(
&mut self,
operands: &IndexVec<FieldIdx, Operand<'tcx>>,
ty: Ty<'tcx>,
Expand All @@ -508,7 +508,7 @@ impl<'tcx> GotocCtx<'tcx> {
let discriminant_field = match &layout.variants {
Variants::Multiple { tag_encoding: TagEncoding::Direct, tag_field, .. } => tag_field,
_ => unreachable!(
"Expected generators to have multiple variants and direct encoding, but found: {layout:?}"
"Expected coroutines to have multiple variants and direct encoding, but found: {layout:?}"
),
};
let overall_t = self.codegen_ty(ty);
Expand Down Expand Up @@ -664,7 +664,7 @@ impl<'tcx> GotocCtx<'tcx> {
&self.symbol_table,
)
}
AggregateKind::Generator(_, _, _) => self.codegen_rvalue_generator(&operands, res_ty),
AggregateKind::Coroutine(_, _, _) => self.codegen_rvalue_coroutine(&operands, res_ty),
}
}

Expand Down Expand Up @@ -784,8 +784,8 @@ impl<'tcx> GotocCtx<'tcx> {
),
"discriminant field (`case`) only exists for multiple variants and direct encoding"
);
let expr = if ty.is_generator() {
// Generators are translated somewhat differently from enums (see [`GotoCtx::codegen_ty_generator`]).
let expr = if ty.is_coroutine() {
// Coroutines are translated somewhat differently from enums (see [`GotoCtx::codegen_ty_coroutine`]).
// As a consequence, the discriminant is accessed as `.direct_fields.case` instead of just `.case`.
place.member("direct_fields", &self.symbol_table)
} else {
Expand Down
2 changes: 1 addition & 1 deletion 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 @@ -195,7 +195,7 @@ impl<'tcx> GotocCtx<'tcx> {
TerminatorKind::FalseEdge { .. } | TerminatorKind::FalseUnwind { .. } => {
unreachable!("drop elaboration removes these TerminatorKind")
}
TerminatorKind::Yield { .. } | TerminatorKind::GeneratorDrop => {
TerminatorKind::Yield { .. } | TerminatorKind::CoroutineDrop => {
unreachable!("we should not hit these cases") // why?
}
TerminatorKind::InlineAsm { .. } => self.codegen_unimplemented_stmt(
Expand Down
Loading
Loading