[ARITH] Analyzer CanonicalSimplifier #2891

tqchen · 2019-03-25T03:54:43Z

This PR contains one step of #2588

CanonicalSimplifier Infra
Support "split normal form" to handle simplification of div mod expressions
Move the old Canonical simplification to the new one
Move the reduction simplification to the new infra.

The main highlight of this PR is the introduction of the "split normal form", so we can simplify the following expression.

x/6*6 + (((x/3) % 2)*3) + (x % 3) => x

It is quite fun to implement the split normalization. Currently, we only support constant div and mod co-efficient for simplicity, we can consider adding symbolic support later.

tqchen · 2019-03-25T03:58:05Z

cc @sgrechanik-h @merrymercy @derisavi @kazum @sxjscience @wweic

tqchen · 2019-03-25T03:59:05Z

Also as a side note, this PR helps to demonstrate how we can consolidate some of the simplification infra around the Analayzer, which could be helpful to improve some open PR that @sgrechanik-h is working on

tqchen · 2019-03-26T21:46:19Z

CI is now green, would be great if we can get some inputs into the PR

tqchen · 2019-03-27T01:17:50Z

@Hzfengsy can you also help review this PR?

sgrechanik-h

Sorry, I have little time currently. I'll try to look again today or tomorrow.

sgrechanik-h · 2019-03-27T05:46:31Z

src/arithmetic/analyzer.cc

-  this->const_int_bound.Update(var, this->const_int_bound(expr));
-  this->modular_set.Update(var, this->modular_set(expr));
-  this->rewrite_simplify.Update(var, this->rewrite_simplify(expr));
+  Expr new_expr = expr;


I don't understand why do you copy expr to new_expr here.

To make new expr mutable

But none of the subsequent lines changes it, or am I wrong?.

sgrechanik-h · 2019-03-27T05:47:33Z

src/arithmetic/canonical_simplify.cc

