Skip to content

Investigate order dependence in AvarBoundsInference::mergeReachableProgramVars #597

Open
@john-h-kastner

Description

@john-h-kastner

Issue #585 was closed by PR #589, but the underlying issue in AvarBoundsInference:: mergeReachableProgramVars is not fully resolved. The behavior of this function depends on the order it encounters potential bounds, when that shouldn't be the case.
The PR makes it so that order of the bounds is now consistent, so this no longer causes an observable bug, but this should still be resolved.

Matts comment on this from the PR:

But it appears to me that this particular loop is intended to produce an order-independent result: in effect, it's trying to choose the maximum bound variable (if any) from the set according to a particular partial order. So it would be good to understand why the result was order-dependent in the example of #585. If we don't want to do this now, fine, but I'd like to have an issue for follow-up, even though I realize that we might eventually decide to just replace this code rather than investigate the specific issue. (The issue could just link to this comment without further explanation.)

In fact, I may have spotted the mistake: When the code sees two incomparable variables (call them X and Y), it sets BVar = nullptr, but then the next variable Z will get stored in BVar unconditionally. It should be stored only if it is better than both X and Y. In general, I think we would keep a set of the best "incomparable" variables seen so far. Then for each variable Z, we add Z to the set and remove all variables worse than Z from the set. At the end, if the set contains exactly one variable, we use it, otherwise we have no result. Do you want to try implementing this and see if it fixes the problem on Windows even without this PR?

If that doesn't solve the problem, I guess the next step would be to add print statements for all the information that affects the partial order, run the code repeatedly on Windows until we see the two different results, and look at the debug output to (hopefully) see where the symmetry is being lost. In general, it's not good to have all of this error-prone boilerplate code that results from inlining the logic that defines the partial order into the logic that finds the maximum element according to that partial order. If we could factor those two things apart, it would probably make bugs like the one I alleged above much more obvious.

Originally posted by @mattmccutchen-cci in #589 (comment)

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions