<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Wed, Apr 30, 2014 at 7:16 PM, Jordan Rose <span dir="ltr"><<a href="mailto:jordan_rose@apple.com" target="_blank">jordan_rose@apple.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><br><div><div class=""><div>On Apr 30, 2014, at 1:35 , Manuel Klimek <<a href="mailto:klimek@google.com" target="_blank">klimek@google.com</a>> wrote:</div>
<br><blockquote type="cite"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Wed, Apr 30, 2014 at 5:34 AM, Jordan Rose <span dir="ltr"><<a href="mailto:jordan_rose@apple.com" target="_blank">jordan_rose@apple.com</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">What this is basically saying is that we will never be in a situation where the condition (or the rightmost branch in the condition) was not evaluated in the current CFG block. That seems a bit questionable in general but reasonable given the way the CFG is currently constructed.</blockquote>

<div><br></div><div>Well, all I've been trying to do here is to a) document and b) encode in the assert the actual current CFG invariant the analyzer relies on for correctness.</div><div>The problem is that if what is returned from ResolveCondition is *not* evaluated in the block, we have no guarantee that it was evaluated at all - but the correctness of all the path analyses relies on it being in the SVal cache of the state. Otherwise we will assume branches are reachable that are clearly unreachable because of which parts of the logical operator tree we *assumed* to be true (so we know the condition must be statically knowable in the current state).</div>

<div><br></div><div>I have a hard time putting that into words though, so any help for how to wordsmith this to be easier to understand would be highly appreciated...</div></div></div></div></blockquote><div><br></div></div>
<div>"in the SVal cache of the state" is "in the Environment" using analyzer terminology (it's not really a cache, since it's not reproducible)</div></div></div></blockquote><div><br></div><div>
exactly :) I learned that today while doing more digging through the code...</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><div>, but since things regularly get cleaned <i>out</i> of the Environment there aren't that many cases where a condition would be present but wouldn't have been evaluated in the previous block.</div></div></div>
</blockquote><div><br></div><div>I don't yet understand how exactly things get cleaned out of the environment (other than losing scope).</div><div>It seems to me like a lot of the warnings rely on branch conditions always being in the environment at the point of the terminator, otherwise it's easy to produce false positives in unreachable code paths.</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><div>As I understand it, the actual purpose of ResolveCondition is that when your branch condition is a BinaryOperator, you might not have bothered to evaluate the BinaryOperator expression itself, but if not you definitely would have evaluated its RHS. (Testing <i>without</i> ResolveCondition, this happens when you have chained logical operators "a || b || c", because we don't stop to evaluate the entire "a || b" expression when deciding whether to get to "c". We know we wouldn't have gotten to this point if we hadn't evaluated the RHS.)</div>
</div></div></blockquote><div><br></div><div>Exactly.</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><div>Looking at Ted's original patch, it looks like some constructs will still stop to evaluate the expression before using it as a condition, so if the last statement in the CFG really does happen to be the whole logical expression, we can use it as a condition directly.</div>
<div><br></div><div>...hm, that's still not so clearly worded!</div></div></div></blockquote><div><br></div><div>:) I can just check in the current version, seems better than not having any documentation, and I think it's factually right (if not perfectly worded)...</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><div class=""><div><br></div><blockquote type="cite"><div dir="ltr">
<div class="gmail_extra"><div class="gmail_quote"><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
(Especially if/when this whole block of code can go away!)<br></blockquote><div><br></div><div>I'm not sure what you mean about "this whole block of code can go away". The only part that will go away is the special case handling for temporary dtor terminators, as those will be handled in a completely different code path.</div>
</div></div></div></blockquote><br></div></div><div>Ah, you're right. The code is there to handle a logical expressions being used as conditions, and that's not going away. It took me a long time to understand that this comment:</div>
<div><br></div><div>  // For logical operations, we still have the case where some branches<br>  // use the traditional "merge" approach and others sink the branch<br>  // directly into the basic blocks representing the logical operation.<br>
  // We need to distinguish between those two cases here.<br><br></div><div>refers to the "some constructs will still evaluate the expression before using it as a condition" I said above.</div><span class="HOEnZb"><font color="#888888"><div>
<br></div><div>Jordan</div></font></span></div></blockquote></div><br></div></div>