Distinguish VTable unsizes, add metadata

[N1ark]

Based on AeneasVerif/hax#6

Rename UnsizingMetadata::VTablePtr -> VTableDirect, and add to it an optional GlobalDeclRef for the associated VTable. Note I don't do anything about the global's generics right now, which I believe is wrong. There are also cases where the global is not known because the impl atom isn't ImplExprAtom::Concrete; I have no idea how to fix this, maybe @ssyram knows, but for now it's already better than nothing :)

Add UnsizingMetadata::VTableNested, for dyn-dyn unsizes. It also carries a TraitRef, along with an optional FieldId, for the field in the current VTable that contains the sub-vtable to unsize to. Note here that the field id is optional, in the case of no-op unsizes (e.g. dyn T + 'static -> dyn T).

I believe we should distinguish these two cases, since fundamentally they operate differently: the former "creates" metadata from a statically known VTable address, the latter fetches a VTable dynamically, from the current VTable in the metadata.

To obtain the FieldId in VTableNested I had to slightly reorganise the way fields are added to the vtable structure (commit 07a71ed)

(disregard the branch name, this is a first step towards mono dyn but I didn't get there)

[Nadrieril]

There are also cases where the global is not known because the impl atom isn't ImplExprAtom::Concrete

The only general fix is a ConstantExprKind::VTable(TraitRef). I'd prefer that over storing the GlobalDeclRef in fact, and I'd expect us to add a normalizing function for these that does compute the GlobalDeclRef. We're in fact starting to have a lot of normalization functions, which will eventually have to be pulled out into their own module.

[Nadrieril]

This is looking more and more like UnsizingMetadata is a defunctionalization x) What I'd actually want instead of ptr := unsize(ptr, UnsizingMetadata::VTableNested("field1")) is ptr := ptr with metadata (copy ptr.metadata.field1). I'm not saying you have to do that in this PR though, and we should be careful not to introduce a reborrow that wasn't there.

[Nadrieril]

Also the TraitRef is basically useless once we have the GlobalDeclRef, so I propose we add ConstantExprKind::Vtable and change VTableDirect to take only a ConstantExpr.

[Nadrieril]

Ah, something else that can happen: dyn Trait -> dyn Sized, despite the fact that Sized is not a supertrait of Trait. We might need to store a vtable pointer to dyn Sized in every vtable.

[Nadrieril]

I decided to ignore that for now and just keep the same vtable.

[Nadrieril]

You should be able to get the right generics using translate_item instead of register_item.

[Nadrieril]

nit: calling this unsizing feels wrong because we're not going from sized to unsized. I'd prefer dyn-cast-to-supertrait.rs

[Nadrieril]

You'll notice that even if we return ConstantExprKind::VTable in this branch, we can't register the vtable instance since we don't know the impl. That's a fundamental incompleteness in the choice I made to translate vtable instances lazily: it won't work for:

fn foo<T: Trait>(x: &T) -> &dyn Trait { x }
fn main() {
    let _ = foo::<SomeType>(...);
}

You might want a --always-translate-vtable-instances for your purposes. Or maybe we should do a static analysis at the end of translation to register all the ones that might be used indirectly like that 🤔. Or maybe if we see any dyn Trait anywhere then we just register all the vtable instances for that trait, kinda like how we deal with lazily translating methods. Yeah that's saner.

[ssyram]

Thanks for this PR! But I also totally agree with @Nadrieril that we in fact cannot always have that explicit field of GlobalRef, except monomorphised codes... Especially with:

fn to_dyn<T : Trait>(t : &T) -> &dyn Trait { t }

[N1ark]

Thanks for this PR! But I also totally agree with @Nadrieril that we in fact cannot always have that explicit field of GlobalRef, except monomorphised codes... Especially with:

fn to_dyn<T : Trait>(t : &T) -> &dyn Trait { t }

This is not a VTableNested unsize, since it's a non-dyn to dyn unsize. In all possible dyn-dyn unsizes I believe you always necessarily know what the field is? Regardless I'm not sure how a client is expected to perform the unsize without having the field

I understand that in both cases there is a possibility we can't get the GlobalDeclRef/FieldIdx, but I would really much rather still have the information there, optionally. In monomorphic code that information is necessarily always known, and it is much easier to use that than to somehow always recompute the right global/field anytime an unsize is reached. If you prefer, I'm happy to rename these MonoVTableNested/MonoVTableDirect, but I strongly believe that information must go through. I have no idea how my tool is supposed to handle &dyn otherwise.

[ssyram]

I'm not sure how a client is expected to perform the unsize without having the field

If I'm understanding it correctly, this is always a problem as it is somehow conceptually impossible to know the field. And I think we have reached a consensus here.

As for the explicit GlobalRef field, what I'm not that understanding is that I think for those possible, we already have the Concrete things, with which we easily compute the required GlobalRef. If it is not possible, then it should also be None in your case? So I guess what you need is something like the normalisation that computes the Concrete trait-ref, when possible? In all, I think the current mechanism already provides somehow precise description of the dyn object casting?

BTW, in Eurydice now, we are now actually getting the GlobalRef from the trait-ref for Concrete, and it works fine at least for our current application for generic codes.

[Nadrieril]

Can you use translate_dyn_binder here instead of managing the binder levels yourself?