#include "expr/Lexer.h"
#include "expr/Parser.h"

#include "klee/Constraints.h"
#include "klee/Expr.h"
#include "klee/Solver.h"
#include "klee/util/ExprPPrinter.h"
#include "klee/util/ExprVisitor.h"

#include "llvm/ADT/StringExtras.h"
#include "llvm/Support/CommandLine.h"
#include "llvm/Support/ManagedStatic.h"
#include "llvm/Support/MemoryBuffer.h"
#include "llvm/Support/Streams.h"
#include "llvm/System/Signals.h"

#include <iomanip>
#include <sstream>

using namespace llvm;
using namespace klee;
using namespace klee::expr;

namespace {
  llvm::cl::opt<std::string>
  InputFile(llvm::cl::desc("<input query log>"), llvm::cl::Positional,
            llvm::cl::init("-"));

  enum ToolActions {
    PrintTokens,
    PrintAST,
    Evaluate
  };

  static llvm::cl::opt<ToolActions> 
  ToolAction(llvm::cl::desc("Tool actions:"),
             llvm::cl::init(Evaluate),
             llvm::cl::values(
             clEnumValN(PrintTokens, "print-tokens",
                        "Print tokens from the input file."),
             clEnumValN(PrintAST, "print-ast",
                        "Print parsed AST nodes from the input file."),
             clEnumValN(Evaluate, "evaluate",
                        "Print parsed AST nodes from the input file."),
             clEnumValEnd));
}

static std::string escapedString(const char *start, unsigned length) {
  std::stringstream s;
  for (unsigned i=0; i<length; ++i) {
    char c = start[i];
    if (isprint(c)) {
      s << c;
    } else if (c == '\n') {
      s << "\\n";
    } else {
      s << "\\x" 
        << hexdigit(((unsigned char) c >> 4) & 0xF) 
        << hexdigit((unsigned char) c & 0xF);
    }
  }
  return s.str();
}

static void PrintInputTokens(const MemoryBuffer *MB) {
  Lexer L(MB);
  Token T;
  do {
    L.Lex(T);
    llvm::cout << "(Token \"" << T.getKindName() << "\" "
               << "\"" << escapedString(T.start, T.length) << "\" "
               << T.length << " "
               << T.line << " " << T.column << ")\n";
  } while (T.kind != Token::EndOfFile);
}

static bool PrintInputAST(const char *Filename,
                          const MemoryBuffer *MB) {
  Parser *P = Parser::Create(Filename, MB);
  P->SetMaxErrors(20);
  while (Decl *D = P->ParseTopLevelDecl()) {
    if (!P->GetNumErrors())
      D->dump();
    delete D;
  }

  bool success = true;
  if (unsigned N = P->GetNumErrors()) {
    llvm::cerr << Filename << ": parse failure: "
               << N << " errors.\n";
    success = false;
  }
  delete P;

  return success;
}

static bool EvaluateInputAST(const char *Filename,
                          const MemoryBuffer *MB) {
  std::vector<Decl*> Decls;
  Parser *P = Parser::Create(Filename, MB);
  P->SetMaxErrors(20);
  while (Decl *D = P->ParseTopLevelDecl()) {
    Decls.push_back(D);
  }

  bool success = true;
  if (unsigned N = P->GetNumErrors()) {
    llvm::cerr << Filename << ": parse failure: "
               << N << " errors.\n";
    success = false;
  }  
  delete P;

  if (!success) {
    for (std::vector<Decl*>::iterator it = Decls.begin(),
           ie = Decls.end(); it != ie; ++it)
      delete *it;
    return success;
  }

  // FIXME: Support choice of solver.
  Solver *S, *STP = new STPSolver(true);
  S = createCexCachingSolver(STP);
  S = createCachingSolver(S);
  S = createIndependentSolver(S);

  unsigned Index = 0;
  for (std::vector<Decl*>::iterator it = Decls.begin(),
         ie = Decls.end(); it != ie; ++it) {
    Decl *D = *it;
    if (QueryCommand *QC = dyn_cast<QueryCommand>(D)) {
      llvm::cout << "Query " << Index << ":\t";

      assert("FIXME: Support counterexample query commands!");
      if (QC->Values.empty() && QC->Objects.empty()) {
        bool result;
        if (S->mustBeTrue(Query(ConstraintManager(QC->Constraints), QC->Query),
                          result)) {
          llvm::cout << (result ? "VALID" : "INVALID");
        } else {
          llvm::cout << "FAIL";
        }
      } else if (!QC->Values.empty()) {
        assert(QC->Objects.empty() && 
               "FIXME: Support counterexamples for values and objects!");
        assert(QC->Values.size() == 1 &&
               "FIXME: Support counterexamples for multiple values!");
        assert(QC->Query->isFalse() &&
               "FIXME: Support counterexamples with non-trivial query!");
        ref<ConstantExpr> result;
        if (S->getValue(Query(ConstraintManager(QC->Constraints), 
                              QC->Values[0]),
                        result)) {
          llvm::cout << "INVALID\n";
          llvm::cout << "\tExpr 0:\t" << result;
        } else {
          llvm::cout << "FAIL";
        }
      } else {
        std::vector< std::vector<unsigned char> > result;
        
        if (S->getInitialValues(Query(ConstraintManager(QC->Constraints), 
                                      QC->Query),
                                QC->Objects, result)) {
          llvm::cout << "INVALID\n";

          for (unsigned i = 0, e = result.size(); i != e; ++i) {
            llvm::cout << "\tArray " << i << ":\t"
                       << "arr" << QC->Objects[i]->id
                       << "[";
            for (unsigned j = 0; j != QC->Objects[i]->size; ++j) {
              llvm::cout << (unsigned) result[i][j];
              if (j + 1 != QC->Objects[i]->size)
                llvm::cout << ", ";
            }
            llvm::cout << "]";
            if (i + 1 != e)
              llvm::cout << "\n";
          }
        } else {
          llvm::cout << "FAIL";
        }
      }

      llvm::cout << "\n";
      ++Index;
    }

    delete D;
  }

  delete S;

  return success;
}

int main(int argc, char **argv) {
  bool success = true;

  llvm::sys::PrintStackTraceOnErrorSignal();
  llvm::cl::ParseCommandLineOptions(argc, argv);

  std::string ErrorStr;
  MemoryBuffer *MB = MemoryBuffer::getFileOrSTDIN(InputFile.c_str(), &ErrorStr);
  if (!MB) {
    llvm::cerr << argv[0] << ": error: " << ErrorStr << "\n";
    return 1;
  }

  switch (ToolAction) {
  case PrintTokens:
    PrintInputTokens(MB);
    break;
  case PrintAST:
    success = PrintInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), MB);
    break;
  case Evaluate:
    success = EvaluateInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(),
                               MB);
    break;
  default:
    llvm::cerr << argv[0] << ": error: Unknown program action!\n";
  }

  delete MB;

  llvm::llvm_shutdown();
  return success ? 0 : 1;
}