VTables of builtin traits are missing in monomorphic mode, making it impossible to just naively evaluated VTables, as all of them inherit from MetaSized, which never has a vtable. The simplest fix for this is probably to treat these traits as regular empty traits, and generate a vtable with drop/size/align.
Code:
fn main() {
let _x: &dyn Send = &0;
}
Command (output shortened):
$ charon rustc --monomorphize --print-llbc -- test.rs
# Final LLBC before serialization:
opaque type {vtable}
#[lang_item("Send")]
pub trait Send<Self>
fn main()
{
...
_x_1 = unsize_cast<&'6 i32, &'10 (dyn Send + '11), &vtable_of({built_in impl Send for i32})>(move _2)
...
}
Note this also happens with e.g. the Fn family of traits, in which case we would need to add the call method(s)
fn main() {
let _x: &dyn Fn() = &(|| {});
}
// compiles
// _x_1 = unsize_cast<&'6 closure, &'10 (dyn Fn<(), ImpliedClause1::ImpliedClause1::Output = ()> + '11), &vtable_of(impl_Fn_unit_for_closure)>(move _2)
VTables of builtin traits are missing in monomorphic mode, making it impossible to just naively evaluated VTables, as all of them inherit from
MetaSized, which never has a vtable. The simplest fix for this is probably to treat these traits as regular empty traits, and generate a vtable with drop/size/align.Code:
Command (output shortened):
Note this also happens with e.g. the
Fnfamily of traits, in which case we would need to add thecallmethod(s)