//===-- ExecutorTimers.cpp ------------------------------------------------===//
//
//                     The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//

#include "Common.h"

#include "CoreStats.h"
#include "Executor.h"
#include "PTree.h"
#include "StatsTracker.h"

#include "klee/ExecutionState.h"
#include "klee/Internal/Module/InstructionInfoTable.h"
#include "klee/Internal/Module/KInstruction.h"
#include "klee/Internal/Module/KModule.h"
#include "klee/Internal/System/Time.h"

#include "llvm/Function.h"
#include "llvm/Support/CommandLine.h"

#include <unistd.h>
#include <signal.h>
#include <sys/time.h>
#include <math.h>


using namespace llvm;
using namespace klee;

cl::opt<double>
MaxTime("max-time",
        cl::desc("Halt execution after the specified number of seconds (0=off)"),
        cl::init(0));

///

class HaltTimer : public Executor::Timer {
  Executor *executor;

public:
  HaltTimer(Executor *_executor) : executor(_executor) {}
  ~HaltTimer() {}

  void run() {
    std::cerr << "KLEE: HaltTimer invoked\n";
    executor->setHaltExecution(true);
  }
};

///

static const double kSecondsPerTick = .1;
static volatile unsigned timerTicks = 0;

// XXX hack
extern "C" unsigned dumpStates, dumpPTree;
unsigned dumpStates = 0, dumpPTree = 0;

static void onAlarm(int) {
  ++timerTicks;
}

// oooogalay
static void setupHandler() {
  struct itimerval t;
  struct timeval tv;
  
  tv.tv_sec = (long) kSecondsPerTick;
  tv.tv_usec = (long) (fmod(kSecondsPerTick, 1.)*1000000);
  
  t.it_interval = t.it_value = tv;
  
  ::setitimer(ITIMER_REAL, &t, 0);
  ::signal(SIGALRM, onAlarm);
}

void Executor::initTimers() {
  static bool first = true;

  if (first) {
    first = false;
    setupHandler();
  }

  if (MaxTime) {
    addTimer(new HaltTimer(this), MaxTime);
  }
}

///

Executor::Timer::Timer() {}

Executor::Timer::~Timer() {}

class Executor::TimerInfo {
public:
  Timer *timer;
  
  /// Approximate delay per timer firing.
  double rate;
  /// Wall time for next firing.
  double nextFireTime;
  
public:
  TimerInfo(Timer *_timer, double _rate) 
    : timer(_timer),
      rate(_rate),
      nextFireTime(util::getWallTime() + rate) {}
  ~TimerInfo() { delete timer; }
};

void Executor::addTimer(Timer *timer, double rate) {
  timers.push_back(new TimerInfo(timer, rate));
}

void Executor::processTimers(ExecutionState *current,
                             double maxInstTime) {
  static unsigned callsWithoutCheck = 0;
  unsigned ticks = timerTicks;

  if (!ticks && ++callsWithoutCheck > 1000) {
    setupHandler();
    ticks = 1;
  }

  if (ticks || dumpPTree || dumpStates) {
    if (dumpPTree) {
      char name[32];
      sprintf(name, "ptree%08d.dot", (int) stats::instructions);
      std::ostream *os = interpreterHandler->openOutputFile(name);
      if (os) {
        processTree->dump(*os);
        delete os;
      }
      
      dumpPTree = 0;
    }

    if (dumpStates) {
      std::ostream *os = interpreterHandler->openOutputFile("states.txt");
      
      if (os) {
        for (std::set<ExecutionState*>::const_iterator it = states.begin(), 
               ie = states.end(); it != ie; ++it) {
          ExecutionState *es = *it;
          *os << "(" << es << ",";
          *os << "[";
          ExecutionState::stack_ty::iterator next = es->stack.begin();
          ++next;
          for (ExecutionState::stack_ty::iterator sfIt = es->stack.begin(),
                 sf_ie = es->stack.end(); sfIt != sf_ie; ++sfIt) {
            *os << "('" << sfIt->kf->function->getName().str() << "',";
            if (next == es->stack.end()) {
              *os << es->prevPC->info->line << "), ";
            } else {
              *os << next->caller->info->line << "), ";
              ++next;
            }
          }
          *os << "], ";

          StackFrame &sf = es->stack.back();
          uint64_t md2u = computeMinDistToUncovered(es->pc,
                                                    sf.minDistToUncoveredOnReturn);
          uint64_t icnt = theStatisticManager->getIndexedValue(stats::instructions,
                                                               es->pc->info->id);
          uint64_t cpicnt = sf.callPathNode->statistics.getValue(stats::instructions);

          *os << "{";
          *os << "'depth' : " << es->depth << ", ";
          *os << "'weight' : " << es->weight << ", ";
          *os << "'queryCost' : " << es->queryCost << ", ";
          *os << "'coveredNew' : " << es->coveredNew << ", ";
          *os << "'instsSinceCovNew' : " << es->instsSinceCovNew << ", ";
          *os << "'md2u' : " << md2u << ", ";
          *os << "'icnt' : " << icnt << ", ";
          *os << "'CPicnt' : " << cpicnt << ", ";
          *os << "}";
          *os << ")\n";
        }
        
        delete os;
      }

      dumpStates = 0;
    }

    if (maxInstTime>0 && current && !removedStates.count(current)) {
      if (timerTicks*kSecondsPerTick > maxInstTime) {
        klee_warning("max-instruction-time exceeded: %.2fs",
                     timerTicks*kSecondsPerTick);
        terminateStateEarly(*current, "max-instruction-time exceeded");
      }
    }

    if (!timers.empty()) {
      double time = util::getWallTime();

      for (std::vector<TimerInfo*>::iterator it = timers.begin(), 
             ie = timers.end(); it != ie; ++it) {
        TimerInfo *ti = *it;
        
        if (time >= ti->nextFireTime) {
          ti->timer->run();
          ti->nextFireTime = time + ti->rate;
        }
      }
    }

    timerTicks = 0;
    callsWithoutCheck = 0;
  }
}