Skip to content

Commit

Permalink
Upgrade toolchain to nightly-2023-03-09
Browse files Browse the repository at this point in the history
- Remove some superfluous type parameters from layout.rs rust-lang/rust#107163
- Introduce -Zterminal-urls to use OSC8 for error codes rust-lang/rust#107838
- Unify validity checks into a single query rust-lang/rust#108364
- s/eval_usize/eval_target_usize/ for clarity rust-lang/rust#108029
- Use target instead of machine for mir interpreter integer handling rust-lang/rust#108047
- Switch to EarlyBinder for type_of query rust-lang/rust#107753
- 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 Mar 17, 2023
1 parent 048b598 commit 0cfe538
Show file tree
Hide file tree
Showing 12 changed files with 55 additions and 38 deletions.
22 changes: 17 additions & 5 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 @@ -783,19 +783,31 @@ impl<'tcx> GotocCtx<'tcx> {
);
}

let param_env_and_layout = ty::ParamEnv::reveal_all().and(layout);
let param_env_and_layout = ty::ParamEnv::reveal_all().and(ty);

// 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_layout) {
if intrinsic == "assert_zero_valid"
&& !self
.tcx
.check_validity_requirement((ValidityRequirement::Zero, param_env_and_layout))
.unwrap()
{
return self.codegen_fatal_error(
PropertyClass::SafetyCheck,
&format!("attempted to zero-initialize type `{ty}`, which is invalid"),
span,
);
}

