<div dir="ltr">On Thu, Aug 22, 2013 at 7:10 PM, Nick Lewycky <span dir="ltr"><<a href="mailto:nlewycky@google.com" target="_blank">nlewycky@google.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr"><div><div class="h5">But I'm not sure that we should use nsw to fix this, in spite of the fact that this is exactly what nsw was designed for. We know the answer even for the unsigned case, and we should just use that. Add a new SCEV node which lets us return that it's infinite in this case, and trip count X in the other; along the lines of "SCEVPotentiallyInfinite(m > int_max-3, sdiv(m, 4))".<br>
</div></div></div>
</blockquote><div><br></div><div>I think SCEV should use nsw when possible (that's exactly what the flag is for, as you've said). For unsigned cases, "potentially infinite" sounds reasonable, but transforms will have to be updated to handle it. E.g. for vectorization infinite loop is probably OK to vectorize. For closed form computation a check will have to be inserted.</div>
<div><br></div><div>Another thought is that we can prove this particular loop is finite even if i was unsigned. It has *a++ in the body. If a is infinitely incremented the dereference will, at some point, cause undefined behavior.</div>
<div><br></div><div>Eugene<br></div></div>