<div dir="ltr">Right.<div>Like a lot of things, it was probably reasonably assumed this would just work.</div><div><br></div><div>It's take a lot of years to find cases where that's not true.</div><div><br></div><div>While it would have been super nice if, when this was added, folks sat down and thought very hard about the theory behind it and prove it would work, that doesn't always (or often :P) happen.</div><div><br></div><div><br></div><div>Here, it's, sadly, pretty easy to prove it can't work:</div><div><br></div><div>The solver follows chains until the lattice values stop changing.</div><div>The end state is one where things have the "best" lattice value they can.</div><div><br></div><div>Because we use unknown to mean two different things (unprocessed, and undef), it means it does not resolve some things.</div><div>That by itself is okay.</div><div><br></div><div>However, what happens next is two fold:<br><br></div><div>1. At the point the solver finishes, it expects unknown means undef</div><div>2. The iteration order of the resolver is not the same as the solver (IE it walks basic blocks, it does not propagate from defs to uses).</div><div><br></div><div>These two things combine.</div><div><br>Because it iterates in an order not guaranteed to process defs before uses (because it's iterating over *basic blocks* and in *function order* instead of *the ssa graph*, and in *def->use* order) it hits the branch condition use before the branch condition def.</div><div>It then uses #1 to assume that unknown there means undef. But it could just mean "the solver could not resolve this", which is *not* the same as undef.</div><div><br></div><div>For those having trouble following this:</div><div><br></div><div>The solver processs</div><div><br></div><div>%a = or true, undef</div><div><in some other basic block><br>branch %a</div><div><br></div><div>in order of: %a, branch</div><div><br></div><div>The resolver</div><div>may process it as</div><div>branch, %a.</div><div><br></div><div>At the point it sees the branch, it thinks anything marked "unknown" (like %a") is really "undef".</div><div>It's not.</div><div>It's really "unknown" :)</div><div><br></div><div>If the resolver processed it as</div><div>%a, branch</div><div>it would do the "right" thing.</div><div> </div><div>So if you fixed the iteration order, you'd have a much better chance of making it work in the face of #1, but i'm pretty sure, at a minimum, where there are cycles, you can still prove it will break.</div><div><br></div><div>IMHO, it's easier to just distinguish between unknown and undef, *and* move the real work back into the meet/etc of the propagation engine, so that the iteration order is fixed as well.</div><div><br></div><div>(so, yeah, you could also fix this bug by making resolve undefs do the same exact propagation ordering as the solver, *and* by fixing #1. But i'm suggesting it's easier to just integrate most of this work into the solver instead of trying to have two parallel pieces of code have a lockstep ordering of propagation).</div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Nov 9, 2016 at 11:31 AM, David Majnemer <span dir="ltr"><<a href="mailto:david.majnemer@gmail.com" target="_blank">david.majnemer@gmail.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"><br><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="h5">On Wed, Nov 9, 2016 at 11:16 AM, Davide Italiano via llvm-commits <span dir="ltr"><<a href="mailto:llvm-commits@lists.llvm.org" target="_blank">llvm-commits@lists.llvm.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="m_-4911908598339333510HOEnZb"><div class="m_-4911908598339333510h5">On Wed, Nov 9, 2016 at 9:49 AM, Daniel Berlin via llvm-commits<br>
<<a href="mailto:llvm-commits@lists.llvm.org" target="_blank">llvm-commits@lists.llvm.org</a>> wrote:<br>
> Actually, digging further into it, I don't understand how this fixes it at<br>
> all, and your test does nothing because it's all CHECK's :-)<br>
><br>
> The example given in the bug report is or true, undef<br>
><br>
> ResolveUndefs already does the right thing for this, and does not consider<br>
> the result undef.<br>
><br>
> The propagation order makes it impossible for that to happen, because in<br>
> reality, undef is a set of lattice values but not represented in the<br>
> lattice, and resolveUndefs is trying to figure out the lattice values that<br>
> work.<br>
><br>
> That's ... never going to work, as you've discovered (and eli suspects on<br>
> the bug report).<br>
><br>
> I suspect pretty much every part of markForcedConstant is vulnerable to this<br>
> undef different circumstances.<br>
><br>
> Realistically, undef needs to be an actual lattice value lower than unknown<br>
><br>
> That way, or undef, true comes out true during *solving*.<br>
> The parts of resolveundefs handling this need to be made part of the meet<br>
> operation<br>
><br>
> This handles the case where undef must be constrained (IE or undef, true).<br>
><br>
> After solving is finished, anything left as undef can then be filled in<br>
> unconstrained, because you are guaranteed it is not forced to a certain<br>
> value (or that your solver sucks :P)<br>
><br>
> (note that in the freeze/poison proposal, this should just work because the<br>
> freezes will be different ssa names)<br>
><br>
<br>
</div></div>Uh, thanks. Out of curiosity, do you happen to know why undef wasn't<br>
represented as a lattice value from the beginning (and instead we end<br>
up trying values that match up?) Is there a particular reason (e.g.<br>
efficiency)? I can't think of one.<br></blockquote><div><br></div></div></div><div>Our SCCP code dates back to 2001, undef arrived in 2004.</div><span class="HOEnZb"><font color="#888888"><div> </div></font></span><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="HOEnZb"><font color="#888888">
--<br>
Davide</font></span><span class=""><br>
<div class="m_-4911908598339333510HOEnZb"><div class="m_-4911908598339333510h5">______________________________<wbr>_________________<br>
llvm-commits mailing list<br>
<a href="mailto:llvm-commits@lists.llvm.org" target="_blank">llvm-commits@lists.llvm.org</a><br>
<a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-commits" rel="noreferrer" target="_blank">http://lists.llvm.org/cgi-bin/<wbr>mailman/listinfo/llvm-commits</a><br>
</div></div></span></blockquote></div><br></div></div>
</blockquote></div><br></div>