Vtable Instance Support

[ssyram]

Continuing from #259, we propose another PR to support vtable instances, specifically generating concrete vtable pointers. Currently, Eurydice only supports generating vtable structs but not their instances.

We added a test by renaming dyn_trait_struct_type to dyn_trait and included a test case with use_trait(&100), which involves casting &i32 to &dyn Trait.

Charon currently lacks proper implementation for the drop field in vtable instances and implicit implementations. The latter is unavoidable since every vtable requires T: MetaSized, which relies on an implicit implementation. To address this, we introduced a comprehensive placeholder for Opaque values via a new built-in function Eurydice::opaque<T>(reason: char*) : T. This should resolve currently unhandled cases.

For the drop field, we temporarily implemented a Charon version that generates a placeholder value. Therefore, this PR can only be merged after drop is properly implemented, and it would be preferable to wait until implicit implementations are complete. The temporary version we used is https://github.com/ssyram/charon/tree/tmp-empty-drop.

However, two issues remain even after Charon is fully prepared:

Vtable Instance Initialisation

The primary concern involves the generated code for vtable instances. Currently, we produce:

static size_t _vtable__local_0 = Eurydice_sizeof(int32_t, size_t);
static size_t _vtable__local_1 = Eurydice_alignof(int32_t, size_t);

static dyn_trait_Trait__vtable_ _vtable__local_2 = {
    .size = _vtable__local_0,
    .align = _vtable__local_1,
    .drop = dyn_trait__vtable_drop_shim__92,
    .method_method = dyn_trait_method__vtable_method__92,
    .super_trait_0 = Eurydice_opaque(
        "missing supertrait vtable",
        core_marker_MetaSized__vtable_*,
        core_marker_MetaSized__vtable_*
    )
};

const dyn_trait_Trait__vtable_ dyn_trait__dyn_trait__Trait_for_i32___vtable_ = _vtable__local_2;

This code is incompatible with C compilers because the initializations of _vtable__local_2 and dyn_trait__dyn_trait__Trait_for_i32___vtable_ involve non-constant expressions. The only viable solution is to aggressively inline local variables, particularly within global variables.

Opaque handling

Also, the implementation of opaque now also raises compiler complaints: error: indirection of non-volatile null pointer will be deleted. I'm not sure if this is a problem -- I guess it should raise compilation complain as opaque itself is not acceptable for code compilation.

[protz]

Quick response before looking at this more in-depth:

• for initialization, perhaps one other option is to generate a special function, say, initialize_statics, that initializes the fields one by one, and rely on the user to call initialize_statics() before using any function from the library
• opaque: that's because the compiler knows you're dereferencing the NULL pointer, which is not allowed, and it's telling you it's removing your code (instead of generating code that crashes); this will presumably be resolved once the upstream issue is fixed, but if you want something better in the meanwhile, you can use KRML_HOST_EABORT which I think avoids this behavior

[ssyram]

Thanks for the discussion! Yes, I think to re-compose the logic of initialising the global variables is a more systematic approach. That could be another PR on this, haha. As there might be additional complexity as to what to globalize and what should remain local. E.g., if we have let x: &&i32 = &&0, then, we should definitely globalize the variable of storing 0 and storing &0, this is another tough analysis. Not to mention the inherent complexity of variable dependency resolving. I'll raise this as an issue for reminding.

While on the other hand, it would also be suitable for this specific case to handle vtable instances to be simpler -- we may do this via a more radical optimization -- i.e., by inlining the locals and optimizing the let x = e in x to all become e?

As for the second case, I'm rather curious about whether we actually should keep the compiler error, as opaque itself hints at that the user should provide his own implementation instead of assuming everything is OK and trying to run and hence causing unwanted & unexpected error there.

[ssyram]

Ah, no, I was then reminded by my notes on this case that theoretically, we should not have to use an additional function (i.e., initialize_statics) to initialise the global variables.

As internally, Rust has the same restriction as C that it will need to compute everything at compile time and load the compile-time constant as the final target value in runtime.

So, theoretically, we can ask Charon to ask Rustc to compute the final value, which, by a simple simplification, should simplify everything to leaving only the address-taking expressions for us to globalize, e.g., let x = &&0 ==> let x = let local_0 = 0 in let local_1 = &local_0 in &local_1.

[ssyram]

So, for the optimizations, do you think radically do inlining in at least the globals is acceptable? Or, how would you view the potential risk? Especially, I cannot see the problem of turning all let x = e in x to simply e. But current Eurydice passes seem to be more conservative on this front?

[protz]

So, theoretically, we can ask Charon to ask Rustc to compute the final value, which, by a simple simplification, should simplify everything to leaving only the address-taking expressions for us to globalize, e.g., let x = &&0 ==> let x = let local_0 = 0 in let local_1 = &local_0 in &local_1.

ok sounds good -- then in that case the plan is

1. try aggressive inlining of all let-bindings for statics (possibly via a dedicated phase)
2. if that fails, devise another mechanism to ask (via Charon) for the value of a global constant

As for the second case, I'm rather curious about whether we actually should keep the compiler error, as opaque itself hints at that the user should provide his own implementation instead of assuming everything is OK and trying to run and hence causing unwanted & unexpected error there.

the way we have done these things historically is to emit a DExternal so that

1. the user can see the prototype that they need to implement by hand
2. there is a linking error that makes it clear that you need to do something extra (as opposed to silently segfaulting, or worse, in your case, doing nothing, since the compiler is eliminating your *NULL)

[ssyram]

