[llvm-dev] InstCombine, graph rewriting, Equality saturation
John Regehr via llvm-dev
llvm-dev at lists.llvm.org
Fri Sep 8 20:31:36 PDT 2017
> 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
More information about the llvm-dev