-
Notifications
You must be signed in to change notification settings - Fork 3.5k
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
[ARITH] Analyzer RewriteSimplifier: add/sub/mul/div/mod #2722
Conversation
cc @sgrechanik-h @icemelon9 @merrymercy @kazum @grwlf @ZihengJiang @wweic @junrushao1994 @MarisaKirisame please help review the PR |
f590122
to
4ffb199
Compare
This fails for the case in #1711 (comment) ck.verify(x/6*6 + (((x/3) % 2)*3) + (x % 3), x) |
@merrymercy Rewrite simplifier is hard for solving cases like the nested fusion. We will need a improved canonical simplifier to deal with that. So that specific case will need to wait for a better canonical simplifier |
src/arithmetic/rewrite_simplify.cc
Outdated
// Recursive rewrite x | ||
// we limit maximum number of recursive rewrite allowed to | ||
// avoid infinite loop | ||
Expr RecursiveRewrite(Expr x) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
const Expr&
The following case succeeds.
However, the following case fails. Is this out of scope of this PR?
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Great work. I tried to enable it in my autodiff alongside with other simplifiers and didn't get any errors (and there were some small improvements). My main concern is that it is very hard to be sure about the correctness, maybe we should consider testing by generating random expressions using hypothesis or something like this?
} | ||
|
||
private: | ||
typename TA::Nested a_; | ||
typename TB::Nested b_; | ||
}; | ||
|
||
template<typename TA> | ||
class PConstWithTypeLike : | ||
public Pattern<PConstWithTypeLike<TA> > { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please add a class description and some description for its constructor parameters.
src/arithmetic/rewrite_simplify.cc
Outdated
Expr RecursiveRewrite(Expr x) { | ||
if (recur_counter_ >= kMaxRecurCount) return x; | ||
++recur_counter_; | ||
return Mutate(x); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have some doubts about this mechanism. Since the counter is global (for the whole expression), we might get into a situation when we hit the limit of recursive rewrites in one part of the expression and there won't be any more recursive steps allowed for other parts of the expression. Moreover, I think the limit should grow linearly with the expression size instead of being fixed. I would suggest some kind of fuel system, however I'm not sure if it's worth the trouble.
Also we might want to give warnings about expressions which cause the simplifier to exhaust the number of allowed recursive rewrites.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I thought it's was depth. Looks like it's number of calls we can make for the whole expression. Doesn't it make more sense to limit depth of RecursiveRewrite
calls?
TVM_TRY_REWRITE(x * y - x * z, x * (y - z)); | ||
TVM_TRY_REWRITE(y * x - x * z, x * (y - z)); | ||
TVM_TRY_REWRITE(x * y - z * x, x * (y - z)); | ||
TVM_TRY_REWRITE(y * x - z * x, x * (y - z)); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There many rules which are the same up to commutativity. Maybe we should consider adding some option to the Match
function to allow matching up to commutativity?
|
||
if (IsIndexType(op->type)) { | ||
// constant simplification rule | ||
TVM_TRY_REWRITE((x + c1) * c2, x * c2 + c1 * c2); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Does this rule contradict with one of TVM_TRY_REWRITE(x * y + x * z, x * (y + z))
from the Add
section? Does RewriteSimplifier stabilize if repeatedly applied many times?
Edit: (I'm not an expert in rewriting) Do we have some principle or good theory when specifying rewriting rules? For example, could we require that the result of rewriting always has less nodes than the input? I think we should better describe the current approach in comments.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This rewrite only works for constant and note that c1 * c2 will get automatically constant folded
namespace arith { | ||
|
||
using namespace ir; | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In my opinion, this approach to specifying rewriting rules has pros and cons. The good thing is that rule definition looks really clear. The bad thing I see is that rules are declared one after another in a single C++ function. We can't combine rules into bigger rules, and, more importantly, we can't call them individually e.g. in order to apply a testcase.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
in theory, CSE(common subexpression elimination) in compiler could pull out some of the common computed element of these rules and not recompute them
Thanks, @kazum @merrymercy @grwlf @sgrechanik-h for reviews, to collectivly answer some of the questions Coverage of TestcasesWe do not expect RewriteSimplifier to simplify all the possible cases. As a matter of fact, because most rewriting are local it is hard to get simplification over a long distance. This is a known limitation of the rewrite-based simplification. To complement that, we will need a new simplification strategy: CanonicalSimplifier, which brings canonical form and will make it much easier to simplify cases like So the goal of this PR is to get something that is correct and off the ground. We will continue to bring in new CanonicalSimplifier and improve both collectively. CorrectnessCorrectness is a big problem for us, that is why we need test-coverage, and code reviews to review these rules. The general goal is to vet the rules explicitly. Again since many of the weights are going to be carried by CanonicalSimplifier, we do not need to have a comprehensive list of rules in here. |
src/arithmetic/rewrite_simplify.cc
Outdated
Expr RecursiveRewrite(Expr x) { | ||
if (recur_counter_ >= kMaxRecurCount) return x; | ||
++recur_counter_; | ||
return Mutate(x); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I thought it's was depth. Looks like it's number of calls we can make for the whole expression. Doesn't it make more sense to limit depth of RecursiveRewrite
calls?
TVM_TRY_REWRITE(max(x, y - z) + z, max(x + z, y)); | ||
TVM_TRY_REWRITE(max(x - z, y) + z, max(x, y + z)); | ||
TVM_TRY_REWRITE(max(x, y) + min(x, y), x + y); | ||
TVM_TRY_REWRITE(min(x, y) + max(x, y), x + y); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Also add the following rule?
TVM_TRY_REWRITE(max(x, y) + min(y, x), x + y);
TVM_TRY_REWRITE(min(x, y) + max(y, x), x + y);
TVM_TRY_REWRITE(select(x, y, z) - z, | ||
select(x, y - z, ZeroWithTypeLike(z))); | ||
TVM_TRY_REWRITE(select(x, y, z) - y, | ||
select(x, ZeroWithTypeLike(y), z - y)); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks like tests for these cases are missing.
ck.verify(tvm.expr.Select(x > 0, y, z) - y, tvm.expr.Select(x > 0, 0, z - y))
ck.verify(tvm.expr.Select(x > 0, y, z) - z, tvm.expr.Select(x > 0, y - z, 0))
Changed to limit recursive depth as per suggestion by @wweic and @sgrechanik-h , added test cases suggested by @kazum . Please help take another look |
Thanks @kazum @wweic @sgrechanik-h @grwlf , this is now merged |
Follow up PR #2768 |
This PR contains one step of #2588
We still need to add rules for other ops. Given that these rules are self-contained and covered by test-case, I will request reviews and aim to merge them in before we can in parallel add support for other ops.
Need a few reviewers to check since the rules can be tricky(even though when each of them are covered by at least one test case)