[analyzer] Rework both constraint managers to handle mixed-type comparisons.

This involves keeping track of three separate types: the symbol type, the
adjustment type, and the comparison type. For example, in "$x + 5 > 0ULL",
if the type of $x is 'signed char', the adjustment type is 'int' and the
comparison type is 'unsigned long long'. Most of the time these three types
will be the same, but we should still do the right thing when the
comparison value is out of range, and wraparound should be calculated in
the adjustment type.

This also re-disables an out-of-bounds test; we were extracting the symbol
from non-additive SymIntExprs, but then throwing away the integer.

Sorry for the large patch; both the basic and range constraint managers needed
to be updated together, since they share code in SimpleConstraintManager.

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@156361 91177308-0d34-0410-b5e6-96231b3b80d8

10 files changed, 766 insertions, 219 deletions

diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h b/include/clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h
index dcb77792ff..e1ff17b361 100644
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h
+++ b/include/clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h
@@ -51,6 +51,11 @@ public:
     return Result;
   }
 
+  /// Returns an all-zero value for this type.
+  llvm::APSInt getZeroValue() const LLVM_READONLY {
+    return llvm::APSInt(BitWidth, IsUnsigned);
+  }
+
   /// Returns the minimum value for this type.
   llvm::APSInt getMinValue() const LLVM_READONLY {
     return llvm::APSInt::getMinValue(BitWidth, IsUnsigned);
@@ -61,6 +66,21 @@ public:
     return llvm::APSInt::getMaxValue(BitWidth, IsUnsigned);
   }
 
+  /// Used to classify whether a value is representable using this type.
+  ///
+  /// \see testInRange
+  enum RangeTestResultKind {
+    RTR_Below = -1, ///< Value is less than the minimum representable value.
+    RTR_Within = 0, ///< Value is representable using this type.
+    RTR_Above = 1   ///< Value is greater than the maximum representable value.
+  };
+
+  /// Tests whether a given value is losslessly representable using this type.
+  ///
+  /// Note that signedness conversions will be rejected, even with the same bit
+  /// pattern. For example, -1s8 is not in range for 'unsigned char' (u8).
+  RangeTestResultKind testInRange(const llvm::APSInt &Val) const LLVM_READONLY;
+  
   bool operator==(const APSIntType &Other) const {
     return BitWidth == Other.BitWidth && IsUnsigned == Other.IsUnsigned;
   }
diff --git a/lib/StaticAnalyzer/Core/APSIntType.cpp b/lib/StaticAnalyzer/Core/APSIntType.cpp
new file mode 100644
index 0000000000..884b0faa9e
--- /dev/null
+++ b/lib/StaticAnalyzer/Core/APSIntType.cpp
@@ -0,0 +1,38 @@
+//===--- APSIntType.cpp - Simple record of the type of APSInts ------------===//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
+
+using namespace clang;
+using namespace ento;
+
+APSIntType::RangeTestResultKind
+APSIntType::testInRange(const llvm::APSInt &Value) const {
+  // Negative numbers cannot be losslessly converted to unsigned type.
+  if (IsUnsigned && Value.isSigned() && Value.isNegative())
+    return RTR_Below;
+
+  // Signed integers can be converted to signed integers of the same width
+  // or (if positive) unsigned integers with one fewer bit.
+  // Unsigned integers can be converted to unsigned integers of the same width
+  // or signed integers with one more bit.
+  unsigned MinBits;
+  if (Value.isSigned())
+    MinBits = Value.getMinSignedBits() - IsUnsigned;
+  else
+    MinBits = Value.getActiveBits() + !IsUnsigned;
+
+  if (MinBits <= BitWidth)
+    return RTR_Within;
+
+  if (Value.isSigned() && Value.isNegative())
+    return RTR_Below;
+  else
+    return RTR_Above;
+}
diff --git a/lib/StaticAnalyzer/Core/BasicConstraintManager.cpp b/lib/StaticAnalyzer/Core/BasicConstraintManager.cpp
index 2d9addd2ce..7a095d57d2 100644
--- a/lib/StaticAnalyzer/Core/BasicConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/BasicConstraintManager.cpp
@@ -13,6 +13,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "SimpleConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
 #include "llvm/Support/raw_ostream.h"
