[RFC][EXPR] Formalize Integer Arithmetic Analysis

[tqchen]

The integer analysis (arith namespace) serves as a foundational tool for the low-level code generation. At this point, the analysis code is somewhat scattered in the codebase. This RFC proposes to revamp them.

Here is the list of currently related code:

• Symbolic integer simplification
  • Canonical form based simplification(as in CanonicalSimplify)
  • Rewrite-rule based simplification(Simplify in HalideIR)
• Symbolic interval bound analysis
• Modulo analysis(DetectLinearEquation)
• Deep equivalence checking

We have also seen issues on this topic.

• [BUG] Integer overflow during interval analysis and simplification #2455
• [RFC] Disable Floating-point distributive property #2418
• [ARITH] Improve Canonical Simplification to Handle Fused Pattern  #1711
• [ARITH] Simplifier Improvement #2173

Most of the current analysis functions can be put into two categories:

• Symbolic equivalent analysis: maps a symbolic expression e1 to e2 such that e2 and e1 are equivalent to each other (in the case of simplification)
• Relaxed integer set analysis: for e1, provide a set representation S, such that we ensure e1 \subset S.
  • For example, the result of DetectLinearEquation can be viewed as an integer set {x * factor + base}

Relaxed integer set analysis only requires us to find a superset of the corresponding set. Such relaxation allows us to deal with cases such as division or other functions.

Here is a list of observations about these analysis functions.

• They can use results from each other.
  • For example, we can use the result of a modulo analysis when simplifying divisions.
• They can complement each other.
  • Constant integer bound and symbolic bound can give us two different perspectives.
• They are context dependent
  • We need the context information about(bound, positiveness and other properties) about variables in an expression to get the best analysis result.

Given these observations, the new API is a super analyzer that carries states about the context information, and bundles sub-analyzers.

Proposed sub-analyzers

• CanonicalSimplifier
• RewriteSimplifier
• Deep equality class(via possibly via union-find)
• Symbolic interval finder
• Constant integer bound
• LinearEquation detector(modulo analysis)
• Integer polynomial(optional, its special case of the linear equation should be sufficient)
• Make it easy to plug-in a "new-view" when we have a new analysis

Each sub-analyzer will use memoization to cache the intermediate result. Importantly, each sub-analyzer has a handle(weak reference) back to the super analyzer to allow them to call other sub-analyzers. A user needs to create a super analyzer, populates related context states, and run the analysis.

Followup Goals Enabled by This Proposal

There are several things that formalization can enable.

• Better context-dependent analysis, we can populate context info(e.g., the shape size is non-negative), and use the information in code generation.
• Constant integer bound analysis and automatic integer narrowing.
  • So far we use int32 for most indices. Ideally, we want to be able to default to int64, and automatically narrows the integers to int32 when we detect all the arithmetic are within the bound.
• A centralized arithmetic logic that deals with integer analysis
• Improve simplification in general

Proposed Steps

• Design discussion and RFC comment(please reply to this thread).
• Pattern match utility to better port RewriteSimplification ([EXPR] Expression-template based pattern matching. #2589)
• Scaffolding of Super Analyzer and sub analyzer structure ([ARITH] Analyzer Infra, ConstIntBound, Modular #2668)
• Populating the new infra
  • constant integer bound
  • modular set
  • RewriteSimplifier
  • CanonicalSimplifier
• Migration the existing simplifier to the new stack
  Comments are welcomed.

[sgrechanik-h]

Concerning using int32/int64 for indices, I think we should create a separate, conceptually unbounded integer type for index arithmetic. Ideally, in compile-time we should use some arbitrary precision integer library for it, but using int64 may do as a starting point. (And of course it should be represented with int32/64 in run-time).

[sergei-mironov]

@tqchen I think this is very important direction to improve. Have you thought about using existing libraries like ISL? As far as I know it contains many useful algorithms and, more importantly, well-defined notation for describing formulas and relations of variables.

[tqchen]

re conceptual integer index. I think moving toward int64 as default and do optional narrowing is a good starting point as @sgrechanik-h pointed out.

re ISL. My understanding of isl is that it tries to do exact integer set analysis, and uses a constraint solver based approach(although I am not an expert in isl). As a result, it has some restrictions in terms of operation, as well as speed of solving.

In our case, we aim at providing simple forward solving ways for relaxed integer set analysis. Integer set abstraction and pushing most analysis to integer set primitives are important, and we should learn that perspective from isl.

On the other hand, I think the first pass of scaffolding should aim to build a self-contained analyzer. Then we can see if there is value to bring isl as an optional sub-anlayzer.

[tqchen]

Constant bound analyzer #2668