Thanks for the discussion! We agree with the first point. As for the second, the Eurydice::opaque<T> is a generic function, so Eurydice automatically drops it after its mono phase and requires us to provide the impl?

[protz]

You could implement it with a macro that uses KRML_HOST_EABORT to abort cleanly and return a value of type T?

[ssyram]

Sure, will try, thanks!

[ssyram]

Updated, I guess this is what you mean?

[protz]

Yes. Thanks!

[ssyram]

OK, we then further refined the problem, and added the generics to globals (see the latest two commits). But then Krml complains that:
"lib/krml/Checker.ml", line 126, characters 10-16: Assertion failed
We found that it is to assert that globals all should have empty generic types (also, globals do not have CGs):

| DGlobal (_, lid, n, t, _) ->
          assert (n = 0);
          { env with globals = M.add lid t env.globals }

This is in Krml, so we are not sure if it is a fundamental problem. Could you please have a look?

FYI, we are testing against the example:

fn use_debug(_d : &dyn std::fmt::Debug) {}
fn main() { use_debug(&&1) }

With the Charon branch in https://github.com/ssyram/charon/tree/tmp-empty-drop -- this branch now generates an empty stub for the drop fields.

[protz]

I will have a look, thank you.

Can globals have const generics in Rust?

[ssyram]

I think so, but should have a test to confirm if Rust itself has. Anyway, the generated LLBC will indeed have global with CGs. This is because the vtable instance will have the same generic params as the impl environment. But if this is a tough fix, we can ignore that and simply work on type parameters only. As I guess there is no use of vtable instances with CG in our urgent need.

[protz]

This diff in krml seems to be enough for your example to go through:

diff --git a/lib/Checker.ml b/lib/Checker.ml
index a6b0efc6..4399c882 100644
--- a/lib/Checker.ml
+++ b/lib/Checker.ml
@@ -123,7 +123,7 @@ let populate_env files =
           in
           { env with types = M.add lid typ env.types }
       | DGlobal (_, lid, n, t, _) ->
-          assert (n = 0);
+          let t = if n > 0 then TPoly ({ n; n_cgs = 0 }, t) else t in
           { env with globals = M.add lid t env.globals }
       | DFunction (_, _, n_cgs, n, ret, lid, binders, _) ->
           if not !Options.allow_tapps && n <> 0 then
@@ -212,7 +212,7 @@ and check_decl env d =
       let env = { env with n_cgs } in
       check env t body
   | DGlobal (_, name, n, t, body) ->
-      assert (n = 0);
+      assert (!Options.allow_tapps || n = 0);
       let env = locate env (InTop name) in
       check env t body
   | DExternal _

after that, your example fails with

Warning 2: in top-level declaration global_poly.main, in file global_poly: Reference to core.fmt.{core::fmt::Debug␣for␣&0␣(T)}.{vtable} has no corresponding implementation; please provide a C implementation

I believe this is because the references to the vtable have a name that is different from the vtable declaration; you also need to make sure references to the (now-polymorphic!) vtable are under an ETApp node to make sure they get monomorphized.

Hope this unblocks you -- let me know how far you get! Cheers.

[ssyram]

Thanks for this! We've tried the method, but we then found that it is more complicated than conceived that we will need to collect the fn_ptrs of traits as in the function pointers. As the generics for globals is just for this case, I'm personally considering ignoring / bypassing this problem by simply emitting an EAbort as the value and wait for the mono migration (#257) to complete.

Out of curiosity, I'm not sure that for example, in line 1887 of this PR, is this substitution a correct way or we should recover the TPoly type and use TApp instead?

[protz]

Is the vtable type a parameterized data type T<'a> and instances have type T? If so, yes, ETApp is necessary because it will trigger monomorphization

[Lin23299]

@protz Thanks for the help on the const flag for IdGlobal! Here is the other technical issue about Eurydice_opaque, for the generated C code:

typedef struct dyn_trait_Trait__vtable__s
{
  size_t size;
  size_t align;
  void (*drop)(Eurydice_dst_ref_mut_dd x0);
  void (*method_method)(Eurydice_dst_ref_mut_dd x0);
  core_marker_MetaSized__vtable_ *super_trait_0;
}
dyn_trait_Trait__vtable_;

dyn_trait_Trait__vtable_
dyn_trait__dyn_trait__Trait_for_i32___vtable_ =
  {
    .size = Eurydice_sizeof(int32_t, size_t), .align = Eurydice_alignof(int32_t, size_t),
    .drop = dyn_trait__vtable_drop_shim__92, .method_method = dyn_trait_method__vtable_method__92,
    .super_trait_0 = Eurydice_opaque("missing supertrait vtable",
      core_marker_MetaSized__vtable_ *,
      core_marker_MetaSized__vtable_ *)
  };

Basically we need this Eurydice_opaque("comment", t, _) to return a placeholder for type t. The solution provided by KRML_EABORT, or directly defining it as:

#define Eurydice_opaque(reason, t, _) *((t *)KRML_HOST_MALLOC(sizeof(t)))

will cause error: initializer element is not constant which I think is because we cannot use malloc (which is not a constant expression) to initialize a field of struct.

Currently I'm using

#define Eurydice_opaque(reason, t, _) (t)0

which can pass the test for this dyn_trait.rs. However, it seems quite Ad hoc but i cannot find an elegant implementation for this Eurydice_opaque to compile. Do you have a better idea?

[protz]

I don't have a better idea. Is it giving you a compiler warning, or is it working ok?

[Lin23299]

I don't have a better idea. Is it giving you a compiler warning, or is it working ok?

It's working for now. Then I just keep it as is