ddcc updated this revision to Diff 78049.
ddcc added a comment.

Rebase on recent changes


https://reviews.llvm.org/D26061

Files:
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
  lib/StaticAnalyzer/Core/CMakeLists.txt
  lib/StaticAnalyzer/Core/ConstraintManager.cpp
  lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  lib/StaticAnalyzer/Core/RangedConstraintManager.h
  lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
  lib/StaticAnalyzer/Core/SimpleConstraintManager.h

Index: lib/StaticAnalyzer/Core/SimpleConstraintManager.h
===================================================================
--- lib/StaticAnalyzer/Core/SimpleConstraintManager.h
+++ /dev/null
@@ -1,121 +0,0 @@
-//== SimpleConstraintManager.h ----------------------------------*- C++ -*--==//
-//
-//                     The LLVM Compiler Infrastructure
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-//  Code shared between BasicConstraintManager and RangeConstraintManager.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_SIMPLECONSTRAINTMANAGER_H
-#define LLVM_CLANG_LIB_STATICANALYZER_CORE_SIMPLECONSTRAINTMANAGER_H
-
-#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
-
-namespace clang {
-
-namespace ento {
-
-class SimpleConstraintManager : public ConstraintManager {
-  SubEngine *SU;
-  SValBuilder &SVB;
-public:
-  SimpleConstraintManager(SubEngine *subengine, SValBuilder &SB)
-    : SU(subengine), SVB(SB) {}
-  ~SimpleConstraintManager() override;
-
-  //===------------------------------------------------------------------===//
-  // Common implementation for the interface provided by ConstraintManager.
-  //===------------------------------------------------------------------===//
-
-  ProgramStateRef assume(ProgramStateRef state, DefinedSVal Cond,
-                        bool Assumption) override;
-
-  ProgramStateRef assume(ProgramStateRef state, NonLoc Cond, bool Assumption);
-
-  ProgramStateRef assumeInclusiveRange(ProgramStateRef State,
-                                             NonLoc Value,
-                                             const llvm::APSInt &From,
-                                             const llvm::APSInt &To,
-                                             bool InRange) override;
-
-  ProgramStateRef assumeSymRel(ProgramStateRef state,
-                              const SymExpr *LHS,
-                              BinaryOperator::Opcode op,
-                              const llvm::APSInt& Int);
-
-  ProgramStateRef assumeSymWithinInclusiveRange(ProgramStateRef State,
-                                                SymbolRef Sym,
-                                                const llvm::APSInt &From,
-                                                const llvm::APSInt &To,
-                                                bool InRange);
-
-
-protected:
-
-  //===------------------------------------------------------------------===//
-  // Interface that subclasses must implement.
-  //===------------------------------------------------------------------===//
-
-  // Each of these is of the form "$sym+Adj <> V", where "<>" is the comparison
-  // operation for the method being invoked.
-  virtual ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
-                                     const llvm::APSInt& V,
-                                     const llvm::APSInt& Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym,
-                                     const llvm::APSInt& V,
-                                     const llvm::APSInt& Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym,
-                                     const llvm::APSInt& V,
-                                     const llvm::APSInt& Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym,
-                                     const llvm::APSInt& V,
-                                     const llvm::APSInt& Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym,
-                                     const llvm::APSInt& V,
-                                     const llvm::APSInt& Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym,
-                                     const llvm::APSInt& V,
-                                     const llvm::APSInt& Adjustment) = 0;
-
-
-  virtual ProgramStateRef assumeSymbolWithinInclusiveRange(
-      ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
-      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
-
-  virtual ProgramStateRef assumeSymbolOutOfInclusiveRange(
-      ProgramStateRef state, SymbolRef Sym, const llvm::APSInt &From,
-      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
-  //===------------------------------------------------------------------===//
-  // Internal implementation.
-  //===------------------------------------------------------------------===//
-
-  BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); }
-  SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
-
-  bool canReasonAbout(SVal X) const override;
-
-  ProgramStateRef assumeAux(ProgramStateRef state,
-                                NonLoc Cond,
-                                bool Assumption);
-
-  ProgramStateRef assumeAuxForSymbol(ProgramStateRef State,
-                                         SymbolRef Sym,
-                                         bool Assumption);
-};
-
-} // end GR namespace
-
-} // end clang namespace
-
-#endif
Index: lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -7,12 +7,12 @@
 //
 //===----------------------------------------------------------------------===//
 //
-//  This file defines SimpleConstraintManager, a class that holds code shared
-//  between BasicConstraintManager and RangeConstraintManager.
+//  This file defines SimpleConstraintManager, a class that provides a
+//  simplified constraint manager interface, compared to ConstraintManager.
 //
 //===----------------------------------------------------------------------===//
 
-#include "SimpleConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
@@ -23,54 +23,12 @@
 
 SimpleConstraintManager::~SimpleConstraintManager() {}
 
-bool SimpleConstraintManager::canReasonAbout(SVal X) const {
-  Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
-  if (SymVal && SymVal->isExpression()) {
-    const SymExpr *SE = SymVal->getSymbol();
-
-    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
-      switch (SIE->getOpcode()) {
-          // We don't reason yet about bitwise-constraints on symbolic values.
-        case BO_And:
-        case BO_Or:
-        case BO_Xor:
-          return false;
-        // We don't reason yet about these arithmetic constraints on
-        // symbolic values.
-        case BO_Mul:
-        case BO_Div:
-        case BO_Rem:
-        case BO_Shl:
-        case BO_Shr:
-          return false;
-        // All other cases.
-        default:
-          return true;
-      }
-    }
-
-    if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
-      if (BinaryOperator::isComparisonOp(SSE->getOpcode())) {
-        // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
-        if (Loc::isLocType(SSE->getLHS()->getType())) {
-          assert(Loc::isLocType(SSE->getRHS()->getType()));
-          return true;
-        }
-      }
-    }
-
-    return false;
-  }
-
-  return true;
-}
-
-ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
-                                               DefinedSVal Cond,
-                                               bool Assumption) {
+ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef State,
+                                                DefinedSVal Cond,
+                                                bool Assumption) {
   // If we have a Loc value, cast it to a bool NonLoc first.
   if (Optional<Loc> LV = Cond.getAs<Loc>()) {
-    SValBuilder &SVB = state->getStateManager().getSValBuilder();
+    SValBuilder &SVB = State->getStateManager().getSValBuilder();
     QualType T;
     const MemRegion *MR = LV->getAsRegion();
     if (const TypedRegion *TR = dyn_cast_or_null<TypedRegion>(MR))
@@ -81,115 +39,69 @@
     Cond = SVB.evalCast(*LV, SVB.getContext().BoolTy, T).castAs<DefinedSVal>();
   }
 
-  return assume(state, Cond.castAs<NonLoc>(), Assumption);
+  return assume(State, Cond.castAs<NonLoc>(), Assumption);
 }
 
-ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef state,
-                                               NonLoc cond,
-                                               bool assumption) {
-  state = assumeAux(state, cond, assumption);
+ProgramStateRef SimpleConstraintManager::assume(ProgramStateRef State,
+                                                NonLoc Cond, bool Assumption) {
+  State = assumeAux(State, Cond, Assumption);
   if (NotifyAssumeClients && SU)
-    return SU->processAssume(state, cond, assumption);
-  return state;
+    return SU->processAssume(State, Cond, Assumption);
+  return State;
 }
 
-
-ProgramStateRef
-SimpleConstraintManager::assumeAuxForSymbol(ProgramStateRef State,
-                                            SymbolRef Sym, bool Assumption) {
-  BasicValueFactory &BVF = getBasicVals();
-  QualType T = Sym->getType();
-
-  // None of the constraint solvers currently support non-integer types.
-  if (!T->isIntegralOrEnumerationType())
-    return State;
-
-  const llvm::APSInt &zero = BVF.getValue(0, T);
-  if (Assumption)
-    return assumeSymNE(State, Sym, zero, zero);
-  else
-    return assumeSymEQ(State, Sym, zero, zero);
-}
-
-ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
-                                                  NonLoc Cond,
-                                                  bool Assumption) {
+ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef State,
+                                                   NonLoc Cond,
+                                                   bool Assumption) {
 
   // We cannot reason about SymSymExprs, and can only reason about some
   // SymIntExprs.
   if (!canReasonAbout(Cond)) {
     // Just add the constraint to the expression without trying to simplify.
-    SymbolRef sym = Cond.getAsSymExpr();
-    return assumeAuxForSymbol(state, sym, Assumption);
+    SymbolRef Sym = Cond.getAsSymExpr();
+    assert(Sym);
+    return assumeSymUnsupported(State, Sym, Assumption);
   }
 
   switch (Cond.getSubKind()) {
   default:
     llvm_unreachable("'Assume' not implemented for this NonLoc");
 
   case nonloc::SymbolValKind: {
     nonloc::SymbolVal SV = Cond.castAs<nonloc::SymbolVal>();
-    SymbolRef sym = SV.getSymbol();
-    assert(sym);
-
-    // Handle SymbolData.
-    if (!SV.isExpression()) {
-      return assumeAuxForSymbol(state, sym, Assumption);
-
-    // Handle symbolic expression.
-    } else if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym)) {
-      // We can only simplify expressions whose RHS is an integer.
-
-      BinaryOperator::Opcode op = SE->getOpcode();
-      if (BinaryOperator::isComparisonOp(op)) {
-        if (!Assumption)
-          op = BinaryOperator::negateComparisonOp(op);
-
-        return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
-      }
-
-    } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(sym)) {
-      // Translate "a != b" to "(b - a) != 0".
-      // We invert the order of the operands as a heuristic for how loop
-      // conditions are usually written ("begin != end") as compared to length
-      // calculations ("end - begin"). The more correct thing to do would be to
-      // canonicalize "a - b" and "b - a", which would allow us to treat
-      // "a != b" and "b != a" the same.
-      SymbolManager &SymMgr = getSymbolManager();
-      BinaryOperator::Opcode Op = SSE->getOpcode();
-      assert(BinaryOperator::isComparisonOp(Op));
-
-      // For now, we only support comparing pointers.
-      assert(Loc::isLocType(SSE->getLHS()->getType()));
-      assert(Loc::isLocType(SSE->getRHS()->getType()));
-      QualType DiffTy = SymMgr.getContext().getPointerDiffType();
-      SymbolRef Subtraction = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub,
-                                                   SSE->getLHS(), DiffTy);
-
-      const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
-      Op = BinaryOperator::reverseComparisonOp(Op);
-      if (!Assumption)
-        Op = BinaryOperator::negateComparisonOp(Op);
-      return assumeSymRel(state, Subtraction, Op, Zero);
-    }
+    SymbolRef Sym = SV.getSymbol();
+    assert(Sym);
 
-    // If we get here, there's nothing else we can do but treat the symbol as
-    // opaque.
-    return assumeAuxForSymbol(state, sym, Assumption);
+    return assumeSym(State, Sym, Assumption);
   }
 
   case nonloc::ConcreteIntKind: {
     bool b = Cond.castAs<nonloc::ConcreteInt>().getValue() != 0;
     bool isFeasible = b ? Assumption : !Assumption;
-    return isFeasible ? state : nullptr;
+    return isFeasible ? State : nullptr;
   }
 
   case nonloc::LocAsIntegerKind:
-    return assume(state, Cond.castAs<nonloc::LocAsInteger>().getLoc(),
+    return assume(State, Cond.castAs<nonloc::LocAsInteger>().getLoc(),
                   Assumption);
   } // end switch
 }
 
