Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Upgrade toolchain to nightly-2023-03-09 #2293

Closed
wants to merge 2 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 12 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use cbmc::goto_program::{
Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
};
use rustc_middle::mir::{BasicBlock, Operand, Place};
use rustc_middle::ty::layout::LayoutOf;
use rustc_middle::ty::layout::{LayoutOf, ValidityRequirement};
use rustc_middle::ty::{self, Ty};
use rustc_middle::ty::{Instance, InstanceDef};
use rustc_span::Span;
Expand Down Expand Up @@ -788,7 +788,10 @@ impl<'tcx> GotocCtx<'tcx> {
// 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(param_env_and_type).ok().unwrap()
&& !self
.tcx
.check_validity_requirement((ValidityRequirement::Zero, param_env_and_type))
.unwrap()
{
return self.codegen_fatal_error(
PropertyClass::SafetyCheck,
Expand All @@ -798,7 +801,13 @@ impl<'tcx> GotocCtx<'tcx> {
}

if intrinsic == "assert_uninit_valid"
&& !self.tcx.permits_uninit_init(param_env_and_type).ok().unwrap()
&& !self
.tcx
.check_validity_requirement((
ValidityRequirement::UninitMitigated0x01Fill,
param_env_and_type,
))
.unwrap()
{
return self.codegen_fatal_error(
PropertyClass::SafetyCheck,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ impl<'tcx> GotocCtx<'tcx> {
let pretty_name = Instance::new(def_id, InternalSubsts::empty()).to_string();
debug!(?symbol_name, ?pretty_name, "declare_static {}", item);

let typ = self.codegen_ty(self.tcx.type_of(def_id));
let typ = self.codegen_ty(self.tcx.type_of(def_id).subst_identity());
let span = self.tcx.def_span(def_id);
let location = self.codegen_span(&span);
let symbol = Symbol::static_variable(symbol_name.clone(), symbol_name, typ, location)
Expand Down
22 changes: 11 additions & 11 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -272,7 +272,7 @@ impl<'tcx> GotocCtx<'tcx> {
let env = prev_args[0];

// Recombine arguments: environment first, then the flattened tuple elements
let recombined_args = iter::once(env).chain(args);
let recombined_args: Vec<_> = iter::once(env).chain(args).collect();

return ty::Binder::bind_with_vars(
self.tcx.mk_fn_sig(
Expand All @@ -297,7 +297,7 @@ impl<'tcx> GotocCtx<'tcx> {

// In addition to `def_id` and `substs`, we need to provide the kind of region `env_region`
// in `closure_env_ty`, which we can build from the bound variables as follows
let bound_vars = self.tcx.mk_bound_variable_kinds(
let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(
sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))),
);
let br = ty::BoundRegion {
Expand All @@ -314,7 +314,7 @@ impl<'tcx> GotocCtx<'tcx> {
// * the rest of attributes are obtained from `sig`
let sig = ty::Binder::bind_with_vars(
self.tcx.mk_fn_sig(
iter::once(env_ty).chain(iter::once(sig.inputs()[0])),
[env_ty, sig.inputs()[0]],
sig.output(),
sig.c_variadic,
sig.unsafety,
Expand All @@ -338,19 +338,19 @@ impl<'tcx> GotocCtx<'tcx> {
) -> ty::PolyFnSig<'tcx> {
let sig = substs.as_generator().poly_sig();

let bound_vars = self.tcx.mk_bound_variable_kinds(
let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(
sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))),
);
let br = ty::BoundRegion {
var: ty::BoundVar::from_usize(bound_vars.len() - 1),
kind: ty::BoundRegionKind::BrEnv,
};
let env_region = ty::ReLateBound(ty::INNERMOST, br);
let env_ty = self.tcx.mk_mut_ref(self.tcx.mk_region(env_region), ty);
let env_ty = self.tcx.mk_mut_ref(self.tcx.mk_region_from_kind(env_region), ty);

let pin_did = self.tcx.require_lang_item(LangItem::Pin, None);
let pin_adt_ref = self.tcx.adt_def(pin_did);
let pin_substs = self.tcx.intern_substs(&[env_ty.into()]);
let pin_substs = self.tcx.mk_substs(&[env_ty.into()]);
let env_ty = self.tcx.mk_adt(pin_adt_ref, pin_substs);

let sig = sig.skip_binder();
Expand All @@ -363,7 +363,7 @@ impl<'tcx> GotocCtx<'tcx> {
// The signature should be `Future::poll(_, &mut Context<'_>) -> Poll<Output>`
let poll_did = tcx.require_lang_item(LangItem::Poll, None);
let poll_adt_ref = tcx.adt_def(poll_did);
let poll_substs = tcx.intern_substs(&[sig.return_ty.into()]);
let poll_substs = tcx.mk_substs(&[sig.return_ty.into()]);
let ret_ty = tcx.mk_adt(poll_adt_ref, poll_substs);

// We have to replace the `ResumeTy` that is used for type and borrow checking
Expand All @@ -384,16 +384,16 @@ impl<'tcx> GotocCtx<'tcx> {
// The signature should be `Generator::resume(_, Resume) -> GeneratorState<Yield, Return>`
let state_did = tcx.require_lang_item(LangItem::GeneratorState, None);
let state_adt_ref = tcx.adt_def(state_did);
let state_substs = tcx.intern_substs(&[sig.yield_ty.into(), sig.return_ty.into()]);
let state_substs = tcx.mk_substs(&[sig.yield_ty.into(), sig.return_ty.into()]);
let ret_ty = tcx.mk_adt(state_adt_ref, state_substs);

(sig.resume_ty, ret_ty)
};

ty::Binder::bind_with_vars(
tcx.mk_fn_sig(
[env_ty, resume_ty].iter(),
&ret_ty,
[env_ty, resume_ty],
ret_ty,
false,
Unsafety::Normal,
rustc_target::spec::abi::Abi::Rust,
Expand Down Expand Up @@ -423,7 +423,7 @@ impl<'tcx> GotocCtx<'tcx> {
impl<'tcx> GotocCtx<'tcx> {
pub fn monomorphize<T>(&self, value: T) -> T
where
T: TypeFoldable<'tcx>,
T: TypeFoldable<TyCtxt<'tcx>>,
{
// Instance is Some(..) only when current codegen unit is a function.
if let Some(current_fn) = &self.current_fn {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ use rustc_codegen_ssa::traits::CodegenBackend;
use rustc_codegen_ssa::{CodegenResults, CrateInfo};
use rustc_data_structures::fx::FxHashMap;
use rustc_data_structures::temp_dir::MaybeTempDir;
use rustc_errors::ErrorGuaranteed;
use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE};
use rustc_hir::def_id::LOCAL_CRATE;
use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
use rustc_metadata::EncodedMetadata;
Expand Down Expand Up @@ -70,6 +70,10 @@ impl GotocCodegenBackend {
}

impl CodegenBackend for GotocCodegenBackend {
fn locale_resource(&self) -> &'static str {
DEFAULT_LOCALE_RESOURCE
}

fn metadata_loader(&self) -> Box<MetadataLoaderDyn> {
Box::new(rustc_codegen_ssa::back::metadata::DefaultMetadataLoader)
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -422,6 +422,7 @@ impl<'tcx> FnAbiOfHelpers<'tcx> for GotocCtx<'tcx> {
}
}

#[derive(Debug)]
pub struct GotocMetadataLoader();
impl MetadataLoader for GotocMetadataLoader {
fn get_rlib_metadata(&self, _: &Target, _filename: &Path) -> Result<MetadataRef, String> {
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/provide.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,10 @@

use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items};
use crate::kani_middle::stubbing;
use crate::kani_middle::ty::query::query_provided::collect_and_partition_mono_items;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This change looks a bit odd. Isn't this importing collect_and_partition_mono_items from rustc_middle? If so, why is it referring to crate::kani_middle?

use kani_queries::{QueryDb, UserInput};
use rustc_hir::def_id::DefId;
use rustc_interface;
use rustc_middle::ty::query::query_stored::collect_and_partition_mono_items;
use rustc_middle::{
mir::Body,
ty::{query::ExternProviders, query::Providers, TyCtxt},
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/reachability.rs
Original file line number Diff line number Diff line change
Expand Up @@ -215,7 +215,7 @@ struct MonoItemsFnCollector<'a, 'tcx> {
impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
fn monomorphize<T>(&self, value: T) -> T
where
T: TypeFoldable<'tcx>,
T: TypeFoldable<TyCtxt<'tcx>>,
{
trace!(instance=?self.instance, ?value, "monomorphize");
self.instance.subst_mir_and_normalize_erasing_regions(
Expand Down
5 changes: 2 additions & 3 deletions kani-compiler/src/session.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use crate::parser;
use clap::ArgMatches;
use rustc_errors::{
emitter::Emitter, emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter,
ColorConfig, Diagnostic, TerminalUrl,
ColorConfig, Diagnostic, TerminalUrl, DEFAULT_LOCALE_RESOURCE,
};
use std::panic;
use std::str::FromStr;
Expand Down Expand Up @@ -47,8 +47,7 @@ static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send
panic::set_hook(Box::new(|info| {
// Print stack trace.
let msg = format!("Kani unexpectedly panicked at {info}.",);
let fallback_bundle =
fallback_fluent_bundle(rustc_errors::DEFAULT_LOCALE_RESOURCES, false);
let fallback_bundle = fallback_fluent_bundle(vec![DEFAULT_LOCALE_RESOURCE], false);
let mut emitter = JsonEmitter::basic(
false,
HumanReadableErrorType::Default(ColorConfig::Never),
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-02-17"
channel = "nightly-2023-03-09"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
6 changes: 4 additions & 2 deletions tools/bookrunner/librustdoc/doctest.rs
Original file line number Diff line number Diff line change
Expand Up @@ -78,8 +78,10 @@ pub fn make_test(
// send all the errors that librustc_ast emits directly into a `Sink` instead of stderr.
let sm = Lrc::new(SourceMap::new(FilePathMapping::empty()));

let fallback_bundle =
rustc_errors::fallback_fluent_bundle(rustc_errors::DEFAULT_LOCALE_RESOURCES, false);
let fallback_bundle = rustc_errors::fallback_fluent_bundle(
vec![rustc_errors::DEFAULT_LOCALE_RESOURCE],
false,
);
supports_color = EmitterWriter::stderr(
ColorConfig::Auto,
None,
Expand Down