Skip to content

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

Closed
@eddyb

Description

@eddyb

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-type-systemArea: Type systemC-bugCategory: This is a bug.T-compilerRelevant to the compiler team, which will review and decide on the PR/issue.

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions