A few fixes to the MCF solver, and equation stuff

General work on the equation systems. Trying to get them to generate
correctly with the MCF stuff. It's harder than it seems!

1 files changed, 136 insertions, 27 deletions

diff --git a/clang/lib/Analysis/Interval.cpp b/clang/lib/Analysis/Interval.cpp
index 7096d75..e643f5e 100644
--- a/clang/lib/Analysis/Interval.cpp
+++ b/clang/lib/Analysis/Interval.cpp
@@ -8,6 +8,8 @@
 #include "clang/Analysis/Analyses/IntervalSolver/Complete.hpp"
 #include "clang/Analysis/Analyses/IntervalSolver/VariableAssignment.hpp"
 #include "clang/Analysis/Analyses/IntervalSolver/EquationSystem.hpp"
+
+#include "MCFSimplex.h"
   
 #include "llvm/ADT/PostOrderIterator.h"
 #include "llvm/ADT/DenseMap.h"
@@ -41,6 +43,11 @@ std::ostream& operator<<(std::ostream& cout, const std::pair<K,V>& v) {
   cout << "(" << v.first << ", " << v.second << ")";
   return cout;
 }
+template<typename V>
+std::ostream& operator<<(std::ostream& cout, const std::pair<Variable<Complete<int64_t> >*, V>& v) {
+  cout << "(" << v.first->name() << ", " << v.second << ")";
+  return cout;
+}
 
 template<typename V>
 std::ostream& operator<<(std::ostream& cout, const std::vector<V>& v) {
@@ -485,6 +492,86 @@ Condition fromComparison(const BinaryOperator* op, bool negate) {
   return cond;
 }
 
+
+struct MinCostFlow : public Operator<ZBar> {
+  MinCostFlow(const std::vector<std::pair<EqnVar*, ZBar> >& supplies)
+    : solver(0, 0) {
+    assert(supplies.size() % 2 == 0);
+
+    if (supplies.size() == 0)
+      return;
+
+    MCFClass::FNumber* deficits = new MCFClass::FNumber[supplies.size()];
+    MCFClass::Index* starts = new MCFClass::Index[supplies.size()];
+    MCFClass::Index* ends = new MCFClass::Index[supplies.size()];
+
+    for (int i = 0, size = supplies.size(); i < size; i += 2) {
+      deficits[i] = -supplies[i].second.as<MCFClass::FNumber>();
+      deficits[i+1] = -supplies[i+1].second.as<MCFClass::FNumber>();
+
+      starts[i] = i+1;
+      ends[i] = i+2;
+
+      starts[i+1] = i+2;
+      ends[i+1] = i+1;
+
+      printableSupply.push_back(supplies[i].second);
+      printableSupply.push_back(supplies[i+1].second);
+    }
+
+    solver.LoadNet(supplies.size(), supplies.size(), // max nodes/arcs
+                   supplies.size(), supplies.size(), // current nodes/arcs
+                   NULL, NULL, // arcs have inf cap, zero cost (to begin)
+                   deficits, // deficits for each node
+                   starts, ends); // start/end of each edge
+
+    delete[] deficits;
+    delete[] starts;
+    delete[] ends;
+  }
+
+  ZBar eval(const std::vector<ZBar>& args) const {
+    if (args.size() == 0)
+      return 0;
+    for (int i = 0, size = args.size(); i < size; ++i) {
+      //if (args[i] == infinity<ZBar>()) {
+      //  if (!solver.IsClosedArc(i))
+      //      solver.CloseArc(i);
+      //} else {
+      //  if (solver.IsClosedArc(i))
+      //    solver.OpenArc(i);
+      solver.ChgCost(i, args[i].as<MCFClass::CNumber>());
+      //}
+    }
+    std::cerr << "MCF" << this << "<" << printableSupply << ">(" << args << ")" << " = ";
+    solver.SolveMCF();
+    if (solver.MCFGetStatus() == MCFClass::kUnfeasible){
+      std::cerr << -infinity<ZBar>() << std::endl;
+      return -infinity<ZBar>();
+    } else {
+      if (solver.MCFGetFO() == MCFClass::Inf<MCFClass::FONumber>()) {
+        std::cerr << infinity<ZBar>() << std::endl;
+        return infinity<ZBar>();
+      } else if (solver.MCFGetFO() == -MCFClass::Inf<MCFClass::FONumber>()) {
+        std::cerr << -infinity<ZBar>() << std::endl;
+        return -infinity<ZBar>();        
+      } else {
+        ZBar result = solver.MCFGetFO();
+        std::cerr << result << std::endl;
+        return result;
+      }
+    }
+  }
+
+  virtual void print(std::ostream& cout) const {
+    cout << "MCF" << this << "<" << printableSupply << ">";
+  }
+  
+  mutable MCFSimplex solver;
+  std::vector<ZBar> printableSupply;
+};
+
+
 /* Blocks */
 
 typedef std::map<std::string, unsigned int> Counters;
@@ -551,28 +638,41 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) {
       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);
