Hi Ted, thanks for the comments. I have made a new version of the patch here < http://llvm-reviews.chandlerc.com/D1340>. I do have one question below.
On 18 August 2013 07:39, Ted Kremenek <[email protected]> wrote: > On Aug 16, 2013, at 1:19 AM, Pavel Labath <[email protected]> wrote: > > 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. > > > Hi Pavel, > > (I’m reviewing D1340.3.patch) > > While I agree that your assessment of EvaluateLogicalExpressions is more > sensible, I think it depends on an assumption that isn’t true (yet). > > Specifically, I’m concerned about the following snippet in > EvaluateLogicalExpression: > > + assert(!X.isUnknownOrUndef() && "Value should have already been > computed."); > + ProgramStateRef StTrue, StFalse; > + llvm::tie(StTrue, StFalse) = > State->assume(X.castAs<DefinedOrUnknownSVal>()); > + > + assert(!StTrue != !StFalse && "Value should be evaluate to true or > false.”); > > 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. > > To be sure, earlier logic in your patch does handle the case of UnknownVal: > > // If the condition is still unknown, give up. > if (X.isUnknownOrUndef()) { > - builder.generateNode(PrevState, true, PredI); > - builder.generateNode(PrevState, false, PredI); > + SValBuilder &SVB = PrevState->getStateManager().getSValBuilder(); > + > + StTrue = PrevState->BindExpr(Condition, BldCtx.LC, > SVB.makeTruthVal(true)); > + StFalse = PrevState->BindExpr(Condition, BldCtx.LC, > SVB.makeTruthVal(false)); > + > + builder.generateNode(StTrue, true, PredI); > + builder.generateNode(StFalse, false, PredI); > continue; > } > > 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. > 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.
_______________________________________________ cfe-commits mailing list [email protected] http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
