Skip to content

Soundness regression with for<'lt> closure having an implied bound from return type #114936

Closed
@danielhenrymantilla

Description

Bug originally found by @ast-ral, over Discord, which I've then reduced.

Code

I tried this code:

fn whoops(
    s: String,
    f: impl for<'s> FnOnce(&'s str) -> (&'static str, [&'static &'s (); 0]),
) -> &'static str
{
    f(&s).0
}

I expected to see this happen:

error[E0597]: `s` does not live long enough
 --> <source>:6:7
  |
6 |     f(&s).0
  |     --^^-
  |     | |
  |     | borrowed value does not live long enough
  |     argument requires that `s` is borrowed for `'static`
7 | }
  | - `s` dropped here while still borrowed

error: aborting due to previous error

For more information about this error, try `rustc --explain E0597`.

Instead, this happened: code compiles successfully

Version it soundly rejected this code:

1.64.0

Version with soundness regression

1.65.0 and onwards

Proof of unsoundness:

fn static_str_identity()
  -> impl for<'s> FnOnce(&'s str) -> (
        [&'static &'s (); 0],
        &'static str,
    )
{
    |s: &/* 's */ str| ( // <----------------+ inputs restricted to `'s`.
        [], // `: [&'static &'s (); 0]`,     |
            //   thus `'s : 'static` ->------+
            //            +-<----------------+
            //            |
            //            v
        s, // `: &'s str <: &'static str`
    )
}fn main()
{
    let f = static_str_identity();
    let local = String::from("...");
    let s: &'static str = f(&local).1; // <- should be rejected!
    drop(local);
    let _unrelated = String::from("UB!");
    dbg!(s); // <- compiles and prints `"UB!"`
}

@rustbot modify labels: +I-unsound +regression-from-stable-to-stable -regression-untriaged

Observations

  • This does not occur if the implied-lifetime-bounds array is in closure parameter position; so it looks like a bug w.r.t. not properly checking the closure output type implied bounds?

  • -Ztrait-solver=next does not help (as of 2023-08-16)

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Labels

C-bugCategory: This is a bug.I-unsoundIssue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/SoundnessP-highHigh priorityT-typesRelevant to the types team, which will review and decide on the PR/issue.regression-from-stable-to-stablePerformance or correctness regression from one stable version to another.

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions