Skip to content

Commit c54b716

Browse files
qinhepingtautschnig
authored andcommitted
Upgrade toolchain to nightly-2023-03-09
- 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
1 parent 048b598 commit c54b716

File tree

13 files changed

+58
-39
lines changed

13 files changed

+58
-39
lines changed

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

+17-5
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ use cbmc::goto_program::{
99
Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
1010
};
1111
use rustc_middle::mir::{BasicBlock, Operand, Place};
12-
use rustc_middle::ty::layout::LayoutOf;
12+
use rustc_middle::ty::layout::{LayoutOf, ValidityRequirement};
1313
use rustc_middle::ty::{self, Ty};
1414
use rustc_middle::ty::{Instance, InstanceDef};
1515
use rustc_span::Span;
@@ -783,19 +783,31 @@ impl<'tcx> GotocCtx<'tcx> {
783783
);
784784
}
785785

786-
let param_env_and_layout = ty::ParamEnv::reveal_all().and(layout);
786+
let param_env_and_layout = ty::ParamEnv::reveal_all().and(ty);
787787

788788
// Then we check if the type allows "raw" initialization for the cases
789789
// where memory is zero-initialized or entirely uninitialized
790-
if intrinsic == "assert_zero_valid" && !self.tcx.permits_zero_init(param_env_and_layout) {
790+
if intrinsic == "assert_zero_valid"
791+
&& !self
792+
.tcx
793+
.check_validity_requirement((ValidityRequirement::Zero, param_env_and_layout))
794+
.unwrap()
795+
{
791796
return self.codegen_fatal_error(
792797
PropertyClass::SafetyCheck,
793798
&format!("attempted to zero-initialize type `{ty}`, which is invalid"),
794799
span,
795800
);
796801
}
797802

798-
if intrinsic == "assert_uninit_valid" && !self.tcx.permits_uninit_init(param_env_and_layout)
803+
if intrinsic == "assert_uninit_valid"
804+
&& !self
805+
.tcx
806+
.check_validity_requirement((
807+
ValidityRequirement::UninitMitigated0x01Fill,
808+
param_env_and_layout,
809+
))
810+
.unwrap()
799811
{
800812
return self.codegen_fatal_error(
801813
PropertyClass::SafetyCheck,
@@ -1226,7 +1238,7 @@ impl<'tcx> GotocCtx<'tcx> {
12261238
// `simd_shuffle4`) is type-checked
12271239
match farg_types[2].kind() {
12281240
ty::Array(ty, len) if matches!(ty.kind(), ty::Uint(ty::UintTy::U32)) => {
1229-
len.try_eval_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap_or_else(|| {
1241+
len.try_eval_target_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap_or_else(|| {
12301242
self.tcx.sess.span_err(
12311243
span.unwrap(),
12321244
"could not evaluate shuffle index array length",

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -253,7 +253,7 @@ impl<'tcx> GotocCtx<'tcx> {
253253
IntTy::I64 => Expr::int_constant(s.to_i64().unwrap(), Type::signed_int(64)),
254254
IntTy::I128 => Expr::int_constant(s.to_i128().unwrap(), Type::signed_int(128)),
255255
IntTy::Isize => {
256-
Expr::int_constant(s.to_machine_isize(self).unwrap(), Type::ssize_t())
256+
Expr::int_constant(s.to_target_isize(self).unwrap(), Type::ssize_t())
257257
}
258258
},
259259
(Scalar::Int(_), ty::Uint(it)) => match it {
@@ -263,7 +263,7 @@ impl<'tcx> GotocCtx<'tcx> {
263263
UintTy::U64 => Expr::int_constant(s.to_u64().unwrap(), Type::unsigned_int(64)),
264264
UintTy::U128 => Expr::int_constant(s.to_u128().unwrap(), Type::unsigned_int(128)),
265265
UintTy::Usize => {
266-
Expr::int_constant(s.to_machine_usize(self).unwrap(), Type::size_t())
266+
Expr::int_constant(s.to_target_usize(self).unwrap(), Type::size_t())
267267
}
268268
},
269269
(Scalar::Int(_), ty::Bool) => Expr::c_bool_constant(s.to_bool().unwrap()),

kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -462,7 +462,7 @@ impl<'tcx> GotocCtx<'tcx> {
462462
// https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html
463463
match before.mir_typ().kind() {
464464
ty::Array(ty, len) => {
465-
let len = len.kind().try_to_machine_usize(self.tcx).unwrap();
465+
let len = len.kind().try_to_target_usize(self.tcx).unwrap();
466466
let subarray_len = if from_end {
467467
// `to` counts from the end of the array
468468
len - to - from
@@ -642,7 +642,7 @@ impl<'tcx> GotocCtx<'tcx> {
642642
match before.mir_typ().kind() {
643643
//TODO, ask on zulip if we can ever have from_end here?
644644
ty::Array(elemt, length) => {
645-
let length = length.kind().try_to_machine_usize(self.tcx).unwrap();
645+
let length = length.kind().try_to_target_usize(self.tcx).unwrap();
646646
assert!(length >= min_length);
647647
let idx = if from_end { length - offset } else { offset };
648648
let idxe = Expr::int_constant(idx, Type::ssize_t());

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -143,7 +143,7 @@ impl<'tcx> GotocCtx<'tcx> {
143143
) -> Expr {
144144
let res_t = self.codegen_ty(res_ty);
145145
let op_expr = self.codegen_operand(op);
146-
let width = sz.try_eval_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap();
146+
let width = sz.try_eval_target_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap();
147147
Expr::struct_expr(
148148
res_t,
149149
btree_string_map![("0", op_expr.array_constant(width))],

kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ impl<'tcx> GotocCtx<'tcx> {
2828
let pretty_name = Instance::new(def_id, InternalSubsts::empty()).to_string();
2929
debug!(?symbol_name, ?pretty_name, "declare_static {}", item);
3030

31-
let typ = self.codegen_ty(self.tcx.type_of(def_id));
31+
let typ = self.codegen_ty(self.tcx.type_of(def_id).subst_identity());
3232
let span = self.tcx.def_span(def_id);
3333
let location = self.codegen_span(&span);
3434
let symbol = Symbol::static_variable(symbol_name.clone(), symbol_name, typ, location)

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

+20-20
Original file line numberDiff line numberDiff line change
@@ -272,7 +272,7 @@ impl<'tcx> GotocCtx<'tcx> {
272272
let env = prev_args[0];
273273

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

277277
return ty::Binder::bind_with_vars(
278278
self.tcx.mk_fn_sig(
@@ -297,14 +297,14 @@ impl<'tcx> GotocCtx<'tcx> {
297297

298298
// In addition to `def_id` and `substs`, we need to provide the kind of region `env_region`
299299
// in `closure_env_ty`, which we can build from the bound variables as follows
300-
let bound_vars = self.tcx.mk_bound_variable_kinds(
300+
let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(
301301
sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))),
302302
);
303303
let br = ty::BoundRegion {
304304
var: ty::BoundVar::from_usize(bound_vars.len() - 1),
305305
kind: ty::BoundRegionKind::BrEnv,
306306
};
307-
let env_region = ty::ReLateBound(ty::INNERMOST, br);
307+
let env_region = self.tcx.mk_re_late_bound(ty::INNERMOST, br);
308308
let env_ty = self.tcx.closure_env_ty(def_id, substs, env_region).unwrap();
309309

310310
let sig = sig.skip_binder();
@@ -314,7 +314,7 @@ impl<'tcx> GotocCtx<'tcx> {
314314
// * the rest of attributes are obtained from `sig`
315315
let sig = ty::Binder::bind_with_vars(
316316
self.tcx.mk_fn_sig(
317-
iter::once(env_ty).chain(iter::once(sig.inputs()[0])),
317+
[env_ty, sig.inputs()[0]],
318318
sig.output(),
319319
sig.c_variadic,
320320
sig.unsafety,
@@ -338,19 +338,19 @@ impl<'tcx> GotocCtx<'tcx> {
338338
) -> ty::PolyFnSig<'tcx> {
339339
let sig = substs.as_generator().poly_sig();
340340

341-
let bound_vars = self.tcx.mk_bound_variable_kinds(
341+
let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(
342342
sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))),
343343
);
344344
let br = ty::BoundRegion {
345345
var: ty::BoundVar::from_usize(bound_vars.len() - 1),
346346
kind: ty::BoundRegionKind::BrEnv,
347347
};
348348
let env_region = ty::ReLateBound(ty::INNERMOST, br);
349-
let env_ty = self.tcx.mk_mut_ref(self.tcx.mk_region(env_region), ty);
349+
let env_ty = self.tcx.mk_mut_ref(self.tcx.mk_region_from_kind(env_region), ty);
350350

351351
let pin_did = self.tcx.require_lang_item(LangItem::Pin, None);
352352
let pin_adt_ref = self.tcx.adt_def(pin_did);
353-
let pin_substs = self.tcx.intern_substs(&[env_ty.into()]);
353+
let pin_substs = self.tcx.mk_substs(&[env_ty.into()]);
354354
let env_ty = self.tcx.mk_adt(pin_adt_ref, pin_substs);
355355

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

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

390390
(sig.resume_ty, ret_ty)
391391
};
392392

393393
ty::Binder::bind_with_vars(
394394
tcx.mk_fn_sig(
395-
[env_ty, resume_ty].iter(),
396-
&ret_ty,
395+
[env_ty, resume_ty],
396+
ret_ty,
397397
false,
398398
Unsafety::Normal,
399399
rustc_target::spec::abi::Abi::Rust,
@@ -423,7 +423,7 @@ impl<'tcx> GotocCtx<'tcx> {
423423
impl<'tcx> GotocCtx<'tcx> {
424424
pub fn monomorphize<T>(&self, value: T) -> T
425425
where
426-
T: TypeFoldable<'tcx>,
426+
T: TypeFoldable<TyCtxt<'tcx>>,
427427
{
428428
// Instance is Some(..) only when current codegen unit is a function.
429429
if let Some(current_fn) = &self.current_fn {
@@ -778,7 +778,7 @@ impl<'tcx> GotocCtx<'tcx> {
778778
}
779779
ty::Foreign(defid) => self.codegen_foreign(ty, *defid),
780780
ty::Array(et, len) => {
781-
let evaluated_len = len.try_eval_usize(self.tcx, self.param_env()).unwrap();
781+
let evaluated_len = len.try_eval_target_usize(self.tcx, self.param_env()).unwrap();
782782
let array_name = format!("[{}; {evaluated_len}]", self.ty_mangled_name(*et));
783783
let array_pretty_name = format!("[{}; {evaluated_len}]", self.ty_pretty_name(*et));
784784
// wrap arrays into struct so that one can take advantage of struct copy in C
@@ -903,7 +903,7 @@ impl<'tcx> GotocCtx<'tcx> {
903903
fn codegen_alignment_padding(
904904
&self,
905905
size: Size,
906-
layout: &LayoutS<VariantIdx>,
906+
layout: &LayoutS,
907907
idx: usize,
908908
) -> Option<DatatypeComponent> {
909909
let align = Size::from_bits(layout.align.abi.bits());
@@ -928,7 +928,7 @@ impl<'tcx> GotocCtx<'tcx> {
928928
fn codegen_struct_fields(
929929
&mut self,
930930
flds: Vec<(String, Ty<'tcx>)>,
931-
layout: &LayoutS<VariantIdx>,
931+
layout: &LayoutS,
932932
initial_offset: Size,
933933
) -> Vec<DatatypeComponent> {
934934
match &layout.fields {
@@ -1386,7 +1386,7 @@ impl<'tcx> GotocCtx<'tcx> {
13861386
&mut self,
13871387
variant: &VariantDef,
13881388
subst: &'tcx InternalSubsts<'tcx>,
1389-
layout: &LayoutS<VariantIdx>,
1389+
layout: &LayoutS,
13901390
initial_offset: Size,
13911391
) -> Vec<DatatypeComponent> {
13921392
let flds: Vec<_> =
@@ -1555,7 +1555,7 @@ impl<'tcx> GotocCtx<'tcx> {
15551555
ty: Ty<'tcx>,
15561556
adtdef: &'tcx AdtDef,
15571557
subst: &'tcx InternalSubsts<'tcx>,
1558-
variants: &IndexVec<VariantIdx, LayoutS<VariantIdx>>,
1558+
variants: &IndexVec<VariantIdx, LayoutS>,
15591559
) -> Type {
15601560
let non_zst_count = variants.iter().filter(|layout| layout.size.bytes() > 0).count();
15611561
let mangled_name = self.ty_mangled_name(ty);
@@ -1574,7 +1574,7 @@ impl<'tcx> GotocCtx<'tcx> {
15741574

15751575
pub(crate) fn variant_min_offset(
15761576
&self,
1577-
variants: &IndexVec<VariantIdx, LayoutS<VariantIdx>>,
1577+
variants: &IndexVec<VariantIdx, LayoutS>,
15781578
) -> Option<Size> {
15791579
variants
15801580
.iter()
@@ -1658,7 +1658,7 @@ impl<'tcx> GotocCtx<'tcx> {
16581658
pretty_name: InternedString,
16591659
def: &'tcx AdtDef,
16601660
subst: &'tcx InternalSubsts<'tcx>,
1661-
layouts: &IndexVec<VariantIdx, LayoutS<VariantIdx>>,
1661+
layouts: &IndexVec<VariantIdx, LayoutS>,
16621662
initial_offset: Size,
16631663
) -> Vec<DatatypeComponent> {
16641664
def.variants()
@@ -1690,7 +1690,7 @@ impl<'tcx> GotocCtx<'tcx> {
16901690
pretty_name: InternedString,
16911691
case: &VariantDef,
16921692
subst: &'tcx InternalSubsts<'tcx>,
1693-
variant: &LayoutS<VariantIdx>,
1693+
variant: &LayoutS,
16941694
initial_offset: Size,
16951695
) -> Type {
16961696
let case_name = format!("{name}::{}", case.name);

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

+5-1
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ use rustc_codegen_ssa::traits::CodegenBackend;
2323
use rustc_codegen_ssa::{CodegenResults, CrateInfo};
2424
use rustc_data_structures::fx::FxHashMap;
2525
use rustc_data_structures::temp_dir::MaybeTempDir;
26-
use rustc_errors::ErrorGuaranteed;
26+
use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE};
2727
use rustc_hir::def_id::LOCAL_CRATE;
2828
use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
2929
use rustc_metadata::EncodedMetadata;
@@ -70,6 +70,10 @@ impl GotocCodegenBackend {
7070
}
7171

7272
impl CodegenBackend for GotocCodegenBackend {
73+
fn locale_resource(&self) -> &'static str {
74+
DEFAULT_LOCALE_RESOURCE
75+
}
76+
7377
fn metadata_loader(&self) -> Box<MetadataLoaderDyn> {
7478
Box::new(rustc_codegen_ssa::back::metadata::DefaultMetadataLoader)
7579
}

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

+1
Original file line numberDiff line numberDiff line change
@@ -422,6 +422,7 @@ impl<'tcx> FnAbiOfHelpers<'tcx> for GotocCtx<'tcx> {
422422
}
423423
}
424424

425+
#[derive(Debug)]
425426
pub struct GotocMetadataLoader();
426427
impl MetadataLoader for GotocMetadataLoader {
427428
fn get_rlib_metadata(&self, _: &Target, _filename: &Path) -> Result<MetadataRef, String> {

kani-compiler/src/kani_middle/provide.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,10 @@
66
77
use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items};
88
use crate::kani_middle::stubbing;
9+
use crate::kani_middle::ty::query::query_provided::collect_and_partition_mono_items;
910
use kani_queries::{QueryDb, UserInput};
1011
use rustc_hir::def_id::DefId;
1112
use rustc_interface;
12-
use rustc_middle::ty::query::query_stored::collect_and_partition_mono_items;
1313
use rustc_middle::{
1414
mir::Body,
1515
ty::{query::ExternProviders, query::Providers, TyCtxt},

kani-compiler/src/kani_middle/reachability.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -215,7 +215,7 @@ struct MonoItemsFnCollector<'a, 'tcx> {
215215
impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
216216
fn monomorphize<T>(&self, value: T) -> T
217217
where
218-
T: TypeFoldable<'tcx>,
218+
T: TypeFoldable<TyCtxt<'tcx>>,
219219
{
220220
trace!(instance=?self.instance, ?value, "monomorphize");
221221
self.instance.subst_mir_and_normalize_erasing_regions(

kani-compiler/src/session.rs

+3-3
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ use crate::parser;
77
use clap::ArgMatches;
88
use rustc_errors::{
99
emitter::Emitter, emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter,
10-
ColorConfig, Diagnostic,
10+
ColorConfig, Diagnostic, TerminalUrl, DEFAULT_LOCALE_RESOURCE,
1111
};
1212
use std::panic;
1313
use std::str::FromStr;
@@ -47,8 +47,7 @@ static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send
4747
panic::set_hook(Box::new(|info| {
4848
// Print stack trace.
4949
let msg = format!("Kani unexpectedly panicked at {info}.",);
50-
let fallback_bundle =
51-
fallback_fluent_bundle(rustc_errors::DEFAULT_LOCALE_RESOURCES, false);
50+
let fallback_bundle = fallback_fluent_bundle(vec![DEFAULT_LOCALE_RESOURCE], false);
5251
let mut emitter = JsonEmitter::basic(
5352
false,
5453
HumanReadableErrorType::Default(ColorConfig::Never),
@@ -57,6 +56,7 @@ static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send
5756
None,
5857
false,
5958
false,
59+
TerminalUrl::No,
6060
);
6161
let diagnostic = Diagnostic::new(rustc_errors::Level::Bug, msg);
6262
emitter.emit_diagnostic(&diagnostic);

rust-toolchain.toml

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2023-02-03"
5+
channel = "nightly-2023-03-09"
66
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

tools/bookrunner/librustdoc/doctest.rs

+3-1
Original file line numberDiff line numberDiff line change
@@ -79,7 +79,7 @@ pub fn make_test(
7979
let sm = Lrc::new(SourceMap::new(FilePathMapping::empty()));
8080

8181
let fallback_bundle =
82-
rustc_errors::fallback_fluent_bundle(rustc_errors::DEFAULT_LOCALE_RESOURCES, false);
82+
rustc_errors::fallback_fluent_bundle(vec![rustc_errors::DEFAULT_LOCALE_RESOURCE], false);
8383
supports_color = EmitterWriter::stderr(
8484
ColorConfig::Auto,
8585
None,
@@ -90,6 +90,7 @@ pub fn make_test(
9090
Some(80),
9191
false,
9292
false,
93+
rustc_errors::TerminalUrl::Auto,
9394
)
9495
.supports_color();
9596

@@ -104,6 +105,7 @@ pub fn make_test(
104105
None,
105106
false,
106107
false,
108+
rustc_errors::TerminalUrl::Auto,
107109
);
108110

109111
// FIXME(misdreavus): pass `-Z treat-err-as-bug` to the doctest parser

0 commit comments

Comments
 (0)