[llvm-dev] InstCombine, graph rewriting, Equality saturation
Hal Finkel via llvm-dev
llvm-dev at lists.llvm.org
Fri Sep 8 17:32:44 PDT 2017
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:
> Link to review where this came up (and I first heard about it):
> 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.
> Also, there is the idea of Equality Saturation
> <http://www.cs.cornell.edu/%7Eross/publications/eqsat/>) that I found
> out about recently. Could this be used to augment the InstCombine
> Sending this from my phone, please excuse any typos!
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
Lead, Compiler Technology and Programming Languages
Leadership Computing Facility
Argonne National Laboratory
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the llvm-dev