Skip to content

Commit

Permalink
Upgrade Rust toolchain to nightly-2023-02-03 (model-checking#2291)
Browse files Browse the repository at this point in the history
  • Loading branch information
qinheping authored Mar 10, 2023
1 parent 4b925fd commit 688aa59
Show file tree
Hide file tree
Showing 6 changed files with 25 additions and 15 deletions.
7 changes: 5 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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"),
Expand Down
16 changes: 9 additions & 7 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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)
}
Expand Down
9 changes: 7 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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")
}
}
Expand Down Expand Up @@ -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()),
Expand Down Expand Up @@ -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 })
}
}
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/resolve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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() })
}
Expand Down Expand Up @@ -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);
}
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
2 changes: 1 addition & 1 deletion tests/ui/code-location/expected
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 688aa59

Please sign in to comment.