[LLVMdev] [global-isel] Simplifying the simplifier

[Nuno Lopes]

>>>> What might be better is to put some abstract interface between
>>>> instcombine and the IR, so that instcombine can be run on these 
>>>> pseudo-MIs
>>>> as well as on IR.
>>>
>>>
>>> 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.
>>
>
> Just a comment:
> If you believe you can represent all instcombine transformations in
> DSL, you then transform them to C++.
> Why not work out a method for checking correctness in the C++?
> Then, you would not have to convert everything to DSL, and could run
> the checks on the current C++.
> The code in C++ should be able to be written in a static analysis
> friendly way so that we could use static analysis to prove no infinite
> loops.

I believe the advantage of writing down the optimizations in a DSL is that 
the representation is way more succinct.  The code in instcombine is a bit 
boring and repetitive (and huge!).
We could, however, try to automatically convert from C++ to the DSL.  Not 
impossible, AFAICT.
Proving absence of loops is a bit more complicated than traditional static 
analysis.  It often requires things like synthesis of ranking functions (to 
prove that the transition relation is well-founded), which is not trivial.

Nuni