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.
On 19 August 2013 15:24, Pavel Labath <[email protected]> wrote: > 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
