Skip to content
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

NLL: unsound verification of higher ranked outlives bounds #98095

Closed
aliemjay opened this issue Jun 14, 2022 · 10 comments · Fixed by #98109
Closed

NLL: unsound verification of higher ranked outlives bounds #98095

aliemjay opened this issue Jun 14, 2022 · 10 comments · Fixed by #98109
Assignees
Labels
C-bug Category: This is a bug. I-unsound Issue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/Soundness P-critical Critical priority regression-from-stable-to-nightly Performance or correctness regression from stable to nightly. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. T-types Relevant to the types team, which will review and decide on the PR/issue.

Comments

@aliemjay
Copy link
Member

This code now passes under under NLL after #95565: (playground)

fn assert_static<T>() where for<'a> T: 'a, {}

// `test` passes without requiring `T: 'static`
fn test<T>() { assert_static::<T>(); }

assert_static should be able to infer that T: 'static because, in the language of Chalk, I believe the bound for<'a> T: 'a should be lowered to forall<'a> { Outlives(T: 'a) :- WellFormed(T). } and because the well-formedness of T is assumed to be true, we can instantiate 'a to any lifetime including 'static.

@rustbot label T-compiler T-types regression-from-stable-to-nightly C-bug

@rustbot rustbot added C-bug Category: This is a bug. regression-from-stable-to-nightly Performance or correctness regression from stable to nightly. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. T-types Relevant to the types team, which will review and decide on the PR/issue. I-prioritize Issue: Indicates that prioritization has been requested for this issue. labels Jun 14, 2022
@jackh726 jackh726 added the I-types-nominated Nominated for discussion during a types team meeting. label Jun 14, 2022
@steffahn
Copy link
Member

steffahn commented Jun 14, 2022

Here’s a way to exploit this behavior for unsoundness:

use std::any::Any;

trait Lt<'a>: 'a {}
impl<'a, T: ?Sized + 'a> Lt<'a> for T {}

trait Tr {}
impl<T: ?Sized> Tr for T {}

fn test<T, R: Any>(x: T) -> R {
    // works despite non-'static
    step1::<T, R>(x)
}

// remark: starting in `test` with `step2` directly works, too.
fn step1<T, R: Any>(x: T) -> R
where
    for<'a> T: 'a,
{
    step2::<T, R>(x)
}

fn step2<T, R: Any>(x: T) -> R
where
    for<'a> T: Lt<'a>,
{
    step3::<T, R>(x)
}

fn step3<T, R: Any>(x: T) -> R
where
    T: Lt<'static>,
{
    step4::<T, R>(x)
}

fn step4<T, R: Any>(x: T) -> R
where
    T: 'static,
{
    *(Box::new(x) as Box<dyn Any>).downcast::<R>().unwrap()
}

fn main() {
    let x = String::from("Hello World");
    let r: &'static str = test(&x[..]);
    drop(x);
    println!("{r}");
}
����0V���

(playground)

@rustbot label I-unsound


Interestingly, not only calling step1 or step2 from test fails on stable, but calling step2 from step1 doesn’t work on stable either, so maybe a for<'a> T: 'a constraint on its own is actually kinda useless at the moment?

@rustbot

This comment was marked as resolved.

@rustbot rustbot added the I-unsound Issue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/Soundness label Jun 14, 2022
@oli-obk
Copy link
Contributor

oli-obk commented Jun 14, 2022

but calling step2 from step1 doesn’t work on stable either, so maybe a for<'a> T: 'a constraint on its own is actually kinda useless at the moment?

Yea fn foo<T>() where for<'a> T: 'a { foo::<T>() } fails to compile on stable right now, because higher kinded outlives bounds don't satisfy themselves

@jackh726
Copy link
Member

This is confirmed to be directly because of NLL and not something else.

I'm going to nominate for compiler team, since this is pretty significant. We'll continue to discuss within types team if there is a reasonable fix here, but I want this to be on people's radar since this might end up being a NLL stabilization revert in the short-term.

@jackh726 jackh726 added the I-compiler-nominated Nominated for discussion during a compiler team meeting. label Jun 14, 2022
@lqd
Copy link
Member

lqd commented Jun 14, 2022

This is used to be rejected by NLLs, and started being accepted in nightly-2020-07-28 (commit range).

List of merged PRs for that nightly

Out of those, #73503 looks like the most likely candidate, cc PR author @lcnr and reviewer @nikomatsakis.

@apiraino
Copy link
Contributor

WG-prioritization assigning priority (Zulip discussion).

@rustbot label -I-prioritize +P-critical

@rustbot rustbot added P-critical Critical priority and removed I-prioritize Issue: Indicates that prioritization has been requested for this issue. labels Jun 14, 2022
@nikomatsakis
Copy link
Contributor

Discussed with @oli-obk and @lcnr -- we believe the problem is that the outlives code isn't handling placeholder regions correctly... they are in this fallthrough

but they should be handled more like parameters, except that (at least at present) we can only bound them by 'static.

I might be able to make this fix today else could mentor someone potentially (ping me on Zulip).

@compiler-errors compiler-errors self-assigned this Jun 14, 2022
@compiler-errors
Copy link
Member

compiler-errors commented Jun 14, 2022

I have a somewhat clear understanding for why this happens. Specifically, consider the two cases:

fn outlives_forall<T>() where for<'u> T: 'u {}

fn test1<S>() { outlives_forall::<S>(); }

struct Value<'a>(&'a ());
fn test2<'a>() { outlives_forall::<Value<'a>>(); }

