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

[John Regehr via llvm-dev]

> 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