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

1 files changed, 101 insertions, 1 deletions

diff --git a/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp b/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp
index badb671..c1e0273 100644
--- a/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp
+++ b/clang/lib/StaticAnalyzer/Checkers/IntervalTest.cpp
@@ -7,6 +7,15 @@
 
 using namespace clang;
 using namespace ento;
+using namespace std;
+
+#include <sstream>
+template<typename T>
+string toString(const T& obj) {
+  stringstream stream;
+  stream << obj;
+  return stream.str();
+}
 
 namespace {
 class IntervalTest: public Checker<check::ASTCodeBody> {
@@ -14,7 +23,98 @@ public:
   void checkASTCodeBody(const Decl *D, AnalysisManager& mgr,
                         BugReporter &BR) const {
     if (IntervalAnalysis *a = mgr.getAnalysis<IntervalAnalysis>(D)) {
-      a->runOnAllBlocks(*D);
+      CFG* cfg = mgr.getCFG(D);
+
+      set<string> variables;
+
+      if (const FunctionDecl* func = dyn_cast<const FunctionDecl>(D)) {
+        for (unsigned int i = func->getNumParams(); i > 0; i--) {
+          variables.insert(func->getParamDecl(i-1)->getNameAsString());
+        }
+      }
+      for (CFG::iterator
+             it = cfg->begin(),
+             ei = cfg->end();
+           it != ei;
+           ++it) {
+        for (CFGBlock::iterator
+               block_it = (*it)->begin(),
+               block_end = (*it)->end();
+             block_it != block_end;
+             block_it++) {
+          const CFGStmt* cfg_stmt = block_it->getAs<CFGStmt>();
+          const Stmt* stmt = cfg_stmt->getStmt();
+          if (stmt->getStmtClass() == Stmt::BinaryOperatorClass) {
+            const BinaryOperator* binop = static_cast<const BinaryOperator*>(stmt);
+            if (binop->isAssignmentOp()) {
+              const Expr* left = binop->getLHS()->IgnoreParenCasts();
+              if (left->getStmtClass() == Stmt::DeclRefExprClass) {
+                variables.insert(static_cast<const DeclRefExpr*>(left)->getNameInfo().getAsString());
+              }
+            }
+          } else if (stmt->getStmtClass() == Stmt::DeclStmtClass) {
+            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);
+                variables.insert(decl->getNameAsString());
+                jt++;
+                if (jt != ej) {
+                  llvm::errs() << "Only the first declaration in a multi-declaration statement is used.\n";
+                }
+                break; // only take the first one, for now
+              }
+            }
+          }
+        }
+      }
+
+
+
+      vector<string> labels;
+      ConstraintMatrix T;
+      set<string>::iterator end = variables.end();
+      for (set<string>::iterator it = variables.begin();
+           it != end;
+           ++it) {
+        map<string,int> pos_row;
+        pos_row[*it] = 1;
+        T.push_back(pos_row);
+        labels.push_back(*it);
+
+        map<string,int> neg_row;
+        neg_row[*it] = -1;
+        T.push_back(neg_row);
+        labels.push_back("-" + *it);
+
+        for (set<string>::iterator jt = variables.begin();
+             jt != end;
+             ++jt) {
+          if (it != jt) {
+            map<string,int> diff_row;
+            diff_row[*it] = 1;
+            diff_row[*jt] = -1;
+            T.push_back(diff_row);
+            labels.push_back(*it + " - " + *jt);
+          }
+        }
+      }
+
+      map<CFGBlock*,vector<ZBar> > result = a->runOnAllBlocks(*D, T);
+
+      for (map<CFGBlock*,vector<ZBar> >::iterator
+             it = result.begin(),
+             ei = result.end();
+           it != ei;
+           ++it) {
+        llvm::errs() << "Block " << toString(it->first->getBlockID()) << ": \n";
+        for (unsigned int i = 0; i < T.size(); ++i) {
+          llvm::errs() << "\t" << labels[i] << " <= " << toString(it->second[i]) << "\n";
+        }
+      }
     }
   }
 };