Upgrade toolchain to nightly-2023-01-23

to overcome an issue with async generators. Updated the
codegen_generator to follow the new logic implemented in
rust-lang/rust#105977

Author: celinval

kani-compiler/kani_queries/src/lib.rs

@@ -15,27 +15,22 @@ use {
     std::sync::{Arc, Mutex},
 };
 
-#[derive(Debug, Clone, Copy, AsRefStr, EnumString, EnumVariantNames, PartialEq, Eq)]
+#[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, EnumVariantNames, PartialEq, Eq)]
 #[strum(serialize_all = "snake_case")]
 pub enum ReachabilityType {
     /// Start the cross-crate reachability analysis from all harnesses in the local crate.
     Harnesses,
     /// Use standard rustc monomorphizer algorithm.
     Legacy,
     /// Don't perform any reachability analysis. This will skip codegen for this crate.
+    #[default]
     None,
     /// Start the cross-crate reachability analysis from all public functions in the local crate.
     PubFns,
     /// Start the cross-crate reachability analysis from all *test* (i.e. `#[test]`) harnesses in the local crate.
     Tests,
 }
 
-impl Default for ReachabilityType {
-    fn default() -> Self {
-        ReachabilityType::None
-    }
-}
-
 pub trait UserInput {
     fn set_emit_vtable_restrictions(&mut self, restrictions: bool);
     fn get_emit_vtable_restrictions(&self) -> bool;

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

@@ -358,20 +358,41 @@ impl<'tcx> GotocCtx<'tcx> {
         // `Generator::resume(...) -> GeneratorState` function in case we
         // have an ordinary generator, or the `Future::poll(...) -> Poll`
         // function in case this is a special generator backing an async construct.
-        let ret_ty = if self.tcx.generator_is_async(*did) {
-            let state_did = self.tcx.require_lang_item(LangItem::Poll, None);
-            let state_adt_ref = self.tcx.adt_def(state_did);
-            let state_substs = self.tcx.intern_substs(&[sig.return_ty.into()]);
-            self.tcx.mk_adt(state_adt_ref, state_substs)
+        let tcx = self.tcx;
+        let (resume_ty, ret_ty) = if tcx.generator_is_async(*did) {
+            // The signature should be `Future::poll(_, &mut Context<'_>) -> Poll<Output>`
+            let poll_did = tcx.require_lang_item(LangItem::Poll, None);
+            let poll_adt_ref = tcx.adt_def(poll_did);
+            let poll_substs = tcx.intern_substs(&[sig.return_ty.into()]);
+            let ret_ty = tcx.mk_adt(poll_adt_ref, poll_substs);
+
+            // We have to replace the `ResumeTy` that is used for type and borrow checking
+            // with `&mut Context<'_>` which is used in codegen.
+            #[cfg(debug_assertions)]
+            {
+                if let ty::Adt(resume_ty_adt, _) = sig.resume_ty.kind() {
+                    let expected_adt = tcx.adt_def(tcx.require_lang_item(LangItem::ResumeTy, None));
+                    assert_eq!(*resume_ty_adt, expected_adt);
+                } else {
+                    panic!("expected `ResumeTy`, found `{:?}`", sig.resume_ty);
+                };
+            }
+            let context_mut_ref = tcx.mk_task_context();
+
+            (context_mut_ref, ret_ty)
         } else {
-            let state_did = self.tcx.require_lang_item(LangItem::GeneratorState, None);
-            let state_adt_ref = self.tcx.adt_def(state_did);
-            let state_substs = self.tcx.intern_substs(&[sig.yield_ty.into(), sig.return_ty.into()]);
-            self.tcx.mk_adt(state_adt_ref, state_substs)
+            // The signature should be `Generator::resume(_, Resume) -> GeneratorState<Yield, Return>`
+            let state_did = tcx.require_lang_item(LangItem::GeneratorState, None);
+            let state_adt_ref = tcx.adt_def(state_did);
+            let state_substs = tcx.intern_substs(&[sig.yield_ty.into(), sig.return_ty.into()]);
+            let ret_ty = tcx.mk_adt(state_adt_ref, state_substs);
+
+            (sig.resume_ty, ret_ty)
         };
+
         ty::Binder::bind_with_vars(
-            self.tcx.mk_fn_sig(
-                [env_ty, sig.resume_ty].iter(),
+            tcx.mk_fn_sig(
+                [env_ty, resume_ty].iter(),
                 &ret_ty,
                 false,
                 Unsafety::Normal,

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-01-16"
+channel = "nightly-2023-01-23"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

tests/cargo-kani/vecdeque-cve/src/abstract_vecdeque.rs

@@ -275,8 +275,8 @@ impl AbstractRawVec {
 
 fn handle_reserve(result: Result<(), TryReserveError>) {
     match result.map_err(|e| e.kind()) {
-        Err(CapacityOverflow) => capacity_overflow(),
-        Err(AllocError) => handle_alloc_error(),
+        Err(TryReserveErrorKind::CapacityOverflow) => capacity_overflow(),
+        Err(TryReserveErrorKind::AllocError) => handle_alloc_error(),
         Ok(()) => { /* yay */ }
     }
 }

tests/ui/code-location/expected

@@ -1,6 +1,6 @@
 module/mod.rs:10:5 in function module::not_empty
 main.rs:13:5 in function same_file
 /toolchains/
-alloc/src/vec/mod.rs:3054:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
+alloc/src/vec/mod.rs:3059:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
 
 VERIFICATION:- SUCCESSFUL