[LLVMdev] [global-isel] Simplifying the simplifier

[Jakob Stoklund Olesen]

On Aug 10, 2013, at 7:32 AM, Nuno Lopes <nunoplopes at sapo.pt> wrote:

>> I like the idea of sharing code between IR and MI passes through an abstract interface. I think that later stages in the IR pipeline also need an instruction optimizer instead of a canonicalizer.
>> 
>> An alternative approach would be to describe these transformations in a DSL instead of C++.
> 
>> *Legalization*
>> - What does 'more legal' mean? Can we restrict the possible legalization transformations so the iterative process is guaranteed to make progress?
> 
> 
> I've been thinking for a while that we could express the instcombine transformations in a DSL, and then generate the C++ code from there.  The advantage is that if we formalize the LLVM IR, then we can check the correctness of all the instcombine transformations for "free".
> Moreover, instcombine has also suffered from infinite loops in the past (because canonicalization did not make progress for some inputs), which is also your concern with legalization of MI.  We have algorithms to prove termination of rewriting systems, so I believe we could also prove progress for both instcombine and MI legalization.
> 
> I'm mixing MI legalization and instcombine, since I think that the correctness and progress checking technology that we would need is the exactly the same.
> I wouldn't mind working on this project.  But the time-frame on my side is academic, which may mean 1 or 2 years to be completed.

This sounds promising. But we have some requirements that textbook rewriting systems can't handle:

- Expressions are DAGs, not trees.
- Targets can add custom rewriting rules and override standard rules.
- Rules will have predicates. Some predicates are static and only depend on the subtarget, some predicates will depend on the pattern being matched.
- The system won't be convergent if you ignore all the predicates.

So the question is, given those requirements, can we still prove termination?

Thanks,
/jakob