<div dir="ltr"><div class="gmail_quote"><div dir="ltr">On Wed, Jun 28, 2017 at 12:09 PM Peter Lawrence <<a href="mailto:peterl95124@sbcglobal.net">peterl95124@sbcglobal.net</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">Chandler,<div>                Please give some citations, I’ve search the llvm-dev archives and didn't find any.</div></div></blockquote><div><br></div><div>They are all in the discussions from Nuno, Sanjoy, John and others around poison semantics. I won't be able to find the citations any easier than you, I simply wanted to point out that rather than conclude this is novel, you should probably ask folks who have participated in these discussions for reference points that they may have.</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div><br></div><div>Peter Lawrence.</div></div><div style="word-wrap:break-word"><div><br></div><div><br><div><blockquote type="cite"><div>On Jun 28, 2017, at 12:01 PM, Chandler Carruth <<a href="mailto:chandlerc@gmail.com" target="_blank">chandlerc@gmail.com</a>> wrote:</div><br class="m_-5225391038052294040Apple-interchange-newline"><div><div dir="ltr"><div class="gmail_quote"><div dir="ltr">On Wed, Jun 28, 2017 at 9:39 AM Peter Lawrence <<a href="mailto:peterl95124@sbcglobal.net" target="_blank">peterl95124@sbcglobal.net</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div dir="auto" style="word-wrap:break-word"><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><div style="margin:0px;line-height:normal;min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;line-height:normal"><span style="font-variant-ligatures:no-common-ligatures">Preface: This paper shows that "poison" was never actually necessary</span></div><div style="margin:0px;line-height:normal"><span style="font-variant-ligatures:no-common-ligatures">in the first place. “Poison"</span>s existence is based on incorrect assumptions </div><div style="margin:0px;line-height:normal"><span style="font-variant-ligatures:no-common-ligatures">that are being explored for the first time.</span></div></div></div></div></blockquote><div><br></div><div>Just so you are aware, there have been numerous people in the community who have been exploring the issues you bring up for many years. So I don't think it is correct to say that they are being explored for the first time.</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div dir="auto" style="word-wrap:break-word"><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><div style="margin:0px;line-height:normal;min-height:16px"><br></div><div style="margin:0px;line-height:normal;min-height:16px"><br></div><div style="margin:0px;line-height:normal;min-height:16px"><br></div></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">I have been re-reading Dan Gohman's original post "the nsw story" [1]</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">and have come to the conclusion that Dan got it wrong in some respects.</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">He came up with "no signed wrap" ("nsw") which in his words means</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">"The purpose of the nsw flag is to indicate instructions which are</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">known to have no overflow".  The key operative word here is "known".</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">This means literally an operation with an additional "llvm.assume".</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">For example    (a +nsw b)    when a and b are i32   is really</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">  ((llvm.assume((INT_MIN <= ((i64)a+(i64)b) <= INT_MAX) , (a + b))</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">It is this "assume" that justifies the transformation that Dan does</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">to optimize sign-extension of i32 induction variables out of loops</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">on LP64 targets.  So far so good.</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">Note that there is no "undef" in the IR either before or after the</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">transform, this doesn't just fall out because of a clever definition</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">of IR "undef".</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">Note that even the concept of "undefined" never enters into the </span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">justification, only that "nsw" ==> "assume" ==> the loop iteration</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">bounds don't wrap ==> i64 arithmetic will generate the exact same</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">iterations as i32 arithmetic ==> the induction variable can be</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">promoted ==> there is no longer any sign-extend inside the loop.</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">Note that clang can generate "+nsw" for signed “+" regardless</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">of whether the precise C standard wording is "undefined behavior"</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">or more simply "unspecified value"</span>.</div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">Where Dan goes wrong is in thinking that "+nsw" is an operation</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">rather than an operation with an assume, and therefore he feels</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">the need to define what the result of this operation is when it</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">overflows, which then seems to require a new "poison" instruction</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">because "undef" isn't good enough.</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">But there is no need to ask what the result of overflow is</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">because "+nsw" is like a "+" inside of an if-statement whose</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">condition precludes overflow, and if it can't overflow then</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">asking about it is a non sequitor.</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">And speculatively hoisting the "+nsw" doesn't cause problems</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">because hoisting a "+nsw" is like taking a "+" outside of the</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">if-statement that guarantees no overflow, it is then simply</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">a plain old un-attributed "+" operation which has no undefined</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">behavior.</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">Dan's follow on email "nsw is still inconsistent" [2] shows by</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">example why it is illegal to hoist the "nsw" attribute along </span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">with the "+" operation.</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">It therefore makes no sense to discuss the result of "+nsw" as</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">ever being either "undef" or "poison", and so the need for "poison"</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">is gone.</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">Here's what Dan thought at the time about this "poison" creation</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><div style="margin:0px;line-height:normal;min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;line-height:normal"><span style="font-variant-ligatures:no-common-ligatures">        "I wrote up a description of this concept, and it's been in</span></div><div style="margin:0px;line-height:normal"><span style="font-variant-ligatures:no-common-ligatures">        LangRef ever since. It sticks out though, because it got pretty</span></div><div style="margin:0px;line-height:normal"><span style="font-variant-ligatures:no-common-ligatures">        big and complex, especially in view of its relative obscurity.</span></div><div style="margin:0px;line-height:normal"><span style="font-variant-ligatures:no-common-ligatures">        Realistically speaking, it's probably not fully watertight yet."</span></div></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">I agree with Dan here "it's probably not fully watertight yet", and</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">apparently other folks agree because yet another instruction,</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">"freeze", is being proposed to fix "poison"s problems.  My guess</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">is that "freeze is probably not fully watertight yet" either, but</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">since "poison" isn't needed it is time to delete it from the LangRef,</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">and we can therefore stop considering "freeze".</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">Peter Lawrence.</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">References</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">[1. llvm-dev, Dan Gohman, Tue Nov 29 15:21:58 PST 2011 ]</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255)"><span style="font-variant-ligatures:no-common-ligatures">[2. llvm-dev, Dan Gohman, Mon Dec 12 12:58:31 PST 2011 ]</span></div><div style="margin:0px;font-size:14px;line-height:normal;font-family:Menlo;background-color:rgb(255,255,255);min-height:16px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div></div></div></blockquote></div></div>
</div></blockquote></div><br></div></div></blockquote></div></div>