[analyzer] Remove all uses of ConstraintManager::canResonAbout() from

ExprEngine.

Teach SimpleConstraintManager::assumeSymRel() to propagate constraints
to symbolic expressions.

+ One extra warning (real bug) is now generated due to enhanced
assumeSymRel().

llvm-svn: 145832

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h

@@ -276,6 +276,7 @@ namespace nonloc {
 enum Kind { ConcreteIntKind, SymbolValKind, SymExprValKind,
             LocAsIntegerKind, CompoundValKind, LazyCompoundValKind };
 
+// TODO: Change to contain symbol data.
 class SymbolVal : public NonLoc {
 public:
   SymbolVal(SymbolRef sym) : NonLoc(SymbolValKind, sym) {}

clang/lib/StaticAnalyzer/Core/ExprEngineC.cpp

@@ -121,8 +121,7 @@ void ExprEngine::VisitBinaryOperator(const BinaryOperator* B,
       
       SVal LHSVal;
       
-      if (Result.isUnknown() ||
-          !getConstraintManager().canReasonAbout(Result)) {
+      if (Result.isUnknown()) {
         
         unsigned Count = currentBuilderContext->getCurrentBlockCount();
         
@@ -358,8 +357,7 @@ void ExprEngine::VisitDeclStmt(const DeclStmt *DS, ExplodedNode *Pred,
       
       // Recover some path-sensitivity if a scalar value evaluated to
       // UnknownVal.
-      if ((InitVal.isUnknown() ||
-           !getConstraintManager().canReasonAbout(InitVal)) &&
+      if ((InitVal.isUnknown()) &&
           !VD->getType()->isReferenceType() &&
           !Pred->getState()->isTainted(InitVal)) {
         InitVal = svalBuilder.getConjuredSymbolVal(NULL, InitEx,
@@ -726,7 +724,7 @@ void ExprEngine::VisitIncrementDecrementOperator(const UnaryOperator* U,
       SVal Result = evalBinOp(state, Op, V2, RHS, U->getType());
       
       // Conjure a new symbol if necessary to recover precision.
-      if (Result.isUnknown() || !getConstraintManager().canReasonAbout(Result)){
+      if (Result.isUnknown()){
         DefinedOrUnknownSVal SymVal =
         svalBuilder.getConjuredSymbolVal(NULL, Ex,
                                  currentBuilderContext->getCurrentBlockCount());

clang/lib/StaticAnalyzer/Core/ProgramState.cpp

@@ -550,9 +550,8 @@ bool ScanReachableSymbols::scan(const SymExpr *sym) {
     return true;
   isVisited = 1;
   
-  if (const SymbolData *sData = dyn_cast<SymbolData>(sym))
-    if (!visitor.VisitSymbol(sData))
-      return false;
+  if (!visitor.VisitSymbol(sym))
+    return false;
   
   switch (sym->getKind()) {
     case SymExpr::RegionValueKind:

clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp

@@ -212,6 +212,40 @@ const ProgramState *SimpleConstraintManager::assumeAux(const ProgramState *state
   } // end switch
 }
 
+static llvm::APSInt computeAdjustment(const SymExpr *LHS,
+                                      SymbolRef &Sym) {
+  llvm::APSInt DefaultAdjustment;
+  DefaultAdjustment = 0;
+
+  // First check if the LHS is a simple symbol reference.
+  if (isa<SymbolData>(LHS))
+    return DefaultAdjustment;
+
+  // Next, see if it's a "($sym+constant1)" expression.
+  const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS);
+
+  // We cannot simplify "($sym1+$sym2)".
+  if (!SE)
+    return DefaultAdjustment;
+
+  // Get the constant out of the expression "($sym+constant1)" or
+  // "<expr>+constant1".
+  Sym = SE->getLHS();
+  switch (SE->getOpcode()) {
+  case BO_Add:
+    return SE->getRHS();
+    break;
+  case BO_Sub:
+    return -SE->getRHS();
+    break;
+  default:
+    // We cannot simplify non-additive operators.
+    return DefaultAdjustment;
+  }
+
+  return DefaultAdjustment;
+}
+
 const ProgramState *SimpleConstraintManager::assumeSymRel(const ProgramState *state,
                                                      const SymExpr *LHS,
                                                      BinaryOperator::Opcode op,
@@ -219,48 +253,15 @@ const ProgramState *SimpleConstraintManager::assumeSymRel(const ProgramState *st
   assert(BinaryOperator::isComparisonOp(op) &&
          "Non-comparison ops should be rewritten as comparisons to zero.");
 
-   // We only handle simple comparisons of the form "$sym == constant"
-   // or "($sym+constant1) == constant2".
-   // The adjustment is "constant1" in the above expression. It's used to
-   // "slide" the solution range around for modular arithmetic. For example,
-   // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
-   // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
-   // the subclasses of SimpleConstraintManager to handle the adjustment.
-   llvm::APSInt Adjustment;
-
-  // First check if the LHS is a simple symbol reference.
-  SymbolRef Sym = dyn_cast<SymbolData>(LHS);
-  if (Sym) {
-    Adjustment = 0;
-  } else {
-    // Next, see if it's a "($sym+constant1)" expression.
-    const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS);
-
-    // We don't handle "($sym1+$sym2)".
-    // Give up and assume the constraint is feasible.
-    if (!SE)
-      return state;
-
-    // We don't handle "(<expr>+constant1)".
-    // Give up and assume the constraint is feasible.
-    Sym = dyn_cast<SymbolData>(SE->getLHS());
-    if (!Sym)
-      return state;
-
-    // Get the constant out of the expression "($sym+constant1)".
-    switch (SE->getOpcode()) {
-    case BO_Add:
-      Adjustment = SE->getRHS();
-      break;
-    case BO_Sub:
-      Adjustment = -SE->getRHS();
-      break;
-    default:
-      // We don't handle non-additive operators.
-      // Give up and assume the constraint is feasible.
-      return state;
-    }
-  }
+  // We only handle simple comparisons of the form "$sym == constant"
+  // or "($sym+constant1) == constant2".
+  // The adjustment is "constant1" in the above expression. It's used to
+  // "slide" the solution range around for modular arithmetic. For example,
+  // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
+  // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
+  // the subclasses of SimpleConstraintManager to handle the adjustment.
+  SymbolRef Sym = LHS;
+  llvm::APSInt Adjustment = computeAdjustment(LHS, Sym);
 
   // FIXME: This next section is a hack. It silently converts the integers to
   // be of the same type as the symbol, which is not always correct. Really the

clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

@@ -260,9 +260,10 @@ SVal SimpleSValBuilder::MakeSymIntVal(const SymExpr *LHS,
   // Wrap the LHS up in a NonLoc again and let evalCastFromNonLoc do the
   // dirty work.
   if (isIdempotent) {
-    if (SymbolRef LHSSym = dyn_cast<SymbolData>(LHS))
-      return evalCastFromNonLoc(nonloc::SymbolVal(LHSSym), resultTy);
-    return evalCastFromNonLoc(nonloc::SymExprVal(LHS), resultTy);
+    if (isa<SymbolData>(LHS))
+      return evalCastFromNonLoc(nonloc::SymbolVal(LHS), resultTy);
+    else
+      return evalCastFromNonLoc(nonloc::SymExprVal(LHS), resultTy);
   }
 
   // If we reach this point, the expression cannot be simplified.

clang/test/Analysis/out-of-bounds.c

@@ -128,13 +128,11 @@ void test2_multi_ok(int x) {
   buf[0][0] = 1; // no-warning
 }
 
-// *** FIXME ***
-// We don't get a warning here yet because our symbolic constraint solving
-// doesn't handle:  (symbol * constant) < constant
+// Testing if solver handles (symbol * constant) < constant
 void test3(int x) {
   int buf[100];
   if (x < 0)
-    buf[x] = 1; 
+    buf[x] = 1; // expected-warning {{Out of bound memory access (accessed memory precedes memory block)}}
 }
 
 // *** FIXME ***