Upgrade toolchain to 2024-12-15

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

@@ -283,6 +283,16 @@ impl GotocCtx<'_> {
                             .member("direct_fields", &self.symbol_table)
                             .member(field_name, &self.symbol_table))
                     }
+                    TyKind::RigidTy(RigidTy::CoroutineClosure(def, args)) => {
+                        let typ = Ty::new_coroutine_closure(def, args);
+                        let goto_typ = self.codegen_ty_stable(typ);
+                        Err(UnimplementedData::new(
+                            "Coroutine closures",
+                            "https://github.com/model-checking/kani/issues/3783",
+                            goto_typ,
+                            *parent_expr.location(),
+                        ))
+                    }
                     TyKind::RigidTy(RigidTy::Str)
                     | TyKind::RigidTy(RigidTy::Array(_, _))
                     | TyKind::RigidTy(RigidTy::Slice(_))

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

@@ -729,6 +729,15 @@ impl GotocCtx<'_> {
                 }
             }
             AggregateKind::Coroutine(_, _, _) => self.codegen_rvalue_coroutine(&operands, res_ty),
+            AggregateKind::CoroutineClosure(_, _) => {
+                let ty = self.codegen_ty_stable(res_ty);
+                self.codegen_unimplemented_expr(
+                    "CoroutineClosure",
+                    ty,
+                    loc,
+                    "https://github.com/model-checking/kani/issues/3783",
+                )
+            }
         }
     }
 

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

@@ -590,6 +590,9 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             ty::Closure(_, subst) => self.codegen_ty_closure(ty, subst),
             ty::Coroutine(..) => self.codegen_ty_coroutine(ty),
+            ty::CoroutineClosure(..) => unimplemented!(
+                "Kani does not yet support coroutine closures. Please post your example at https://github.com/model-checking/kani/issues/3783"
+            ),
             ty::Never => self.ensure_struct(NEVER_TYPE_EMPTY_STRUCT_NAME, "!", |_, _| vec![]),
             ty::Tuple(ts) => {
                 if ts.is_empty() {
@@ -619,11 +622,7 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Bound(_, _) | ty::Param(_) => unreachable!("monomorphization bug"),
 
             // type checking remnants which shouldn't be reachable
-            ty::CoroutineWitness(_, _)
-            | ty::CoroutineClosure(_, _)
-            | ty::Infer(_)
-            | ty::Placeholder(_)
-            | ty::Error(_) => {
+            ty::CoroutineWitness(_, _) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => {
                 unreachable!("remnants of type checking")
             }
         }
@@ -879,7 +878,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// 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 coroutine.
+    /// The field `discriminant_field` should be `Some(idx)` when generating the variant for the direct (top-level) 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 coroutine because those don't contain the discriminant as a field.
     fn codegen_coroutine_variant_struct(

kani-compiler/src/kani_middle/points_to/points_to_analysis.rs

@@ -136,7 +136,7 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> {
 
     /// Update current dataflow state based on the information we can infer from the given
     /// statement.
-    fn apply_statement_effect(
+    fn apply_primary_statement_effect(
         &mut self,
         state: &mut Self::Domain,
         statement: &Statement<'tcx>,
@@ -184,7 +184,7 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> {
         }
     }
 
-    fn apply_terminator_effect<'mir>(
+    fn apply_primary_terminator_effect<'mir>(
         &mut self,
         state: &mut Self::Domain,
         terminator: &'mir Terminator<'tcx>,

kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs

@@ -393,6 +393,7 @@ fn data_bytes_for_ty(
                 | RigidTy::FnPtr(_)
                 | RigidTy::Closure(_, _)
                 | RigidTy::Coroutine(_, _, _)
+                | RigidTy::CoroutineClosure(_, _)
                 | RigidTy::CoroutineWitness(_, _)
                 | RigidTy::Foreign(_)
                 | RigidTy::Dynamic(_, _, _) => Err(LayoutComputationError::UnsupportedType(ty)),

kani-compiler/src/kani_middle/transform/check_values.rs

@@ -640,6 +640,7 @@ impl MirVisitor for CheckValueVisitor<'_, '_> {
                 AggregateKind::Array(_)
                 | AggregateKind::Closure(_, _)
                 | AggregateKind::Coroutine(_, _, _)
+                | AggregateKind::CoroutineClosure(_, _)
                 | AggregateKind::RawPtr(_, _)
                 | AggregateKind::Tuple => {}
             },
@@ -981,6 +982,7 @@ pub fn ty_validity_per_offset(
                 | RigidTy::FnPtr(_)
                 | RigidTy::Closure(_, _)
                 | RigidTy::Coroutine(_, _, _)
+                | RigidTy::CoroutineClosure(_, _)
                 | RigidTy::CoroutineWitness(_, _)
                 | RigidTy::Foreign(_)
                 | RigidTy::Dynamic(_, _, _) => Err(format!("Unsupported {ty:?}")),

kani-compiler/src/kani_middle/transform/internal_mir.rs

@@ -56,6 +56,12 @@ impl RustcInternalMir for AggregateKind {
                     internal(tcx, generic_args),
                 )
             }
+            AggregateKind::CoroutineClosure(coroutine_def, generic_args) => {
+                rustc_middle::mir::AggregateKind::CoroutineClosure(
+                    internal(tcx, coroutine_def.0),
+                    internal(tcx, generic_args),
+                )
+            }
             AggregateKind::RawPtr(ty, mutability) => rustc_middle::mir::AggregateKind::RawPtr(
                 internal(tcx, ty),
                 internal(tcx, mutability),

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-12-14"
+channel = "nightly-2024-12-15"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]