Skip to content

ConstraintAnalysis: Add OR fusing of { x == C || x > C } => x >= C#8936

Merged
kripken merged 91 commits into
WebAssembly:mainfrom
kripken:compar.b.replace
Jul 24, 2026
Merged

ConstraintAnalysis: Add OR fusing of { x == C || x > C } => x >= C#8936
kripken merged 91 commits into
WebAssembly:mainfrom
kripken:compar.b.replace

Conversation

@kripken

@kripken kripken commented Jul 24, 2026

Copy link
Copy Markdown
Member

This is common in loops, where there is an initial value + a backedge that
has an incremented but bounded value.

To implement this, add full expansion of the OR of two AndedConstraintSets
into ANDs of the ORs of all their elements, and thorough checking there.

Comment thread test/gtest/constraint.cpp Outdated
Comment thread test/gtest/constraint.cpp Outdated
Comment thread test/gtest/constraint.cpp
checkOr(left7, right, right);

// Change 5 on the left to 99:
// { x == 99 } || { x > 5 && x <= 42 } ==> { x > 5 }

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can have a TODO for adding x <= 99 to the result.

Comment thread test/gtest/constraint.cpp
checkOr(left99, right, rightOnly5);

// Change 5 on the left to 4:
// { x == 4 } || { x > 5 && x <= 42 } ==> { x <= 42 }

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Similarly, we can have a TODO for adding x >= 4.

Comment thread test/gtest/constraint.cpp

// Changes to operations:

// Change the Eq on the left to Ne. We fail to find anything for the OR.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

TODO the result could be x != 5.

Comment thread test/gtest/constraint.cpp
checkOr(leftNe, right, empty);

// Change the GtS on the right to GtU:
// { x == 5 } || { x >U 5 && x <= 42 } ==> { x <= 42 }

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I assume this will be improved in the next PR?

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Eventually, yes, though maybe not the next PR. I'm trying to prove out the path to getting some specific Kotlin code working. I'll fill out related cases later.

kripken and others added 3 commits July 24, 2026 10:11
Co-authored-by: Thomas Lively <tlively123@gmail.com>
Co-authored-by: Thomas Lively <tlively123@gmail.com>
@tlively

tlively commented Jul 24, 2026

Copy link
Copy Markdown
Member

In general it seems profitable to "lift" pairs of greater-than and less-than bounds on constants as well as equality bounds with constants to intervals, do the join on the intervals, then lower them back to individual bounds.

@kripken

kripken commented Jul 24, 2026

Copy link
Copy Markdown
Member Author

Agreed, lifting to intervals internally may make sense here.

@kripken
kripken merged commit 87da91d into WebAssembly:main Jul 24, 2026
16 checks passed
@kripken
kripken deleted the compar.b.replace branch July 24, 2026 18:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants