diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 3dccbea5837f..b6189c070538 100644 --- 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 index 68c174ae2119..d13597794d19 100644 --- 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 index 903baf8eaced..748eb42e7655 100644 --- 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 index 369296db6ed4..345a27309b50 100644 --- 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 index 8a9e3ac094d5..0a1fc16dcc07 100644 --- 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 index 5d66d00cf094..2276906aae81 100644 --- 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 index d29a5e688d2c..4f1095cce06e 100644 --- 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 index c4f751d10526..62deebf7a7d2 100644 --- 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"]