Skip to content

Commit

Permalink
Update calls to internal to pass TyCtxt
Browse files Browse the repository at this point in the history 
  - This is due to the safety fix to the internal function, which was
    done here: rust-lang/rust#120128
  • Loading branch information
@celinval
celinval committed Jan 24, 2024
1 parent fd12a28 commit d8936d6
Show file tree
Hide file tree
Showing 16 changed files with 123 additions and 105 deletions.
7 changes: 4 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ impl<'tcx> GotocCtx<'tcx> {
/// handled later.
pub fn codegen_foreign_fn(&mut self, instance: Instance) -> &Symbol {
debug!(?instance, "codegen_foreign_function");
let instance_internal = rustc_internal::internal(instance);
let instance_internal = rustc_internal::internal(self.tcx, instance);
let fn_name = self.symbol_name_stable(instance).intern();
if self.symbol_table.contains(fn_name) {
// Symbol has been added (either a built-in CBMC function or a Rust allocation function).
Expand Down Expand Up @@ -102,7 +102,7 @@ impl<'tcx> GotocCtx<'tcx> {
/// Generate type for the given foreign instance.
fn codegen_ffi_type(&mut self, instance: Instance) -> Type {
let fn_name = self.symbol_name_stable(instance);
let fn_abi = kani_middle::fn_abi(self.tcx, rustc_internal::internal(instance));
let fn_abi = kani_middle::fn_abi(self.tcx, rustc_internal::internal(self.tcx, instance));
let loc = self.codegen_span_stable(instance.def.span());
let params = fn_abi
.args
Expand Down Expand Up @@ -140,7 +140,8 @@ impl<'tcx> GotocCtx<'tcx> {
let entry = self.unsupported_constructs.entry("foreign function".into()).or_default();
entry.push(loc);

let call_conv = kani_middle::fn_abi(self.tcx, rustc_internal::internal(instance)).conv;
let call_conv =
kani_middle::fn_abi(self.tcx, rustc_internal::internal(self.tcx, instance)).conv;
let msg = format!("call to foreign \"{call_conv:?}\" function `{fn_name}`");
let url = if call_conv == Conv::C {
"https://github.com/model-checking/kani/issues/2423"
Expand Down
50 changes: 27 additions & 23 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
//! this module handles intrinsics
use super::typ;
use super::{bb_label, PropertyClass};
use crate::codegen_cprover_gotoc::codegen::ty_stable::{pointee_type_stable, pretty_ty};
use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
use crate::codegen_cprover_gotoc::{utils, GotocCtx};
use crate::unwrap_or_return_codegen_unimplemented_stmt;
use cbmc::goto_program::{
Expand Down Expand Up @@ -646,7 +646,7 @@ impl<'tcx> GotocCtx<'tcx> {
span,
format!(
"Type check failed for intrinsic `{name}`: Expected {expected}, found {}",
pretty_ty(actual)
self.pretty_ty(actual)
),
);
self.tcx.dcx().abort_if_errors();
Expand Down Expand Up @@ -779,12 +779,16 @@ impl<'tcx> GotocCtx<'tcx> {
if layout.abi.is_uninhabited() {
return self.codegen_fatal_error(
PropertyClass::SafetyCheck,
&format!("attempted to instantiate uninhabited type `{}`", pretty_ty(*target_ty)),
&format!(
"attempted to instantiate uninhabited type `{}`",
self.pretty_ty(*target_ty)
),
span,
);
}

let param_env_and_type = ParamEnv::reveal_all().and(rustc_internal::internal(target_ty));
let param_env_and_type =
ParamEnv::reveal_all().and(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
Expand All @@ -798,7 +802,7 @@ impl<'tcx> GotocCtx<'tcx> {
PropertyClass::SafetyCheck,
&format!(
"attempted to zero-initialize type `{}`, which is invalid",
pretty_ty(*target_ty)
self.pretty_ty(*target_ty)
),
span,
);
Expand All @@ -817,7 +821,7 @@ impl<'tcx> GotocCtx<'tcx> {
PropertyClass::SafetyCheck,
&format!(
"attempted to leave type `{}` uninitialized, which is invalid",
pretty_ty(*target_ty)
self.pretty_ty(*target_ty)
),
span,
);
Expand Down Expand Up @@ -1285,7 +1289,7 @@ impl<'tcx> GotocCtx<'tcx> {
_ => {
let err_msg = format!(
"simd_shuffle index must be an array of `u32`, got `{}`",
pretty_ty(farg_types[2])
self.pretty_ty(farg_types[2])
);
utils::span_err(self.tcx, span, err_msg);
// Return a dummy value
Expand Down Expand Up @@ -1378,7 +1382,7 @@ impl<'tcx> GotocCtx<'tcx> {

// Packed types ignore the alignment of their fields.
if let TyKind::RigidTy(RigidTy::Adt(def, _)) = ty.kind() {
if rustc_internal::internal(def).repr().packed() {
if rustc_internal::internal(self.tcx, def).repr().packed() {
unsized_align = sized_align.clone();
}
}
Expand Down Expand Up @@ -1426,9 +1430,9 @@ impl<'tcx> GotocCtx<'tcx> {
if rust_ret_type != vector_base_type {
let err_msg = format!(
"expected return type `{}` (element of input `{}`), found `{}`",
pretty_ty(vector_base_type),
pretty_ty(rust_arg_types[0]),
pretty_ty(rust_ret_type)
self.pretty_ty(vector_base_type),
self.pretty_ty(rust_arg_types[0]),
self.pretty_ty(rust_ret_type)
);
utils::span_err(self.tcx, span, err_msg);
}
Expand Down Expand Up @@ -1466,9 +1470,9 @@ impl<'tcx> GotocCtx<'tcx> {
if vector_base_type != rust_arg_types[2] {
let err_msg = format!(
"expected inserted type `{}` (element of input `{}`), found `{}`",
pretty_ty(vector_base_type),
pretty_ty(rust_arg_types[0]),
pretty_ty(rust_arg_types[2]),
self.pretty_ty(vector_base_type),
self.pretty_ty(rust_arg_types[0]),
self.pretty_ty(rust_arg_types[2]),
);
utils::span_err(self.tcx, span, err_msg);
}
Expand Down Expand Up @@ -1534,8 +1538,8 @@ impl<'tcx> GotocCtx<'tcx> {
"expected return type with length {} (same as input type `{}`), \
found `{}` with length {}",
arg1.typ().len().unwrap(),
pretty_ty(rust_arg_types[0]),
pretty_ty(rust_ret_type),
self.pretty_ty(rust_arg_types[0]),
self.pretty_ty(rust_ret_type),
ret_typ.len().unwrap()
);
utils::span_err(self.tcx, span, err_msg);
Expand All @@ -1545,8 +1549,8 @@ impl<'tcx> GotocCtx<'tcx> {
let (_, rust_base_type) = self.simd_size_and_type(rust_ret_type);
let err_msg = format!(
"expected return type with integer elements, found `{}` with non-integer `{}`",
pretty_ty(rust_ret_type),
pretty_ty(rust_base_type),
self.pretty_ty(rust_ret_type),
self.pretty_ty(rust_base_type),
);
utils::span_err(self.tcx, span, err_msg);
}
Expand Down Expand Up @@ -1740,18 +1744,18 @@ impl<'tcx> GotocCtx<'tcx> {
if ret_type_len != n {
let err_msg = format!(
"expected return type of length {n}, found `{}` with length {ret_type_len}",
pretty_ty(rust_ret_type),
self.pretty_ty(rust_ret_type),
);
utils::span_err(self.tcx, span, err_msg);
}
if vec_subtype != ret_type_subtype {
let err_msg = format!(
"expected return element type `{}` (element of input `{}`), \
found `{}` with element type `{}`",
pretty_ty(vec_subtype),
pretty_ty(rust_arg_types[0]),
pretty_ty(rust_ret_type),
pretty_ty(ret_type_subtype),
self.pretty_ty(vec_subtype),
self.pretty_ty(rust_arg_types[0]),
self.pretty_ty(rust_ret_type),
self.pretty_ty(ret_type_subtype),
);
utils::span_err(self.tcx, span, err_msg);
}
Expand Down
9 changes: 5 additions & 4 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -260,7 +260,7 @@ impl<'tcx> GotocCtx<'tcx> {
Ok(parent_expr.member(Self::tuple_fld_name(field_idx), &self.symbol_table))
}
TyKind::RigidTy(RigidTy::Adt(def, _))
if rustc_internal::internal(def).repr().simd() =>
if rustc_internal::internal(self.tcx, def).repr().simd() =>
{
Ok(self.codegen_simd_field(
parent_expr,
Expand Down Expand Up @@ -415,7 +415,7 @@ impl<'tcx> GotocCtx<'tcx> {
};

let inner_mir_typ_internal =
std_pointee_type(rustc_internal::internal(base_type)).unwrap();
std_pointee_type(rustc_internal::internal(self.tcx, base_type)).unwrap();
let inner_mir_typ = rustc_internal::stable(inner_mir_typ_internal);
let (fat_ptr_mir_typ, fat_ptr_goto_expr) = if self
.use_thin_pointer(inner_mir_typ_internal)
Expand All @@ -436,6 +436,7 @@ impl<'tcx> GotocCtx<'tcx> {
);
assert!(
self.use_fat_pointer(rustc_internal::internal(
self.tcx,
pointee_type(fat_ptr_mir_typ.unwrap()).unwrap()
)),
"Unexpected type: {:?} -- {:?}",
Expand Down Expand Up @@ -582,7 +583,7 @@ impl<'tcx> GotocCtx<'tcx> {
(variant.name().into(), TypeOrVariant::Variant(variant))
}
TyKind::RigidTy(RigidTy::Coroutine(..)) => {
let idx_internal = rustc_internal::internal(idx);
let idx_internal = rustc_internal::internal(self.tcx, idx);
(
self.coroutine_variant_name(idx_internal),
TypeOrVariant::CoroutineVariant(*idx),
Expand All @@ -593,7 +594,7 @@ impl<'tcx> GotocCtx<'tcx> {
&ty.kind()
),
};
let layout = self.layout_of(rustc_internal::internal(ty));
let layout = self.layout_of(rustc_internal::internal(self.tcx, ty));
let expr = match &layout.variants {
Variants::Single { .. } => before.goto_expr,
Variants::Multiple { tag_encoding, .. } => match tag_encoding {
Expand Down
17 changes: 10 additions & 7 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -555,7 +555,7 @@ impl<'tcx> GotocCtx<'tcx> {
let layout = self.layout_of_stable(res_ty);
let fields = match &layout.variants {
Variants::Single { index } => {
if *index != rustc_internal::internal(variant_index) {
if *index != rustc_internal::internal(self.tcx, variant_index) {
// This may occur if all variants except for the one pointed by
// index can never be constructed. Generic code might still try
// to initialize the non-existing invariant.
Expand All @@ -565,7 +565,7 @@ impl<'tcx> GotocCtx<'tcx> {
&layout.fields
}
Variants::Multiple { variants, .. } => {
&variants[rustc_internal::internal(variant_index)].fields
&variants[rustc_internal::internal(self.tcx, variant_index)].fields
}
};

Expand Down Expand Up @@ -716,7 +716,10 @@ impl<'tcx> GotocCtx<'tcx> {
.offset_of_subfield(
self,
fields.iter().map(|(var_idx, field_idx)| {
(rustc_internal::internal(var_idx), (*field_idx).into())
(
rustc_internal::internal(self.tcx, var_idx),
(*field_idx).into(),
)
}),
)
.bytes(),
Expand Down Expand Up @@ -1180,7 +1183,7 @@ impl<'tcx> GotocCtx<'tcx> {
if self.vtable_ctx.emit_vtable_restrictions {
// Add to the possible method names for this trait type
self.vtable_ctx.add_possible_method(
self.normalized_trait_name(rustc_internal::internal(ty)).into(),
self.normalized_trait_name(rustc_internal::internal(self.tcx, ty)).into(),
idx,
fn_name.into(),
);
Expand All @@ -1205,7 +1208,7 @@ impl<'tcx> GotocCtx<'tcx> {

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

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

let src_name = self.ty_mangled_name(rustc_internal::internal(src_mir_type));
let src_name = self.ty_mangled_name(rustc_internal::internal(self.tcx, src_mir_type));
// The name needs to be the same as inserted in typ.rs
let vtable_name = self.vtable_name_stable(trait_type).intern();
let vtable_impl_name = format!("{vtable_name}_impl_for_{src_name}");
Expand All @@ -1310,7 +1313,7 @@ impl<'tcx> GotocCtx<'tcx> {
// Build the vtable, using Rust's vtable_entries to determine field order
let vtable_entries = if let Some(principal) = trait_type.kind().trait_principal() {
let trait_ref_binder = principal.with_self_ty(src_mir_type);
ctx.tcx.vtable_entries(rustc_internal::internal(trait_ref_binder))
ctx.tcx.vtable_entries(rustc_internal::internal(ctx.tcx, trait_ref_binder))
} else {
TyCtxt::COMMON_VTABLE_ENTRIES
};
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ impl<'tcx> GotocCtx<'tcx> {
}

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

/// Get the location of the caller. This will attempt to reach the macro caller.
Expand Down
8 changes: 4 additions & 4 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -219,8 +219,8 @@ impl<'tcx> GotocCtx<'tcx> {
location: Location,
) -> Stmt {
// this requires place points to an enum type.
let dest_ty_internal = rustc_internal::internal(dest_ty);
let variant_index_internal = rustc_internal::internal(variant_index);
let dest_ty_internal = rustc_internal::internal(self.tcx, dest_ty);
let variant_index_internal = rustc_internal::internal(self.tcx, variant_index);
let layout = self.layout_of(dest_ty_internal);
match &layout.variants {
Variants::Single { .. } => Stmt::skip(location),
Expand Down Expand Up @@ -532,7 +532,7 @@ impl<'tcx> GotocCtx<'tcx> {
let instance = Instance::resolve(def, &subst).unwrap();

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

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

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

0 comments on commit d8936d6

Please sign in to comment.