[PATCH] [analyzer] Refactor conditional expression evaluating code

Pavel Labath labath at google.com
Mon Aug 19 09:50:04 PDT 2013

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 <labath at google.com> 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 <kremenek at apple.com> wrote:
>> On Aug 16, 2013, at 1:19 AM, Pavel Labath <labath at google.com> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20130819/18176785/attachment.html>

More information about the cfe-commits mailing list