Upgrade toolchain to 2024-12-15 (#3784)

Culprit PRs: - rust-lang/rust#133938, specifically rust-lang/rust@1d56943 - rust-lang/rust#134295 For coroutine closures, I opened #3783 to track feature support--adding support for this appears non-trivial, and I didn't want to block toolchain upgrades on it. Resolves #3781 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
model-checking · Dec 16, 2024 · e6f6d7d · e6f6d7d
1 parent d253bda
commit e6f6d7d
Show file tree

Hide file tree

Showing 8 changed files with 36 additions and 9 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/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(_))

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/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",
+                )
+            }
         }
     }
 

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/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(

diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/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>,

diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs b/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)),

diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/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:?}")),

diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/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),

diff --git a/rust-toolchain.toml b/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"]