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
model-checking · Mar 17, 2023 · 30eb983 · 30eb983
1 parent 048b598
commit 30eb983
Show file tree

Hide file tree

Showing 13 changed files with 70 additions and 47 deletions.
diff --git 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,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,
@@ -1226,14 +1238,16 @@ 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(|| {
-                        self.tcx.sess.span_err(
-                            span.unwrap(),
-                            "could not evaluate shuffle index array length",
-                        );
-                        // Return a dummy value
-                        u64::MIN
-                    })
+                    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",
+                            );
+                            // Return a dummy value
+                            u64::MIN
+                        },
+                    )
                 }
                 _ => {
                     let err_msg = format!(

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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,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();
@@ -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
@@ -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,
@@ -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 {
@@ -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<VariantIdx>,
+        layout: &LayoutS,
         idx: usize,
     ) -> Option<DatatypeComponent> {
         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<VariantIdx>,
+        layout: &LayoutS,
         initial_offset: Size,
     ) -> Vec<DatatypeComponent> {
         match &layout.fields {
@@ -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<_> =
@@ -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);
@@ -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()
@@ -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()
@@ -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);

diff --git 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<MetadataLoaderDyn> {
         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
@@ -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> {

diff --git 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
@@ -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(

diff --git 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<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),
@@ -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);

diff --git 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"]