Skip to content

Commit

Permalink
Fix issues and Update toolchain 10-26 (#2843)
Browse files Browse the repository at this point in the history
Resolves issues caused by
1. rust-lang/rust#116958
2. rust-lang/rust#117103
  • Loading branch information
jaisnan committed Oct 31, 2023
1 parent 0941e3d commit d230735
Show file tree
Hide file tree
Showing 42 changed files with 330 additions and 324 deletions.
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
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
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
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
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

0 comments on commit d230735

Please sign in to comment.