+      EqnExpr* expression;
+
+      if (result.first.size() > 0) {
+        // set up the min-cost stuff
+        std::vector<EqnExpr*> minCostArgs;
+        std::vector<std::pair<EqnVar*, ZBar> > varCosts;
+        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");
+
+          EqnVar& var = *vars[it->first];
+          EqnVar& negVar = *vars[negate_string(it->first)];
+
+          varCosts.push_back(std::pair<EqnVar*, ZBar>(&var, it->second));
+          varCosts.push_back(std::pair<EqnVar*, ZBar>(&negVar, -it->second));
+
+          minCostArgs.push_back(&var);
+          minCostArgs.push_back(&negVar);
+        }
+        EqnExpr* minCostExpr = &system.expression(new MinCostFlow(varCosts), minCostArgs);
+        
+        // add the constant factor to the min-cost bit
+        std::vector<EqnExpr*> additionArgs;
+        additionArgs.push_back(&system.constant(result.second));
+        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
       std::vector<EqnExpr*> maxArgs;
       maxArgs.push_back(&system.constant(-infinity<ZBar>()));
       maxArgs.push_back(expression);
@@ -612,6 +712,7 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) {
       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;
@@ -623,7 +724,9 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) {
 	expr = &system.expression(new Minimum<ZBar>(), minArgs);
       }
 
-      if (expr) {
+      system[*var]->arguments().push_back(expr);
+
+      /*if (expr) {
 	std::set<std::string> ignore;
 	for (VarMap::iterator
 	       variables = vars.begin(),
@@ -638,10 +741,13 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) {
 	  for (int negate = 0; negate < 2; ++negate) {
 	    std::string var_name = negate ? negate_string(variables->first) : variables->first;
             if (cond[var_name] == infinity<ZBar>()) {
+              // min(x, inf) = x
               plusArgs.push_back(vars[var_name]);
             } else if (cond[var_name] == -infinity<ZBar>()) {
+              // min(x, -inf) = -inf
               plusArgs.push_back(&system.constant(-infinity<ZBar>()));
             } else {
+              // min(x, y) = ?
               std::vector<EqnExpr*> minArgs;
               minArgs.push_back(vars[var_name]);
               minArgs.push_back(&system.constant(cond[var_name]));
@@ -656,7 +762,7 @@ void runOnBlock(const CFGBlock* block, EqnSys& system, BlockVars& block_vars) {
 	  expr = &system.expression(new Guard<ZBar>(), guard_args);
 	}
 	system[*var]->arguments().push_back(expr);
-      }
+        }*/
     }
   }
 }
@@ -683,6 +789,7 @@ void IntervalAnalysis::runOnAllBlocks(const Decl& decl) {
   BlockVars block_vars;
 
   std::vector<EqnExpr*> infArg; 
+  infArg.push_back(&system.constant(-infinity<ZBar>())); // left-most argument has to be -infinity
   infArg.push_back(&system.constant(infinity<ZBar>()));
   std::set<std::string>& function_arguments = block_vars[&cfg->getEntry()];
   std::string block_id = toString(cfg->getEntry().getBlockID());
@@ -690,11 +797,13 @@ void IntervalAnalysis::runOnAllBlocks(const Decl& decl) {
     for (unsigned int i = func->getNumParams(); i > 0; i--) {
       std::string name = func->getParamDecl(i-1)->getNameAsString();
 
-      function_arguments.insert(name); // add it to the first block's vars
-      function_arguments.insert(negate_string(name));  // add it to the first block's vars
-
-      system[system.variable(name + '-' + block_id + "-pre")] = &system.maxExpression(infArg); // set the vars to infinity in the system here
-      system[system.variable(negate_string(name) + '-' + block_id + "-pre")] = &system.maxExpression(infArg); // set the vars to infinity in the system here
+      // add the variables to the first block
+      function_arguments.insert(name);
+      function_arguments.insert(negate_string(name));
+      
+      // set the vars to infinity (unconstrained)
+      system[system.variable(name + '-' + block_id + "-pre")] = &system.maxExpression(infArg);
+      system[system.variable(negate_string(name) + '-' + block_id + "-pre")] = &system.maxExpression(infArg);
     }
   }