diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index d657de37c601..f999257df880 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -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; @@ -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, @@ -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, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs index dfea9d31858d..42eb3982b08f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs @@ -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) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 6520b330af03..49e8a23eea00 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -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( @@ -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 { @@ -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, @@ -338,7 +338,7 @@ 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 { @@ -346,11 +346,11 @@ impl<'tcx> GotocCtx<'tcx> { 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(); @@ -363,7 +363,7 @@ impl<'tcx> GotocCtx<'tcx> { // The signature should be `Future::poll(_, &mut Context<'_>) -> Poll` 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 @@ -384,7 +384,7 @@ impl<'tcx> GotocCtx<'tcx> { // The signature should be `Generator::resume(_, Resume) -> GeneratorState` 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) @@ -392,8 +392,8 @@ impl<'tcx> GotocCtx<'tcx> { 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, @@ -423,7 +423,7 @@ impl<'tcx> GotocCtx<'tcx> { impl<'tcx> GotocCtx<'tcx> { pub fn monomorphize(&self, value: T) -> T where - T: TypeFoldable<'tcx>, + T: TypeFoldable>, { // Instance is Some(..) only when current codegen unit is a function. if let Some(current_fn) = &self.current_fn { diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 100fba0ef281..b66132a2ff87 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -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; @@ -70,6 +70,10 @@ impl GotocCodegenBackend { } impl CodegenBackend for GotocCodegenBackend { + fn locale_resource(&self) -> &'static str { + DEFAULT_LOCALE_RESOURCE + } + fn metadata_loader(&self) -> Box { Box::new(rustc_codegen_ssa::back::metadata::DefaultMetadataLoader) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 1d9d2fbaa403..1567d4ec65c8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -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 { diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index 990b56639890..03cf5bd5d9f6 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -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}, diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 7845f4bab4ca..2f6b3464cdcb 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -215,7 +215,7 @@ struct MonoItemsFnCollector<'a, 'tcx> { impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { fn monomorphize(&self, value: T) -> T where - T: TypeFoldable<'tcx>, + T: TypeFoldable>, { trace!(instance=?self.instance, ?value, "monomorphize"); self.instance.subst_mir_and_normalize_erasing_regions( diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index 99d7b7239d05..2be20d3d341d 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -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; @@ -47,8 +47,7 @@ static JSON_PANIC_HOOK: LazyLock) + 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), diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 621fdb226fe7..143f16eaa457 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -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"] diff --git a/tools/bookrunner/librustdoc/doctest.rs b/tools/bookrunner/librustdoc/doctest.rs index 58f6ea8d1b18..88a4ea218a89 100644 --- a/tools/bookrunner/librustdoc/doctest.rs +++ b/tools/bookrunner/librustdoc/doctest.rs @@ -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,