Skip to content

trait cache can be poisoned through an associated type #42796

Closed
@arielb1

Description

@arielb1

I was trying to root out the root cause of #39970 and I found this:

Meta

rustc 1.20.0-nightly (445077963 2017-06-20)

STR

pub trait Mirror<Smoke> {
    type Image;
}

impl<T, Smoke> Mirror<Smoke> for T {
    type Image = T;
}

pub fn poison<S>(victim: String) where <String as Mirror<S>>::Image: Copy {
    loop { drop(victim); }
}

fn main() {
    let s = "Hello!".to_owned();
    let mut s_copy = s;
    s_copy.push_str("World!");
    "0wned!".to_owned();
    println!("{}", s);
}

Expected result

Code does not compile, because it attempts to copy a string..

Actual result

Code compiles, is UB, generally prints 0wned!

Explanation

The global fulfilled predicates cache (GlobalFulfilledPredicates) tries to cache "environment-independent" predicates. The idea is that if a predicate contains neither parameters nor inference variables, then whether it holds is unaffected by the parameter environment.

This property almost holds - because in the absence of inference variables, trait impl search is "predicative", its results are independent of the universe of types, and therefore can be transferred from a "maximal universe" where the type parameters can be assigned variables.

However, that argument isn't 100% correct. If predicates are inconsistent, then there can be no such "maximal universe", and so String: Copy might be implied by <String as Mirror<T>>::Image: Copy.

We can say that this would be "fixed by Chalk" (as of course, in the absence of "intelligent" caching, this is not a problem), but that assumes the implementation of Chalk would not make the same mistake. I think a good way to fix this would be to check global predicates in the empty environment directly - if the current environment is consistent that will return the correct result, and if it is inconsistent we already don't always care about any kind of stability (e.g. we occasionally "know" that [T] is never Sized, even if some predicate tries to claim so).

cc @nikomatsakis @aturon @RalfJung (are you interested in trait systems?)

Metadata

Metadata

Assignees

Labels

I-unsoundIssue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/SoundnessP-mediumMedium priorityT-compilerRelevant to the compiler team, which will review and decide on the PR/issue.

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions