Implement support for generators (rust-lang#1378)

Author: fzaiser

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

@@ -44,8 +44,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Get the number of parameters that the current function expects.
     fn get_params_size(&self) -> usize {
         let sig = self.current_fn().sig();
-        let sig =
-            self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig.unwrap());
+        let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig);
         // we don't call [codegen_function_sig] because we want to get a bit more metainformation.
         sig.inputs().len()
     }

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

@@ -313,9 +313,19 @@ impl<'tcx> GotocCtx<'tcx> {
         macro_rules! codegen_size_align {
             ($which: ident) => {{
                 let tp_ty = instance.substs.type_at(0);
-                let arg = fargs.remove(0);
-                let size_align = self.size_and_align_of_dst(tp_ty, arg);
-                self.codegen_expr_to_place(p, size_align.$which)
+                if tp_ty.is_generator() {
+                    let e = self.codegen_unimplemented(
+                        "size or alignment of a generator type",
+                        cbmc_ret_ty,
+                        loc,
+                        "https://github.com/model-checking/kani/issues/1395",
+                    );
+                    self.codegen_expr_to_place(p, e)
+                } else {
+                    let arg = fargs.remove(0);
+                    let size_align = self.size_and_align_of_dst(tp_ty, arg);
+                    self.codegen_expr_to_place(p, size_align.$which)
+                }
             }};
         }
 

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

@@ -331,8 +331,7 @@ impl<'tcx> GotocCtx<'tcx> {
             let var = tcx.gen_function_local_variable(2, &func_name, cgt.clone()).to_expr();
             let body = vec![
                 Stmt::decl(var.clone(), None, Location::none()),
-                var.clone()
-                    .member("case", &tcx.symbol_table)
+                tcx.codegen_discriminant_field(var.clone(), ty)
                     .assign(param.to_expr(), Location::none()),
                 var.ret(Location::none()),
             ];
@@ -641,7 +640,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// This is tracked in <https://github.com/model-checking/kani/issues/1350>.
     pub fn codegen_func_symbol(&mut self, instance: Instance<'tcx>) -> (&Symbol, Type) {
         let func = self.symbol_name(instance);
-        let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance).unwrap());
+        let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance));
         // make sure the functions imported from other modules are in the symbol table
         let sym = self.ensure(&func, |ctx, _| {
             Symbol::function(

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

@@ -15,7 +15,7 @@ use rustc_middle::{
     mir::{Field, Local, Place, ProjectionElem},
     ty::{self, Ty, TypeAndMut, VariantDef},
 };
-use rustc_target::abi::{TagEncoding, Variants};
+use rustc_target::abi::{TagEncoding, VariantIdx, Variants};
 use tracing::{debug, trace, warn};
 
 /// A projection in Kani can either be to a type (the normal case),
@@ -24,6 +24,7 @@ use tracing::{debug, trace, warn};
 pub enum TypeOrVariant<'tcx> {
     Type(Ty<'tcx>),
     Variant(&'tcx VariantDef),
+    GeneratorVariant(VariantIdx),
 }
 
 /// A struct for storing the data for passing to `codegen_unimplemented`
@@ -129,7 +130,7 @@ impl<'tcx> ProjectedPlace<'tcx> {
                 }
             }
             // TODO: handle Variant https://github.com/model-checking/kani/issues/448
-            TypeOrVariant::Variant(_) => None,
+            TypeOrVariant::Variant(_) | TypeOrVariant::GeneratorVariant(_) => None,
         }
     }
 
@@ -197,7 +198,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(_) => self,
+            TypeOrVariant::Variant(_) | TypeOrVariant::GeneratorVariant(_) => self,
         }
     }
 }
@@ -207,6 +208,9 @@ 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)
+            }
         }
     }
 
@@ -215,6 +219,9 @@ 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)
+            }
         }
     }
 }
@@ -269,12 +276,12 @@ impl<'tcx> GotocCtx<'tcx> {
                         Ok(res.member(&field.name.to_string(), &self.symbol_table))
                     }
                     ty::Closure(..) => Ok(res.member(&f.index().to_string(), &self.symbol_table)),
-                    ty::Generator(..) => Err(UnimplementedData::new(
-                        "ty::Generator",
-                        "https://github.com/model-checking/kani/issues/416",
-                        Type::code(vec![], Type::empty()),
-                        *res.location(),
-                    )),
+                    ty::Generator(..) => {
+                        let field_name = self.generator_field_name(f.index().into());
+                        Ok(res
+                            .member("direct_fields", &self.symbol_table)
+                            .member(field_name, &self.symbol_table))
+                    }
                     _ => unimplemented!(),
                 }
             }
@@ -283,6 +290,10 @@ impl<'tcx> GotocCtx<'tcx> {
                 let field = &v.fields[f.index()];
                 Ok(res.member(&field.name.to_string(), &self.symbol_table))
             }
+            TypeOrVariant::GeneratorVariant(_var_idx) => {
+                let field_name = self.generator_field_name(f.index().into());
+                Ok(res.member(field_name, &self.symbol_table))
+            }
         }
     }
 
