Implement support for generators

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()