Skip to content

Commit d8936d6

Browse files
celinvalcelinval
committed
Update calls to internal to pass TyCtxt
 - This is due to the safety fix to the internal function, which was done here: rust-lang/rust#120128
1 parent fd12a28 commit d8936d6

16 files changed

Lines changed: 123 additions & 105 deletions

File tree

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

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ impl<'tcx> GotocCtx<'tcx> {
4848
/// handled later.
4949
pub fn codegen_foreign_fn(&mut self, instance: Instance) -> &Symbol {
5050
debug!(?instance, "codegen_foreign_function");
51-
let instance_internal = rustc_internal::internal(instance);
51+
let instance_internal = rustc_internal::internal(self.tcx, instance);
5252
let fn_name = self.symbol_name_stable(instance).intern();
5353
if self.symbol_table.contains(fn_name) {
5454
// Symbol has been added (either a built-in CBMC function or a Rust allocation function).
@@ -102,7 +102,7 @@ impl<'tcx> GotocCtx<'tcx> {
102102
/// Generate type for the given foreign instance.
103103
fn codegen_ffi_type(&mut self, instance: Instance) -> Type {
104104
let fn_name = self.symbol_name_stable(instance);
105-
let fn_abi = kani_middle::fn_abi(self.tcx, rustc_internal::internal(instance));
105+
let fn_abi = kani_middle::fn_abi(self.tcx, rustc_internal::internal(self.tcx, instance));
106106
let loc = self.codegen_span_stable(instance.def.span());
107107
let params = fn_abi
108108
.args
@@ -140,7 +140,8 @@ impl<'tcx> GotocCtx<'tcx> {
140140
let entry = self.unsupported_constructs.entry("foreign function".into()).or_default();
141141
entry.push(loc);
142142

143-
let call_conv = kani_middle::fn_abi(self.tcx, rustc_internal::internal(instance)).conv;
143+
let call_conv =
144+
kani_middle::fn_abi(self.tcx, rustc_internal::internal(self.tcx, instance)).conv;
144145
let msg = format!("call to foreign \"{call_conv:?}\" function `{fn_name}`");
145146
let url = if call_conv == Conv::C {
146147
"https://github.com/model-checking/kani/issues/2423"

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

Lines changed: 27 additions & 23 deletions
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‎

Lines changed: 5 additions & 4 deletions
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‎

Lines changed: 10 additions & 7 deletions
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‎

Lines changed: 1 addition & 1 deletion
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‎

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

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

@@ -587,7 +587,7 @@ impl<'tcx> GotocCtx<'tcx> {
587587
fn extract_ptr(&self, arg_expr: Expr, arg_ty: Ty) -> Expr {
588588
// Generate an expression that indexes the pointer.
589589
let expr = self
590-
.receiver_data_path(rustc_internal::internal(arg_ty))
590+
.receiver_data_path(rustc_internal::internal(self.tcx, arg_ty))
591591
.fold(arg_expr, |curr_expr, (name, _)| curr_expr.member(name, &self.symbol_table));
592592

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

0 commit comments

Comments
 (0)