[PATCH] [analyzer] Refactor conditional expression evaluating code

[Pavel Labath]

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/503b1eb1/attachment.html>