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

Jordy Rose jediknil at belkadan.com
Tue Jun 8 17:38:18 PDT 2010


Here's the latest version of the patch, in which the overflow logic has
been moved into SimpleConstraintManager and SValuator is a little more
discerning about when it should just return UnknownVal.

I considered moving the simplification into SValuator, but haven't done it
yet because of this overflow thing. Here's a (roundabout) explanation why:

The whole reduction currently relies on this manipulation:
  $sym + k1 == k2  <--> $sym == k2 - k1
This is always true logically, but breaks down for other operators with
modular arithmetic. Admittedly, ordering comparisons are less meaningful in
a modular-arithmetic context, but...

x+1 > 0 is the same as x > -1, logically -- any nonnegative integer.
However, in a modular unsigned context, this becomes x > UINT_MAX, which
has no solutions. This is what originally motivated the overflow-checking
code, and just supporting disjoint ranges doesn't eliminate the need to
track overflow.

So, if all this constant folding was handled in SValuator, how does the
constraint manager know the difference between x+1 > 0 and x > UINT_MAX?

(What /can/ be folded in the SValuator is sequences of
addition/subtraction operations, but that still leaves the final
manipulation in the constraint manager. That may still be a worthwhile
operation, though.)

What do you think? Is it worth leaving the code in the constraint manager,
and adding code for disjoint ranges when an overflow occurs (probably in a
later commit)? Or is there a way we could move everything to the SValuator?


On Tue, 8 Jun 2010 16:14:43 -0700, Ted Kremenek <kremenek at 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 <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".
> 
> 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?
-------------- next part --------------
Index: lib/Checker/SimpleSValuator.cpp
===================================================================
--- lib/Checker/SimpleSValuator.cpp	(revision 105480)
+++ lib/Checker/SimpleSValuator.cpp	(working copy)
@@ -211,6 +211,28 @@
   return ValMgr.makeTruthVal(isEqual ? lhs == rhs : lhs != rhs, resultTy);
 }
 
