Upgrade toolchain to nightly-2023-01-16

This commit fixes compilation errors but not runtime ones. Related changes: rust-lang/rust#104986 rust-lang/rust#105657 rust-lang/rust#105603 rust-lang/rust#105613
celinval · Jan 23, 2023 · 379413f · 379413f
1 parent 55fe61c
commit 379413f
Show file tree

Hide file tree

Showing 6 changed files with 13 additions and 13 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -365,7 +365,9 @@ impl<'tcx> GotocCtx<'tcx> {
             "add_with_overflow" => codegen_op_with_overflow!(add_overflow_result),
             "arith_offset" => self.codegen_offset(intrinsic, instance, fargs, p, loc),
             "assert_inhabited" => self.codegen_assert_intrinsic(instance, intrinsic, span),
-            "assert_uninit_valid" => self.codegen_assert_intrinsic(instance, intrinsic, span),
+            "assert_mem_uninitialized_valid" => {
+                self.codegen_assert_intrinsic(instance, intrinsic, span)
+            }
             "assert_zero_valid" => self.codegen_assert_intrinsic(instance, intrinsic, span),
             // https://doc.rust-lang.org/core/intrinsics/fn.assume.html
             // Informs the optimizer that a condition is always true.

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -243,7 +243,8 @@ impl<'tcx> GotocCtx<'tcx> {
         match t {
             TypeOrVariant::Type(t) => {
                 match t.kind() {
-                    ty::Bool
+                    ty::Alias(..)
+                    | ty::Bool
                     | ty::Char
                     | ty::Int(_)
                     | ty::Uint(_)
@@ -254,10 +255,8 @@ impl<'tcx> GotocCtx<'tcx> {
                     | ty::GeneratorWitness(..)
                     | ty::Foreign(..)
                     | ty::Dynamic(..)
-                    | ty::Projection(_)
                     | ty::Bound(..)
                     | ty::Placeholder(..)
-                    | ty::Opaque(..)
                     | ty::Param(_)
                     | ty::Infer(_)
                     | ty::Error(_) => unreachable!("type {:?} does not have a field", t),

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -813,7 +813,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     )
                 }
             }
-            ty::Projection(_) | ty::Opaque(_, _) => {
+            ty::Alias(..) => {
                 unreachable!("Type should've been normalized already")
             }
 
@@ -1226,7 +1226,7 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Dynamic(..) | ty::Slice(_) | ty::Str => {
                 unreachable!("Should have generated a fat pointer")
             }
-            ty::Projection(_) | ty::Opaque(..) => {
+            ty::Alias(..) => {
                 unreachable!("Should have been removed by normalization")
             }
 

diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
@@ -17,7 +17,7 @@ use rustc_hir::lang_items::LangItem;
 use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
 use rustc_middle::ty::adjustment::CustomCoerceUnsized;
 use rustc_middle::ty::TypeAndMut;
-use rustc_middle::ty::{self, ParamEnv, TraitRef, Ty, TyCtxt};
+use rustc_middle::ty::{self, ParamEnv, Ty, TyCtxt};
 use rustc_span::symbol::Symbol;
 use tracing::trace;
 
@@ -213,10 +213,9 @@ fn custom_coerce_unsize_info<'tcx>(
 ) -> CustomCoerceUnsized {
     let def_id = tcx.require_lang_item(LangItem::CoerceUnsized, None);
 
-    let trait_ref = ty::Binder::dummy(TraitRef {
-        def_id,
-        substs: tcx.mk_substs_trait(source_ty, [target_ty.into()]),
-    });
+    let trait_ref = ty::Binder::dummy(
+        tcx.mk_trait_ref(def_id, tcx.mk_substs_trait(source_ty, [target_ty.into()])),
+    );
 
     match tcx.codegen_select_candidate((ParamEnv::reveal_all(), trait_ref)) {
         Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { impl_def_id, .. })) => {

diff --git a/kani-compiler/src/kani_middle/stubbing/annotations.rs b/kani-compiler/src/kani_middle/stubbing/annotations.rs
@@ -40,7 +40,7 @@ impl Callbacks for CollectorCallbacks {
         _compiler: &Compiler,
         queries: &'tcx Queries<'tcx>,
     ) -> Compilation {
-        queries.global_ctxt().unwrap().peek_mut().enter(|tcx| {
+        queries.global_ctxt().unwrap().enter(|tcx| {
             for item in tcx.hir_crate_items(()).items() {
                 let local_def_id = item.owner_id.def_id;
                 let def_id = local_def_id.to_def_id();

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-2022-12-11"
+channel = "nightly-2023-01-16"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]