Skip to content

incompletely relating alias args is unsound during vtable creation #140212

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lcnr opened this issue Apr 23, 2025 · 0 comments · May be fixed by #136988
Open

incompletely relating alias args is unsound during vtable creation #140212

lcnr opened this issue Apr 23, 2025 · 0 comments · May be fixed by #136988
Assignees
Labels
fixed-by-next-solver Fixed by the next-generation trait solver, `-Znext-solver`. I-unsound Issue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/Soundness P-medium Medium priority T-types Relevant to the types team, which will review and decide on the PR/issue.

Comments

@lcnr
Copy link
Contributor

lcnr commented Apr 23, 2025

cc #140211 the following snippet segfaults :3

trait Id {
    type This<'a>;
}
impl<T> Id for T {
    type This<'a> = T;
}

trait Trait<T> {}
impl<T: Id> Trait<for<'a> fn(T::This<'a>)> for T {}

trait Method<T: Id> {
    fn call_me(&self)
    where
        T: Trait<for<'a> fn(T::This<'a>)>;
}

impl<T, U> Method<U> for T {
    fn call_me(&self) {}
}

fn generic<T: Id>(x: &dyn Method<T>) {
    // Proving `T: Trait<for<'a> fn(T::This<'a>)>` holds.
    x.call_me();
}

fn main() {
    // Proving `u32: Trait<fn(u32)>` fails due to incompleteness.
    // We don't add the method to the vtable of `dyn Method`, so
    // calling it causes UB.
    generic::<u32>(&());
}
@rustbot rustbot added the needs-triage This issue may need triage. Remove it if it has been sufficiently triaged. label Apr 23, 2025
@lcnr lcnr added P-medium Medium priority I-unsound Issue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/Soundness T-types Relevant to the types team, which will review and decide on the PR/issue. fixed-by-next-solver Fixed by the next-generation trait solver, `-Znext-solver`. labels Apr 23, 2025
@lcnr lcnr moved this to new solver everywhere in T-types unsound issues Apr 23, 2025
@compiler-errors compiler-errors linked a pull request Apr 23, 2025 that will close this issue
@compiler-errors compiler-errors self-assigned this Apr 23, 2025
@saethlin saethlin removed the needs-triage This issue may need triage. Remove it if it has been sufficiently triaged. label Apr 23, 2025
bors added a commit to rust-lang-ci/rust that referenced this issue May 15, 2025
…s, r=lcnr

Use the new solver in the `impossible_predicates`

The old solver is unsound for many reasons. One of which was weaponized by `@lcnr` in rust-lang#140212, where the old solver was incompletely considering a dyn vtable method to be impossible and replacing its vtable entry with a null value. This null function could be called post-mono.

The new solver is expected to be less incomplete due to its correct handling of higher-ranked aliases in relate. This PR switches the `impossible_predicates` query to use the new solver, which patches this UB.

r? lcnr
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
fixed-by-next-solver Fixed by the next-generation trait solver, `-Znext-solver`. I-unsound Issue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/Soundness P-medium Medium priority T-types Relevant to the types team, which will review and decide on the PR/issue.
Projects
Status: new solver everywhere
Development

Successfully merging a pull request may close this issue.

4 participants