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

[Jordy Rose]

Thanks for comments; responses inline.


On Sat, 5 Jun 2010 23:43:42 -0700, Ted Kremenek <kremenek at apple.com>
wrote:
> On Jun 5, 2010, at 6:01 PM, Jordy Rose wrote:
>> public:
>>   enum OverflowKind {
>>     NoOverflow = 0,
>>     AdditionOverflow = 1,
>>     AdditionUnderflow = -AdditionOverflow
>>   };
> 
> Is there a reason we want to make AdditionUnderflow negative?  Why not
> just make it 2?  From the algorithm in SimpleConstraintManager, this
looks
> intended.  If so, please comment.

Yes; the idea is that a negative overflow followed by a positive overflow
is no overflow at all, and so the two should cancel out. This occurs in
situations like these:

void doSomething (unsigned x, unsigned length) {
  // pretend this is a branch being Assumed true
  assert(length == 0);
  --x;
  if (x+1 <= length) {
    // actually do work
  }
}

Here, the condition reduces to "(($x-1)+1) <= 0", which has an
intermediate step of "($x-1) <= -1".


> I am also not certain if this even needs to be in BasicValueFactory.  It
> seems specific to SimpleConstraintManager, and the places where the
> underflow/overflow values are used are only for temporary APSInt values.

> BasicValueFactory is meant to created values that are permanently
resident
> in a GRState.

Good point. I wasn't entirely clear on BasicValueFactory before.


> Minor nit: Please keep your comment style consistent with the LLVM
coding
> style.  Please try to have sentences that start capitalized and end with
a
> period.  I'd also prefer that the break appear on the following line
with
> the comment above it, but that's minor.  We tend to prefer comments
above
> statements then on the side of them.

Rewritten with better comments all over. Thanks.


> @@ -316,8 +304,18 @@
>              assert(symIntExpr->getType(ValMgr.getContext()) ==
resultTy);
>              return ValMgr.makeNonLoc(symIntExpr->getLHS(), opc,
>                                       symIntExpr->getRHS(), resultTy);
> +          }
>          }
>        }
> +      
> +      // for now, only handle ($sym op constant) here as well
> 
> Minor nit: Please keep this comment in the LLVM coding style (make it a
> sentence).  It's also probably worth pointing out what cases these
handle,
> and why Mul, Div, and friends are handled here.  Brief comments like
this
> are helpful, especially when the logic is broken up so recursively. 
Also,
> can we really handle 'Mul', 'Div', 'Shl', etc., in this case?  In
> SimpleConstraintManager::canReasonAbout, we still return false for these
> cases for SymIntExpr.

I wasn't reading the section quite right at first, but actually it seems
correct. There are two things going on here:

- !(expr) is represented as (expr) == 0. For comparison ops, we can
simplify the expression by negating the comparison and returning that. The
original code only allowed this and returned UnknownVal otherwise,
disallowing things like ($a*3 == 0)
- The new code also allows "(expr) op constant". Previously, this would
have been UnknownVal(). Here, it's a SymExprVal that probably still can't
be evaluated. It's less efficent, but there's no harm done.

It's worth noting that $sym*3 is not currently considered an UnknownVal;
the case for a SymbolVal LHS and ConcreteInt RHS also just makes a
SymExprVal.

Do you think it's worth checking the expression type in the SymbolVal
case? That would let the UnknownVal bubble up and probably save a bit of
work later, but it'd be more stuff to keep in sync with the constraint
manager.

I'm going back to clean up this section. Wondering if I can actually push
all this simplification into SimpleSValuator -- it's all arithmetic stuff
anyway. Going to try tonight.


> +      const llvm::APSInt *RHS = &SE->getRHS();
> +      int TotalOverflow = 0;
> 
> Should TotalOverflow by an APInt, or a uint64_t?  Seems like this could
> overflow itself in some cases.

TotalOverflow is not measuring a quantity, but the net number of
overflows, where positive overflows cancel out negative overflows.
Commented and renamed to NetOverflow in my local version.

John brought up an important point, though: "(x+1) <= 0" has a solution at
x = UINT_MAX, since unsigned overflow is defined in C and C++, and people
are used to signed wraparound as well. Worse, "(x+1) <= 1" has two
solutions: x = UINT_MAX and x = 0. How can we handle these wraparound
cases?

Until that's resolved, I'm not sure it's a good idea to commit, though
leaving it as is (pretending wraparound doesn't exist) might be the least
troublesome mechanism for now.