[cfe-commits] [patch] Tracking simple arithmetic constraints (PR2695) (resubmitted)

[Ted Kremenek]

On Jun 5, 2010, at 11:15 PM, Jordy Rose wrote:

> 
> On Sun, 6 Jun 2010 13:52:30 +0800, Zhongxing Xu <xuzhongxing at gmail.com>
> wrote:
>> I understand your point. I mean we should also report such tautology
>> conditions to the user in some checker and re-use that results in the
>> following evaluation.
>> 
> 
> Oh, okay. Well, it is using the overflow to determine feasibility (this
> block, which does need to be better commented):
> 
>  if (TotalOverflow) {
>    switch (SE->getOpcode()) {
>    default:
>      return state;
>    case BinaryOperator::EQ:
>      return Assumption ? NULL : state;
>    case BinaryOperator::GE:
>    case BinaryOperator::GT:
>      return (Assumption ^ (TotalOverflow > 0)) ? state : NULL;
>    case BinaryOperator::LE:
>    case BinaryOperator::LT:
>      return (Assumption ^ (TotalOverflow < 0)) ? state : NULL;
>    }
>  }
> 
> 
> I'm a bit leery of warning since it could be a path-dependent tautology:
> 
>  if (length == 1)
>    delta = -1;
>  else
>    delta = calculateDelta(length);
> 
>  if (length+delta > 0)
>    doSomethingUsefulWith(length, delta);
> 
> Do you think it's worth warning in cases like this?

I don't think it's worth warning until we have the apparatus in place to report lucid diagnostics to the user.  Otherwise issuing warnings is just noise.

In the mean time, I'd rather constrain the focus of this patch into improving the constraint reasoning logic, which will help reduce false positives and possibly find other bugs.  Where we see opportunities to expand or refine things, we should add a FIXME.

I think if want to issue warnings here, we should consider how that could be done.  A path-sensitive warning is typically associated with ExplodedNodes, while SValuator and ConstraintManager only reason about values.  I think the SValuator/ConstraintManager should do the heavy lifting of computing integer overflow conditions, but reporting problems should some how tie into our checker infrastructure (which knows how to report issues to the user).