[llvm-dev] Path condition propagation

Sean Silva via llvm-dev llvm-dev at lists.llvm.org
Fri Jul 1 15:29:22 PDT 2016


Thanks for the explanation!

On Fri, Jul 1, 2016 at 1:06 AM, Daniel Berlin <dberlin at dberlin.org> wrote:

>
>
> On Fri, Jul 1, 2016 at 12:19 AM, Sean Silva <chisophugis at gmail.com> wrote:
>
>>
>>
>> On Thu, Jun 30, 2016 at 8:45 PM, Daniel Berlin <dberlin at dberlin.org>
>> wrote:
>>
>>> The current gvn equality propagation is not powerful enough to get this
>>> because it doesn't try to infer values in predicates based on other
>>> predicates,   so it never realizes a>b -> a !=b in a useful way.
>>>
>>> It otherwise would get this
>>>
>>
>> Sorry if this is a bit of a stupid question, but what exactly is the
>> scope of what a GVN pass does?
>>
>
> Depends on who you ask. The most general correct answer i can give is:
> prove whatever things it can to be equivalent by computing their value.
>
> If you could prove everything equivalent that is possible, you would,
> subject to compile time :)
>
> Think of GVN as an analysis whose goal is to prove what things in the
> domain of the program have equivalent values.
>
>
>> I've read various "textbook" definitions of GVN but they all seem to
>> revolve around proving that different expressions in the program are
>> equivalent.
>>
>
> Most textboox definitions ignore conditionals.
> For example, "complete" value numbering would be discovery of all herbrand
> equivalences.
> This ignores conditionals and what equivalences they can be used to prove
> (they treat conditionals as always non-deterministic).
>
> Predicated GVN algorithms instead try to take predicates into account, in
> order to infer the equality of more values.  If you were, for example, to
> drop the predicate support current GVN has, you'd heavily decrease it's
> effectiveness.
>
> Note that a lot of research papers have to be read very carefully to
> discover what their domain is.
>
> If you read, http://arxiv.org/pdf/1302.6325.pdf, they point out most of
> the papers restrict the problem to discovering the equality of variables in
> the program, and not discovering the equality of *expressions*.
>
>
>
>> What you're talking about here seems to go outside that; e.g. being more
>> like what one would expect CorrelatedValuePropagation to do.
>>
>> You are just thinking about it in terms of existing program expressions.
>
> Necula proves (here:
> http://people.eecs.berkeley.edu/~necula/Papers/gvndet_sas04.pdf) that
> there is a significant distinction to be made between computing all
> herbrand equivalences and computing all herbrand equivalences among
> sub-expressions of the program.
>
> In this case, GVN would just be proving n1 == n2 is equivalent to the
> expression false.
> If it has some form of redundancy elimination built on top of it, it
> usually then replaces it with that value.
> It would then do nothing else.
>
> It's possible to unify gvn with dead code elimination and constant
> propagation (pretty easily in fact).
>
> In such a formulation, it will discover that n1 == n2 is equivalent to
> false, and thus that the block it leads to is unreachable.
>
> Again, the new gvn itself does nothing with this info other than use it to
> further prove things about values (IE for example, that only one edge of a
> phi is live and thus the phi has the same value as that live edge's
> incoming value).
>
> Elimination can, of course, trivially just delete all the unreachable
> blocks (or mark them unreachable if it wants).
>
> Our current GVN already does predication, just not in a very
> algorithmically complete way.
>
> Doing it in a complete way would eliminate most of
> correlatedValuePropagation. You could eliminate the rest of it by
> integrating proper range analysis as you want. That's just "another source
> of predicates".
>
> In *practice*, what i care about is getting good enough results quickly,
> and making GVN a real analysis used by other things (PRE, etc) while making
> it fast.
>
> (If i ever finish, i'll then likely move on to replacing LVI with some
> extended SSA + range analysis :P)
>
>
>> -- Sean Silva
>>
>>
>>>
>>> On Thu, Jun 30, 2016, 7:41 PM Sean Silva <chisophugis at gmail.com> wrote:
>>>
>>>> On Thu, Jun 30, 2016 at 6:45 PM, Daniel Berlin via llvm-dev <
>>>> llvm-dev at lists.llvm.org> wrote:
>>>>
>>>>>
>>>>>
>>>>> On Thu, Jun 30, 2016 at 6:09 PM, Carlos Liam via llvm-dev <
>>>>> llvm-dev at lists.llvm.org> wrote:
>>>>>
>>>>>> Hi all,
>>>>>>
>>>>>> Consider this C code:
>>>>>>
>>>>>> #include <stdbool.h>
>>>>>>
>>>>>> bool func(int n1, int n2, bool b) {
>>>>>>     bool greater = n1 > n2;
>>>>>>     if (greater && b) {
>>>>>>         if (n1 == n2) {
>>>>>>             return false; // unreachable
>>>>>>         }
>>>>>>     }
>>>>>>     return true;
>>>>>> }
>>>>>>
>>>>>> The line marked unreachable cannot be reached, however currently LLVM
>>>>>> does not optimize it out
>>>>>
>>>>> ?????
>>>>> Yes it does.
>>>>>
>>>>
>>>> It seems like we get this almost by accident though. I find that I need
>>>> `-mem2reg -instcombine -simplifycfg -instcombine` (on clang -O0 IR; the
>>>> `-mem2reg -instcombine` are just cleanup) and essentially it boils down to
>>>> simplifycfg merging everything into a single branch-free expression and
>>>> then instcombine algebraically merging the comparisons.
>>>>
>>>> A small modification defeats LLVM's optimizer:
>>>>
>>>> bool func(int n1, int n2, bool b) {
>>>>     bool greater = n1 > n2;
>>>>     if (greater && b) {
>>>>         foo();
>>>>
>>>>         if (n1 == n2) {
>>>>             return false; // unreachable
>>>>         }
>>>>     }
>>>>     return true;
>>>> }
>>>>
>>>> In this case, simplifycfg doesn't go wild merging everything into a
>>>> single branch-free expression and so we don't get it.
>>>>
>>>>
>>>> CorrelatedValuePropagation doesn't get this because its processCmp is
>>>> quite weak (it bails out if one operand isn't a constant). JumpThreading is
>>>> the only other pass that uses LazyValueInfo and it can't fold this since it
>>>> can't thread a jump around the side-effecting `foo()` call.
>>>>
>>>> I'm not familiar with GVN but it doesn't seem to help for this modified
>>>> test case either.
>>>>
>>>> Carlos, in answer to your original question, you may want to see if you
>>>> can make LLVM get this case by modifying processCmp in
>>>> lib/Transforms/Scalar/CorrelatedValuePropagation.cpp
>>>>
>>>> -- Sean Silva
>>>>
>>>>
>>>>> [dannyb at dannyb-macbookpro3 18:39:18] ~/sources/llvm
>>>>> (git-svn)-[newgvn-predicates]- :( $ clang -c -emit-llvm ~/greater.c -O1
>>>>> [dannyb at dannyb-macbookpro3 18:39:22] ~/sources/llvm
>>>>> (git-svn)-[newgvn-predicates]- :) $ debug-build/bin/llvm-dis greater.bc
>>>>> [dannyb at dannyb-macbookpro3 18:39:24] ~/sources/llvm
>>>>> (git-svn)-[newgvn-predicates]- :) $ cat greater.ll
>>>>> ; Function Attrs: norecurse nounwind readnone ssp uwtable
>>>>> define zeroext i1 @func(i32, i32, i1 zeroext) #0 {
>>>>>   ret i1 true
>>>>> }
>>>>>
>>>>>
>>>>> opt -simplifycfg -instcombine does the same thing to it if you use -O0
>>>>> with clang
>>>>>
>>>>>>
>>>>>
>>>>> I believe this is because LLVM does not recognize that meeting path
>>>>>> conditions like, for example, X && Y logically means that X is true and Y
>>>>>> is true.
>>>>>>
>>>>>
>>>>>
>>>>> Yes it does. See both GVN's propagateequality and
>>>>> correlatedvaluepropagation, among other things :)
>>>>>
>>>>> In this case, simplifycfg +instcombine will do it
>>>>>
>>>>> The new predicate support i'm building for GVN will also do it.
>>>>>
>>>>>
>>>>>>
>>>>>> I'm interested in creating a patch to remedy this; is there a file or
>>>>>> function I should look at?
>>>>>>
>>>>>> Thanks in advance.
>>>>>>
>>>>>>  - CL
>>>>>> _______________________________________________
>>>>>> LLVM Developers mailing list
>>>>>> llvm-dev at lists.llvm.org
>>>>>> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
>>>>>>
>>>>>
>>>>>
>>>>> _______________________________________________
>>>>> LLVM Developers mailing list
>>>>> llvm-dev at lists.llvm.org
>>>>> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
>>>>>
>>>>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20160701/04abc7e9/attachment.html>


More information about the llvm-dev mailing list