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

Unsoundness related to implied bounds for return types #57265

Closed
scalexm opened this issue Jan 2, 2019 · 5 comments
Closed

Unsoundness related to implied bounds for return types #57265

scalexm opened this issue Jan 2, 2019 · 5 comments
Labels
A-NLL Area: Non Lexical Lifetimes (NLL) I-unsound Issue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/Soundness NLL-sound Working towards the "invalid code does not compile" goal regression-from-stable-to-stable Performance or correctness regression from one stable version to another.

Comments

@scalexm
Copy link
Member

scalexm commented Jan 2, 2019

The following code compiles and is unsound:

https://play.rust-lang.org/?version=stable&mode=debug&edition=2018&gist=fc4210fcb8ba91c1ae883cd20deb2279

I believe this is due to the fact that we compute implied bounds for return types? Ironically, I did write about this some months ago, as a reminder to myself for the implementation of the implied bounds RFC:

https://gist.github.com/scalexm/cf32cea831a5d8193fa8a484099b71a2

I wasn’t aware this bug was actually existing in Rust already.

cc @nikomatsakis

@matthewjasper matthewjasper added regression-from-stable-to-stable Performance or correctness regression from one stable version to another. I-unsound Issue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/Soundness A-NLL Area: Non Lexical Lifetimes (NLL) NLL-sound Working towards the "invalid code does not compile" goal labels Jan 2, 2019
@matthewjasper
Copy link
Contributor

Only an issue on 2018 edition. Probably NLL.

@scalexm
Copy link
Member Author

scalexm commented Jan 2, 2019

@matthewjasper Ah right I didn’t notice. This may make investigations easier.
What bugs me is the fact that y‘s type seems not to be WF-checked when declared.

@matthewjasper
Copy link
Contributor

Variable types aren't WF-checked in NLL. We should include the output type here:

sig.inputs().iter().map(|ty| ty::Predicate::WellFormed(ty)),

@scalexm
Copy link
Member Author

scalexm commented Jan 2, 2019

Variable types aren't WF-checked in NLL. We should include the output type here:

rust/src/librustc_mir/borrow_check/nll/type_check/mod.rs
Line 1455 in d370493
sig.inputs().iter().map(|ty| ty::Predicate::WellFormed(ty)),

Indeed, that works :) Care to make a PR? I won’t be able to do it myself today.

I’ve not been able to weaponize my code snippet with this fix (or with the 2015 edition); however I believe this is because currently, when you have fn(...) -> S<T> as an input type, like in:

fn call<'a, T>(x: &'a T, f: fn(&'a T) -> S<&'a T>) {
    let y = f(x);
}

then you consider S<&'a T> to be an input type as well, hence you have an implied &'a T: 'static bound preventing the kind of weaponization that I described in my gist.

But when we designed implied bounds with @nikomatsakis, we thought that function pointers would be seen only in a « shallow » way, i.e. we would not consider the types appearing in the function pointer as input types, so that we don’t get any implied bounds from them.

Regarding the fact that we currently do have implied bounds for return types, coupled with my gist above, I think we may want to reconsider either the WF-ness of function pointers in the implied bounds setting, or the computation of implied bounds for return types (but removing it would be a breaking change).

@nikomatsakis
Copy link
Contributor

I've always regretted that output types are used for WF purposes, but I don't know how to fix it without breakage.

Still @scalexm we should definitely revisit the definition and make sure we get this straight. We also have to think about the interaction of variance (#25860). I've been assuming that as we transition more towards chalk, we would be able to solve the soundness hole by encoding the "implied bounds" for a fn into the for binder on the fn type -- so e.g. the type might be for<'a> where ('a: 'static) fn(...) -> ... The basic idea is that variance only becomes a factor once we get to the fn pointer type. But I feel like there are enough subtle points here that we really have to sit down again and go over everything (particularly since the implied bounds proposal itself went through so many revisions).

bors added a commit that referenced this issue Jan 3, 2019
…akis

Wf-check the output type of a function in MIR-typeck

Closes #57265

cc @scalexm
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-NLL Area: Non Lexical Lifetimes (NLL) I-unsound Issue: A soundness hole (worst kind of bug), see: https://en.wikipedia.org/wiki/Soundness NLL-sound Working towards the "invalid code does not compile" goal regression-from-stable-to-stable Performance or correctness regression from one stable version to another.
Projects
None yet
Development

No branches or pull requests

3 participants