+ProgramStateRef
+SimpleConstraintManager::assumeSymUnsupported(ProgramStateRef State,
+                                              SymbolRef Sym, bool Assumption) {
+  BasicValueFactory &BVF = getBasicVals();
+  QualType T = Sym->getType();
+
+  // None of the constraint solvers currently support non-integer types.
+  if (!T->isIntegralOrEnumerationType())
+    return State;
+
+  // Reverse the operation.
+  const llvm::APSInt &Zero = BVF.getValue(0, T);
+  return assumeSymRel(State, Sym, Assumption ? BO_NE : BO_EQ, Zero);
+}
+
 ProgramStateRef SimpleConstraintManager::assumeInclusiveRange(
     ProgramStateRef State, NonLoc Value, const llvm::APSInt &From,
     const llvm::APSInt &To, bool InRange) {
@@ -202,7 +114,7 @@
     // Just add the constraint to the expression without trying to simplify.
     SymbolRef Sym = Value.getAsSymExpr();
     assert(Sym);
-    return assumeSymWithinInclusiveRange(State, Sym, From, To, InRange);
+    return assumeSymInclusiveRange(State, Sym, From, To, InRange);
   }
 
   switch (Value.getSubKind()) {
@@ -213,7 +125,7 @@
   case nonloc::LocAsIntegerKind:
   case nonloc::SymbolValKind: {
     if (SymbolRef Sym = Value.getAsSymbol())
-      return assumeSymWithinInclusiveRange(State, Sym, From, To, InRange);
+      return assumeSymInclusiveRange(State, Sym, From, To, InRange);
     return State;
   } // end switch
 
@@ -226,109 +138,6 @@
   } // end switch
 }
 
-static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment) {
-  // Is it a "($sym+constant1)" expression?
-  if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
-    BinaryOperator::Opcode Op = SE->getOpcode();
-    if (Op == BO_Add || Op == BO_Sub) {
-      Sym = SE->getLHS();
-      Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
-
-      // Don't forget to negate the adjustment if it's being subtracted.
-      // This should happen /after/ promotion, in case the value being
-      // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
-      if (Op == BO_Sub)
-        Adjustment = -Adjustment;
-    }
-  }
-}
-
-ProgramStateRef SimpleConstraintManager::assumeSymRel(ProgramStateRef state,
-                                                     const SymExpr *LHS,
-                                                     BinaryOperator::Opcode op,
-                                                     const llvm::APSInt& Int) {
-  assert(BinaryOperator::isComparisonOp(op) &&
-         "Non-comparison ops should be rewritten as comparisons to zero.");
-
-  // Get the type used for calculating wraparound.
-  BasicValueFactory &BVF = getBasicVals();
-  APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType());
-
-  // 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 = WraparoundType.getZeroValue();
-  computeAdjustment(Sym, Adjustment);
-
-  // Convert the right-hand side integer as necessary.
-  APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
-  llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
-
-  // Prefer unsigned comparisons.
-  if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
-      ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
-    Adjustment.setIsSigned(false);
-
-  switch (op) {
-  default:
-    llvm_unreachable("invalid operation not caught by assertion above");
-
-  case BO_EQ:
-    return assumeSymEQ(state, Sym, ConvertedInt, Adjustment);
-
-  case BO_NE:
-    return assumeSymNE(state, Sym, ConvertedInt, Adjustment);
-
-  case BO_GT:
-    return assumeSymGT(state, Sym, ConvertedInt, Adjustment);
-
-  case BO_GE:
-    return assumeSymGE(state, Sym, ConvertedInt, Adjustment);
-
-  case BO_LT:
-    return assumeSymLT(state, Sym, ConvertedInt, Adjustment);
-
-  case BO_LE:
-    return assumeSymLE(state, Sym, ConvertedInt, Adjustment);
-  } // end switch
-}
-
-ProgramStateRef
-SimpleConstraintManager::assumeSymWithinInclusiveRange(ProgramStateRef State,
-                                                       SymbolRef Sym,
-                                                       const llvm::APSInt &From,
-                                                       const llvm::APSInt &To,
-                                                       bool InRange) {
-  // Get the type used for calculating wraparound.
-  BasicValueFactory &BVF = getBasicVals();
-  APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
-
-  llvm::APSInt Adjustment = WraparoundType.getZeroValue();
-  SymbolRef AdjustedSym = Sym;
-  computeAdjustment(AdjustedSym, Adjustment);
-
-  // Convert the right-hand side integer as necessary.
-  APSIntType ComparisonType = std::max(WraparoundType, APSIntType(From));
-  llvm::APSInt ConvertedFrom = ComparisonType.convert(From);
-  llvm::APSInt ConvertedTo = ComparisonType.convert(To);
-
-  // Prefer unsigned comparisons.
-  if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
-      ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
-    Adjustment.setIsSigned(false);
-
-  if (InRange)
-    return assumeSymbolWithinInclusiveRange(State, AdjustedSym, ConvertedFrom,
-                                            ConvertedTo, Adjustment);
-  return assumeSymbolOutOfInclusiveRange(State, AdjustedSym, ConvertedFrom,
-                                         ConvertedTo, Adjustment);
-}
-
 } // end of namespace ento
 
 } // end of namespace clang
Index: lib/StaticAnalyzer/Core/RangedConstraintManager.h
===================================================================
--- /dev/null
+++ lib/StaticAnalyzer/Core/RangedConstraintManager.h
@@ -0,0 +1,98 @@
+//== RangedConstraintManager.h ----------------------------------*- C++ -*--==//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+//  Ranged constraint manager, built on SimpleConstraintManager.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
+#define LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
+
+namespace clang {
+
+namespace ento {
+
+class RangedConstraintManager : public SimpleConstraintManager {
+public:
+  RangedConstraintManager(SubEngine *SE, SValBuilder &SB)
+      : SimpleConstraintManager(SE, SB) {}
+
+  ~RangedConstraintManager() override;
+
+  //===------------------------------------------------------------------===//
+  // Implementation for interface from SimpleConstraintManager.
+  //===------------------------------------------------------------------===//
+
+  ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
+                            bool Assumption) override;
+
+  ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym,
+                               BinaryOperator::Opcode op,
+                               const llvm::APSInt &Int) override;
+
+  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
+                                          const llvm::APSInt &From,
+                                          const llvm::APSInt &To,
+                                          bool InRange) override;
+
+protected:
+  //===------------------------------------------------------------------===//
+  // Interface that subclasses must implement.
+  //===------------------------------------------------------------------===//
+
+  // Each of these is of the form "$Sym+Adj <> V", where "<>" is the comparison
+  // operation for the method being invoked.
+
+  virtual ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym,
+                                      const llvm::APSInt &V,
+                                      const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymWithinInclusiveRange(
+      ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
+
+  virtual ProgramStateRef assumeSymOutsideInclusiveRange(
+      ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+      const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
+
+  //===------------------------------------------------------------------===//
+  // Internal implementation.
+  //===------------------------------------------------------------------===//
+private:
+  static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
+};
+
+} // end GR namespace
+
+} // end clang namespace
+
+#endif
Index: lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
===================================================================
--- /dev/null
+++ lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -0,0 +1,176 @@
+//== RangedConstraintManager.cpp --------------------------------*- C++ -*--==//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+//  This file defines RangedConstraintManager, a class that provides a
+//  range-based constraint manager interface.
+//
+//===----------------------------------------------------------------------===//
+
+#include "RangedConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+
+namespace clang {
+
+namespace ento {
+
+RangedConstraintManager::~RangedConstraintManager() {}
+
+ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
+                                                   SymbolRef Sym,
+                                                   bool Assumption) {
+  // Handle SymbolData.
+  if (isa<SymbolData>(Sym)) {
+    return assumeSymUnsupported(State, Sym, Assumption);
+
+    // Handle symbolic expression.
+  } else if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Sym)) {
+    // We can only simplify expressions whose RHS is an integer.
+
+    BinaryOperator::Opcode op = SIE->getOpcode();
+    if (BinaryOperator::isComparisonOp(op)) {
+      if (!Assumption)
+        op = BinaryOperator::negateComparisonOp(op);
+
+      return assumeSymRel(State, SIE->getLHS(), op, SIE->getRHS());
+    }
+
+  } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(Sym)) {
+    // Translate "a != b" to "(b - a) != 0".
+    // We invert the order of the operands as a heuristic for how loop
+    // conditions are usually written ("begin != end") as compared to length
+    // calculations ("end - begin"). The more correct thing to do would be to
+    // canonicalize "a - b" and "b - a", which would allow us to treat
+    // "a != b" and "b != a" the same.
+    SymbolManager &SymMgr = getSymbolManager();
+    BinaryOperator::Opcode Op = SSE->getOpcode();
+    assert(BinaryOperator::isComparisonOp(Op));
+
+    // For now, we only support comparing pointers.
+    assert(Loc::isLocType(SSE->getLHS()->getType()));
+    assert(Loc::isLocType(SSE->getRHS()->getType()));
+    QualType DiffTy = SymMgr.getContext().getPointerDiffType();
+    SymbolRef Subtraction =
+        SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy);
+
+    const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
+    Op = BinaryOperator::reverseComparisonOp(Op);
+    if (!Assumption)
+      Op = BinaryOperator::negateComparisonOp(Op);
+    return assumeSymRel(State, Subtraction, Op, Zero);
+  }
+
+  // If we get here, there's nothing else we can do but treat the symbol as
+  // opaque.
+  return assumeSymUnsupported(State, Sym, Assumption);
+}
+
+ProgramStateRef RangedConstraintManager::assumeSymRel(ProgramStateRef State,
+                                                      SymbolRef LHS,
+                                                      BinaryOperator::Opcode op,
+                                                      const llvm::APSInt &Int) {
+  assert(BinaryOperator::isComparisonOp(op) &&
+         "Non-comparison ops should be rewritten as comparisons to zero.");
+
+  // Get the type used for calculating wraparound.
+  BasicValueFactory &BVF = getBasicVals();
+  APSIntType WraparoundType = BVF.getAPSIntType(LHS->getType());
+
+  // 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 = WraparoundType.getZeroValue();
+  computeAdjustment(Sym, Adjustment);
+
+  // Convert the right-hand side integer as necessary.
+  APSIntType ComparisonType = std::max(WraparoundType, APSIntType(Int));
+  llvm::APSInt ConvertedInt = ComparisonType.convert(Int);
+
+  // Prefer unsigned comparisons.
+  if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
+      ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
+    Adjustment.setIsSigned(false);
+
+  switch (op) {
+  default:
+    llvm_unreachable("invalid operation not caught by assertion above");
+
+  case BO_EQ:
+    return assumeSymEQ(State, Sym, ConvertedInt, Adjustment);
+
+  case BO_NE:
+    return assumeSymNE(State, Sym, ConvertedInt, Adjustment);
+
+  case BO_GT:
+    return assumeSymGT(State, Sym, ConvertedInt, Adjustment);
+
+  case BO_GE:
+    return assumeSymGE(State, Sym, ConvertedInt, Adjustment);
+
+  case BO_LT:
+    return assumeSymLT(State, Sym, ConvertedInt, Adjustment);
+
+  case BO_LE:
+    return assumeSymLE(State, Sym, ConvertedInt, Adjustment);
+  } // end switch
+}
+
+ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
+    ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+    const llvm::APSInt &To, bool InRange) {
+  // Get the type used for calculating wraparound.
+  BasicValueFactory &BVF = getBasicVals();
+  APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
+
+  llvm::APSInt Adjustment = WraparoundType.getZeroValue();
+  SymbolRef AdjustedSym = Sym;
+  computeAdjustment(AdjustedSym, Adjustment);
+
+  // Convert the right-hand side integer as necessary.
+  APSIntType ComparisonType = std::max(WraparoundType, APSIntType(From));
+  llvm::APSInt ConvertedFrom = ComparisonType.convert(From);
+  llvm::APSInt ConvertedTo = ComparisonType.convert(To);
+
+  // Prefer unsigned comparisons.
+  if (ComparisonType.getBitWidth() == WraparoundType.getBitWidth() &&
+      ComparisonType.isUnsigned() && !WraparoundType.isUnsigned())
+    Adjustment.setIsSigned(false);
+
+  if (InRange)
+    return assumeSymWithinInclusiveRange(State, AdjustedSym, ConvertedFrom,
+                                         ConvertedTo, Adjustment);
+  return assumeSymOutsideInclusiveRange(State, AdjustedSym, ConvertedFrom,
+                                        ConvertedTo, Adjustment);
+}
+
+void RangedConstraintManager::computeAdjustment(SymbolRef &Sym,
+                                                llvm::APSInt &Adjustment) {
+  // Is it a "($sym+constant1)" expression?
+  if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(Sym)) {
+    BinaryOperator::Opcode Op = SE->getOpcode();
+    if (Op == BO_Add || Op == BO_Sub) {
+      Sym = SE->getLHS();
+      Adjustment = APSIntType(Adjustment).convert(SE->getRHS());
+
+      // Don't forget to negate the adjustment if it's being subtracted.
+      // This should happen /after/ promotion, in case the value being
+      // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
+      if (Op == BO_Sub)
+        Adjustment = -Adjustment;
+    }
+  }
+}
+
+} // end of namespace ento
+
+} // end of namespace clang
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -12,7 +12,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "SimpleConstraintManager.h"
+#include "RangedConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
@@ -27,22 +27,17 @@
 /// guarantee that from <= to.  Note that Range is immutable, so as not
 /// to subvert RangeSet's immutability.
 namespace {
-class Range : public std::pair<const llvm::APSInt*,
-                                                const llvm::APSInt*> {
+class Range : public std::pair<const llvm::APSInt *, const llvm::APSInt *> {
 public:
   Range(const llvm::APSInt &from, const llvm::APSInt &to)
-    : std::pair<const llvm::APSInt*, const llvm::APSInt*>(&from, &to) {
+      : std::pair<const llvm::APSInt *, const llvm::APSInt *>(&from, &to) {
     assert(from <= to);
   }
   bool Includes(const llvm::APSInt &v) const {
     return *first <= v && v <= *second;
   }
-  const llvm::APSInt &From() const {
-    return *first;
-  }
-  const llvm::APSInt &To() const {
-    return *second;
-  }
+  const llvm::APSInt &From() const { return *first; }
+  const llvm::APSInt &To() const { return *second; }
   const llvm::APSInt *getConcreteValue() const {
     return &From() == &To() ? &From() : nullptr;
   }
@@ -53,16 +48,15 @@
   }
 };
 
-
 class RangeTrait : public llvm::ImutContainerInfo<Range> {
 public:
   // When comparing if one Range is less than another, we should compare
   // the actual APSInt values instead of their pointers.  This keeps the order
   // consistent (instead of comparing by pointer values) and can potentially
   // be used to speed up some of the operations in RangeSet.
   static inline bool isLess(key_type_ref lhs, key_type_ref rhs) {
-    return *lhs.first < *rhs.first || (!(*rhs.first < *lhs.first) &&
-                                       *lhs.second < *rhs.second);
+    return *lhs.first < *rhs.first ||
+           (!(*rhs.first < *lhs.first) && *lhs.second < *rhs.second);
   }
 };
 
@@ -96,25 +90,23 @@
 
   /// Construct a new RangeSet representing '{ [from, to] }'.
   RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to)
-    : ranges(F.add(F.getEmptySet(), Range(from, to))) {}
+      : ranges(F.add(F.getEmptySet(), Range(from, to))) {}
 
   /// Profile - Generates a hash profile of this RangeSet for use
   ///  by FoldingSet.
   void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); }
 
   /// getConcreteValue - If a symbol is contrained to equal a specific integer
   ///  constant then this method returns that value.  Otherwise, it returns
   ///  NULL.
