<div dir="ltr">Btw, you may not want to review this yet, I found out that I am getting some crashes when I try to run this large-scale... I'll debug it tomorrow.</div><div class="gmail_extra"><br><br><div class="gmail_quote">
On 19 August 2013 15:24, Pavel Labath <span dir="ltr"><<a href="mailto:labath@google.com" target="_blank">labath@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">Hi Ted,<div><br></div><div>thanks for the comments. I have made a new version of the patch here <<a href="http://llvm-reviews.chandlerc.com/D1340" target="_blank">http://llvm-reviews.chandlerc.com/D1340</a>>. I do have one question below.</div>
<div class="gmail_extra"><br><br><div class="gmail_quote"><div><div class="h5">On 18 August 2013 07:39, Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com" target="_blank">kremenek@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"><div>On Aug 16, 2013, at 1:19 AM, Pavel Labath <<a href="mailto:labath@google.com" target="_blank">labath@google.com</a>> wrote:<br><div><br><blockquote type="cite"><div class="gmail_extra" style="font-family:Helvetica;font-size:13px;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px">
Although it may be debatable, I actually find this implementation of EvaluateLogicalExpressions more sensible. My impression of the ProgramState structure is that it is supposed to contain everything needed for further program evaluation. The current implementation seems to bypass that, because it is looking at the exploded graph history. I agree that it is a sensitive part and understand your caution. If you have any further questions, I would be happy to answer them.</div>
<br></blockquote></div><br></div><div>Hi Pavel,</div><div><br></div><div>(I’m reviewing D1340.3.patch)</div><div><br></div><div>While I agree that your assessment of EvaluateLogicalExpressions is more sensible, I think it depends on an assumption that isn’t true (yet).</div>
<div><br></div><div>Specifically, I’m concerned about the following snippet in EvaluateLogicalExpression:</div><div><div><div><br></div><div>+ assert(!X.isUnknownOrUndef() && "Value should have already been computed.");</div>
</div><div><div>+ ProgramStateRef StTrue, StFalse;</div><div>+ llvm::tie(StTrue, StFalse) = State->assume(X.castAs<DefinedOrUnknownSVal>());</div><div>+</div><div>+ assert(!StTrue != !StFalse && "Value should be evaluate to true or false.”);</div>
</div><div><br></div></div><div>This snippet assumes that the left-hand expression of a ‘&&’ or ‘||’ evaluated to a fully-constrained value. That is, the value cannot be both true and false. This is an invalid assumption.</div>
<div><br></div><div>To be sure, earlier logic in your patch does handle the case of UnknownVal:</div><div><br></div><div><div> // If the condition is still unknown, give up.</div><div> if (X.isUnknownOrUndef()) {</div>
<div>- builder.generateNode(PrevState, true, PredI);</div><div>- builder.generateNode(PrevState, false, PredI);</div><div>+ SValBuilder &SVB = PrevState->getStateManager().getSValBuilder();</div><div>
+</div><div>+ StTrue = PrevState->BindExpr(Condition, BldCtx.LC, SVB.makeTruthVal(true));</div><div>+ StFalse = PrevState->BindExpr(Condition, BldCtx.LC, SVB.makeTruthVal(false));</div><div>+</div><div>+ builder.generateNode(StTrue, true, PredI);</div>
<div>+ builder.generateNode(StFalse, false, PredI);</div><div> continue;</div><div> }</div></div><div><br></div><div>Thus you are explicitly recording the truth value in the state for UnknownVal. However, UnknownVal is not the only under constrained value. It is also possible to get an under constrained value if the constraint solver can’t model the constraint for a symbol. In such cases it is possible for a symbol to be both true or false, simply because that distinction cannot be represented in ProgramState. That scenario would cause the first assertion in the first code snippet to succeed (checking for UnknownVal), but the second assertion to fail. This undermines the entire approach.</div>
</div></blockquote><div> </div></div></div><div>That thought had crossed my mind, but I wasn't sure if such a thing can even happen. I have played with it a bit today, but I couldn't create a case where this would happen -- the assume logic would always add a constraint on the symbolic value such that in the new states, the value was always true, or always false. If you know any a case where this will not be possible, I think it would be great to add that as a test case.</div>
<div><br></div></div></div></div>
</blockquote></div><br></div>