<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Mon, May 5, 2014 at 2:55 PM, Manuel Klimek <span dir="ltr"><<a href="mailto:klimek@google.com" target="_blank">klimek@google.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">
<div class="">On Thu, May 1, 2014 at 6:27 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:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div style="word-wrap:break-word"><br><div><div><div>On Apr 30, 2014, at 10:23 , 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 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:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div style="word-wrap:break-word"><br><div><div><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:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style: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:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div style="word-wrap:break-word">
<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>
</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></div></blockquote><div><br></div></div><div>The presence of bindings in the Environment is controlled by the LiveVariables analysis. Essentially, an expression is live from the point of its evaluation to the point it is consumed.</div>
</div></div></blockquote><div><br></div></div><div>Can you elaborate on what "consumed" means in this context?</div><div class=""><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div style="word-wrap:break-word"><div><div> Unfortunately, it can be a little more complicated than that sometimes...especially with LiveVariables being a flow-sensitive analysis but not a path-sensitive one.</div></div>
</div></blockquote><div><br></div></div><div>What is the difference of flow vs. path sensitive analysis here?</div><div class=""><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div style="word-wrap:break-word"><div><div> (This is one of the reasons for the liveness bug that Pavel uncovered.)</div></div></div></blockquote><div><br></div></div><div>I'm not sure yet where there was a liveness bug - every instance of bug I've seen was due to expression not having yet been evaluated (due to the logical operator optimization that ResolveCondition relies on). I've not seen a case yet where an expression was removed from the Environment after it had been in. Do you have an example for that?</div>
</div></div></div></blockquote><div><br></div><div>To go into a little more details. Take this code:</div><div><div>void f() {</div><div> struct Dtor {</div><div> ~Dtor();</div><div> operator bool() const;</div><div>
};</div><div> extern bool coin();</div><div> if (coin() || coin() || Dtor()) {</div><div> }</div><div>}</div></div><div><br></div><div>It currently leads to this CFG:</div><div><div>void f()</div><div> [B8 (ENTRY)]</div>
<div> Succs (1): B7</div><div><br></div><div> [B1]</div><div> Preds (1): B2</div><div> Succs (1): B0</div><div><br></div><div> [B2]</div><div> T: if [B4.1]</div><div> Preds (2): B3 B4</div><div> Succs (2): B1 B0</div>
<div><br></div><div> [B3]</div><div> 1: ~Dtor() (Temporary object destructor)</div><div> Preds (1): B4</div><div> Succs (1): B2</div><div><br></div><div> [B4]</div><div> 1: [B7.3] || [B6.3] || [B5.6]</div><div> T: (Temp Dtor) [B7.3] || [B6.3] || ...</div>
<div><br></div><div>^^^^ This is the interesting part: The expression B7.3 || B6.3 has never been executed. The terminator B6.T, which references the same expression, only works because in that case ResolveCondition sees "oh, we're in a logical operator branch, so we already know we only need to look at B6.3". B6.3 has been executed and is in the environment, so everything is fine.</div>
<div><br></div><div>The problem is that we cannot just use the same shortcut logic to decide which temp destructors to execute - we actually need an evaluation of B7.3 || B6.3 to decide whether we need to go into B3 (because the temporary destructors are called in reverse order). B7.3 || B6.3 is never executed though, so it's not in the environment, so we assume both branches are always possible, even if it shouldn't be possible in the current Environment.</div>
<div><br></div><div>My current theory is that putting the condition statement that's needed to decide the branch in as statement right before the temp dtor terminator would fix this (but, alas, I don't fully understand this yet ;). In this case, it would be:</div>
<div>[B4]</div><div>1: [B7.3] || [B6.3] || [B5.6]</div><div>2: [B7.3] || [B6.3]</div><div>T: (Temp Dtor) [B7.3] || [B6.3]</div><div>which would put B4.2 into the environment, so we would know its value in B4.T.</div><div>
<br></div><div>On a tangent, B4.1 is also strangely placed. If you look at B2, you see that the block is empty and only has a teminator (the if). The condition of the if is not in the same block. Today, this only works with ResolveCondition, because I can't think of a way to create this kind of CFG without the if() having a ExprWithCleanups as its first child, thus exiting early in ResolveCondition.</div>
<div><br></div><div> Preds (3): B5 B6 B7</div><div> Succs (2): B2 B3</div><div><br></div><div> [B5]</div><div> 1: Dtor() (CXXConstructExpr, struct Dtor)</div><div> 2: [B5.1] (BindTemporary)</div><div> 3: [B5.2] (ImplicitCastExpr, NoOp, const struct Dtor)</div>
<div> 4: [B5.3].operator bool</div><div> 5: [B5.3]</div><div> 6: [B5.5] (ImplicitCastExpr, UserDefinedConversion, _Bool)</div><div> Preds (1): B6</div><div> Succs (1): B4</div><div><br></div><div> [B6]</div><div>
1: coin</div><div> 2: [B6.1] (ImplicitCastExpr, FunctionToPointerDecay, _Bool (*)(void))</div><div> 3: [B6.2]()</div><div> T: [B7.3] || [B6.3] || ...</div><div> Preds (1): B7</div><div> Succs (2): B4 B5</div>
<div><br></div><div> [B7]</div><div> 1: coin</div><div> 2: [B7.1] (ImplicitCastExpr, FunctionToPointerDecay, _Bool (*)(void))</div><div> 3: [B7.2]()</div><div> T: [B7.3] || ...</div><div> Preds (1): B8</div><div>
Succs (2): B4 B6</div><div><br></div><div> [B0 (EXIT)]</div><div> Preds (2): B1 B2</div></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><div class="">
<div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div style="word-wrap:break-word"><div><div>
Please do commit the change. Thanks for taking the time to work through it!</div>
</div></div></blockquote><div><br></div></div><div>Done. Thx for the review and taking the time to answer all my questions! :D</div><div><br></div><div>Cheers,</div><div>/Manuel</div><div><br></div></div></div></div>
</blockquote></div><br></div></div>