Skip to content

Commit

Permalink
Update toolchain to nightly-2024-11-26 (#3740)
Browse files Browse the repository at this point in the history
Fix required due to the following changes to Rust's internal API:
- rust-lang/rust#132460
- rust-lang/rust#133212
- rust-lang/rust#131326

Resolves #3731

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
  • Loading branch information
celinval and zhassan-aws authored Nov 28, 2024
1 parent 69b8b37 commit 4f5e53e
Show file tree
Hide file tree
Showing 13 changed files with 74 additions and 48 deletions.
5 changes: 3 additions & 2 deletions kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -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(&paramtc.name),
Expand Down
10 changes: 5 additions & 5 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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(
Expand All @@ -756,7 +756,7 @@ impl GotocCtx<'_> {
.tcx
.check_validity_requirement((
ValidityRequirement::UninitMitigated0x01Fill,
param_env_and_type,
typing_env_and_type,
))
.unwrap()
{
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -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)| {
(
Expand Down
5 changes: 3 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -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(),
);
Expand Down
25 changes: 16 additions & 9 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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.
Expand Down Expand Up @@ -523,7 +523,8 @@ impl<'tcx> GotocCtx<'tcx> {
/// c.f. <https://rust-lang.github.io/unsafe-code-guidelines/introduction.html>
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(|| {
Expand Down Expand Up @@ -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) => {
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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))
}

Expand Down
10 changes: 5 additions & 5 deletions kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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()
}
}

Expand Down
9 changes: 6 additions & 3 deletions kani-compiler/src/kani_middle/coercion.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -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!(
Expand Down Expand Up @@ -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()
}
Expand Down
11 changes: 9 additions & 2 deletions kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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. */ }
}
}
Expand Down Expand Up @@ -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."
Expand Down
10 changes: 7 additions & 3 deletions kani-compiler/src/kani_middle/stubbing/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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),
)
}
Expand All @@ -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;
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
3 changes: 2 additions & 1 deletion tests/expected/llbc/enum/expected
Original file line number Diff line number Diff line change
Expand Up @@ -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
}

25 changes: 13 additions & 12 deletions tests/expected/llbc/projection/expected
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
}

3 changes: 2 additions & 1 deletion tests/expected/llbc/struct/expected
Original file line number Diff line number Diff line change
Expand Up @@ -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
}

0 comments on commit 4f5e53e

Please sign in to comment.