@@ -498,33 +509,43 @@ impl<'tcx> GotocCtx<'tcx> {
             ProjectionElem::Downcast(_, idx) => {
                 // downcast converts a variable of an enum type to one of its discriminated cases
                 let t = before.mir_typ();
-                match t.kind() {
+                let (case_name, type_or_variant) = match t.kind() {
                     ty::Adt(def, _) => {
-                        let variant = def.variants().get(idx).unwrap();
-                        let case_name = variant.name.to_string();
-                        let typ = TypeOrVariant::Variant(variant);
-                        let expr = match &self.layout_of(t).variants {
-                            Variants::Single { .. } => before.goto_expr,
-                            Variants::Multiple { tag_encoding, .. } => match tag_encoding {
-                                TagEncoding::Direct => before
-                                    .goto_expr
-                                    .member("cases", &self.symbol_table)
-                                    .member(&case_name, &self.symbol_table),
-                                TagEncoding::Niche { .. } => {
-                                    before.goto_expr.member(&case_name, &self.symbol_table)
-                                }
-                            },
-                        };
-                        ProjectedPlace::try_new(
-                            expr,
-                            typ,
-                            before.fat_ptr_goto_expr,
-                            before.fat_ptr_mir_typ,
-                            self,
-                        )
+                        let variant = def.variant(idx);
+                        (variant.name.as_str().into(), TypeOrVariant::Variant(variant))
                     }
-                    _ => unreachable!("it's a bug to reach here!"),
-                }
+                    ty::Generator(..) => {
+                        (self.generator_variant_name(idx), TypeOrVariant::GeneratorVariant(idx))
+                    }
+                    _ => unreachable!(
+                        "cannot downcast {:?} to a variant (only enums and generators can)",
+                        &t.kind()
+                    ),
+                };
+                let layout = self.layout_of(t);
+                let expr = match &layout.variants {
+                    Variants::Single { .. } => before.goto_expr,
+                    Variants::Multiple { tag_encoding, .. } => match tag_encoding {
+                        TagEncoding::Direct => {
+                            let cases = if t.is_generator() {
+                                before.goto_expr
+                            } else {
+                                before.goto_expr.member("cases", &self.symbol_table)
+                            };
+                            cases.member(case_name, &self.symbol_table)
+                        }
+                        TagEncoding::Niche { .. } => {
+                            before.goto_expr.member(case_name, &self.symbol_table)
+                        }
+                    },
+                };
+                ProjectedPlace::try_new(
+                    expr,
+                    type_or_variant,
+                    before.fat_ptr_goto_expr,
+                    before.fat_ptr_mir_typ,
+                    self,
+                )
             }
             ProjectionElem::OpaqueCast(ty) => ProjectedPlace::try_new(
                 before.goto_expr.cast_to(self.codegen_ty(ty)),

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

@@ -502,6 +502,25 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    pub fn codegen_discriminant_field(&self, place: Expr, ty: Ty<'tcx>) -> Expr {
+        let layout = self.layout_of(ty);
+        assert!(
+            matches!(
+                &layout.variants,
+                Variants::Multiple { tag_encoding: TagEncoding::Direct, .. }
+            ),
+            "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`]).
+            // As a consequence, the discriminant is accessed as `.direct_fields.case` instead of just `.case`.
+            place.member("direct_fields", &self.symbol_table)
+        } else {
+            place
+        };
+        expr.member("case", &self.symbol_table)
+    }
+
     /// e: ty
     /// get the discriminant of e, of type res_ty
     pub fn codegen_get_discriminant(&mut self, e: Expr, ty: Ty<'tcx>, res_ty: Ty<'tcx>) -> Expr {
@@ -516,7 +535,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding {
                 TagEncoding::Direct => {
-                    e.member("case", &self.symbol_table).cast_to(self.codegen_ty(res_ty))
+                    self.codegen_discriminant_field(e, ty).cast_to(self.codegen_ty(res_ty))
                 }
                 TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
                     // This code follows the logic in the cranelift codegen backend:

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

@@ -65,8 +65,6 @@ impl<'tcx> GotocCtx<'tcx> {
                 let layout = self.layout_of(dst_mir_ty);
                 if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 {
                     // We ignore assignment for all zero size types
-                    // Ignore generators too for now:
-                    // https://github.com/model-checking/kani/issues/416
                     Stmt::skip(location)
                 } else {
                     unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place))
@@ -77,26 +75,13 @@ impl<'tcx> GotocCtx<'tcx> {
             StatementKind::SetDiscriminant { place, variant_index } => {
                 // this requires place points to an enum type.
                 let pt = self.place_ty(place);
-                let (def, _) = match pt.kind() {
-                    ty::Adt(def, substs) => (def, substs),
-                    ty::Generator(..) => {
-                        return self
-                            .codegen_unimplemented(
-                                "ty::Generator",
-                                Type::code(vec![], Type::empty()),
-                                location,
-                                "https://github.com/model-checking/kani/issues/416",
-                            )
-                            .as_stmt(location);
-                    }
-                    _ => unreachable!(),
-                };
                 let layout = self.layout_of(pt);
                 match &layout.variants {
                     Variants::Single { .. } => Stmt::skip(location),
                     Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding {
                         TagEncoding::Direct => {
-                            let discr = def.discriminant_for_variant(self.tcx, *variant_index);
+                            let discr =
+                                pt.discriminant_for_variant(self.tcx, *variant_index).unwrap();
                             let discr_t = self.codegen_enum_discr_typ(pt);
                             // The constant created below may not fit into the type.
                             // https://github.com/model-checking/kani/issues/996
@@ -111,13 +96,13 @@ impl<'tcx> GotocCtx<'tcx> {
                             // DISCRIMINANT - val:0 ty:i8
                             // DISCRIMINANT - val:1 ty:i8
                             let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t));
-                            unwrap_or_return_codegen_unimplemented_stmt!(
+                            let place_goto_expr = unwrap_or_return_codegen_unimplemented_stmt!(
                                 self,
                                 self.codegen_place(place)
                             )
-                            .goto_expr
-                            .member("case", &self.symbol_table)
-                            .assign(discr, location)
+                            .goto_expr;
+                            self.codegen_discriminant_field(place_goto_expr, pt)
+                                .assign(discr, location)
                         }
                         TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
                             if dataful_variant != variant_index {
@@ -206,7 +191,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 loc,
             ),
             TerminatorKind::Return => {
-                let rty = self.current_fn().sig().unwrap().skip_binder().output();
+                let rty = self.current_fn().sig().skip_binder().output();
                 if rty.is_unit() {
                     self.codegen_ret_unit()
                 } else {
@@ -534,15 +519,11 @@ impl<'tcx> GotocCtx<'tcx> {
     /// N.B. public only because instrinsics use this directly, too.
     pub(crate) fn codegen_funcall_args(&mut self, args: &[Operand<'tcx>]) -> Vec<Expr> {
         args.iter()
-            .filter_map(|o| {
-                let ot = self.operand_ty(o);
-                if self.ignore_var_ty(ot) {
-                    trace!(operand=?o, typ=?ot, "codegen_funcall_args ignore");
-                    None
-                } else if ot.is_bool() {
-                    Some(self.codegen_operand(o).cast_to(Type::c_bool()))
+            .map(|o| {
+                if self.operand_ty(o).is_bool() {
+                    self.codegen_operand(o).cast_to(Type::c_bool())
                 } else {
-                    Some(self.codegen_operand(o))
+                    self.codegen_operand(o)
                 }
             })
             .collect()

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

@@ -28,7 +28,7 @@ pub struct CurrentFnCtx<'tcx> {
     /// A human readable pretty name for the current function
     readable_name: String,
     /// The signature of the current function
-    sig: Option<PolyFnSig<'tcx>>,
+    sig: PolyFnSig<'tcx>,
     /// A counter to enable creating temporary variables
     temp_var_counter: u64,
 }
@@ -105,7 +105,7 @@ impl<'tcx> CurrentFnCtx<'tcx> {
     }
 
     /// The signature of the function we are currently compiling
-    pub fn sig(&self) -> Option<PolyFnSig<'tcx>> {
+    pub fn sig(&self) -> PolyFnSig<'tcx> {
         self.sig
     }
 }

kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs

@@ -6,7 +6,6 @@ use crate::codegen_cprover_gotoc::codegen::PropertyClass;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, SymbolTable, Type};
 use cbmc::{btree_string_map, InternedString};
-use rustc_errors::FatalError;
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{Instance, Ty};
 use tracing::debug;
@@ -101,11 +100,6 @@ impl<'tcx> GotocCtx<'tcx> {
         }
         s
     }
-
-    pub fn emit_error_and_exit(&self, error_msg: &str) -> ! {
-        self.tcx.sess.err(error_msg);
-        FatalError.raise()
-    }
 }
 
 /// Members traverse path to get to the raw pointer of a box (b.0.pointer.pointer).

kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs

@@ -1,2 +1 @@
-Status: FAILURE\
-Description: "ty::Generator is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/416"
+VERIFICATION:- SUCCESSFUL

tests/expected/generators/as_parameter/expected

@@ -1,18 +1,22 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Test that includes a generator as a parameter to a function
-// Codegen should succeed, but verification should fail (codegen_unimplemented)
+// 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;
+use std::ops::{Generator, GeneratorState};
+use std::pin::Pin;
 
-fn foo<T>(g: T)
+fn foo<G: Generator<Yield = u8, Return = u8> + Unpin>(mut g: G)
 where
-    T: Generator,
+    <G as std::ops::Generator>::Return: std::cmp::PartialEq,
 {
-    let _ = g;
+    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]

tests/expected/generators/as_parameter/main.rs

@@ -0,0 +1,10 @@
+SUCCESS\
+Description: "assertion failed: res == GeneratorState::Yielded(val)"
+
+SUCCESS\
+Description: "assertion failed: res == GeneratorState::Complete(!val)"
+
+UNREACHABLE\
+Description: "generator resumed after completion"
+
+VERIFICATION:- SUCCESSFUL

tests/expected/generators/expected

@@ -0,0 +1,23 @@
+// 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));
+}

tests/expected/generators/main.rs

@@ -1,2 +1,13 @@
-The `generators` feature is not currently supported by Kani
-exited with status exit status: 101
+SUCCESS\
+Description: "unexpected return from resume"\
+in function main
+
+SUCCESS\
+Description: "unexpected yield from resume"\
+in function main
+
+UNREACHABLE\
+Description: "generator resumed after completion"
+in function main::{closure#0}
+
+VERIFICATION:- SUCCESSFUL

tests/expected/generators/pin/expected

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // Test contains a call to a generator via a Pin
-// This is currently not supported, so Kani should error out
+// from https://github.com/model-checking/kani/issues/416
 
 #![feature(generators, generator_trait)]
 
@@ -13,15 +13,15 @@ use std::pin::Pin;
 fn main() {
     let mut generator = || {
         yield 1;
-        return "foo";
+        return true;
     };
 
     match Pin::new(&mut generator).resume(()) {
         GeneratorState::Yielded(1) => {}
         _ => panic!("unexpected return from resume"),
     }
     match Pin::new(&mut generator).resume(()) {
-        GeneratorState::Complete("foo") => {}
-        _ => panic!("unexpected return from resume"),
+        GeneratorState::Complete(true) => {}
+        _ => panic!("unexpected yield from resume"),
     }
 }

tests/expected/generators/pin/main.rs

@@ -1,27 +1,23 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that we can codegen code that has a Generator type present,
-// as long as the path is not dynamically used. Full Generator support
-// tracked in: https://github.com/model-checking/kani/issues/416
+// This tests that generators work, even with a non-() resume type.
 
 #![feature(generators, generator_trait)]
 
 use std::ops::{Generator, GeneratorState};
-
-// Seperate function to force translation
-fn maybe_call(call: bool) {
-    if call {
-        let mut _generator = || {
-            yield 1;
-            return 2;
-        };
-    } else {
-        assert!(1 + 1 == 2);
-    }
-}
+use std::pin::Pin;
 
 #[kani::proof]
 fn main() {
-    maybe_call(false);
+    let mut add_one = |mut resume: u8| {
+        loop {
+            resume = yield resume.saturating_add(1);
+        }
+    };
+    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)));
+    }
 }

tests/kani/Generator/main.rs

@@ -0,0 +1,74 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/conditional-drop.rs
+
+// run-pass
+
+// revisions: default nomiropt
+//[nomiropt]compile-flags: -Z mir-opt-level=0
+
+#![feature(generators, generator_trait)]
+
+use std::ops::Generator;
+use std::pin::Pin;
+use std::sync::atomic::{AtomicUsize, Ordering};
+
+static A: AtomicUsize = AtomicUsize::new(0);
+
+struct B;
+
+impl Drop for B {
+    fn drop(&mut self) {
+        A.fetch_add(1, Ordering::SeqCst);
+    }
+}
+
+fn test() -> bool {
+    true
+}
+fn test2() -> bool {
+    false
+}
+
+#[kani::proof]
+#[kani::unwind(4)]
+fn main() {
+    t1();
+    t2();
+}
+
+fn t1() {
+    let mut a = || {
+        let b = B;
+        if test() {
+            drop(b);
+        }
+        yield;
+    };
+
+    let n = A.load(Ordering::SeqCst);
+    Pin::new(&mut a).resume(());
+    assert_eq!(A.load(Ordering::SeqCst), n + 1);
+    Pin::new(&mut a).resume(());
+    assert_eq!(A.load(Ordering::SeqCst), n + 1);
+}
+
+fn t2() {
+    let mut a = || {
+        let b = B;
+        if test2() {
+            drop(b);
+        }
+        yield;
+    };
+
+    let n = A.load(Ordering::SeqCst);
+    Pin::new(&mut a).resume(());
+    assert_eq!(A.load(Ordering::SeqCst), n);
+    Pin::new(&mut a).resume(());
+    assert_eq!(A.load(Ordering::SeqCst), n + 1);
+}

tests/kani/Generator/rustc-generator-tests/conditional-drop.rs

@@ -0,0 +1,66 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/control-flow.rs
+
+// run-pass
+
+// revisions: default nomiropt
+//[nomiropt]compile-flags: -Z mir-opt-level=0
+
+#![feature(generators, generator_trait)]
+
+use std::marker::Unpin;
+use std::ops::{Generator, GeneratorState};
+use std::pin::Pin;
+
+fn finish<T>(mut amt: usize, mut t: T) -> T::Return
+where
+    T: Generator<(), Yield = ()> + Unpin,
+{
+    loop {
+        match Pin::new(&mut t).resume(()) {
+            GeneratorState::Yielded(()) => amt = amt.checked_sub(1).unwrap(),
+            GeneratorState::Complete(ret) => {
+                assert_eq!(amt, 0);
+                return ret;
+            }
+        }
+    }
+}
+
+#[kani::proof]
+#[kani::unwind(16)]
+fn main() {
+    finish(1, || yield);
+    finish(8, || {
+        for _ in 0..8 {
+            yield;
+        }
+    });
+    finish(1, || {
+        if true {
+            yield;
+        } else {
+        }
+    });
+    finish(1, || {
+        if false {
+        } else {
+            yield;
+        }
+    });
+    finish(2, || {
+        if {
+            yield;
+            false
+        } {
+            yield;
+            panic!()
+        }
+        yield
+    });
+}

tests/kani/Generator/rustc-generator-tests/control-flow.rs

@@ -0,0 +1,151 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/discriminant.rs
+
+// This test creates some large generators with around 256 variants, some of them need a u16 discriminant instead of u8.
+// This test ensures that we use the right discriminant type.
+
+//! Tests that generator discriminant sizes and ranges are chosen optimally and that they are
+//! reflected in the output of `mem::discriminant`.
+
+// run-pass
+
+#![feature(generators, generator_trait, core_intrinsics, discriminant_kind)]
+
+use std::intrinsics::discriminant_value;
+use std::marker::{DiscriminantKind, Unpin};
+use std::mem::size_of_val;
+use std::{cmp, ops::*};
+
+macro_rules! yield25 {
+    ($e:expr) => {
+        yield $e;
+        yield $e;
+        yield $e;
+        yield $e;
+        yield $e;
+
+        yield $e;
+        yield $e;
+        yield $e;
+        yield $e;
+        yield $e;
+
+        yield $e;
+        yield $e;
+        yield $e;
+        yield $e;
+        yield $e;
+
+        yield $e;
+        yield $e;
+        yield $e;
+        yield $e;
+        yield $e;
+
+        yield $e;
+        yield $e;
+        yield $e;
+        yield $e;
+        yield $e;
+    };
+}
+
+/// Yields 250 times.
+macro_rules! yield250 {
+    () => {
+        yield250!(())
+    };
+
+    ($e:expr) => {
+        yield25!($e);
+        yield25!($e);
+        yield25!($e);
+        yield25!($e);
+        yield25!($e);
+
+        yield25!($e);
+        yield25!($e);
+        yield25!($e);
+        yield25!($e);
+        yield25!($e);
+    };
+}
+
+fn cycle(
+    gen: impl Generator<()> + Unpin + DiscriminantKind<Discriminant = u32>,
+    expected_max_discr: u32,
+) {
+    let mut gen = Box::pin(gen);
+    let mut max_discr = 0;
+    loop {
+        max_discr = cmp::max(max_discr, discriminant_value(gen.as_mut().get_mut()));
+        match gen.as_mut().resume(()) {
+            GeneratorState::Yielded(_) => {}
+            GeneratorState::Complete(_) => {
+                assert_eq!(max_discr, expected_max_discr);
+                return;
+            }
+        }
+    }
+}
+
+#[kani::proof]
+#[kani::unwind(260)]
+fn main() {
+    // Has only one invalid discr. value.
+    let gen_u8_tiny_niche = || {
+        || {
+            // 3 reserved variants
+
+            yield250!(); // 253 variants
+
+            yield; // 254
+            yield; // 255
+        }
+    };
+
+    // Uses all values in the u8 discriminant.
+    let gen_u8_full = || {
+        || {
+            // 3 reserved variants
+
+            yield250!(); // 253 variants
+
+            yield; // 254
+            yield; // 255
+            yield; // 256
+        }
+    };
+
+    // Barely needs a u16 discriminant.
+    let gen_u16 = || {
+        || {
+            // 3 reserved variants
+
+            yield250!(); // 253 variants
+
+            yield; // 254
+            yield; // 255
+            yield; // 256
+            yield; // 257
+        }
+    };
+
+    // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395)
+    assert_eq!(size_of_val(&gen_u8_tiny_niche()), 1);
+    assert_eq!(size_of_val(&Some(gen_u8_tiny_niche())), 1); // uses niche
+    assert_eq!(size_of_val(&Some(Some(gen_u8_tiny_niche()))), 2); // cannot use niche anymore
+    assert_eq!(size_of_val(&gen_u8_full()), 1);
+    assert_eq!(size_of_val(&Some(gen_u8_full())), 2); // cannot use niche
+    assert_eq!(size_of_val(&gen_u16()), 2);
+    assert_eq!(size_of_val(&Some(gen_u16())), 2); // uses niche
+
+    cycle(gen_u8_tiny_niche(), 254);
+    cycle(gen_u8_full(), 255);
+    cycle(gen_u16(), 256);
+}

tests/kani/Generator/rustc-generator-tests/discriminant_fixme.rs

@@ -0,0 +1,75 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/env-drop.rs
+
+// run-pass
+
+// revisions: default nomiropt
+//[nomiropt]compile-flags: -Z mir-opt-level=0
+
+#![feature(generators, generator_trait)]
+
+use std::ops::Generator;
+use std::pin::Pin;
+use std::sync::atomic::{AtomicUsize, Ordering};
+
+static A: AtomicUsize = AtomicUsize::new(0);
+
+struct B;
+
+impl Drop for B {
+    fn drop(&mut self) {
+        A.fetch_add(1, Ordering::SeqCst);
+    }
+}
+
+#[kani::proof]
+fn main() {
+    t1();
+    t2();
+    t3();
+}
+
+fn t1() {
+    let b = B;
+    let mut foo = || {
+        yield;
+        drop(b);
+    };
+
+    let n = A.load(Ordering::SeqCst);
+    drop(Pin::new(&mut foo).resume(()));
+    assert_eq!(A.load(Ordering::SeqCst), n);
+    drop(foo);
+    assert_eq!(A.load(Ordering::SeqCst), n + 1);
+}
+
+fn t2() {
+    let b = B;
+    let mut foo = || {
+        yield b;
+    };
+
+    let n = A.load(Ordering::SeqCst);
+    drop(Pin::new(&mut foo).resume(()));
+    assert_eq!(A.load(Ordering::SeqCst), n + 1);
+    drop(foo);
+    assert_eq!(A.load(Ordering::SeqCst), n + 1);
+}
+
+fn t3() {
+    let b = B;
+    let foo = || {
+        yield;
+        drop(b);
+    };
+
+    let n = A.load(Ordering::SeqCst);
+    assert_eq!(A.load(Ordering::SeqCst), n);
+    drop(foo);
+    assert_eq!(A.load(Ordering::SeqCst), n + 1);
+}

tests/kani/Generator/rustc-generator-tests/env-drop.rs

@@ -0,0 +1,54 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/iterator-count.rs
+
+// run-pass
+
+#![feature(generators, generator_trait)]
+
+use std::marker::Unpin;
+use std::ops::{Generator, GeneratorState};
+use std::pin::Pin;
+
+struct W<T>(T);
+
+// This impl isn't safe in general, but the generator used in this test is movable
+// so it won't cause problems.
+impl<T: Generator<(), 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),
+        }
+    }
+}
+
+fn test() -> impl Generator<(), Return = (), Yield = u8> + Unpin {
+    || {
+        for i in 1..6 {
+            yield i
+        }
+    }
+}
+
+#[kani::proof]
+#[kani::unwind(11)]
+fn main() {
+    let end = 11;
+
+    let closure_test = |start| {
+        move || {
+            for i in start..end {
+                yield i
+            }
+        }
+    };
+
+    assert!(W(test()).chain(W(closure_test(6))).eq(1..11));
+}

tests/kani/Generator/rustc-generator-tests/iterator-count.rs

@@ -0,0 +1,24 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/live-upvar-across-yield.rs
+
+// run-pass
+
+#![feature(generators, generator_trait)]
+
+use std::ops::Generator;
+use std::pin::Pin;
+
+#[kani::proof]
+#[kani::unwind(2)]
+fn main() {
+    let b = |_| 3;
+    let mut a = || {
+        b(yield);
+    };
+    Pin::new(&mut a).resume(());
+}

tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs

@@ -0,0 +1,30 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/nested-generators.rs
+
+// run-pass
+
+#![feature(generators, generator_trait)]
+
+use std::ops::{Generator, GeneratorState};
+use std::pin::Pin;
+
+#[kani::proof]
+fn main() {
+    let _generator = || {
+        let mut sub_generator = || {
+            yield 2;
+        };
+
+        match Pin::new(&mut sub_generator).resume(()) {
+            GeneratorState::Yielded(x) => {
+                yield x;
+            }
+            _ => panic!(),
+        };
+    };
+}

tests/kani/Generator/rustc-generator-tests/nested-generators.rs

@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/niche-in-generator.rs
+
+// Test that niche finding works with captured generator upvars.
+
+// run-pass
+
+#![feature(generators, generator_trait)]
+
+use std::ops::{Generator, GeneratorState};
+use std::pin::Pin;
+
+use std::mem::size_of_val;
+
+fn take<T>(_: T) {}
+
+#[kani::proof]
+fn main() {
+    let x = false;
+    let mut gen1 = || {
+        yield;
+        take(x);
+    };
+
+    // FIXME: for some reason, these asserts are very hard for CBMC to figure out
+    // Kani didn't terminate within 5 minutes.
+    // assert_eq!(Pin::new(&mut gen1).resume(()), GeneratorState::Yielded(()));
+    // assert_eq!(Pin::new(&mut gen1).resume(()), GeneratorState::Complete(()));
+    assert!(false); // to make the test fail without taking forever
+}

tests/kani/Generator/rustc-generator-tests/niche-in-generator-slow_fixme.rs

@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/niche-in-generator.rs
+
+// Test that niche finding works with captured generator upvars.
+
+// run-pass
+
+#![feature(generators)]
+
+use std::mem::size_of_val;
+
+fn take<T>(_: T) {}
+
+#[kani::proof]
+fn main() {
+    let x = false;
+    let gen1 = || {
+        yield;
+        take(x);
+    };
+
+    // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395)
+    assert_eq!(size_of_val(&gen1), size_of_val(&Some(gen1)));
+}

tests/kani/Generator/rustc-generator-tests/niche-in-generator_fixme.rs

@@ -0,0 +1,42 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/overlap-locals.rs
+
+// run-pass
+
+#![feature(generators, generator_trait)]
+
+use std::ops::{Generator, GeneratorState};
+use std::pin::Pin;
+
+#[kani::proof]
+fn main() {
+    let mut a = || {
+        {
+            let w: i32 = 4;
+            yield;
+        }
+        {
+            let x: i32 = 5;
+            yield;
+        }
+        {
+            let y: i32 = 6;
+            yield;
+        }
+        {
+            let z: i32 = 7;
+            yield;
+        }
+    };
+
+    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(()));
+}

tests/kani/Generator/rustc-generator-tests/overlap-locals.rs

@@ -0,0 +1,40 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/overlap-locals.rs
+
+// run-pass
+
+#![feature(generators)]
+
+#[kani::proof]
+fn main() {
+    let a = || {
+        {
+            let w: i32 = 4;
+            yield;
+            println!("{:?}", w);
+        }
+        {
+            let x: i32 = 5;
+            yield;
+            println!("{:?}", x);
+        }
+        {
+            let y: i32 = 6;
+            yield;
+            println!("{:?}", y);
+        }
+        {
+            let z: i32 = 7;
+            yield;
+            println!("{:?}", z);
+        }
+    };
+
+    // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395)
+    assert_eq!(8, std::mem::size_of_val(&a));
+}

tests/kani/Generator/rustc-generator-tests/overlap-locals_fixme.rs

@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/resume-arg-size.rs
+
+#![feature(generators)]
+
+// run-pass
+
+use std::mem::size_of_val;
+
+#[kani::proof]
+fn main() {
+    // Generator taking a `Copy`able resume arg.
+    let gen_copy = |mut x: usize| {
+        loop {
+            drop(x);
+            x = yield;
+        }
+    };
+
+    // Generator taking a non-`Copy` resume arg.
+    let gen_move = |mut x: Box<usize>| {
+        loop {
+            drop(x);
+            x = yield;
+        }
+    };
+
+    // Neither of these generators 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)
+    assert_eq!(size_of_val(&gen_copy), 1);
+    assert_eq!(size_of_val(&gen_move), 1);
+}

tests/kani/Generator/rustc-generator-tests/resume-arg-size_fixme.rs

@@ -0,0 +1,41 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/resume-arg-size.rs
+
+#![feature(generators, generator_trait)]
+
+use std::ops::{Generator, GeneratorState};
+use std::pin::Pin;
+
+// run-pass
+
+use std::mem::size_of_val;
+
+#[kani::proof]
+fn main() {
+    // Generator taking a `Copy`able resume arg.
+    let mut gen_copy = |mut x: usize| {
+        loop {
+            drop(x);
+            x = yield;
+        }
+    };
+
+    // Generator taking a non-`Copy` resume arg.
+    let mut gen_move = |mut x: Box<usize>| {
+        loop {
+            drop(x);
+            x = yield;
+        }
+    };
+
+    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_move).resume(Box::new(0)), GeneratorState::Yielded(()));
+    assert_eq!(Pin::new(&mut gen_move).resume(Box::new(1)), GeneratorState::Yielded(()));
+}

tests/kani/Generator/rustc-generator-tests/resume-arg.rs

@@ -0,0 +1,55 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/resume-live-across-yield.rs
+
+// run-pass
+
+#![feature(generators, generator_trait)]
+
+use std::ops::{Generator, GeneratorState};
+use std::pin::Pin;
+use std::sync::atomic::{AtomicUsize, Ordering};
+
+static DROP: AtomicUsize = AtomicUsize::new(0);
+
+#[derive(PartialEq, Eq, Debug)]
+struct Dropper(String);
+
+impl Drop for Dropper {
+    fn drop(&mut self) {
+        DROP.fetch_add(1, Ordering::SeqCst);
+    }
+}
+
+#[kani::proof]
+#[kani::unwind(16)]
+fn main() {
+    let mut g = |mut _d| {
+        _d = yield;
+        _d
+    };
+
+    let mut g = Pin::new(&mut g);
+
+    assert_eq!(
+        g.as_mut().resume(Dropper(String::from("Hello world!"))),
+        GeneratorState::Yielded(())
+    );
+    assert_eq!(DROP.load(Ordering::Acquire), 0);
+    match g.as_mut().resume(Dropper(String::from("Number Two"))) {
+        GeneratorState::Complete(dropper) => {
+            assert_eq!(DROP.load(Ordering::Acquire), 1);
+            assert_eq!(dropper.0, "Number Two");
+            drop(dropper);
+            assert_eq!(DROP.load(Ordering::Acquire), 2);
+        }
+        _ => unreachable!(),
+    }
+
+    drop(g);
+    assert_eq!(DROP.load(Ordering::Acquire), 2);
+}

tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs

@@ -0,0 +1,136 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/size-moved-locals.rs
+
+// run-pass
+// Test that we don't duplicate storage for a variable that is moved to another
+// binding. This used to happen in the presence of unwind and drop edges (see
+// `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
+// (which would indicate it is reserving space for two copies of Foo.)
+//
+// See issue #59123 for a full explanation.
+
+// edition:2018
+// ignore-wasm32 issue #62807
+// ignore-asmjs issue #62807
+
+#![feature(generators, generator_trait)]
+
+use std::ops::{Generator, GeneratorState};
+use std::pin::Pin;
+
+const FOO_SIZE: usize = 1024;
+struct Foo([u8; FOO_SIZE]);
+
+impl Drop for Foo {
+    fn drop(&mut self) {}
+}
+
+fn move_before_yield() -> impl Generator<Yield = (), Return = ()> {
+    static || {
+        let first = Foo([0; FOO_SIZE]);
+        let _second = first;
+        yield;
+        // _second dropped here
+    }
+}
+
+fn noop() {}
+
+fn move_before_yield_with_noop() -> impl Generator<Yield = (), Return = ()> {
+    static || {
+        let first = Foo([0; FOO_SIZE]);
+        noop();
+        let _second = first;
+        yield;
+        // _second dropped here
+    }
+}
+
+// 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 = ()> {
+    static || {
+        let first = Foo([0; FOO_SIZE]);
+        yield;
+        let second = first;
+        yield;
+        let _third = second;
+        yield;
+    }
+}
+
+fn overlap_x_and_y() -> impl Generator<Yield = (), Return = ()> {
+    static || {
+        let x = Foo([0; FOO_SIZE]);
+        yield;
+        drop(x);
+        let y = Foo([0; FOO_SIZE]);
+        yield;
+        drop(y);
+    }
+}
+
+#[kani::proof]
+fn main() {
+    // FIXME: the following tests are very slow (did not terminate in a couple of minutes)
+    /* let mut generator = move_before_yield();
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Yielded(())
+    );
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Complete(())
+    );
+
+    let mut generator = move_before_yield_with_noop();
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Yielded(())
+    );
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Complete(())
+    );
+
+    let mut generator = overlap_move_points();
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Yielded(())
+    );
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Yielded(())
+    );
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Yielded(())
+    );
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Complete(())
+    );
+
+    let mut generator = overlap_x_and_y();
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Yielded(())
+    );
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Yielded(())
+    );
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Complete(())
+    ); */
+    assert!(false); // to make the test fail without taking forever
+}

tests/kani/Generator/rustc-generator-tests/size-moved-locals-slow_fixme.rs

@@ -0,0 +1,90 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/size-moved-locals.rs
+
+// run-pass
+// Test that we don't duplicate storage for a variable that is moved to another
+// binding. This used to happen in the presence of unwind and drop edges (see
+// `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
+// (which would indicate it is reserving space for two copies of Foo.)
+//
+// See issue #59123 for a full explanation.
+
+// edition:2018
+// ignore-wasm32 issue #62807
+// ignore-asmjs issue #62807
+
+#![feature(generators, generator_trait)]
+
+use std::ops::Generator;
+
+const FOO_SIZE: usize = 1024;
+struct Foo([u8; FOO_SIZE]);
+
+impl Drop for Foo {
+    fn drop(&mut self) {}
+}
+
+fn move_before_yield() -> impl Generator<Yield = (), Return = ()> {
+    static || {
+        let first = Foo([0; FOO_SIZE]);
+        let _second = first;
+        yield;
+        // _second dropped here
+    }
+}
+
+fn noop() {}
+
+fn move_before_yield_with_noop() -> impl Generator<Yield = (), Return = ()> {
+    static || {
+        let first = Foo([0; FOO_SIZE]);
+        noop();
+        let _second = first;
+        yield;
+        // _second dropped here
+    }
+}
+
+// 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 = ()> {
+    static || {
+        let first = Foo([0; FOO_SIZE]);
+        yield;
+        let second = first;
+        yield;
+        let _third = second;
+        yield;
+    }
+}
+
+fn overlap_x_and_y() -> impl Generator<Yield = (), Return = ()> {
+    static || {
+        let x = Foo([0; FOO_SIZE]);
+        yield;
+        drop(x);
+        let y = Foo([0; FOO_SIZE]);
+        yield;
+        drop(y);
+    }
+}
+
+#[kani::proof]
+fn main() {
+    // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395)
+    assert_eq!(1025, std::mem::size_of_val(&move_before_yield()));
+    // The following assertion fails for some reason (tracking issue: https://github.com/model-checking/kani/issues/1395).
+    // But it also fails for WASM (https://github.com/rust-lang/rust/issues/62807),
+    // so it is probably not a big problem:
+    assert_eq!(1026, std::mem::size_of_val(&move_before_yield_with_noop()));
+    assert_eq!(2051, std::mem::size_of_val(&overlap_move_points()));
+    assert_eq!(1026, std::mem::size_of_val(&overlap_x_and_y()));
+}

tests/kani/Generator/rustc-generator-tests/size-moved-locals_fixme.rs

@@ -0,0 +1,110 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/smoke-resume-args.rs
+
+// run-pass
+
+// revisions: default nomiropt
+//[nomiropt]compile-flags: -Z mir-opt-level=0
+
+#![feature(generators, generator_trait)]
+
+use std::fmt::Debug;
+use std::marker::Unpin;
+use std::ops::{
+    Generator,
+    GeneratorState::{self, *},
+};
+use std::pin::Pin;
+use std::sync::atomic::{AtomicUsize, Ordering};
+
+fn drain<G: Generator<R, Yield = Y> + Unpin, R, Y>(
+    gen: &mut G,
+    inout: Vec<(R, GeneratorState<Y, G::Return>)>,
+) where
+    Y: Debug + PartialEq,
+    G::Return: Debug + PartialEq,
+{
+    let mut gen = Pin::new(gen);
+
+    for (input, out) in inout {
+        assert_eq!(gen.as_mut().resume(input), out);
+    }
+}
+
+static DROPS: AtomicUsize = AtomicUsize::new(0);
+
+#[derive(Debug, PartialEq)]
+struct DropMe;
+
+impl Drop for DropMe {
+    fn drop(&mut self) {
+        DROPS.fetch_add(1, Ordering::SeqCst);
+    }
+}
+
+fn expect_drops<T>(expected_drops: usize, f: impl FnOnce() -> T) -> T {
+    DROPS.store(0, Ordering::SeqCst);
+
+    let res = f();
+
+    let actual_drops = DROPS.load(Ordering::SeqCst);
+    assert_eq!(actual_drops, expected_drops);
+    res
+}
+
+#[kani::proof]
+#[kani::unwind(8)]
+fn main() {
+    drain(
+        &mut |mut b| {
+            while b != 0 {
+                b = yield (b + 1);
+            }
+            -1
+        },
+        vec![(1, Yielded(2)), (-45, Yielded(-44)), (500, Yielded(501)), (0, Complete(-1))],
+    );
+
+    expect_drops(2, || drain(&mut |a| yield a, vec![(DropMe, Yielded(DropMe))]));
+
+    expect_drops(6, || {
+        drain(
+            &mut |a| yield yield a,
+            vec![(DropMe, Yielded(DropMe)), (DropMe, Yielded(DropMe)), (DropMe, Complete(DropMe))],
+        )
+    });
+
+    #[allow(unreachable_code)]
+    expect_drops(2, || drain(&mut |a| yield return a, vec![(DropMe, Complete(DropMe))]));
+
+    expect_drops(2, || {
+        drain(
+            &mut |a: DropMe| {
+                if false { yield () } else { a }
+            },
+            vec![(DropMe, Complete(DropMe))],
+        )
+    });
+
+    expect_drops(4, || {
+        drain(
+            #[allow(unused_assignments, unused_variables)]
+            &mut |mut a: DropMe| {
+                a = yield;
+                a = yield;
+                a = yield;
+            },
+            vec![
+                (DropMe, Yielded(())),
+                (DropMe, Yielded(())),
+                (DropMe, Yielded(())),
+                (DropMe, Complete(())),
+            ],
+        )
+    });
+}

tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs

@@ -0,0 +1,191 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/smoke.rs
+
+// run-pass
+
+// revisions: default nomiropt
+//[nomiropt]compile-flags: -Z mir-opt-level=0
+
+// ignore-emscripten no threads support
+// compile-flags: --test
+
+#![feature(generators, generator_trait)]
+
+use std::ops::{Generator, GeneratorState};
+use std::pin::Pin;
+use std::thread;
+
+#[kani::proof]
+fn simple() {
+    let mut foo = || {
+        if false {
+            yield;
+        }
+    };
+
+    match Pin::new(&mut foo).resume(()) {
+        GeneratorState::Complete(()) => {}
+        s => panic!("bad state: {:?}", s),
+    }
+}
+
+#[kani::proof]
+#[kani::unwind(4)]
+fn return_capture() {
+    let a = String::from("foo");
+    let mut foo = || {
+        if false {
+            yield;
+        }
+        a
+    };
+
+    match Pin::new(&mut foo).resume(()) {
+        GeneratorState::Complete(ref s) if *s == "foo" => {}
+        s => panic!("bad state: {:?}", s),
+    }
+}
+
+#[kani::proof]
+fn simple_yield() {
+    let mut foo = || {
+        yield;
+    };
+
+    match Pin::new(&mut foo).resume(()) {
+        GeneratorState::Yielded(()) => {}
+        s => panic!("bad state: {:?}", s),
+    }
+    match Pin::new(&mut foo).resume(()) {
+        GeneratorState::Complete(()) => {}
+        s => panic!("bad state: {:?}", s),
+    }
+}
+
+#[kani::proof]
+#[kani::unwind(4)]
+fn yield_capture() {
+    let b = String::from("foo");
+    let mut foo = || {
+        yield b;
+    };
+
+    match Pin::new(&mut foo).resume(()) {
+        GeneratorState::Yielded(ref s) if *s == "foo" => {}
+        s => panic!("bad state: {:?}", s),
+    }
+    match Pin::new(&mut foo).resume(()) {
+        GeneratorState::Complete(()) => {}
+        s => panic!("bad state: {:?}", s),
+    }
+}
+
+#[kani::proof]
+#[kani::unwind(4)]
+fn simple_yield_value() {
+    let mut foo = || {
+        yield String::from("bar");
+        return String::from("foo");
+    };
+
+    match Pin::new(&mut foo).resume(()) {
+        GeneratorState::Yielded(ref s) if *s == "bar" => {}
+        s => panic!("bad state: {:?}", s),
+    }
+    match Pin::new(&mut foo).resume(()) {
+        GeneratorState::Complete(ref s) if *s == "foo" => {}
+        s => panic!("bad state: {:?}", s),
+    }
+}
+
+#[kani::proof]
+#[kani::unwind(4)]
+fn return_after_yield() {
+    let a = String::from("foo");
+    let mut foo = || {
+        yield;
+        return a;
+    };
+
+    match Pin::new(&mut foo).resume(()) {
+        GeneratorState::Yielded(()) => {}
+        s => panic!("bad state: {:?}", s),
+    }
+    match Pin::new(&mut foo).resume(()) {
+        GeneratorState::Complete(ref s) if *s == "foo" => {}
+        s => panic!("bad state: {:?}", s),
+    }
+}
+
+// This test is useless for Kani
+fn send_and_sync() {
+    assert_send_sync(|| yield);
+    assert_send_sync(|| {
+        yield String::from("foo");
+    });
+    assert_send_sync(|| {
+        yield;
+        return String::from("foo");
+    });
+    let a = 3;
+    assert_send_sync(|| {
+        yield a;
+        return;
+    });
+    let a = 3;
+    assert_send_sync(move || {
+        yield a;
+        return;
+    });
+    let a = String::from("a");
+    assert_send_sync(|| {
+        yield;
+        drop(a);
+        return;
+    });
+    let a = String::from("a");
+    assert_send_sync(move || {
+        yield;
+        drop(a);
+        return;
+    });
+
+    fn assert_send_sync<T: Send + Sync>(_: T) {}
+}
+
+// Kani does not support threads, so we cannot run this test:
+fn send_over_threads() {
+    let mut foo = || yield;
+    thread::spawn(move || {
+        match Pin::new(&mut foo).resume(()) {
+            GeneratorState::Yielded(()) => {}
+            s => panic!("bad state: {:?}", s),
+        }
+        match Pin::new(&mut foo).resume(()) {
+            GeneratorState::Complete(()) => {}
+            s => panic!("bad state: {:?}", s),
+        }
+    })
+    .join()
+    .unwrap();
+
+    let a = String::from("a");
+    let mut foo = || yield a;
+    thread::spawn(move || {
+        match Pin::new(&mut foo).resume(()) {
+            GeneratorState::Yielded(ref s) if *s == "a" => {}
+            s => panic!("bad state: {:?}", s),
+        }
+        match Pin::new(&mut foo).resume(()) {
+            GeneratorState::Complete(()) => {}
+            s => panic!("bad state: {:?}", s),
+        }
+    })
+    .join()
+    .unwrap();
+}

