Skip to content

Commit a216542

Browse files
committed
Remove pretty_ty and use rustc_public's formatter instead
rust-lang/rust#118364 (or, really, its successor) has been merged over a year ago. We can now directly use the formatter.
1 parent 587bd03 commit a216542

File tree

2 files changed

+16
-42
lines changed

2 files changed

+16
-42
lines changed

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

Lines changed: 16 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -563,8 +563,7 @@ impl GotocCtx<'_> {
563563
self.tcx,
564564
span,
565565
format!(
566-
"Type check failed for intrinsic `{name}`: Expected {expected}, found {}",
567-
self.pretty_ty(actual)
566+
"Type check failed for intrinsic `{name}`: Expected {expected}, found {actual}"
568567
),
569568
);
570569
self.tcx.dcx().abort_if_errors();
@@ -715,10 +714,7 @@ impl GotocCtx<'_> {
715714
if layout.is_uninhabited() {
716715
return self.codegen_fatal_error(
717716
PropertyClass::SafetyCheck,
718-
&format!(
719-
"attempted to instantiate uninhabited type `{}`",
720-
self.pretty_ty(*target_ty)
721-
),
717+
&format!("attempted to instantiate uninhabited type `{}`", *target_ty),
722718
span,
723719
);
724720
}
@@ -736,10 +732,7 @@ impl GotocCtx<'_> {
736732
{
737733
return self.codegen_fatal_error(
738734
PropertyClass::SafetyCheck,
739-
&format!(
740-
"attempted to zero-initialize type `{}`, which is invalid",
741-
self.pretty_ty(*target_ty)
742-
),
735+
&format!("attempted to zero-initialize type `{}`, which is invalid", *target_ty),
743736
span,
744737
);
745738
}
@@ -757,7 +750,7 @@ impl GotocCtx<'_> {
757750
PropertyClass::SafetyCheck,
758751
&format!(
759752
"attempted to leave type `{}` uninitialized, which is invalid",
760-
self.pretty_ty(*target_ty)
753+
*target_ty
761754
),
762755
span,
763756
);
@@ -1142,7 +1135,7 @@ impl GotocCtx<'_> {
11421135
} else {
11431136
let err_msg = format!(
11441137
"simd_shuffle index must be a SIMD vector of `u32`, got `{}`",
1145-
self.pretty_ty(farg_types[2])
1138+
farg_types[2]
11461139
);
11471140
utils::span_err(self.tcx, span, err_msg);
11481141
// Return a dummy value
@@ -1281,10 +1274,8 @@ impl GotocCtx<'_> {
12811274
let (_, vector_base_type) = self.simd_size_and_type(rust_arg_types[0]);
12821275
if rust_ret_type != vector_base_type {
12831276
let err_msg = format!(
1284-
"expected return type `{}` (element of input `{}`), found `{}`",
1285-
self.pretty_ty(vector_base_type),
1286-
self.pretty_ty(rust_arg_types[0]),
1287-
self.pretty_ty(rust_ret_type)
1277+
"expected return type `{vector_base_type}` (element of input `{}`), found `{rust_ret_type}`",
1278+
rust_arg_types[0]
12881279
);
12891280
utils::span_err(self.tcx, span, err_msg);
12901281
}
@@ -1322,10 +1313,8 @@ impl GotocCtx<'_> {
13221313
let (_, vector_base_type) = self.simd_size_and_type(rust_arg_types[0]);
13231314
if vector_base_type != rust_arg_types[2] {
13241315
let err_msg = format!(
1325-
"expected inserted type `{}` (element of input `{}`), found `{}`",
1326-
self.pretty_ty(vector_base_type),
1327-
self.pretty_ty(rust_arg_types[0]),
1328-
self.pretty_ty(rust_arg_types[2]),
1316+
"expected inserted type `{vector_base_type}` (element of input `{}`), found `{}`",
1317+
rust_arg_types[0], rust_arg_types[2],
13291318
);
13301319
utils::span_err(self.tcx, span, err_msg);
13311320
}
@@ -1389,10 +1378,9 @@ impl GotocCtx<'_> {
13891378
if arg1.typ().len().unwrap() != ret_typ.len().unwrap() {
13901379
let err_msg = format!(
13911380
"expected return type with length {} (same as input type `{}`), \
1392-
found `{}` with length {}",
1381+
found `{rust_ret_type}` with length {}",
13931382
arg1.typ().len().unwrap(),
1394-
self.pretty_ty(rust_arg_types[0]),
1395-
self.pretty_ty(rust_ret_type),
1383+
rust_arg_types[0],
13961384
ret_typ.len().unwrap()
13971385
);
13981386
utils::span_err(self.tcx, span, err_msg);
@@ -1401,9 +1389,7 @@ impl GotocCtx<'_> {
14011389
if !ret_typ.base_type().unwrap().is_integer() {
14021390
let (_, rust_base_type) = self.simd_size_and_type(rust_ret_type);
14031391
let err_msg = format!(
1404-
"expected return type with integer elements, found `{}` with non-integer `{}`",
1405-
self.pretty_ty(rust_ret_type),
1406-
self.pretty_ty(rust_base_type),
1392+
"expected return type with integer elements, found `{rust_ret_type}` with non-integer `{rust_base_type}`"
14071393
);
14081394
utils::span_err(self.tcx, span, err_msg);
14091395
}
@@ -1591,19 +1577,15 @@ impl GotocCtx<'_> {
15911577
let (ret_type_len, ret_type_subtype) = self.simd_size_and_type(rust_ret_type);
15921578
if ret_type_len != n {
15931579
let err_msg = format!(
1594-
"expected return type of length {n}, found `{}` with length {ret_type_len}",
1595-
self.pretty_ty(rust_ret_type),
1580+
"expected return type of length {n}, found `{rust_ret_type}` with length {ret_type_len}"
15961581
);
15971582
utils::span_err(self.tcx, span, err_msg);
15981583
}
15991584
if vec_subtype != ret_type_subtype {
16001585
let err_msg = format!(
1601-
"expected return element type `{}` (element of input `{}`), \
1602-
found `{}` with element type `{}`",
1603-
self.pretty_ty(vec_subtype),
1604-
self.pretty_ty(rust_arg_types[0]),
1605-
self.pretty_ty(rust_ret_type),
1606-
self.pretty_ty(ret_type_subtype),
1586+
"expected return element type `{vec_subtype}` (element of input `{}`), \
1587+
found `{rust_ret_type}` with element type `{ret_type_subtype}`",
1588+
rust_arg_types[0]
16071589
);
16081590
utils::span_err(self.tcx, span, err_msg);
16091591
}

kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -109,14 +109,6 @@ impl<'tcx> GotocCtx<'tcx> {
109109
}
110110
}
111111

112-
/// Convert a type into a user readable type representation.
113-
///
114-
/// This should be replaced by StableMIR `pretty_ty()` after
115-
/// <https://github.com/rust-lang/rust/pull/118364> is merged.
116-
pub fn pretty_ty(&self, ty: Ty) -> String {
117-
ty.to_string()
118-
}
119-
120112
pub fn requires_caller_location(&self, instance: Instance) -> bool {
121113
let instance_internal = rustc_internal::internal(self.tcx, instance);
122114
instance_internal.def.requires_caller_location(self.tcx)

0 commit comments

Comments
 (0)