llvm dev - Feb 2015 - [LLVMdev] Proposal for Poison Semantics

On Wed, Feb 4, 2015 at 9:13 AM, John Regehr <regehr at cs.utah.edu> wrote:
> I think such a thing would be great.  However, there is a problem that the
>> RFC wasn't aware of when it was
>> written:
>>
>> consider:
>> %S = select %A, %B, undef
>>
>> without us knowing anything about %A or %B, we will replace all uses of
>> %S with %B.  This transform would be
>> considered wrong with the RFC in mind.
>>
>> If this transform was valid, there could not be any value or value-like
>> property in LLVM with semantics more
>> powerful than undef.  This makes me think that what LLVM *actually*
>> implements is not poison or something like
>> it.
>>
>
> Is it possible that the new weaker poison subsumes undef?  The interaction
> between these different but related UB-like concepts is confusing at best.

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.

>
>
> John
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20150204/a8dbeecb/attachment.html>

> 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.

John

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>