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

Potential WF unsoundness: predicate_obligations doesn't check compute's return type. #70168

Closed
eddyb opened this issue Mar 19, 2020 · 2 comments · Fixed by #70170
Closed

Potential WF unsoundness: predicate_obligations doesn't check compute's return type. #70168

eddyb opened this issue Mar 19, 2020 · 2 comments · Fixed by #70170
Labels
A-typesystem Area: The type system C-bug Category: This is a bug. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue.

Comments

@eddyb
Copy link
Member

eddyb commented Mar 19, 2020

WfPredicates::compute returns false if it can't make progress on an inference variable, and the original obligation should be retried later.
However, wf::predicate_obligations doesn't check that return type and may (incorrectly) return no obligations.

On #70107 I suggested this:

Maybe it would be better to have a struct NoProgress; and compute return Result<(), NoProgress> instead of bool.

I'm pretty sure now that it would've prevented this bug.


Looking at the users, only wfcheck uses this function, and only for the user-specified bounds, so it's possible inference variables are impossible to find (unless normalization introduces them, I guess?).
It might be fine to just create WellFormed obligation for the ty::Infer instead of bailing out (see below, this is the same as moving return false out of WfPredicats::compute)


Related, this looks wrong, or perhaps outdated?

assert!(self.compute(ty));

It's true that ty::Infer can't be found as the first type in the recursive call, but compute is a loop, and it uses Ty::walk.
I'm amazed nobody has triggered this assert by e.g. causing an inference variable to be unified with Vec<_>, how is that possible?

Maybe ty::Infer should only cause return false (i.e. return Err(NoProgress)) for ty0), not any of its descendants?

(EDIT: Read the code more carefully and the check is ty == ty0, so while it's not an early like I would prefer, it does seem to only trigger on the root type)

However, a few other things call WfPredicats::compute and it would be fine for them to create an obligation rather than erroring out, so maybe wf::obligations itself should do that check?

cc @nikomatsakis @matthewjasper

@jonas-schievink jonas-schievink added A-typesystem Area: The type system C-bug Category: This is a bug. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. labels Mar 19, 2020
@lcnr
Copy link
Contributor

lcnr commented Mar 19, 2020

#70107 changes the return type of compute to a Result and discards it using let _ = self.compute(ty). Might cause us to be slightly more cautious in the future.

@eddyb
Copy link
Member Author

eddyb commented Mar 19, 2020

I'm working on a fix that makes WfPredicates::compute itself never bail out, so the check is done in wf::obligations, hopefully that will also work nicely for consts.

EDIT: opened #70170.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-typesystem Area: The type system C-bug Category: This is a bug. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants