<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Feb 4, 2015 at 11:24 AM, John Regehr <span dir="ltr"><<a href="mailto:regehr@cs.utah.edu" target="_blank">regehr@cs.utah.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><span><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
I am actively working towards removing poison altogether.  I think a more accurate model of LLVM's wrapping<br>
flags is not poison but instead something akin to the fast-math flags on floating point instructions.<br>
</blockquote>
<br></span>
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.</blockquote><div><br></div><div>Turns out that undef + fast math flags is enough to cause LLVM to become inconsistent:<br></div><div><div>define i1 @f(i1 %a.is_nan, float %a, float %b) {</div><div>  %add = fadd nnan float %a, %b</div><div>  %sel = select i1 %a.is_nan, float undef, float %add</div><div>  %cmp = fcmp ord float %b, %sel</div><div>  ret i1 %cmp</div><div>}</div><br class="">When 'b' is NaN, the following occurs:</div><div>%add = float undef</div><div>%sel = float undef</div><div>%cmp = i1 false</div><div><br></div><div>However, the 'select i1 %A, %B, undef' -> 'undef' optimization permits us to transform @f to:</div><div>define i1 @f(i1 %a.is_nan, float %a, float %b) {<br></div><div><div>  %add = fadd nnan float %a, %b</div><div>  %cmp = fcmp ord float %add, 0.000000e+00</div><div>  ret i1 %cmp</div><div>}</div></div><div><br></div><div>Now we will have:</div><div>%add = float undef</div><div>%cmp = i1 undef</div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><span><font color="#888888"><br>
<br>
John</font></span></blockquote></div><br></div></div>