Check vtable projections for validity in miri #130727

compiler-errors · 2024-09-23T00:20:16Z

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 · 2024-09-23T00:20:25Z

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 · 2024-09-23T00:51:27Z

Some changes occurred in compiler/rustc_codegen_cranelift

cc @bjorn3

Some changes occurred in compiler/rustc_codegen_gcc

cc @antoyo, @GuillaumeGomez

compiler-errors · 2024-09-23T01:00:55Z

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 · 2024-09-23T06:23:18Z

compiler/rustc_middle/src/mir/interpret/mod.rs

@@ -259,7 +258,7 @@ pub enum GlobalAlloc<'tcx> {
    /// The alloc ID is used as a function pointer.
    Function { instance: Instance<'tcx> },
    /// This alloc ID points to a symbolic (not-reified) vtable.
-    VTable(Ty<'tcx>, Option<ty::PolyExistentialTraitRef<'tcx>>),


Codegen fully identifies a vtable using just the Option<ty::PolyExistentialTraitRef<'tcx>>:

rust/compiler/rustc_codegen_ssa/src/meth.rs

Line 118 in bdacdfe

pub(crate) fn get_vtable<'tcx, Cx: CodegenMethods<'tcx>>(

So how can it be that Miri would require more than this? Is it just that currently it happens to be the case that vtables only depend on the principal (i.e., never depend on projections or auto traits) but we want to reserve the right to change this later?

Codegen fully identifies a vtable using a Option<PolyExistentialTraitRef> and a self Ty.

Miri doesn't require the full set of predicates, either, technically, but computing the set of projections that correspond to a vtable requires also using the self type to compute what the projections would be. We could also pass that in to the validity, since it's stored in the allocation, but that would be pretty expensive to test a bunch of projection goals every time we want to validate vtable equality.

For the record, that corresponds roughly to my alternative here:

#130727 (comment)

RalfJung · 2024-09-23T06:34:38Z

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.

RalfJung · 2024-09-23T06:38:13Z

compiler/rustc_middle/src/mir/interpret/error.rs

+        /// The vtable that was actually allocated into global memory.
+        allocated_vtable: &'tcx ty::List<ty::PolyExistentialPredicate<'tcx>>,
+        /// The vtable that was expected at the point in MIR that it was accessed.
+        expected_vtable: &'tcx ty::List<ty::PolyExistentialPredicate<'tcx>>,


"allocated" sounds odd here. IMO the previous distinction makes more sense -- the "expected" info comes from the type, and that is compared with the actual info stored in the vtable pointer. There is no "expected vtable", there's just an expected list of predicates. IOW, List<ty::PolyExistentialPredicate<'tcx>> isn't a vtable, only GlobalAlloc::Vtable is a vtable.

Well, I mostly had a problem with calling it a "trait". It's now not a trait, it's ... poly_existential_predicates which is a mouthful. I understand vtable is a misnomer here, but do you have a better suggestion for a name?

I think "allocated" also here makes total sense, it's the vtable that was allocated in the first place. "expected" here is what we expected the vtable to end up as; that's the unsoundness.

It's like calling the type of an allocation its "allocated type" and the type you end up making an invalid read on some place as its "expected type". Again, I'm totally happy to rename this, but I'd rather not call it "trait" when it's no longer an (existential) trait.

Maybe vtable → dyn type? After all this list is exactly all the things that go into a dyn Trait type.

Then I'd use expected_dyn_type and vtable_dyn_type.

Ya that's fine 👍

RalfJung · 2024-09-23T06:39:46Z

compiler/rustc_passes/src/reachable.rs

                        let ExistentialTraitRef { def_id, args } = trait_ref.skip_binder();
                        self.visit_def_id(def_id, "", &"");
                        self.visit(args);
                    }
+
+                    // FIXME: are we just skipping the auto traits here?
+                    // What is this reachability *for*?


There's a very detailed comment at the top of this file explaining what it is for.

RalfJung · 2024-09-23T06:40:59Z

compiler/rustc_const_eval/src/interpret/traits.rs

@@ -18,19 +18,18 @@ impl<'tcx, M: Machine<'tcx>> InterpCx<'tcx, M> {
    pub fn get_vtable_ptr(
        &self,
        ty: Ty<'tcx>,
-        poly_trait_ref: Option<ty::PolyExistentialTraitRef<'tcx>>,
+        vtable: &'tcx ty::List<ty::PolyExistentialPredicate<'tcx>>,


Please don't call this a "vtable". This is confusing the "information required to compute a vtable" with the resulting output, the vtable.

Do you have a better name than trait_ref, since that's no longer a valid name either?

RalfJung · 2024-09-23T06:44:51Z

src/tools/miri/tests/fail/issue-miri-3905-transmute-vtable-projection-term.rs

This is a validity test, so it should go in fail/validity. It should also have dyn in its name like all the other dyn trait tests. wrong-dyn-trait-assoc-type.rs would be a good name, IMO.

compiler-errors · 2024-09-23T06:58:54Z

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 assigned lcnr Sep 23, 2024

rustbot added S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. labels Sep 23, 2024

This comment has been minimized.

Sign in to view

Check vtable projections for validity in miri

ffa70dd

compiler-errors force-pushed the objects branch from 0d6923d to ffa70dd Compare September 23, 2024 00:51

RalfJung reviewed Sep 23, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Check vtable projections for validity in miri #130727

Check vtable projections for validity in miri #130727

compiler-errors commented Sep 23, 2024 •

edited

Loading

rustbot commented Sep 23, 2024

This comment has been minimized.

rustbot commented Sep 23, 2024

compiler-errors commented Sep 23, 2024 •

edited

Loading

RalfJung Sep 23, 2024

compiler-errors Sep 23, 2024

compiler-errors Sep 23, 2024

RalfJung commented Sep 23, 2024 •

edited

Loading

RalfJung Sep 23, 2024 •

edited

Loading

compiler-errors Sep 23, 2024

compiler-errors Sep 23, 2024

RalfJung Sep 23, 2024

compiler-errors Sep 23, 2024

RalfJung Sep 23, 2024

RalfJung Sep 23, 2024

compiler-errors Sep 23, 2024

RalfJung Sep 23, 2024

compiler-errors commented Sep 23, 2024 •

edited

Loading

	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;
	}

Check vtable projections for validity in miri #130727

Are you sure you want to change the base?

Check vtable projections for validity in miri #130727

Conversation

compiler-errors commented Sep 23, 2024 • edited Loading

rustbot commented Sep 23, 2024

This comment has been minimized.

rustbot commented Sep 23, 2024

compiler-errors commented Sep 23, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

RalfJung commented Sep 23, 2024 • edited Loading

RalfJung Sep 23, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

compiler-errors commented Sep 23, 2024 • edited Loading

compiler-errors commented Sep 23, 2024 •

edited

Loading

compiler-errors commented Sep 23, 2024 •

edited

Loading

RalfJung commented Sep 23, 2024 •

edited

Loading

RalfJung Sep 23, 2024 •

edited

Loading

compiler-errors commented Sep 23, 2024 •

edited

Loading