@@ -53,18 +54,25 @@ class BasicConstraintManager
   ProgramState::IntSetTy::Factory ISetFactory;
 public:
   BasicConstraintManager(ProgramStateManager &statemgr, SubEngine &subengine)
-    : SimpleConstraintManager(subengine), 
+    : SimpleConstraintManager(subengine, statemgr.getBasicVals()),
       ISetFactory(statemgr.getAllocator()) {}
 
-  ProgramStateRef assumeSymNE(ProgramStateRef state,
-                                  SymbolRef sym,
-                                  const llvm::APSInt& V,
-                                  const llvm::APSInt& Adjustment);
+  ProgramStateRef assumeSymEquality(ProgramStateRef State, SymbolRef Sym,
+                                    const llvm::APSInt &V,
+                                    const llvm::APSInt &Adjustment,
+                                    bool Assumption);
 
-  ProgramStateRef assumeSymEQ(ProgramStateRef state,
-                                  SymbolRef sym,
-                                  const llvm::APSInt& V,
-                                  const llvm::APSInt& Adjustment);
+  ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              const llvm::APSInt &Adjustment) {
+    return assumeSymEquality(State, Sym, V, Adjustment, false);
+  }
+
+  ProgramStateRef assumeSymEQ(ProgramStateRef State, SymbolRef Sym,
+                              const llvm::APSInt &V,
+                              const llvm::APSInt &Adjustment) {
+    return assumeSymEquality(State, Sym, V, Adjustment, true);
+  }
 
   ProgramStateRef assumeSymLT(ProgramStateRef state,
                                   SymbolRef sym,
@@ -108,6 +116,9 @@ public:
   ProgramStateRef removeDeadBindings(ProgramStateRef state,
                                          SymbolReaper& SymReaper);
 
+  bool performTest(llvm::APSInt SymVal, llvm::APSInt Adjustment,
+                   BinaryOperator::Opcode Op, llvm::APSInt ComparisonVal);
+
   void print(ProgramStateRef state,
              raw_ostream &Out,
              const char* nl,
@@ -122,60 +133,94 @@ ento::CreateBasicConstraintManager(ProgramStateManager& statemgr,
   return new BasicConstraintManager(statemgr, subengine);
 }
 
-ProgramStateRef 
-BasicConstraintManager::assumeSymNE(ProgramStateRef state,
-                                    SymbolRef sym,
-                                    const llvm::APSInt &V,
-                                    const llvm::APSInt &Adjustment) {
-  // First, determine if sym == X, where X+Adjustment != V.
-  llvm::APSInt Adjusted = V-Adjustment;
-  if (const llvm::APSInt* X = getSymVal(state, sym)) {
-    bool isFeasible = (*X != Adjusted);
-    return isFeasible ? state : NULL;
-  }
-
-  // Second, determine if sym+Adjustment != V.
-  if (isNotEqual(state, sym, Adjusted))
-    return state;
-
-  // If we reach here, sym is not a constant and we don't know if it is != V.
-  // Make that assumption.
-  return AddNE(state, sym, Adjusted);
+// FIXME: This is a more general utility and should live somewhere else.
+bool BasicConstraintManager::performTest(llvm::APSInt SymVal,
+                                         llvm::APSInt Adjustment,
+                                         BinaryOperator::Opcode Op,
+                                         llvm::APSInt ComparisonVal) {
+  APSIntType Type(Adjustment);
+  Type.apply(SymVal);
+  Type.apply(ComparisonVal);
+  SymVal += Adjustment;
+
+  assert(BinaryOperator::isComparisonOp(Op));
+  BasicValueFactory &BVF = getBasicVals();
+  const llvm::APSInt *Result = BVF.evalAPSInt(Op, SymVal, ComparisonVal);
+  assert(Result && "Comparisons should always have valid results.");
+
+  return Result->getBoolValue();
 }
 
-ProgramStateRef 
-BasicConstraintManager::assumeSymEQ(ProgramStateRef state,
-                                    SymbolRef sym,
-                                    const llvm::APSInt &V,
-                                    const llvm::APSInt &Adjustment) {
-  // First, determine if sym == X, where X+Adjustment != V.
-  llvm::APSInt Adjusted = V-Adjustment;
-  if (const llvm::APSInt* X = getSymVal(state, sym)) {
-    bool isFeasible = (*X == Adjusted);
-    return isFeasible ? state : NULL;
+ProgramStateRef
+BasicConstraintManager::assumeSymEquality(ProgramStateRef State, SymbolRef Sym,
+                                          const llvm::APSInt &V,
+                                          const llvm::APSInt &Adjustment,
+                                          bool Assumption) {
+  // Before we do any real work, see if the value can even show up.
+  APSIntType AdjustmentType(Adjustment);
+  if (AdjustmentType.testInRange(V) != APSIntType::RTR_Within)
+    return Assumption ? NULL : State;
+
+  // Get the symbol type.
+  BasicValueFactory &BVF = getBasicVals();
+  ASTContext &Ctx = BVF.getContext();
+  APSIntType SymbolType = BVF.getAPSIntType(Sym->getType(Ctx));
+
+  // First, see if the adjusted value is within range for the symbol.
+  llvm::APSInt Adjusted = AdjustmentType.convert(V) - Adjustment;
+  if (SymbolType.testInRange(Adjusted) != APSIntType::RTR_Within)
+    return Assumption ? NULL : State;
+
+  // Now we can do things properly in the symbol space.
+  SymbolType.apply(Adjusted);
+
+  // Second, determine if sym == X, where X+Adjustment != V.
+  if (const llvm::APSInt *X = getSymVal(State, Sym)) {
+    bool IsFeasible = (*X == Adjusted);
+    return (IsFeasible == Assumption) ? State : NULL;
   }
 
-  // Second, determine if sym+Adjustment != V.
-  if (isNotEqual(state, sym, Adjusted))
-    return NULL;
+  // Third, determine if we already know sym+Adjustment != V.
+  if (isNotEqual(State, Sym, Adjusted))
+    return Assumption ? NULL : State;
 
-  // If we reach here, sym is not a constant and we don't know if it is == V.
-  // Make that assumption.
-  return AddEQ(state, sym, Adjusted);
+  // If we reach here, sym is not a constant and we don't know if it is != V.
+  // Make the correct assumption.
+  if (Assumption)
+    return AddEQ(State, Sym, Adjusted);
+  else
+    return AddNE(State, Sym, Adjusted);
 }
 
 // The logic for these will be handled in another ConstraintManager.
+// Approximate it here anyway by handling some edge cases.
 ProgramStateRef 
 BasicConstraintManager::assumeSymLT(ProgramStateRef state,
                                     SymbolRef sym,
                                     const llvm::APSInt &V,
                                     const llvm::APSInt &Adjustment) {
-  // Is 'V' the smallest possible value?
-  if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) {
+  APSIntType ComparisonType(V), AdjustmentType(Adjustment);
+
+  // Is 'V' out of range above the type?
+  llvm::APSInt Max = AdjustmentType.getMaxValue();
+  if (V > ComparisonType.convert(Max)) {
+    // This path is trivially feasible.
+    return state;
+  }
+
+  // Is 'V' the smallest possible value, or out of range below the type?
+  llvm::APSInt Min = AdjustmentType.getMinValue();
+  if (V <= ComparisonType.convert(Min)) {
     // sym cannot be any value less than 'V'.  This path is infeasible.
     return NULL;
   }
 
+  // Reject a path if the value of sym is a constant X and !(X+Adj < V).
+  if (const llvm::APSInt *X = getSymVal(state, sym)) {
+    bool isFeasible = performTest(*X, Adjustment, BO_LT, V);
+    return isFeasible ? state : NULL;
+  }
+
   // FIXME: For now have assuming x < y be the same as assuming sym != V;
   return assumeSymNE(state, sym, V, Adjustment);
 }
@@ -185,12 +230,28 @@ BasicConstraintManager::assumeSymGT(ProgramStateRef state,
                                     SymbolRef sym,
                                     const llvm::APSInt &V,
                                     const llvm::APSInt &Adjustment) {
-  // Is 'V' the largest possible value?
-  if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) {
+  APSIntType ComparisonType(V), AdjustmentType(Adjustment);
+
+  // Is 'V' the largest possible value, or out of range above the type?
+  llvm::APSInt Max = AdjustmentType.getMaxValue();
+  if (V >= ComparisonType.convert(Max)) {
     // sym cannot be any value greater than 'V'.  This path is infeasible.
     return NULL;
   }
 
+  // Is 'V' out of range below the type?
+  llvm::APSInt Min = AdjustmentType.getMinValue();
+  if (V < ComparisonType.convert(Min)) {
+    // This path is trivially feasible.
+    return state;
+  }
+
+  // Reject a path if the value of sym is a constant X and !(X+Adj > V).
+  if (const llvm::APSInt *X = getSymVal(state, sym)) {
+    bool isFeasible = performTest(*X, Adjustment, BO_GT, V);
+    return isFeasible ? state : NULL;
+  }
+
   // FIXME: For now have assuming x > y be the same as assuming sym != V;
   return assumeSymNE(state, sym, V, Adjustment);
 }
@@ -200,25 +261,33 @@ BasicConstraintManager::assumeSymGE(ProgramStateRef state,
                                     SymbolRef sym,
                                     const llvm::APSInt &V,
                                     const llvm::APSInt &Adjustment) {
-  // Reject a path if the value of sym is a constant X and !(X+Adj >= V).
-  if (const llvm::APSInt *X = getSymVal(state, sym)) {
-    bool isFeasible = (*X >= V-Adjustment);
-    return isFeasible ? state : NULL;
-  }
-
-  // Sym is not a constant, but it is worth looking to see if V is the
-  // maximum integer value.
-  if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) {
-    llvm::APSInt Adjusted = V-Adjustment;
+  APSIntType ComparisonType(V), AdjustmentType(Adjustment);
 
-    // If we know that sym != V (after adjustment), then this condition
-    // is infeasible since there is no other value greater than V.
-    bool isFeasible = !isNotEqual(state, sym, Adjusted);
+  // Is 'V' the largest possible value, or out of range above the type?
+  llvm::APSInt Max = AdjustmentType.getMaxValue();
+  ComparisonType.apply(Max);
 
-    // If the path is still feasible then as a consequence we know that
+  if (V > Max) {
+    // sym cannot be any value greater than 'V'.  This path is infeasible.
+    return NULL;
+  } else if (V == Max) {
+    // If the path is feasible then as a consequence we know that
     // 'sym+Adjustment == V' because there are no larger values.
     // Add this constraint.
-    return isFeasible ? AddEQ(state, sym, Adjusted) : NULL;
+    return assumeSymEQ(state, sym, V, Adjustment);
+  }
+
+  // Is 'V' out of range below the type?
+  llvm::APSInt Min = AdjustmentType.getMinValue();
+  if (V < ComparisonType.convert(Min)) {
+    // This path is trivially feasible.
+    return state;
+  }
+
+  // Reject a path if the value of sym is a constant X and !(X+Adj >= V).
+  if (const llvm::APSInt *X = getSymVal(state, sym)) {
+    bool isFeasible = performTest(*X, Adjustment, BO_GE, V);
+    return isFeasible ? state : NULL;
   }
 
   return state;
@@ -229,25 +298,33 @@ BasicConstraintManager::assumeSymLE(ProgramStateRef state,
                                     SymbolRef sym,
                                     const llvm::APSInt &V,
                                     const llvm::APSInt &Adjustment) {
-  // Reject a path if the value of sym is a constant X and !(X+Adj <= V).
-  if (const llvm::APSInt* X = getSymVal(state, sym)) {
-    bool isFeasible = (*X <= V-Adjustment);
-    return isFeasible ? state : NULL;
-  }
+  APSIntType ComparisonType(V), AdjustmentType(Adjustment);
 
-  // Sym is not a constant, but it is worth looking to see if V is the
-  // minimum integer value.
-  if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) {
-    llvm::APSInt Adjusted = V-Adjustment;
+  // Is 'V' out of range above the type?
+  llvm::APSInt Max = AdjustmentType.getMaxValue();
+  if (V > ComparisonType.convert(Max)) {
+    // This path is trivially feasible.
+    return state;
+  }
 
-    // If we know that sym != V (after adjustment), then this condition
-    // is infeasible since there is no other value less than V.
-    bool isFeasible = !isNotEqual(state, sym, Adjusted);
+  // Is 'V' the smallest possible value, or out of range below the type?
+  llvm::APSInt Min = AdjustmentType.getMinValue();
+  ComparisonType.apply(Min);
 
-    // If the path is still feasible then as a consequence we know that
+  if (V < Min) {
+    // sym cannot be any value less than 'V'.  This path is infeasible.
+    return NULL;
+  } else if (V == Min) {
+    // If the path is feasible then as a consequence we know that
     // 'sym+Adjustment == V' because there are no smaller values.
     // Add this constraint.
-    return isFeasible ? AddEQ(state, sym, Adjusted) : NULL;
+    return assumeSymEQ(state, sym, V, Adjustment);
+  }
+
+  // Reject a path if the value of sym is a constant X and !(X+Adj >= V).
+  if (const llvm::APSInt *X = getSymVal(state, sym)) {
+    bool isFeasible = performTest(*X, Adjustment, BO_LE, V);
+    return isFeasible ? state : NULL;
   }
 
   return state;
@@ -257,7 +334,7 @@ ProgramStateRef BasicConstraintManager::AddEQ(ProgramStateRef state,
                                                   SymbolRef sym,
                                              const llvm::APSInt& V) {
   // Create a new state with the old binding replaced.
-  return state->set<ConstEq>(sym, &state->getBasicVals().getValue(V));
+  return state->set<ConstEq>(sym, &getBasicVals().getValue(V));
 }
 
 ProgramStateRef BasicConstraintManager::AddNE(ProgramStateRef state,
@@ -269,7 +346,7 @@ ProgramStateRef BasicConstraintManager::AddNE(ProgramStateRef state,
   ProgramState::IntSetTy S = T ? *T : ISetFactory.getEmptySet();
 
   // Now add V to the NE set.
-  S = ISetFactory.add(S, &state->getBasicVals().getValue(V));
+  S = ISetFactory.add(S, &getBasicVals().getValue(V));
 
   // Create a new state with the old binding replaced.
   return state->set<ConstNotEq>(sym, S);
@@ -289,7 +366,7 @@ bool BasicConstraintManager::isNotEqual(ProgramStateRef state,
   const ConstNotEqTy::data_type* T = state->get<ConstNotEq>(sym);
 
   // See if V is present in the NE-set.
-  return T ? T->contains(&state->getBasicVals().getValue(V)) : false;
+  return T ? T->contains(&getBasicVals().getValue(V)) : false;
 }
 
 bool BasicConstraintManager::isEqual(ProgramStateRef state,
diff --git a/lib/StaticAnalyzer/Core/CMakeLists.txt b/lib/StaticAnalyzer/Core/CMakeLists.txt
index 1ea25bd01b..23d1dcc10b 100644
--- a/lib/StaticAnalyzer/Core/CMakeLists.txt
+++ b/lib/StaticAnalyzer/Core/CMakeLists.txt
@@ -4,6 +4,7 @@ set(LLVM_USED_LIBS clangBasic clangLex clangAST clangFrontend clangRewrite)
 
 add_clang_library(clangStaticAnalyzerCore
   AnalysisManager.cpp
+  APSIntType.cpp
   BasicConstraintManager.cpp
   BasicValueFactory.cpp
   BlockCounter.cpp
diff --git a/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index 98eb958e1e..550404a510 100644
--- a/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -13,6 +13,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "SimpleConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
 #include "llvm/Support/Debug.h"
@@ -143,6 +144,92 @@ private:
     }
   }
 
+  const llvm::APSInt &getMinValue() const {
+    assert(!isEmpty());
+    return ranges.begin()->From();
+  }
+
+  bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const {
+    // This function has nine cases, the cartesian product of range-testing
+    // both the upper and lower bounds against the symbol's type.
+    // Each case requires a different pinning operation.
+    // The function returns false if the described range is entirely outside
+    // the range of values for the associated symbol.
+    APSIntType Type(getMinValue());
+    APSIntType::RangeTestResultKind LowerTest = Type.testInRange(Lower);
+    APSIntType::RangeTestResultKind UpperTest = Type.testInRange(Upper);
+
+    switch (LowerTest) {
+    case APSIntType::RTR_Below:
+      switch (UpperTest) {
+      case APSIntType::RTR_Below:
+        // The entire range is outside the symbol's set of possible values.
+        // If this is a conventionally-ordered range, the state is infeasible.
+        if (Lower < Upper)
+          return false;
+
+        // However, if the range wraps around, it spans all possible values.
+        Lower = Type.getMinValue();
+        Upper = Type.getMaxValue();
+        break;
+      case APSIntType::RTR_Within:
+        // The range starts below what's possible but ends within it. Pin.
+        Lower = Type.getMinValue();
+        Type.apply(Upper);
+        break;
+      case APSIntType::RTR_Above:
+        // The range spans all possible values for the symbol. Pin.
+        Lower = Type.getMinValue();
+        Upper = Type.getMaxValue();
+        break;
+      }
+      break;
+    case APSIntType::RTR_Within:
+      switch (UpperTest) {
+      case APSIntType::RTR_Below:
+        // The range wraps around, but all lower values are not possible.
+        Type.apply(Lower);
+        Upper = Type.getMaxValue();
+        break;
+      case APSIntType::RTR_Within:
+        // The range may or may not wrap around, but both limits are valid.
+        Type.apply(Lower);
+        Type.apply(Upper);
+        break;
+      case APSIntType::RTR_Above:
+        // The range starts within what's possible but ends above it. Pin.
+        Type.apply(Lower);
+        Upper = Type.getMaxValue();
+        break;
+      }
+      break;
+    case APSIntType::RTR_Above:
+      switch (UpperTest) {
+      case APSIntType::RTR_Below:
+        // The range wraps but is outside the symbol's set of possible values.
+        return false;
+      case APSIntType::RTR_Within:
+        // The range starts above what's possible but ends within it (wrap).
+        Lower = Type.getMinValue();
+        Type.apply(Upper);
+        break;
+      case APSIntType::RTR_Above:
+        // The entire range is outside the symbol's set of possible values.
+        // If this is a conventionally-ordered range, the state is infeasible.
+        if (Lower < Upper)
+          return false;
+
+        // However, if the range wraps around, it spans all possible values.
+        Lower = Type.getMinValue();
+        Upper = Type.getMaxValue();
+        break;
+      }
+      break;
+    }
+
+    return true;
+  }
+
 public:
   // Returns a set containing the values in the receiving set, intersected with
   // the closed range [Lower, Upper]. Unlike the Range type, this range uses
@@ -152,8 +239,10 @@ public:
   // 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,
-                     const llvm::APSInt &Lower,
-                     const llvm::APSInt &Upper) const {
+                     llvm::APSInt Lower, llvm::APSInt Upper) const {
+    if (!pin(Lower, Upper))
+      return F.getEmptySet();
+
     PrimRangeSet newRanges = F.getEmptySet();
 
     PrimRangeSet::iterator i = begin(), e = end();
@@ -166,6 +255,7 @@ public:
       IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e);
       IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e);
     }
+
     return newRanges;
   }
 
@@ -206,8 +296,8 @@ namespace {
 class RangeConstraintManager : public SimpleConstraintManager{
   RangeSet GetRange(ProgramStateRef state, SymbolRef sym);
 public:
-  RangeConstraintManager(SubEngine &subengine)
-    : SimpleConstraintManager(subengine) {}
+  RangeConstraintManager(SubEngine &subengine, BasicValueFactory &BVF)
+    : SimpleConstraintManager(subengine, BVF) {}
 
   ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
                              const llvm::APSInt& Int,
@@ -252,9 +342,9 @@ private:
 
 } // end anonymous namespace
 
-ConstraintManager* ento::CreateRangeConstraintManager(ProgramStateManager&,
-                                                    SubEngine &subeng) {
-  return new RangeConstraintManager(subeng);
+ConstraintManager *
+ento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine &Eng) {
+  return new RangeConstraintManager(Eng, StMgr.getBasicVals());
 }
 
 const llvm::APSInt* RangeConstraintManager::getSymVal(ProgramStateRef St,
@@ -288,8 +378,8 @@ RangeConstraintManager::GetRange(ProgramStateRef state, SymbolRef sym) {
 
   // Lazily generate a new RangeSet representing all possible values for the
   // given symbol type.
-  QualType T = state->getSymbolManager().getType(sym);
-  BasicValueFactory& BV = state->getBasicVals();
+  BasicValueFactory &BV = getBasicVals();
+  QualType T = sym->getType(BV.getContext());
   return RangeSet(F, BV.getMinValue(T), BV.getMaxValue(T));
 }
 
@@ -306,117 +396,154 @@ RangeConstraintManager::GetRange(ProgramStateRef state, SymbolRef sym) {
 // UINT_MAX, 0, 1, and 2.
 
 ProgramStateRef 
-RangeConstraintManager::assumeSymNE(ProgramStateRef state, SymbolRef sym,
-                                    const llvm::APSInt& Int,
-                                    const llvm::APSInt& Adjustment) {
-  BasicValueFactory &BV = state->getBasicVals();
-
-  llvm::APSInt Lower = Int-Adjustment;
+RangeConstraintManager::assumeSymNE(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);
+  if (AdjustmentType.testInRange(Int) != APSIntType::RTR_Within)
+    return St;
+
+  llvm::APSInt Lower = AdjustmentType.convert(Int) - Adjustment;
   llvm::APSInt Upper = Lower;
   --Lower;
   ++Upper;
 
   // [Int-Adjustment+1, Int-Adjustment-1]
   // Notice that the lower bound is greater than the upper bound.
-  RangeSet New = GetRange(state, sym).Intersect(BV, F, Upper, Lower);
-  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Upper, Lower);
+  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
 }
 
 ProgramStateRef 
-RangeConstraintManager::assumeSymEQ(ProgramStateRef state, SymbolRef sym,
-                                    const llvm::APSInt& Int,
-                                    const llvm::APSInt& Adjustment) {
+RangeConstraintManager::assumeSymEQ(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);
+  if (AdjustmentType.testInRange(Int) != APSIntType::RTR_Within)
+    return NULL;
+
   // [Int-Adjustment, Int-Adjustment]
-  BasicValueFactory &BV = state->getBasicVals();
-  llvm::APSInt AdjInt = Int-Adjustment;
-  RangeSet New = GetRange(state, sym).Intersect(BV, F, AdjInt, AdjInt);
-  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+  llvm::APSInt AdjInt = AdjustmentType.convert(Int) - Adjustment;
+  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, AdjInt, AdjInt);
+  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
 }
 
 ProgramStateRef 
-RangeConstraintManager::assumeSymLT(ProgramStateRef state, SymbolRef sym,
-                                    const llvm::APSInt& Int,
-                                    const llvm::APSInt& Adjustment) {
-  BasicValueFactory &BV = state->getBasicVals();
-
-  QualType T = state->getSymbolManager().getType(sym);
-  const llvm::APSInt &Min = BV.getMinValue(T);
+RangeConstraintManager::assumeSymLT(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)) {
+  case APSIntType::RTR_Below:
+    return NULL;
+  case APSIntType::RTR_Within:
+    break;
+  case APSIntType::RTR_Above:
+    return St;
+  }
 
   // Special case for Int == Min. This is always false.
-  if (Int == Min)
+  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
+  llvm::APSInt Min = AdjustmentType.getMinValue();
+  if (ComparisonVal == Min)
     return NULL;
 
   llvm::APSInt Lower = Min-Adjustment;
-  llvm::APSInt Upper = Int-Adjustment;
+  llvm::APSInt Upper = ComparisonVal-Adjustment;
   --Upper;
 
-  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
-  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
 }
 
 ProgramStateRef 
-RangeConstraintManager::assumeSymGT(ProgramStateRef state, SymbolRef sym,
-                                    const llvm::APSInt& Int,
-                                    const llvm::APSInt& Adjustment) {
-  BasicValueFactory &BV = state->getBasicVals();
-
-  QualType T = state->getSymbolManager().getType(sym);
-  const llvm::APSInt &Max = BV.getMaxValue(T);
+RangeConstraintManager::assumeSymGT(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)) {
+  case APSIntType::RTR_Below:
+    return St;
+  case APSIntType::RTR_Within:
+    break;
+  case APSIntType::RTR_Above:
+    return NULL;
+  }
 
   // Special case for Int == Max. This is always false.
-  if (Int == Max)
+  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
+  llvm::APSInt Max = AdjustmentType.getMaxValue();
+  if (ComparisonVal == Max)
     return NULL;
 
-  llvm::APSInt Lower = Int-Adjustment;
+  llvm::APSInt Lower = ComparisonVal-Adjustment;
   llvm::APSInt Upper = Max-Adjustment;
   ++Lower;
 
-  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
-  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
 }
 
 ProgramStateRef 
-RangeConstraintManager::assumeSymGE(ProgramStateRef state, SymbolRef sym,
-                                    const llvm::APSInt& Int,
-                                    const llvm::APSInt& Adjustment) {
-  BasicValueFactory &BV = state->getBasicVals();
-
-  QualType T = state->getSymbolManager().getType(sym);
-  const llvm::APSInt &Min = BV.getMinValue(T);
+RangeConstraintManager::assumeSymGE(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)) {
+  case APSIntType::RTR_Below:
+    return St;
+  case APSIntType::RTR_Within:
+    break;
+  case APSIntType::RTR_Above:
+    return NULL;
+  }
 
   // Special case for Int == Min. This is always feasible.
-  if (Int == Min)
-    return state;
-
-  const llvm::APSInt &Max = BV.getMaxValue(T);
+  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
+  llvm::APSInt Min = AdjustmentType.getMinValue();
+  if (ComparisonVal == Min)
+    return St;
 
-  llvm::APSInt Lower = Int-Adjustment;
+  llvm::APSInt Max = AdjustmentType.getMaxValue();
+  llvm::APSInt Lower = ComparisonVal-Adjustment;
   llvm::APSInt Upper = Max-Adjustment;
 
-  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
-  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
 }
 
 ProgramStateRef 
-RangeConstraintManager::assumeSymLE(ProgramStateRef state, SymbolRef sym,
-                                    const llvm::APSInt& Int,
-                                    const llvm::APSInt& Adjustment) {
-  BasicValueFactory &BV = state->getBasicVals();
-
-  QualType T = state->getSymbolManager().getType(sym);
-  const llvm::APSInt &Max = BV.getMaxValue(T);
+RangeConstraintManager::assumeSymLE(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)) {
+  case APSIntType::RTR_Below:
+    return NULL;
+  case APSIntType::RTR_Within:
+    break;
+  case APSIntType::RTR_Above:
+    return St;
+  }
 
   // Special case for Int == Max. This is always feasible.
-  if (Int == Max)
-    return state;
-
-  const llvm::APSInt &Min = BV.getMinValue(T);
+  llvm::APSInt ComparisonVal = AdjustmentType.convert(Int);
+  llvm::APSInt Max = AdjustmentType.getMaxValue();
+  if (ComparisonVal == Max)
+    return St;
 
+  llvm::APSInt Min = AdjustmentType.getMinValue();
   llvm::APSInt Lower = Min-Adjustment;
-  llvm::APSInt Upper = Int-Adjustment;
+  llvm::APSInt Upper = ComparisonVal-Adjustment;
 
-  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
-  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+  RangeSet New = GetRange(St, Sym).Intersect(getBasicVals(), F, Lower, Upper);
+  return New.isEmpty() ? NULL : St->set<ConstraintRange>(Sym, New);
 }
 
 //===------------------------------------------------------------------------===
diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
index a76a2da001..92a8eb1a7a 100644
--- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -13,6 +13,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "SimpleConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"