klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExecutorTimers.cpp
Go to the documentation of this file.
1 //===-- ExecutorTimers.cpp ------------------------------------------------===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #include "Common.h"
11 
12 #include "CoreStats.h"
13 #include "Executor.h"
14 #include "PTree.h"
15 #include "StatsTracker.h"
16 #include "ExecutorTimerInfo.h"
17 
18 #include "klee/ExecutionState.h"
23 
24 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
25 #include "llvm/IR/Function.h"
26 #else
27 #include "llvm/Function.h"
28 #endif
29 
30 #include "llvm/Support/CommandLine.h"
31 
32 #include <unistd.h>
33 #include <signal.h>
34 #include <sys/time.h>
35 #include <math.h>
36 
37 
38 using namespace llvm;
39 using namespace klee;
40 
41 cl::opt<double>
42 MaxTime("max-time",
43  cl::desc("Halt execution after the specified number of seconds (0=off)"),
44  cl::init(0));
45 
47 
48 class HaltTimer : public Executor::Timer {
50 
51 public:
52  HaltTimer(Executor *_executor) : executor(_executor) {}
54 
55  void run() {
56  llvm::errs() << "KLEE: HaltTimer invoked\n";
57  executor->setHaltExecution(true);
58  }
59 };
60 
62 
63 static const double kSecondsPerTick = .1;
64 static volatile unsigned timerTicks = 0;
65 
66 // XXX hack
67 extern "C" unsigned dumpStates, dumpPTree;
68 unsigned dumpStates = 0, dumpPTree = 0;
69 
70 static void onAlarm(int) {
71  ++timerTicks;
72 }
73 
74 // oooogalay
75 static void setupHandler() {
76  struct itimerval t;
77  struct timeval tv;
78 
79  tv.tv_sec = (long) kSecondsPerTick;
80  tv.tv_usec = (long) (fmod(kSecondsPerTick, 1.)*1000000);
81 
82  t.it_interval = t.it_value = tv;
83 
84  ::setitimer(ITIMER_REAL, &t, 0);
85  ::signal(SIGALRM, onAlarm);
86 }
87 
88 void Executor::initTimers() {
89  static bool first = true;
90 
91  if (first) {
92  first = false;
93  setupHandler();
94  }
95 
96  if (MaxTime) {
97  addTimer(new HaltTimer(this), MaxTime.getValue());
98  }
99 }
100 
102 
103 Executor::Timer::Timer() {}
104 
105 Executor::Timer::~Timer() {}
106 
107 void Executor::addTimer(Timer *timer, double rate) {
108  timers.push_back(new TimerInfo(timer, rate));
109 }
110 
111 void Executor::processTimers(ExecutionState *current,
112  double maxInstTime) {
113  static unsigned callsWithoutCheck = 0;
114  unsigned ticks = timerTicks;
115 
116  if (!ticks && ++callsWithoutCheck > 1000) {
117  setupHandler();
118  ticks = 1;
119  }
120 
121  if (ticks || dumpPTree || dumpStates) {
122  if (dumpPTree) {
123  char name[32];
124  sprintf(name, "ptree%08d.dot", (int) stats::instructions);
125  llvm::raw_ostream *os = interpreterHandler->openOutputFile(name);
126  if (os) {
127  processTree->dump(*os);
128  delete os;
129  }
130 
131  dumpPTree = 0;
132  }
133 
134  if (dumpStates) {
135  llvm::raw_ostream *os = interpreterHandler->openOutputFile("states.txt");
136 
137  if (os) {
138  for (std::set<ExecutionState*>::const_iterator it = states.begin(),
139  ie = states.end(); it != ie; ++it) {
140  ExecutionState *es = *it;
141  *os << "(" << es << ",";
142  *os << "[";
143  ExecutionState::stack_ty::iterator next = es->stack.begin();
144  ++next;
145  for (ExecutionState::stack_ty::iterator sfIt = es->stack.begin(),
146  sf_ie = es->stack.end(); sfIt != sf_ie; ++sfIt) {
147  *os << "('" << sfIt->kf->function->getName().str() << "',";
148  if (next == es->stack.end()) {
149  *os << es->prevPC->info->line << "), ";
150  } else {
151  *os << next->caller->info->line << "), ";
152  ++next;
153  }
154  }
155  *os << "], ";
156 
157  StackFrame &sf = es->stack.back();
158  uint64_t md2u = computeMinDistToUncovered(es->pc,
161  es->pc->info->id);
162  uint64_t cpicnt = sf.callPathNode->statistics.getValue(stats::instructions);
163 
164  *os << "{";
165  *os << "'depth' : " << es->depth << ", ";
166  *os << "'weight' : " << es->weight << ", ";
167  *os << "'queryCost' : " << es->queryCost << ", ";
168  *os << "'coveredNew' : " << es->coveredNew << ", ";
169  *os << "'instsSinceCovNew' : " << es->instsSinceCovNew << ", ";
170  *os << "'md2u' : " << md2u << ", ";
171  *os << "'icnt' : " << icnt << ", ";
172  *os << "'CPicnt' : " << cpicnt << ", ";
173  *os << "}";
174  *os << ")\n";
175  }
176 
177  delete os;
178  }
179 
180  dumpStates = 0;
181  }
182 
183  if (maxInstTime>0 && current && !removedStates.count(current)) {
184  if (timerTicks*kSecondsPerTick > maxInstTime) {
185  klee_warning("max-instruction-time exceeded: %.2fs",
187  terminateStateEarly(*current, "max-instruction-time exceeded");
188  }
189  }
190 
191  if (!timers.empty()) {
192  double time = util::getWallTime();
193 
194  for (std::vector<TimerInfo*>::iterator it = timers.begin(),
195  ie = timers.end(); it != ie; ++it) {
196  TimerInfo *ti = *it;
197 
198  if (time >= ti->nextFireTime) {
199  ti->timer->run();
200  ti->nextFireTime = time + ti->rate;
201  }
202  }
203  }
204 
205  timerTicks = 0;
206  callsWithoutCheck = 0;
207  }
208 }
209 
uint64_t getValue(const Statistic &s) const
Definition: Statistics.h:120
double rate
Approximate delay per timer firing.
StatisticManager * theStatisticManager
Definition: Statistics.cpp:57
void klee_warning(char *name)
Definition: klee-replay.c:390
static void setupHandler()
static volatile unsigned timerTicks
void run()
The event callback.
double getWallTime()
Definition: Time.cpp:24
CallPathNode * callPathNode
double nextFireTime
Wall time for next firing.
unsigned id
Definition: Statistic.h:33
uint64_t getIndexedValue(const Statistic &s, unsigned index) const
Definition: Statistics.h:142
static void onAlarm(int)
StatisticRecord statistics
unsigned dumpPTree
HaltTimer(Executor *_executor)
uint64_t computeMinDistToUncovered(const KInstruction *ki, uint64_t minDistAtRA)
unsigned dumpStates
static const double kSecondsPerTick
cl::opt< double > MaxTime("max-time", cl::desc("Halt execution after the specified number of seconds (0=off)"), cl::init(0))
virtual void run()=0
The event callback.
Executor * executor
Statistic instructions
unsigned minDistToUncoveredOnReturn
Statistic states