Updated solver stuff. This really should have already been in here...

1 files changed, 212 insertions, 138 deletions

diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp
index 4b274ed..ab79abb 100644
--- a/clang/lib/Analysis/Interval.cpp
+++ b/clang/lib/Analysis/Interval.cpp
@@ -5,7 +5,6 @@
 #include "clang/AST/StmtVisitor.h"
 
 #include "clang/Analysis/Analyses/IntervalSolver/Log.hpp"
-#include "clang/Analysis/Analyses/IntervalSolver/Complete.hpp"
 #include "clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp"
 #include "clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp"
 
@@ -22,6 +21,7 @@
 using namespace clang;
 using namespace std;
 
+
 template<typename T>
 T neg(const T& t) {
   return -t;
@@ -90,14 +90,6 @@ ostream& operator<<(ostream& cout, const map<K,V>& v) {
 //
 // Hooray!
 
-typedef Complete<int64_t> ZBar;
-template<>
-ZBar infinity() {
-  return ZBar(1, true);
-}
-
-
-
 
 
 struct Vector : public map<string, ZBar> {
@@ -160,7 +152,7 @@ Vector operator+(const Vector& left, const Vector& right) {
 
   return result;
 }
-Vector operator*(const ZBar& left, const Vector& right) {
+Vector scalar_mult(const ZBar& left, const Vector& right) {
   Vector result(left * right._val);
 
   for (Vector::const_iterator
@@ -173,9 +165,6 @@ Vector operator*(const ZBar& left, const Vector& right) {
 
   return result;
 }
-Vector operator*(const Vector& left, const ZBar& right) {
-  return right * left;
-}
 
 ostream& operator<<(ostream& cout, const Vector& v) {
   cout << "{";
@@ -225,6 +214,7 @@ Result fromDeclExpr(const DeclRefExpr* expr) {
 }
 
 Result fromUnary(const UnaryOperator* op) {
+  assert(false); // unary operations aren't supported. Sorry!
   switch (op->getOpcode()) {
   case UO_PreInc:
     break;
@@ -235,7 +225,7 @@ Result fromUnary(const UnaryOperator* op) {
 }
 
 Result operator*(const ZBar& l, const Result& r) {
-  return Result(l * r.first, l * r.second);
+  return Result(scalar_mult(l, r.first), l * r.second);
 }
 
 Result fromBinary(const BinaryOperator* op) {
@@ -276,12 +266,8 @@ Result fromBinary(const BinaryOperator* op) {
         return scalar * -value;
       }
     }
-  case BO_LT:
-  case BO_LE:
-  case BO_GT:
-  case BO_GE:
-    break;
-  } 
+  }
+  assert(false); // Unknown binary operation. Only assignment, addition, subtraction and multiplication are permitted
   return Result();
 }
 
@@ -384,24 +370,25 @@ Condition fromComparison(const BinaryOperator* op, bool negate) {
 
 /* Blocks */
 
-typedef map<string, unsigned int> Counters;
-typedef map<string, EqnVar*> VarMap;
-typedef map<const CFGBlock*, set<string> > BlockVars;
+struct Block : public map<string,Result> {
+  Result& operator[](const string& key) {
+    iterator it = this->find(key);
+    if (it != this->end())
+      return it->second;
+    Vector vector;
+    vector[key] = 1;
+    pair<iterator,bool> p = this->insert(pair<const string, Result>(key, Result(vector, 0)));
+    return p.first->second;
+  }
+};
 
-void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) {
-  Counters counters;
-  string block_id = toString(block->getBlockID());
-  VarMap vars;
 
-  for (set<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();
+vector<Block> splitBlock(const CFGBlock* block) {
+  vector<Block> subBlocks;
+
+  for (CFGBlock::const_iterator
+         it = block->begin(),
+         ei = block->end();
        it != ei;
        ++it) {
     const CFGStmt* cfg_stmt = it->getAs<CFGStmt>();
@@ -437,78 +424,161 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) {
         }
       }
     }
-    if (name == "")
-      continue;
 
-    string count = toString(counters[name]);
-    EqnVar* var = &system.variable(name + '-' + block_id + '[' + count + ']');
-    EqnVar* negative_var = &system.variable(-name + '-' + block_id + '[' + count + ']');
-    counters[name]++;
-    for (int negative = 0; negative < 2; ++negative) { // one loop for positive, the other for negative
-      if (negative) {
-	result = -result;
-      }
-      
-      EqnExpr* expression;
+    if (name != "") {
+      if (subBlocks.empty())
+        subBlocks.push_back(Block());
+      Block& subBlock = subBlocks.back();
 
-      if (result.first.size() > 0) {
-        // make sure all our variables exist in vars
+      bool make_new = subBlock.find(name) != subBlock.end();
+      if (!make_new) {
         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");
+          if (subBlock.find(it->first) != subBlock.end()) {
+            make_new = true;
+            break;
+          }
         }
+      }
+      if (make_new) {
+        Block newBlock;
+        newBlock[name] = result;
+        subBlocks.push_back(newBlock);
+      } else {
+        subBlock[name] = result;
+      }
+    }
+  }
 
-        // set up the min-cost-flow operator
-        vector<ZBar> supplies;
-        vector<pair<int,int> > arcs;
-        vector<EqnExpr*> minCostArgs;
-        ZBar dummy_value = 0;
-        supplies.push_back(dummy_value); // dummy node to suck up flow
-        int index = 1; // the solver uses 1-indexing, for some reason
-        for (map<std::string,EqnVar*>::iterator
-               it = vars.begin(),
-               ei = vars.end();
-             it != ei;
-             it++) {
-          index++;
-          supplies.push_back(result.first[it->first]);
-          dummy_value -= result.first[it->first];
-          if (it->first[0] == '-')
-            arcs.push_back(pair<int,int>(1,index));
-          else 
-            arcs.push_back(pair<int,int>(index,1));
-          minCostArgs.push_back(vars[it->first]);
+  return subBlocks;
+}
+
+typedef map<string, unsigned int> Counters;
+
+string var_name(const int& i, const string& block_id) {
+  return toString(i) + '-' + block_id;
+}
+
+void runOnBlock(const ConstraintMatrix& T, const CFGBlock* block, EqnSys& system) {
+
+  int size = T.size();
+  string block_id = toString(block->getBlockID());
+  vector<unsigned int> counters(size);
+  vector<EqnVar*> vars(size);
+
+  vector<EqnExpr*> infArgs;
+  infArgs.push_back(&system.constant(-infinity<ZBar>()));
+  infArgs.push_back(&system.constant(infinity<ZBar>()));
+  for (int i = 0; i < size; ++i) {
+    vars[i] = &system.variable(var_name(i, block_id)+"-pre");
+    if (system[*vars[i]] == NULL) {
+      system[*vars[i]] = &system.maxExpression(infArgs);
+    }
+  }
+
+  vector<Block> subBlocks = splitBlock(block);
+
+  map<string,int> mcf_indices; // 1-indexed, for the mcf stuff
+  int mcf_vert_count = 1;
+  vector<pair<int,int> > mcf_edges;
+  {
+    for (int j = 0; j < size; ++j) {
+      string from = "";
+      string to = "";
+      for (map<string,int>::const_iterator
+             jt = T[j].begin(),
+             ej = T[j].end();
+           jt != ej;
+           ++jt) {
+        if (mcf_indices.find(jt->first) == mcf_indices.end()) {
+          mcf_indices[jt->first] = ++mcf_vert_count;
+        }
+        assert(jt->second == 1 || jt->second == -1);
+        assert(jt->second != 1 || from == "");
+        assert(jt->second != -1 || to == "");
+        if (jt->second == 1)
+          from = jt->first;
+        if (jt->second == -1)
+          to = jt->first;
+      }
+      int source = (from == "" ? 1 : mcf_indices[from]);
+      int dest = (to == "" ? 1 : mcf_indices[to]);
+      
+      mcf_edges.push_back(pair<int,int>(source,dest));
+    }
+  }
+
+  
+
+  for (int blockIndex = 0, blockSize = subBlocks.size(); blockIndex < blockSize; ++blockIndex) {
+    Block& subBlock = subBlocks[blockIndex];
+
+    vector<EqnVar*> nextVars(size);
+    for (int i = 0; i < size; ++i) {
+      const map<string,int>& tk = T[i];
+
+      ZBar b = 0;
+      map<string,int> indices;
+      for (map<string,int>::const_iterator
+             tk_it = tk.begin(),
+             tk_end = tk.end();
+           tk_it != tk_end;
+           tk_it++) {
+        b += ZBar(tk_it->second) * subBlock[tk_it->first].second;
+      }
+
+      vector<ZBar> g(mcf_vert_count);
+      for (map<string,int>::const_iterator
+             tk_it = tk.begin(),
+             tk_end = tk.end();
+           tk_it != tk_end;
+           tk_it++) { // each column of Tk
+        const map<string,ZBar>& A = subBlock[tk_it->first].first;
+        for (map<string,ZBar>::const_iterator
+               A_it = A.begin(),
+               A_end = A.end();
+             A_it != A_end;
+             A_it++) { // each row of A
+          ZBar value = A_it->second * ZBar(tk_it->second);
+          g[mcf_indices[A_it->first]-1] += value;
+          g[0] -= value;
         }
-        supplies[0] = dummy_value;
+      }
+
+      vector<EqnExpr*> args(size);
+      for (int j = 0; j < size; ++j) {
+        assert(vars[j] != NULL);
+        args[j] = vars[j];
+      }
+      
+      EqnExpr* minCostExpr = &system.expression(new MinCostFlow<ZBar>(g, mcf_edges), args);
 
-        EqnExpr* minCostExpr = &system.expression(new MinCostFlow<ZBar>(supplies, arcs), minCostArgs);
-        
+      EqnExpr* expression;
+      if (b == 0) {
+        expression = minCostExpr;
+      } else {
         // add the constant factor to the min-cost bit
         vector<EqnExpr*> additionArgs;
-        additionArgs.push_back(&system.constant(result.second));
+        additionArgs.push_back(&system.constant(b));
         additionArgs.push_back(minCostExpr);
         expression = &system.expression(new Addition<ZBar>(), additionArgs);
-      } else {
-        expression = &system.constant(result.second);
       }
 
-      // max(-inf, expr), so strategy iteration will work
+      string count = toString(counters[i]);
+      counters[i]++;
+      EqnVar* newVar = &system.variable(var_name(i, block_id)+'-'+count);
+      
+      // make it max(-inf, expr), so strategy iteration will work
       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);
+      system[*newVar] = &system.maxExpression(maxArgs);
+      nextVars[i] = newVar;
     }
-    vars[name] = var;
-    vars[-name] = negative_var;
-    block_vars[block].insert(name);
-    block_vars[block].insert(-name);
+    vars = nextVars; // update our variable listings
   }
 
   // add to our successor entry values
@@ -519,35 +589,43 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) {
        ++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");
+
+    for (int i = 0; i < size; ++i) {
+      EqnVar* var = &system.variable(var_name(i, toString((*it)->getBlockID()))+"-pre");
       if (system[*var] == NULL) {
 	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)
-        expr = &system.constant(-infinity<ZBar>());
-      } 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
-	vector<EqnExpr*> minArgs;
-	minArgs.push_back(&system.constant(val));
-	minArgs.push_back(jt->second);
-	expr = &system.expression(new Minimum<ZBar>(), minArgs);
+      if (T[i].size() == 1) { // only one value in this row, so it's okay for a test
+        ZBar val = infinity<ZBar>();
+        Vector::iterator cond_finder;
+        if (T[i].begin()->second < 0)
+          cond_finder = cond.find('-' + T[i].begin()->first);
+        else
+          cond_finder = cond.find(T[i].begin()->first);
+        if (cond_finder != cond.end()) {
+          val = cond_finder->second;
+          //val *= ; // potentially change it's sign
+        }
+        if (val == -infinity<ZBar>()) {
+          // don't do anything here: min(-inf, x) = -inf  (for all x)
+          expr = &system.constant(-infinity<ZBar>());
+        } else if (val == infinity<ZBar>()) {
+          // no need to have a min here: min(inf, x) = x  (for all x)
+          expr = vars[i];
+        } else {
+          // need a min here
+          vector<EqnExpr*> minArgs;
+          minArgs.push_back(&system.constant(val));
+          minArgs.push_back(vars[i]);
+          expr = &system.expression(new Minimum<ZBar>(), minArgs);
+        }
+      } else { // more than one value in this row, so leave it for now...
+        expr = vars[i];
       }
-
       system[*var]->arguments().push_back(expr);
     }
   }
@@ -565,33 +643,13 @@ IntervalAnalysis :: IntervalAnalysis(AnalysisDeclContext &context)
 IntervalAnalysis :: ~IntervalAnalysis() {
 }
 
-void IntervalAnalysis::runOnAllBlocks(const Decl& decl) {
+map<CFGBlock*,vector<ZBar> > IntervalAnalysis::runOnAllBlocks(const Decl& decl, const ConstraintMatrix& T) {
   const CFG *cfg = this->context->getCFG();
 
   cfg->dump(context->getASTContext().getLangOpts(),
             llvm::sys::Process::StandardErrHasColors());
 
-  EqnSys system; 
-  BlockVars block_vars;
-
-  vector<EqnExpr*> infArg; 
-  infArg.push_back(&system.constant(-infinity<ZBar>())); // left-most argument has to be -infinity
-  infArg.push_back(&system.constant(infinity<ZBar>()));
-  set<string>& function_arguments = block_vars[&cfg->getEntry()];
-  string block_id = toString(cfg->getEntry().getBlockID());
-  if (const FunctionDecl* func = dyn_cast<const FunctionDecl>(&decl)) {
-    for (unsigned int i = func->getNumParams(); i > 0; i--) {
-      string name = func->getParamDecl(i-1)->getNameAsString();
-
-      // add the variables to the first block
-      function_arguments.insert(name);
-      function_arguments.insert(neg(name));
-      
-      // set the vars to infinity (unconstrained)
-      system[system.variable(name + '-' + block_id + "-pre")] = &system.maxExpression(infArg);
-      system[system.variable(neg(name) + '-' + block_id + "-pre")] = &system.maxExpression(infArg);
-    }
-  }
+  EqnSys system;
 
   set<const CFGBlock*> seen;
   deque<const CFGBlock*> todo;
@@ -605,25 +663,41 @@ void IntervalAnalysis::runOnAllBlocks(const Decl& decl) {
     }
     seen.insert(block);
     todo.pop_front();
-    runOnBlock(block, system, block_vars);
+    runOnBlock(T, block, system);
     for (CFGBlock::const_succ_iterator it = block->succ_begin(),
-                                       ei = block->succ_end();
+           ei = block->succ_end();
          it != ei;
          it++ ) {
       todo.push_back(*it);
     }
   }
 
-  llvm::errs() << toString(system) << "\n";
-
   system.indexMaxExpressions();
 
   Solver<ZBar> solver(system);
 
-  for (unsigned int i = 0, size = system.variableCount(); i < size; ++i) {
-    EqnVar& var = system.variable(i);
-    llvm::errs() << toString(var.name()) << " = " << toString(solver.solve(var)) << "\n";
+  map<CFGBlock*, vector<ZBar> > resultMap;
+
+  for (int i = 0; i < system.variableCount(); ++i) {
+    solver.solve(system.variable(i));
+  }
+
+  for (CFG::const_iterator
+         it = cfg->begin(),
+         ei = cfg->end();
+       it != ei;
+       ++it) {
+    vector<ZBar>& vector = resultMap[*it];
+    string block_id = toString((*it)->getBlockID());
+    for (int i = 0, size = T.size(); i < size; ++i) {
+      EqnVar& var = system.variable(var_name(i, block_id) + "-pre");
+      vector.push_back(solver.solve(var));
+    }
   }
+
+  llvm::errs() << toString(system) << "\n";
+
+  return resultMap;
 }