Repository navigation
Simplify (x*c0 + y)/c1 to x/(c1/c0) when 0 <= y < c0 - #9520
alexreinking wants to merge 4 commits into
Conversation
|
We're trying to delete all can_prove usage from the simplifier, as it's very expensive and not guaranteed to terminate. |
|
In general I'd like to be able to retrieve what the computed ConstantInterval was for subexpressions in rewrite rules, as those were already available while mutating the LHS of the division. But currently they've been dropped. |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## alexreinking/struct-let-loads #9520 +/- ##
================================================================
Coverage ? 72.79%
================================================================
Files ? 263
Lines ? 82133
Branches ? 20060
================================================================
Hits ? 59786
Misses ? 15957
Partials ? 6390 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
|
This is trivially done right once the can-prove-facts branch is in. |
How would you do this in terms of #9400's |
|
This PR no longer uses |
There was a problem hiding this comment.
I think this PR should also drop the last term in this predicate, because the new rules bundle in this transformation but omitting this last term. After discussion we decided the last term was a relic from before when we defined division by zero.
| // in_range only looks up the bounds already known for y, without | ||
| // simplifying anything, so it recognizes y only as a constant or a | ||
| // variable with constant bounds (from loops, lets, learned facts, | ||
| // or the caller's bounds), or a broadcast of one. |
There was a problem hiding this comment.
Please drop comment entirely. The rule is easier to read than the comment.
abadams
left a comment
There was a problem hiding this comment.
Approved pending two requested changes
505b388 to
f73276e
Compare
bc38e1e to
29dcc55
Compare
29dcc55 to
a5dbfc2
Compare
a5dbfc2 to
a471315
Compare
a471315 to
36e1bee
Compare
653a0e2 to
f7490c3
Compare
When c0 > 0 divides the denominator c1, x*c0 % c1 is a multiple of c0 no greater than |c1| - c0, so an offset y in [0, c0) can never carry into the next multiple of c1 and doesn't affect the quotient. For example, (x*4 + y) / 32 == x / 8 for y in [0, 4). This form arises when a reduction is split twice (e.g. into blocks of 32 and then lanes of 4) and a per-block factor is indexed by r / 32: after rfactor, the factor's index is ((lane*4 + rxi) / 32) + u, which this rule reduces to lane/8 + u so it can be recognized as invariant in the innermost loop. The bound on y is established with can_prove(y / c0 == 0), which is equivalent to 0 <= y < c0 for c0 > 0 and mentions y only once, following the existing ramp rule in Simplify_Mod.cpp. The rule is restricted to integer types (it is false for floats) and applies lanewise to vectors. It holds under the no-overflow assumption only, and is placed inside the existing no_overflow block. To be revisited when #9400 lands, which bounds can_prove's recursion depth and may offer an allocation-free alternative. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The (x*c0 + y)/c1 -> x/(c1/c0) rule checked 0 <= y < c0 with can_prove(y / c0 == 0), which builds and simplifies IR every time the rule's cheaper predicates pass. Replace it with a new IRMatch predicate, in_range(y, lo, hi, this), which tests y against the half-open range [lo, hi) without building, simplifying, or reference counting any IR. in_range requires y to be a wildcard and lo/hi to be WildConsts or integer literals (enforced by static_assert), and accepts only an integer constant, a variable whose constant bounds the simplifier already tracks (from loops, lets, learned facts, or the caller's bounds), or a broadcast of either. Anything else fails the predicate, so the rule no longer fires for compound offsets such as y % 4 or clamp(y, 0, 3). Wild::bound_node, WildConst::bound_const_int, IntLiteral::bound_const_int and the has_bound_node/has_bound_const_int traits are taken unchanged from #9400, which needs the same allocation-free access to matched terms. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Remove the obsolete nonzero quotient predicate and the explanatory comment on bounded-offset division rules. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Parse half-open range predicates with an optional matcher context, document their interpretation, and cover boundaries and bounded-offset division rules. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
f7490c3 to
6692ec4
Compare
Adds a Div simplifier rule (and its commuted form):
An offset
yin[0, c0)can't carry into the next multiple ofc1. This makes per-block factor indices such asscale((lane*4 + ki) / 32)invariant inki, sohoist_invariants()can hoist them (#9521).in_rangeis a new allocation-free IRMatch predicate, sincecan_proveis too expensive in rule predicates. It only reads constant bounds of anIntImm, a bareVariable(frombounds_and_alignment_info), or aBroadcastof either, so compound offsets likey % 4don't fire. It reuses #9400'sbound_node/bound_const_intbuilding blocks verbatim; whichever PR lands second gets one trivial conflict (keep #9400's side).Verified with
apps/simplifier_rule_verifier: true and correctly ordered under no-overflow (the rule is in theno_overflowblock), false with wraparound.Tests: positive and negative cases in
correctness_simplify.Authored by GitHub Copilot