Skip to content

Commit

Permalink
Update Rust toolchain to 2023-10-05 (model-checking#2802)
Browse files Browse the repository at this point in the history
Source changes required by the following upstream commits:

* rust-lang/rust@44ac8dcc71 Remove GeneratorWitness and rename
GeneratorWitnessMIR.
* rust-lang/rust@4ed4913e67 Merge ExternProviders into the general
Providers struct
* rust-lang/rust@3c52a3e280 subst -> instantiate
* rust-lang/rust@6a02baaa3d Partially outline code inside the panic!
macro
* rust-lang/rust@3148e6a993 subtyping_projections

Resolves: model-checking#2811
  • Loading branch information
tautschnig authored Oct 6, 2023
1 parent 534b050 commit 88204c2
Show file tree
Hide file tree
Showing 8 changed files with 23 additions and 42 deletions.
17 changes: 9 additions & 8 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
Original file line number Diff line number Diff line change
Expand Up @@ -260,7 +260,6 @@ impl<'tcx> GotocCtx<'tcx> {
| ty::Never
| ty::FnDef(..)
| ty::GeneratorWitness(..)
| ty::GeneratorWitnessMIR(..)
| ty::Foreign(..)
| ty::Dynamic(..)
| ty::Bound(..)
Expand Down Expand Up @@ -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,
)
}
}
}

Expand Down
11 changes: 3 additions & 8 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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),
Expand Down Expand Up @@ -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")
}
}
Expand Down Expand Up @@ -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()),
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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"));
}
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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")
Expand Down
21 changes: 5 additions & 16 deletions kani-compiler/src/kani_middle/provide.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,35 +11,24 @@ 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;
}
}
}

/// 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
}
Expand All @@ -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)
}

Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/reachability.rs
Original file line number Diff line number Diff line change
Expand Up @@ -242,7 +242,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
T: TypeFoldable<TyCtxt<'tcx>>,
{
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),
Expand Down Expand Up @@ -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),
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-09-23"
channel = "nightly-2023-10-05"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
2 changes: 1 addition & 1 deletion src/setup.rs
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ pub fn appears_incomplete() -> Option<PathBuf> {
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));
Expand Down

0 comments on commit 88204c2

Please sign in to comment.