if intrinsic == "assert_uninit_valid" && !self.tcx.permits_uninit_init(param_env_and_layout)
if intrinsic == "assert_uninit_valid"
&& !self
.tcx
.check_validity_requirement((
ValidityRequirement::UninitMitigated0x01Fill,
param_env_and_layout,
))
.unwrap()
{
return self.codegen_fatal_error(
PropertyClass::SafetyCheck,
Expand Down Expand Up @@ -1226,7 +1238,7 @@ impl<'tcx> GotocCtx<'tcx> {
// `simd_shuffle4`) is type-checked
match farg_types[2].kind() {
ty::Array(ty, len) if matches!(ty.kind(), ty::Uint(ty::UintTy::U32)) => {
len.try_eval_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap_or_else(|| {
len.try_eval_target_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap_or_else(|| {
self.tcx.sess.span_err(
span.unwrap(),
"could not evaluate shuffle index array length",
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Original file line number Diff line number Diff line change
Expand Up @@ -253,7 +253,7 @@ impl<'tcx> GotocCtx<'tcx> {
IntTy::I64 => Expr::int_constant(s.to_i64().unwrap(), Type::signed_int(64)),
IntTy::I128 => Expr::int_constant(s.to_i128().unwrap(), Type::signed_int(128)),
IntTy::Isize => {
Expr::int_constant(s.to_machine_isize(self).unwrap(), Type::ssize_t())
Expr::int_constant(s.to_target_isize(self).unwrap(), Type::ssize_t())
}
},
(Scalar::Int(_), ty::Uint(it)) => match it {
Expand All @@ -263,7 +263,7 @@ impl<'tcx> GotocCtx<'tcx> {
UintTy::U64 => Expr::int_constant(s.to_u64().unwrap(), Type::unsigned_int(64)),
UintTy::U128 => Expr::int_constant(s.to_u128().unwrap(), Type::unsigned_int(128)),
UintTy::Usize => {
Expr::int_constant(s.to_machine_usize(self).unwrap(), Type::size_t())
Expr::int_constant(s.to_target_usize(self).unwrap(), Type::size_t())
}
},
(Scalar::Int(_), ty::Bool) => Expr::c_bool_constant(s.to_bool().unwrap()),
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
Original file line number Diff line number Diff line change
Expand Up @@ -462,7 +462,7 @@ impl<'tcx> GotocCtx<'tcx> {
// https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html
match before.mir_typ().kind() {
ty::Array(ty, len) => {
let len = len.kind().try_to_machine_usize(self.tcx).unwrap();
let len = len.kind().try_to_target_usize(self.tcx).unwrap();
let subarray_len = if from_end {
// `to` counts from the end of the array
len - to - from
Expand Down Expand Up @@ -642,7 +642,7 @@ impl<'tcx> GotocCtx<'tcx> {
match before.mir_typ().kind() {
//TODO, ask on zulip if we can ever have from_end here?
ty::Array(elemt, length) => {
let length = length.kind().try_to_machine_usize(self.tcx).unwrap();
let length = length.kind().try_to_target_usize(self.tcx).unwrap();
assert!(length >= min_length);
let idx = if from_end { length - offset } else { offset };
let idxe = Expr::int_constant(idx, Type::ssize_t());
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -143,7 +143,7 @@ impl<'tcx> GotocCtx<'tcx> {
) -> Expr {
let res_t = self.codegen_ty(res_ty);
let op_expr = self.codegen_operand(op);
let width = sz.try_eval_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap();
let width = sz.try_eval_target_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap();
Expr::struct_expr(
res_t,
btree_string_map![("0", op_expr.array_constant(width))],
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
40 changes: 20 additions & 20 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,14 +297,14 @@ 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 {
var: ty::BoundVar::from_usize(bound_vars.len() - 1),
kind: ty::BoundRegionKind::BrEnv,
};
let env_region = ty::ReLateBound(ty::INNERMOST, br);
let env_region = self.tcx.mk_re_late_bound(ty::INNERMOST, br);
let env_ty = self.tcx.closure_env_ty(def_id, substs, env_region).unwrap();

let sig = sig.skip_binder();
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 Expand Up @@ -778,7 +778,7 @@ impl<'tcx> GotocCtx<'tcx> {
}
ty::Foreign(defid) => self.codegen_foreign(ty, *defid),
ty::Array(et, len) => {
let evaluated_len = len.try_eval_usize(self.tcx, self.param_env()).unwrap();
let evaluated_len = len.try_eval_target_usize(self.tcx, self.param_env()).unwrap();
let array_name = format!("[{}; {evaluated_len}]", self.ty_mangled_name(*et));
let array_pretty_name = format!("[{}; {evaluated_len}]", self.ty_pretty_name(*et));
// wrap arrays into struct so that one can take advantage of struct copy in C
Expand Down Expand Up @@ -903,7 +903,7 @@ impl<'tcx> GotocCtx<'tcx> {
fn codegen_alignment_padding(
&self,
size: Size,
layout: &LayoutS<VariantIdx>,
layout: &LayoutS,
idx: usize,
) -> Option<DatatypeComponent> {
let align = Size::from_bits(layout.align.abi.bits());
Expand All @@ -928,7 +928,7 @@ impl<'tcx> GotocCtx<'tcx> {
fn codegen_struct_fields(
&mut self,
flds: Vec<(String, Ty<'tcx>)>,
layout: &LayoutS<VariantIdx>,
layout: &LayoutS,
initial_offset: Size,
) -> Vec<DatatypeComponent> {
match &layout.fields {
Expand Down Expand Up @@ -1386,7 +1386,7 @@ impl<'tcx> GotocCtx<'tcx> {
&mut self,
variant: &VariantDef,
subst: &'tcx InternalSubsts<'tcx>,
layout: &LayoutS<VariantIdx>,
layout: &LayoutS,
initial_offset: Size,
) -> Vec<DatatypeComponent> {
let flds: Vec<_> =
Expand Down Expand Up @@ -1555,7 +1555,7 @@ impl<'tcx> GotocCtx<'tcx> {
ty: Ty<'tcx>,
adtdef: &'tcx AdtDef,
subst: &'tcx InternalSubsts<'tcx>,
variants: &IndexVec<VariantIdx, LayoutS<VariantIdx>>,
variants: &IndexVec<VariantIdx, LayoutS>,
) -> Type {
let non_zst_count = variants.iter().filter(|layout| layout.size.bytes() > 0).count();
let mangled_name = self.ty_mangled_name(ty);
Expand All @@ -1574,7 +1574,7 @@ impl<'tcx> GotocCtx<'tcx> {

pub(crate) fn variant_min_offset(
&self,
variants: &IndexVec<VariantIdx, LayoutS<VariantIdx>>,
variants: &IndexVec<VariantIdx, LayoutS>,
) -> Option<Size> {
variants
.iter()
Expand Down Expand Up @@ -1658,7 +1658,7 @@ impl<'tcx> GotocCtx<'tcx> {
pretty_name: InternedString,
def: &'tcx AdtDef,
subst: &'tcx InternalSubsts<'tcx>,
layouts: &IndexVec<VariantIdx, LayoutS<VariantIdx>>,
layouts: &IndexVec<VariantIdx, LayoutS>,
initial_offset: Size,
) -> Vec<DatatypeComponent> {
def.variants()
Expand Down Expand Up @@ -1690,7 +1690,7 @@ impl<'tcx> GotocCtx<'tcx> {
pretty_name: InternedString,
case: &VariantDef,
subst: &'tcx InternalSubsts<'tcx>,
variant: &LayoutS<VariantIdx>,
variant: &LayoutS,
initial_offset: Size,
) -> Type {
let case_name = format!("{name}::{}", case.name);
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;
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
6 changes: 3 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,
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 All @@ -57,6 +56,7 @@ static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send
None,
false,
false,
TerminalUrl::No,
);
let diagnostic = Diagnostic::new(rustc_errors::Level::Bug, msg);
emitter.emit_diagnostic(&diagnostic);
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-03"
channel = "nightly-2023-03-09"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

0 comments on commit 0cfe538

Please sign in to comment.