Generic Global Variables

[ssyram]

We found that currently Eurydice does not support generic global variables. Originally, user-defined generic global variable is rare, but now, as we generate for each impl Trait for T a vtable instance for Trait, which is in turn a global variable, it becomes a common issue.

For example, if we test the following code like that in AeneasVerif/charon#873 :

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

It involves the impl <T: Debug> Debug for &T, and hence involves the generic global variable. Will there be a possible quick fix for this now? Like, can we share the logic of generic handling from functions to also globals?

We understand that this is a feature going to be deprecated in the future by mono migration, but it would be convenient at least for now to have this issue resolved.

[protz]

if you look at lib/krml/Monomorphization.ml, DGlobals are covered by the monomorphization procedure, so this should be handled.

Do you know what is not working? Right now your example gives me:

ERROR translating core::fmt::{core::fmt::Debug<&'0 @T>}::{vtable}: Not_found

so I can't investigate any further... thanks!

[ssyram]

Oh, according to @Lin23299 , he found that the Not_found problem comes from that the generic parameters are not properly pushed in the binders so that when translating with typ_of_ty, it says it cannot find the type parameter T.

He has also identified that in the AstOfLlbc file, the global translation does not push the generic binders as it is for functions. So we were curious about whether this is a design intention or just a bug that we can quickly fix.

[protz]

I'm pretty sure it's a bug. I was not aware that global variables could be generic. You should go ahead and fix it!