tests/kani/Generator/rustc-generator-tests/smoke.rs

@@ -0,0 +1,30 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/static-generator.rs
+
+// run-pass
+
+#![feature(generators, generator_trait)]
+
+use std::ops::{Generator, GeneratorState};
+use std::pin::Pin;
+
+#[kani::proof]
+#[kani::unwind(2)]
+fn main() {
+    let mut generator = 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
+    // 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(()));
+}

tests/kani/Generator/rustc-generator-tests/static-generator.rs

@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/yield-in-box.rs
+
+// run-pass
+// Test that box-statements with yields in them work.
+
+#![feature(generators, box_syntax, generator_trait)]
+use std::ops::Generator;
+use std::ops::GeneratorState;
+use std::pin::Pin;
+
+#[kani::proof]
+#[kani::unwind(2)]
+fn main() {
+    let x = 0i32;
+    || {
+        //~ WARN unused generator that must be used
+        let y = 2u32;
+        {
+            let _t = box (&x, yield 0, &y);
+        }
+        match box (&x, yield 0, &y) {
+            _t => {}
+        }
+    };
+
+    let mut g = |_| box yield;
+    assert_eq!(Pin::new(&mut g).resume(1), GeneratorState::Yielded(()));
+    assert_eq!(Pin::new(&mut g).resume(2), GeneratorState::Complete(box 2));
+}