Skip to content

Commit d230735

Browse files
authored
Fix issues and Update toolchain 10-26 (#2843)
Resolves issues caused by 1. rust-lang/rust#116958 2. rust-lang/rust#117103
1 parent 0941e3d commit d230735

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

42 files changed

+330
-324
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -383,7 +383,7 @@ impl<'tcx> GotocCtx<'tcx> {
383383
assert_eq!(
384384
fields[0].name().to_string(),
385385
"case",
386-
"Unexpected field in enum/generator. Please report your failing case at https://github.com/model-checking/kani/issues/1465"
386+
"Unexpected field in enum/coroutine. Please report your failing case at https://github.com/model-checking/kani/issues/1465"
387387
);
388388
Expr::struct_expr_with_nondet_fields(
389389
cgt,

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

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ use tracing::{debug, trace, warn};
2626
pub enum TypeOrVariant<'tcx> {
2727
Type(Ty<'tcx>),
2828
Variant(&'tcx VariantDef),
29-
GeneratorVariant(VariantIdx),
29+
CoroutineVariant(VariantIdx),
3030
}
3131

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

@@ -205,7 +205,7 @@ impl<'tcx> TypeOrVariant<'tcx> {
205205
pub fn monomorphize(self, ctx: &GotocCtx<'tcx>) -> Self {
206206
match self {
207207
TypeOrVariant::Type(t) => TypeOrVariant::Type(ctx.monomorphize(t)),
208-
TypeOrVariant::Variant(_) | TypeOrVariant::GeneratorVariant(_) => self,
208+
TypeOrVariant::Variant(_) | TypeOrVariant::CoroutineVariant(_) => self,
209209
}
210210
}
211211
}
@@ -215,8 +215,8 @@ impl<'tcx> TypeOrVariant<'tcx> {
215215
match self {
216216
TypeOrVariant::Type(t) => *t,
217217
TypeOrVariant::Variant(v) => panic!("expect a type but variant is found: {v:?}"),
218-
TypeOrVariant::GeneratorVariant(v) => {
219-
panic!("expect a type but generator variant is found: {v:?}")
218+
TypeOrVariant::CoroutineVariant(v) => {
219+
panic!("expect a type but coroutine variant is found: {v:?}")
220220
}
221221
}
222222
}
@@ -226,8 +226,8 @@ impl<'tcx> TypeOrVariant<'tcx> {
226226
match self {
227227
TypeOrVariant::Type(t) => panic!("expect a variant but type is found: {t:?}"),
228228
TypeOrVariant::Variant(v) => v,
229-
TypeOrVariant::GeneratorVariant(v) => {
230-
panic!("expect a variant but generator variant found {v:?}")
229+
TypeOrVariant::CoroutineVariant(v) => {
230+
panic!("expect a variant but coroutine variant found {v:?}")
231231
}
232232
}
233233
}
@@ -236,7 +236,7 @@ impl<'tcx> TypeOrVariant<'tcx> {
236236
impl<'tcx> GotocCtx<'tcx> {
237237
/// Codegen field access for types that allow direct field projection.
238238
///
239-
/// I.e.: Algebraic data types, closures, and generators.
239+
/// I.e.: Algebraic data types, closures, and coroutines.
240240
///
241241
/// Other composite types such as array only support index projection.
242242
fn codegen_field(
@@ -258,7 +258,7 @@ impl<'tcx> GotocCtx<'tcx> {
258258
| ty::FnPtr(_)
259259
| ty::Never
260260
| ty::FnDef(..)
261-
| ty::GeneratorWitness(..)
261+
| ty::CoroutineWitness(..)
262262
| ty::Foreign(..)
263263
| ty::Dynamic(..)
264264
| ty::Bound(..)
@@ -283,8 +283,8 @@ impl<'tcx> GotocCtx<'tcx> {
283283
ty::Closure(..) => {
284284
Ok(parent_expr.member(field.index().to_string(), &self.symbol_table))
285285
}
286-
ty::Generator(..) => {
287-
let field_name = self.generator_field_name(field.as_usize());
286+
ty::Coroutine(..) => {
287+
let field_name = self.coroutine_field_name(field.as_usize());
288288
Ok(parent_expr
289289
.member("direct_fields", &self.symbol_table)
290290
.member(field_name, &self.symbol_table))
@@ -301,8 +301,8 @@ impl<'tcx> GotocCtx<'tcx> {
301301
let field = &parent_var.fields[*field];
302302
Ok(parent_expr.member(field.name.to_string(), &self.symbol_table))
303303
}
304-
TypeOrVariant::GeneratorVariant(_var_idx) => {
305-
let field_name = self.generator_field_name(field.index());
304+
TypeOrVariant::CoroutineVariant(_var_idx) => {
305+
let field_name = self.coroutine_field_name(field.index());
306306
Ok(parent_expr.member(field_name, &self.symbol_table))
307307
}
308308
}
@@ -570,11 +570,11 @@ impl<'tcx> GotocCtx<'tcx> {
570570
let variant = def.variant(idx);
571571
(variant.name.as_str().into(), TypeOrVariant::Variant(variant))
572572
}
573-
ty::Generator(..) => {
574-
(self.generator_variant_name(idx), TypeOrVariant::GeneratorVariant(idx))
573+
ty::Coroutine(..) => {
574+
(self.coroutine_variant_name(idx), TypeOrVariant::CoroutineVariant(idx))
575575
}
576576
_ => unreachable!(
577-
"cannot downcast {:?} to a variant (only enums and generators can)",
577+
"cannot downcast {:?} to a variant (only enums and coroutines can)",
578578
&t.kind()
579579
),
580580
};
@@ -583,7 +583,7 @@ impl<'tcx> GotocCtx<'tcx> {
583583
Variants::Single { .. } => before.goto_expr,
584584
Variants::Multiple { tag_encoding, .. } => match tag_encoding {
585585
TagEncoding::Direct => {
586-
let cases = if t.is_generator() {
586+
let cases = if t.is_coroutine() {
587587
before.goto_expr
588588
} else {
589589
before.goto_expr.member("cases", &self.symbol_table)

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -498,8 +498,8 @@ impl<'tcx> GotocCtx<'tcx> {
498498
}
499499
}
500500

501-
/// Create an initializer for a generator struct.
502-
fn codegen_rvalue_generator(
501+
/// Create an initializer for a coroutine struct.
502+
fn codegen_rvalue_coroutine(
503503
&mut self,
504504
operands: &IndexVec<FieldIdx, Operand<'tcx>>,
505505
ty: Ty<'tcx>,
@@ -508,7 +508,7 @@ impl<'tcx> GotocCtx<'tcx> {
508508
let discriminant_field = match &layout.variants {
509509
Variants::Multiple { tag_encoding: TagEncoding::Direct, tag_field, .. } => tag_field,
510510
_ => unreachable!(
511-
"Expected generators to have multiple variants and direct encoding, but found: {layout:?}"
511+
"Expected coroutines to have multiple variants and direct encoding, but found: {layout:?}"
512512
),
513513
};
514514
let overall_t = self.codegen_ty(ty);
@@ -664,7 +664,7 @@ impl<'tcx> GotocCtx<'tcx> {
664664
&self.symbol_table,
665665
)
666666
}
667-
AggregateKind::Generator(_, _, _) => self.codegen_rvalue_generator(&operands, res_ty),
667+
AggregateKind::Coroutine(_, _, _) => self.codegen_rvalue_coroutine(&operands, res_ty),
668668
}
669669
}
670670

@@ -784,8 +784,8 @@ impl<'tcx> GotocCtx<'tcx> {
784784
),
785785
"discriminant field (`case`) only exists for multiple variants and direct encoding"
786786
);
787-
let expr = if ty.is_generator() {
788-
// Generators are translated somewhat differently from enums (see [`GotoCtx::codegen_ty_generator`]).
787+
let expr = if ty.is_coroutine() {
788+
// Coroutines are translated somewhat differently from enums (see [`GotoCtx::codegen_ty_coroutine`]).
789789
// As a consequence, the discriminant is accessed as `.direct_fields.case` instead of just `.case`.
790790
place.member("direct_fields", &self.symbol_table)
791791
} else {

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -195,7 +195,7 @@ impl<'tcx> GotocCtx<'tcx> {
195195
TerminatorKind::FalseEdge { .. } | TerminatorKind::FalseUnwind { .. } => {
196196
unreachable!("drop elaboration removes these TerminatorKind")
197197
}
198-
TerminatorKind::Yield { .. } | TerminatorKind::GeneratorDrop => {
198+
TerminatorKind::Yield { .. } | TerminatorKind::CoroutineDrop => {
199199
unreachable!("we should not hit these cases") // why?
200200
}
201201
TerminatorKind::InlineAsm { .. } => self.codegen_unimplemented_stmt(

0 commit comments

Comments
 (0)