Lets keep trying with this here equation system.

Still not there, but more non-functional code is there.

Splitting blocks into sub-blocks now works, as does some of the guard stuff and
the general "shape" of the resulting equation system.

16 files changed, 902 insertions, 122 deletions

diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#EquationSystem.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/.#EquationSystem.hpp
deleted file mode 120000
index 56b9060..0000000
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#EquationSystem.hpp
+++ /dev/null
@@ -1 +0,0 @@
-carlo@pc-4w14-0.cs.usyd.edu.au.4300:1348200365
\ No newline at end of file
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#EquationSystem_flymake.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/.#EquationSystem_flymake.hpp
deleted file mode 120000
index 4dc56be..0000000
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#EquationSystem_flymake.hpp
+++ /dev/null
@@ -1 +0,0 @@
-carlo@pc-4w14-0.cs.usyd.edu.au.9390:1348126501
\ No newline at end of file
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Expression.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Expression.hpp
deleted file mode 120000
index 4dc56be..0000000
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Expression.hpp
+++ /dev/null
@@ -1 +0,0 @@
-carlo@pc-4w14-0.cs.usyd.edu.au.9390:1348126501
\ No newline at end of file
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Expression_flymake.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Expression_flymake.hpp
deleted file mode 120000
index 4dc56be..0000000
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Expression_flymake.hpp
+++ /dev/null
@@ -1 +0,0 @@
-carlo@pc-4w14-0.cs.usyd.edu.au.9390:1348126501
\ No newline at end of file
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Operator_flymake.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Operator_flymake.hpp
deleted file mode 120000
index 4dc56be..0000000
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/.#Operator_flymake.hpp
+++ /dev/null
@@ -1 +0,0 @@
-carlo@pc-4w14-0.cs.usyd.edu.au.9390:1348126501
\ No newline at end of file
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp
index 701da7c..d95366d 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp
@@ -91,22 +91,18 @@ struct EquationSystem {
   void indexMaxExpressions() {
     _expr_to_var = new IdMap<MaxExpression<Domain>,Variable<Domain>*>(maxExpressionCount(), NULL); 
     for (unsigned int i = 0, length = _right_sides.size(); i < length; ++i) {
-      _right_sides[i]->mapTo(*_variables[i], *_expr_to_var);
+      if (_right_sides[i])
+        _right_sides[i]->mapTo(*_variables[i], *_expr_to_var);
     }
   }
 
   Variable<Domain>* varFromExpr(const Expression<Domain>& expr) const {
-    if (_expr_to_var) { // we've indexed:
-      const MaxExpression<Domain>* maxExpr = expr.toMaxExpression();//dynamic_cast<const MaxExpression<Domain>*>(&expr);
-      if (maxExpr) {
-        return (*_expr_to_var)[*maxExpr];
-      } else {
-        return NULL;
-      }
+    assert(_expr_to_var != NULL); // ensure we've indexed
+    const MaxExpression<Domain>* maxExpr = expr.toMaxExpression();//dynamic_cast<const MaxExpression<Domain>*>(&expr);
+    if (maxExpr) {
+      return (*_expr_to_var)[*maxExpr];
     } else {
-      std::cout << "throw exception" << *(char*)NULL;
       return NULL;
-      //throw "Must index max expressions before attempting lookup";
     }
   }
 
@@ -125,7 +121,10 @@ struct EquationSystem {
     for (unsigned int i = 0, length = _variables.size();
          i < length;
          ++i) {
-      cout << *_variables[i] << " = " << *_right_sides[i] << std::endl;
+      if (_right_sides[i])
+        cout << *_variables[i] << " = " << *_right_sides[i] << std::endl;
+      else
+        cout << *_variables[i] << " = NULL" << std::endl;
     }
   }
 
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp
index 7b0f2cf..c4ee4c0 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp
@@ -84,7 +84,9 @@ struct Variable : public Expression<Domain> {
 template<typename Domain>
 struct OperatorExpression : public Expression<Domain> {
   OperatorExpression(const Operator<Domain>& op, const std::vector<Expression<Domain>*>& arguments)
-    : _operator(op), _arguments(arguments) { }
+    : _operator(op), _arguments(arguments) {
+    assert(!arguments.empty());
+  }
 
   virtual Domain eval(const VariableAssignment<Domain>& rho) const {
     std::vector<Domain> argumentValues;
@@ -145,7 +147,6 @@ struct MaxExpression : public OperatorExpression<Domain> {
   MaxExpression(const unsigned int& id, const Maximum<Domain>& op, const std::vector<Expression<Domain>*>& arguments)
     : OperatorExpression<Domain>(op, arguments), _id(id) { }
 
-
   const MaxExpression* toMaxExpression() const {
     return this;
   }
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp
index 27c0806..5e3aa3b 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/IdMap.hpp
@@ -7,7 +7,7 @@ template<typename T, typename V>
 struct IdMap {
   IdMap(unsigned int length, V initial)
     : _length(length), _assignment(new V[length]) {
-    for (unsigned int i = 0; i < _length; ++i) {
+    for (unsigned int i = 0; i < length; ++i) {
       _assignment[i] = initial;
     }
   }
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp
index b67591f..08c66ff 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Operator.hpp
@@ -28,6 +28,11 @@ struct Maximum : public Operator<Domain> {
   }
 };
 
+
+template<class T>
+T minimum(const T& l, const T& r) {
+  return (l < r ? l : r);
+}
 template<typename Domain>
 struct Minimum : public Operator<Domain> {
   virtual Domain eval(const std::vector<Domain>& arguments) const {
@@ -35,7 +40,7 @@ struct Minimum : public Operator<Domain> {
     for (typename std::vector<Domain>::const_iterator it = arguments.begin();
          it != arguments.end();
          ++it) {
-      result = (*it < result ? *it : result);
+      result = minimum(*it, result); //*it < result ? *it : result);
     }
     return result;
   }
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
index d2adff5..0bbebfc 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
@@ -47,6 +47,8 @@ private:
       solver_log::fixpoint << indent() << "Stabilise " << x << std::endl;
 
       stack_depth++;
+      if (!_system[x])
+        return;
       Domain val = _system[x]->eval(DependencyAssignment(*this, x),
                                     _strategy);
       stack_depth--;
diff --git a/clang/include/clang/Frontend/Analyses.def b/clang/include/clang/Frontend/Analyses.def
index b5b9394..902575f 100644
--- a/clang/include/clang/Frontend/Analyses.def
+++ b/clang/include/clang/Frontend/Analyses.def
@@ -23,6 +23,7 @@ ANALYSIS_STORE(RegionStore, "region", "Use region-based analyzer store", CreateR
 
 ANALYSIS_CONSTRAINTS(BasicConstraints, "basic", "Use basic constraint tracking", CreateBasicConstraintManager)
 ANALYSIS_CONSTRAINTS(RangeConstraints, "range", "Use constraint tracking of concrete value ranges", CreateRangeConstraintManager)
+ANALYSIS_CONSTRAINTS(IntervalConstraints, "interval", "Use constraint tracking of intervals", CreateIntervalConstraintManager)
 
 #ifndef ANALYSIS_DIAGNOSTICS
 #define ANALYSIS_DIAGNOSTICS(NAME, CMDFLAG, DESC, CREATEFN, AUTOCREATE)
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
index 631858d..4051cfc 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -73,6 +73,8 @@ ConstraintManager* CreateBasicConstraintManager(ProgramStateManager& statemgr,
                                                 SubEngine &subengine);
 ConstraintManager* CreateRangeConstraintManager(ProgramStateManager& statemgr,
                                                 SubEngine &subengine);
+ConstraintManager* CreateIntervalConstraintManager(ProgramStateManager& statemgr,
+                                                   SubEngine &subengine);
 
 } // end GR namespace
 
diff --git a/clang/lib/Analysis/.#Interval.cpp b/clang/lib/Analysis/.#Interval.cpp
deleted file mode 120000
index 235903b..0000000
--- a/clang/lib/Analysis/.#Interval.cpp
+++ /dev/null
@@ -1 +0,0 @@
-carlo@pc-4w14-0.cs.usyd.edu.au.1585:1347012043
\ No newline at end of file
diff --git a/clang/lib/Analysis/.#Interval_flymake.cpp b/clang/lib/Analysis/.#Interval_flymake.cpp
deleted file mode 120000
index 235903b..0000000
--- a/clang/lib/Analysis/.#Interval_flymake.cpp
+++ /dev/null
@@ -1 +0,0 @@
-carlo@pc-4w14-0.cs.usyd.edu.au.1585:1347012043
\ No newline at end of file
diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp
index 726c6de..96dd841 100644
--- a/clang/lib/Analysis/Interval.cpp
+++ b/clang/lib/Analysis/Interval.cpp
@@ -17,12 +17,10 @@
 #include <algorithm>
 #include <vector>
 #include <map>
+#include <set>
 
 using namespace clang;
 
-typedef EquationSystem<Complete<int> > EqnSys;
-typedef Expression<Complete<int> > EqnExpr;
-
 #include <sstream>
 template<typename T>
 std::string toString(const T& obj) {
@@ -31,6 +29,28 @@ std::string toString(const T& obj) {
   return stream.str();
 }
 
+#include <ostream>
+template<typename K,typename V>
+std::ostream& operator<<(std::ostream& cout, const std::pair<K,V>& v) {
+  cout << "(" << v.first << ", " << v.second << ")";
+  return cout;
+}
+
+template<typename K,typename V>
+std::ostream& operator<<(std::ostream& cout, const std::map<K,V>& v) {
+  cout << "{";
+  for (typename std::map<K,V>::const_iterator it = v.begin(), ei = v.end();
+       it != ei;
+       ++it) {
+    if (it != v.begin())
+      cout << ", ";
+    cout << it->first << ": " << it->second;
+  }
+  cout << "}";
+  return cout;  
+}
+
+
 IntervalAnalysis :: IntervalAnalysis(AnalysisDeclContext &context)
   : context(&context) {
 }
@@ -48,9 +68,89 @@ IntervalAnalysis :: ~IntervalAnalysis() {
 // Hooray!
 
 typedef Complete<int64_t> ZBar;
-typedef std::map<std::string, ZBar> Vector;
+//typedef std::map<std::string, ZBar> Vector;
+
+struct Vector : public std::map<std::string, ZBar> {
+  Vector(const ZBar& val=infinity<ZBar>())
+    : _val(val) { }
+  ZBar operator[](const std::string& key) const {
+    if (this->find(key) != this->end())
+      return this->find(key)->second;
+    return _val;
+  }
+  ZBar& operator[](const std::string& key) {
+    if (this->find(key) != this->end())
+      return this->find(key)->second;
+    std::pair<iterator,bool> p = this->insert(std::pair<const std::string, ZBar>(key, _val));
+    return p.first->second;
+  }
+  ZBar _val;
+};
+
 typedef std::pair<Vector, ZBar> Result; // a "slice" of an equation
 
+//typedef std::map<std::string, Result> LinearEquation; // one `Result` per variable
+struct LinearEquation : public std::map<std::string, Result> {
+  Result operator[](const std::string& key) const {
+    if (this->find(key) != this->end())
+      return this->find(key)->second;
+    Result r;
+    r.first[key] = 1;
+    r.second = 0;
+    return r;
+  }
+  Result& operator[](const std::string& key) {
+    if (this->find(key) != this->end())
+      return this->find(key)->second;
+    Result r;
+    r.first[key] = 1;
+    r.second = 0;
+    std::pair<iterator,bool> p = this->insert(std::pair<const std::string, Result>(key, r));
+    return p.first->second;
+  }
+};
+
+typedef Vector Condition;
+
+typedef EquationSystem<Vector> EqnSys;
+typedef Expression<Vector> EqnExpr;
+typedef Variable<Vector> EqnVar;
+
+
+struct LinearOperator : public Operator<Vector> {
+  LinearOperator(const LinearEquation& result)
+    : _values(result) {}
+
+  Vector eval(const std::vector<Vector>& vector) const {
+    assert(vector.size() == 1);
+    const Vector& v = vector[0];
+    Vector result = v;
+    for (LinearEquation::const_iterator it = _values.begin(),
+           ei = _values.end();
+         it != ei;
+         ++it) {
+      ZBar subresult = 0;
+      for (Vector::const_iterator jt = it->second.first.begin(),
+             ej = it->second.first.end();
+           jt != ej;
+           ++jt) {
+        subresult += jt->second * v[jt->first];
+      }
+      subresult += it->second.second;
+      result[it->first] = subresult;
+    }
+    return result;
+  }
+
+  void print(std::ostream& cout) const {
+    cout << "linear[" << _values << "]";
+  }
+
+  LinearEquation _values;
+};
+
+
+
 template<class F, class M>
 void transform_values(const F& f, M& map) {
   for (typename M::iterator it = map.begin(),
@@ -90,6 +190,14 @@ M merge_maps_with(const F& f, const M& left, const M& right) {
   return result;
 }
 
+template<>
+Vector minimum(const Vector& l, const Vector& r) {
+  return merge_maps_with(minimum<ZBar>, l, r);
+}
+template<class T>
+T max(const T& l, const T& r) {
+  return (l < r ? l : r);
+}
 template<class T>
 T negate(const T& v) {
   return -v;
@@ -98,25 +206,90 @@ template<class T>
 T addValues(const T& l, const T& r) {
   return l + r;
 }
-template<class T>
-T subValues(const T& l, const T& r) {
-  return l - r;
+
+Vector operator-(const Vector& vector) {
+  Vector result(-vector._val);
+  for (Vector::const_iterator it = vector.begin(),
+         ei = vector.end();
+       it != ei;
+       ++it) {
+    result[it->first] = -it->second;
+  }
+  return result;
+}
+
+Vector operator+(const Vector& left, const Vector& right) {
+  return merge_maps_with(addValues<ZBar>, left, right);
+}
+
+Vector operator-(const Vector& left, const Vector& right) {
+  return merge_maps_with(addValues<ZBar>, left, -right);
+}
+
+Vector operator*(const Vector& left, const ZBar& right) {
+  Vector result;
+  for (Vector::const_iterator it = left.begin(),
+         ei = left.end();
+       it != ei;
+       ++it) {
+    result[it->first] = (it->second * right);
+  }
+  return result;
+}
+Vector operator*(const ZBar& left, const Vector& right) {
+  return right * left;
+}
+bool operator<(const Vector& left, const Vector& right) {
+  for (Vector::const_iterator it = left.begin(),
+         ei = left.end();
+       it != ei;
+       ++it) {
+    if (it->second < right[it->first]) {
+      return true;
+    }
+  }
+  for (Vector::const_iterator it = right.begin(),
+         ei = right.end();
+       it != ei;
+       ++it) {
+    if (left[it->first] < it->second) {
+      return true;
+    }
+  }
+  return false;
+}
+
+template<>
+Vector infinity<Vector>() {
+  return Vector(infinity<ZBar>());
+}
+
+std::ostream& operator<<(std::ostream& cout, const Vector& v) {
+  cout << "{";
+  for (Vector::const_iterator it = v.begin(), ei = v.end();
+       it != ei;
+       ++it) {
+    cout << it->first << ": " << it->second << ", ";
+  }
+  cout << "_: " << v._val;
+  cout << "}";
+  return cout;
 }
 
 
-Result fromStmt(const Stmt*, EqnSys&);
+Result fromStmt(const Stmt*);
 
-Result fromInteger(const IntegerLiteral* expr, EqnSys& system) {
+Result fromInteger(const IntegerLiteral* expr) {
   return Result(Vector(), *expr->getValue().getRawData());
 }
 
-Result fromDeclExpr(const DeclRefExpr* expr, EqnSys& system) {
+Result fromDeclExpr(const DeclRefExpr* expr) {
   Vector val;
   val[expr->getNameInfo().getAsString()] = 1;
   return Result(val, 0);
 }
 
-Result fromUnary(const UnaryOperator* op, EqnSys& system) {
+Result fromUnary(const UnaryOperator* op) {
   switch (op->getOpcode()) {
   case UO_PreInc:
     break;
@@ -126,18 +299,16 @@ Result fromUnary(const UnaryOperator* op, EqnSys& system) {
   return Result(Vector(), 0);
 }
 
-
-Addition<Complete<int> >* add = new Addition<Complete<int> >();
-Subtraction<Complete<int> >* sub = new Subtraction<Complete<int> >();
-Multiplication<Complete<int> >* mul = new Multiplication<Complete<int> >();
-
-Result fromBinary(const BinaryOperator* op, EqnSys& system) {
-  Result left = fromStmt(op->getLHS()->IgnoreParenCasts(), system);
-  Result right = fromStmt(op->getRHS()->IgnoreParenCasts(), system);
+Result fromBinary(const BinaryOperator* op) {
+  Result left = fromStmt(op->getLHS()->IgnoreParenCasts());
+  Result right = fromStmt(op->getRHS()->IgnoreParenCasts());
   
   switch (op->getOpcode()) {
+  case BO_Assign:
+    return right;
   case BO_Sub:
     transform_values(negate<ZBar>, right.first);
+    right.second *= -1;
   case BO_Add:
     {
       Result result;
@@ -160,11 +331,27 @@ Result fromBinary(const BinaryOperator* op, EqnSys& system) {
         scalar = right.second;
         value = left;
       }
-      for (Vector::iterator it = value.first.begin(),
-             ei = value.first.end();
-           it != ei;
-           ++it) {
-        it->second *= scalar;
+      if (scalar > 0) {
+        for (Vector::iterator it = value.first.begin(),
+               ei = value.first.end();
+             it != ei;
+             ++it) {
+          it->second *= scalar;
+        }
+      } else {
+        Vector newValue;
+        for (Vector::iterator it = value.first.begin(),
+               ei = value.first.end();
+             it != ei;
+             ++it) {
+          std::string name;
+          if (it->first[0] == '-') {
+            name = it->first.substr(1);
+          } else {
+            name = '-' + it->first;
+          }
+          newValue[name] = (-scalar) * it->second;
+        }
       }
       right.second *= scalar;
       return value;
@@ -178,21 +365,7 @@ Result fromBinary(const BinaryOperator* op, EqnSys& system) {
   return Result();
 }
 
-Result fromDeclStmt(const DeclStmt* stmt, EqnSys& system) {
-  /*for (DeclStmt::const_decl_iterator it = stmt->decl_begin(),
-                                     ei = stmt->decl_end();
-       it != ei;
-       ++it) {
-    if ((*it)->getKind() == Decl::Var) {
-      const VarDecl* decl = static_cast<const VarDecl*>(*it);
-      Variable<Complete<int> > var = system.variable(decl->getNameAsString());
-      std::vector<EqnExpr*> args;
-      args.push_back(&system.constant(-infinity<Complete<int> >()));
-      args.push_back(fromStmt(decl->getInit(), system));
-      system[var] = &system.maxExpression(args);
-    }
-  }*/
-
+Result fromDeclStmt(const DeclStmt* stmt) {
   for (DeclStmt::const_decl_iterator it = stmt->decl_begin(),
                                      ei = stmt->decl_end();
        it != ei;
@@ -201,110 +374,272 @@ Result fromDeclStmt(const DeclStmt* stmt, EqnSys& system) {
       const VarDecl* decl = static_cast<const VarDecl*>(*it);
       llvm::errs() << decl->getNameAsString() << " = ";
 
-      Result expr = fromStmt(decl->getInit(), system);
-      llvm::errs() << "<{ ";
+      Result expr = fromStmt(decl->getInit());
       for (Vector::iterator it = expr.first.begin(),
              ei = expr.first.end();
            it != ei;
            ++it) {
         if (it != expr.first.begin())
-          llvm::errs() << ", ";
-        llvm::errs() << toString(it->first) << " = " << toString(it->second);
+          llvm::errs() << " + ";
+        llvm::errs() << toString(it->second) << "*" << toString(it->first);
       }
-      llvm::errs() << " }, " << toString(expr.second) << ">\n";
+      llvm::errs() << " + " << toString(expr.second) << "\n";
+
+
+      llvm::errs() << "-" << decl->getNameAsString() << " = ";
+      for (Vector::iterator it = expr.first.begin(),
+             ei = expr.first.end();
+           it != ei;
+           ++it) {
+        if (it != expr.first.begin())
+          llvm::errs() << " + ";
+        llvm::errs() << toString(it->second) << "*" << toString(it->first);
+      }
+      llvm::errs() << " - " << toString(expr.second) << "\n";
     }
   }
 
   return Result();
 }
 
-Result fromAssignment(const BinaryOperator* op, EqnSys& system) {
-  /*EqnExpr* left = fromStmt(op->getLHS()->IgnoreParenCasts(), system);
-  EqnExpr* right = fromStmt(op->getRHS()->IgnoreParenCasts(), system);
-  Variable<Complete<int> >* var = static_cast<Variable<Complete<int> >*>(left);
-
-  std::vector<EqnExpr*> args;
-  args.push_back(&system.constant(-infinity<Complete<int> >()));
-  args.push_back(right);
-  if (system[*var] != NULL)
-    args.push_back(system[*var]);
-    system[*var] = &system.maxExpression(args);*/
-  
+Result fromAssignment(const BinaryOperator* op) {
   const Expr* left = op->getLHS()->IgnoreParenCasts();
   if (left->getStmtClass() == Stmt::DeclRefExprClass) {
     std::string name = static_cast<const DeclRefExpr*>(left)->getNameInfo().getAsString();
 
-    Result expr = fromStmt(op->getRHS()->IgnoreParenCasts(), system);
-    llvm::errs() << name << " = <{ ";
+    Result expr = fromStmt(op->getRHS()->IgnoreParenCasts());
+    llvm::errs() << name << " = ";
     for (Vector::iterator it = expr.first.begin(),
            ei = expr.first.end();
          it != ei;
          ++it) {
       if (it != expr.first.begin())
-        llvm::errs() << ", ";
-      llvm::errs() << toString(it->first) << " = " << toString(it->second);
+        llvm::errs() << " + ";
+      llvm::errs() << toString(it->second) << "*" << toString(it->first);
     }
-    llvm::errs() << " }, " << toString(expr.second) << ">\n";
+    llvm::errs() << " + " << toString(expr.second) << "\n";
     return expr;
   }
   return Result();
 }
 
-Result fromStmt(const Stmt* stmt, EqnSys& system) {
+Result fromStmt(const Stmt* stmt) {
   if (!stmt)
     return Result();
+  //stmt->dump();
   switch (stmt->getStmtClass()) {
   case Stmt::IntegerLiteralClass:
-    return fromInteger(static_cast<const IntegerLiteral*>(stmt), system);
+    return fromInteger(static_cast<const IntegerLiteral*>(stmt));
   case Stmt::DeclRefExprClass:
-    return fromDeclExpr(static_cast<const DeclRefExpr*>(stmt), system);
+    return fromDeclExpr(static_cast<const DeclRefExpr*>(stmt));
   case Stmt::UnaryOperatorClass:
-    return fromUnary(static_cast<const UnaryOperator*>(stmt), system);
+    return fromUnary(static_cast<const UnaryOperator*>(stmt));
   case Stmt::DeclStmtClass:
-    return fromDeclStmt(static_cast<const DeclStmt*>(stmt), system);
+    return fromDeclStmt(static_cast<const DeclStmt*>(stmt));
   case Stmt::BinaryOperatorClass:
-    {
-      const BinaryOperator* binop = static_cast<const BinaryOperator*>(stmt);
-      if (binop->isAssignmentOp())
-        return fromAssignment(binop, system);
-      else
-        return fromBinary(binop, system);
-    }
+    return fromBinary(static_cast<const BinaryOperator*>(stmt));
+  }
+  const Expr* expr = dyn_cast<const Expr>(stmt);
+  if (expr) {
+    const Expr* expr2 = expr->IgnoreParenCasts();
+    if (expr != expr2)
+      return fromStmt(expr2);
   }
+  llvm::errs() << "we shouldn't get here...\n";
   return Result();
 }
 
-void runOnBlock(std::string id, const CFGBlock* block, EqnSys& system) {
+Condition fromComparison(const BinaryOperator* op) {
+  if (op->isRelationalOp()) {
+    const Expr* left = op->getLHS()->IgnoreParenCasts();
+    const Expr* right = op->getRHS()->IgnoreParenCasts();
+
+    Condition cond;
+    std::string name;
+    int64_t value;
+    if (left->getStmtClass() == Stmt::DeclRefExprClass) {
+      if (right->getStmtClass() == Stmt::IntegerLiteralClass) {
+        name = static_cast<const DeclRefExpr*>(left)->getNameInfo().getAsString();
+        value = *static_cast<const IntegerLiteral*>(right)->getValue().getRawData();
+        switch (op->getOpcode()) {
+        case BO_LT:
+          cond[name] = value - 1;
+          break;
+        case BO_LE:
+          cond[name] = value;
+          break;
+        case BO_GE:
+          cond['-' + name] = -value;
+          break;
+        case BO_GT:
+          cond['-' + name] = -(value + 1);
+          break;
+        }
+        return cond;
+      } else {
+        return Condition();
+      }
+    } else if (right->getStmtClass() == Stmt::DeclRefExprClass) {
+      if (left->getStmtClass() == Stmt::IntegerLiteralClass) {
+        name = static_cast<const DeclRefExpr*>(right)->getNameInfo().getAsString();
+        value = *static_cast<const IntegerLiteral*>(left)->getValue().getRawData();
+        switch (op->getOpcode()) {
+        case BO_LT:
+          cond['-' + name] = -(value + 1);
+          break;
+        case BO_LE:
+          cond['-' + name] = -value;
+          break;
+        case BO_GE:
+          cond[name] = value;
+          break;
+        case BO_GT:
+          cond[name] = value - 1;
+          break;
+        }
+        return cond;
+      } else {
+        return Condition();
+      }
+    }
+    return Condition();
+  }
+  return Condition();
+}
+
+std::map<const CFGBlock*, EqnVar*> seen_blocks;
+EqnVar* runOnBlock(const CFGBlock* block, EqnSys& system) {
+  if (seen_blocks.find(block) != seen_blocks.end())
+    return seen_blocks.find(block)->second;
+
+  std::string id = toString(block->getBlockID());
+  unsigned int counter = 0;
+  
+  // detemine equations for this block
+  LinearEquation eqn;
+  EqnVar* var;
+  Result current;
+
+  var = &system.variable(id);
   for (CFGBlock::const_iterator it = block->begin(),
                                 ei = block->end();
        it != ei;
        ++it) {
     const CFGStmt* cfg_stmt = it->getAs<CFGStmt>();
-    Result expr = fromStmt(cfg_stmt->getStmt(), system);
-    /*llvm::errs() << "<{ ";
-    for (Vector::iterator it = expr.first.begin(),
-           ei = expr.first.end();
-         it != ei;
-         ++it) {
-      if (it != expr.first.begin())
-        llvm::errs() << ", ";
-      llvm::errs() << toString(it->first) << " = " << toString(it->second);
+    const Stmt* stmt = cfg_stmt->getStmt();
+
+    std::string name = "";
+    Result expr;
+    if (stmt->getStmtClass() == Stmt::BinaryOperatorClass) {
+      const BinaryOperator* binop = static_cast<const BinaryOperator*>(stmt);
+      if (binop->isAssignmentOp()) {
+        const Expr* left = binop->getLHS()->IgnoreParenCasts();
+        const Expr* right = binop->getRHS()->IgnoreParenCasts();
+        if (left->getStmtClass() == Stmt::DeclRefExprClass) {
+          name = static_cast<const DeclRefExpr*>(left)->getNameInfo().getAsString();
+          expr = fromStmt(right);
+        }
+      }
+    } else if (stmt->getStmtClass() == Stmt::DeclStmtClass) {
+      stmt->dump();
+      const DeclStmt* decl_stmt = static_cast<const DeclStmt*>(stmt);
+      for (DeclStmt::const_decl_iterator jt = decl_stmt->decl_begin(),
+             ej = decl_stmt->decl_end();
+           jt != ej;
+           ++jt) {
+        if ((*jt)->getKind() == Decl::Var) {
+          const VarDecl* decl = static_cast<const VarDecl*>(*jt);
+          name = decl->getNameAsString();
+          expr = fromStmt(decl->getInit());
+          if (jt+1 != ej) {
+            llvm::errs() << "Only the first declaration in a multi-declaration statement is used.\n";
+          }
+          llvm::errs() << "Name: " << name << "\n";
+          llvm::errs() << toString(expr) << "\n";
+          break; // only take the first one, for now
+        } else {
+          llvm::errs() << (*jt)->getDeclKindName() << "\n";
+        }
+      }
     }
-    llvm::errs() << "}, " << toString(expr.second) << ">\n";*/
+    if (name == "")
+      continue;
+
+    // by here we expect `name` and `expr` to be set correctly
+
+    bool newBlock = false;
+    for (Vector::const_iterator jt = expr.first.begin(),
+           ej = expr.first.end();
+         jt != ej;
+         ++jt) {
+      // new block if we read from any variable we've already written to
+      newBlock |= (eqn.find(jt->first) != eqn.end());
+    }
+
+    if (newBlock) {
+      EqnVar* lastVar = var;
+      var = &system.variable(id + "-" + toString(++counter));
+
+      // the linear expression
+      std::vector<EqnExpr*> args;
+      args.push_back(lastVar);
+      EqnExpr* expr = &system.expression(new LinearOperator(eqn), args);
+
+      // the max expression
+      std::vector<EqnExpr*> maxArgs;
+      maxArgs.push_back(&system.constant(-infinity<Vector>()));
+      maxArgs.push_back(expr);
+      system[*var] = &system.maxExpression(args);
+      eqn = LinearEquation();
+    }
+
+    eqn[name] = expr;
+    expr.first = expr.first;
+    expr.second = -expr.second;
+    eqn["-"+name] = expr;
   }
-  fromStmt(block->getTerminatorCondition(), system);
 
-  /*if (terminator.getStmt() != NULL) {
-    if (terminator.getStmt()->getStmtClass() == Stmt::IfStmtClass) {
-      const IfStmt* if_stmt = static_cast<const IfStmt*>(terminator.getStmt());
-      llvm::errs() << "If: \n";
-      if_stmt->dump();
+  EqnVar* lastVar = var;
+  var = &system.variable(id + "-" + toString(++counter));
+
+  // the linear expression
+  std::vector<EqnExpr*> args;
+  args.push_back(lastVar);
+  EqnExpr* expr = &system.expression(new LinearOperator(eqn), args);
+
+  // the max expression
+  std::vector<EqnExpr*> maxArgs;
+  maxArgs.push_back(&system.constant(-infinity<Vector>()));
+  maxArgs.push_back(expr);
+  system[*var] = &system.maxExpression(maxArgs);
+
+  // save the last variable we used (the final values from this block)
+  seen_blocks[block] = var;
+
+  // determine predecessor variables/conditions
+  // we have to do this last to prevent an infinite loop situation
+  std::vector<EqnExpr*> preArgs;
+  for (CFGBlock::const_pred_iterator it = block->pred_begin(),
+         ei = block->pred_end();
+       it != ei;
+       ++it) {
+    if ((*it)->getTerminatorCondition()) {
+      const BinaryOperator* binop = static_cast<const BinaryOperator*>((*it)->getTerminatorCondition());
+      std::vector<EqnExpr*> args;
+      args.push_back(&system.constant(fromComparison(binop)));
+      args.push_back(runOnBlock(*it, system));
+      preArgs.push_back(&system.expression(new Minimum<Vector>(), args));
     } else {
-      llvm::errs() << "\n";
-      terminator.getStmt()->dump();
+      preArgs.push_back(runOnBlock(*it, system));
     }
-    }*/
-  return; // TODO: return a generated expression
+  }
+  EqnVar* preVar = &system.variable(id);
+  if (preArgs.empty())
+    preArgs.push_back(&system.constant(infinity<Vector>()));
+  system[*preVar] = &system.maxExpression(preArgs);
+
+  // return the final value we used
+  return var;
 }
 
 void IntervalAnalysis::runOnAllBlocks() {
@@ -324,16 +659,16 @@ void IntervalAnalysis::runOnAllBlocks() {
       todo.pop_front();
       continue;
     }
-    llvm::errs() << (void*)block << "\n";
+    llvm::errs() << block->getBlockID() << "\n";
     seen.insert(block);
     todo.pop_front();
-    runOnBlock(toString(block), block, system);
+    runOnBlock(block, system);
     llvm::errs() << "-> ";
     for (CFGBlock::const_succ_iterator it = block->succ_begin(),
                                        ei = block->succ_end();
          it != ei;
          it++ ) {
-      llvm::errs() << (void*) *it << ", ";
+      llvm::errs() << (*it)->getBlockID() << ", ";
       todo.push_back(*it);
     }
     llvm::errs() << "\n\n";
@@ -344,12 +679,12 @@ void IntervalAnalysis::runOnAllBlocks() {
   llvm::errs() << toString(system) << "\n";
 
   system.indexMaxExpressions();
-  DynamicMaxStrategy<Complete<int> > strategy(system);
-  DynamicVariableAssignment<Complete<int> > rho(system, strategy);
+  DynamicMaxStrategy<Vector> strategy(system);
+  DynamicVariableAssignment<Vector> rho(system, strategy);
   strategy.setRho(rho);
 
   for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
-    Variable<Complete<int> >& var = system.variable(i);
+    Variable<Vector>& var = system.variable(i);
     llvm::errs() << toString(var.name()) << " = " << toString(rho[var]) << "\n";
   }
 
diff --git a/clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp
new file mode 100644
index 0000000..9d04720
--- /dev/null
+++ b/clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp
@@ -0,0 +1,442 @@
+//== IntervalConstraintManager.cpp - Manage range constraints.------*- 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 IntervalConstraintManager, a class that tracks simple
+//  equality and inequality constraints on symbolic values of ProgramState.
+//
+//===----------------------------------------------------------------------===//
+
+#include "SimpleConstraintManager.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
+#include "llvm/Support/Debug.h"
+#include "llvm/ADT/FoldingSet.h"
+#include "llvm/ADT/ImmutableSet.h"
+#include "llvm/Support/raw_ostream.h"
+
+using namespace clang;
+using namespace ento;
+
+namespace { class ConstraintRange {}; }
+static int ConstraintRangeIndex = 0;
+
+/// A Range represents the closed range [from, to].  The caller must
+/// 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*> {
+public:
+  Range(const llvm::APSInt &from, const llvm::APSInt &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 *getConcreteValue() const {
+    return &From() == &To() ? &From() : NULL;
+  }
+
+  void Profile(llvm::FoldingSetNodeID &ID) const {
+    ID.AddPointer(&From());
+    ID.AddPointer(&To());
+  }
+};
+
+
+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);
+  }
+};
+
+/// RangeSet contains a set of ranges. If the set is empty, then
+///  there the value of a symbol is overly constrained and there are no
+///  possible values for that symbol.
+class RangeSet {
+  typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet;
+  PrimRangeSet ranges; // no need to make const, since it is an
+                       // ImmutableSet - this allows default operator=
+                       // to work.
+public:
+  typedef PrimRangeSet::Factory Factory;
+  typedef PrimRangeSet::iterator iterator;
+
+  RangeSet(PrimRangeSet RS) : ranges(RS) {}
+
+  iterator begin() const { return ranges.begin(); }
+  iterator end() const { return ranges.end(); }
+
+  bool isEmpty() const { return ranges.isEmpty(); }
+
+  /// 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))) {}
+
+  /// 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 {
+    return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : 0;
+  }
+
+private:
+  void IntersectInRange(BasicValueFactory &BV, Factory &F,
+                        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.
+    //   2. R is entirely after the intersection range.
+    //   3. R contains the entire intersection range.
+    //   4. R starts before the intersection range and ends in the middle.
+    //   5. R starts in the middle of the intersection range and ends after it.
+    //   6. R is entirely contained in the intersection range.
+    // These correspond to each of the conditions below.
+    for (/* i = begin(), e = end() */; i != e; ++i) {
+      if (i->To() < Lower) {
+        continue;
+      }
+      if (i->From() > Upper) {
+        break;
+      }
+
+      if (i->Includes(Lower)) {
+        if (i->Includes(Upper)) {
+          newRanges = F.add(newRanges, Range(BV.getValue(Lower),
+                                             BV.getValue(Upper)));
+          break;
+        } else
+          newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To()));
+      } else {
+        if (i->Includes(Upper)) {
+          newRanges = F.add(newRanges, Range(i->From(), BV.getValue(Upper)));
+          break;
+        } else
+          newRanges = F.add(newRanges, *i);
+      }
+    }
+  }
+
+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
+  // modular arithmetic, corresponding to the common treatment of C integer
+  // overflow. Thus, if the Lower bound is greater than the Upper bound, the
+  // 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,
+                     const llvm::APSInt &Lower,
+                     const llvm::APSInt &Upper) const {
+    PrimRangeSet newRanges = F.getEmptySet();
+
+    PrimRangeSet::iterator i = begin(), e = end();
+    if (Lower <= Upper)
+      IntersectInRange(BV, F, Lower, Upper, newRanges, i, e);
+    else {
+      // The order of the next two statements is important!
+      // IntersectInRange() does not reset the iteration state for i and e.
+      // Therefore, the lower range most be handled first.
+      IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e);
+      IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e);
+    }
+    return newRanges;
+  }
+
+  void print(raw_ostream &os) const {
+    bool isFirst = true;
+    os << "{ ";
+    for (iterator i = begin(), e = end(); i != e; ++i) {
+      if (isFirst)
+        isFirst = false;
+      else
+        os << ", ";
+
+      os << '[' << i->From().toString(10) << ", " << i->To().toString(10)
+         << ']';
+    }
+    os << " }";
+  }
+
+  bool operator==(const RangeSet &other) const {
+    return ranges == other.ranges;
+  }
+};
+} // end anonymous namespace
+
+typedef llvm::ImmutableMap<SymbolRef,RangeSet> ConstraintRangeTy;
+
+namespace clang {
+namespace ento {
+template<>
+struct ProgramStateTrait<ConstraintRange>
+  : public ProgramStatePartialTrait<ConstraintRangeTy> {
+  static inline void *GDMIndex() { return &ConstraintRangeIndex; }
+};
+}
+}
+
+namespace {
+class IntervalConstraintManager : public SimpleConstraintManager{
+  RangeSet GetRange(ProgramStateRef state, SymbolRef sym);
+public:
+  IntervalConstraintManager(SubEngine &subengine)
+    : SimpleConstraintManager(subengine) {}
+
+  ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
+                             const llvm::APSInt& Int,
+                             const llvm::APSInt& Adjustment);
+
+  ProgramStateRef assumeSymEQ(ProgramStateRef state, SymbolRef sym,
+                             const llvm::APSInt& Int,
+                             const llvm::APSInt& Adjustment);
+
+  ProgramStateRef assumeSymLT(ProgramStateRef state, SymbolRef sym,
+                             const llvm::APSInt& Int,
+                             const llvm::APSInt& Adjustment);
+
+  ProgramStateRef assumeSymGT(ProgramStateRef state, SymbolRef sym,
+                             const llvm::APSInt& Int,
+                             const llvm::APSInt& Adjustment);
+
+  ProgramStateRef assumeSymGE(ProgramStateRef state, SymbolRef sym,
+                             const llvm::APSInt& Int,
+                             const llvm::APSInt& Adjustment);
+
+  ProgramStateRef assumeSymLE(ProgramStateRef state, SymbolRef sym,
+                             const llvm::APSInt& Int,
+                             const llvm::APSInt& Adjustment);
+
+  const llvm::APSInt* getSymVal(ProgramStateRef St, SymbolRef sym) const;
+
+  // FIXME: Refactor into SimpleConstraintManager?
+  bool isEqual(ProgramStateRef St, SymbolRef sym, const llvm::APSInt& V) const {
+    const llvm::APSInt *i = getSymVal(St, sym);
+    return i ? *i == V : false;
+  }
+
+  ProgramStateRef removeDeadBindings(ProgramStateRef St, SymbolReaper& SymReaper);
+
+  void print(ProgramStateRef St, raw_ostream &Out,
+             const char* nl, const char *sep);
+
+private:
+  RangeSet::Factory F;
+};
+
+} // end anonymous namespace
+
+ConstraintManager* ento::CreateIntervalConstraintManager(ProgramStateManager&,
+                                                         SubEngine &subeng) {
+  return new IntervalConstraintManager(subeng);
+}
+
+const llvm::APSInt* IntervalConstraintManager::getSymVal(ProgramStateRef St,
+                                                      SymbolRef sym) const {
+  const ConstraintRangeTy::data_type *T = St->get<ConstraintRange>(sym);
+  return T ? T->getConcreteValue() : NULL;
+}
+
+/// Scan all symbols referenced by the constraints. If the symbol is not alive
+/// as marked in LSymbols, mark it as dead in DSymbols.
+ProgramStateRef 
+IntervalConstraintManager::removeDeadBindings(ProgramStateRef state,
+                                           SymbolReaper& SymReaper) {
+
+  ConstraintRangeTy CR = state->get<ConstraintRange>();
+  ConstraintRangeTy::Factory& CRFactory = state->get_context<ConstraintRange>();
+
+  for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
+    SymbolRef sym = I.getKey();
+    if (SymReaper.maybeDead(sym))
+      CR = CRFactory.remove(CR, sym);
+  }
+
+  return state->set<ConstraintRange>(CR);
+}
+
+RangeSet
+IntervalConstraintManager::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
+  // given symbol type.
+  QualType T = state->getSymbolManager().getType(sym);
+  BasicValueFactory& BV = state->getBasicVals();
+  return RangeSet(F, BV.getMinValue(T), BV.getMaxValue(T));
+}
+
+//===------------------------------------------------------------------------===
+// assumeSymX methods: public interface for IntervalConstraintManager.
+//===------------------------------------------------------------------------===/
+
+// The syntax for ranges below is mathematical, using [x, y] for closed ranges
+// and (x, y) for open ranges. These ranges are modular, corresponding with
+// a common treatment of C integer overflow. This means that these methods
+// do not have to worry about overflow; RangeSet::Intersect can handle such a
+// "wraparound" range.
+// As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1,
+// UINT_MAX, 0, 1, and 2.
+
+ProgramStateRef 
+IntervalConstraintManager::assumeSymNE(ProgramStateRef state, SymbolRef sym,
+                                    const llvm::APSInt& Int,
+                                    const llvm::APSInt& Adjustment) {
+  BasicValueFactory &BV = state->getBasicVals();
+
+  llvm::APSInt Lower = 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);
+}
+
+ProgramStateRef 
+IntervalConstraintManager::assumeSymEQ(ProgramStateRef state, SymbolRef sym,
+                                    const llvm::APSInt& Int,
+                                    const llvm::APSInt& Adjustment) {
+  // [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);
+}
+
+ProgramStateRef 
+IntervalConstraintManager::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);
+
+  // Special case for Int == Min. This is always false.
+  if (Int == Min)
+    return NULL;
+
+  llvm::APSInt Lower = Min-Adjustment;
+  llvm::APSInt Upper = Int-Adjustment;
+  --Upper;
+
+  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
+  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+}
+
+ProgramStateRef 
+IntervalConstraintManager::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);
+
+  // Special case for Int == Max. This is always false.
+  if (Int == Max)
+    return NULL;
+
+  llvm::APSInt Lower = Int-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);
+}
+
+ProgramStateRef 
+IntervalConstraintManager::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);
+
+  // Special case for Int == Min. This is always feasible.
+  if (Int == Min)
+    return state;
+
+  const llvm::APSInt &Max = BV.getMaxValue(T);
+
+  llvm::APSInt Lower = Int-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);
+}
+
+ProgramStateRef 
+IntervalConstraintManager::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);
+
+  // Special case for Int == Max. This is always feasible.
+  if (Int == Max)
+    return state;
+
+  const llvm::APSInt &Min = BV.getMinValue(T);
+
+  llvm::APSInt Lower = Min-Adjustment;
+  llvm::APSInt Upper = Int-Adjustment;
+
+  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
+  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+}
+
+//===------------------------------------------------------------------------===
+// Pretty-printing.
+//===------------------------------------------------------------------------===/
+
+void IntervalConstraintManager::print(ProgramStateRef St, raw_ostream &Out,
+                                   const char* nl, const char *sep) {
+
+  ConstraintRangeTy Ranges = St->get<ConstraintRange>();
+
+  if (Ranges.isEmpty()) {
+    Out << nl << sep << "Ranges are empty." << nl;
+    return;
+  }
+
+  Out << nl << sep << "Ranges of symbol values:";
+  for (ConstraintRangeTy::iterator I=Ranges.begin(), E=Ranges.end(); I!=E; ++I){
+    Out << nl << ' ' << I.getKey() << " : ";
+    I.getData().print(Out);
+  }
+  Out << nl;
+}