Skip to content

Commit dce6524

Browse files
committed
Fix printer rustc change
1 parent 4d68b45 commit dce6524

File tree

1 file changed

+61
-60
lines changed
  • kani-compiler/src/codegen_cprover_gotoc/codegen

1 file changed

+61
-60
lines changed

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

Lines changed: 61 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ use rustc_middle::ty::print::with_no_trimmed_paths;
1414
use rustc_middle::ty::print::FmtPrinter;
1515
use rustc_middle::ty::GenericArgsRef;
1616
use rustc_middle::ty::{
17-
self, AdtDef, Const, FloatTy, GeneratorArgs, Instance, IntTy, PolyFnSig, Ty, TyCtxt, TyKind,
17+
self, AdtDef, Const, CoroutineArgs, FloatTy, Instance, IntTy, PolyFnSig, Ty, TyCtxt, TyKind,
1818
UintTy, VariantDef, VtblEntry,
1919
};
2020
use rustc_middle::ty::{List, TypeFoldable};
@@ -326,13 +326,13 @@ impl<'tcx> GotocCtx<'tcx> {
326326
// Adapted from `fn_sig_for_fn_abi` in
327327
// https://github.com/rust-lang/rust/blob/739d68a76e35b22341d9930bb6338bf202ba05ba/compiler/rustc_ty_utils/src/abi.rs#L88
328328
// Code duplication tracked here: https://github.com/model-checking/kani/issues/1365
329-
fn generator_sig(
329+
fn coroutine_sig(
330330
&self,
331331
did: &DefId,
332332
ty: Ty<'tcx>,
333333
args: ty::GenericArgsRef<'tcx>,
334334
) -> ty::PolyFnSig<'tcx> {
335-
let sig = args.as_generator().poly_sig();
335+
let sig = args.as_coroutine().poly_sig();
336336

337337
let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(
338338
sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))),
@@ -350,12 +350,12 @@ impl<'tcx> GotocCtx<'tcx> {
350350
let env_ty = Ty::new_adt(self.tcx, pin_adt_ref, pin_args);
351351

352352
let sig = sig.skip_binder();
353-
// The `FnSig` and the `ret_ty` here is for a generators main
354-
// `Generator::resume(...) -> GeneratorState` function in case we
355-
// have an ordinary generator, or the `Future::poll(...) -> Poll`
356-
// function in case this is a special generator backing an async construct.
353+
// The `FnSig` and the `ret_ty` here is for a coroutines main
354+
// `coroutine::resume(...) -> CoroutineState` function in case we
355+
// have an ordinary coroutine, or the `Future::poll(...) -> Poll`
356+
// function in case this is a special coroutine backing an async construct.
357357
let tcx = self.tcx;
358-
let (resume_ty, ret_ty) = if tcx.generator_is_async(*did) {
358+
let (resume_ty, ret_ty) = if tcx.coroutine_is_async(*did) {
359359
// The signature should be `Future::poll(_, &mut Context<'_>) -> Poll<Output>`
360360
let poll_did = tcx.require_lang_item(LangItem::Poll, None);
361361
let poll_adt_ref = tcx.adt_def(poll_did);
@@ -378,8 +378,8 @@ impl<'tcx> GotocCtx<'tcx> {
378378

379379
(context_mut_ref, ret_ty)
380380
} else {
381-
// The signature should be `Generator::resume(_, Resume) -> GeneratorState<Yield, Return>`
382-
let state_did = tcx.require_lang_item(LangItem::GeneratorState, None);
381+
// The signature should be `Coroutine::resume(_, Resume) -> CoroutineState<Yield, Return>`
382+
let state_did = tcx.require_lang_item(LangItem::CoroutineState, None);
383383
let state_adt_ref = tcx.adt_def(state_did);
384384
let state_args = tcx.mk_args(&[sig.yield_ty.into(), sig.return_ty.into()]);
385385
let ret_ty = Ty::new_adt(tcx, state_adt_ref, state_args);
@@ -411,7 +411,7 @@ impl<'tcx> GotocCtx<'tcx> {
411411
}
412412
sig
413413
}
414-
ty::Generator(did, args, _) => self.generator_sig(did, fntyp, args),
414+
ty::Coroutine(did, args, _) => self.coroutine_sig(did, fntyp, args),
415415
_ => unreachable!("Can't get function signature of type: {:?}", fntyp),
416416
})
417417
}
@@ -632,16 +632,17 @@ impl<'tcx> GotocCtx<'tcx> {
632632
}
633633

