diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 98ed0421e05d..fc88333f8325 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -783,9 +783,11 @@ 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"), @@ -793,7 +795,8 @@ impl<'tcx> GotocCtx<'tcx> { ); } - 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 index 75ee1a0e65f7..dbae4073451b 100644 --- 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 index fca6ffe5db61..278f246161eb 100644 --- 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 index cb36ec1ef32d..5c04089cd200 100644 --- 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 index 185bd4ff4136..a173312be9b8 100644 --- 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 index 1d188e17314a..79e1ac6cb30e 100644 --- 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 as std::ops::Drop>::drop +alloc/src/vec/mod.rs:3030:81 in function as std::ops::Drop>::drop VERIFICATION:- SUCCESSFUL