 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
41.9% |
26 / 62 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
54.8% |
34 / 62 |
| |
|
Line Coverage: |
50.0% |
44 / 88 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "Common.h"
4 :
5 : #include "CoreStats.h"
6 : #include "Executor.h"
7 : #include "PTree.h"
8 : #include "StatsTracker.h"
9 :
10 : #include "klee/ExecutionState.h"
11 : #include "klee/Internal/Module/InstructionInfoTable.h"
12 : #include "klee/Internal/Module/KInstruction.h"
13 : #include "klee/Internal/Module/KModule.h"
14 : #include "klee/Internal/System/Time.h"
15 :
16 : #include "llvm/Function.h"
17 : #include "llvm/Support/CommandLine.h"
18 :
19 : #include <unistd.h>
20 : #include <signal.h>
21 : #include <sys/time.h>
22 : #include <math.h>
23 :
24 : #include "klee/Internal/FIXME/sugar.h"
25 :
26 : using namespace llvm;
27 : using namespace klee;
28 :
29 : cl::opt<double>
30 103: MaxTime("max-time",
31 : cl::desc("Halt execution after the specified number of seconds (0=off)"),
32 103: cl::init(0));
33 :
34 : ///
35 :
36 : class HaltTimer : public Executor::Timer {
37 : Executor *executor;
38 :
39 : public:
40 1: HaltTimer(Executor *_executor) : executor(_executor) {}
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
41 0: ~HaltTimer() {}
42 :
43 0: void run() {
44 : llvm::cerr << "KLEE: HaltTimer invoked\n";
45 0: executor->setHaltExecution(true);
46 0: }
47 : };
48 :
49 : ///
50 :
51 : static const double kSecondsPerTick = .1;
52 : static volatile unsigned timerTicks = 0;
53 :
54 : // XXX hack
55 : extern "C" unsigned dumpStates, dumpPTree;
56 : unsigned dumpStates = 0, dumpPTree = 0;
57 :
58 161: static void onAlarm(int) {
59 161: ++timerTicks;
60 161: }
61 :
62 : // oooogalay
63 10443: static void setupHandler() {
64 : struct itimerval t;
65 : struct timeval tv;
66 :
67 10443: tv.tv_sec = (long) kSecondsPerTick;
68 10443: tv.tv_usec = (long) (fmod(kSecondsPerTick, 1.)*1000000);
69 :
70 10443: t.it_interval = t.it_value = tv;
71 :
72 10443: ::setitimer(ITIMER_REAL, &t, 0);
73 10443: ::signal(SIGALRM, onAlarm);
74 10443: }
75 :
76 103: void Executor::initTimers() {
77 : static bool first = true;
78 :
103: branch 0 taken
0: branch 1 not taken
79 103: if (first) {
80 103: first = false;
81 103: setupHandler();
82 : }
83 :
1: branch 0 taken
102: branch 1 taken
84 103: if (MaxTime) {
85 2: addTimer(new HaltTimer(this), MaxTime);
86 : }
87 103: }
88 :
89 : ///
90 :
91 207: Executor::Timer::Timer() {}
92 :
0: branch 0 not taken
0: branch 1 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 6 not taken
0: branch 7 not taken
93 0: Executor::Timer::~Timer() {}
94 :
95 : class Executor::TimerInfo {
96 : public:
97 : Timer *timer;
98 :
99 : /// Approximate delay per timer firing.
100 : double rate;
101 : /// Wall time for next firing.
102 : double nextFireTime;
103 :
104 : public:
105 : TimerInfo(Timer *_timer, double _rate)
106 : : timer(_timer),
107 : rate(_rate),
108 207: nextFireTime(util::getWallTime() + rate) {}
109 : ~TimerInfo() { delete timer; }
110 : };
111 :
112 207: void Executor::addTimer(Timer *timer, double rate) {
113 414: timers.push_back(new TimerInfo(timer, rate));
114 207: }
115 :
116 : void Executor::processTimers(ExecutionState *current,
117 10391932: double maxInstTime) {
118 : static unsigned callsWithoutCheck = 0;
119 10391932: unsigned ticks = timerTicks;
120 :
10391803: branch 0 taken
129: branch 1 taken
10340: branch 2 taken
10381463: branch 3 taken
10340: branch 4 taken
10381592: branch 5 taken
121 10391932: if (!ticks && ++callsWithoutCheck > 1000) {
122 10340: setupHandler();
123 10340: ticks = 1;
124 : }
125 :
10381463: branch 0 taken
10469: branch 1 taken
10381463: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
10381463: branch 5 taken
126 10391932: if (ticks || dumpPTree || dumpStates) {
0: branch 0 not taken
10469: branch 1 taken
127 10469: if (dumpPTree) {
128 : char name[32];
129 0: sprintf(name, "ptree%08d.dot", (int) stats::instructions);
130 0: std::ostream *os = interpreterHandler->openOutputFile(name);
0: branch 0 not taken
0: branch 1 not taken
131 0: if (os) {
132 0: processTree->dump(*os);
0: branch 0 not taken
0: branch 1 not taken
133 0: delete os;
134 : }
135 :
136 0: dumpPTree = 0;
137 : }
138 :
0: branch 0 not taken
10469: branch 1 taken
139 10469: if (dumpStates) {
140 0: std::ostream *os = interpreterHandler->openOutputFile("states.txt");
141 :
0: branch 0 not taken
0: branch 1 not taken
142 0: if (os) {
0: branch 0 not taken
0: branch 1 not taken
143 0: foreach(it, states.begin(), states.end()) {
144 0: ExecutionState *es = *it;
145 0: *os << "(" << es << ",";
146 0: *os << "[";
147 0: let(next, es->stack.begin());
148 : ++next;
0: branch 0 not taken
0: branch 1 not taken
149 0: foreach(sfIt, es->stack.begin(), es->stack.end()) {
150 0: *os << "('" << sfIt->kf->function->getName() << "',";
0: branch 0 not taken
0: branch 1 not taken
151 0: if (next == es->stack.end()) {
152 0: *os << es->prevPC->info->line << "), ";
153 : } else {
154 0: *os << next->caller->info->line << "), ";
155 : ++next;
156 : }
157 : }
158 0: *os << "], ";
159 :
160 0: StackFrame &sf = es->stack.back();
161 : uint64_t md2u = computeMinDistToUncovered(es->pc,
162 0: sf.minDistToUncoveredOnReturn);
163 : uint64_t icnt = theStatisticManager->getIndexedValue(stats::instructions,
164 0: es->pc->info->id);
165 0: uint64_t cpicnt = sf.callPathNode->statistics.getValue(stats::instructions);
166 :
167 0: *os << "{";
168 0: *os << "'depth' : " << es->depth << ", ";
169 0: *os << "'weight' : " << es->weight << ", ";
170 0: *os << "'queryCost' : " << es->queryCost << ", ";
171 0: *os << "'coveredNew' : " << es->coveredNew << ", ";
172 0: *os << "'instsSinceCovNew' : " << es->instsSinceCovNew << ", ";
173 0: *os << "'md2u' : " << md2u << ", ";
174 0: *os << "'icnt' : " << icnt << ", ";
175 0: *os << "'CPicnt' : " << cpicnt << ", ";
176 0: *os << "}";
177 0: *os << ")\n";
178 : }
179 :
0: branch 0 not taken
0: branch 1 not taken
180 0: delete os;
181 : }
182 :
183 0: dumpStates = 0;
184 : }
185 :
0: branch 0 not taken
10469: branch 1 taken
10469: branch 2 taken
10469: branch 3 taken
0: branch 4 not taken
10469: branch 5 taken
186 10469: if (maxInstTime>0 && current && !removedStates.count(current)) {
0: branch 0 not taken
0: branch 1 not taken
187 0: if (timerTicks*kSecondsPerTick > maxInstTime) {
188 : klee_warning("max-instruction-time exceeded: %.2fs",
189 0: timerTicks*kSecondsPerTick);
190 0: terminateStateEarly(*current, "max-instruction-time exceeded");
191 : }
192 : }
193 :
10469: branch 0 taken
0: branch 1 not taken
194 20938: if (!timers.empty()) {
195 10469: double time = util::getWallTime();
196 :
21049: branch 0 taken
10469: branch 1 taken
197 52456: foreach(it, timers.begin(), timers.end()) {
198 21049: TimerInfo *ti = *it;
199 :
35: branch 0 taken
21014: branch 1 taken
200 21049: if (time >= ti->nextFireTime) {
201 35: ti->timer->run();
202 35: ti->nextFireTime = time + ti->rate;
203 : }
204 : }
205 : }
206 :
207 10469: timerTicks = 0;
208 10469: callsWithoutCheck = 0;
209 : }
103: branch 0 taken
0: branch 1 not taken
103: branch 2 taken
0: branch 3 not taken
210 10392241: }
211 :
Generated: 2009-05-17 22:47 by zcov