634634
pub fn ty_pretty_name(&self, t: Ty<'tcx>) -> InternedString {
635+
use crate::rustc_middle::ty::print::Print;
635636
use rustc_hir::def::Namespace;
636-
use rustc_middle::ty::print::Printer;
637-
let printer = FmtPrinter::new(self.tcx, Namespace::TypeNS);
637+
let mut printer = FmtPrinter::new(self.tcx, Namespace::TypeNS);
638638

639639
// Monomorphizing the type ensures we get a cannonical form for dynamic trait
640640
// objects with auto traits, such as:
641641
// StructTag("tag-std::boxed::Box<(dyn std::error::Error + std::marker::Send + std::marker::Sync)>") }
642642
// StructTag("tag-std::boxed::Box<dyn std::error::Error + std::marker::Send + std::marker::Sync>") }
643643
let t = self.monomorphize(t);
644-
with_no_trimmed_paths!(printer.print_type(t).unwrap().into_buffer()).intern()
644+
t.print(&mut printer).unwrap();
645+
with_no_trimmed_paths!(printer.into_buffer()).intern()
645646
}
646647

647648
pub fn ty_mangled_name(&self, t: Ty<'tcx>) -> InternedString {
@@ -790,7 +791,7 @@ impl<'tcx> GotocCtx<'tcx> {
790791
}
791792
ty::FnPtr(sig) => self.codegen_function_sig(*sig).to_pointer(),
792793
ty::Closure(_, subst) => self.codegen_ty_closure(ty, subst),
793-
ty::Generator(..) => self.codegen_ty_generator(ty),
794+
ty::Coroutine(..) => self.codegen_ty_coroutine(ty),
794795
ty::Never => self.ensure_struct(NEVER_TYPE_EMPTY_STRUCT_NAME, "!", |_, _| vec![]),
795796
ty::Tuple(ts) => {
796797
if ts.is_empty() {
@@ -813,7 +814,7 @@ impl<'tcx> GotocCtx<'tcx> {
813814
ty::Bound(_, _) | ty::Param(_) => unreachable!("monomorphization bug"),
814815

815816
// type checking remnants which shouldn't be reachable
816-
ty::GeneratorWitness(_, _) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => {
817+
ty::CoroutineWitness(_, _) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => {
817818
unreachable!("remnants of type checking")
818819
}
819820
}
@@ -981,9 +982,9 @@ impl<'tcx> GotocCtx<'tcx> {
981982
})
982983
}
983984

984-
/// Translate a generator type similarly to an enum with a variant for each suspend point.
985+
/// Translate a coroutine type similarly to an enum with a variant for each suspend point.
985986
///
986-
/// Consider the following generator:
987+
/// Consider the following coroutine:
987988
/// ```
988989
/// || {
989990
/// let a = true;
@@ -995,13 +996,13 @@ impl<'tcx> GotocCtx<'tcx> {
995996
/// ```
996997
///
997998
/// Rustc compiles this to something similar to the following enum (but there are differences, see below!),
998-
/// as described at the top of <https://github.com/rust-lang/rust/blob/master/compiler/rustc_mir_transform/src/generator.rs>:
999+
/// as described at the top of <https://github.com/rust-lang/rust/blob/master/compiler/rustc_mir_transform/src/coroutine.rs>:
9991000
///
10001001
/// ```ignore
1001-
/// enum GeneratorEnum {
1002-
/// Unresumed, // initial state of the generator
1003-
/// Returned, // generator has returned
1004-
/// Panicked, // generator has panicked
1002+
/// enum CoroutineEnum {
1003+
/// Unresumed, // initial state of the coroutine
1004+
/// Returned, // coroutine has returned
1005+
/// Panicked, // coroutine has panicked
10051006
/// Suspend0 { b: &bool, a: bool }, // state after suspending (`yield`ing) for the first time
10061007
/// Suspend1, // state after suspending (`yield`ing) for the second time
10071008
/// }
@@ -1014,12 +1015,12 @@ impl<'tcx> GotocCtx<'tcx> {
10141015
/// This means that we CANNOT use the enum translation, which would be roughly as follows:
10151016
///
10161017
/// ```ignore
1017-
/// struct GeneratorEnum {
1018+
/// struct CoroutineEnum {
10181019
/// int case; // discriminant
1019-
/// union GeneratorEnum-union cases; // variant
1020+
/// union CoroutineEnum-union cases; // variant
10201021
/// }
10211022
///
1022-
/// union GeneratorEnum-union {
1023+
/// union CoroutineEnum-union {
10231024
/// struct Unresumed variant0;
10241025
/// struct Returned variant1;
10251026
/// // ...
@@ -1029,10 +1030,10 @@ impl<'tcx> GotocCtx<'tcx> {
10291030
/// Instead, we use the following translation:
10301031
///
10311032
/// ```ignore
1032-
/// union GeneratorEnum {
1033+
/// union CoroutineEnum {
10331034
/// struct DirectFields direct_fields;
1034-
/// struct Unresumed generator_variant_Unresumed;
1035-
/// struct Returned generator_variant_Returned;
1035+
/// struct Unresumed coroutine_variant_Unresumed;
1036+
/// struct Returned coroutine_variant_Returned;
10361037
/// // ...
10371038
/// }
10381039
///
@@ -1049,17 +1050,17 @@ impl<'tcx> GotocCtx<'tcx> {
10491050
/// // ...
10501051
///
10511052
/// struct Suspend0 {
1052-
/// bool *generator_field_0; // variable b in the generator code above
1053+
/// bool *coroutine_field_0; // variable b in the coroutine code above
10531054
/// // padding (for char case in DirectFields)
1054-
/// bool generator_field_1; // variable a in the generator code above
1055+
/// bool coroutine_field_1; // variable a in the coroutine code above
10551056
/// }
10561057
/// ```
10571058
///
1058-
/// Of course, if the generator has any other top-level/direct fields, they'd be included in the `DirectFields` struct as well.
1059-
fn codegen_ty_generator(&mut self, ty: Ty<'tcx>) -> Type {
1060-
let generator_name = self.ty_mangled_name(ty);
1059+
/// Of course, if the coroutine has any other top-level/direct fields, they'd be included in the `DirectFields` struct as well.
1060+
fn codegen_ty_coroutine(&mut self, ty: Ty<'tcx>) -> Type {
1061+
let coroutine_name = self.ty_mangled_name(ty);
10611062
let pretty_name = self.ty_pretty_name(ty);
1062-
debug!(?pretty_name, "codeged_ty_generator");
1063+
debug!(?pretty_name, "codeged_ty_coroutine");
10631064
self.ensure_union(self.ty_mangled_name(ty), pretty_name, |ctx, _| {
10641065
let type_and_layout = ctx.layout_of(ty);
10651066
let (discriminant_field, variants) = match &type_and_layout.variants {
@@ -1069,13 +1070,13 @@ impl<'tcx> GotocCtx<'tcx> {
10691070
variants,
10701071
..
10711072
} => (tag_field, variants),
1072-
_ => unreachable!("Generators have more than one variant and use direct encoding"),
1073+
_ => unreachable!("Coroutines have more than one variant and use direct encoding"),
10731074
};
10741075
// generate a struct for the direct fields of the layout (fields that don't occur in the variants)
10751076
let direct_fields = DatatypeComponent::Field {
10761077
name: "direct_fields".into(),
1077-
typ: ctx.codegen_generator_variant_struct(
1078-
generator_name,
1078+
typ: ctx.codegen_coroutine_variant_struct(
1079+
coroutine_name,
10791080
pretty_name,
10801081
type_and_layout,
10811082
"DirectFields".into(),
@@ -1084,11 +1085,11 @@ impl<'tcx> GotocCtx<'tcx> {
10841085
};
10851086
let mut fields = vec![direct_fields];
10861087
for var_idx in variants.indices() {
1087-
let variant_name = GeneratorArgs::variant_name(var_idx).into();
1088+
let variant_name = CoroutineArgs::variant_name(var_idx).into();
10881089
fields.push(DatatypeComponent::Field {
1089-
name: ctx.generator_variant_name(var_idx),
1090-
typ: ctx.codegen_generator_variant_struct(
1091-
generator_name,
1090+
name: ctx.coroutine_variant_name(var_idx),
1091+
typ: ctx.codegen_coroutine_variant_struct(
1092+
coroutine_name,
10921093
pretty_name,
10931094
type_and_layout.for_variant(ctx, var_idx),
10941095
variant_name,
@@ -1100,22 +1101,22 @@ impl<'tcx> GotocCtx<'tcx> {
11001101
})
11011102
}
11021103

1103-
/// Generates a struct for a variant of the generator.
1104+
/// Generates a struct for a variant of the coroutine.
11041105
///
1105-
/// The field `discriminant_field` should be `Some(idx)` when generating the variant for the direct (top-[evel) fields of the generator.
1106+
/// The field `discriminant_field` should be `Some(idx)` when generating the variant for the direct (top-[evel) fields of the coroutine.
11061107
/// Then the field with the index `idx` will be treated as the discriminant and will be given a special name to work with the rest of the code.
1107-
/// The field `discriminant_field` should be `None` when generating an actual variant of the generator because those don't contain the discriminant as a field.
1108-
fn codegen_generator_variant_struct(
1108+
/// The field `discriminant_field` should be `None` when generating an actual variant of the coroutine because those don't contain the discriminant as a field.
1109+
fn codegen_coroutine_variant_struct(
11091110
&mut self,
1110-
generator_name: InternedString,
1111-
pretty_generator_name: InternedString,
1111+
coroutine_name: InternedString,
1112+
pretty_coroutine_name: InternedString,
11121113
type_and_layout: TyAndLayout<'tcx, Ty<'tcx>>,
11131114
variant_name: InternedString,
11141115
discriminant_field: Option<usize>,
11151116
) -> Type {
1116-
let struct_name = format!("{generator_name}::{variant_name}");
1117-
let pretty_struct_name = format!("{pretty_generator_name}::{variant_name}");
1118-
debug!(?pretty_struct_name, "codeged_generator_variant_struct");
1117+
let struct_name = format!("{coroutine_name}::{variant_name}");
1118+
let pretty_struct_name = format!("{pretty_coroutine_name}::{variant_name}");
1119+
debug!(?pretty_struct_name, "codeged_coroutine_variant_struct");
11191120
self.ensure_struct(struct_name, pretty_struct_name, |ctx, _| {
11201121
let mut offset = Size::ZERO;
11211122
let mut fields = vec![];
@@ -1125,7 +1126,7 @@ impl<'tcx> GotocCtx<'tcx> {
11251126
let field_name = if Some(idx) == discriminant_field {
11261127
"case".into()
11271128
} else {
1128-
ctx.generator_field_name(idx)
1129+
ctx.coroutine_field_name(idx)
11291130
};
11301131
let field_ty = type_and_layout.field(ctx, idx).ty;
11311132
let field_offset = type_and_layout.fields.offset(idx);
@@ -1148,12 +1149,12 @@ impl<'tcx> GotocCtx<'tcx> {
11481149
})
11491150
}
11501151

1151-
pub fn generator_variant_name(&self, var_idx: VariantIdx) -> InternedString {
1152-
format!("generator_variant_{}", GeneratorArgs::variant_name(var_idx)).into()
1152+
pub fn coroutine_variant_name(&self, var_idx: VariantIdx) -> InternedString {
1153+
format!("coroutine_variant_{}", CoroutineArgs::variant_name(var_idx)).into()
11531154
}
11541155

1155-
pub fn generator_field_name(&self, field_idx: usize) -> InternedString {
1156-
format!("generator_field_{field_idx}").into()
1156+
pub fn coroutine_field_name(&self, field_idx: usize) -> InternedString {
1157+
format!("coroutine_field_{field_idx}").into()
11571158
}
11581159

11591160
/// Codegen "fat pointers" to the given `pointee_type`. These are pointers with metadata.
@@ -1230,7 +1231,7 @@ impl<'tcx> GotocCtx<'tcx> {
12301231
| ty::Closure(..)
12311232
| ty::Float(_)
12321233
| ty::Foreign(_)
1233-
| ty::Generator(..)
1234+
| ty::Coroutine(..)
12341235
| ty::Int(_)
12351236
| ty::RawPtr(_)
12361237
| ty::Ref(..)
@@ -1250,7 +1251,7 @@ impl<'tcx> GotocCtx<'tcx> {
12501251
// For soundness, hold off on generating them till we have test-cases.
12511252
ty::Bound(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
12521253
ty::Error(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
1253-
ty::GeneratorWitness(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
1254+
ty::CoroutineWitness(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
12541255
ty::Infer(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
12551256
ty::Param(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
12561257
ty::Placeholder(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
@@ -1441,9 +1442,9 @@ impl<'tcx> GotocCtx<'tcx> {
14411442
})
14421443
}
14431444
Variants::Multiple { tag_encoding, variants, tag_field, .. } => {
1444-
// Contrary to generators, currently enums have only one field (the discriminant), the rest are in the variants:
1445+
// Contrary to coroutines, currently enums have only one field (the discriminant), the rest are in the variants:
14451446
assert!(layout.fields.count() <= 1);
1446-
// Contrary to generators, the discriminant is the first (and only) field for enums:
1447+
// Contrary to coroutines, the discriminant is the first (and only) field for enums:
14471448
assert_eq!(*tag_field, 0);
14481449
match tag_encoding {
14491450
TagEncoding::Direct => {

0 commit comments

Comments
 (0)