On Wed, Feb 4, 2015 at 11:24 AM, John Regehr <regehr at cs.utah.edu> wrote:> I am actively working towards removing poison altogether. I think a more >> accurate model of LLVM's wrapping >> flags is not poison but instead something akin to the fast-math flags on >> floating point instructions. >> > > Looking forward to seeing it. One of my students has a hacked lli that > tracks poison, it's a nice playground for trying to understand the > interaction of poison with programs and with LLVM passes. We can hopefully > implement your new semantics as an option in order to better understand it. > In one way, the hacked lli is not as good as Alive (it only reasons about > one execution at a time) but on the other hand it tells us what happens for > real codes which Alive does not.Turns out that undef + fast math flags is enough to cause LLVM to become inconsistent: define i1 @f(i1 %a.is_nan, float %a, float %b) { %add = fadd nnan float %a, %b %sel = select i1 %a.is_nan, float undef, float %add %cmp = fcmp ord float %b, %sel ret i1 %cmp } When 'b' is NaN, the following occurs: %add = float undef %sel = float undef %cmp = i1 false However, the 'select i1 %A, %B, undef' -> 'undef' optimization permits us to transform @f to: define i1 @f(i1 %a.is_nan, float %a, float %b) { %add = fadd nnan float %a, %b %cmp = fcmp ord float %add, 0.000000e+00 ret i1 %cmp } Now we will have: %add = float undef %cmp = i1 undef> > > John-------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20150204/5727d4d5/attachment.html>
> Turns out that undef + fast math flags is enough to cause LLVM to become > inconsistent: > define i1 @f(i1 %a.is_nan, float %a, float %b) { > %add = fadd nnan float %a, %b > %sel = select i1 %a.is_nan, float undef, float %add > %cmp = fcmp ord float %b, %sel > ret i1 %cmp > } > > When 'b' is NaN, the following occurs: > %add = float undef > %sel = float undef > %cmp = i1 false > > However, the 'select i1 %A, %B, undef' -> 'undef' optimization permits us toHow can you transform 'select X, Y, undef' to undef? What if X is true? Did you mean 'select X, undef, undef' -> undef?> transform @f to: > define i1 @f(i1 %a.is_nan, float %a, float %b) { > %add = fadd nnan float %a, %b > %cmp = fcmp ord float %add, 0.000000e+00I don't see how you got here -- %cmp was "fcmp ord float %b, %sel". Now %b is NaN so %add is undef, making %cmp = "fcmp ord NaN, undef" which is false for any value of undef. Maybe I'm being thick, but I think it will help if you break down the second half of your argument into smaller steps. :) Having said that I won't be surprised if fast-math flags suffer from issues similar to poison -- "Allow algebraically equivalent transformations that may dramatically change results in floating point" sounds somewhat vague to me. -- Sanjoy> ret i1 %cmp > } > > Now we will have: > %add = float undef > %cmp = i1 undef > > >> >> >> >> John > > > > _______________________________________________ > LLVM Developers mailing list > LLVMdev at cs.uiuc.edu http://llvm.cs.uiuc.edu > http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev >
On Wed, Feb 4, 2015 at 5:47 PM, Sanjoy Das <sanjoy at playingwithpointers.com> wrote:> > Turns out that undef + fast math flags is enough to cause LLVM to become > > inconsistent: > > define i1 @f(i1 %a.is_nan, float %a, float %b) { > > %add = fadd nnan float %a, %b > > %sel = select i1 %a.is_nan, float undef, float %add > > %cmp = fcmp ord float %b, %sel > > ret i1 %cmp > > } > > > > When 'b' is NaN, the following occurs: > > %add = float undef > > %sel = float undef > > %cmp = i1 false > > > > However, the 'select i1 %A, %B, undef' -> 'undef' optimization permits > us to > > How can you transform 'select X, Y, undef' to undef? What if X is > true? Did you mean 'select X, undef, undef' -> undef? >Sorry, I meant 'select X, Y, undef' to 'Y'> > > transform @f to: > > define i1 @f(i1 %a.is_nan, float %a, float %b) { > > %add = fadd nnan float %a, %b > > %cmp = fcmp ord float %add, 0.000000e+00 > > I don't see how you got here -- %cmp was "fcmp ord float %b, %sel". > Now %b is NaN so %add is undef, making %cmp = "fcmp ord NaN, undef" > which is false for any value of undef. >Just to be clear, I agree. This is why I said that %cmp = i1 false in the untransformed @f.> > Maybe I'm being thick, but I think it will help if you break down the > second half of your argument into smaller steps. :) >We start with: define i1 @f(i1 %a.is_nan, float %a, float %b) { %add = fadd nnan float %a, %b %sel = select i1 %a.is_nan, float undef, float %add %cmp = fcmp ord float %b, %sel ret i1 %cmp } LLVM (currently) permits 'select i1 %a.is_nan, float undef, float %add' to turn into '%add', this leaves us with: define i1 @f(i1 %a.is_nan, float %a, float %b) { %add = fadd nnan float %a, %b %cmp = fcmp ord float %b, %add ret i1 %cmp } 'fadd nnan' claims that it is allowed to assume that its operands can't be NaN and that those which value depend on the value will not get NaN. I believe this would let 'fcmp' assume that it only needs to look at the result of '%add': define i1 @f(i1 %a.is_nan, float %a, float %b) { %add = fadd nnan float %a, %b %cmp = fcmp ord float 0., %add ret i1 %cmp }> Having said that I won't be surprised if fast-math flags suffer from > issues similar to poison -- "Allow algebraically equivalent > transformations that may dramatically change results in floating > point" sounds somewhat vague to me. > > -- Sanjoy > > > ret i1 %cmp > > } > > > > Now we will have: > > %add = float undef > > %cmp = i1 undef > > > > > >> > >> > >> > >> John > > > > > > > > _______________________________________________ > > LLVM Developers mailing list > > LLVMdev at cs.uiuc.edu http://llvm.cs.uiuc.edu > > http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev > > >-------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20150204/bca71788/attachment.html>
> Having said that I won't be surprised if fast-math flags suffer from > issues similar to poison -- "Allow algebraically equivalent > transformations that may dramatically change results in floating > point" sounds somewhat vague to me.The vaguenss should be expected since nobody seems to know what "gcc -ffast-math" or "clang -ffast-math" mean at the source level either. John