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

John Regehr via llvm-dev
2017-09-09T03:31:36Z

> 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.

YES to all of this (except TableGen :).

It should also be possible to find chains of transformations that fire
in sequence and make them happen all at once, avoiding intermediate
results and associated allocations/deallocations. Nuno has some ideas
along these lines.

> 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.

I went down this rabbit hole a few years ago, there's indeed a lot of
existing material.

John