[LLVMdev] annotations for optimization?

[David Blaikie]

On Tue, Nov 13, 2012 at 8:29 AM, Giacomo Tagliabue
<giacomo.tag at gmail.com> wrote:
> Hello everyone,
> As a research project we are trying to figure out how to insert some
> annotations in the compiler in order to optimize the code. For example:
>
> /*@ ensures x == 5 */
> if(x>5){
>   {...}
> }
>
> where the comment is written in ACSL. The example is trivial, but gives the
> idea, if LLVM is be able to read the annotation, it would optimize the code
> removing the if below.
> The question is: does exist an annotation language to do that? if it
> doesnt't exist, what should be modified in order to carry the information of
> the annotations into LLVM? In other words, how can we let LLVM "know" about
> these assertion?

LLVM currently doesn't have anything to do this. PR810 tracks some
thoughts/ideas/experiments with implementing something like this, but
it is, as yet, unresolved.

Basically the only really concrete idea that's been floated to address
this is to simply have front-ends branch on the "fact" (x == 5 in this
case) to an unreachable block (eg: "if (x == 5) { /* normal code */ }
else { unreachable }"). That way LLVM should see that the condition
dominates the uses & propagate the constant.

The problem with this is that the first thing LLVM does (in the
SimplyCFG pass) is throw out any unreachable blocks & drops the
condition - so we lose the "fact".

A possible solution to this would be to teach SimplifyCFG not to do
this. The problem here is that doing so impedes other optimizations
that don't see through the (constant) condition. Maybe this could be
fixed by improving optimizations, maybe. Possibly running some
optimizations again after removing the unreachable blocks later in the
compilation. But it's not clear that this strategy would actually have
a viable solution.

The alternative is some kind of explicit annotation scheme to describe
these facts. That's not something that's really been
explored/proposed/described in detail so far as I know.