From 4d68b45ca149624a17e8b1315be2bae0e061d4db Mon Sep 17 00:00:00 2001
From: jaisnan <jaisnan@amazon.com>
Date: Fri, 27 Oct 2023 18:06:07 +0000
Subject: [PATCH 1/3] Rename Generators to Coroutines

---
 .../codegen_cprover_gotoc/codegen/operand.rs  |  2 +-
 .../codegen_cprover_gotoc/codegen/place.rs    | 34 +++++-----
 .../codegen_cprover_gotoc/codegen/rvalue.rs   | 12 ++--
 .../codegen/statement.rs                      |  2 +-
 kani-compiler/src/kani_middle/analysis.rs     |  2 +-
 kani-compiler/src/kani_middle/reachability.rs |  2 +-
 kani-driver/src/cbmc_property_renderer.rs     | 15 ++--
 rust-toolchain.toml                           |  2 +-
 .../as_parameter/expected                     |  0
 .../expected/coroutines/as_parameter/main.rs  | 28 ++++++++
 tests/expected/coroutines/expected            | 10 +++
 tests/expected/coroutines/main.rs             | 23 +++++++
 .../{generators => coroutines}/pin/expected   |  2 +-
 .../{generators => coroutines}/pin/main.rs    | 16 ++---
 .../expected/generators/as_parameter/main.rs  | 28 --------
 tests/expected/generators/expected            | 10 ---
 tests/expected/generators/main.rs             | 23 -------
 .../{Generator => Coroutines}/issue-1593.rs   |  2 +-
 .../{Generator => Coroutines}/issue-2434.rs   |  0
 tests/kani/{Generator => Coroutines}/main.rs  |  8 +--
 .../conditional-drop.rs                       |  6 +-
 .../rustc-coroutine-tests}/control-flow.rs    | 12 ++--
 .../rustc-coroutine-tests}/env-drop.rs        |  6 +-
 .../rustc-coroutine-tests}/iterator-count.rs  | 16 ++---
 .../live-upvar-across-yield.rs                |  6 +-
 .../moved-locals-size.rs                      | 20 +++---
 .../rustc-coroutine-tests}/moved-locals.rs    | 68 +++++++++----------
 .../nested-generators.rs                      | 14 ++--
 .../niche-in-generator-size.rs                |  8 +--
 .../niche-in-generator.rs                     | 12 ++--
 .../overlap-locals-size.rs                    |  6 +-
 .../rustc-coroutine-tests}/overlap-locals.rs  | 16 ++---
 .../rustc-coroutine-tests}/resume-arg-size.rs | 12 ++--
 .../rustc-coroutine-tests}/resume-arg.rs      | 18 ++---
 .../resume-live-across-yield.rs               | 10 +--
 .../smoke-resume-args.rs                      | 12 ++--
 .../rustc-coroutine-tests}/smoke.rs           | 34 +++++-----
 .../static-generator.rs                       | 16 ++---
 .../rustc-coroutine-tests}/yield-in-box.rs    | 14 ++--
 tests/kani/Scopes_Returning/main.rs           |  4 +-
 40 files changed, 268 insertions(+), 263 deletions(-)
 rename tests/expected/{generators => coroutines}/as_parameter/expected (100%)
 create mode 100644 tests/expected/coroutines/as_parameter/main.rs
 create mode 100644 tests/expected/coroutines/expected
 create mode 100644 tests/expected/coroutines/main.rs
 rename tests/expected/{generators => coroutines}/pin/expected (81%)
 rename tests/expected/{generators => coroutines}/pin/main.rs (53%)
 delete mode 100644 tests/expected/generators/as_parameter/main.rs
 delete mode 100644 tests/expected/generators/expected
 delete mode 100644 tests/expected/generators/main.rs
 rename tests/kani/{Generator => Coroutines}/issue-1593.rs (90%)
 rename tests/kani/{Generator => Coroutines}/issue-2434.rs (100%)
 rename tests/kani/{Generator => Coroutines}/main.rs (64%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/conditional-drop.rs (91%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/control-flow.rs (78%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/env-drop.rs (91%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/iterator-count.rs (65%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/live-upvar-across-yield.rs (76%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/moved-locals-size.rs (81%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/moved-locals.rs (52%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/nested-generators.rs (55%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/niche-in-generator-size.rs (68%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/niche-in-generator.rs (55%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/overlap-locals-size.rs (84%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/overlap-locals.rs (58%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/resume-arg-size.rs (70%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/resume-arg.rs (52%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/resume-live-across-yield.rs (83%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/smoke-resume-args.rs (90%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/smoke.rs (80%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/static-generator.rs (50%)
 rename tests/kani/{Generator/rustc-generator-tests => Coroutines/rustc-coroutine-tests}/yield-in-box.rs (64%)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index 2e76cb00276c..bd2df19afcc5 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -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,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index c32962e3e4b8..551de7034e15 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -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`
@@ -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,
         }
     }
 
@@ -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,
         }
     }
 }
@@ -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:?}")
             }
         }
     }
@@ -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:?}")
             }
         }
     }
@@ -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(
@@ -258,7 +258,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     | ty::FnPtr(_)
                     | ty::Never
                     | ty::FnDef(..)
-                    | ty::GeneratorWitness(..)
+                    | ty::CoroutineWitness(..)
                     | ty::Foreign(..)
                     | ty::Dynamic(..)
                     | ty::Bound(..)
@@ -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))
@@ -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))
             }
         }
@@ -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()
                     ),
                 };
@@ -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)
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 896da44f532f..db792d6cb6af 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -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>,
@@ -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);
@@ -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),
         }
     }
 
@@ -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 {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index e706e55dc50a..a4597885716a 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -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(
diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs
index 6aa448539946..e5cced950e01 100644
--- a/kani-compiler/src/kani_middle/analysis.rs
+++ b/kani-compiler/src/kani_middle/analysis.rs
@@ -152,7 +152,7 @@ impl<'tcx> From<&Terminator<'tcx>> for Key {
             TerminatorKind::Assert { .. } => Key("Assert"),
             TerminatorKind::Call { .. } => Key("Call"),
             TerminatorKind::Drop { .. } => Key("Drop"),
-            TerminatorKind::GeneratorDrop => Key("GeneratorDrop"),
+            TerminatorKind::CoroutineDrop => Key("CoroutineDrop"),
             TerminatorKind::Goto { .. } => Key("Goto"),
             TerminatorKind::FalseEdge { .. } => Key("FalseEdge"),
             TerminatorKind::FalseUnwind { .. } => Key("FalseUnwind"),
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index 55f425c6da69..35ba3d6229f4 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -567,7 +567,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> {
             | TerminatorKind::UnwindResume
             | TerminatorKind::Return
             | TerminatorKind::Unreachable => {}
-            TerminatorKind::GeneratorDrop
+            TerminatorKind::CoroutineDrop
             | TerminatorKind::Yield { .. }
             | TerminatorKind::FalseEdge { .. }
             | TerminatorKind::FalseUnwind { .. } => {
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index be788c5d1c0c..62ef748a1ad5 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -532,10 +532,14 @@ fn build_failure_message(description: String, trace: &Option<Vec<TraceItem>>) ->
 /// to `--object-bits` being too low. The message is edited to show Kani
 /// options.
 fn postprocess_error_message(message: ParserItem) -> ParserItem {
-    if let ParserItem::Message { ref message_text, message_type: _ } = message && message_text.contains("use the `--object-bits n` option") {
+    if let ParserItem::Message { ref message_text, message_type: _ } = message
+        && message_text.contains("use the `--object-bits n` option")
+    {
         ParserItem::Message {
-            message_text: message_text.replace("--object-bits ", "--enable-unstable --cbmc-args --object-bits "),
-            message_type: String::from("ERROR") }
+            message_text: message_text
+                .replace("--object-bits ", "--enable-unstable --cbmc-args --object-bits "),
+            message_type: String::from("ERROR"),
+        }
     } else {
         message
     }
@@ -619,7 +623,10 @@ fn modify_undefined_function_checks(mut properties: Vec<Property>) -> (Vec<Prope
         {
             // Missing functions come with mangled names.
             // `demangle` produces the demangled version if it's a mangled name.
-            let modified_description = format!("Function `{:#}` with missing definition is unreachable", demangle(function));
+            let modified_description = format!(
+                "Function `{:#}` with missing definition is unreachable",
+                demangle(function)
+            );
             prop.description = modified_description;
             if prop.status == CheckStatus::Failure {
                 has_unknown_location_checks = true;
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 0762784d9e34..55f140064ad6 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-10-20"
+channel = "nightly-2023-10-26"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/expected/generators/as_parameter/expected b/tests/expected/coroutines/as_parameter/expected
similarity index 100%
rename from tests/expected/generators/as_parameter/expected
rename to tests/expected/coroutines/as_parameter/expected
diff --git a/tests/expected/coroutines/as_parameter/main.rs b/tests/expected/coroutines/as_parameter/main.rs
new file mode 100644
index 000000000000..7c0b9aed0373
--- /dev/null
+++ b/tests/expected/coroutines/as_parameter/main.rs
@@ -0,0 +1,28 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Test that a coroutine can be passed as a parameter.
+// (adapted from https://github.com/model-checking/kani/issues/1075)
+
+#![feature(coroutines, coroutine_trait)]
+
+use std::ops::{Coroutine, CoroutineState};
+use std::pin::Pin;
+
+fn foo<G: Coroutine<Yield = u8, Return = u8> + Unpin>(mut g: G)
+where
+    <G as std::ops::Coroutine>::Return: std::cmp::PartialEq,
+{
+    let res = Pin::new(&mut g).resume(());
+    assert_eq!(res, CoroutineState::Yielded(1));
+    let res2 = Pin::new(&mut g).resume(());
+    assert_eq!(res2, CoroutineState::Complete(2));
+}
+
+#[kani::proof]
+fn main() {
+    foo(|| {
+        yield 1;
+        return 2;
+    });
+}
diff --git a/tests/expected/coroutines/expected b/tests/expected/coroutines/expected
new file mode 100644
index 000000000000..c1be99367ed3
--- /dev/null
+++ b/tests/expected/coroutines/expected
@@ -0,0 +1,10 @@
+SUCCESS\
+Description: "assertion failed: res == CoroutineState::Yielded(val)"
+
+SUCCESS\
+Description: "assertion failed: res == CoroutineState::Complete(!val)"
+
+UNREACHABLE\
+Description: "coroutine resumed after completion"
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/coroutines/main.rs b/tests/expected/coroutines/main.rs
new file mode 100644
index 000000000000..a49d9944d0f1
--- /dev/null
+++ b/tests/expected/coroutines/main.rs
@@ -0,0 +1,23 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#![feature(coroutines, coroutine_trait)]
+
+use std::ops::{Coroutine, CoroutineState};
+use std::pin::Pin;
+
+#[kani::proof]
+#[kani::unwind(2)]
+fn main() {
+    let val: bool = kani::any();
+    let mut coroutine = move || {
+        let x = val;
+        yield x;
+        return !x;
+    };
+
+    let res = Pin::new(&mut coroutine).resume(());
+    assert_eq!(res, CoroutineState::Yielded(val));
+    let res = Pin::new(&mut coroutine).resume(());
+    assert_eq!(res, CoroutineState::Complete(!val));
+}
diff --git a/tests/expected/generators/pin/expected b/tests/expected/coroutines/pin/expected
similarity index 81%
rename from tests/expected/generators/pin/expected
rename to tests/expected/coroutines/pin/expected
index f665f880591d..1c2dc54a2f62 100644
--- a/tests/expected/generators/pin/expected
+++ b/tests/expected/coroutines/pin/expected
@@ -7,7 +7,7 @@ Description: "unexpected yield from resume"\
 in function main
 
 UNREACHABLE\
-Description: "generator resumed after completion"
+Description: "coroutine resumed after completion"
 in function main::{closure#0}
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/generators/pin/main.rs b/tests/expected/coroutines/pin/main.rs
similarity index 53%
rename from tests/expected/generators/pin/main.rs
rename to tests/expected/coroutines/pin/main.rs
index bf7ddf4e4dc5..0052715377ec 100644
--- a/tests/expected/generators/pin/main.rs
+++ b/tests/expected/coroutines/pin/main.rs
@@ -1,27 +1,27 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Test contains a call to a generator via a Pin
+// Test contains a call to a coroutine via a Pin
 // from https://github.com/model-checking/kani/issues/416
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
-use std::ops::{Generator, GeneratorState};
+use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 #[kani::proof]
 fn main() {
-    let mut generator = || {
+    let mut coroutine = || {
         yield 1;
         return true;
     };
 
-    match Pin::new(&mut generator).resume(()) {
-        GeneratorState::Yielded(1) => {}
+    match Pin::new(&mut coroutine).resume(()) {
+        CoroutineState::Yielded(1) => {}
         _ => panic!("unexpected return from resume"),
     }
-    match Pin::new(&mut generator).resume(()) {
-        GeneratorState::Complete(true) => {}
+    match Pin::new(&mut coroutine).resume(()) {
+        CoroutineState::Complete(true) => {}
         _ => panic!("unexpected yield from resume"),
     }
 }
diff --git a/tests/expected/generators/as_parameter/main.rs b/tests/expected/generators/as_parameter/main.rs
deleted file mode 100644
index 513204e230ec..000000000000
--- a/tests/expected/generators/as_parameter/main.rs
+++ /dev/null
@@ -1,28 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-// Test that a generator can be passed as a parameter.
-// (adapted from https://github.com/model-checking/kani/issues/1075)
-
-#![feature(generators, generator_trait)]
-
-use std::ops::{Generator, GeneratorState};
-use std::pin::Pin;
-
-fn foo<G: Generator<Yield = u8, Return = u8> + Unpin>(mut g: G)
-where
-    <G as std::ops::Generator>::Return: std::cmp::PartialEq,
-{
-    let res = Pin::new(&mut g).resume(());
-    assert_eq!(res, GeneratorState::Yielded(1));
-    let res2 = Pin::new(&mut g).resume(());
-    assert_eq!(res2, GeneratorState::Complete(2));
-}
-
-#[kani::proof]
-fn main() {
-    foo(|| {
-        yield 1;
-        return 2;
-    });
-}
diff --git a/tests/expected/generators/expected b/tests/expected/generators/expected
deleted file mode 100644
index b619dd8c009a..000000000000
--- a/tests/expected/generators/expected
+++ /dev/null
@@ -1,10 +0,0 @@
-SUCCESS\
-Description: "assertion failed: res == GeneratorState::Yielded(val)"
-
-SUCCESS\
-Description: "assertion failed: res == GeneratorState::Complete(!val)"
-
-UNREACHABLE\
-Description: "generator resumed after completion"
-
-VERIFICATION:- SUCCESSFUL
\ No newline at end of file
diff --git a/tests/expected/generators/main.rs b/tests/expected/generators/main.rs
deleted file mode 100644
index b6dbce9363c5..000000000000
--- a/tests/expected/generators/main.rs
+++ /dev/null
@@ -1,23 +0,0 @@
-// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-#![feature(generators, generator_trait)]
-
-use std::ops::{Generator, GeneratorState};
-use std::pin::Pin;
-
-#[kani::proof]
-#[kani::unwind(2)]
-fn main() {
-    let val: bool = kani::any();
-    let mut generator = move || {
-        let x = val;
-        yield x;
-        return !x;
-    };
-
-    let res = Pin::new(&mut generator).resume(());
-    assert_eq!(res, GeneratorState::Yielded(val));
-    let res = Pin::new(&mut generator).resume(());
-    assert_eq!(res, GeneratorState::Complete(!val));
-}
diff --git a/tests/kani/Generator/issue-1593.rs b/tests/kani/Coroutines/issue-1593.rs
similarity index 90%
rename from tests/kani/Generator/issue-1593.rs
rename to tests/kani/Coroutines/issue-1593.rs
index c1ee4a8ddf31..9028dadad3d3 100644
--- a/tests/kani/Generator/issue-1593.rs
+++ b/tests/kani/Coroutines/issue-1593.rs
@@ -4,7 +4,7 @@
 // compile-flags: --edition 2018
 
 // Regression test for https://github.com/model-checking/kani/issues/1593
-// The problem was that the size of a generator was wrong, which was discovered
+// The problem was that the size of a coroutine was wrong, which was discovered
 // in the context of vtables.
 
 use std::sync::{
diff --git a/tests/kani/Generator/issue-2434.rs b/tests/kani/Coroutines/issue-2434.rs
similarity index 100%
rename from tests/kani/Generator/issue-2434.rs
rename to tests/kani/Coroutines/issue-2434.rs
diff --git a/tests/kani/Generator/main.rs b/tests/kani/Coroutines/main.rs
similarity index 64%
rename from tests/kani/Generator/main.rs
rename to tests/kani/Coroutines/main.rs
index c9f6e9f51db9..10d92571aaa6 100644
--- a/tests/kani/Generator/main.rs
+++ b/tests/kani/Coroutines/main.rs
@@ -1,11 +1,11 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// This tests that generators work, even with a non-() resume type.
+// This tests that coroutines work, even with a non-() resume type.
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
-use std::ops::{Generator, GeneratorState};
+use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 #[kani::proof]
@@ -18,6 +18,6 @@ fn main() {
     for _ in 0..2 {
         let val = kani::any();
         let res = Pin::new(&mut add_one).resume(val);
-        assert_eq!(res, GeneratorState::Yielded(val.saturating_add(1)));
+        assert_eq!(res, CoroutineState::Yielded(val.saturating_add(1)));
     }
 }
diff --git a/tests/kani/Generator/rustc-generator-tests/conditional-drop.rs b/tests/kani/Coroutines/rustc-coroutine-tests/conditional-drop.rs
similarity index 91%
rename from tests/kani/Generator/rustc-generator-tests/conditional-drop.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/conditional-drop.rs
index 7cd1f792858d..81036a8f1238 100644
--- a/tests/kani/Generator/rustc-generator-tests/conditional-drop.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/conditional-drop.rs
@@ -1,5 +1,5 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/conditional-drop.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/conditional-drop.rs
 
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
@@ -11,9 +11,9 @@
 // revisions: default nomiropt
 //[nomiropt]compile-flags: -Z mir-opt-level=0
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
-use std::ops::Generator;
+use std::ops::Coroutine;
 use std::pin::Pin;
 use std::sync::atomic::{AtomicUsize, Ordering};
 
diff --git a/tests/kani/Generator/rustc-generator-tests/control-flow.rs b/tests/kani/Coroutines/rustc-coroutine-tests/control-flow.rs
similarity index 78%
rename from tests/kani/Generator/rustc-generator-tests/control-flow.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/control-flow.rs
index 726801f9420b..6e48b96e1d2a 100644
--- a/tests/kani/Generator/rustc-generator-tests/control-flow.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/control-flow.rs
@@ -1,5 +1,5 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/control-flow.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/control-flow.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
@@ -11,20 +11,20 @@
 // revisions: default nomiropt
 //[nomiropt]compile-flags: -Z mir-opt-level=0
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
 use std::marker::Unpin;
-use std::ops::{Generator, GeneratorState};
+use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 fn finish<T>(mut amt: usize, mut t: T) -> T::Return
 where
-    T: Generator<(), Yield = ()> + Unpin,
+    T: Coroutine<(), Yield = ()> + Unpin,
 {
     loop {
         match Pin::new(&mut t).resume(()) {
-            GeneratorState::Yielded(()) => amt = amt.checked_sub(1).unwrap(),
-            GeneratorState::Complete(ret) => {
+            CoroutineState::Yielded(()) => amt = amt.checked_sub(1).unwrap(),
+            CoroutineState::Complete(ret) => {
                 assert_eq!(amt, 0);
                 return ret;
             }
diff --git a/tests/kani/Generator/rustc-generator-tests/env-drop.rs b/tests/kani/Coroutines/rustc-coroutine-tests/env-drop.rs
similarity index 91%
rename from tests/kani/Generator/rustc-generator-tests/env-drop.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/env-drop.rs
index 47a3f4a08fa5..a6420aca283b 100644
--- a/tests/kani/Generator/rustc-generator-tests/env-drop.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/env-drop.rs
@@ -1,5 +1,5 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/env-drop.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/env-drop.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
@@ -11,9 +11,9 @@
 // revisions: default nomiropt
 //[nomiropt]compile-flags: -Z mir-opt-level=0
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
-use std::ops::Generator;
+use std::ops::Coroutine;
 use std::pin::Pin;
 use std::sync::atomic::{AtomicUsize, Ordering};
 
diff --git a/tests/kani/Generator/rustc-generator-tests/iterator-count.rs b/tests/kani/Coroutines/rustc-coroutine-tests/iterator-count.rs
similarity index 65%
rename from tests/kani/Generator/rustc-generator-tests/iterator-count.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/iterator-count.rs
index f4a7378cfad0..caa2efec216f 100644
--- a/tests/kani/Generator/rustc-generator-tests/iterator-count.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/iterator-count.rs
@@ -1,5 +1,5 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/iterator-count.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/iterator-count.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
@@ -8,28 +8,28 @@
 
 // run-pass
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
 use std::marker::Unpin;
-use std::ops::{Generator, GeneratorState};
+use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 struct W<T>(T);
 
-// This impl isn't safe in general, but the generator used in this test is movable
+// This impl isn't safe in general, but the coroutine used in this test is movable
 // so it won't cause problems.
-impl<T: Generator<(), Return = ()> + Unpin> Iterator for W<T> {
+impl<T: Coroutine<(), Return = ()> + Unpin> Iterator for W<T> {
     type Item = T::Yield;
 
     fn next(&mut self) -> Option<Self::Item> {
         match Pin::new(&mut self.0).resume(()) {
-            GeneratorState::Complete(..) => None,
-            GeneratorState::Yielded(v) => Some(v),
+            CoroutineState::Complete(..) => None,
+            CoroutineState::Yielded(v) => Some(v),
         }
     }
 }
 
-fn test() -> impl Generator<(), Return = (), Yield = u8> + Unpin {
+fn test() -> impl Coroutine<(), Return = (), Yield = u8> + Unpin {
     || {
         for i in 1..6 {
             yield i
diff --git a/tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs b/tests/kani/Coroutines/rustc-coroutine-tests/live-upvar-across-yield.rs
similarity index 76%
rename from tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/live-upvar-across-yield.rs
index df1f0c0eb3db..9bce8679464f 100644
--- a/tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/live-upvar-across-yield.rs
@@ -1,5 +1,5 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/live-upvar-across-yield.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/live-upvar-across-yield.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
@@ -8,9 +8,9 @@
 
 // run-pass
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
-use std::ops::Generator;
+use std::ops::Coroutine;
 use std::pin::Pin;
 
 #[kani::proof]
diff --git a/tests/kani/Generator/rustc-generator-tests/moved-locals-size.rs b/tests/kani/Coroutines/rustc-coroutine-tests/moved-locals-size.rs
similarity index 81%
rename from tests/kani/Generator/rustc-generator-tests/moved-locals-size.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/moved-locals-size.rs
index 77cdd6ada955..d63d34427ca6 100644
--- a/tests/kani/Generator/rustc-generator-tests/moved-locals-size.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/moved-locals-size.rs
@@ -1,13 +1,13 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/size-moved-locals.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/size-moved-locals.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 // Modifications Copyright Kani Contributors
 // See GitHub history for details.
 
-//! Tests the size of generators
-//! Note that the size of generators can depend on the panic strategy.
+//! Tests the size of coroutines
+//! Note that the size of coroutines can depend on the panic strategy.
 //! This is the case here (see the bottom of the file).
 //! In particular, running rustc with default options on this file will fail an assertion.
 //! Since Kani uses "panic=abort", you need to run rustc with `-C panic=abort`
@@ -20,7 +20,7 @@
 // `complex` below.)
 //
 // The exact sizes here can change (we'd like to know when they do). What we
-// don't want to see is the `complex` generator size being upwards of 2048 bytes
+// don't want to see is the `complex` coroutine size being upwards of 2048 bytes
 // (which would indicate it is reserving space for two copies of Foo.)
 //
 // See issue https://github.com/rust-lang/rust/issues/59123 for a full explanation.
@@ -29,9 +29,9 @@
 // ignore-wasm32 issue #62807
 // ignore-asmjs issue #62807
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
-use std::ops::Generator;
+use std::ops::Coroutine;
 
 const FOO_SIZE: usize = 1024;
 struct Foo([u8; FOO_SIZE]);
@@ -40,7 +40,7 @@ impl Drop for Foo {
     fn drop(&mut self) {}
 }
 
-fn move_before_yield() -> impl Generator<Yield = (), Return = ()> {
+fn move_before_yield() -> impl Coroutine<Yield = (), Return = ()> {
     static || {
         let first = Foo([0; FOO_SIZE]);
         let _second = first;
@@ -51,7 +51,7 @@ fn move_before_yield() -> impl Generator<Yield = (), Return = ()> {
 
 fn noop() {}
 
-fn move_before_yield_with_noop() -> impl Generator<Yield = (), Return = ()> {
+fn move_before_yield_with_noop() -> impl Coroutine<Yield = (), Return = ()> {
     static || {
         let first = Foo([0; FOO_SIZE]);
         noop();
@@ -63,7 +63,7 @@ fn move_before_yield_with_noop() -> impl Generator<Yield = (), Return = ()> {
 
 // Today we don't have NRVO (we allocate space for both `first` and `second`,)
 // but we can overlap `first` with `_third`.
-fn overlap_move_points() -> impl Generator<Yield = (), Return = ()> {
+fn overlap_move_points() -> impl Coroutine<Yield = (), Return = ()> {
     static || {
         let first = Foo([0; FOO_SIZE]);
         yield;
@@ -74,7 +74,7 @@ fn overlap_move_points() -> impl Generator<Yield = (), Return = ()> {
     }
 }
 
-fn overlap_x_and_y() -> impl Generator<Yield = (), Return = ()> {
+fn overlap_x_and_y() -> impl Coroutine<Yield = (), Return = ()> {
     static || {
         let x = Foo([0; FOO_SIZE]);
         yield;
diff --git a/tests/kani/Generator/rustc-generator-tests/moved-locals.rs b/tests/kani/Coroutines/rustc-coroutine-tests/moved-locals.rs
similarity index 52%
rename from tests/kani/Generator/rustc-generator-tests/moved-locals.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/moved-locals.rs
index d5a9469be4e7..b3b6c4cc6767 100644
--- a/tests/kani/Generator/rustc-generator-tests/moved-locals.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/moved-locals.rs
@@ -1,5 +1,5 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/size-moved-locals.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/size-moved-locals.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
@@ -12,7 +12,7 @@
 // `complex` below.)
 //
 // The exact sizes here can change (we'd like to know when they do). What we
-// don't want to see is the `complex` generator size being upwards of 2048 bytes
+// don't want to see is the `complex` coroutine size being upwards of 2048 bytes
 // (which would indicate it is reserving space for two copies of Foo.)
 //
 // See issue #59123 for a full explanation.
@@ -21,9 +21,9 @@
 // ignore-wasm32 issue #62807
 // ignore-asmjs issue #62807
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
-use std::ops::{Generator, GeneratorState};
+use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 const FOO_SIZE: usize = 128;
@@ -33,7 +33,7 @@ impl Drop for Foo {
     fn drop(&mut self) {}
 }
 
-fn move_before_yield() -> impl Generator<Yield = (), Return = ()> {
+fn move_before_yield() -> impl Coroutine<Yield = (), Return = ()> {
     static || {
         let first = Foo([0; FOO_SIZE]);
         let _second = first;
@@ -44,7 +44,7 @@ fn move_before_yield() -> impl Generator<Yield = (), Return = ()> {
 
 fn noop() {}
 
-fn move_before_yield_with_noop() -> impl Generator<Yield = (), Return = ()> {
+fn move_before_yield_with_noop() -> impl Coroutine<Yield = (), Return = ()> {
     static || {
         let first = Foo([0; FOO_SIZE]);
         noop();
@@ -56,7 +56,7 @@ fn move_before_yield_with_noop() -> impl Generator<Yield = (), Return = ()> {
 
 // Today we don't have NRVO (we allocate space for both `first` and `second`,)
 // but we can overlap `first` with `_third`.
-fn overlap_move_points() -> impl Generator<Yield = (), Return = ()> {
+fn overlap_move_points() -> impl Coroutine<Yield = (), Return = ()> {
     static || {
         let first = Foo([0; FOO_SIZE]);
         yield;
@@ -67,7 +67,7 @@ fn overlap_move_points() -> impl Generator<Yield = (), Return = ()> {
     }
 }
 
-fn overlap_x_and_y() -> impl Generator<Yield = (), Return = ()> {
+fn overlap_x_and_y() -> impl Coroutine<Yield = (), Return = ()> {
     static || {
         let x = Foo([0; FOO_SIZE]);
         yield;
@@ -80,55 +80,55 @@ fn overlap_x_and_y() -> impl Generator<Yield = (), Return = ()> {
 
 #[kani::proof]
 fn main() {
-    let mut generator = move_before_yield();
+    let mut coroutine = move_before_yield();
     assert_eq!(
-        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
-        GeneratorState::Yielded(())
+        unsafe { Pin::new_unchecked(&mut coroutine) }.resume(()),
+        CoroutineState::Yielded(())
     );
     assert_eq!(
-        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
-        GeneratorState::Complete(())
+        unsafe { Pin::new_unchecked(&mut coroutine) }.resume(()),
+        CoroutineState::Complete(())
     );
 
-    let mut generator = move_before_yield_with_noop();
+    let mut coroutine = move_before_yield_with_noop();
     assert_eq!(
-        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
-        GeneratorState::Yielded(())
+        unsafe { Pin::new_unchecked(&mut coroutine) }.resume(()),
+        CoroutineState::Yielded(())
     );
     assert_eq!(
-        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
-        GeneratorState::Complete(())
+        unsafe { Pin::new_unchecked(&mut coroutine) }.resume(()),
+        CoroutineState::Complete(())
     );
 
-    let mut generator = overlap_move_points();
+    let mut coroutine = overlap_move_points();
     assert_eq!(
-        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
-        GeneratorState::Yielded(())
+        unsafe { Pin::new_unchecked(&mut coroutine) }.resume(()),
+        CoroutineState::Yielded(())
     );
     assert_eq!(
-        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
-        GeneratorState::Yielded(())
+        unsafe { Pin::new_unchecked(&mut coroutine) }.resume(()),
+        CoroutineState::Yielded(())
     );
     assert_eq!(
-        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
-        GeneratorState::Yielded(())
+        unsafe { Pin::new_unchecked(&mut coroutine) }.resume(()),
+        CoroutineState::Yielded(())
     );
     assert_eq!(
-        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
-        GeneratorState::Complete(())
+        unsafe { Pin::new_unchecked(&mut coroutine) }.resume(()),
+        CoroutineState::Complete(())
     );
 
-    let mut generator = overlap_x_and_y();
+    let mut coroutine = overlap_x_and_y();
     assert_eq!(
-        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
-        GeneratorState::Yielded(())
+        unsafe { Pin::new_unchecked(&mut coroutine) }.resume(()),
+        CoroutineState::Yielded(())
     );
     assert_eq!(
-        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
-        GeneratorState::Yielded(())
+        unsafe { Pin::new_unchecked(&mut coroutine) }.resume(()),
+        CoroutineState::Yielded(())
     );
     assert_eq!(
-        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
-        GeneratorState::Complete(())
+        unsafe { Pin::new_unchecked(&mut coroutine) }.resume(()),
+        CoroutineState::Complete(())
     );
 }
diff --git a/tests/kani/Generator/rustc-generator-tests/nested-generators.rs b/tests/kani/Coroutines/rustc-coroutine-tests/nested-generators.rs
similarity index 55%
rename from tests/kani/Generator/rustc-generator-tests/nested-generators.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/nested-generators.rs
index 31ab9a47daa6..0d770380e2b9 100644
--- a/tests/kani/Generator/rustc-generator-tests/nested-generators.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/nested-generators.rs
@@ -1,5 +1,5 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/nested-generators.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/nested-coroutines.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
@@ -8,20 +8,20 @@
 
 // run-pass
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
-use std::ops::{Generator, GeneratorState};
+use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 #[kani::proof]
 fn main() {
-    let _generator = || {
-        let mut sub_generator = || {
+    let _coroutine = || {
+        let mut sub_coroutine = || {
             yield 2;
         };
 
-        match Pin::new(&mut sub_generator).resume(()) {
-            GeneratorState::Yielded(x) => {
+        match Pin::new(&mut sub_coroutine).resume(()) {
+            CoroutineState::Yielded(x) => {
                 yield x;
             }
             _ => panic!(),
diff --git a/tests/kani/Generator/rustc-generator-tests/niche-in-generator-size.rs b/tests/kani/Coroutines/rustc-coroutine-tests/niche-in-generator-size.rs
similarity index 68%
rename from tests/kani/Generator/rustc-generator-tests/niche-in-generator-size.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/niche-in-generator-size.rs
index 6796fd3a1a26..5de21166c318 100644
--- a/tests/kani/Generator/rustc-generator-tests/niche-in-generator-size.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/niche-in-generator-size.rs
@@ -1,16 +1,16 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/niche-in-generator.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/niche-in-coroutine.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 // Modifications Copyright Kani Contributors
 // See GitHub history for details.
 
-// Test that niche finding works with captured generator upvars.
+// Test that niche finding works with captured coroutine upvars.
 
 // run-pass
 
-#![feature(generators)]
+#![feature(coroutines)]
 
 use std::mem::size_of_val;
 
@@ -24,6 +24,6 @@ fn main() {
         take(x);
     };
 
-    // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395)
+    // FIXME: size of coroutines does not work reliably (https://github.com/model-checking/kani/issues/1395)
     assert_eq!(size_of_val(&gen1), size_of_val(&Some(gen1)));
 }
diff --git a/tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs b/tests/kani/Coroutines/rustc-coroutine-tests/niche-in-generator.rs
similarity index 55%
rename from tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/niche-in-generator.rs
index 6e09b0967032..170a356fb318 100644
--- a/tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/niche-in-generator.rs
@@ -1,18 +1,18 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/niche-in-generator.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/niche-in-coroutine.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 // Modifications Copyright Kani Contributors
 // See GitHub history for details.
 
-// Test that niche finding works with captured generator upvars.
+// Test that niche finding works with captured coroutine upvars.
 
 // run-pass
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
-use std::ops::{Generator, GeneratorState};
+use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 use std::mem::size_of_val;
@@ -27,6 +27,6 @@ fn main() {
         take(x);
     };
 
-    assert_eq!(Pin::new(&mut gen1).resume(()), GeneratorState::Yielded(()));
-    assert_eq!(Pin::new(&mut gen1).resume(()), GeneratorState::Complete(()));
+    assert_eq!(Pin::new(&mut gen1).resume(()), CoroutineState::Yielded(()));
+    assert_eq!(Pin::new(&mut gen1).resume(()), CoroutineState::Complete(()));
 }
diff --git a/tests/kani/Generator/rustc-generator-tests/overlap-locals-size.rs b/tests/kani/Coroutines/rustc-coroutine-tests/overlap-locals-size.rs
similarity index 84%
rename from tests/kani/Generator/rustc-generator-tests/overlap-locals-size.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/overlap-locals-size.rs
index 6043d9024744..d22ed53f8b60 100644
--- a/tests/kani/Generator/rustc-generator-tests/overlap-locals-size.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/overlap-locals-size.rs
@@ -1,5 +1,5 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/overlap-locals.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/overlap-locals.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
@@ -8,7 +8,7 @@
 
 // run-pass
 
-#![feature(generators)]
+#![feature(coroutines)]
 
 #[kani::proof]
 fn main() {
@@ -35,6 +35,6 @@ fn main() {
         }
     };
 
-    // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395)
+    // FIXME: size of coroutines does not work reliably (https://github.com/model-checking/kani/issues/1395)
     assert_eq!(8, std::mem::size_of_val(&a));
 }
diff --git a/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs b/tests/kani/Coroutines/rustc-coroutine-tests/overlap-locals.rs
similarity index 58%
rename from tests/kani/Generator/rustc-generator-tests/overlap-locals.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/overlap-locals.rs
index 319e5d429842..6033b2f06a99 100644
--- a/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/overlap-locals.rs
@@ -1,5 +1,5 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/overlap-locals.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/overlap-locals.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
@@ -8,9 +8,9 @@
 
 // run-pass
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
-use std::ops::{Generator, GeneratorState};
+use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 #[kani::proof]
@@ -34,9 +34,9 @@ fn main() {
         }
     };
 
-    assert_eq!(Pin::new(&mut a).resume(()), GeneratorState::Yielded(()));
-    assert_eq!(Pin::new(&mut a).resume(()), GeneratorState::Yielded(()));
-    assert_eq!(Pin::new(&mut a).resume(()), GeneratorState::Yielded(()));
-    assert_eq!(Pin::new(&mut a).resume(()), GeneratorState::Yielded(()));
-    assert_eq!(Pin::new(&mut a).resume(()), GeneratorState::Complete(()));
+    assert_eq!(Pin::new(&mut a).resume(()), CoroutineState::Yielded(()));
+    assert_eq!(Pin::new(&mut a).resume(()), CoroutineState::Yielded(()));
+    assert_eq!(Pin::new(&mut a).resume(()), CoroutineState::Yielded(()));
+    assert_eq!(Pin::new(&mut a).resume(()), CoroutineState::Yielded(()));
+    assert_eq!(Pin::new(&mut a).resume(()), CoroutineState::Complete(()));
 }
diff --git a/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs b/tests/kani/Coroutines/rustc-coroutine-tests/resume-arg-size.rs
similarity index 70%
rename from tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/resume-arg-size.rs
index 70318ebfb6d0..f59ef260bcda 100644
--- a/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/resume-arg-size.rs
@@ -1,12 +1,12 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/resume-arg-size.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/resume-arg-size.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 // Modifications Copyright Kani Contributors
 // See GitHub history for details.
 
-#![feature(generators)]
+#![feature(coroutines)]
 
 // run-pass
 
@@ -14,7 +14,7 @@ use std::mem::size_of_val;
 
 #[kani::proof]
 fn main() {
-    // Generator taking a `Copy`able resume arg.
+    // Coroutine taking a `Copy`able resume arg.
     let gen_copy = |mut x: usize| {
         loop {
             drop(x);
@@ -22,7 +22,7 @@ fn main() {
         }
     };
 
-    // Generator taking a non-`Copy` resume arg.
+    // Coroutine taking a non-`Copy` resume arg.
     let gen_move = |mut x: Box<usize>| {
         loop {
             drop(x);
@@ -30,9 +30,9 @@ fn main() {
         }
     };
 
-    // Neither of these generators have the resume arg live across the `yield`, so they should be
+    // Neither of these coroutines have the resume arg live across the `yield`, so they should be
     // 1 Byte in size (only storing the discriminant)
-    // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395)
+    // FIXME: size of coroutines does not work reliably (https://github.com/model-checking/kani/issues/1395)
     assert_eq!(size_of_val(&gen_copy), 1);
     assert_eq!(size_of_val(&gen_move), 1);
 }
diff --git a/tests/kani/Generator/rustc-generator-tests/resume-arg.rs b/tests/kani/Coroutines/rustc-coroutine-tests/resume-arg.rs
similarity index 52%
rename from tests/kani/Generator/rustc-generator-tests/resume-arg.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/resume-arg.rs
index b2237a8bb96d..0c2c87f5eb2e 100644
--- a/tests/kani/Generator/rustc-generator-tests/resume-arg.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/resume-arg.rs
@@ -1,14 +1,14 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/resume-arg-size.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/resume-arg-size.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 // Modifications Copyright Kani Contributors
 // See GitHub history for details.
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
-use std::ops::{Generator, GeneratorState};
+use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 // run-pass
@@ -17,7 +17,7 @@ use std::mem::size_of_val;
 
 #[kani::proof]
 fn main() {
-    // Generator taking a `Copy`able resume arg.
+    // Coroutine taking a `Copy`able resume arg.
     let mut gen_copy = |mut x: usize| {
         loop {
             drop(x);
@@ -25,7 +25,7 @@ fn main() {
         }
     };
 
-    // Generator taking a non-`Copy` resume arg.
+    // Coroutine taking a non-`Copy` resume arg.
     let mut gen_move = |mut x: Box<usize>| {
         loop {
             drop(x);
@@ -33,9 +33,9 @@ fn main() {
         }
     };
 
-    assert_eq!(Pin::new(&mut gen_copy).resume(0), GeneratorState::Yielded(()));
-    assert_eq!(Pin::new(&mut gen_copy).resume(1), GeneratorState::Yielded(()));
+    assert_eq!(Pin::new(&mut gen_copy).resume(0), CoroutineState::Yielded(()));
+    assert_eq!(Pin::new(&mut gen_copy).resume(1), CoroutineState::Yielded(()));
 
-    assert_eq!(Pin::new(&mut gen_move).resume(Box::new(0)), GeneratorState::Yielded(()));
-    assert_eq!(Pin::new(&mut gen_move).resume(Box::new(1)), GeneratorState::Yielded(()));
+    assert_eq!(Pin::new(&mut gen_move).resume(Box::new(0)), CoroutineState::Yielded(()));
+    assert_eq!(Pin::new(&mut gen_move).resume(Box::new(1)), CoroutineState::Yielded(()));
 }
diff --git a/tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs b/tests/kani/Coroutines/rustc-coroutine-tests/resume-live-across-yield.rs
similarity index 83%
rename from tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/resume-live-across-yield.rs
index d515a1acc04e..10d4d36223d5 100644
--- a/tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/resume-live-across-yield.rs
@@ -1,5 +1,5 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/resume-live-across-yield.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/resume-live-across-yield.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
@@ -8,9 +8,9 @@
 
 // run-pass
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
-use std::ops::{Generator, GeneratorState};
+use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 use std::sync::atomic::{AtomicUsize, Ordering};
 
@@ -37,11 +37,11 @@ fn main() {
 
     assert_eq!(
         g.as_mut().resume(Dropper(String::from("Hello world!"))),
-        GeneratorState::Yielded(())
+        CoroutineState::Yielded(())
     );
     assert_eq!(DROP.load(Ordering::Acquire), 0);
     match g.as_mut().resume(Dropper(String::from("Number Two"))) {
-        GeneratorState::Complete(dropper) => {
+        CoroutineState::Complete(dropper) => {
             assert_eq!(DROP.load(Ordering::Acquire), 1);
             assert_eq!(dropper.0, "Number Two");
             drop(dropper);
diff --git a/tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs b/tests/kani/Coroutines/rustc-coroutine-tests/smoke-resume-args.rs
similarity index 90%
rename from tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/smoke-resume-args.rs
index 26882285469a..85c75bc8147d 100644
--- a/tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/smoke-resume-args.rs
@@ -1,5 +1,5 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/smoke-resume-args.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/smoke-resume-args.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
@@ -11,20 +11,20 @@
 // revisions: default nomiropt
 //[nomiropt]compile-flags: -Z mir-opt-level=0
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
 use std::fmt::Debug;
 use std::marker::Unpin;
 use std::ops::{
-    Generator,
-    GeneratorState::{self, *},
+    Coroutine,
+    CoroutineState::{self, *},
 };
 use std::pin::Pin;
 use std::sync::atomic::{AtomicUsize, Ordering};
 
-fn drain<G: Generator<R, Yield = Y> + Unpin, R, Y>(
+fn drain<G: Coroutine<R, Yield = Y> + Unpin, R, Y>(
     gen: &mut G,
-    inout: Vec<(R, GeneratorState<Y, G::Return>)>,
+    inout: Vec<(R, CoroutineState<Y, G::Return>)>,
 ) where
     Y: Debug + PartialEq,
     G::Return: Debug + PartialEq,
diff --git a/tests/kani/Generator/rustc-generator-tests/smoke.rs b/tests/kani/Coroutines/rustc-coroutine-tests/smoke.rs
similarity index 80%
rename from tests/kani/Generator/rustc-generator-tests/smoke.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/smoke.rs
index 888ec969877b..2b9aa40a06c0 100644
--- a/tests/kani/Generator/rustc-generator-tests/smoke.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/smoke.rs
@@ -1,5 +1,5 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/smoke.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/smoke.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
@@ -14,9 +14,9 @@
 // ignore-emscripten no threads support
 // compile-flags: --test
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
-use std::ops::{Generator, GeneratorState};
+use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 use std::thread;
 
@@ -29,7 +29,7 @@ fn simple() {
     };
 
     match Pin::new(&mut foo).resume(()) {
-        GeneratorState::Complete(()) => {}
+        CoroutineState::Complete(()) => {}
         s => panic!("bad state: {:?}", s),
     }
 }
@@ -46,7 +46,7 @@ fn return_capture() {
     };
 
     match Pin::new(&mut foo).resume(()) {
-        GeneratorState::Complete(ref s) if *s == "foo" => {}
+        CoroutineState::Complete(ref s) if *s == "foo" => {}
         s => panic!("bad state: {:?}", s),
     }
 }
@@ -58,11 +58,11 @@ fn simple_yield() {
     };
 
     match Pin::new(&mut foo).resume(()) {
-        GeneratorState::Yielded(()) => {}
+        CoroutineState::Yielded(()) => {}
         s => panic!("bad state: {:?}", s),
     }
     match Pin::new(&mut foo).resume(()) {
-        GeneratorState::Complete(()) => {}
+        CoroutineState::Complete(()) => {}
         s => panic!("bad state: {:?}", s),
     }
 }
@@ -76,11 +76,11 @@ fn yield_capture() {
     };
 
     match Pin::new(&mut foo).resume(()) {
-        GeneratorState::Yielded(ref s) if *s == "foo" => {}
+        CoroutineState::Yielded(ref s) if *s == "foo" => {}
         s => panic!("bad state: {:?}", s),
     }
     match Pin::new(&mut foo).resume(()) {
-        GeneratorState::Complete(()) => {}
+        CoroutineState::Complete(()) => {}
         s => panic!("bad state: {:?}", s),
     }
 }
@@ -94,11 +94,11 @@ fn simple_yield_value() {
     };
 
     match Pin::new(&mut foo).resume(()) {
-        GeneratorState::Yielded(ref s) if *s == "bar" => {}
+        CoroutineState::Yielded(ref s) if *s == "bar" => {}
         s => panic!("bad state: {:?}", s),
     }
     match Pin::new(&mut foo).resume(()) {
-        GeneratorState::Complete(ref s) if *s == "foo" => {}
+        CoroutineState::Complete(ref s) if *s == "foo" => {}
         s => panic!("bad state: {:?}", s),
     }
 }
@@ -113,11 +113,11 @@ fn return_after_yield() {
     };
 
     match Pin::new(&mut foo).resume(()) {
-        GeneratorState::Yielded(()) => {}
+        CoroutineState::Yielded(()) => {}
         s => panic!("bad state: {:?}", s),
     }
     match Pin::new(&mut foo).resume(()) {
-        GeneratorState::Complete(ref s) if *s == "foo" => {}
+        CoroutineState::Complete(ref s) if *s == "foo" => {}
         s => panic!("bad state: {:?}", s),
     }
 }
@@ -163,11 +163,11 @@ fn send_over_threads() {
     let mut foo = || yield;
     thread::spawn(move || {
         match Pin::new(&mut foo).resume(()) {
-            GeneratorState::Yielded(()) => {}
+            CoroutineState::Yielded(()) => {}
             s => panic!("bad state: {:?}", s),
         }
         match Pin::new(&mut foo).resume(()) {
-            GeneratorState::Complete(()) => {}
+            CoroutineState::Complete(()) => {}
             s => panic!("bad state: {:?}", s),
         }
     })
@@ -178,11 +178,11 @@ fn send_over_threads() {
     let mut foo = || yield a;
     thread::spawn(move || {
         match Pin::new(&mut foo).resume(()) {
-            GeneratorState::Yielded(ref s) if *s == "a" => {}
+            CoroutineState::Yielded(ref s) if *s == "a" => {}
             s => panic!("bad state: {:?}", s),
         }
         match Pin::new(&mut foo).resume(()) {
-            GeneratorState::Complete(()) => {}
+            CoroutineState::Complete(()) => {}
             s => panic!("bad state: {:?}", s),
         }
     })
diff --git a/tests/kani/Generator/rustc-generator-tests/static-generator.rs b/tests/kani/Coroutines/rustc-coroutine-tests/static-generator.rs
similarity index 50%
rename from tests/kani/Generator/rustc-generator-tests/static-generator.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/static-generator.rs
index 519e00f29afa..52f89438255a 100644
--- a/tests/kani/Generator/rustc-generator-tests/static-generator.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/static-generator.rs
@@ -1,5 +1,5 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/static-generator.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/static-coroutine.rs
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
@@ -8,22 +8,22 @@
 
 // run-pass
 
-#![feature(generators, generator_trait)]
+#![feature(coroutines, coroutine_trait)]
 
-use std::ops::{Generator, GeneratorState};
+use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 #[kani::proof]
 fn main() {
-    let mut generator = static || {
+    let mut coroutine = static || {
         let a = true;
         let b = &a;
         yield;
         assert_eq!(b as *const _, &a as *const _);
     };
-    // SAFETY: We shadow the original generator variable so have no safe API to
+    // SAFETY: We shadow the original coroutine variable so have no safe API to
     // move it after this point.
-    let mut generator = unsafe { Pin::new_unchecked(&mut generator) };
-    assert_eq!(generator.as_mut().resume(()), GeneratorState::Yielded(()));
-    assert_eq!(generator.as_mut().resume(()), GeneratorState::Complete(()));
+    let mut coroutine = unsafe { Pin::new_unchecked(&mut coroutine) };
+    assert_eq!(coroutine.as_mut().resume(()), CoroutineState::Yielded(()));
+    assert_eq!(coroutine.as_mut().resume(()), CoroutineState::Complete(()));
 }
diff --git a/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs b/tests/kani/Coroutines/rustc-coroutine-tests/yield-in-box.rs
similarity index 64%
rename from tests/kani/Generator/rustc-generator-tests/yield-in-box.rs
rename to tests/kani/Coroutines/rustc-coroutine-tests/yield-in-box.rs
index 79690d9140c1..5dbf580f5f57 100644
--- a/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs
+++ b/tests/kani/Coroutines/rustc-coroutine-tests/yield-in-box.rs
@@ -1,5 +1,5 @@
 // Copyright rustc Contributors
-// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/yield-in-box.rs
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/coroutine/yield-in-box.rs
 
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
@@ -9,16 +9,16 @@
 // run-pass
 // Test that box-statements with yields in them work.
 
-#![feature(generators, generator_trait)]
-use std::ops::Generator;
-use std::ops::GeneratorState;
+#![feature(coroutines, coroutine_trait)]
+use std::ops::Coroutine;
+use std::ops::CoroutineState;
 use std::pin::Pin;
 
 #[kani::proof]
 fn main() {
     let x = 0i32;
     || {
-        //~ WARN unused generator that must be used
+        //~ WARN unused coroutine that must be used
         let y = 2u32;
         {
             let _t = Box::new((&x, yield 0, &y));
@@ -29,6 +29,6 @@ fn main() {
     };
 
     let mut g = |_| Box::new(yield);
-    assert_eq!(Pin::new(&mut g).resume(1), GeneratorState::Yielded(()));
-    assert_eq!(Pin::new(&mut g).resume(2), GeneratorState::Complete(Box::new(2)));
+    assert_eq!(Pin::new(&mut g).resume(1), CoroutineState::Yielded(()));
+    assert_eq!(Pin::new(&mut g).resume(2), CoroutineState::Complete(Box::new(2)));
 }
diff --git a/tests/kani/Scopes_Returning/main.rs b/tests/kani/Scopes_Returning/main.rs
index 3566479fdaf1..696e09ffc9b1 100644
--- a/tests/kani/Scopes_Returning/main.rs
+++ b/tests/kani/Scopes_Returning/main.rs
@@ -34,8 +34,6 @@ fn main() {
     assert!(e == d || e == 10);
 
     let g: u32 = kani::any();
-    let h = {
-        if g < 10 { g } else { 10 }
-    };
+    let h = { if g < 10 { g } else { 10 } };
     assert!(h == g || h == 10);
 }

From dce6524b61967929394f16d94a74da28d43e1321 Mon Sep 17 00:00:00 2001
From: jaisnan <jaisnan@amazon.com>
Date: Fri, 27 Oct 2023 19:04:15 +0000
Subject: [PATCH 2/3] Fix printer rustc change

---
 .../src/codegen_cprover_gotoc/codegen/typ.rs  | 121 +++++++++---------
 1 file changed, 61 insertions(+), 60 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 5538f4d9ceff..7de7e3673f9f 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -14,7 +14,7 @@ use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::print::FmtPrinter;
 use rustc_middle::ty::GenericArgsRef;
 use rustc_middle::ty::{
-    self, AdtDef, Const, FloatTy, GeneratorArgs, Instance, IntTy, PolyFnSig, Ty, TyCtxt, TyKind,
+    self, AdtDef, Const, CoroutineArgs, FloatTy, Instance, IntTy, PolyFnSig, Ty, TyCtxt, TyKind,
     UintTy, VariantDef, VtblEntry,
 };
 use rustc_middle::ty::{List, TypeFoldable};
@@ -326,13 +326,13 @@ impl<'tcx> GotocCtx<'tcx> {
     // Adapted from `fn_sig_for_fn_abi` in
     // https://github.com/rust-lang/rust/blob/739d68a76e35b22341d9930bb6338bf202ba05ba/compiler/rustc_ty_utils/src/abi.rs#L88
     // Code duplication tracked here: https://github.com/model-checking/kani/issues/1365
-    fn generator_sig(
+    fn coroutine_sig(
         &self,
         did: &DefId,
         ty: Ty<'tcx>,
         args: ty::GenericArgsRef<'tcx>,
     ) -> ty::PolyFnSig<'tcx> {
-        let sig = args.as_generator().poly_sig();
+        let sig = args.as_coroutine().poly_sig();
 
         let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(
             sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))),
@@ -350,12 +350,12 @@ impl<'tcx> GotocCtx<'tcx> {
         let env_ty = Ty::new_adt(self.tcx, pin_adt_ref, pin_args);
 
         let sig = sig.skip_binder();
-        // The `FnSig` and the `ret_ty` here is for a generators main
-        // `Generator::resume(...) -> GeneratorState` function in case we
-        // have an ordinary generator, or the `Future::poll(...) -> Poll`
-        // function in case this is a special generator backing an async construct.
+        // The `FnSig` and the `ret_ty` here is for a coroutines main
+        // `coroutine::resume(...) -> CoroutineState` function in case we
+        // have an ordinary coroutine, or the `Future::poll(...) -> Poll`
+        // function in case this is a special coroutine backing an async construct.
         let tcx = self.tcx;
-        let (resume_ty, ret_ty) = if tcx.generator_is_async(*did) {
+        let (resume_ty, ret_ty) = if tcx.coroutine_is_async(*did) {
             // The signature should be `Future::poll(_, &mut Context<'_>) -> Poll<Output>`
             let poll_did = tcx.require_lang_item(LangItem::Poll, None);
             let poll_adt_ref = tcx.adt_def(poll_did);
@@ -378,8 +378,8 @@ impl<'tcx> GotocCtx<'tcx> {
 
             (context_mut_ref, ret_ty)
         } else {
-            // The signature should be `Generator::resume(_, Resume) -> GeneratorState<Yield, Return>`
-            let state_did = tcx.require_lang_item(LangItem::GeneratorState, None);
+            // The signature should be `Coroutine::resume(_, Resume) -> CoroutineState<Yield, Return>`
+            let state_did = tcx.require_lang_item(LangItem::CoroutineState, None);
             let state_adt_ref = tcx.adt_def(state_did);
             let state_args = tcx.mk_args(&[sig.yield_ty.into(), sig.return_ty.into()]);
             let ret_ty = Ty::new_adt(tcx, state_adt_ref, state_args);
@@ -411,7 +411,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 }
                 sig
             }
-            ty::Generator(did, args, _) => self.generator_sig(did, fntyp, args),
+            ty::Coroutine(did, args, _) => self.coroutine_sig(did, fntyp, args),
             _ => unreachable!("Can't get function signature of type: {:?}", fntyp),
         })
     }
@@ -632,16 +632,17 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn ty_pretty_name(&self, t: Ty<'tcx>) -> InternedString {
+        use crate::rustc_middle::ty::print::Print;
         use rustc_hir::def::Namespace;
-        use rustc_middle::ty::print::Printer;
-        let printer = FmtPrinter::new(self.tcx, Namespace::TypeNS);
+        let mut printer = FmtPrinter::new(self.tcx, Namespace::TypeNS);
 
         // Monomorphizing the type ensures we get a cannonical form for dynamic trait
         // objects with auto traits, such as:
         //   StructTag("tag-std::boxed::Box<(dyn std::error::Error + std::marker::Send + std::marker::Sync)>") }
         //   StructTag("tag-std::boxed::Box<dyn std::error::Error + std::marker::Send + std::marker::Sync>") }
         let t = self.monomorphize(t);
-        with_no_trimmed_paths!(printer.print_type(t).unwrap().into_buffer()).intern()
+        t.print(&mut printer).unwrap();
+        with_no_trimmed_paths!(printer.into_buffer()).intern()
     }
 
     pub fn ty_mangled_name(&self, t: Ty<'tcx>) -> InternedString {
@@ -790,7 +791,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             ty::FnPtr(sig) => self.codegen_function_sig(*sig).to_pointer(),
             ty::Closure(_, subst) => self.codegen_ty_closure(ty, subst),
-            ty::Generator(..) => self.codegen_ty_generator(ty),
+            ty::Coroutine(..) => self.codegen_ty_coroutine(ty),
             ty::Never => self.ensure_struct(NEVER_TYPE_EMPTY_STRUCT_NAME, "!", |_, _| vec![]),
             ty::Tuple(ts) => {
                 if ts.is_empty() {
@@ -813,7 +814,7 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Bound(_, _) | ty::Param(_) => unreachable!("monomorphization bug"),
 
             // type checking remnants which shouldn't be reachable
-            ty::GeneratorWitness(_, _) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => {
+            ty::CoroutineWitness(_, _) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => {
                 unreachable!("remnants of type checking")
             }
         }
@@ -981,9 +982,9 @@ impl<'tcx> GotocCtx<'tcx> {
         })
     }
 
-    /// Translate a generator type similarly to an enum with a variant for each suspend point.
+    /// Translate a coroutine type similarly to an enum with a variant for each suspend point.
     ///
-    /// Consider the following generator:
+    /// Consider the following coroutine:
     /// ```
     /// || {
     ///     let a = true;
@@ -995,13 +996,13 @@ impl<'tcx> GotocCtx<'tcx> {
     /// ```
     ///
     /// Rustc compiles this to something similar to the following enum (but there are differences, see below!),
-    /// as described at the top of <https://github.com/rust-lang/rust/blob/master/compiler/rustc_mir_transform/src/generator.rs>:
+    /// as described at the top of <https://github.com/rust-lang/rust/blob/master/compiler/rustc_mir_transform/src/coroutine.rs>:
     ///
     /// ```ignore
-    /// enum GeneratorEnum {
-    ///     Unresumed,                        // initial state of the generator
-    ///     Returned,                         // generator has returned
-    ///     Panicked,                         // generator has panicked
+    /// enum CoroutineEnum {
+    ///     Unresumed,                        // initial state of the coroutine
+    ///     Returned,                         // coroutine has returned
+    ///     Panicked,                         // coroutine has panicked
     ///     Suspend0 { b: &bool, a: bool },   // state after suspending (`yield`ing) for the first time
     ///     Suspend1,                         // state after suspending (`yield`ing) for the second time
     /// }
@@ -1014,12 +1015,12 @@ impl<'tcx> GotocCtx<'tcx> {
     /// This means that we CANNOT use the enum translation, which would be roughly as follows:
     ///
     /// ```ignore
-    /// struct GeneratorEnum {
+    /// struct CoroutineEnum {
     ///     int case; // discriminant
-    ///     union GeneratorEnum-union cases; // variant
+    ///     union CoroutineEnum-union cases; // variant
     /// }
     ///
-    /// union GeneratorEnum-union {
+    /// union CoroutineEnum-union {
     ///     struct Unresumed variant0;
     ///     struct Returned variant1;
     ///     // ...
@@ -1029,10 +1030,10 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Instead, we use the following translation:
     ///
     /// ```ignore
-    /// union GeneratorEnum {
+    /// union CoroutineEnum {
     ///     struct DirectFields direct_fields;
-    ///     struct Unresumed generator_variant_Unresumed;
-    ///     struct Returned generator_variant_Returned;
+    ///     struct Unresumed coroutine_variant_Unresumed;
+    ///     struct Returned coroutine_variant_Returned;
     ///     // ...
     /// }
     ///
@@ -1049,17 +1050,17 @@ impl<'tcx> GotocCtx<'tcx> {
     /// // ...
     ///
     /// struct Suspend0 {
-    ///     bool *generator_field_0; // variable b in the generator code above
+    ///     bool *coroutine_field_0; // variable b in the coroutine code above
     ///     // padding (for char case in DirectFields)
-    ///     bool generator_field_1; // variable a in the generator code above
+    ///     bool coroutine_field_1; // variable a in the coroutine code above
     /// }
     /// ```
     ///
-    /// Of course, if the generator has any other top-level/direct fields, they'd be included in the `DirectFields` struct as well.
-    fn codegen_ty_generator(&mut self, ty: Ty<'tcx>) -> Type {
-        let generator_name = self.ty_mangled_name(ty);
+    /// Of course, if the coroutine has any other top-level/direct fields, they'd be included in the `DirectFields` struct as well.
+    fn codegen_ty_coroutine(&mut self, ty: Ty<'tcx>) -> Type {
+        let coroutine_name = self.ty_mangled_name(ty);
         let pretty_name = self.ty_pretty_name(ty);
-        debug!(?pretty_name, "codeged_ty_generator");
+        debug!(?pretty_name, "codeged_ty_coroutine");
         self.ensure_union(self.ty_mangled_name(ty), pretty_name, |ctx, _| {
             let type_and_layout = ctx.layout_of(ty);
             let (discriminant_field, variants) = match &type_and_layout.variants {
@@ -1069,13 +1070,13 @@ impl<'tcx> GotocCtx<'tcx> {
                     variants,
                     ..
                 } => (tag_field, variants),
-                _ => unreachable!("Generators have more than one variant and use direct encoding"),
+                _ => unreachable!("Coroutines have more than one variant and use direct encoding"),
             };
             // generate a struct for the direct fields of the layout (fields that don't occur in the variants)
             let direct_fields = DatatypeComponent::Field {
                 name: "direct_fields".into(),
-                typ: ctx.codegen_generator_variant_struct(
-                    generator_name,
+                typ: ctx.codegen_coroutine_variant_struct(
+                    coroutine_name,
                     pretty_name,
                     type_and_layout,
                     "DirectFields".into(),
@@ -1084,11 +1085,11 @@ impl<'tcx> GotocCtx<'tcx> {
             };
             let mut fields = vec![direct_fields];
             for var_idx in variants.indices() {
-                let variant_name = GeneratorArgs::variant_name(var_idx).into();
+                let variant_name = CoroutineArgs::variant_name(var_idx).into();
                 fields.push(DatatypeComponent::Field {
-                    name: ctx.generator_variant_name(var_idx),
-                    typ: ctx.codegen_generator_variant_struct(
-                        generator_name,
+                    name: ctx.coroutine_variant_name(var_idx),
+                    typ: ctx.codegen_coroutine_variant_struct(
+                        coroutine_name,
                         pretty_name,
                         type_and_layout.for_variant(ctx, var_idx),
                         variant_name,
@@ -1100,22 +1101,22 @@ impl<'tcx> GotocCtx<'tcx> {
         })
     }
 
-    /// Generates a struct for a variant of the generator.
+    /// Generates a struct for a variant of the coroutine.
     ///
-    /// The field `discriminant_field` should be `Some(idx)` when generating the variant for the direct (top-[evel) fields of the generator.
+    /// The field `discriminant_field` should be `Some(idx)` when generating the variant for the direct (top-[evel) fields of the coroutine.
     /// 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.
-    /// 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.
-    fn codegen_generator_variant_struct(
+    /// 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.
+    fn codegen_coroutine_variant_struct(
         &mut self,
-        generator_name: InternedString,
-        pretty_generator_name: InternedString,
+        coroutine_name: InternedString,
+        pretty_coroutine_name: InternedString,
         type_and_layout: TyAndLayout<'tcx, Ty<'tcx>>,
         variant_name: InternedString,
         discriminant_field: Option<usize>,
     ) -> Type {
-        let struct_name = format!("{generator_name}::{variant_name}");
-        let pretty_struct_name = format!("{pretty_generator_name}::{variant_name}");
-        debug!(?pretty_struct_name, "codeged_generator_variant_struct");
+        let struct_name = format!("{coroutine_name}::{variant_name}");
+        let pretty_struct_name = format!("{pretty_coroutine_name}::{variant_name}");
+        debug!(?pretty_struct_name, "codeged_coroutine_variant_struct");
         self.ensure_struct(struct_name, pretty_struct_name, |ctx, _| {
             let mut offset = Size::ZERO;
             let mut fields = vec![];
@@ -1125,7 +1126,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 let field_name = if Some(idx) == discriminant_field {
                     "case".into()
                 } else {
-                    ctx.generator_field_name(idx)
+                    ctx.coroutine_field_name(idx)
                 };
                 let field_ty = type_and_layout.field(ctx, idx).ty;
                 let field_offset = type_and_layout.fields.offset(idx);
@@ -1148,12 +1149,12 @@ impl<'tcx> GotocCtx<'tcx> {
         })
     }
 
-    pub fn generator_variant_name(&self, var_idx: VariantIdx) -> InternedString {
-        format!("generator_variant_{}", GeneratorArgs::variant_name(var_idx)).into()
+    pub fn coroutine_variant_name(&self, var_idx: VariantIdx) -> InternedString {
+        format!("coroutine_variant_{}", CoroutineArgs::variant_name(var_idx)).into()
     }
 
-    pub fn generator_field_name(&self, field_idx: usize) -> InternedString {
-        format!("generator_field_{field_idx}").into()
+    pub fn coroutine_field_name(&self, field_idx: usize) -> InternedString {
+        format!("coroutine_field_{field_idx}").into()
     }
 
     /// Codegen "fat pointers" to the given `pointee_type`. These are pointers with metadata.
@@ -1230,7 +1231,7 @@ impl<'tcx> GotocCtx<'tcx> {
             | ty::Closure(..)
             | ty::Float(_)
             | ty::Foreign(_)
-            | ty::Generator(..)
+            | ty::Coroutine(..)
             | ty::Int(_)
             | ty::RawPtr(_)
             | ty::Ref(..)
@@ -1250,7 +1251,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // For soundness, hold off on generating them till we have test-cases.
             ty::Bound(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
             ty::Error(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
-            ty::GeneratorWitness(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
+            ty::CoroutineWitness(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
             ty::Infer(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
             ty::Param(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
             ty::Placeholder(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
@@ -1441,9 +1442,9 @@ impl<'tcx> GotocCtx<'tcx> {
                 })
             }
             Variants::Multiple { tag_encoding, variants, tag_field, .. } => {
-                // Contrary to generators, currently enums have only one field (the discriminant), the rest are in the variants:
+                // Contrary to coroutines, currently enums have only one field (the discriminant), the rest are in the variants:
                 assert!(layout.fields.count() <= 1);
-                // Contrary to generators, the discriminant is the first (and only) field for enums:
+                // Contrary to coroutines, the discriminant is the first (and only) field for enums:
                 assert_eq!(*tag_field, 0);
                 match tag_encoding {
                     TagEncoding::Direct => {

From 4dfc327a95b7f9db547ddb860df6993db7c00eef Mon Sep 17 00:00:00 2001
From: jaisnan <jaisnan@amazon.com>
Date: Fri, 27 Oct 2023 19:29:34 +0000
Subject: [PATCH 3/3] update w/ clippy recommendation

---
 kani-driver/src/main.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs
index 15b66db8084d..1d2afa177ca9 100644
--- a/kani-driver/src/main.rs
+++ b/kani-driver/src/main.rs
@@ -130,7 +130,7 @@ enum InvocationType {
 
 /// Peeks at command line arguments to determine if we're being invoked as 'kani' or 'cargo-kani'
 fn determine_invocation_type(mut args: Vec<OsString>) -> InvocationType {
-    let exe = util::executable_basename(&args.get(0));
+    let exe = util::executable_basename(&args.first());
 
     // Case 1: if 'kani' is our first real argument, then we're being invoked as cargo-kani
     // 'cargo kani ...' will cause cargo to run 'cargo-kani kani ...' preserving argv1