diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs index 62a772fc6873..24cb007be0b8 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -46,7 +46,7 @@ use charon_lib::ullbc_ast::{ use charon_lib::{error_assert, error_or_panic}; use core::panic; use rustc_data_structures::fx::FxHashMap; -use rustc_middle::ty::TyCtxt; +use rustc_middle::ty::{TyCtxt, TypingEnv}; use rustc_smir::rustc_internal; use stable_mir::abi::PassMode; use stable_mir::mir::mono::{Instance, InstanceDef}; @@ -226,7 +226,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> { GenericArgKind::Const(tc) => match tc.kind() { TyConstKind::Param(paramtc) => { let def_id_internal = rustc_internal::internal(self.tcx, adtdef.def_id()); - let paramenv = self.tcx.param_env(def_id_internal); + let paramenv = + TypingEnv::post_analysis(self.tcx, def_id_internal).param_env; let pc_internal = rustc_middle::ty::ParamConst { index: paramtc.index, name: rustc_span::Symbol::intern(¶mtc.name), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 3a72fd45fa35..a1daeec5f88b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -10,7 +10,7 @@ use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{ ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type, }; -use rustc_middle::ty::ParamEnv; +use rustc_middle::ty::TypingEnv; use rustc_middle::ty::layout::ValidityRequirement; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; @@ -730,15 +730,15 @@ impl GotocCtx<'_> { ); } - let param_env_and_type = - ParamEnv::reveal_all().and(rustc_internal::internal(self.tcx, target_ty)); + let typing_env_and_type = TypingEnv::fully_monomorphized() + .as_query_input(rustc_internal::internal(self.tcx, target_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 - .check_validity_requirement((ValidityRequirement::Zero, param_env_and_type)) + .check_validity_requirement((ValidityRequirement::Zero, typing_env_and_type)) .unwrap() { return self.codegen_fatal_error( @@ -756,7 +756,7 @@ impl GotocCtx<'_> { .tcx .check_validity_requirement(( ValidityRequirement::UninitMitigated0x01Fill, - param_env_and_type, + typing_env_and_type, )) .unwrap() { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index c5f2f9fd2c08..f84e0a89f937 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -18,7 +18,7 @@ use cbmc::goto_program::{ }; use cbmc::{InternString, InternedString, btree_string_map}; use num::bigint::BigInt; -use rustc_middle::ty::{ParamEnv, TyCtxt, VtblEntry}; +use rustc_middle::ty::{TyCtxt, TypingEnv, VtblEntry}; use rustc_smir::rustc_internal; use rustc_target::abi::{FieldsShape, TagEncoding, Variants}; use stable_mir::abi::{Primitive, Scalar, ValueAbi}; @@ -832,7 +832,7 @@ impl GotocCtx<'_> { NullOp::OffsetOf(fields) => Expr::int_constant( self.tcx .offset_of_subfield( - ParamEnv::reveal_all(), + TypingEnv::fully_monomorphized(), layout, fields.iter().map(|(var_idx, field_idx)| { ( diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 8171c5ffdda3..12a61c45b558 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -8,7 +8,7 @@ use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{Expr, Location, Stmt, Type}; use rustc_middle::ty::layout::LayoutOf; -use rustc_middle::ty::{List, ParamEnv}; +use rustc_middle::ty::{List, TypingEnv}; use rustc_smir::rustc_internal; use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants}; use stable_mir::abi::{ArgAbi, FnAbi, PassMode}; @@ -663,7 +663,8 @@ impl GotocCtx<'_> { let fn_ptr_abi = rustc_internal::stable( self.tcx .fn_abi_of_fn_ptr( - ParamEnv::reveal_all().and((fn_sig_internal, &List::empty())), + TypingEnv::fully_monomorphized() + .as_query_input((fn_sig_internal, &List::empty())), ) .unwrap(), ); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index ff553c67a738..903baf8eaced 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -229,7 +229,7 @@ impl<'tcx> GotocCtx<'tcx> { if let Some(current_fn) = &self.current_fn { current_fn.instance().instantiate_mir_and_normalize_erasing_regions( self.tcx, - ty::ParamEnv::reveal_all(), + ty::TypingEnv::fully_monomorphized(), ty::EarlyBinder::bind(value), ) } else { @@ -251,7 +251,7 @@ impl<'tcx> GotocCtx<'tcx> { pub fn is_unsized(&self, t: Ty<'tcx>) -> bool { !self .monomorphize(t) - .is_sized(*self.tcx.at(rustc_span::DUMMY_SP), ty::ParamEnv::reveal_all()) + .is_sized(*self.tcx.at(rustc_span::DUMMY_SP), ty::TypingEnv::fully_monomorphized()) } /// Generates the type for a single field for a dynamic vtable. @@ -523,7 +523,8 @@ impl<'tcx> GotocCtx<'tcx> { /// c.f. pub fn codegen_ty(&mut self, ty: Ty<'tcx>) -> Type { // TODO: Remove all monomorphize calls - let normalized = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), ty); + let normalized = + self.tcx.normalize_erasing_regions(ty::TypingEnv::fully_monomorphized(), ty); let goto_typ = self.codegen_ty_inner(normalized); if let Some(tag) = goto_typ.tag() { self.type_map.entry(tag).or_insert_with(|| { @@ -573,10 +574,14 @@ impl<'tcx> GotocCtx<'tcx> { ty::Str => Type::unsigned_int(8).flexible_array_of(), ty::Ref(_, t, _) | ty::RawPtr(t, _) => self.codegen_ty_ref(*t), ty::FnDef(def_id, args) => { - let instance = - Instance::try_resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args) - .unwrap() - .unwrap(); + let instance = Instance::try_resolve( + self.tcx, + ty::TypingEnv::fully_monomorphized(), + *def_id, + args, + ) + .unwrap() + .unwrap(); self.codegen_fndef_type(instance) } ty::FnPtr(sig_tys, hdr) => { @@ -980,7 +985,7 @@ impl<'tcx> GotocCtx<'tcx> { // Normalize pointee_type to remove projection and opaque types trace!(?pointee_type, "codegen_ty_ref"); let pointee_type = - self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), pointee_type); + self.tcx.normalize_erasing_regions(ty::TypingEnv::fully_monomorphized(), pointee_type); if !self.use_thin_pointer(pointee_type) { return self.codegen_fat_ptr(pointee_type); @@ -1076,7 +1081,9 @@ impl<'tcx> GotocCtx<'tcx> { /// one can only apply this function to a monomorphized signature pub fn codegen_function_sig(&mut self, sig: PolyFnSig<'tcx>) -> Type { let sig = self.monomorphize(sig); - let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig); + let sig = self + .tcx + .normalize_erasing_late_bound_regions(ty::TypingEnv::fully_monomorphized(), sig); self.codegen_function_sig_stable(rustc_internal::stable(sig)) } 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 6fd9da651002..0e5e72af70b6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -29,8 +29,8 @@ use cbmc::{InternedString, MachineModel}; use rustc_data_structures::fx::FxHashMap; use rustc_middle::span_bug; use rustc_middle::ty::layout::{ - FnAbiError, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError, LayoutOfHelpers, - TyAndLayout, + FnAbiError, FnAbiOfHelpers, FnAbiRequest, HasTyCtxt, HasTypingEnv, LayoutError, + LayoutOfHelpers, TyAndLayout, }; use rustc_middle::ty::{self, Ty, TyCtxt}; use rustc_span::Span; @@ -337,9 +337,9 @@ impl<'tcx> LayoutOfHelpers<'tcx> for GotocCtx<'tcx> { } } -impl<'tcx> HasParamEnv<'tcx> for GotocCtx<'tcx> { - fn param_env(&self) -> ty::ParamEnv<'tcx> { - ty::ParamEnv::reveal_all() +impl<'tcx> HasTypingEnv<'tcx> for GotocCtx<'tcx> { + fn typing_env(&self) -> ty::TypingEnv<'tcx> { + ty::TypingEnv::fully_monomorphized() } } diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index ebef669e0f5d..afb0ff5e6c73 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -17,7 +17,7 @@ use rustc_hir::lang_items::LangItem; use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData}; use rustc_middle::ty::TraitRef; use rustc_middle::ty::adjustment::CustomCoerceUnsized; -use rustc_middle::ty::{ParamEnv, Ty, TyCtxt}; +use rustc_middle::ty::{PseudoCanonicalInput, Ty, TyCtxt, TypingEnv}; use rustc_smir::rustc_internal; use stable_mir::Symbol; use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind}; @@ -102,7 +102,7 @@ pub fn extract_unsize_casting<'tcx>( let (src_base_ty, dst_base_ty) = tcx.struct_lockstep_tails_for_codegen( src_pointee_ty, dst_pointee_ty, - ParamEnv::reveal_all(), + TypingEnv::fully_monomorphized(), ); trace!(?src_base_ty, ?dst_base_ty, "extract_unsize_casting result"); assert!( @@ -251,7 +251,10 @@ fn custom_coerce_unsize_info<'tcx>( let trait_ref = TraitRef::new(tcx, def_id, tcx.mk_args_trait(source_ty, [target_ty.into()])); - match tcx.codegen_select_candidate((ParamEnv::reveal_all(), trait_ref)) { + match tcx.codegen_select_candidate(PseudoCanonicalInput { + typing_env: TypingEnv::fully_monomorphized(), + value: trait_ref, + }) { Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { impl_def_id, .. })) => { tcx.coerce_unsized_info(impl_def_id).unwrap().custom_kind.unwrap() } diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 8d9f14b3f969..369296db6ed4 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -38,7 +38,7 @@ use rustc_middle::{ ProjectionElem, Rvalue, Statement, StatementKind, Terminator, TerminatorEdges, TerminatorKind, }, - ty::{Instance, InstanceKind, List, ParamEnv, TyCtxt, TyKind}, + ty::{Instance, InstanceKind, List, TyCtxt, TyKind, TypingEnv}, }; use rustc_mir_dataflow::{Analysis, Forward, JoinSemiLattice}; use rustc_smir::rustc_internal; @@ -179,6 +179,7 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> { | StatementKind::AscribeUserType(..) | StatementKind::Coverage(..) | StatementKind::ConstEvalCounter + | StatementKind::BackwardIncompatibleDropHint { .. } | StatementKind::Nop => { /* This is a no-op with regard to aliasing. */ } } } @@ -356,7 +357,13 @@ fn try_resolve_instance<'tcx>( TyKind::FnDef(def, args) => { // Span here is used for error-reporting, which we don't expect to encounter anyway, so // it is ok to use a dummy. - Ok(Instance::expect_resolve(tcx, ParamEnv::reveal_all(), *def, &args, DUMMY_SP)) + Ok(Instance::expect_resolve( + tcx, + TypingEnv::fully_monomorphized(), + *def, + &args, + DUMMY_SP, + )) } _ => Err(format!( "Kani was not able to resolve the instance of the function operand `{ty:?}`. Currently, memory initialization checks in presence of function pointers and vtable calls are not supported. For more information about planned support, see https://github.com/model-checking/kani/issues/3300." diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 90bb0173ac55..d70e884400bb 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -12,7 +12,7 @@ use tracing::{debug, trace}; use kani_metadata::HarnessMetadata; use rustc_hir::def_id::DefId; use rustc_middle::mir::Const; -use rustc_middle::ty::{self, EarlyBinder, ParamEnv, TyCtxt, TypeFoldable}; +use rustc_middle::ty::{self, EarlyBinder, TyCtxt, TypeFoldable, TypingEnv}; use rustc_smir::rustc_internal; use stable_mir::mir::ConstOperand; use stable_mir::mir::mono::Instance; @@ -152,7 +152,7 @@ impl<'tcx> StubConstChecker<'tcx> { trace!(instance=?self.instance, ?value, "monomorphize"); self.instance.instantiate_mir_and_normalize_erasing_regions( self.tcx, - ParamEnv::reveal_all(), + TypingEnv::fully_monomorphized(), EarlyBinder::bind(value), ) } @@ -171,7 +171,11 @@ impl MirVisitor for StubConstChecker<'_> { Const::Val(..) | Const::Ty(..) => {} Const::Unevaluated(un_eval, _) => { // Thread local fall into this category. - if self.tcx.const_eval_resolve(ParamEnv::reveal_all(), un_eval, DUMMY_SP).is_err() { + if self + .tcx + .const_eval_resolve(TypingEnv::fully_monomorphized(), un_eval, DUMMY_SP) + .is_err() + { // The `monomorphize` call should have evaluated that constant already. let tcx = self.tcx; let mono_const = &un_eval; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index a2d54d0caf15..e216a29bcbd0 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-11-19" +channel = "nightly-2024-11-26" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/llbc/enum/expected b/tests/expected/llbc/enum/expected index 6c86139a52e8..10409fdab8e8 100644 --- a/tests/expected/llbc/enum/expected +++ b/tests/expected/llbc/enum/expected @@ -29,8 +29,9 @@ fn test::main() let i@2: i32; // local e@1 := test::MyEnum::A { 0: const (1 : i32) } - i@2 := @Fun0(move (e@1)) + i@2 := @Fun1(move (e@1)) drop i@2 @0 := () return } + diff --git a/tests/expected/llbc/projection/expected b/tests/expected/llbc/projection/expected index 5f71248c8d44..50f7758ad86f 100644 --- a/tests/expected/llbc/projection/expected +++ b/tests/expected/llbc/projection/expected @@ -5,22 +5,22 @@ struct test::MyStruct = } enum test::MyEnum0 = -| A(0: @Adt1, 1: i32) +| A(0: @Adt0, 1: i32) | B() enum test::MyEnum = -| A(0: @Adt1, 1: @Adt2) +| A(0: @Adt0, 1: @Adt2) | B(0: (i32, i32)) -fn test::enum_match(@1: @Adt0) -> i32 +fn test::enum_match(@1: @Adt1) -> i32 { let @0: i32; // return - let e@1: @Adt0; // arg #1 - let s@2: @Adt1; // local + let e@1: @Adt1; // arg #1 + let s@2: @Adt0; // local let e0@3: @Adt2; // local - let s1@4: @Adt1; // local + let s1@4: @Adt0; // local let b@5: i32; // local let @6: i32; // anonymous local let @7: i32; // anonymous local @@ -66,19 +66,20 @@ fn test::enum_match(@1: @Adt0) -> i32 fn test::main() { let @0: (); // return - let s@1: @Adt1; // local - let s0@2: @Adt1; // local - let e@3: @Adt0; // local + let s@1: @Adt0; // local + let s0@2: @Adt0; // local + let e@3: @Adt1; // local let @4: @Adt2; // anonymous local let i@5: i32; // local - s@1 := @Adt1 { a: const (1 : i32), b: const (2 : i32) } - s0@2 := @Adt1 { a: const (1 : i32), b: const (2 : i32) } + s@1 := @Adt0 { a: const (1 : i32), b: const (2 : i32) } + s0@2 := @Adt0 { a: const (1 : i32), b: const (2 : i32) } @4 := test::MyEnum0::A { 0: move (s0@2), 1: const (1 : i32) } e@3 := test::MyEnum::A { 0: move (s@1), 1: move (@4) } drop @4 - i@5 := @Fun0(move (e@3)) + i@5 := @Fun1(move (e@3)) drop i@5 @0 := () return } + diff --git a/tests/expected/llbc/struct/expected b/tests/expected/llbc/struct/expected index e686cfaed0bc..a81e73b38895 100644 --- a/tests/expected/llbc/struct/expected +++ b/tests/expected/llbc/struct/expected @@ -20,8 +20,9 @@ fn test::main() let a@2: i32; // local s@1 := @Adt0 { a: const (1 : i32), b: const (true) } - a@2 := @Fun1(move (s@1)) + a@2 := @Fun0(move (s@1)) drop a@2 @0 := () return } +