-  const llvm::APSInt* getConcreteValue() const {
+  const llvm::APSInt *getConcreteValue() const {
     return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : nullptr;
   }
 
 private:
   void IntersectInRange(BasicValueFactory &BV, Factory &F,
-                        const llvm::APSInt &Lower,
-                        const llvm::APSInt &Upper,
-                        PrimRangeSet &newRanges,
-                        PrimRangeSet::iterator &i,
+                        const llvm::APSInt &Lower, const llvm::APSInt &Upper,
+                        PrimRangeSet &newRanges, PrimRangeSet::iterator &i,
                         PrimRangeSet::iterator &e) const {
     // There are six cases for each range R in the set:
     //   1. R is entirely before the intersection range.
@@ -134,8 +126,8 @@
 
       if (i->Includes(Lower)) {
         if (i->Includes(Upper)) {
-          newRanges = F.add(newRanges, Range(BV.getValue(Lower),
-                                             BV.getValue(Upper)));
+          newRanges =
+              F.add(newRanges, Range(BV.getValue(Lower), BV.getValue(Upper)));
           break;
         } else
           newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To()));
@@ -243,8 +235,8 @@
   // range is taken to wrap around. This is equivalent to taking the
   // intersection with the two ranges [Min, Upper] and [Lower, Max],
   // or, alternatively, /removing/ all integers between Upper and Lower.
-  RangeSet Intersect(BasicValueFactory &BV, Factory &F,
-                     llvm::APSInt Lower, llvm::APSInt Upper) const {
+  RangeSet Intersect(BasicValueFactory &BV, Factory &F, llvm::APSInt Lower,
+                     llvm::APSInt Upper) const {
     if (!pin(Lower, Upper))
       return F.getEmptySet();
 
@@ -290,56 +282,69 @@
                                                              RangeSet))
 
 namespace {
-class RangeConstraintManager : public SimpleConstraintManager{
-  RangeSet GetRange(ProgramStateRef state, SymbolRef sym);
+class RangeConstraintManager : public RangedConstraintManager {
 public:
-  RangeConstraintManager(SubEngine *subengine, SValBuilder &SVB)
-    : SimpleConstraintManager(subengine, SVB) {}
+  RangeConstraintManager(SubEngine *SE, SValBuilder &SVB)
+      : RangedConstraintManager(SE, SVB) {}
+
+  //===------------------------------------------------------------------===//
+  // Implementation for interface from ConstraintManager.
+  //===------------------------------------------------------------------===//
 
-  ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
-                             const llvm::APSInt& Int,
-                             const llvm::APSInt& Adjustment) override;
+  bool canReasonAbout(SVal X) const override;
 
-  ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym,
-                             const llvm::APSInt& Int,
-                             const llvm::APSInt& Adjustment) override;
+  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
 
-  ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym,
-                             const llvm::APSInt& Int,
-                             const llvm::APSInt& Adjustment) override;
+  const llvm::APSInt *getSymVal(ProgramStateRef State,
+                                SymbolRef Sym) const override;
 
-  ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym,
-                             const llvm::APSInt& Int,
-                             const llvm::APSInt& Adjustment) override;
+  ProgramStateRef removeDeadBindings(ProgramStateRef State,
+                                     SymbolReaper &SymReaper) override;
 
