1
Fork 0

Rollup merge of #123176 - celinval:smir-field-ty, r=oli-obk

Normalize the result of `Fields::ty_with_args`

We were only instantiating before, which would leak an AliasTy. I added a test case that reproduce the issue seen here:

https://github.com/model-checking/kani/issues/3113

r? ``@oli-obk``
This commit is contained in:
Matthias Krüger 2024-03-29 15:17:10 +01:00 committed by GitHub
commit 73a4208638
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 101 additions and 3 deletions

View file

@ -420,7 +420,10 @@ impl<'tcx> Context for TablesWrapper<'tcx> {
let tcx = tables.tcx;
let args = args.internal(&mut *tables, tcx);
let def_ty = tables.tcx.type_of(item.internal(&mut *tables, tcx));
def_ty.instantiate(tables.tcx, args).stable(&mut *tables)
tables
.tcx
.instantiate_and_normalize_erasing_regions(args, ty::ParamEnv::reveal_all(), def_ty)
.stable(&mut *tables)
}
fn const_pretty(&self, cnst: &stable_mir::ty::Const) -> String {

View file

@ -654,7 +654,7 @@ impl AdtDef {
with(|cx| cx.def_ty(self.0))
}
/// Retrieve the type of this Adt instantiating the type with the given arguments.
/// Retrieve the type of this Adt by instantiating and normalizing it with the given arguments.
///
/// This will assume the type can be instantiated with these arguments.
pub fn ty_with_args(&self, args: &GenericArgs) -> Ty {
@ -733,7 +733,7 @@ pub struct FieldDef {
}
impl FieldDef {
/// Retrieve the type of this field instantiating the type with the given arguments.
/// Retrieve the type of this field instantiating and normalizing it with the given arguments.
///
/// This will assume the type can be instantiated with these arguments.
pub fn ty_with_args(&self, args: &GenericArgs) -> Ty {