Miri does not report UB when transmuting vtables between instances of the same trait with different associated types

[ChayimFriedman2]

Take the following code for example (https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=f1fc9b16c4d0b7cc512fcd33ee2097b6):

trait Trait {
    type Assoc;
    
    fn foo(&self) {}
}

impl Trait for bool {
    type Assoc = bool;
}

fn main() {
    let v: Box<dyn Trait<Assoc = bool>> = Box::new(true);
    let _v: Box<dyn Trait<Assoc = ()>> = unsafe { std::mem::transmute(v) };
}

I included an empty function in the trait so its vtable won't be empty which may affect things somehow. AFAIK, changing principal trait (aka. not removing or adding auto traits only) is immediate UB, because the vtable has a validity invariant of being valid, and the compiler will exploit this (e.g. to hoist method loads).

However, Miri does not report this as UB.

[RalfJung]

We check that the principal trait still matches. But I seem to recall there was some problem with dyn types also affecting the type checker, where two dyn trait references were considered equal even when they should not? I don't know if that has been fixed already and Miri needs to copy that fix (i.e., the fix doesn't automatically apply everywhere), or whether that work is still ongoing, or whether it is a different issue.

Cc @lcnr @compiler-errors
The check that tries to ensure that the trait in the vtable matches the "expected" trait given in the type is here.

[compiler-errors]

@RalfJung: The type checker specifically checks that all projections are equal, but miri only checks the principal. I could extend the vtable compatibility check to implement this check, too, if you'd like.

Side-note: We probably also need to check that the auto traits match... I feel like there may be some sketchy stuff going on when we transmute dyn Trait to dyn Trait + Send, though I cannot immediately turn that into UB.

[compiler-errors]

But I seem to recall there was some problem with dyn types also affecting the type checker [...] I don't know if that has been fixed already and Miri needs to copy that fix (i.e., the fix doesn't automatically apply everywhere), or whether that work is still ongoing, or whether it is a different issue.

This is a totally unrelated issue to the recent strengthening of checks for pointer conversions allowed for a dyn trait (i.e. disallowing conversion like *const dyn Foo<A> as *const dyn Foo<B>), since this is using transmute.

[RalfJung]

Codegen has a fast-path where if the principal does not change in a cast, it makes the cast a NOP. So if the vtable is affected by anything not captured in the principal -- projections or auto traits -- isn't that completely unsound? In fact that fast-path only checks the DefId of the principal trait, it doesn't even check the generic parameters. How can that possibly be correct, given what you said above?

[RalfJung]

and the compiler will exploit this (e.g. to hoist method loads).

I'm pretty sure the compiler cannot exploit this since codegen fully identifies a vtable using the principal trait ref. So I am fairly sure that what Miri does (not erroring in your example) is correct wrt current codegen.

But if we might want to change codegen in the future to have the vtable depend on more than just the principal trait, then we should change this in Miri first.

[compiler-errors]

@RalfJung: How is what correct? I am not certain what you're asking.

Remember that that optimization during codegen is only being performed on well-formed unsize casts. Codegen is sound because we check during typeck that much stronger goals of the Unsize trait hold, which enforces equality of all of the parts of the dyn type, and we only permit certain kinds of casts to even make it to codegen.

Then during codegen, we can optimize a subset of those casts because they must correspond to cases where the whole dyn trait was equal (modulo auto traits). Like, if the principal def ids match during an unsize cast, then we must have previously proven that the whole trait ref and all the projections were equal.

This issue is unrelated to any soundness fixes recently fixed because miri is not validating an unsize cast right now; these are the source and target type of the transmute operator, which has no well-formedness checks performed on it except for the operand size.

Am I misunderstanding something? 🤔

[RalfJung]

Codegen is sound because we check during typeck that much stronger goals of the Unsize trait hold, which enforces equality of all of the parts of the dyn type, and we only permit certain kinds of casts to even make it to codegen.

If there is a non-local invariant on unsize casts here, then that should be documented in mir/syntax.rs and checked by MIR validation, and a comment in codegen should explain the chain of reasoning that makes it okay to skip this cast when the principals are identical. Absent that, I could only assume that codegen does this optimization because it is obviously trivially correct.

and the compiler will exploit this (e.g. to hoist method loads).

I am also curious what exactly the compiler does that would cause issues here.

[compiler-errors]

If there is a non-local invariant on unsize casts here, then that should be documented in mir/syntax.rs and checked by MIR validation, and a comment in codegen should explain the chain of reasoning that makes it okay to skip this cast when the principals are identical. Absent that, I could only assume that codegen does this optimization because it is obviously trivially correct.

Apparently it's "hard to check" :)

https://github.com/rust-lang/rust/blob/66b0b29e65c77e5801c308e725a233c0728df300/compiler/rustc_mir_transform/src/validate.rs#L1207-L1210

[RalfJung]

Apparently it's "hard to check" :)

That doesn't even say what is hard to check though, so I am not sure it is referring to the same things as what you have been talking about. It's also no explanation for a lack of comment in the MIR docs and in codegen. ;)

[compiler-errors]

It's also no explanation for a lack of comment in the MIR docs and in codegen. ;)

Well, I hope it's obvious that I didn't implement that codegen optimization or the lack of MIR validation, either. I'm just trying to explain why what is sound in codegen is sound today, according to the way the type system implements the (currently internal) Unsize trait.

I can probably get around to documenting the subtleties of how Unsize casts should be codegen'd, since I think I am well-equipped to do so, and I'm also skeptical that some validation couldn't be implemented for unsize casts, but this is definitely not my fault or doing; I basically just volunteering my knowledge here since I was pinged 😅

That doesn't even say what is hard to check though, so I am not sure it is referring to the same things as what you have been talking about.

As it stands, the way that the Unsize trait is implemented means that any cast that goes from dyn Tr<...> to dyn Tr<...> implies equality of trait refs. Somewhere in the middle this assumption is lost to the MIR validation or MIR syntax file or whatever, but it's certainly sound today.

This is difficult to check because it requires peeling a complex pair of type arguments to an unsize cast like &Struct<..., dyn A, ...> and &Struct<..., dyn B, ...> down to just the dyn types, then checking that if A and B correspond to the same trait ref, all their args are correct. The way this is implemented in HIR typeck is quite involved, and I would assume an equally annoying routine would need to be implemented for that as well.

[RalfJung]

To be clear I wasn't blaming you or anyone. :) I just expressed that the current situation led me to (incorrectly) conclude that the checks Miri does are sufficient, it is all quite non obvious and how that could be improved. If soundness of this is actually partially handled by the *library*, it seems even more important to write all this down, so yeah if you could do that that would be much appreciated. :)