+static bool canReasonAbout(BinaryOperator::Opcode op) {
+  // FIXME: is there a way to keep this in sync with the constraint manager?
+  switch (op) {
+  // We don't reason yet about bitwise-constraints on symbolic values.
+  case BinaryOperator::And:
+  case BinaryOperator::Or:
+  case BinaryOperator::Xor:
+    return false;
+  // We don't reason yet about these arithmetic constraints on
+  // symbolic values.
+  case BinaryOperator::Mul:
+  case BinaryOperator::Div:
+  case BinaryOperator::Rem:
+  case BinaryOperator::Shl:
+  case BinaryOperator::Shr:
+    return false;
+  // All other cases.
+  default:
+    return true;
+  }
+}
+
 SVal SimpleSValuator::EvalBinOpNN(const GRState *state,
                                   BinaryOperator::Opcode op,
                                   NonLoc lhs, NonLoc rhs,
@@ -261,63 +283,73 @@
       }
     }
     case nonloc::SymExprValKind: {
-      // Logical not?
-      if (!(op == BinaryOperator::EQ && rhs.isZeroConstant()))
+      nonloc::SymExprVal *selhs = cast<nonloc::SymExprVal>(&lhs);
+
+      // Only handle LHS of the form "$sym op constant", at least for now.
+      const SymIntExpr *symIntExpr =
+        dyn_cast<SymIntExpr>(selhs->getSymbolicExpression());
+
+      if (!symIntExpr)
         return UnknownVal();
 
-      const SymExpr *symExpr =
-        cast<nonloc::SymExprVal>(lhs).getSymbolicExpression();
+      // Is this a logical not? (!x is represented as x == 0.)
+      if (op == BinaryOperator::EQ && rhs.isZeroConstant()) {
+        // We know how to negate certain expressions. Simplify them here.
 
-      // Only handle ($sym op constant) for now.
-      if (const SymIntExpr *symIntExpr = dyn_cast<SymIntExpr>(symExpr)) {
+        // Only handle !($sym op constant) for now.
         BinaryOperator::Opcode opc = symIntExpr->getOpcode();
         switch (opc) {
-          case BinaryOperator::LAnd:
-          case BinaryOperator::LOr:
-            assert(false && "Logical operators handled by branching logic.");
-            return UnknownVal();
-          case BinaryOperator::Assign:
-          case BinaryOperator::MulAssign:
-          case BinaryOperator::DivAssign:
-          case BinaryOperator::RemAssign:
-          case BinaryOperator::AddAssign:
-          case BinaryOperator::SubAssign:
-          case BinaryOperator::ShlAssign:
-          case BinaryOperator::ShrAssign:
-          case BinaryOperator::AndAssign:
-          case BinaryOperator::XorAssign:
-          case BinaryOperator::OrAssign:
-          case BinaryOperator::Comma:
-            assert(false && "'=' and ',' operators handled by GRExprEngine.");
-            return UnknownVal();
-          case BinaryOperator::PtrMemD:
-          case BinaryOperator::PtrMemI:
-            assert(false && "Pointer arithmetic not handled here.");
-            return UnknownVal();
-          case BinaryOperator::Mul:
-          case BinaryOperator::Div:
-          case BinaryOperator::Rem:
-          case BinaryOperator::Add:
-          case BinaryOperator::Sub:
-          case BinaryOperator::Shl:
-          case BinaryOperator::Shr:
-          case BinaryOperator::And:
-          case BinaryOperator::Xor:
-          case BinaryOperator::Or:
-            // Not handled yet.
-            return UnknownVal();
-          case BinaryOperator::LT:
-          case BinaryOperator::GT:
-          case BinaryOperator::LE:
-          case BinaryOperator::GE:
-          case BinaryOperator::EQ:
-          case BinaryOperator::NE:
-            opc = NegateComparison(opc);
-            assert(symIntExpr->getType(ValMgr.getContext()) == resultTy);
-            return ValMgr.makeNonLoc(symIntExpr->getLHS(), opc,
-                                     symIntExpr->getRHS(), resultTy);
+        default:
+          // We don't know how to negate this operation.
+          // Just handle it as if it were a normal comparison to 0.
+          break;
+        case BinaryOperator::LAnd:
+        case BinaryOperator::LOr:
+          assert(false && "Logical operators handled by branching logic.");
+          return UnknownVal();
+        case BinaryOperator::Assign:
+        case BinaryOperator::MulAssign:
+        case BinaryOperator::DivAssign:
+        case BinaryOperator::RemAssign:
+        case BinaryOperator::AddAssign:
+        case BinaryOperator::SubAssign:
+        case BinaryOperator::ShlAssign:
+        case BinaryOperator::ShrAssign:
+        case BinaryOperator::AndAssign:
+        case BinaryOperator::XorAssign:
+        case BinaryOperator::OrAssign:
+        case BinaryOperator::Comma:
+          assert(false && "'=' and ',' operators handled by GRExprEngine.");
+          return UnknownVal();
+        case BinaryOperator::PtrMemD:
+        case BinaryOperator::PtrMemI:
+          assert(false && "Pointer arithmetic not handled here.");
+          return UnknownVal();
+        case BinaryOperator::LT:
+        case BinaryOperator::GT:
+        case BinaryOperator::LE:
+        case BinaryOperator::GE:
+        case BinaryOperator::EQ:
+        case BinaryOperator::NE:
+          // Negate the comparison and make a value.
+          opc = NegateComparison(opc);
+          assert(symIntExpr->getType(ValMgr.getContext()) == resultTy);
+          return ValMgr.makeNonLoc(symIntExpr->getLHS(), opc,
+                                   symIntExpr->getRHS(), resultTy);
         }
       }
+
+      // For now, only handle expressions whose RHS is a constant,
+      // and whose operation is supported by the constraint manager.
+      const nonloc::ConcreteInt *rhsInt = dyn_cast<nonloc::ConcreteInt>(&rhs);
+      if (rhsInt && canReasonAbout(op)) {
+         return ValMgr.makeNonLoc(symIntExpr, op, rhsInt->getValue(),
+                                  resultTy);
+      }
+
+      // We can't reason about expressions whose RHS is not constant,
+      // or those whose operations are not supported by the constraint manager.
+      return UnknownVal();
     }
     case nonloc::ConcreteIntKind: {
       if (isa<nonloc::ConcreteInt>(rhs)) {
@@ -376,9 +408,11 @@
           continue;
         }
       
-      if (isa<nonloc::ConcreteInt>(rhs)) {
-        return ValMgr.makeNonLoc(slhs->getSymbol(), op,
-                                 cast<nonloc::ConcreteInt>(rhs).getValue(),
+      // For now, only handle expressions whose RHS is a constant,
+      // and whose operation is supported by the constraint manager.
+      const nonloc::ConcreteInt *rhsInt = dyn_cast<nonloc::ConcreteInt>(&rhs);
+      if (rhsInt && canReasonAbout(op)) {
+        return ValMgr.makeNonLoc(slhs->getSymbol(), op, rhsInt->getValue(),
                                  resultTy);
       }
 
Index: lib/Checker/SimpleConstraintManager.cpp
===================================================================
--- lib/Checker/SimpleConstraintManager.cpp	(revision 105480)
+++ lib/Checker/SimpleConstraintManager.cpp	(working copy)
@@ -35,12 +35,11 @@
         case BinaryOperator::Or:
         case BinaryOperator::Xor:
           return false;
-        // We don't reason yet about arithmetic constraints on symbolic values.
+        // We don't reason yet about these arithmetic constraints on
+        // symbolic values.
         case BinaryOperator::Mul:
         case BinaryOperator::Div:
         case BinaryOperator::Rem:
-        case BinaryOperator::Add:
-        case BinaryOperator::Sub:
         case BinaryOperator::Shl:
         case BinaryOperator::Shr:
           return false;
@@ -125,7 +124,8 @@
                                                   NonLoc Cond,
                                                   bool Assumption) {
 
-  // We cannot reason about SymIntExpr and SymSymExpr.
+  // We cannot reason about SymSymExprs,
+  // and can only reason about some SymIntExprs.
   if (!canReasonAbout(Cond)) {
     // Just return the current state indicating that the path is feasible.
     // This may be an over-approximation of what is possible.
@@ -151,17 +151,102 @@
 
   case nonloc::SymExprValKind: {
     nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond);
-    if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression())){
-      // FIXME: This is a hack.  It silently converts the RHS integer to be
-      // of the same type as on the left side.  This should be removed once
-      // we support truncation/extension of symbolic values.      
+
+    // For now, we only handle expressions whose RHS is an integer.
+    if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression())){      
+      // First, attempt to convert expressions of the form
+      //    ($sym + int1) == int2
+      // to
+      //    $sym == (int1 - int2)
+      // where == is any comparison operator,
+      // and + and - are a binary operator and its inverse.
+      // Currently only addition and subtraction are modeled;
+      // constraints involving other operators are assumed to be feasible.
+
+      // This tracks the net number of overflows (the number of positive
+      // overflows minus the number of negative overflows).
+      int32_t NetOverflow = 0;
+
+      const SymExpr *LHS = SE->getLHS();
+      llvm::APSInt RHS(SE->getRHS());
+
+      while (const SymIntExpr *LSE = dyn_cast<SymIntExpr>(LHS)) {
+        LHS = LSE->getLHS();
+        BinaryOperator::Opcode op = LSE->getOpcode();
+
+        // FIXME: Should eventually model other operations.
+        switch (op) {
+        default:
+          // We can't model this operation,
+          // so we have to assume the constraint is feasible.
+          return state;
+        case BinaryOperator::Add:
+          op = BinaryOperator::SubAssign;
+          break;
+        case BinaryOperator::Sub:
+          op = BinaryOperator::AddAssign;
+          break;
+        }
+
+        // If LSE is $sym + int1, this performs RHS -= int1.
+        // The net count overflow is updated as well.
+        // FIXME: once operations that destroy information are implemented
+        // (shifts, division, bitwise ops), there will be kinds of overflow
+        // that don't cancel out like positive and negative addition overflow.
+        NetOverflow += EvaluateWithOverflow(op, RHS, LSE->getRHS());
+      }
+
+      // The next block checks if there were more positive overflows than
+      // negative or vice versa. If so, the condition is logically a tautology.
+      // For example, if the condition is (i+1 <= length), and 'length' is
+      // known to be 0, the constraint reduces to $i <= -1.
+
+      // If there was no overflow, or if the positive and negative overflows
+      // cancelled out (by wrapping back and forth), the assumption proceeds
+      // as usual.
+
+      // FIXME: Unsigned integer overflow is actually defined in C and C++,
+      // and both Clang and GCC allow signed integer overflow as well,
+      // which makes the above constraint satisfiable at $i == INT_MAX.
+      if (NetOverflow != 0) {
+        switch (SE->getOpcode()) {
+        default:
+          return state;
+        case BinaryOperator::EQ:
+          // It is impossible to equal an out-of-range value.
+          return Assumption ? NULL : state;
+        case BinaryOperator::GE:
+        case BinaryOperator::GT:
+          // If we had positive overflow, we essentially have $sym > MAX,
+          // which is infeasible.
+          return (Assumption ^ (NetOverflow > 0)) ? state : NULL;
+        case BinaryOperator::LE:
+        case BinaryOperator::LT:
+          // If we had negative overflow, we essentially have $sym < MIN,
+          // which is also infeasible.
+          return (Assumption ^ (NetOverflow < 0)) ? state : NULL;
+        }
+      }
+
       GRStateManager &StateMgr = state->getStateManager();
       ASTContext &Ctx = StateMgr.getContext();
-      QualType LHSType = SE->getLHS()->getType(Ctx);
       BasicValueFactory &BasicVals = StateMgr.getBasicVals();
-      const llvm::APSInt &RHS = BasicVals.Convert(LHSType, SE->getRHS());
-      SymIntExpr SENew(SE->getLHS(), SE->getOpcode(), RHS, SE->getType(Ctx));
 
+      // FIXME: This is a hack.  It silently converts the RHS integer to be
+      // of the same type as on the left side.  This should be removed once
+      // we support truncation/extension of symbolic values.      
+      QualType LHSType = LHS->getType(Ctx);
+      const llvm::APSInt *finalRHS = &BasicVals.Convert(LHSType, RHS);
+
+      // BasicVals.Convert() is smart enough not to make a new value if the
+      // types are already compatible. However, we need this final RHS to
+      // persist as part of the assumption. Get a managed APSInt if necessary.
+      if (finalRHS == &RHS)
+        finalRHS = &BasicVals.getValue(RHS);
+
+      // Finally, assemble the new expression and Assume it.
+      SymIntExpr SENew(LHS, SE->getOpcode(), *finalRHS, SE->getType(Ctx));
+
       return AssumeSymInt(state, Assumption, &SENew);
     }
 
@@ -186,9 +271,13 @@
                                                      bool Assumption,
                                                      const SymIntExpr *SE) {
 
+  // If we failed to simplify the expression to "$sym op int",
+  // we have to give up and assume the constraint is feasible.
+  if (!isa<SymbolData>(SE->getLHS()))
+    return state;
 
-  // Here we assume that LHS is a symbol.  This is consistent with the
-  // rest of the constraint manager logic.
+  // At this point we can assume that LHS is a symbol.
+  // This is consistent with the rest of the constraint manager logic.
   SymbolRef Sym = cast<SymbolData>(SE->getLHS());
   const llvm::APSInt &Int = SE->getRHS();
 
@@ -246,4 +335,70 @@
   return isFeasible ? state : NULL;
 }
 
+SimpleConstraintManager::OverflowKind
+SimpleConstraintManager::EvaluateWithOverflow(BinaryOperator::Opcode Op,
+                                              llvm::APSInt& Left,
+                                              const llvm::APSInt& RawRight) {
+  // FIXME: does not handle mixed signedness well
+  SimpleConstraintManager::OverflowKind Overflow
+    = SimpleConstraintManager::NoOverflow;
+
+  // FIXME: This silently converts the RHS integer to be of the same width
+  // as the left side.  Is that correct behavior?
+  llvm::APSInt Right(RawRight);
+  Right.extOrTrunc(Left.getBitWidth());
+
+  assert(BinaryOperator::isAssignmentOp(Op) && "Must use an assignment op.");
+
+  switch (Op) {
+  default:
+    assert(false && "Can't reason about that operator yet.");
+
+  case BinaryOperator::AddAssign: {
+    // Negative overflow if R < 0, and INT_MIN + (-R) > L
+    // Positive overflow if R >= 0, and INT_MAX - R < L
+
+    bool Unsigned = Right.isUnsigned();
+    if (!Unsigned && Right.isNegative()) {
+      llvm::APSInt Min(llvm::APSInt::getMinValue(Right.getBitWidth(),
+                                                 Unsigned));
+      if (Min - Right > Left) {
+        Overflow = SimpleConstraintManager::NegativeAdditionOverflow;
+      }
+    } else {
+      llvm::APSInt Max(llvm::APSInt::getMaxValue(Right.getBitWidth(),
+                                                 Unsigned));
+      if (Max - Right < Left) {
+        Overflow = SimpleConstraintManager::PositiveAdditionOverflow;
+      }
+    }
+    Left += Right;
+    break;
+  }
+  case BinaryOperator::SubAssign: {
+    // Positive overflow if R < 0, and INT_MAX - (-R) < L
+    // Negative overflow if R >= 0, and INT_MIN + R > L
+
+    bool Unsigned = Right.isUnsigned();
+    if (!Unsigned && Right.isNegative()) {
+      llvm::APSInt Max(llvm::APSInt::getMaxValue(Right.getBitWidth(),
+                                                 Unsigned));
+      if (Max + Right < Left) {
+        Overflow = SimpleConstraintManager::PositiveAdditionOverflow;
+      }
+    } else {
+      llvm::APSInt Min(llvm::APSInt::getMinValue(Right.getBitWidth(),
+                                                 Unsigned));
+      if (Min + Right > Left) {
+        Overflow = SimpleConstraintManager::NegativeAdditionOverflow;
+      }
+    }
+    Left -= Right;
+    break;
+  }
+  }
+
+  return Overflow;
+}
+
 }  // end of namespace clang
Index: lib/Checker/SimpleConstraintManager.h
===================================================================
--- lib/Checker/SimpleConstraintManager.h	(revision 105480)
+++ lib/Checker/SimpleConstraintManager.h	(working copy)
@@ -76,6 +76,22 @@
   const GRState *AssumeAux(const GRState *state, Loc Cond,bool Assumption);
 
   const GRState *AssumeAux(const GRState *state, NonLoc Cond, bool Assumption);
+
+  // Used to identify tautological conditions.
+  // NegativeAdditionOverflow is -PositiveAdditionOverflow so that the two can
+  // cancel out: ((n+1)-1) is not logically an overflow, even if n == INT_MAX.
+  enum OverflowKind {
+    NoOverflow = 0,
+    PositiveAdditionOverflow = 1,
+    NegativeAdditionOverflow = -PositiveAdditionOverflow
+  };
+  
+  // Performs the given operation on the two integers and returns what overflow
+  // happened, if any. Op must be an assignment operator.
+  // Currently only handles addition and subtraction.
+  OverflowKind EvaluateWithOverflow(BinaryOperator::Opcode Op,
+                                    llvm::APSInt& Left,
+                                    const llvm::APSInt& Right);
 };
 
 }  // end clang namespace
Index: include/clang/AST/Expr.h
===================================================================
--- include/clang/AST/Expr.h	(revision 105480)
+++ include/clang/AST/Expr.h	(working copy)
@@ -2188,7 +2188,11 @@
   static bool isLogicalOp(Opcode Opc) { return Opc == LAnd || Opc == LOr; }
   bool isLogicalOp() const { return isLogicalOp(Opc); }
 
