Rename Generators to Coroutines

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,

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)

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 {

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(

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"),

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 { .. } => {

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;

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"]

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;
+    });
+}

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

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));
+}

tests/expected/generators/pin/expected → 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

tests/expected/generators/pin/main.rs → 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"),
     }
 }