NLL: unsound verification of higher ranked outlives bounds

@rustbot

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

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?

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

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.

@lcnr

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

Update Clippy #74792 - flip1995:clippyup, r=Manishearth
Ensure stack when type checking and building MIR for large if expressions #74708 - kanru:issue-74564, r=davidtwco
Serialize span hygiene data #72121 - Aaron1011:final-hygiene-rebase, r=petrochenkov
Fix #[track_caller] shims for trait objects. #74784 - anp:track-vtables, r=eddyb
proc_macro: Add API for tracked access to environment variables #74653 - petrochenkov:pmenv, r=dtolnay
Pull out some duplicated code into a new function #74737 - smmalis37:astconv-factor, r=davidtwco
Rollup of 6 pull requests #74817 - JohnTitor:rollup-0fchdye, r=JohnTitor, rolling up:
- Avoid writes without any data in Write::write_all_vectored #74088 (Avoid writes without any data in Write::write_all_vectored)
- Fix sync_once_cell_does_not_leak_partially_constructed_boxes #74598 (Fix sync_once_cell_does_not_leak_partially_constructed_boxes)
- Clean up some uses of logging in ui tests #74750 (Clean up some uses of logging in ui tests)
- python codes cleanup #74783 (python codes cleanup)
- Don't italicize comments in ayu theme #74790 (Don't italicize comments in ayu theme)
- Fixed typo in closure #74799 (Fixed typo in closure)
Miri: replace canonical_alloc_id mechanism by extern_static_alloc_id #74775 - RalfJung:miri-alloc-ids, r=oli-obk
Rollup of 4 pull requests #74831 - Manishearth:rollup-ugw4pt4, r=Manishearth, rolling up:
- Make more primitive integer methods const #73858 (Make more primitive integer methods const)
- Forbid generic parameters in anon consts inside of type defaults #74487 (Forbid generic parameters in anon consts inside of type defaults)
- rustbuild: fix bad usage of UNIX exec() in rustc wrapper #74803 (rustbuild: fix bad usage of UNIX exec() in rustc wrapper)
- More ensure stack to avoid segfault with increased recursion_limit #74822 (More ensure stack to avoid segfault with increased recursion_limit)
convert higher ranked Predicates to PredicateKind::ForAll #73503 - lcnr:forall-predicate-what-and-why-2, r=nikomatsakis

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

@rustbot

WG-prioritization assigning priority (Zulip discussion).

@rustbot label -I-prioritize +P-critical

@oli-obk

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

rust/compiler/rustc_infer/src/infer/outlives/components.rs

Line 180 in edab34a

ty::Placeholder(..) |

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).

@aliemjay

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 :^)

@compiler-errors

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.

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

Auto merge of rust-lang#98109 - nikomatsakis:issue-98095, r=jackh726

Navigation Menu

Repository navigation

NLL: unsound verification of higher ranked outlives bounds #98095

Why does `test2` fail?

Why does `test1` not fail?

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

NLL: unsound verification of higher ranked outlives bounds #98095

Description

Activity

steffahn commented on Jun 14, 2022

rustbot commented on Jun 14, 2022

oli-obk commented on Jun 14, 2022

jackh726 commented on Jun 14, 2022

lqd commented on Jun 14, 2022

apiraino commented on Jun 14, 2022

nikomatsakis commented on Jun 14, 2022

compiler-errors commented on Jun 14, 2022

Why does test2 fail?

Why does test1 not fail?

nikomatsakis commented on Jun 14, 2022

nikomatsakis commented on Jun 15, 2022

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Why does `test2` fail?

Why does `test1` not fail?