[LLVMdev] Proposal for Poison Semantics

[David Majnemer]

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>