Skip to content

Commit

Permalink
Upgrade toolchain to nightly-2023-03-09
Browse files Browse the repository at this point in the history
- Introduce -Zterminal-urls to use OSC8 for error codes rust-lang/rust#107838
- Unify validity checks into a single query rust-lang/rust#108364
- Rename interner funcs rust-lang/rust#108250
- Optimize mk_region rust-lang/rust#108020
- Clarify iterator interners rust-lang/rust#108112
  • Loading branch information
qinheping authored and tautschnig committed Apr 17, 2023
1 parent b4152b2 commit 53e07cc
Show file tree
Hide file tree
Showing 8 changed files with 37 additions and 22 deletions.
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
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/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-18"
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

0 comments on commit 53e07cc

Please sign in to comment.