On stable, both test1 and test2 fail, because the migrate borrowck mode is still enabled. On nightly, just test2 fails.

Why does test2 fail?

When we call outlives_forall::<Value<'a>> in test2, we get back a TypeOutlives constraint that looks like Value<'a>: RePlaceholder(U1, 'u). We walk the type and gather its outlives components, being [ReFree('a)]. So we register ReFree('a): RePlaceholder(U1, 'u).

This part is a bit more fuzzy, but I think the outlives constraint establishes an edge on the SCC graph, that causes us to call incompatible_universe(), forcing the placeholder region to be inferred as 'static, and leading to the error.

Why does test1 not fail?

When we call outlives_forall::<S> in test1, we get an outlives constraint that instead looks like S: RePlaceholder(U1, 'u). We walk the type and gather its outlives components, being [U]. This means we don't register a region-outlives relationship, but instead delay this relationship as a type test. That type test looks like:

TypeTest { 
  generic_kind: T/#0, 
  lower_bound: '_#3r, 
  locations: Single(bb0[1]), 
  verify_bound: AnyBound([OutlivedBy('_#1r)]) 
}

where '_#3r is the placeholder and '_#1r is the region vid associated with the ReFree lifetime of the type parameter. What's notable is that this is basically equivalent to '_#1r: '_#3r, except for the fact that we don't use this when we're solving regions, and instead delay it as a test to be performed afterwards. This means we never call incompatible_universe, meaning we never shorten(?) the placeholder region to 'static...


What @aliemjay and @nikomatsakis independently found is that a second bug exists in eval_outlives that Niko fixed in #98109, one that only shows up in type tests as above. That is fixed with the PR, but it manifests other bugs :^)

@nikomatsakis
Copy link
Contributor

So @compiler-errors and I did a deep dive here. What we found is that:

  • There is a bug in the NLL type check (which @compiler-errors described above) that is causing it to be unsound.
  • However, fixing that bug exposes a (pre-existing) bug around how we handle for<'a> T: 'a bounds, particularly with projections, causing regressions.
  • The good news is that I think fixing this bug will benefit @oli-obk and others. (I'll describe it in detail later.) The bad news is that a proper fix is non-trivial, so for the short term it may be better to revert NLL stabilization. I'll have to check with @jackh726 about how difficult that will be.

@nikomatsakis
Copy link
Contributor

nikomatsakis commented Jun 15, 2022

Fix is in #98109, this includes the fix for both this bug and the bug that the fix revealed :)

@wesleywiser wesleywiser removed the I-compiler-nominated Nominated for discussion during a compiler team meeting. label Jun 23, 2022
@bors bors closed this as completed in d017d59 Jun 24, 2022
@jackh726 jackh726 removed the I-types-nominated Nominated for discussion during a types team meeting. label Jul 29, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
C-bug Category: This is a bug. I-unsound Issue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/Soundness P-critical Critical priority regression-from-stable-to-nightly Performance or correctness regression from stable to nightly. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. T-types Relevant to the types team, which will review and decide on the PR/issue.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

10 participants