diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 69 | ||||
| -rw-r--r-- | lib/Core/Executor.h | 4 | ||||
| -rw-r--r-- | lib/Core/ExecutorTimers.cpp | 66 |
3 files changed, 76 insertions, 63 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 5590af41..85cb8e8d 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -405,6 +405,10 @@ namespace klee { RNG theRNG; } +// XXX hack +extern "C" unsigned dumpStates, dumpPTree; +unsigned dumpStates = 0, dumpPTree = 0; + const char *Executor::TerminateReasonNames[] = { [ Abort ] = "abort", [ Assert ] = "assert", @@ -2904,6 +2908,8 @@ void Executor::run(ExecutionState &initialState) { executeInstruction(state, ki); processTimers(&state, maxInstructionTime * numSeeds); + if (::dumpStates) dumpStates(); + if (::dumpPTree) dumpPTree(); updateStates(&state); if ((stats::instructions % 1000) == 0) { @@ -2958,6 +2964,8 @@ void Executor::run(ExecutionState &initialState) { executeInstruction(state, ki); processTimers(&state, maxInstructionTime); + if (::dumpStates) dumpStates(); + if (::dumpPTree) dumpPTree(); checkMemoryUsage(); @@ -4082,6 +4090,67 @@ int *Executor::getErrnoLocation(const ExecutionState &state) const { #endif } + +void Executor::dumpPTree() { + if (!::dumpPTree) return; + + char name[32]; + snprintf(name, sizeof(name),"ptree%08d.dot", (int) stats::instructions); + auto os = interpreterHandler->openOutputFile(name); + if (os) { + processTree->dump(*os); + } + + ::dumpPTree = 0; +} + +void Executor::dumpStates() { + if (!::dumpStates) return; + + auto os = interpreterHandler->openOutputFile("states.txt"); + + if (os) { + for (ExecutionState *es : states) { + *os << "(" << es << ","; + *os << "["; + auto next = es->stack.begin(); + ++next; + for (auto 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"; + } + } + + ::dumpStates = 0; +} + /// Interpreter *Interpreter::create(LLVMContext &ctx, const InterpreterOptions &opts, diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index e2aab56c..851a52ec 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -479,6 +479,10 @@ private: void printDebugInstructions(ExecutionState &state); void doDumpStates(); + /// Only for debug purposes; enable via debugger or klee-control + void dumpStates(); + void dumpPTree(); + public: Executor(llvm::LLVMContext &ctx, const InterpreterOptions &opts, InterpreterHandler *ie); diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp index e1d6684d..81ab7651 100644 --- a/lib/Core/ExecutorTimers.cpp +++ b/lib/Core/ExecutorTimers.cpp @@ -62,10 +62,6 @@ public: static const time::Span kMilliSecondsPerTick(time::milliseconds(100)); static volatile unsigned timerTicks = 0; -// XXX hack -extern "C" unsigned dumpStates, dumpPTree; -unsigned dumpStates = 0, dumpPTree = 0; - static void onAlarm(int) { ++timerTicks; } @@ -114,63 +110,7 @@ void Executor::processTimers(ExecutionState *current, ticks = 1; } - if (ticks || dumpPTree || dumpStates) { - if (dumpPTree) { - char name[32]; - snprintf(name, sizeof(name), "ptree%08d.dot", (int) stats::instructions); - auto os = interpreterHandler->openOutputFile(name); - if (os) { - processTree->dump(*os); - } - - dumpPTree = 0; - } - - if (dumpStates) { - auto os = interpreterHandler->openOutputFile("states.txt"); - - if (os) { - for (ExecutionState *es : states) { - *os << "(" << es << ","; - *os << "["; - auto next = es->stack.begin(); - ++next; - for (auto 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"; - } - } - - dumpStates = 0; - } - + if (ticks) { if (maxInstTime && current && std::find(removedStates.begin(), removedStates.end(), current) == removedStates.end()) { @@ -183,10 +123,10 @@ void Executor::processTimers(ExecutionState *current, if (!timers.empty()) { auto time = time::getWallTime(); - for (std::vector<TimerInfo*>::iterator it = timers.begin(), + 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; |