diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index def8c2275e8b..70458ad3fe78 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -404,8 +404,11 @@ impl<'tcx> GotocCtx<'tcx> { }}; } - if let Some(stripped) = intrinsic.strip_prefix("simd_shuffle") { - let _n: u64 = stripped.parse().unwrap(); + if let Some(_stripped) = intrinsic.strip_prefix("simd_shuffle") { + // TODO: can be empty now (i.e. `simd_shuffle` instead of `simd_shuffle8`) + // `parse` fails on empty, so comment that bit of code out. + // To re-enable this we'll need to investigate how size is computed now. + // let n: u64 = stripped.parse().unwrap(); return unstable_codegen!(self.codegen_intrinsic_simd_shuffle( fargs, p, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index b04565df1e67..6e232894a32d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -9,7 +9,7 @@ use rustc_ast::ast::Mutability; use rustc_middle::mir::interpret::{ read_target_uint, AllocId, Allocation, ConstValue, GlobalAlloc, Scalar, }; -use rustc_middle::mir::{Constant, ConstantKind, Operand}; +use rustc_middle::mir::{Constant, ConstantKind, Operand, UnevaluatedConst}; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{self, Const, ConstKind, FloatTy, Instance, IntTy, Ty, Uint, UintTy}; use rustc_span::def_id::DefId; @@ -47,12 +47,26 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_constant(&mut self, c: &Constant<'tcx>) -> Expr { trace!(constant=?c, "codegen_constant"); - let const_ = match self.monomorphize(c.literal) { - ConstantKind::Ty(ct) => ct, - ConstantKind::Val(val, ty) => return self.codegen_const_value(val, ty, Some(&c.span)), - }; + let span = Some(&c.span); + match self.monomorphize(c.literal) { + ConstantKind::Ty(ct) => self.codegen_const(ct, span), + ConstantKind::Val(val, ty) => self.codegen_const_value(val, ty, span), + ConstantKind::Unevaluated(unevaluated, ty) => { + self.codegen_const_unevaluated(unevaluated, ty, span) + } + } + } - self.codegen_const(const_, Some(&c.span)) + fn codegen_const_unevaluated( + &mut self, + unevaluated: UnevaluatedConst<'tcx>, + ty: Ty<'tcx>, + span: Option<&Span>, + ) -> Expr { + debug!(?unevaluated, "codegen_const_unevaluated"); + let const_val = + self.tcx.const_eval_resolve(ty::ParamEnv::reveal_all(), unevaluated, None).unwrap(); + self.codegen_const_value(const_val, ty, span) } pub fn codegen_const(&mut self, lit: Const<'tcx>, span: Option<&Span>) -> Expr { @@ -60,15 +74,10 @@ impl<'tcx> GotocCtx<'tcx> { let lit = self.monomorphize(lit); match lit.kind() { - // evaluate constant if it has no been evaluated yet - ConstKind::Unevaluated(unevaluated) => { - debug!("The literal was a Unevaluated"); - let const_val = self - .tcx - .const_eval_resolve(ty::ParamEnv::reveal_all(), unevaluated, None) - .unwrap(); - self.codegen_const_value(const_val, lit.ty(), span) - } + // A `ConstantKind::Ty(ConstKind::Unevaluated)` should no longer show up + // and should be a `ConstantKind::Unevaluated` instead (and thus handled + // at the level of `codegen_constant` instead of `codegen_const`.) + ConstKind::Unevaluated(_) => unreachable!(), ConstKind::Value(valtree) => { let value = self.tcx.valtree_to_const_val((lit.ty(), valtree)); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index e066ea98200d..18fe364adf18 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -547,6 +547,13 @@ impl<'tcx> GotocCtx<'tcx> { self, ) } + ProjectionElem::OpaqueCast(ty) => ProjectedPlace::try_new( + before.goto_expr.cast_to(self.codegen_ty(ty)), + TypeOrVariant::Type(ty), + before.fat_ptr_goto_expr, + before.fat_ptr_mir_typ, + self, + ), } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index f1dc2ebae8d1..429133e59a0f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -402,7 +402,12 @@ impl<'tcx> GotocCtx<'tcx> { // Rust has begun distinguishing "ptr -> num" and "num -> ptr" (providence-relevant casts) but we do not yet: // Should we? Tracking ticket: https://github.com/model-checking/kani/issues/1274 Rvalue::Cast( - CastKind::Misc + CastKind::IntToInt + | CastKind::FloatToFloat + | CastKind::FloatToInt + | CastKind::IntToFloat + | CastKind::FnPtrToPtr + | CastKind::PtrToPtr | CastKind::PointerExposeAddress | CastKind::PointerFromExposedAddress, e, @@ -411,6 +416,15 @@ impl<'tcx> GotocCtx<'tcx> { let t = self.monomorphize(*t); self.codegen_misc_cast(e, t) } + Rvalue::Cast(CastKind::DynStar, _, _) => { + let ty = self.codegen_ty(res_ty); + self.codegen_unimplemented_expr( + "CastKind::DynStar", + ty, + loc, + "https://github.com/model-checking/kani/issues/1784", + ) + } Rvalue::Cast(CastKind::Pointer(k), e, t) => { let t = self.monomorphize(*t); self.codegen_pointer_cast(k, e, t, loc) @@ -636,7 +650,7 @@ impl<'tcx> GotocCtx<'tcx> { // this is a noop in the case dst_subt is a Projection or Opaque type dst_subt = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), dst_subt); match dst_subt.kind() { - ty::Slice(_) | ty::Str | ty::Dynamic(_, _) => { + ty::Slice(_) | ty::Str | ty::Dynamic(_, _, _) => { //TODO: this does the wrong thing on Strings/fixme_boxed_str.rs // if we cast to slice or string, then we know the source is also a slice or string, // so there shouldn't be anything to do diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 076f937c44d2..faa857b1e00c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -555,7 +555,7 @@ impl<'tcx> GotocCtx<'tcx> { /// We follow the order from the `TyCtxt::COMMON_VTABLE_ENTRIES`. fn trait_vtable_field_types(&mut self, t: ty::Ty<'tcx>) -> Vec { let mut vtable_base = common_vtable_fields(self.trait_vtable_drop_type(t)); - if let ty::Dynamic(binder, _region) = t.kind() { + if let ty::Dynamic(binder, _, _) = t.kind() { // The virtual methods on the trait ref. Some auto traits have no methods. if let Some(principal) = binder.principal() { let poly = principal.with_self_ty(self.tcx, t); @@ -710,7 +710,7 @@ impl<'tcx> GotocCtx<'tcx> { /// codegen for types. it finds a C type which corresponds to a rust type. /// that means [ty] has to be monomorphized before calling this function. /// - /// check [rustc_middle::ty::layout::LayoutCx::layout_of_uncached] for LLVM codegen + /// check `rustc_ty_utils::layout::layout_of_uncached` for LLVM codegen /// /// also c.f. /// c.f. diff --git a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs index d5e175f97c7e..5b8bc5755af0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs @@ -29,8 +29,8 @@ use rustc_middle::ty::adjustment::CustomCoerceUnsized; use rustc_middle::ty::adjustment::PointerCast; use rustc_middle::ty::TypeAndMut; use rustc_middle::ty::{ - self, Closure, ClosureKind, Const, ConstKind, Instance, InstanceDef, ParamEnv, TraitRef, Ty, - TyCtxt, TyKind, TypeFoldable, VtblEntry, + self, Closure, ClosureKind, ConstKind, Instance, InstanceDef, ParamEnv, TraitRef, Ty, TyCtxt, + TyKind, TypeFoldable, VtblEntry, }; use rustc_span::def_id::DefId; use tracing::{debug, debug_span, trace, warn}; @@ -337,22 +337,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { ConstantKind::Val(const_val, _) => const_val, ConstantKind::Ty(ct) => match ct.kind() { ConstKind::Value(v) => self.tcx.valtree_to_const_val((ct.ty(), v)), - ConstKind::Unevaluated(un_eval) => { - // Thread local fall into this category. - match self.tcx.const_eval_resolve(ParamEnv::reveal_all(), un_eval, None) { - // The `monomorphize` call should have evaluated that constant already. - Ok(const_val) => const_val, - Err(ErrorHandled::TooGeneric) => span_bug!( - self.body.source_info(location).span, - "Unexpected polymorphic constant: {:?}", - literal - ), - Err(error) => { - warn!(?error, "Error already reported"); - return; - } - } - } + ConstKind::Unevaluated(_) => unreachable!(), // Nothing to do ConstKind::Param(..) | ConstKind::Infer(..) | ConstKind::Error(..) => return, @@ -361,15 +346,26 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { unreachable!("Unexpected constant type {:?} ({:?})", ct, ct.kind()) } }, + ConstantKind::Unevaluated(un_eval, _) => { + // Thread local fall into this category. + match self.tcx.const_eval_resolve(ParamEnv::reveal_all(), un_eval, None) { + // The `monomorphize` call should have evaluated that constant already. + Ok(const_val) => const_val, + Err(ErrorHandled::TooGeneric) => span_bug!( + self.body.source_info(location).span, + "Unexpected polymorphic constant: {:?}", + literal + ), + Err(error) => { + warn!(?error, "Error already reported"); + return; + } + } + } }; self.collect_const_value(val); } - fn visit_const(&mut self, constant: Const<'tcx>, location: Location) { - trace!(?constant, ?location, "visit_const"); - self.super_const(constant); - } - /// Collect function calls. fn visit_terminator(&mut self, terminator: &Terminator<'tcx>, location: Location) { trace!(?terminator, ?location, "visit_terminator"); diff --git a/kani_metadata/src/lib.rs b/kani_metadata/src/lib.rs index f17927945a16..71fd3d10ac79 100644 --- a/kani_metadata/src/lib.rs +++ b/kani_metadata/src/lib.rs @@ -12,7 +12,7 @@ use serde::{Deserialize, Serialize}; /// The structure of `.kani-metadata.json` files, which are emitted for each crate #[derive(Debug, Clone, Serialize, Deserialize)] pub struct KaniMetadata { - /// The proof harnesses (#[kani::proof]) found in this crate. + /// The proof harnesses (`#[kani::proof]`) found in this crate. pub proof_harnesses: Vec, /// The features found in this crate that Kani does not support. /// (These general translate to `assert(false)` so we can still attempt verification.) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 15c481946b65..a854243a3dfe 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2022-09-13" +channel = "nightly-2022-10-11" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/kani/Intrinsics/Assert/uninit_valid_panic.rs b/tests/kani/Intrinsics/Assert/uninit_valid_panic.rs index b81f4f8b8a0f..efad65a2c14c 100644 --- a/tests/kani/Intrinsics/Assert/uninit_valid_panic.rs +++ b/tests/kani/Intrinsics/Assert/uninit_valid_panic.rs @@ -5,11 +5,11 @@ #![feature(core_intrinsics)] use std::intrinsics; -// The code below attempts to leave type `bool` uninitialized, causing the +// The code below attempts to leave type `&u32` uninitialized, causing the // intrinsic `assert_uninit_valid` to generate a panic during compilation. #[kani::proof] fn main() { let _var: () = unsafe { - intrinsics::assert_uninit_valid::(); + intrinsics::assert_uninit_valid::<&u32>(); }; } diff --git a/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs b/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs index 3f86391824c1..4fadabd92da2 100644 --- a/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs +++ b/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs @@ -2,10 +2,6 @@ // // Modifications Copyright Kani Contributors // See GitHub history for details. -// -// NOTE: The initial fix for this has been reverted from rustc. I'm keeping this test here so we -// will know when it has been reverted back. -// kani-check-fail //! Tests that check handling of opaque casts. Tests were adapted from the rustc repository. diff --git a/tests/ui/code-location/expected b/tests/ui/code-location/expected index 1c6d8ff7dffa..a554e0865965 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:2921:81 in function as std::ops::Drop>::drop +alloc/src/vec/mod.rs:3031:81 in function as std::ops::Drop>::drop VERIFICATION:- SUCCESSFUL diff --git a/tools/bookrunner/librustdoc/lib.rs b/tools/bookrunner/librustdoc/lib.rs index 0ae9af33782d..57ae24335c2a 100644 --- a/tools/bookrunner/librustdoc/lib.rs +++ b/tools/bookrunner/librustdoc/lib.rs @@ -12,7 +12,6 @@ #![feature(box_patterns)] #![feature(control_flow_enum)] #![feature(box_syntax)] -#![feature(let_else)] #![feature(test)] #![feature(never_type)] #![feature(once_cell)] @@ -62,7 +61,6 @@ extern crate rustc_session; extern crate rustc_span; extern crate rustc_target; extern crate rustc_trait_selection; -extern crate rustc_typeck; extern crate test; pub mod doctest; diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index 4d76614f8fe3..0804deea69c5 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -511,5 +511,8 @@ fn make_test_closure( let config = config.clone(); let testpaths = testpaths.clone(); let revision = revision.cloned(); - test::DynTestFn(Box::new(move || runtest::run(config, &testpaths, revision.as_deref()))) + test::DynTestFn(Box::new(move || { + runtest::run(config, &testpaths, revision.as_deref()); + Ok(()) + })) }