diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index fc88333f8325..e249a747b08b 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; @@ -783,11 +783,16 @@ 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"), @@ -795,7 +800,14 @@ impl<'tcx> GotocCtx<'tcx> { ); } - 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, @@ -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", diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 5bb66a7dff76..8342364f4279 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -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 { @@ -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()), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 67801f747acc..b051ec204373 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -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 @@ -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()); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index d06fabd27b0e..f1d6d37fb5ce 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -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))], 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 278f246161eb..695af6acc312 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,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(); @@ -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 { @@ -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 @@ -903,7 +903,7 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_alignment_padding( &self, size: Size, - layout: &LayoutS, + layout: &LayoutS, idx: usize, ) -> Option { let align = Size::from_bits(layout.align.abi.bits()); @@ -928,7 +928,7 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_struct_fields( &mut self, flds: Vec<(String, Ty<'tcx>)>, - layout: &LayoutS, + layout: &LayoutS, initial_offset: Size, ) -> Vec { match &layout.fields { @@ -1386,7 +1386,7 @@ impl<'tcx> GotocCtx<'tcx> { &mut self, variant: &VariantDef, subst: &'tcx InternalSubsts<'tcx>, - layout: &LayoutS, + layout: &LayoutS, initial_offset: Size, ) -> Vec { let flds: Vec<_> = @@ -1555,7 +1555,7 @@ impl<'tcx> GotocCtx<'tcx> { ty: Ty<'tcx>, adtdef: &'tcx AdtDef, subst: &'tcx InternalSubsts<'tcx>, - variants: &IndexVec>, + variants: &IndexVec, ) -> Type { let non_zst_count = variants.iter().filter(|layout| layout.size.bytes() > 0).count(); let mangled_name = self.ty_mangled_name(ty); @@ -1574,7 +1574,7 @@ impl<'tcx> GotocCtx<'tcx> { pub(crate) fn variant_min_offset( &self, - variants: &IndexVec>, + variants: &IndexVec, ) -> Option { variants .iter() @@ -1658,7 +1658,7 @@ impl<'tcx> GotocCtx<'tcx> { pretty_name: InternedString, def: &'tcx AdtDef, subst: &'tcx InternalSubsts<'tcx>, - layouts: &IndexVec>, + layouts: &IndexVec, initial_offset: Size, ) -> Vec { def.variants() @@ -1690,7 +1690,7 @@ impl<'tcx> GotocCtx<'tcx> { pretty_name: InternedString, case: &VariantDef, subst: &'tcx InternalSubsts<'tcx>, - variant: &LayoutS, + variant: &LayoutS, initial_offset: Size, ) -> Type { let case_name = format!("{name}::{}", case.name); 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 9b83d55a8c34..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, + 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), @@ -57,6 +56,7 @@ static JSON_PANIC_HOOK: LazyLock) + Sync + Send None, false, false, + TerminalUrl::No, ); let diagnostic = Diagnostic::new(rustc_errors::Level::Bug, msg); emitter.emit_diagnostic(&diagnostic); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index a173312be9b8..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-03" +channel = "nightly-2023-03-09" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]