[llvm-dev] InstCombine, graph rewriting, Equality saturation

[Hal Finkel via llvm-dev]

On 09/05/2017 05:57 PM, (IIIT) Siddharth Bhat via llvm-dev wrote:

> Hello all,
>
> I've seen some discussion that InstCombine is "too general" and that 
> llvm should implement a proper graph rewrite mechanism:
>
> Link to llvm-dev discussion about this: 
> http://lists.llvm.org/pipermail/llvm-dev/2017-May/113219.html,
> Link to review where this came up (and I first heard about it): 
> https://reviews.llvm.org/D37195.
>
> I wanted to understand what the current issues with InstCombine are, 
> and if a graph rewriter prototype is something people are interested 
> in. I find the idea appealing, from what little I know it, so I'd be 
> interested in hacking something up.
>
> What would such a framework look like? Is there past literature on the 
> subject? From what I know, many functional compilers using combinator 
> based compilation were graph rewriting. Is there other prior art?

I'm not sure that I'd describe it as "too general", but I suspect that 
it could be made much more efficient. Currently, the patterns are 
implemented in C++, which is often fairly verbose, and because many of 
the checks are implemented separately, we end up touching instructions 
many times as we attempt to match different patterns. Worse, for many of 
these instructions we end up checking properties, such as known bits, 
that are computed by further backward instructions visiting. It is also 
hard to automatically check the correctness of the transformations, and 
moreover, it is hard to prove that we'll eventually reach a fixed point 
(we've certainly had problems in the past where some inputs would cause 
an endless loop between two different InstCombine patterns).

I'd love to see a solution where most of the transformations were 
specified in TableGen files and:
  1. We, as a result, had an easy way to convert these into a form where 
some SMT-solver-based checker could certify correctness.
  2. We, as a result, has an easy way to somehow check soundness, as a 
rewrite system, so we'd know it would reach a fixed point for all inputs.
  3. We, as a result, reduced the number of lines of code we need to 
maintain for these peephole optimizations.
  4. We, as a result, could generate efficient code for matching the 
patterns using some automaton technique for minimizing unnecessary 
visiting of instructions.

I'm not sure how closely it matches what we would need, but Stratego/XT 
comes to mind in terms of prior art (now here: 
http://www.metaborg.org/en/latest/). There's been a lot of work over the 
years on terminating graph rewriting systems in compilers.

  -Hal

>
> Also, there is the idea of Equality Saturation 
> (http://www.cs.cornell.edu/~ross/publications/eqsat/ 
> <http://www.cs.cornell.edu/%7Eross/publications/eqsat/>) that I found 
> out about recently. Could this be used to augment the InstCombine 
> infrastructure?
>
> Thanks,
> ~Siddharth
>
> -- 
> Sending this from my phone, please excuse any typos!
>
>
> _______________________________________________
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev

-- 
Hal Finkel
Lead, Compiler Technology and Programming Languages
Leadership Computing Facility
Argonne National Laboratory

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20170908/cfec3a54/attachment.html>