-  ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym,
-                             const llvm::APSInt& Int,
-                             const llvm::APSInt& Adjustment) override;
+  void print(ProgramStateRef State, raw_ostream &Out, const char *nl,
+             const char *sep) override;
 
-  ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym,
-                             const llvm::APSInt& Int,
-                             const llvm::APSInt& Adjustment) override;
+  //===------------------------------------------------------------------===//
+  // Implementation for interface from RangedConstraintManager.
+  //===------------------------------------------------------------------===//
 
-  ProgramStateRef assumeSymbolWithinInclusiveRange(
-        ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
-        const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
+  ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              const llvm::APSInt &Adjustment) override;
 
-  ProgramStateRef assumeSymbolOutOfInclusiveRange(
-        ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
-        const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
+  ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              const llvm::APSInt &Adjustment) override;
 
-  const llvm::APSInt* getSymVal(ProgramStateRef St,
-                                SymbolRef sym) const override;
-  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
+  ProgramStateRef assumeSymLT(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              const llvm::APSInt &Adjustment) override;
+
+  ProgramStateRef assumeSymGT(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              const llvm::APSInt &Adjustment) override;
+
+  ProgramStateRef assumeSymLE(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              const llvm::APSInt &Adjustment) override;
+
+  ProgramStateRef assumeSymGE(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              const llvm::APSInt &Adjustment) override;
 
-  ProgramStateRef removeDeadBindings(ProgramStateRef St,
-                                     SymbolReaper& SymReaper) override;
+  ProgramStateRef assumeSymWithinInclusiveRange(
+      ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+      const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
 
-  void print(ProgramStateRef St, raw_ostream &Out,
-             const char* nl, const char *sep) override;
+  ProgramStateRef assumeSymOutsideInclusiveRange(
+      ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
+      const llvm::APSInt &To, const llvm::APSInt &Adjustment) override;
 
 private:
   RangeSet::Factory F;
+
+  RangeSet getRange(ProgramStateRef state, SymbolRef sym);
+
   RangeSet getSymLTRange(ProgramStateRef St, SymbolRef Sym,
                          const llvm::APSInt &Int,
                          const llvm::APSInt &Adjustment);
@@ -363,10 +368,46 @@
   return llvm::make_unique<RangeConstraintManager>(Eng, StMgr.getSValBuilder());
 }
 
-const llvm::APSInt* RangeConstraintManager::getSymVal(ProgramStateRef St,
-                                                      SymbolRef sym) const {
-  const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym);
-  return T ? T->getConcreteValue() : nullptr;
+bool RangeConstraintManager::canReasonAbout(SVal X) const {
+  Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
+  if (SymVal && SymVal->isExpression()) {
+    const SymExpr *SE = SymVal->getSymbol();
+
+    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
+      switch (SIE->getOpcode()) {
+      // We don't reason yet about bitwise-constraints on symbolic values.
+      case BO_And:
+      case BO_Or:
+      case BO_Xor:
+        return false;
+      // We don't reason yet about these arithmetic constraints on
+      // symbolic values.
+      case BO_Mul:
+      case BO_Div:
+      case BO_Rem:
+      case BO_Shl:
+      case BO_Shr:
+        return false;
+      // All other cases.
+      default:
+        return true;
+      }
+    }
+
+    if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
+      if (BinaryOperator::isComparisonOp(SSE->getOpcode())) {
+        // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
+        if (Loc::isLocType(SSE->getLHS()->getType())) {
+          assert(Loc::isLocType(SSE->getRHS()->getType()));
+          return true;
+        }
+      }
+    }
+
+    return false;
+  }
+
+  return true;
 }
 
 ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
@@ -393,11 +434,17 @@
   return ConditionTruthVal();
 }
 
+const llvm::APSInt *RangeConstraintManager::getSymVal(ProgramStateRef St,
+                                                      SymbolRef Sym) const {
+  const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(Sym);
+  return T ? T->getConcreteValue() : nullptr;
+}
+
 /// Scan all symbols referenced by the constraints. If the symbol is not alive
 /// as marked in LSymbols, mark it as dead in DSymbols.
 ProgramStateRef
 RangeConstraintManager::removeDeadBindings(ProgramStateRef state,
-                                           SymbolReaper& SymReaper) {
+                                           SymbolReaper &SymReaper) {
   bool Changed = false;
   ConstraintRangeTy CR = state->get<ConstraintRange>();
   ConstraintRangeTy::Factory &CRFactory = state->get_context<ConstraintRange>();
@@ -413,9 +460,9 @@
   return Changed ? state->set<ConstraintRange>(CR) : state;
 }
 
-RangeSet
-RangeConstraintManager::GetRange(ProgramStateRef state, SymbolRef sym) {
-  if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym))
+RangeSet RangeConstraintManager::getRange(ProgramStateRef state,
+                                          SymbolRef sym) {
+  if (ConstraintRangeTy::data_type *V = state->get<ConstraintRange>(sym))
     return *V;
 
   // Lazily generate a new RangeSet representing all possible values for the
@@ -429,14 +476,14 @@
   if (T->isReferenceType()) {
     APSIntType IntType = BV.getAPSIntType(T);
     Result = Result.Intersect(BV, F, ++IntType.getZeroValue(),
-                                     --IntType.getZeroValue());
+                              --IntType.getZeroValue());
   }
 
   return Result;
 }
 
 //===------------------------------------------------------------------------===
-// assumeSymX methods: public interface for RangeConstraintManager.
+// assumeSymX methods: protected interface for RangeConstraintManager.
 //===------------------------------------------------------------------------===/
 
 // The syntax for ranges below is mathematical, using [x, y] for closed ranges
@@ -463,7 +510,7 @@
 
   // [Int-Adjustment+1, Int-Adjustment-1]
   // Notice that the lower bound is greater than the upper bound.
-  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower);
+  RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower);
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
@@ -478,7 +525,7 @@
 
   // [Int-Adjustment, Int-Adjustment]
   llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
-  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt);
+  RangeSet New = getRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt);
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
@@ -494,7 +541,7 @@
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
-    return GetRange(St, Sym);
+    return getRange(St, Sym);
   }
 
   // Special case for Int == Min. This is always false.
@@ -507,7 +554,7 @@
   llvm::APSInt Upper = ComparisonVal - Adjustment;
   --Upper;
 
-  return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
 }
 
 ProgramStateRef