-  bool isAssignmentOp() const { return Opc >= Assign && Opc <= OrAssign; }
+  static bool isAssignmentOp(Opcode Opc) {
+    return Opc >= Assign && Opc <= OrAssign;
+  }
+  bool isAssignmentOp() const { return isAssignmentOp(Opc); }
+
   bool isCompoundAssignmentOp() const { return Opc > Assign && Opc <= OrAssign;}
   bool isShiftAssignOp() const { return Opc == ShlAssign || Opc == ShrAssign; }
 
Index: test/Analysis/linearity.c
===================================================================
--- test/Analysis/linearity.c	(revision 0)
+++ test/Analysis/linearity.c	(revision 0)
@@ -0,0 +1,154 @@
+// RUN: %clang_cc1 -analyze -analyzer-check-objc-mem -analyzer-experimental-checks -verify %s
+#include <limits.h>
+
+// Used to trigger warnings
+typedef typeof(sizeof(int)) size_t;
+void *malloc(size_t);
+void free(void *);
+
+// Tests a simple rewrite to "length == 2".
+void subtractRegular(unsigned int length) {
+  char* name = malloc(1);
+  if (length-1 == 1) {
+    free(name);
+    name = 0;
+  }
+  if (length-1 == 1) {
+    name = malloc(1); // no-warning
+  }
+
+  free(name);
+}
+
+// Tests a case that may be mistaken for !(length-1).
+void subtractEqZero(unsigned int length) {
+  char* name = malloc(1);
+  if (length-1 == 0) {
+    free(name);
+    name = 0;
+  }
+  if (length-1 == 0) {
+    name = malloc(1); // no-warning
+  }
+
+  free(name);
+}
+
+// Tests a case with nested SymIntExprs
+// The second branch condition reduces to (($length-2)-1 == 0)
+// which the constraint manager should still be able to handle.
+void subtractMultiple(unsigned int length) {
+  char* name = malloc(1);
+  if (length-2 == 1) {
+    free(name);
+    name = 0;
+  } else {
+    length -= 2;
+  }
+  if (length-1 == 0) {
+    name = malloc(1); // no-warning
+  }
+
+  free(name);
+}
+
+// Tests a simple rewrite to "length == 9".
+// Same as before, but with addition
+void addRegular(unsigned int length) {
+  char* name = malloc(1);
+  if (length+1 == 10) {
+    free(name);
+    name = 0;
+  }
+  if (length+1 == 10) {
+    name = malloc(1); // no-warning
+  }
+
+  free(name);
+}
+
+
+// The next two cases test negative and positive overflow,
+// which create tautological conditions.
+void negativeOverflow(unsigned int length) {
+  char* name = malloc(1);
+  if (length+1 == 0) {
+    name = malloc(1); // no-warning
+  }
+  if (length+1 <= 0) {
+    name = malloc(1); // no-warning
+  }
+
+  free(name);
+}
+
+void positiveOverflow(unsigned int length) {
+  char* name = malloc(1);
+  if (length-1 == UINT_MAX) {
+    name = malloc(1); // no-warning
+  }
+  if (length-1 >= UINT_MAX) {
+    name = malloc(1); // no-warning
+  }
+
+  free(name);
+}
+
+// Similar to subtractMultiple()
+// Tests multiple uses of $length, both as $length-10 and (($length-10)+10).
+void compoundSafe(unsigned int length) {
+  char* name = malloc(1);
+  unsigned int lots = length - 10;
+  if (lots == 10) {
+    free(name);
+    name = 0;
+  }
+  if (lots+10 == 20) {
+    name = malloc(1); // no-warning
+  }
+
+  free(name);
+}
+
+// Same as compoundSafe(), but with multiple paths to the second branch.
+void compoundDangerous(unsigned int length) {
+  char* name = malloc(1);
+  unsigned int lots = length - 10;
+  if (lots == 10) {
+    free(name);
+    name = 0;
+    lots += 10;
+  }
+  if (lots == 20) {
+    name = malloc(1); // expected-warning{{Allocated memory never released. Potential memory leak.}}
+  }
+
+  free(name);
+}
+
+// The next two tests verify that negative and positive overflows cancel out.
+void wraparoundSafeGT(unsigned int length) {
+  char* name = malloc(1);
+  unsigned int temp = length-1;
+  if (length > 0) {
+    free(name);
+  }
+  if (temp+1 > 0) {
+    name = malloc(1); // no-warning
+  }
+
+  free(name);
+}
+
+void wraparoundSafeEQ(unsigned int length) {
+  char* name = malloc(1);
+  unsigned int temp = length-1;
+  if (length == 0) {
+    free(name);
+  }
+  if (temp+1 == 0) {
+    name = malloc(1); // no-warning
+  }
+
+  free(name);
+}


More information about the cfe-commits mailing list