#include "ClangSACheckers.h"
#include "clang/StaticAnalyzer/Core/Checker.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
#include "clang/Analysis/Analyses/Interval.h"
#include "clang/Analysis/CallGraph.h"
#include "llvm/Support/Process.h"

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> {
public:
  void checkASTCodeBody(const Decl *D, AnalysisManager& mgr,
                        BugReporter &BR) const {
    if (IntervalAnalysis *a = mgr.getAnalysis<IntervalAnalysis>(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";
        }
      }
    }
  }
};
}

void ento::registerIntervalTestChecker(CheckerManager &mgr) {
  mgr.registerChecker<IntervalTest>();
}