diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 31fa878c854a..7c3e9dbdf305 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -260,7 +260,6 @@ impl<'tcx> GotocCtx<'tcx> { | ty::Never | ty::FnDef(..) | ty::GeneratorWitness(..) - | ty::GeneratorWitnessMIR(..) | ty::Foreign(..) | ty::Dynamic(..) | ty::Bound(..) @@ -605,13 +604,15 @@ 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, - ), + ProjectionElem::OpaqueCast(ty) | ProjectionElem::Subtype(ty) => { + ProjectedPlace::try_new( + before.goto_expr.cast_to(self.codegen_ty(self.monomorphize(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/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index cdbe84d5111a..800c256108bb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -424,7 +424,7 @@ impl<'tcx> GotocCtx<'tcx> { { // Instance is Some(..) only when current codegen unit is a function. if let Some(current_fn) = &self.current_fn { - current_fn.instance().subst_mir_and_normalize_erasing_regions( + current_fn.instance().instantiate_mir_and_normalize_erasing_regions( self.tcx, ty::ParamEnv::reveal_all(), ty::EarlyBinder::bind(value), @@ -813,11 +813,7 @@ impl<'tcx> GotocCtx<'tcx> { ty::Bound(_, _) | ty::Param(_) => unreachable!("monomorphization bug"), // type checking remnants which shouldn't be reachable - ty::GeneratorWitness(_) - | ty::GeneratorWitnessMIR(_, _) - | ty::Infer(_) - | ty::Placeholder(_) - | ty::Error(_) => { + ty::GeneratorWitness(_, _) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => { unreachable!("remnants of type checking") } } @@ -1254,8 +1250,7 @@ impl<'tcx> GotocCtx<'tcx> { // For soundness, hold off on generating them till we have test-cases. 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::GeneratorWitness(_, _) => 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()), diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 68fb2b88cb52..f0021c14e9d7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -37,8 +37,8 @@ use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME}; use rustc_metadata::EncodedMetadata; use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; use rustc_middle::mir::mono::MonoItem; -use rustc_middle::query::{ExternProviders, Providers}; use rustc_middle::ty::TyCtxt; +use rustc_middle::util::Providers; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::cstore::MetadataLoaderDyn; use rustc_session::output::out_filename; @@ -193,10 +193,6 @@ impl CodegenBackend for GotocCodegenBackend { provide::provide(providers, &self.queries.lock().unwrap()); } - fn provide_extern(&self, providers: &mut ExternProviders) { - provide::provide_extern(providers, &self.queries.lock().unwrap()); - } - fn print_version(&self) { println!("Kani-goto version: {}", env!("CARGO_PKG_VERSION")); } diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 0287e4b9b01f..e648d9ffc006 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -201,7 +201,7 @@ impl<'tcx> GotocHook<'tcx> for Panic { fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { let def_id = instance.def.def_id(); Some(def_id) == tcx.lang_items().panic_fn() - || Some(def_id) == tcx.lang_items().panic_display() + || tcx.has_attr(def_id, rustc_span::sym::rustc_const_panic_str) || Some(def_id) == tcx.lang_items().panic_fmt() || Some(def_id) == tcx.lang_items().begin_panic_fn() || matches_function(tcx, instance, "KaniPanic") diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index d668d439b96a..033eae3b460f 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -11,19 +11,17 @@ use crate::kani_middle::stubbing; use crate::kani_queries::QueryDb; use rustc_hir::def_id::{DefId, LocalDefId}; use rustc_interface; -use rustc_middle::{ - mir::Body, - query::{queries, ExternProviders, Providers}, - ty::TyCtxt, -}; +use rustc_middle::util::Providers; +use rustc_middle::{mir::Body, query::queries, ty::TyCtxt}; /// Sets up rustc's query mechanism to apply Kani's custom queries to code from -/// the present crate. +/// a crate. pub fn provide(providers: &mut Providers, queries: &QueryDb) { let args = queries.args(); if should_override(args) { // Don't override queries if we are only compiling our dependencies. providers.optimized_mir = run_mir_passes; + providers.extern_queries.optimized_mir = run_mir_passes_extern; if args.stubbing_enabled { // TODO: Check if there's at least one stub being applied. providers.collect_and_partition_mono_items = collect_and_partition_mono_items; @@ -31,15 +29,6 @@ pub fn provide(providers: &mut Providers, queries: &QueryDb) { } } -/// Sets up rustc's query mechanism to apply Kani's custom queries to code from -/// external crates. -pub fn provide_extern(providers: &mut ExternProviders, queries: &QueryDb) { - if should_override(queries.args()) { - // Don't override queries if we are only compiling our dependencies. - providers.optimized_mir = run_mir_passes_extern; - } -} - fn should_override(args: &Arguments) -> bool { args.reachability_analysis != ReachabilityType::None && !args.build_std } @@ -48,7 +37,7 @@ fn should_override(args: &Arguments) -> bool { /// running rustc's optimization passes followed by Kani-specific passes. fn run_mir_passes_extern(tcx: TyCtxt, def_id: DefId) -> &Body { tracing::debug!(?def_id, "run_mir_passes_extern"); - let body = (rustc_interface::DEFAULT_EXTERN_QUERY_PROVIDERS.optimized_mir)(tcx, def_id); + let body = (rustc_interface::DEFAULT_QUERY_PROVIDERS.extern_queries.optimized_mir)(tcx, def_id); run_kani_mir_passes(tcx, def_id, body) } diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index c27b5e9ae0d9..55f425c6da69 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -242,7 +242,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { T: TypeFoldable>, { trace!(instance=?self.instance, ?value, "monomorphize"); - self.instance.subst_mir_and_normalize_erasing_regions( + self.instance.instantiate_mir_and_normalize_erasing_regions( self.tcx, ParamEnv::reveal_all(), EarlyBinder::bind(value), @@ -519,7 +519,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { // even the return type, for instance for a // trait like `FromIterator`. let generic_ty = outer_args[0].ty(self.body, tcx).peel_refs(); - let receiver_ty = tcx.subst_and_normalize_erasing_regions( + let receiver_ty = tcx.instantiate_and_normalize_erasing_regions( substs, ParamEnv::reveal_all(), EarlyBinder::bind(generic_ty), diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 53fedae29b02..431c80e5e0e2 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-09-23" +channel = "nightly-2023-10-05" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/src/setup.rs b/src/setup.rs index 1e9287542c93..6c24bf00cce0 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -59,7 +59,7 @@ pub fn appears_incomplete() -> Option { let kani_dir = kani_dir().expect("couldn't find kani directory"); let kani_dir_parent = kani_dir.parent().unwrap(); - for entry in std::fs::read_dir(&kani_dir_parent).ok()?.flatten() { + for entry in std::fs::read_dir(kani_dir_parent).ok()?.flatten() { if let Some(file_name) = entry.file_name().to_str() { if file_name.ends_with(".tar.gz") { return Some(kani_dir_parent.join(file_name));