+/*!
+ * \brief Internal "Split normal form" of expression.
+ *
+ * This is a special expression that represent


typo: represents

sgrechanik-h · 2019-03-27T05:50:29Z

src/arithmetic/canonical_simplify.cc

+  Expr NormalizeWithScale(int64_t sscale) const {
+    Expr res = this->index;
+    Type dtype = this->type;
+    CHECK_EQ(this->type, dtype);


This check seems redundant.

Just like an asset, to check runtime consistency

But dtype gets initialized with this->type in the previous line, so this check is obviously true.

sgrechanik-h · 2019-03-27T05:50:58Z

src/arithmetic/canonical_simplify.cc

+   * args are divided into segments with the same index.
+   * within each segment, the SplitExpr is ordered in descending order of lower_factor.
+   *
+   * \note Can be mutated by TryMergeSplitExpr, which is idempotent


What is TryMergeSplitExpr? (Didn't find it in the code)

sgrechanik-h · 2019-03-27T05:51:39Z

src/arithmetic/canonical_simplify.cc

+          //
+          //    ((x / (c * s)) * s + (x % (c * s)) / c
+          // => ((x / c) / s) * s + ((x / c) % s)
+          // => (x / c)


Honestly speaking, I can't understand this algorithm. Probably I have to return to it in a better
state of mind. Expanding the explanation may be helpful too.

The simplification rule and proof are correct. It's based on two basic rules:

Rule 1: (x % (c * s)) / c = (x / c) % s Proof: x can always be decomposed into p * c * s + q * c + r where 0 <= q * c + r < c * s and 0 <= r < c. Then, lhs = ((p * c * s + q * c + r) % (c * s)) / c = (q * c + r) / c = q rhs = ((p * c * s + q * c + r) / c) % s = (p * s + q) % s = q Thus, lhs = rhs Rule 2: (x / s) * s + x % s = x

Thanks. Although it not obvious to me if the rules are still correct for the C/C++ division used in tvm.

The rule works for both trunc div and floor version. Mainly because that the first rule only involves mul div and mod. And you can simply take abs of all operands and then take addd the final sign. The second rule is an invariant for both types of div

sgrechanik-h · 2019-03-27T05:52:09Z

src/arithmetic/canonical_simplify.cc

+    }
+    // sort by the entry
+    auto fcompare = [](const SplitExpr& lhs, const SplitExpr& rhs) {
+      // order by scale first


Shouldn't it be ordered by index first? Or at least if the indices are different, the elements
should be incomparable.

This is a good point, however, it is can be quite costly to deep compare indices. So instead we just order by the scale and factor so that it is mostly in a consistent form(ignoring the indices)

Since the algorithm assumes that the vector contains contiguous segments of same-index elements, we have to check in the comparison function if lhs and rhs have the same index, otherwise this assumption may be destroyed by sorting.

Also I would still suggest sorting by index because otherwise we may often get into the situation when something like f(x + y) - f(y + x) don't get simplified. And if it really leads to performance problems, we should think about optimizing deep comparison somehow (probably we can cache the size or some other measure of an expression).

For now the code is fine because the result is only directly used by normalize, which is the intended usecase. It does break if we call it in the middle.

The only reason why I am not sure about comparing index is that var comparison can depend on runtime, which makes its behavior indeterministic. I want to think a bit more about this before we come back to revisit it

sgrechanik-h · 2019-03-27T05:53:06Z

src/arithmetic/canonical_simplify.cc

+  void DivideBy(int64_t scale) {
+    this->base /= scale;
+    for (size_t i = 0; i < this->args.size(); ++i) {
+      args[i].CopyOnWrite()->scale /= scale;


Shouldn't we raise an error if some of the scales are not divisible by the argument?

sgrechanik-h · 2019-03-27T05:55:05Z

src/arithmetic/canonical_simplify.cc

+        return;
+      }
+    }
+    // Insert other in the end.


Probably we should also sort by index.

Hzfengsy · 2019-03-27T09:08:49Z

src/arithmetic/canonical_simplify.cc

+   * \param other The expression to be added.
+   * \param scale The additional scale on value.
+   */
+  void AddToSelf(SplitExpr other, int64_t scale) {


It may be a better way to use const SplitExpr &other instead of SplitExpr other

Need to use CopyOnWrite inside the arguments so use SplitExpr directly. If the item is newly constructed, other will be directly passed in as a unique copy, and CopyOnWrite will reuse that data from there.

Hzfengsy · 2019-03-27T12:28:42Z

src/arithmetic/canonical_simplify.cc

+  if (!IsIndexType(op->type)) {
+    return Rewriter::Mutate_(op, self);
+  }
+  // normalize


Probably we may build a function to reduce the duplicate code in above three functions

sgrechanik-h · 2019-03-28T17:42:58Z

src/arithmetic/canonical_simplify.cc

+          // note: x = z, c = 3, s = 2
+          //
+          //    ((z % 12) / 6) * 6 + ((z % 6) / 3) * 3
+          // => (((z % 12) / 6) * 2 + ((z % 12) % 6) / 3) * 3


Shouldn't there be a condition that lhs->upper_factor % rhs->upper_factor == 0 so that we can perform the transformation z % rhs->upper_factor => (z % lhs->upper_factor) % rhs->upper_factor?

This is an invariant condition that lhs->upper_factor % lhs->lower_factor == 0

tqchen · 2019-03-29T02:57:59Z

@Hzfengsy @sxjscience @sgrechanik-h thanks for the reviews, I have updated the comment blocks to add more explanations about the proof

xqdan · 2019-03-29T14:08:12Z

we have a case like this, can this PR handle it?

for (ee10, 0, 16) {
  for (mo_11, 0, 5) {
    for (mi_12, 0, 16) {
      for (ee13, 0, 16) {
        max_1[(((((((ee10*14) + (mo_11 + ((mi_12 + (mo_11*16))/14)))*14) + ((mi_12 + (mo_11*16)) % 14))*16) + ee13) + 2688)] = max_1_local_UB[((((((ee10*5) + mo_11)*16) + mi_12)*16) + ee13)]
      }
    }
  }
}

tqchen · 2019-03-29T18:31:38Z

@xqdan you should try it out. In theory this canonical simplifier is able to handle all kinds of div mode mul pattern that comes out from split and re-fuse

xqdan · 2019-03-30T00:49:03Z

@xqdan you should try it out. In theory this canonical simplifier is able to handle all kinds of div mode mul pattern that comes out from split and re-fuse

nice, I will try after this is merged.

kazum · 2019-03-30T10:48:51Z

src/arithmetic/canonical_simplify.cc

+          // note also the invariance lhs->upper_factor % lhs->lower_factor == 0
+          //
+          SplitExprNode* merged = rhs.CopyOnWrite();
+          merged->upper_factor = lhs->upper_factor;


Is this correct only when lhs->uppper_factor == kPosInf? For example, ((x % 5) / (3 * 2)) * 2 + (x % (3 * 2)) / 3 is simplified to x % 5 / 3, but this is not correct when x == 5.

See comment above on invariance

Ah I see, sorry for my confusion.

kazum · 2019-03-30T10:50:22Z

src/arithmetic/canonical_simplify.cc

+          // - s = lhs->scale / rhs->scale
+          // - c = rhs->lower_factor
+          //
+          //    ((x / (c * s)) * s + (x % (c * s)) / c


Redundant (.

(x / (c * s)) * s + (x % (c * s)) / c

kazum · 2019-03-30T14:23:54Z

src/arithmetic/canonical_simplify.cc

+          // note also the invariance lhs->upper_factor % lhs->lower_factor == 0
+          //
+          SplitExprNode* merged = rhs.CopyOnWrite();
+          merged->upper_factor = lhs->upper_factor;


Ah I see, sorry for my confusion.

kazum · 2019-03-30T14:31:57Z

src/arithmetic/canonical_simplify.cc

+  if (cval % lhs->scale == 0) {
+    int64_t scaled_cval = cval / lhs->scale;
+    lhs.CopyOnWrite()->scale = 1;
+    lhs.CopyOnWrite()->lower_factor *= scaled_cval;


Does this guarantee the invariance lhs->upper_factor % lhs->lower_factor == 0? It looks not obvious and I wonder if we should call lhs->Verify() here.

Nice catch :)

tqchen · 2019-03-30T18:08:52Z

@Hzfengsy @sxjscience @sgrechanik-h @kazum thanks for the reviews, please take another look

sgrechanik-h

I skimmed through the rest, seems ok. My main concern is sorting by the index field, but it can be done in subsequent PRs.

sgrechanik-h · 2019-03-28T17:44:28Z

src/arithmetic/canonical_simplify.cc

+   * \param coeff The co-efficient.
+   * \param out_divisible The result divisible component.
+   * \param out_non_divisible The non-divisible component.
+   * \return Whetjer detection is successful.


typo whether

sgrechanik-h · 2019-03-31T08:20:39Z

src/arithmetic/stmt_simplify.cc

+      ConstraintContext ctx(&analyzer_, Mutate(Not::make(condition)));
+      else_case = this->Mutate(op->else_case);
+    }
+    if (is_one(condition)) return op->then_case;


Shouldn't we return then_case instead of op->then_case here? (And same thing with the else_case)

kazum · 2019-03-31T17:56:42Z

src/arithmetic/canonical_simplify.cc

+      return lhs;
+    } else if (lhs->upper_factor <= (lhs->lower_factor * scaled_cval)) {
+      // (x % c1) / c2  => 0 when c2 >= c1
+      return ToSplitExpr(make_zero(lhs.type()));


Can we also return zero when cval % lhs->scale != 0? I mean the below looks correct in any cases.

if (lhs->upper_factor <= (lhs->lower_factor * cval / lhs->scale)) return ToSplitExpr(make_zero(lhs.type()));

Because the mul and division are not necessarily exchangeable, in the case of cval % lhs->scale != 0, we will need to consider the consequence more carefully, because it is rare to have such case, we just skip the optimization

tqchen · 2019-03-31T22:07:10Z

Thanks, @sgrechanik-h @sxjscience @kazum @xqdan @Hzfengsy , this is now merged

tqchen added the status: need review label Mar 25, 2019

tqchen force-pushed the canonical branch 2 times, most recently from 337f7d1 to b433c00 Compare March 25, 2019 05:12

tqchen added 2 commits March 25, 2019 20:16

[ARITH] CanonicalSimplfier

dc3f8ca

Remove old canonical

65eab01

tqchen force-pushed the canonical branch from b433c00 to 65eab01 Compare March 26, 2019 03:19

sgrechanik-h reviewed Mar 27, 2019

View reviewed changes

Hzfengsy reviewed Mar 27, 2019

View reviewed changes

address review comments

9477621

sgrechanik-h reviewed Mar 28, 2019

View reviewed changes

fix per comment

4e62769

tqchen added 2 commits March 28, 2019 23:04

more on proof

d0ccaf4

Move to avoid mutables and keep things immutable

8659cac

kazum requested changes Mar 30, 2019

View reviewed changes

kazum reviewed Mar 30, 2019

View reviewed changes

tqchen added 2 commits March 30, 2019 09:37

bugfix split div const

c7b8ac5

remove duplicate (

56d9406

sgrechanik-h approved these changes Mar 31, 2019

View reviewed changes

Hzfengsy approved these changes Mar 31, 2019

View reviewed changes

kazum reviewed Mar 31, 2019

View reviewed changes

Fix ifthenelse

f5151fe

kazum approved these changes Mar 31, 2019

View reviewed changes

tqchen removed the status: need review label Mar 31, 2019

tqchen merged commit 7afbca5 into apache:master Mar 31, 2019

tqchen deleted the canonical branch March 31, 2019 22:26

wweic pushed a commit to wweic/tvm that referenced this pull request Apr 7, 2019

[ARITH] Analyzer CanonicalSimplifier (apache#2891)

3b31cac

wweic pushed a commit to wweic/tvm that referenced this pull request Apr 7, 2019

[ARITH] Analyzer CanonicalSimplifier (apache#2891)

94417e7

wweic pushed a commit to wweic/tvm that referenced this pull request Apr 8, 2019

[ARITH] Analyzer CanonicalSimplifier (apache#2891)

428ae9b

wweic pushed a commit to wweic/tvm that referenced this pull request Apr 10, 2019

[ARITH] Analyzer CanonicalSimplifier (apache#2891)

083021c

wweic pushed a commit to neo-ai/tvm that referenced this pull request Apr 11, 2019

[ARITH] Analyzer CanonicalSimplifier (apache#2891)

af4a7a3

[ARITH] Analyzer CanonicalSimplifier #2891

[ARITH] Analyzer CanonicalSimplifier #2891

Conversation

tqchen commented Mar 25, 2019 • edited Loading

tqchen commented Mar 25, 2019 • edited Loading

tqchen commented Mar 25, 2019

tqchen commented Mar 26, 2019

tqchen commented Mar 27, 2019

sgrechanik-h left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sgrechanik-h Mar 28, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tqchen commented Mar 29, 2019

xqdan commented Mar 29, 2019

tqchen commented Mar 29, 2019

xqdan commented Mar 30, 2019 • edited Loading

Choose a reason for hiding this comment

tqchen Mar 30, 2019 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tqchen commented Mar 30, 2019

sgrechanik-h left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tqchen commented Mar 31, 2019 • edited Loading

tqchen commented Mar 25, 2019 •

edited

Loading

tqchen commented Mar 25, 2019 •

edited

Loading

sgrechanik-h Mar 28, 2019 •

edited

Loading

xqdan commented Mar 30, 2019 •

edited

Loading

tqchen Mar 30, 2019 •

edited

Loading

tqchen commented Mar 31, 2019 •

edited

Loading