[PATCH] [analyzer] Refactor conditional expression evaluating code

[Pavel Labath]

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>