<div dir="ltr"><div dir="ltr">On Tue, Sep 14, 2021 at 10:15 PM Arthur O'Dwyer <<a href="mailto:arthur.j.odwyer@gmail.com">arthur.j.odwyer@gmail.com</a>> wrote:<br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div dir="ltr">On Tue, Sep 14, 2021 at 9:22 AM Serge Pavlov via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org" target="_blank">cfe-dev@lists.llvm.org</a>> wrote:<br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div dir="ltr">On Tue, Sep 14, 2021 at 8:21 PM Krzysztof Parzyszek <<a href="mailto:kparzysz@quicinc.com" target="_blank">kparzysz@quicinc.com</a>> wrote:<br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div lang="EN-US">
<div>
<p class="MsoNormal" style="margin-left:0.5in">If `has_nan` returns "true", it means that the explanation "there are no NaNs" does not work anymore and something more complex is needed to explain the effect of the option. In this case it is difficult to say
that this approach is "intuitively clear".<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">If your program has “x = *p”, it means that at this point p is never a null pointer. Does this imply that the type of p can no longer represent a null pointer?</p></div></div></blockquote><div><br></div><div>Good example! If you use integer division `r = a / b`, you promise that `b` is not zero. It however does not mean that preceding check `b == 0` may be optimized to `false`.</div></div></div></blockquote><div><br></div><div>In C and C++, it actually <i><b>does</b></i> mean that, although of the compilers I just tested on Godbolt, only MSVC seems to take advantage of that permission.</div><div><a href="https://godbolt.org/z/11ss5T7e8" target="_blank">https://godbolt.org/z/11ss5T7e8</a></div></div></div></blockquote><div><br></div><div>But this is the *following* check, not preceding. </div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div class="gmail_quote"><div><br></div><div>The question of whether it is acceptable to treat as equivalent the statements "p is known to be dereferenced in all successors of B" and "p is known to be non-null in B," was discussed extensively about 20 years ago, and then again 12 years ago when it bit someone in the Linux kernel:</div><div><a href="https://www.gnu.org/software/gcc/news/null.html" target="_blank">https://www.gnu.org/software/gcc/news/null.html</a><br></div><div><a href="https://lwn.net/Articles/342330/" target="_blank">https://lwn.net/Articles/342330/</a><br></div><div><a href="https://lwn.net/Articles/342420/" target="_blank">https://lwn.net/Articles/342420/</a><br></div><div><a href="https://qinsb.blogspot.com/2018/03/ub-will-delete-your-null-checks.html" target="_blank">https://qinsb.blogspot.com/2018/03/ub-will-delete-your-null-checks.html</a><br></div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div lang="EN-US"><div><div><div><div><div><p class="MsoNormal">On Mon, Sep 13, 2021 at 10:28 PM Arthur O'Dwyer <<a href="mailto:arthur.j.odwyer@gmail.com" target="_blank">arthur.j.odwyer@gmail.com</a>> wrote: </p></div><blockquote style="border-top:none;border-right:none;border-bottom:none;border-left:1pt solid rgb(204,204,204);padding:0in 0in 0in 6pt;margin-left:4.8pt;margin-right:0in"><div><div><p class="MsoNormal"><u></u></p>
</div>
<div>
<div>
<p class="MsoNormal">Btw, I don't think this thread has paid enough attention to Richard Smith's suggestion:</p></div></div></div></blockquote>
<div>
<p class="MsoNormal">I can only subscribe to James Y Knight's opinion. Indeed, it can be a good criterion of which operations should work in finite-math-only mode and which can not work. The only thing which I worry about is the possibility of checking the
operation result for infinity (and nan for symmetry). But the suggested criterion is formulated in terms of arguments, not results, so it must allow such checks.</p></div></div></div></div></div></div></blockquote></div></div></blockquote><div><br></div><div><i><b>What</b></i> is the opinion to which you subscribe?</div></div></div></blockquote><div><br></div><div>I mean this post:</div><div><br></div><div><div dir="ltr" class="gmail_attr">On Fri, Sep 10, 2021 at 9:29 PM James Y Knight via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div dir="auto"><div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Sep 9, 2021, 8:59 PM Richard Smith via llvm-dev <<a href="mailto:llvm-dev@lists.llvm.org" rel="noreferrer" target="_blank">llvm-dev@lists.llvm.org</a>> wrote:</div></div></div><div dir="auto"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div class="gmail_quote"><div>Would it be reasonable to treat operations on Inf and NaN values as UB in this mode only if the same operation on a signaling NaN might signal? (Approximately, that'd mean we imagine these non-finite value encodings all encode sNaNs that are UB if they would signal.) That means the operations that ISO 60559 defines as non-computational or quiet-computational would be permitted to receive NaN and Inf as input and produce them as output, but that other computational operations would not.</div><div><br></div><div>Per ISO 60559, the quiet-computational operations that I think are relevant to us are: copy, negate, abs, copySign, and conversions between encoding (eg, bitcast). The non-computational operations that I think are relevant to us are classification functions (including isNaN).</div><div></div></div></div></blockquote></div></div><div dir="auto"><br></div><div dir="auto">I'm in favor. (Perhaps unsurprisingly, as this is precisely the proposal I made earlier, worded slightly differently. :)</div></div></div></blockquote></div><div> </div><div>Sorry for the unclear statement.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div class="gmail_quote"><div><br></div><div>Anyway, Richard's "quiet is signaling and signals are unspecified values" is really the only way out of the difficulty, as far as compiler people are concerned. You two (Serge and Krzysztof) can keep talking past each other at the application level, but the compiler people are going to have to do <i>something</i> in the code eventually, and that <i>something</i> is going to have to be expressed in terms similar to what Richard and I have been saying, because these are the terms that the compiler understands.</div><div><br></div></div></div></blockquote><div> </div><div>Glad to hear it. If we decide to implement Richard's approach, I will put back the patches that implement `llvm.isnan` and continue implementing other similar intrinsics. Clang needs missing `__builtin_*` intrinsics, they should be mapped into the new llvm intrinsics. Not sure when the user's manual should be updated, now or after the desired behavior will be implemented.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div class="gmail_quote"><div></div><div>Thanks,</div><div>Arthur</div></div></div>
</blockquote></div></div>