<div dir="ltr"><div><div><div><div><div><div>Hi John,<br><br>More background is in this post (at which time "poison" was still named "trap") (and I apologize for the verbosity) [0]<br><br>[0] <a href="http://lists.cs.uiuc.edu/pipermail/llvmdev/2011-November/045730.html">http://lists.cs.uiuc.edu/pipermail/llvmdev/2011-November/045730.html</a><br></div><br>The poison concept aimed to<br></div><div>  (a) enable the sign-extension elimination optimization<br></div><div>  (b) permit arbitrary speculation that doesn't destroy any optimization opportunities<br></div><div><br></div><div>Undef does (b) but not (a). Immediate UB does (a) but not (b). Additionally, here are some interesting debatable requirements:<br></div><br></div></div>  - Select(a, b, c) should be semantically equivalent to (sext(a) & b)|(~sext(a) & c) (with appropriate bitcasting).<br>  - Select should be semantically equivalent to its intuitive translation as a branch and a phi (the current poison concept violates 
this)<br></div><div>  - Branch should be semantically equivalent to its intuitive translation as a switch, and as an indirect branch<br>  - Constant folding, mem2reg, and reg2mem should always be safe *and* optimization-opportunity-preserving<br><br></div><div><div>I personally suggest a compromise on the optimization, and instead a focus on helping programmers write better code. C++11 range-based for loops are easier for humans to read, and in some cases avoid ol' "int" to step through arrays. Quoting the Zen of Python, "let's do more of those!"<br></div><br></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Sep 11, 2014 at 7:17 PM, 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:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Poison is a flawed concept. I proved it was flawed back in 2011 [0]<br>
</blockquote>
<br></span>
Nice. My colleagues and I will dig through this material and possibly come back with some ideas. We're going to need some sort of semantics for UB in LLVM since otherwise these formal-methods-based tools like Souper and Alive risk not making sense.<div class="HOEnZb"><div class="h5"><br>
<br>
Thanks,<br>
<br>
John<br>
______________________________<u></u>_________________<br>
LLVM Developers mailing list<br>
<a href="mailto:LLVMdev@cs.uiuc.edu" target="_blank">LLVMdev@cs.uiuc.edu</a>         <a href="http://llvm.cs.uiuc.edu" target="_blank">http://llvm.cs.uiuc.edu</a><br>
<a href="http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev" target="_blank">http://lists.cs.uiuc.edu/<u></u>mailman/listinfo/llvmdev</a><br>
</div></div></blockquote></div><br></div>