Supporting dyn Trait

[ssyram]

Now the dyn Trait Support should be quite ready with a few TODOs.

Features Implemented

• Supporting associated types, now the vtable structs & instances all additionally take additional generic types corresponding to and taken from &dyn Trait's associated type restrictions. The basic support of the associated types are from Translate vtables with associated types #796.
• The vtable instances are now properly generated for the concrete impls, i.e., those with explicit impl Trait for Ty environments.
• The vtable method calls are propertly generated that, calling methods of &dyn Trait will be translated to finding the corresponding function pointer from the vtable (fetched by ptr_metadata operation) and then call the function pointer.
• A new pass is added to compute the correct vtable instance metadata when possible, i.e., the size, align and, the most complex case, the drop fields. Naturally, the content will not be computable if the stuff is behind a generics, this is inevitable and the fields will remain unknown. But everything should be explicit in the monomorphized case in the future. Specifically, the size and align subjects to whether the layout of the type is properly computable. The drop field, as the most complex case, now also handles the cases when the concrete impl types are Arrays & Tuples -- they should be the only composite cases.
• The vtable instances support for closures are now added. All tests passed. But there are identified issues, see Bug: Closures with drop glue translated ssyram/charon#20 for the closure itself. But it should work properly in most of the cases -- as dyn FnOnce is really strange, and rare.

TODOs

• Monomorphization support for dyn Trait.
• Vtable instances for closures.

[Nadrieril]

Haven't reviewed everything but from what I've seen: could you change how we represent the existential predicates? The current encoding will cause issues with generics (see inline comments).

[ssyram]

Thanks for all the suggestions from both of you! I'm still not sure about how to refractor the Predicate form. So I will leave it to the discussion in Zulip. Let me fetch & implement the vtable struct & instances first.

[ssyram]

Many fixes applied. Thanks for the advice. Mainly involving the fix for the three kinds of existential predicates. But I'm still not sure about if they work as expected...

[Nadrieril]

Could you add a lot of tests please? We need to cover edge cases even if we don't support them yet (write //@ known-failure at the top for these cases). We should have tests for supertraits, multiple supertraits, casting in a generic context, associated type projections, + 'a bounds, multiple trait bounds (dyn Any + Send), just builtins (dyn Send), traits with methods that are generic and have a Self: Sized bound (which makes them dyn-compatible but means the vtable doesn't have all the methods), etc.

[ssyram]

Yes, of course. Many tests are coming when the infrastructure is about to get done... Maybe we can focus on the implementation for now?

[Nadrieril]

Maybe we can focus on the implementation for now?

The tests will help me understand what the implementation is doing, I can't just be running the code in my head. It's imo crucial to add the tests while doing the implementation because that's when we think of edge cases. When we're done implementing it's too late.

[Nadrieril]

For the CI failures, unfortunately I don't know of a good way to normalize the paths, so just add //@ no-check-output to those test files.

[Nadrieril]

You shouldn't need a hack like that, what caused this?

[ssyram]

I will need the drop for Box type, to fill the vtable metadata. But this is not usually translated.

[Nadrieril]

The pointer here was not a mistake, creating &mut references has semantic side-effects which I don't fully understand, but I know the &mut in Drop::drop is a source of trickiness in relationship to Pin so we should not create more references than rustc does. Hence the pointer (it's meant to call drop_in_place anyway, which takes a pointer).

[ssyram]

Well, but the drop functions are all of type fn<'0>(&'0 mut Self). So I used & to provide the region info.

[Nadrieril]

The drop method of the Drop trait is not the same thing as the drop function we need to put in the vtable. The drop in the vtable must be the monomorphization of std::ptr::drop_in_place for the correct type, that's the language rules. And drop_in_place takes a *mut T not &mut T.

[Nadrieril]

Could you please split this PR into several for the many features it implements? I see at least:

• Remove the redundant TraitDeclRefs in TraitRefKind (that one could just be its own commit, doesn't need a full PR);
• Handle dyn Trait with associated types;
• Translate dyn Trait method calls;
• Support dyn Fn* for closures;
• There's probably more.

I can't review it like this with a messy commit history and a bunch of different features implemented at once. What I do see looks good though!

[ssyram]

The base of this, which implements the first feature you mentioned, is in your PR #796 . I reset the PR to start from that branch. I've made the PR to be as explicit as possible by trying to have one new feature in one commit ever since 171b81a. To break everything into new PRs involves resolving the connection with the current main branch... This is quite a tough work... So basically, the basic support is up until 171b81a, which accomplished the support of instances for Concrete impl blocks. Then, the pass to compute the metadata (e.g., size) is basically done in f68593d. After that, the support for vtables of closures is done in 8778c91 (sorry for the name, it should be vtables support for closures).

Another point is that the modification is one based on another, which makes it very hard to break into several self-contained PR... Do you have any good idea on this?

Also, the //@ no-check-output has been added but some new errors came.

[Nadrieril]

Sorry, I didn't mean that the PRs should be independent. It's ok if one PR depends on another. What I want is to be able to review one change at a time.