Check vtable projections for validity in miri

[compiler-errors]

Currently, miri does not catch when we transmute dyn Trait<Assoc = A> to dyn Trait<Assoc = B>. This PR implements such a check, and fixes rust-lang/miri#3905.

To do this, we modify GlobalAlloc::VTable to contain the whole list of PolyExistentialPredicate, and then modify check_vtable_for_type to validate the PolyExistentialProjections of the vtable, along with the principal trait that was already being validated.

cc @RalfJung
r? @lcnr or types

I also tweaked the diagnostics a bit.

---

Open question: We don't validate the auto traits. You can transmute dyn Foo into dyn Foo + Send. Should we check that? We currently have a test that exercises this as not being UB:

rust/src/tools/miri/tests/pass/dyn-upcast.rs

Lines 14 to 20 in 6c6d210

	fn vtable_nop_cast() {
	let ptr: &dyn fmt::Debug = &0;
	// We transmute things around, but the principal trait does not change, so this is allowed.
	let ptr: *const (dyn fmt::Debug + Send + Sync) = unsafe { std::mem::transmute(ptr) };
	// This cast is a NOP and should be allowed.
	let _ptr2 = ptr as *const dyn fmt::Debug;
	}

I'm not actually sure if we ever decided that's actually UB or not 🤔

We could perhaps still check that the underlying type of the object (i.e. the concrete type that was unsized) implements the auto traits, to catch UB like:

fn main() {
    let x: &dyn Trait = &std::ptr::null_mut::<()>();
    let _: &(dyn Trait + Send) = std::mem::transmute(x);
    //~^ this vtable is not allocated for a type that is `Send`!
}

[rustbot]

Some changes occurred to the CTFE / Miri interpreter

cc @rust-lang/miri

The Miri subtree was changed

cc @rust-lang/miri

Some changes occurred to the CTFE / Miri interpreter

cc @rust-lang/miri

[rustbot]

Some changes occurred in compiler/rustc_codegen_cranelift

cc @bjorn3

Some changes occurred in compiler/rustc_codegen_gcc

cc @antoyo, @GuillaumeGomez

[compiler-errors]

There's technically an alternative here: we could, perhaps, keep the Option<PolyExistentialTraitRef> in the GlobalAlloc::VTable, rather than storing the whole list of poly existential preds.

Then for each projection pred in check_vtable_for_type, we could just prove that predicate holds for the concrete type of the vtable (since miri stores that). This should be complete, since if we prove that the principal trait refs are equivalent, the projections are uniquely determined by those trait refs. So we're just validating that they're correct.

That doesn't seem as nice, though; I like just storing the full set of predicates in the vtable allocation lol.

[RalfJung]

Open question: We don't validate the auto traits. You can transmute dyn Foo into dyn Foo + Send. Should we check that? We currently have a test that exercises this as not being UB:

I'm fine with making this UB. Codegen does rely on these vtables being the same (dropping auto traits in a cast compiles to a NOP), so it is crucial that this does not affect vtable layout... but Miri anyway doesn't have this cast short-cut, and we probably don't want to turn this into a hard guarantee.

Then for each projection pred in check_vtable_for_type, we could just prove that predicate holds for the concrete type of the vtable (since miri stores that). This should be complete, since if we prove that the principal trait refs are equivalent, the projections are uniquely determined by those trait refs. So we're just validating that they're correct.

Ah, so that explains why codegen can get away with just knowing the principal trait ref when generating the vtable -- it also knows the type, and it gets to assume that the type and the impl satisfy the remaining predicates.

This alternative proposal would be equivalent for associated types, right? But for auto traits it would allow transmutes that remove auto traits, or those that add them when the underlying type actually satisfies the auto trait, but reject the case where the auto trait is not satisfied by the underlying type?

I think I am fine with having maximal UB here, i.e. requiring the auto trait list to exactly match, which would require storing the full list of predicates.
Cc @rust-lang/opsem to see what other people think.

[compiler-errors]

I'm fine with making this UB. Codegen does rely on these vtables being the same (dropping auto traits in a cast compiles to a NOP), so it is crucial that this does not affect vtable layout... but Miri anyway doesn't have this cast short-cut, and we probably don't want to turn this into a hard guarantee.

For the record, I think I'd like to split out validating vtable auto traits from this PR. I wouldn't be surprised if there are crates in the wild that are currently using transmutes to temporaily smuggle dyn Trait + Send through dyn Trait or something like that, and I'd rather not add additional churn or FCP or whatever to what is otherwise just a totally sane UB detection in this PR.

[rustbot]

This PR changes Stable MIR

cc @oli-obk, @celinval, @ouz-a

[compiler-errors]

cheers for a miri that detects more UB 🎉

@bors r=RalfJung rollup

[bors]

📌 Commit 702a644 has been approved by RalfJung

It is now in the queue for this repository.