@@ -518,15 +565,15 @@
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
-RangeSet
-RangeConstraintManager::getSymGTRange(ProgramStateRef St, SymbolRef Sym,
-                                      const llvm::APSInt &Int,
-                                      const llvm::APSInt &Adjustment) {
+RangeSet RangeConstraintManager::getSymGTRange(ProgramStateRef St,
+                                               SymbolRef Sym,
+                                               const llvm::APSInt &Int,
+                                               const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
   switch (AdjustmentType.testInRange(Int, true)) {
   case APSIntType::RTR_Below:
-    return GetRange(St, Sym);
+    return getRange(St, Sym);
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
@@ -543,7 +590,7 @@
   llvm::APSInt Upper = Max - Adjustment;
   ++Lower;
 
-  return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
 }
 
 ProgramStateRef
@@ -554,15 +601,15 @@
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
-RangeSet
-RangeConstraintManager::getSymGERange(ProgramStateRef St, SymbolRef Sym,
-                                      const llvm::APSInt &Int,
-                                      const llvm::APSInt &Adjustment) {
+RangeSet RangeConstraintManager::getSymGERange(ProgramStateRef St,
+                                               SymbolRef Sym,
+                                               const llvm::APSInt &Int,
+                                               const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
   switch (AdjustmentType.testInRange(Int, true)) {
   case APSIntType::RTR_Below:
-    return GetRange(St, Sym);
+    return getRange(St, Sym);
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
@@ -573,13 +620,13 @@
   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
   llvm::APSInt Min = AdjustmentType.getMinValue();
   if (ComparisonVal == Min)
-    return GetRange(St, Sym);
+    return getRange(St, Sym);
 
   llvm::APSInt Max = AdjustmentType.getMaxValue();
   llvm::APSInt Lower = ComparisonVal - Adjustment;
   llvm::APSInt Upper = Max - Adjustment;
 
-  return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
 }
 
 ProgramStateRef
@@ -590,10 +637,9 @@
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
-RangeSet
-RangeConstraintManager::getSymLERange(const RangeSet &RS,
-                                      const llvm::APSInt &Int,
-                                      const llvm::APSInt &Adjustment) {
+RangeSet RangeConstraintManager::getSymLERange(const RangeSet &RS,
+                                               const llvm::APSInt &Int,
+                                               const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
   switch (AdjustmentType.testInRange(Int, true)) {
@@ -618,32 +664,32 @@
   return RS.Intersect(getBasicVals(), F, Lower, Upper);
 }
 
-RangeSet
-RangeConstraintManager::getSymLERange(ProgramStateRef St, SymbolRef Sym,
-                                      const llvm::APSInt &Int,
-                                      const llvm::APSInt &Adjustment) {
+RangeSet RangeConstraintManager::getSymLERange(ProgramStateRef St,
+                                               SymbolRef Sym,
+                                               const llvm::APSInt &Int,
+                                               const llvm::APSInt &Adjustment) {
   // Before we do any real work, see if the value can even show up.
   APSIntType AdjustmentType(Adjustment);
   switch (AdjustmentType.testInRange(Int, true)) {
   case APSIntType::RTR_Below:
     return F.getEmptySet();
   case APSIntType::RTR_Within:
     break;
   case APSIntType::RTR_Above:
-    return GetRange(St, Sym);
+    return getRange(St, Sym);
   }
 
   // Special case for Int == Max. This is always feasible.
   llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
   llvm::APSInt Max = AdjustmentType.getMaxValue();
   if (ComparisonVal == Max)
-    return GetRange(St, Sym);
+    return getRange(St, Sym);
 
   llvm::APSInt Min = AdjustmentType.getMinValue();
   llvm::APSInt Lower = Min - Adjustment;
   llvm::APSInt Upper = ComparisonVal - Adjustment;
 
-  return GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return getRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
 }
 
 ProgramStateRef
@@ -654,8 +700,7 @@
   return New.isEmpty() ? nullptr : St->set<ConstraintRange>(Sym, New);
 }
 
-ProgramStateRef
-RangeConstraintManager::assumeSymbolWithinInclusiveRange(
+ProgramStateRef RangeConstraintManager::assumeSymWithinInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
   RangeSet New = getSymGERange(State, Sym, From, Adjustment);
@@ -665,8 +710,7 @@
   return New.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, New);
 }
 
-ProgramStateRef
-RangeConstraintManager::assumeSymbolOutOfInclusiveRange(
+ProgramStateRef RangeConstraintManager::assumeSymOutsideInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
   RangeSet RangeLT = getSymLTRange(State, Sym, From, Adjustment);
@@ -680,7 +724,7 @@
 //===------------------------------------------------------------------------===/
 
 void RangeConstraintManager::print(ProgramStateRef St, raw_ostream &Out,
-                                   const char* nl, const char *sep) {
+                                   const char *nl, const char *sep) {
 
   ConstraintRangeTy Ranges = St->get<ConstraintRange>();
 
@@ -690,7 +734,8 @@
   }
 
   Out << nl << sep << "Ranges of symbol values:";
-  for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){
+  for (ConstraintRangeTy::iterator I = Ranges.begin(), E = Ranges.end(); I != E;
+       ++I) {
     Out << nl << ' ' << I.getKey() << " : ";
     I.getData().print(Out);
   }
Index: lib/StaticAnalyzer/Core/ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/ConstraintManager.cpp
@@ -20,8 +20,8 @@
 
 static DefinedSVal getLocFromSymbol(const ProgramStateRef &State,
                                     SymbolRef Sym) {
-  const MemRegion *R = State->getStateManager().getRegionManager()
-                                               .getSymbolicRegion(Sym);
+  const MemRegion *R =
+      State->getStateManager().getRegionManager().getSymbolicRegion(Sym);
   return loc::MemRegionVal(R);
 }
 
Index: lib/StaticAnalyzer/Core/CMakeLists.txt
===================================================================
--- lib/StaticAnalyzer/Core/CMakeLists.txt
+++ lib/StaticAnalyzer/Core/CMakeLists.txt
@@ -34,6 +34,7 @@
   PlistDiagnostics.cpp
   ProgramState.cpp
   RangeConstraintManager.cpp
+  RangedConstraintManager.cpp
   RegionStore.cpp
   SValBuilder.cpp
   SVals.cpp
Index: include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
===================================================================
--- /dev/null
+++ include/clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h
@@ -0,0 +1,100 @@
+//== SimpleConstraintManager.h ----------------------------------*- C++ -*--==//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+//
+//  Simplified constraint manager backend.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H
+#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SIMPLECONSTRAINTMANAGER_H
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+
+namespace clang {
+
+namespace ento {
+
+class SimpleConstraintManager : public ConstraintManager {
+  SubEngine *SU;
+  SValBuilder &SVB;
+
+public:
+  SimpleConstraintManager(SubEngine *subengine, SValBuilder &SB)
+      : SU(subengine), SVB(SB) {}
+
+  ~SimpleConstraintManager() override;
+
+  //===------------------------------------------------------------------===//
+  // Implementation for interface from ConstraintManager.
+  //===------------------------------------------------------------------===//
+
+  /// Ensures that the DefinedSVal conditional is expressed as a NonLoc by
+  /// creating boolean casts to handle Loc's.
+  ProgramStateRef assume(ProgramStateRef State, DefinedSVal Cond,
+                         bool Assumption) override;
+
+  ProgramStateRef assumeInclusiveRange(ProgramStateRef State, NonLoc Value,
+                                       const llvm::APSInt &From,
+                                       const llvm::APSInt &To,
+                                       bool InRange) override;
+
+protected:
+  /// Given a symbolic expression that cannot be reasoned about, assume that
+  /// it is zero/nonzero and add it directly to the solver state.
+  virtual ProgramStateRef assumeSymUnsupported(ProgramStateRef State,
+                                               SymbolRef Sym, bool Assumption);
+
+  //===------------------------------------------------------------------===//
+  // Interface that subclasses must implement.
+  //===------------------------------------------------------------------===//
+
+  /// Given a symbolic expression that can be reasoned about, assume that it is
+  /// true/false and generate the new program state.
+  virtual ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym,
+                                    bool Assumption) = 0;
+
+  /// Assume a constraint between a symbolic expression and a concrete integer.
+  /// Used to directly add unsupported constraints to the solver state.
+  virtual ProgramStateRef assumeSymRel(ProgramStateRef State, SymbolRef Sym,
+                                       BinaryOperator::Opcode op,
+                                       const llvm::APSInt &Int) = 0;
+
+  /// Given a symbolic expression within the range [From, To], assume that it is
+  /// true/false and generate the new program state.
+  /// This function is used to handle case ranges produced by a language
+  /// extension
+  /// for switch case statements.
+  virtual ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State,
+                                                  SymbolRef Sym,
+                                                  const llvm::APSInt &From,
+                                                  const llvm::APSInt &To,
+                                                  bool InRange) = 0;
+
+  //===------------------------------------------------------------------===//
+  // Internal implementation.
+  //===------------------------------------------------------------------===//
+
+  BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); }
+  SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
+
+private:
+  ProgramStateRef assume(ProgramStateRef State, NonLoc Cond,
+                         bool Assumption);
+
+  ProgramStateRef assumeAux(ProgramStateRef State, NonLoc Cond,
+                            bool Assumption);
+
+};
+
+} // end GR namespace
+
+} // end clang namespace
+
+#endif
Index: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -139,6 +139,8 @@
     return nullptr;
   }
 
+  /// Scan all symbols referenced by the constraints. If the symbol is not
+  /// alive, remove it.
   virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
                                                  SymbolReaper& SymReaper) = 0;
 
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to