Supporting vtables for closures

[ssyram]

This PR is a re-submission of #871 , as @Sam-Ni does not have the permission of running the CI, I resubmit for him to view the CI results.

This PR adds support for vtable instantiation for closures.
The implementation involves two main steps:

1. Matching a closure implementation

2. Instantiating the corresponding vtable

Step 1 is implemented in translate_body.rs, while Step 2 is implemented in translate_trait_objects.rs.
The modifications in each file are described below.

1. translate_body.rs

• translate_rvalue
  Supports registering closure trait implementations. For example, in the test file dyn-fn.rs, the closure |counter| { ... } is matched in the hax::ImplExprAtom::Builtin case and registered as a VTableInstance.

2. translate_trait_objects.rs

• add_method_to_vtable_def
  Adds additional checks for FnOnce when constructing the method field in the FnOnce vtable, due to the incompatibility of FnOnce::call_once with dyn-compatibility.

• get_vtable_instance_info
  Supports retrieving the vtable struct reference and the corresponding trait declaration reference for closures, based on their kind (Fn, FnMut, or FnOnce).

• add_supertraits_to_vtable_value
  Supports filling vtable fields with built-in supertraits. For closures supertraits, they are translated as VTableInstance with TraitImplSource::Closure(kind), generating a vtable according to the closure kind. For other built-in supertraits, they are translated as VTableInstance with TraitImplSource::Normal, whose trait reference itself is used as the impl reference (e.g. @2 := &core::marker::MetaSized::{vtable}).

• gen_vtable_instance_init_body
  Supports generating the vtable body for closures. Closure implementations are treated as trait implementations with no associated items and a single specialized closure method (call or call_mut). call_once is ignored due to the incompatibility mentioned above. Based on this design, the function retrieves (trait_pred, items) for closures and uses mk_field to add the specialized closure method.

• generate_closure_method_shim_ref
  Implements the generation of the closure method shim reference used in the mk_field in gen_vtable_instance_init_body.

[ssyram]

@protz Could you please help us approving the CI procedure?

[ssyram]

@sonmarcho @Nadrieril would you mind approving the CI for us?

[R1kM]

Done

[Nadrieril]

This is not acceptable in a PR. If a PR regresses a test like this you must indicate it in the PR description and explain why you think it is justified to accept this regression. In this case it's a panic, which at the very least should be changed to emit e rpoper error message (but most likely should be fixed instead).

[Sam-Ni]

Sorry for that. This panic occurs because Fn* Traits are builtin traits, which are marked opaque and not translated by default. I fixed this and now charon can translate closures.

[Sam-Ni]

However, a new panic appears when translating dyn-fn.rs. The error message is as follows:

error: Trying to generate a vtable shim for a non-vtable-safe method
  --> tests/ui/simple/dyn-fn.rs:8:15
   |
 8 |       takes_fn(&|counter| {
   |  _______________^
 9 | |         *counter += 1;
10 | |         true
11 | |     })
   | |_____^

This panic happened in function translate_vtable_shim, which assumes that the input impl_func_def is FullDefKind::AssocFun. However, when translating a closure, impl_func_def as a FullDefKind::Closure is passed. So the new problem is that FullDefKind::Closure does not have fields vtable_sig and sig, which are offered by FullDefKind::AssocFun. Should we fcollect these information in charon, or in hax?

[Nadrieril]

I see, this should be added in hax

[Nadrieril]

translate_fn_ptr doesn't work here?

[Nadrieril]

I'd prefer this method to be in translate_closures also

[Sam-Ni]

translate_fn_ptr doesn't work here?

We tried translate_fn_ptr and pass the impl_def of closure. However, error occurs when executing ``translate_fn_ptr->translate_fun_item` -> `translate_generic_args`, reporting “Unexpected error: could not find" type variables `closurekind` and `upvars`.

[Sam-Ni]

I'd prefer this method to be in translate_closures also

moved into translate_closures

[Nadrieril]

I looked into it, that's an inconsistency in hax actually. I fixed it in latest hax, translate_fn_ptr looks like it works now (the generics still need to be fixed up though of course).

[Nadrieril]

This overall looks good, the one issue is the new panic. In the future please don't submit PRs with such regressions without explaining them.

Also just so you know the PR description was not useful information: you don't need to say what you did, I will read that in the code; instead a PR description is useful for context and for why you did things a certain way. FYI LLMs are terrible at generating useful PR descriptions as far as I've seen, please avoid that in the future.

[Nadrieril]

You can't skip binders like that, this will result in errors if the binder is not trivial.. Please use translate_region_binder then erase the resulting charon::RegionBinder.

[Nadrieril]

Please use the appropriate translate_closure_bound_ref_etc method here instead of most of this function