Upgrade Rust toolchain to nightly-2023-02-03 (model-checking#2291)

qinheping · Mar 10, 2023 · 688aa59 · 688aa59
1 parent 4b925fd
commit 688aa59
Show file tree

Hide file tree

Showing 6 changed files with 25 additions and 15 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -783,17 +783,20 @@ impl<'tcx> GotocCtx<'tcx> {
             );
         }
 
+        let param_env_and_layout = ty::ParamEnv::reveal_all().and(layout);
+
         // Then we check if the type allows "raw" initialization for the cases
         // where memory is zero-initialized or entirely uninitialized
-        if intrinsic == "assert_zero_valid" && !self.tcx.permits_zero_init(layout) {
+        if intrinsic == "assert_zero_valid" && !self.tcx.permits_zero_init(param_env_and_layout) {
             return self.codegen_fatal_error(
                 PropertyClass::SafetyCheck,
                 &format!("attempted to zero-initialize type `{ty}`, which is invalid"),
                 span,
             );
         }
 
-        if intrinsic == "assert_uninit_valid" && !self.tcx.permits_uninit_init(layout) {
+        if intrinsic == "assert_uninit_valid" && !self.tcx.permits_uninit_init(param_env_and_layout)
+        {
             return self.codegen_fatal_error(
                 PropertyClass::SafetyCheck,
                 &format!("attempted to leave type `{ty}` uninitialized, which is invalid"),

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -97,12 +97,13 @@ impl<'tcx> GotocCtx<'tcx> {
                                 let niche_value =
                                     variant_index.as_u32() - niche_variants.start().as_u32();
                                 let niche_value = (niche_value as u128).wrapping_add(*niche_start);
-                                let value =
-                                    if niche_value == 0 && tag.primitive() == Primitive::Pointer {
-                                        discr_ty.null()
-                                    } else {
-                                        Expr::int_constant(niche_value, discr_ty.clone())
-                                    };
+                                let value = if niche_value == 0
+                                    && matches!(tag.primitive(), Primitive::Pointer(_))
+                                {
+                                    discr_ty.null()
+                                } else {
+                                    Expr::int_constant(niche_value, discr_ty.clone())
+                                };
                                 let place = unwrap_or_return_codegen_unimplemented_stmt!(
                                     self,
                                     self.codegen_place(place)
@@ -145,7 +146,8 @@ impl<'tcx> GotocCtx<'tcx> {
             | StatementKind::Retag(_, _)
             | StatementKind::AscribeUserType(_, _)
             | StatementKind::Nop
-            | StatementKind::Coverage { .. } => Stmt::skip(location),
+            | StatementKind::Coverage { .. }
+            | StatementKind::ConstEvalCounter => Stmt::skip(location),
         }
         .with_location(location)
     }

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -842,7 +842,11 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Bound(_, _) | ty::Param(_) => unreachable!("monomorphization bug"),
 
             // type checking remnants which shouldn't be reachable
-            ty::GeneratorWitness(_) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => {
+            ty::GeneratorWitness(_)
+            | ty::GeneratorWitnessMIR(_, _)
+            | ty::Infer(_)
+            | ty::Placeholder(_)
+            | ty::Error(_) => {
                 unreachable!("remnants of type checking")
             }
         }
@@ -1280,6 +1284,7 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Bound(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
             ty::Error(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
             ty::GeneratorWitness(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
+            ty::GeneratorWitnessMIR(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
             ty::Infer(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
             ty::Param(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
             ty::Placeholder(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
@@ -1630,7 +1635,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
             Primitive::F32 => self.tcx.types.f32,
             Primitive::F64 => self.tcx.types.f64,
-            Primitive::Pointer => {
+            Primitive::Pointer(_) => {
                 self.tcx.mk_ptr(ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not })
             }
         }

diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
@@ -185,7 +185,7 @@ fn resolve_prefix<'tcx>(
             let current_module_hir_id = tcx.hir().local_def_id_to_hir_id(current_module);
             let crate_root = match tcx.hir().parent_iter(current_module_hir_id).last() {
                 None => current_module,
-                Some((hir_id, _)) => tcx.hir().local_def_id(hir_id),
+                Some((hir_id, _)) => hir_id.owner.def_id,
             };
             Ok(Path { base: crate_root.to_def_id(), segments: segments.collect() })
         }
@@ -227,7 +227,7 @@ where
     while segments.next_if(|segment| segment == SUPER).is_some() {
         if let Some((parent, _)) = parents.next() {
             debug!("parent: {parent:?}");
-            base_module = tcx.hir().local_def_id(parent);
+            base_module = parent.owner.def_id;
         } else {
             return Err(ResolveError::ExtraSuper);
         }

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-2023-01-23"
+channel = "nightly-2023-02-03"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/ui/code-location/expected b/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:3059:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
+alloc/src/vec/mod.rs:3030:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
 
 VERIFICATION:- SUCCESSFUL