From 4eb050e2999bef42f70dcc72a8ee283f8803ce67 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Tue, 30 Jul 2019 18:45:42 +0100 Subject: ExecutorTimers: refactor and move to support lib - moves timer handling from Executor into support lib - introduces TimerGroup, removes TimerInfo/WriteStatsTimer/UpdateReachableTimer/WriteIStatsTimer classes - removes ExecutorTimers.cpp and ExecutorTimerInfo.h - removes -max-instruction-time flag (see #1114) --- lib/Core/ExecutorTimers.cpp | 108 -------------------------------------------- 1 file changed, 108 deletions(-) (limited to 'lib/Core/ExecutorTimers.cpp') diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp index 8ebe5aed..e69de29b 100644 --- a/lib/Core/ExecutorTimers.cpp +++ b/lib/Core/ExecutorTimers.cpp @@ -1,108 +0,0 @@ -//===-- 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 "CoreStats.h" -#include "Executor.h" -#include "ExecutorTimerInfo.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/Support/ErrorHandling.h" -#include "klee/Internal/System/Time.h" -#include "klee/OptionCategories.h" - -#include "llvm/IR/Function.h" -#include "llvm/Support/CommandLine.h" - -#include -#include -#include -#include -#include - -using namespace llvm; -using namespace klee; - -namespace klee { -cl::opt - MaxTime("max-time", - cl::desc("Halt execution after the specified number of seconds. " - "Set to 0s to disable (default=0s)"), - cl::init("0s"), - cl::cat(TerminationCat)); - -cl::opt - TimerInterval("timer-interval", - cl::desc("Minimum interval to check timers (default=1s)"), - cl::init("1s"), - cl::cat(TerminationCat)); // StatsCat? -} - -/// - -class HaltTimer : public Executor::Timer { - Executor *executor; - -public: - HaltTimer(Executor *_executor) : executor(_executor) {} - ~HaltTimer() {} - - void run() { - klee_message("HaltTimer invoked"); - executor->setHaltExecution(true); - } -}; - -/// - -void Executor::initTimers() { - const time::Span maxTime(MaxTime); - if (maxTime) { - addTimer(new HaltTimer(this), maxTime); - } -} - -/// - -void Executor::addTimer(Timer *timer, time::Span rate) { - timers.push_back(new TimerInfo(timer, rate)); -} - -void Executor::processTimers(ExecutionState *current, - time::Span maxInstTime) { - const static time::Span minInterval(TimerInterval); - static time::Point lastCheckedTime; - const auto currentTime = time::getWallTime(); - const auto duration = currentTime - lastCheckedTime; - - if (duration < minInterval) return; - - // check max instruction time - if (maxInstTime && current && - std::find(removedStates.begin(), removedStates.end(), current) == removedStates.end() && - duration > maxInstTime) { - klee_warning("max-instruction-time exceeded: %.2fs", duration.toSeconds()); - terminateStateEarly(*current, "max-instruction-time exceeded"); - } - - - // check timers - for (auto &timerInfo : timers) { - if (currentTime >= timerInfo->nextFireTime) { - timerInfo->timer->run(); - timerInfo->nextFireTime = currentTime + timerInfo->rate; - } - } - - lastCheckedTime = currentTime; -} -- cgit v1.2.3