Skip to content

Emit vtables for "trivial" trait objects that only contain auto traits #239

Description

@RyanGlScott

If you compile this program with saw-rustc:

// test.rs
pub fn f() -> bool {
    let x: &(dyn Send + Sync) = &0u32;
    let p = x as *const _;
    std::ptr::addr_eq(p, p)
}

Then the resulting MIR JSON file will have no vtables:

$ saw-rustc test.rs
$ jq .vtables test.linked-mir.json
[]

This is surprising, as there actually is a vtable backing x: &(dyn Send + Sync). The reason that a vtable doesn't appear in the MIR JSON file is an artifact of the implementation, which uses RawList::principal as part of computing the vtable. RawList::principal will only return Some in the event that at least one trait in the trait object is not an auto trait. Per the documentation for RawList::principal:

It is also possible to have a “trivial” trait object that consists only of auto traits, with no principal - for example, dyn Send + Sync. In that case, the set of auto-trait bounds is {Send, Sync}, while there is no principal. These trait objects have a “trivial” vtable consisting of just the size, alignment, and destructor.

x is an example of a trait object with only auto traits, and as such, RawList::principal returns None on it, causing mir-json to incorrectly conclude that x doesn't have a vtable. As the documentation above indicates, however, we ought to compute a "trivial" vtable instead. We should also make sure that when casting &0u32 from type &u32 to type &(dyn Send + Sync), the cast uses UnsizeVtable instead of Unsize. (Doing so would likely fix GaloisInc/crucible#1730 as a side effect.)

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions