Skip to content

Commit f8fabc4

Browse files
celinvalgithub-actions[bot]tautschnigqinhepingfeliperodri
authored
Upgrade Rust toolchain to nightly-2024-01-23 (#2983)
Related PRs so far: - rust-lang/rust#119869 - rust-lang/rust#120080 - rust-lang/rust#120128 - rust-lang/rust#119369 - rust-lang/rust#116672 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Signed-off-by: Felipe R. Monteiro <[email protected]> Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> Co-authored-by: tautschnig <[email protected]> Co-authored-by: Qinheping Hu <[email protected]> Co-authored-by: Michael Tautschnig <[email protected]> Co-authored-by: Felipe R. Monteiro <[email protected]>
1 parent f08a3e9 commit f8fabc4

File tree

26 files changed

+157
-139
lines changed

26 files changed

+157
-139
lines changed

‎kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ impl<'tcx> GotocCtx<'tcx> {
3939

4040
let mut instance_under_contract = items.iter().filter_map(|i| match i {
4141
MonoItem::Fn(instance @ Instance { def, .. })
42-
if wrapped_fn == rustc_internal::internal(def.def_id()) =>
42+
if wrapped_fn == rustc_internal::internal(tcx, def.def_id()) =>
4343
{
4444
Some(*instance)
4545
}

‎kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

+27-23
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
//! this module handles intrinsics
44
use super::typ;
55
use super::{bb_label, PropertyClass};
6-
use crate::codegen_cprover_gotoc::codegen::ty_stable::{pointee_type_stable, pretty_ty};
6+
use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
77
use crate::codegen_cprover_gotoc::{utils, GotocCtx};
88
use crate::unwrap_or_return_codegen_unimplemented_stmt;
99
use cbmc::goto_program::{
@@ -646,7 +646,7 @@ impl<'tcx> GotocCtx<'tcx> {
646646
span,
647647
format!(
648648
"Type check failed for intrinsic `{name}`: Expected {expected}, found {}",
649-
pretty_ty(actual)
649+
self.pretty_ty(actual)
650650
),
651651
);
652652
self.tcx.dcx().abort_if_errors();
@@ -779,12 +779,16 @@ impl<'tcx> GotocCtx<'tcx> {
779779
if layout.abi.is_uninhabited() {
780780
return self.codegen_fatal_error(
781781
PropertyClass::SafetyCheck,
782-
&format!("attempted to instantiate uninhabited type `{}`", pretty_ty(*target_ty)),
782+
&format!(
783+
"attempted to instantiate uninhabited type `{}`",
784+
self.pretty_ty(*target_ty)
785+
),
783786
span,
784787
);
785788
}
786789

787-
let param_env_and_type = ParamEnv::reveal_all().and(rustc_internal::internal(target_ty));
790+
let param_env_and_type =
791+
ParamEnv::reveal_all().and(rustc_internal::internal(self.tcx, target_ty));
788792

789793
// Then we check if the type allows "raw" initialization for the cases
790794
// where memory is zero-initialized or entirely uninitialized
@@ -798,7 +802,7 @@ impl<'tcx> GotocCtx<'tcx> {
798802
PropertyClass::SafetyCheck,
799803
&format!(
800804
"attempted to zero-initialize type `{}`, which is invalid",
801-
pretty_ty(*target_ty)
805+
self.pretty_ty(*target_ty)
802806
),
803807
span,
804808
);
@@ -817,7 +821,7 @@ impl<'tcx> GotocCtx<'tcx> {
817821
PropertyClass::SafetyCheck,
818822
&format!(
819823
"attempted to leave type `{}` uninitialized, which is invalid",
820-
pretty_ty(*target_ty)
824+
self.pretty_ty(*target_ty)
821825
),
822826
span,
823827
);
@@ -1285,7 +1289,7 @@ impl<'tcx> GotocCtx<'tcx> {
12851289
_ => {
12861290
let err_msg = format!(
12871291
"simd_shuffle index must be an array of `u32`, got `{}`",
1288-
pretty_ty(farg_types[2])
1292+
self.pretty_ty(farg_types[2])
12891293
);
12901294
utils::span_err(self.tcx, span, err_msg);
12911295
// Return a dummy value
@@ -1378,7 +1382,7 @@ impl<'tcx> GotocCtx<'tcx> {
13781382

13791383
// Packed types ignore the alignment of their fields.
13801384
if let TyKind::RigidTy(RigidTy::Adt(def, _)) = ty.kind() {
1381-
if rustc_internal::internal(def).repr().packed() {
1385+
if rustc_internal::internal(self.tcx, def).repr().packed() {
13821386
unsized_align = sized_align.clone();
13831387
}
13841388
}
@@ -1426,9 +1430,9 @@ impl<'tcx> GotocCtx<'tcx> {
14261430
if rust_ret_type != vector_base_type {
14271431
let err_msg = format!(
14281432
"expected return type `{}` (element of input `{}`), found `{}`",
1429-
pretty_ty(vector_base_type),
1430-
pretty_ty(rust_arg_types[0]),
1431-
pretty_ty(rust_ret_type)
1433+
self.pretty_ty(vector_base_type),
1434+
self.pretty_ty(rust_arg_types[0]),
1435+
self.pretty_ty(rust_ret_type)
14321436
);
14331437
utils::span_err(self.tcx, span, err_msg);
14341438
}
@@ -1466,9 +1470,9 @@ impl<'tcx> GotocCtx<'tcx> {
14661470
if vector_base_type != rust_arg_types[2] {
14671471
let err_msg = format!(
14681472
"expected inserted type `{}` (element of input `{}`), found `{}`",
1469-
pretty_ty(vector_base_type),
1470-
pretty_ty(rust_arg_types[0]),
1471-
pretty_ty(rust_arg_types[2]),
1473+
self.pretty_ty(vector_base_type),
1474+
self.pretty_ty(rust_arg_types[0]),
1475+
self.pretty_ty(rust_arg_types[2]),
14721476
);
14731477
utils::span_err(self.tcx, span, err_msg);
14741478
}
@@ -1534,8 +1538,8 @@ impl<'tcx> GotocCtx<'tcx> {
15341538
"expected return type with length {} (same as input type `{}`), \
15351539
found `{}` with length {}",
15361540
arg1.typ().len().unwrap(),
1537-
pretty_ty(rust_arg_types[0]),
1538-
pretty_ty(rust_ret_type),
1541+
self.pretty_ty(rust_arg_types[0]),
1542+
self.pretty_ty(rust_ret_type),
15391543
ret_typ.len().unwrap()
15401544
);
15411545
utils::span_err(self.tcx, span, err_msg);
@@ -1545,8 +1549,8 @@ impl<'tcx> GotocCtx<'tcx> {
15451549
let (_, rust_base_type) = self.simd_size_and_type(rust_ret_type);
15461550
let err_msg = format!(
15471551
"expected return type with integer elements, found `{}` with non-integer `{}`",
1548-
pretty_ty(rust_ret_type),
1549-
pretty_ty(rust_base_type),
1552+
self.pretty_ty(rust_ret_type),
1553+
self.pretty_ty(rust_base_type),
15501554
);
15511555
utils::span_err(self.tcx, span, err_msg);
15521556
}
@@ -1740,18 +1744,18 @@ impl<'tcx> GotocCtx<'tcx> {
17401744
if ret_type_len != n {
17411745
let err_msg = format!(
17421746
"expected return type of length {n}, found `{}` with length {ret_type_len}",
1743-
pretty_ty(rust_ret_type),
1747+
self.pretty_ty(rust_ret_type),
17441748
);
17451749
utils::span_err(self.tcx, span, err_msg);
17461750
}
17471751
if vec_subtype != ret_type_subtype {
17481752
let err_msg = format!(
17491753
"expected return element type `{}` (element of input `{}`), \
17501754
found `{}` with element type `{}`",
1751-
pretty_ty(vec_subtype),
1752-
pretty_ty(rust_arg_types[0]),
1753-
pretty_ty(rust_ret_type),
1754-
pretty_ty(ret_type_subtype),
1755+
self.pretty_ty(vec_subtype),
1756+
self.pretty_ty(rust_arg_types[0]),
1757+
self.pretty_ty(rust_ret_type),
1758+
self.pretty_ty(ret_type_subtype),
17551759
);
17561760
utils::span_err(self.tcx, span, err_msg);
17571761
}

‎kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

+5-4
Original file line numberDiff line numberDiff line change
@@ -260,7 +260,7 @@ impl<'tcx> GotocCtx<'tcx> {
260260
Ok(parent_expr.member(Self::tuple_fld_name(field_idx), &self.symbol_table))
261261
}
262262
TyKind::RigidTy(RigidTy::Adt(def, _))
263-
if rustc_internal::internal(def).repr().simd() =>
263+
if rustc_internal::internal(self.tcx, def).repr().simd() =>
264264
{
265265
Ok(self.codegen_simd_field(
266266
parent_expr,
@@ -415,7 +415,7 @@ impl<'tcx> GotocCtx<'tcx> {
415415
};
416416

417417
let inner_mir_typ_internal =
418-
std_pointee_type(rustc_internal::internal(base_type)).unwrap();
418+
std_pointee_type(rustc_internal::internal(self.tcx, base_type)).unwrap();
419419
let inner_mir_typ = rustc_internal::stable(inner_mir_typ_internal);
420420
let (fat_ptr_mir_typ, fat_ptr_goto_expr) = if self
421421
.use_thin_pointer(inner_mir_typ_internal)
@@ -436,6 +436,7 @@ impl<'tcx> GotocCtx<'tcx> {
436436
);
437437
assert!(
438438
self.use_fat_pointer(rustc_internal::internal(
439+
self.tcx,
439440
pointee_type(fat_ptr_mir_typ.unwrap()).unwrap()
440441
)),
441442
"Unexpected type: {:?} -- {:?}",
@@ -582,7 +583,7 @@ impl<'tcx> GotocCtx<'tcx> {
582583
(variant.name().into(), TypeOrVariant::Variant(variant))
583584
}
584585
TyKind::RigidTy(RigidTy::Coroutine(..)) => {
585-
let idx_internal = rustc_internal::internal(idx);
586+
let idx_internal = rustc_internal::internal(self.tcx, idx);
586587
(
587588
self.coroutine_variant_name(idx_internal),
588589
TypeOrVariant::CoroutineVariant(*idx),
@@ -593,7 +594,7 @@ impl<'tcx> GotocCtx<'tcx> {
593594
&ty.kind()
594595
),
595596
};
596-
let layout = self.layout_of(rustc_internal::internal(ty));
597+
let layout = self.layout_of(rustc_internal::internal(self.tcx, ty));
597598
let expr = match &layout.variants {
598599
Variants::Single { .. } => before.goto_expr,
599600
Variants::Multiple { tag_encoding, .. } => match tag_encoding {

‎kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

+10-7
Original file line numberDiff line numberDiff line change
@@ -555,7 +555,7 @@ impl<'tcx> GotocCtx<'tcx> {
555555
let layout = self.layout_of_stable(res_ty);
556556
let fields = match &layout.variants {
557557
Variants::Single { index } => {
558-
if *index != rustc_internal::internal(variant_index) {
558+
if *index != rustc_internal::internal(self.tcx, variant_index) {
559559
// This may occur if all variants except for the one pointed by
560560
// index can never be constructed. Generic code might still try
561561
// to initialize the non-existing invariant.
@@ -565,7 +565,7 @@ impl<'tcx> GotocCtx<'tcx> {
565565
&layout.fields
566566
}
567567
Variants::Multiple { variants, .. } => {
568-
&variants[rustc_internal::internal(variant_index)].fields
568+
&variants[rustc_internal::internal(self.tcx, variant_index)].fields
569569
}
570570
};
571571

@@ -716,7 +716,10 @@ impl<'tcx> GotocCtx<'tcx> {
716716
.offset_of_subfield(
717717
self,
718718
fields.iter().map(|(var_idx, field_idx)| {
719-
(rustc_internal::internal(var_idx), (*field_idx).into())
719+
(
720+
rustc_internal::internal(self.tcx, var_idx),
721+
(*field_idx).into(),
722+
)
720723
}),
721724
)
722725
.bytes(),
@@ -1180,7 +1183,7 @@ impl<'tcx> GotocCtx<'tcx> {
11801183
if self.vtable_ctx.emit_vtable_restrictions {
11811184
// Add to the possible method names for this trait type
11821185
self.vtable_ctx.add_possible_method(
1183-
self.normalized_trait_name(rustc_internal::internal(ty)).into(),
1186+
self.normalized_trait_name(rustc_internal::internal(self.tcx, ty)).into(),
11841187
idx,
11851188
fn_name.into(),
11861189
);
@@ -1205,7 +1208,7 @@ impl<'tcx> GotocCtx<'tcx> {
12051208

12061209
/// Generate a function pointer to drop_in_place for entry into the vtable
12071210
fn codegen_vtable_drop_in_place(&mut self, ty: Ty, trait_ty: Ty) -> Expr {
1208-
let trait_ty = rustc_internal::internal(trait_ty);
1211+
let trait_ty = rustc_internal::internal(self.tcx, trait_ty);
12091212
let drop_instance = Instance::resolve_drop_in_place(ty);
12101213
let drop_sym_name: InternedString = drop_instance.mangled_name().into();
12111214

@@ -1296,7 +1299,7 @@ impl<'tcx> GotocCtx<'tcx> {
12961299
_ => unreachable!("Cannot codegen_vtable for type {:?}", dst_mir_type.kind()),
12971300
};
12981301

1299-
let src_name = self.ty_mangled_name(rustc_internal::internal(src_mir_type));
1302+
let src_name = self.ty_mangled_name(rustc_internal::internal(self.tcx, src_mir_type));
13001303
// The name needs to be the same as inserted in typ.rs
13011304
let vtable_name = self.vtable_name_stable(trait_type).intern();
13021305
let vtable_impl_name = format!("{vtable_name}_impl_for_{src_name}");
@@ -1310,7 +1313,7 @@ impl<'tcx> GotocCtx<'tcx> {
13101313
// Build the vtable, using Rust's vtable_entries to determine field order
13111314
let vtable_entries = if let Some(principal) = trait_type.kind().trait_principal() {
13121315
let trait_ref_binder = principal.with_self_ty(src_mir_type);
1313-
ctx.tcx.vtable_entries(rustc_internal::internal(trait_ref_binder))
1316+
ctx.tcx.vtable_entries(rustc_internal::internal(ctx.tcx, trait_ref_binder))
13141317
} else {
13151318
TyCtxt::COMMON_VTABLE_ENTRIES
13161319
};

‎kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ impl<'tcx> GotocCtx<'tcx> {
3131
}
3232

3333
pub fn codegen_caller_span_stable(&self, sp: SpanStable) -> Location {
34-
self.codegen_caller_span(&rustc_internal::internal(sp))
34+
self.codegen_caller_span(&rustc_internal::internal(self.tcx, sp))
3535
}
3636

3737
/// Get the location of the caller. This will attempt to reach the macro caller.

‎kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

+4-4
Original file line numberDiff line numberDiff line change
@@ -220,8 +220,8 @@ impl<'tcx> GotocCtx<'tcx> {
220220
location: Location,
221221
) -> Stmt {
222222
// this requires place points to an enum type.
223-
let dest_ty_internal = rustc_internal::internal(dest_ty);
224-
let variant_index_internal = rustc_internal::internal(variant_index);
223+
let dest_ty_internal = rustc_internal::internal(self.tcx, dest_ty);
224+
let variant_index_internal = rustc_internal::internal(self.tcx, variant_index);
225225
let layout = self.layout_of(dest_ty_internal);
226226
match &layout.variants {
227227
Variants::Single { .. } => Stmt::skip(location),
@@ -533,7 +533,7 @@ impl<'tcx> GotocCtx<'tcx> {
533533
let instance = Instance::resolve(def, &subst).unwrap();
534534

535535
// TODO(celina): Move this check to be inside codegen_funcall_args.
536-
if self.ty_needs_untupled_args(rustc_internal::internal(funct)) {
536+
if self.ty_needs_untupled_args(rustc_internal::internal(self.tcx, funct)) {
537537
self.codegen_untupled_args(instance, &mut fargs, args.last());
538538
}
539539

@@ -595,7 +595,7 @@ impl<'tcx> GotocCtx<'tcx> {
595595
fn extract_ptr(&self, arg_expr: Expr, arg_ty: Ty) -> Expr {
596596
// Generate an expression that indexes the pointer.
597597
let expr = self
598-
.receiver_data_path(rustc_internal::internal(arg_ty))
598+
.receiver_data_path(rustc_internal::internal(self.tcx, arg_ty))
599599
.fold(arg_expr, |curr_expr, (name, _)| curr_expr.member(name, &self.symbol_table));
600600

601601
trace!(?arg_ty, gotoc_ty=?expr.typ(), gotoc_expr=?expr.value(), "extract_ptr");

0 commit comments

Comments
 (0)