Fix up the Equation System generation. Now there's a bug in the solver.

The solver seems to work fine when run as a tool by itself, but not in the clang stuff. Very annoying.

11 files changed, 364 insertions, 339 deletions

diff --git a/TODO.org b/TODO.org
deleted file mode 100644
index f59cf4b..0000000
--- a/TODO.org
+++ /dev/null
@@ -1,55 +0,0 @@
-* TODO Refactoring [1/4]
-- [X] Fix up logging
-- [ ] Separate classes into files
-- [ ] Put outer-loop in a class (out of main)
-- [ ] Give EquationSystem methods for creating assignments/strategies
-* TODO Verbosity [2/3]
-- [X] Wrap output streams [5/5]
-  - [X] strategies
-  - [X] fixpoint
-  - [X] debug
-  - [X] trace
-  - [X] info
-- [X] Command-line arguments [5/5]
-  - [X] strategies
-  - [X] fixpoint
-  - [X] debug
-  - [X] trace
-  - [X] info
-- [-] Provide output [0/5]
-  - [-] strategies [1/2]
-    - [ ] print the system and assignment, then the next strategy
-    - [X] print each strategy like this:
-      max(0, x, sub(y,2)) --[2]-> sub(y,2)
-  - [ ] fixpoint
-    print the system we're working with, then print the resultant assignment
-  - [ ] debug
-    print the initial system we're working with
-    print more general info in the main loop (number of loops, each assignment/strategy)
-  - [ ] trace
-    maybe we don't need this
-    would be something like "entering/exiting" everything mildly important
-  - [ ] info
-    print the initial system we're working with    
-* TODO make test [2/3]
-- [-] write test cases [1/4]
-  - [X] examples from paper
-  - [ ] best cases
-  - [ ] worst cases
-  - [ ] average cases
-- [X] write a script to run over each test case and return pass/fail
-- [X] consolidate into makefile as `make test`
-* TODO Min-cost flow problem [1/3]
-- [X] Research min-cost flow libraries
-  Potentially just use LEMON? It looks pretty decent.
-  LEMON it is!
-- [ ] Implement the min-cost flow operator MCF
-  It takes four construction-time arguments and one run-time argument.
-  Construction time:
-  - T (the template constraint matrix)
-  - A (the multiplicative modification factor)
-  - b (the additive modification factor)
-  - c (the bound in the guard)
-  Run-time:
-  - d (the abstract value to be operated on)
-- [ ] Update test cases to include MCF
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp
index 5219c9e..9acb9d0 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Complete.hpp
@@ -15,10 +15,7 @@ struct Complete {
     : _value(value), _infinity(false) { }
   Complete(const T& value, const bool& infinity)
     : _value(value), _infinity(infinity) {
-    if (value == 0 && infinity == true) {
-      std::cout << "throw exception" << *(char*)NULL;
-      //throw "Zero infinity? Die die die!";
-    }
+    assert(value != 0 || infinity == false);
   }
   Complete(const Complete& other)
     : _value(other._value), _infinity(other._infinity) { }
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp
index c4ee4c0..ac9b052 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/Expression.hpp
@@ -28,7 +28,7 @@ struct Expression {
   }
 
   virtual Domain eval(const VariableAssignment<Domain>&) const = 0;
-  virtual Domain eval(const VariableAssignment<Domain>& rho,
+  virtual Domain evalWithStrat(const VariableAssignment<Domain>& rho,
                       const MaxStrategy<Domain>&) const {
     return eval(rho);
   }
@@ -98,16 +98,20 @@ struct OperatorExpression : public Expression<Domain> {
     return _operator.eval(argumentValues);
   }
 
-  virtual Domain eval(const VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
+  virtual Domain evalWithStrat(const VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
     std::vector<Domain> argumentValues;
     for (typename std::vector<Expression<Domain>*>::const_iterator it = _arguments.begin();
          it != _arguments.end();
          ++it) {
-      argumentValues.push_back((*it)->eval(rho, strat));
+      argumentValues.push_back((*it)->evalWithStrat(rho, strat));
     }
     return _operator.eval(argumentValues);
   }
 
+  std::vector<Expression<Domain>*>& arguments() {
+    return _arguments;
+  }
+
   const std::vector<Expression<Domain>*>& arguments() const {
     return _arguments;
   }
@@ -139,7 +143,7 @@ struct OperatorExpression : public Expression<Domain> {
   private:
   const Operator<Domain>& _operator;
   protected:
-  const std::vector<Expression<Domain>*> _arguments;
+  std::vector<Expression<Domain>*> _arguments;
 };
 
 template<typename Domain>
@@ -151,18 +155,18 @@ struct MaxExpression : public OperatorExpression<Domain> {
     return this;
   }
 
-  virtual Domain eval(const VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
-    return this->_arguments[strat.get(*this)]->eval(rho, strat);
+  virtual Domain evalWithStrat(const VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
+    return this->_arguments[strat.get(*this)]->evalWithStrat(rho, strat);
   }
 
   unsigned int bestStrategy(const VariableAssignment<Domain>& rho, const MaxStrategy<Domain>& strat) const {
-    Domain bestValue = this->eval(rho, strat);
+    Domain bestValue = this->evalWithStrat(rho, strat);
     unsigned int bestIndex = strat.get(*this);
 
     for (unsigned int i = 0, length = this->_arguments.size();
          i < length;
          ++i) {
-      const Domain value = this->_arguments[i]->eval(rho, strat);
+      const Domain value = this->_arguments[i]->evalWithStrat(rho, strat);
       if (bestValue < value) {
         bestValue = value;
         bestIndex = i;
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp
index f5cb0d8..57dcdeb 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/MaxStrategy.hpp
@@ -54,9 +54,12 @@ struct DynamicMaxStrategy : public MaxStrategy<Domain> {
     solver_log::strategy << indent() << "Invalidating " << v << " - " << *_system[v] << std::endl;
     _stable.filter(_var_influence[v]);
 
+    IdSet<MaxExpression<Domain> > infl = _var_influence[v];
+    _var_influence[v].clear();
+
     for (typename IdSet<MaxExpression<Domain> >::iterator
-           it = _var_influence[v].begin(),
-           end = _var_influence[v].end();
+           it = infl.begin(),
+           end = infl.end();
          it != end;
          ++it) {
       solve(_system.maxExpression(*it));
diff --git a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
index 0bbebfc..ba5f650 100644
--- a/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
+++ b/clang/include/clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp
@@ -35,8 +35,12 @@ struct DynamicVariableAssignment : public VariableAssignment<Domain> {
 
   void invalidate(const Variable<Domain>& x) const {
     solver_log::fixpoint << indent() << "Invalidating " << x << std::endl;
-    _stable.remove(x);
-    _values[x] = infinity<Domain>();
+    if (_stable.contains(x)) {
+      _stable.remove(x);
+      _values[x] = infinity<Domain>();
+      
+      solve(x);
+    }
   }
 
 private:
@@ -49,8 +53,8 @@ private:
       stack_depth++;
       if (!_system[x])
         return;
-      Domain val = _system[x]->eval(DependencyAssignment(*this, x),
-                                    _strategy);
+      Domain val = _system[x]->evalWithStrat(DependencyAssignment(*this, x),
+					     _strategy);
       stack_depth--;
 
       if (val != _values[x]) {
diff --git a/clang/lib/Analysis/CMakeLists.txt b/clang/lib/Analysis/CMakeLists.txt
index bede002..3d2251e 100644
--- a/clang/lib/Analysis/CMakeLists.txt
+++ b/clang/lib/Analysis/CMakeLists.txt
@@ -21,5 +21,8 @@ add_clang_library(clangAnalysis
   UninitializedValues.cpp
   )
 
+add_library(lib_lemon IMPORTED emon)
+
 add_dependencies(clangAnalysis ClangAttrClasses ClangAttrList
-                 ClangDiagnosticAnalysis ClangDeclNodes ClangStmtNodes)
+                 ClangDiagnosticAnalysis ClangDeclNodes ClangStmtNodes
+                 lib_lemon)
diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp
index 96dd841..ac96107 100644
--- a/clang/lib/Analysis/Interval.cpp
+++ b/clang/lib/Analysis/Interval.cpp
@@ -21,6 +21,12 @@
 
 using namespace clang;
 
+std::string negate_string(const std::string& str) {
+  if (str[0] == '-')
+    return str.substr(1);
+  return '-' + str;
+}
+
 #include <sstream>
 template<typename T>
 std::string toString(const T& obj) {
@@ -36,6 +42,20 @@ std::ostream& operator<<(std::ostream& cout, const std::pair<K,V>& v) {
   return cout;
 }
 
+template<typename V>
+std::ostream& operator<<(std::ostream& cout, const std::vector<V>& v) {
+  cout << "[";
+  for(typename std::vector<V>::const_iterator it = v.begin(), ei = v.end();
+      it != ei;
+      ++it) {
+    if (it != v.begin())
+      cout << ", ";
+    cout << *it;
+  }
+  cout << "]";
+  return cout;
+}
+
 template<typename K,typename V>
 std::ostream& operator<<(std::ostream& cout, const std::map<K,V>& v) {
   cout << "{";
@@ -50,14 +70,6 @@ std::ostream& operator<<(std::ostream& cout, const std::map<K,V>& v) {
   return cout;  
 }
 
-
-IntervalAnalysis :: IntervalAnalysis(AnalysisDeclContext &context)
-  : context(&context) {
-}
-
-IntervalAnalysis :: ~IntervalAnalysis() {
-}
-
 // Two pieces of state:
 //  -> condition protecting a node
 //  -> node's expression itself
@@ -68,10 +80,14 @@ IntervalAnalysis :: ~IntervalAnalysis() {
 // Hooray!
 
 typedef Complete<int64_t> ZBar;
+template<>
+ZBar infinity() {
+  return ZBar(1, true);
+}
 //typedef std::map<std::string, ZBar> Vector;
 
 struct Vector : public std::map<std::string, ZBar> {
-  Vector(const ZBar& val=infinity<ZBar>())
+  Vector(const ZBar& val=0)
     : _val(val) { }
   ZBar operator[](const std::string& key) const {
     if (this->find(key) != this->end())
@@ -87,8 +103,23 @@ struct Vector : public std::map<std::string, ZBar> {
   ZBar _val;
 };
 
+Vector negate_vector(const Vector& v) {
+  Vector result;
+  for (Vector::const_iterator it = v.begin(),
+         ei = v.end();
+       it != ei;
+       ++it) {
+    result[negate_string(it->first)] = it->second;
+  }
+  return result;
+}
+
 typedef std::pair<Vector, ZBar> Result; // a "slice" of an equation
 
+Result negate_result(const Result& r) {
+  return Result(negate_vector(r.first), -r.second);
+}
+
 //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 {
@@ -112,21 +143,21 @@ struct LinearEquation : public std::map<std::string, Result> {
 
 typedef Vector Condition;
 
-typedef EquationSystem<Vector> EqnSys;
-typedef Expression<Vector> EqnExpr;
-typedef Variable<Vector> EqnVar;
+typedef EquationSystem<ZBar> EqnSys;
+typedef Expression<ZBar> EqnExpr;
+typedef Variable<ZBar> EqnVar;
 
 
 struct LinearOperator : public Operator<Vector> {
-  LinearOperator(const LinearEquation& result)
+  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();
+    for (LinearEquation::const_iterator it = _values->begin(),
+           ei = _values->end();
          it != ei;
          ++it) {
       ZBar subresult = 0;
@@ -143,10 +174,10 @@ struct LinearOperator : public Operator<Vector> {
   }
 
   void print(std::ostream& cout) const {
-    cout << "linear[" << _values << "]";
+    cout << "linear[" << *_values << "]";
   }
 
-  LinearEquation _values;
+  const LinearEquation* _values;
 };
 
 
@@ -192,6 +223,7 @@ M merge_maps_with(const F& f, const M& left, const M& right) {
 
 template<>
 Vector minimum(const Vector& l, const Vector& r) {
+  return (l < r ? l : r);
   return merge_maps_with(minimum<ZBar>, l, r);
 }
 template<class T>
@@ -240,12 +272,15 @@ Vector operator*(const ZBar& left, const Vector& right) {
   return right * left;
 }
 bool operator<(const Vector& left, const Vector& right) {
+  bool equal = true;
   for (Vector::const_iterator it = left.begin(),
          ei = left.end();
        it != ei;
        ++it) {
     if (it->second < right[it->first]) {
-      return true;
+      equal = false;
+    } else if (it->second > right[it->first]) {
+      return false;
     }
   }
   for (Vector::const_iterator it = right.begin(),
@@ -253,10 +288,12 @@ bool operator<(const Vector& left, const Vector& right) {
        it != ei;
        ++it) {
     if (left[it->first] < it->second) {
-      return true;
+      equal = false;
+    } else if (left[it->first] > it->second) {
+      return false;
     }
   }
-  return false;
+  return equal ? left._val < right._val : true;
 }
 
 template<>
@@ -277,10 +314,16 @@ std::ostream& operator<<(std::ostream& cout, const Vector& v) {
 }
 
 
-Result fromStmt(const Stmt*);
+
+
+
+
+/* Expression functions */
+
+Result fromExpr(const Expr*);
 
 Result fromInteger(const IntegerLiteral* expr) {
-  return Result(Vector(), *expr->getValue().getRawData());
+  return Result(Vector(0), *expr->getValue().getRawData());
 }
 
 Result fromDeclExpr(const DeclRefExpr* expr) {
@@ -296,19 +339,24 @@ Result fromUnary(const UnaryOperator* op) {
   case UO_PostInc:
     break;
   }
-  return Result(Vector(), 0);
+  return Result(Vector(0), 0);
+}
+
+Result operator*(const ZBar& l, const Result& r) {
+  return Result(l * r.first, l * r.second);
 }
 
 Result fromBinary(const BinaryOperator* op) {
-  Result left = fromStmt(op->getLHS()->IgnoreParenCasts());
-  Result right = fromStmt(op->getRHS()->IgnoreParenCasts());
+  Result left = fromExpr(op->getLHS()->IgnoreParenCasts());
+  Result right = fromExpr(op->getRHS()->IgnoreParenCasts());
   
   switch (op->getOpcode()) {
   case BO_Assign:
     return right;
   case BO_Sub:
-    transform_values(negate<ZBar>, right.first);
-    right.second *= -1;
+    right = negate_result(right);
+    //transform_values(negate<ZBar>, right.first);
+    //right.second *= -1;
   case BO_Add:
     {
       Result result;
@@ -320,7 +368,7 @@ Result fromBinary(const BinaryOperator* op) {
   case BO_Mul:
     {
       if (!left.first.empty() && !right.first.empty()) {
-        return Result(Vector(), 0);
+        return Result(Vector(0), 0);
       }
       ZBar scalar = 0;
       Result value;
@@ -331,30 +379,11 @@ Result fromBinary(const BinaryOperator* op) {
         scalar = right.second;
         value = left;
       }
-      if (scalar > 0) {
-        for (Vector::iterator it = value.first.begin(),
-               ei = value.first.end();
-             it != ei;
-             ++it) {
-          it->second *= scalar;
-        }
+      if (scalar >= 0) {
+        return scalar * value;
       } 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;
-        }
+        return -scalar * negate_result(value);
       }
-      right.second *= scalar;
-      return value;
     }
   case BO_LT:
   case BO_LE:
@@ -365,65 +394,7 @@ Result fromBinary(const BinaryOperator* op) {
   return Result();
 }
 
-Result fromDeclStmt(const DeclStmt* stmt) {
-  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);
-      llvm::errs() << decl->getNameAsString() << " = ";
-
-      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->second) << "*" << toString(it->first);
-      }
-      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) {
-  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());
-    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->second) << "*" << toString(it->first);
-    }
-    llvm::errs() << " + " << toString(expr.second) << "\n";
-    return expr;
-  }
-  return Result();
-}
-
-Result fromStmt(const Stmt* stmt) {
+Result fromExpr(const Expr* stmt) {
   if (!stmt)
     return Result();
   //stmt->dump();
@@ -434,93 +405,109 @@ Result fromStmt(const Stmt* stmt) {
     return fromDeclExpr(static_cast<const DeclRefExpr*>(stmt));
   case Stmt::UnaryOperatorClass:
     return fromUnary(static_cast<const UnaryOperator*>(stmt));
-  case Stmt::DeclStmtClass:
-    return fromDeclStmt(static_cast<const DeclStmt*>(stmt));
   case Stmt::BinaryOperatorClass:
     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);
-  }
+  const Expr* expr = stmt->IgnoreParenCasts();
+  if (stmt != expr)
+    return fromExpr(expr);
   llvm::errs() << "we shouldn't get here...\n";
   return Result();
 }
 
-Condition fromComparison(const BinaryOperator* op) {
+
+/* Comparison stuff */
+
+Condition fromComparison(const BinaryOperator* op, bool negate) {
+  Condition cond(infinity<ZBar>());
+  if (!op) {
+    if (negate)
+      return -cond;
+    else
+      return cond;
+  }
   if (op->isRelationalOp()) {
     const Expr* left = op->getLHS()->IgnoreParenCasts();
     const Expr* right = op->getRHS()->IgnoreParenCasts();
 
-    Condition cond;
+    bool flip = false;
     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();
-      }
+      name = static_cast<const DeclRefExpr*>(left)->getNameInfo().getAsString();
     } 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();
+      name = static_cast<const DeclRefExpr*>(right)->getNameInfo().getAsString();
+      flip = true;
+    } else {
+      return cond;
+    }
+
+    if (right->getStmtClass() == Stmt::IntegerLiteralClass) {
+      value = *static_cast<const IntegerLiteral*>(right)->getValue().getRawData();
+    } else if (left->getStmtClass() == Stmt::IntegerLiteralClass) {
+      value = *static_cast<const IntegerLiteral*>(left)->getValue().getRawData();
+    } else {
+      return cond;
+    }
+
+    BinaryOperator::Opcode operation = op->getOpcode();
+    if (flip) {
+      switch (operation) {
+      case BO_LT: operation = BO_GT; break;
+      case BO_GT: operation = BO_LT; break;
+      case BO_LE: operation = BO_GE; break;
+      case BO_GE: operation = BO_LE; break;
       }
     }
-    return Condition();
+
+    switch (operation) {
+    case BO_LT:
+      if (negate)
+	cond[negate_string(name)] = -value;
+      else
+	cond[name] = value - 1;
+      break;
+    case BO_LE:
+      if (negate)
+	cond[negate_string(name)] = -(value + 1);
+      else
+	cond[name] = value;
+      break;
+    case BO_GE:
+      if (negate)
+	cond[name] = value - 1;
+      else
+	cond[negate_string(name)] = -value;
+      break;
+    case BO_GT:
+      if (negate)
+	cond[name] = value;
+      else
+	cond['-' + name] = -(value + 1);
+      break;
+    }
   }
-  return Condition();
+  return cond;
 }
 
-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;
+/* Blocks */
 
-  std::string id = toString(block->getBlockID());
-  unsigned int counter = 0;
-  
-  // detemine equations for this block
-  LinearEquation eqn;
-  EqnVar* var;
-  Result current;
+typedef std::map<std::string, unsigned int> Counters;
+typedef std::map<std::string, EqnVar*> VarMap;
+typedef std::map<const CFGBlock*, std::set<std::string> > BlockVars;
 
-  var = &system.variable(id);
+void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) {
+  Counters counters;
+  std::string block_id = toString(block->getBlockID());
+  VarMap vars;
+
+  for (std::set<std::string>::iterator it = block_vars[block].begin(),
+	 ei = block_vars[block].end();
+       it != ei;
+       ++it) {
+    vars[*it] = &system.variable(*it + '-' + block_id + "-pre");
+  }
+  
   for (CFGBlock::const_iterator it = block->begin(),
                                 ei = block->end();
        it != ei;
@@ -529,7 +516,7 @@ EqnVar* runOnBlock(const CFGBlock* block, EqnSys& system) {
     const Stmt* stmt = cfg_stmt->getStmt();
 
     std::string name = "";
-    Result expr;
+    Result result;
     if (stmt->getStmtClass() == Stmt::BinaryOperatorClass) {
       const BinaryOperator* binop = static_cast<const BinaryOperator*>(stmt);
       if (binop->isAssignmentOp()) {
@@ -537,11 +524,10 @@ EqnVar* runOnBlock(const CFGBlock* block, EqnSys& system) {
         const Expr* right = binop->getRHS()->IgnoreParenCasts();
         if (left->getStmtClass() == Stmt::DeclRefExprClass) {
           name = static_cast<const DeclRefExpr*>(left)->getNameInfo().getAsString();
-          expr = fromStmt(right);
+          result = fromExpr(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();
@@ -550,104 +536,150 @@ EqnVar* runOnBlock(const CFGBlock* block, EqnSys& system) {
         if ((*jt)->getKind() == Decl::Var) {
           const VarDecl* decl = static_cast<const VarDecl*>(*jt);
           name = decl->getNameAsString();
-          expr = fromStmt(decl->getInit());
-          if (jt+1 != ej) {
+          result = fromExpr(decl->getInit());
+          jt++;
+          if (jt != 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";
         }
       }
     }
     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());
+    std::string count = toString(counters[name]);
+    EqnVar* var = &system.variable(name + '-' + block_id + '[' + count + ']');
+    EqnVar* negative_var = &system.variable(negate_string(name) + '-' + block_id + '[' + count + ']');
+    counters[name]++;
+    for (int negative = 0; negative < 2; ++negative) { // one loop for positive, the other for negative
+      if (negative) {
+	result = negate_result(result);
+      }
+      EqnExpr* expression = &system.constant(result.second);
+      for (Vector::iterator it = result.first.begin(),
+	     ei = result.first.end();
+	   it != ei;
+	   ++it) {
+	if (!vars[it->first])
+	  vars[it->first] = &system.variable(it->first + '-' + block_id + "-pre");
+	std::vector<EqnExpr*> additionArgs;
+	additionArgs.push_back(expression);
+
+	if (it->second == 1) {
+	  additionArgs.push_back(vars[it->first]);
+	} else {
+	  std::vector<EqnExpr*> multiplicationArgs;
+	  multiplicationArgs.push_back(vars[it->first]);
+	  multiplicationArgs.push_back(&system.constant(it->second)); 
+	  additionArgs.push_back(&system.expression(new Multiplication<ZBar>(), multiplicationArgs));
+	}
+      
+	expression = &system.expression(new Addition<ZBar>(), additionArgs);
+      }
+    
+      std::vector<EqnExpr*> maxArgs;
+      maxArgs.push_back(&system.constant(-infinity<ZBar>()));
+      maxArgs.push_back(expression);
+      if (negative)
+	system[*negative_var] = &system.maxExpression(maxArgs);
+      else
+	system[*var] = &system.maxExpression(maxArgs);
     }
+    vars[name] = var;
+    vars[negate_string(name)] = negative_var;
+    block_vars[block].insert(name);
+    block_vars[block].insert(negate_string(name));
+  }
 
-    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);
+  // add to our successor entry values
+  for (CFGBlock::const_succ_iterator
+	 it = block->succ_begin(),
+	 ei = block->succ_end();
+       it != ei;
+       ++it) {
+    bool negate_terminator = it != block->succ_begin(); // not the first means `false` branch
+    Condition cond = fromComparison(static_cast<const BinaryOperator*>(block->getTerminatorCondition()), negate_terminator);
+    for (VarMap::iterator jt = vars.begin(),
+	   ej = vars.end();
+	 jt != ej;
+	 ++jt) {
+      block_vars[*it].insert(jt->first);
+
+      ZBar val = cond[jt->first];
+      EqnVar* var = &system.variable(jt->first + '-' + toString((*it)->getBlockID()) + "-pre");
+      if (system[*var] == NULL) {
+	std::vector<EqnExpr*> maxArgs;
+	maxArgs.push_back(&system.constant(-infinity<ZBar>()));
+	system[*var] = &system.maxExpression(maxArgs);
+      }
+      
+      EqnExpr* expr = NULL;
+      if (val == -infinity<ZBar>()) {
+	// don't do anything here: min(-inf, x) = -inf  (for all x)
+      } else if (val == infinity<ZBar>()) {
+	// no need to have a min here: min(inf, x) = x  (for all x)
+	expr = jt->second;
+      } else {
+	// need a min here
+	std::vector<EqnExpr*> minArgs;
+	minArgs.push_back(&system.constant(val));
+	minArgs.push_back(jt->second);
+	expr = &system.expression(new Minimum<ZBar>(), minArgs);
+      }
 
-      // 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();
+      if (expr) {
+	std::set<std::string> ignore;
+	for (VarMap::iterator
+	       variables = vars.begin(),
+	       variables_end = vars.end();
+	     variables != variables_end;
+	     ++variables) {
+	  if (ignore.find(variables->first) != ignore.end())
+	    continue;
+	  ignore.insert(negate_string(variables->first));
+
+	  std::vector<EqnExpr*> plusArgs;
+	  for (int negate = 0; negate < 2; ++negate) {
+	    std::string var_name = negate ? negate_string(variables->first) : variables->first;
+	    std::vector<EqnExpr*> minArgs;
+	    minArgs.push_back(vars[var_name]);
+	    minArgs.push_back(&system.constant(cond[var_name]));
+	    plusArgs.push_back(&system.expression(new Minimum<ZBar>(), minArgs));
+	  }
+
+	  std::vector<EqnExpr*> guard_args;
+	  guard_args.push_back(&system.expression(new Addition<ZBar>(), plusArgs)); // value
+	  guard_args.push_back(&system.constant(0)); // lower-bound (so value must be >= this)
+	  guard_args.push_back(expr); // result
+	  expr = &system.expression(new Guard<ZBar>(), guard_args);
+	}
+	system[*var]->arguments().push_back(expr);
+      }
     }
-
-    eqn[name] = expr;
-    expr.first = expr.first;
-    expr.second = -expr.second;
-    eqn["-"+name] = expr;
   }
+}
 
-  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 {
-      preArgs.push_back(runOnBlock(*it, system));
-    }
-  }
-  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;
+IntervalAnalysis :: IntervalAnalysis(AnalysisDeclContext &context)
+  : context(&context) {
 }
 
-void IntervalAnalysis::runOnAllBlocks() {
-  llvm::errs() << "Enter run on all blocks\n";
+IntervalAnalysis :: ~IntervalAnalysis() {
+}
 
+void IntervalAnalysis::runOnAllBlocks() {
   const CFG *cfg = this->context->getCFG();
 
+  cfg->dump(context->getASTContext().getLangOpts(),
+            llvm::sys::Process::StandardErrHasColors());
+
   EqnSys system;
+  BlockVars block_vars;
 
   std::set<const CFGBlock*> seen;
   std::deque<const CFGBlock*> todo;
@@ -659,37 +691,51 @@ void IntervalAnalysis::runOnAllBlocks() {
       todo.pop_front();
       continue;
     }
-    llvm::errs() << block->getBlockID() << "\n";
     seen.insert(block);
     todo.pop_front();
-    runOnBlock(block, system);
-    llvm::errs() << "-> ";
+    runOnBlock(block, system, block_vars);
     for (CFGBlock::const_succ_iterator it = block->succ_begin(),
                                        ei = block->succ_end();
          it != ei;
          it++ ) {
-      llvm::errs() << (*it)->getBlockID() << ", ";
       todo.push_back(*it);
     }
-    llvm::errs() << "\n\n";
   }
 
-  llvm::errs() << "Exit run on all blocks\n";
+  std::vector<EqnExpr*> a;
+
+  a.push_back(&system.constant(-infinity<ZBar>()));
+  a.push_back(&system.constant(0));
+  system[system.variable("x")] = &system.maxExpression(a);
+  a.clear();
+  
+  system.variable("y");
+
+  a.push_back(&system.variable("x"));
+  a.push_back(&system.variable("z"));
+  EqnExpr* minExpr = &system.expression(new Maximum<ZBar>(), a);
+  a.clear();
+
+  a.push_back(&system.constant(-infinity<ZBar>()));
+  a.push_back(minExpr);
+  system[system.variable("y")] = &system.maxExpression(a);
+  a.clear();
+
+  a.push_back(&system.constant(-infinity<ZBar>()));
+  a.push_back(&system.variable("y"));
+  system[system.variable("z")] = &system.maxExpression(a);
 
   llvm::errs() << toString(system) << "\n";
 
   system.indexMaxExpressions();
-  DynamicMaxStrategy<Vector> strategy(system);
-  DynamicVariableAssignment<Vector> rho(system, strategy);
+  DynamicMaxStrategy<ZBar> strategy(system);
+  DynamicVariableAssignment<ZBar> rho(system, strategy);
   strategy.setRho(rho);
 
   for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
-    Variable<Vector>& var = system.variable(i);
+    EqnVar& var = system.variable(size - i - 1);
     llvm::errs() << toString(var.name()) << " = " << toString(rho[var]) << "\n";
   }
-
-  //  cfg->dump(context->getASTContext().getLangOpts(),
-  //            llvm::sys::Process::StandardErrHasColors());
 }
 
 
diff --git a/clang/lib/StaticAnalyzer/Checkers/.#ArrayBoundCheckerV2_flymake.cpp b/clang/lib/StaticAnalyzer/Checkers/.#ArrayBoundCheckerV2_flymake.cpp
deleted file mode 120000
index 235903b..0000000
--- a/clang/lib/StaticAnalyzer/Checkers/.#ArrayBoundCheckerV2_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/StaticAnalyzer/Checkers/.#Checkers.td b/clang/lib/StaticAnalyzer/Checkers/.#Checkers.td
deleted file mode 120000
index 235903b..0000000
--- a/clang/lib/StaticAnalyzer/Checkers/.#Checkers.td
+++ /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/StaticAnalyzer/Checkers/Checkers.td b/clang/lib/StaticAnalyzer/Checkers/Checkers.td
index f577a89..3c211a3 100644
--- a/clang/lib/StaticAnalyzer/Checkers/Checkers.td
+++ b/clang/lib/StaticAnalyzer/Checkers/Checkers.td
@@ -28,7 +28,7 @@ def DeadCodeExperimental : Package<"deadcode">, InPackage<Experimental>, Hidden;
 
 def Security : Package <"security">;
 def InsecureAPI : Package<"insecureAPI">, InPackage<Security>;
-def SecurityExperimental : Package<"security">, InPackage<Experimental>, Hidden;
+def SecurityExperimental : Package<"security">, InPackage<Experimental>; //, Hidden;
 def Taint : Package<"taint">, InPackage<SecurityExperimental>, Hidden;  
 
 def Unix : Package<"unix">;
diff --git a/clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp
index 9d04720..dc2f0d9 100644
--- a/clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/IntervalConstraintManager.cpp
@@ -254,6 +254,7 @@ private:
 
 ConstraintManager* ento::CreateIntervalConstraintManager(ProgramStateManager&,
                                                          SubEngine &subeng) {
+  llvm::errs() << "Creating interval constraint manager\n";
   return new IntervalConstraintManager(subeng);
 }
 
@@ -294,7 +295,7 @@ IntervalConstraintManager::GetRange(ProgramStateRef state, SymbolRef sym) {
 }
 
 //===------------------------------------------------------------------------===
-// assumeSymX methods: public interface for IntervalConstraintManager.
+// eSymX methods: public interface for IntervalConstraintManager.
 //===------------------------------------------------------------------------===/
 
 // The syntax for ranges below is mathematical, using [x, y] for closed ranges
@@ -309,6 +310,10 @@ ProgramStateRef
 IntervalConstraintManager::assumeSymNE(ProgramStateRef state, SymbolRef sym,
                                     const llvm::APSInt& Int,
                                     const llvm::APSInt& Adjustment) {
+  llvm::errs() << "AssumeNE\n";
+  state->dump();
+  sym->dump();
+
   BasicValueFactory &BV = state->getBasicVals();
 
   llvm::APSInt Lower = Int-Adjustment;
@@ -326,6 +331,10 @@ ProgramStateRef
 IntervalConstraintManager::assumeSymEQ(ProgramStateRef state, SymbolRef sym,
                                     const llvm::APSInt& Int,
                                     const llvm::APSInt& Adjustment) {
+  llvm::errs() << "AssumeEQ\n";
+  state->dump();
+  sym->dump();
+
   // [Int-Adjustment, Int-Adjustment]
   BasicValueFactory &BV = state->getBasicVals();
   llvm::APSInt AdjInt = Int-Adjustment;
@@ -337,6 +346,10 @@ ProgramStateRef
 IntervalConstraintManager::assumeSymLT(ProgramStateRef state, SymbolRef sym,
                                     const llvm::APSInt& Int,
                                     const llvm::APSInt& Adjustment) {
+  llvm::errs() << "AssumeLT\n";
+  state->dump();
+  sym->dump();
+
   BasicValueFactory &BV = state->getBasicVals();
 
   QualType T = state->getSymbolManager().getType(sym);
@@ -358,6 +371,10 @@ ProgramStateRef
 IntervalConstraintManager::assumeSymGT(ProgramStateRef state, SymbolRef sym,
                                     const llvm::APSInt& Int,
                                     const llvm::APSInt& Adjustment) {
+  llvm::errs() << "AssumeGT\n";
+  state->dump();
+  sym->dump();
+
   BasicValueFactory &BV = state->getBasicVals();
 
   QualType T = state->getSymbolManager().getType(sym);
@@ -379,6 +396,10 @@ ProgramStateRef
 IntervalConstraintManager::assumeSymGE(ProgramStateRef state, SymbolRef sym,
                                     const llvm::APSInt& Int,
                                     const llvm::APSInt& Adjustment) {
+  llvm::errs() << "AssumeGE\n";
+  state->dump();
+  sym->dump();
+
   BasicValueFactory &BV = state->getBasicVals();
 
   QualType T = state->getSymbolManager().getType(sym);
@@ -401,6 +422,10 @@ ProgramStateRef
 IntervalConstraintManager::assumeSymLE(ProgramStateRef state, SymbolRef sym,
                                     const llvm::APSInt& Int,
                                     const llvm::APSInt& Adjustment) {
+  llvm::errs() << "AssumeLE\n";
+  state->dump();
+  sym->dump();
+
   BasicValueFactory &BV = state->getBasicVals();
 
   QualType T = state->getSymbolManager().getType(sym);