On Wed, Jun 9, 2010 at 7:14 AM, Ted Kremenek <kreme...@apple.com> wrote:
> Response inline!
>
> On Jun 6, 2010, at 9:41 PM, Jordy Rose wrote:
>
> > On Sat, 5 Jun 2010 23:43:42 -0700, Ted Kremenek <kreme...@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".
>
> Okay, makes sense!
>
> >> @@ -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.
>
> Okay, got it.
>
> But don't we still have the problem that 'canReasonAbout' is not accurate?
> (e.g., for the opcodes not handled)
>
> >
> > 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.
>
> Right.
>
> > 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.
>
> Are you specifically referring to removing the following code?
>
> // Does the symbol simplify to a constant? If so, "fold" the constant
> // by setting 'lhs' to a ConcreteInt and try again.
> if (Sym->getType(ValMgr.getContext())->isIntegerType())
> if (const llvm::APSInt *Constant = state->getSymVal(Sym)) {
> // The symbol evaluates to a constant. If necessary, promote the
> // folded constant (LHS) to the result type.
>
> >
> > 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.
>
> Yes; keeping this all in SimpleSValuator makes the most sense to me, and
> probably would be more efficient.
>
> >
> >
> >> + 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.
>
> Do they depend on it? If not, and if it is truly undefined for most
> compilers, we should eventually check this case and issue a warning.
>
> > Worse, "(x+1) <= 1" has two
> > solutions: x = UINT_MAX and x = 0. How can we handle these wraparound
> > cases?
>
> This requires modeling a disjunction over the values of x. We could extend
> the ConstraintManager API to allow one to specify such constraints without
> bifurcating the state. RangeConstraintManager, for example, should be able
> to model this case.
>
> >
> > 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.
>
> What you have seems monotonically better than what we have now, and the
> general approach seems okay to me. When we consider doing precise integer
> overflow checking, we will need to be more precise. For now, just add a big
> note to the code documenting the caveats/assumptions about the semantics.
>
> Our requirements with the static analyzer are different than the compiler.
> For the compiler we need conservative semantics. For the analyzer we would
> like that too, but can slide on that when it benefits us to find more
> bugs/less false positives.
>
> Zhongxing: What do you think?
>
The tricky part is this:
C1 + C2 > MAX => MAX - C1 < C2
and
C1 + C2 < MIN => MIN - C1 > C2
Since we don't have general infrastructure for handling overflow, I think
this is reasonable for now. But I'd like it to be kept as local as possible.
And I think it's possible to completely remove it if we are just going to
fix the bug.
_______________________________________________
cfe-commits mailing list
cfe-commits@cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
