#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"
#include <iostream>

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();
}

#include <algorithm> 
#include <functional> 
#include <cctype>
#include <locale>

// trim from start
static inline std::string &ltrim(std::string &s) {
        s.erase(s.begin(), std::find_if(s.begin(), s.end(), std::not1(std::ptr_fun<int, int>(std::isspace))));
        return s;
}

// trim from end
static inline std::string &rtrim(std::string &s) {
        s.erase(std::find_if(s.rbegin(), s.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), s.end());
        return s;
}

// trim from both ends
static inline std::string &trim(std::string &s) {
        return ltrim(rtrim(s));
}

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);
        }
      }
    }*/

    vector<string> labels;
    ConstraintMatrix T;
    while (cin.good()) {
      string line;
      getline(cin, line);
      trim(line);

      if (line.length() == 0)
        continue;

      map<string,int> row;
      size_t neg_sign_index = line.find('-');
      if (neg_sign_index == string::npos) {
        row[line] = 1;
        labels.push_back(line);
      } else if (neg_sign_index == 0) {
        row[line.substr(1)] = -1;
        labels.push_back('-'+line.substr(1));
      } else {
        string left = line.substr(0, neg_sign_index);
        string right = line.substr(neg_sign_index+1);
        trim(left);
        trim(right);
        if (left != right) {
          row[left] = 1;
          row[right] = -1;
        }
        labels.push_back(left + '-' + right);
      }
      T.push_back(row);
    }


    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>();
}