 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
59.0% |
701 / 1188 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
74.6% |
886 / 1188 |
| |
|
Line Coverage: |
76.1% |
1264 / 1662 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "Common.h"
4 :
5 : #include "Executor.h"
6 :
7 : #include "CoreStats.h"
8 : #include "ExternalDispatcher.h"
9 : #include "ImpliedValue.h"
10 : #include "MemoryManager.h"
11 : #include "PTree.h"
12 : #include "Searcher.h"
13 : #include "SeedInfo.h"
14 : #include "SpecialFunctionHandler.h"
15 : #include "StatsTracker.h"
16 : #include "TimingSolver.h"
17 : #include "UserSearcher.h"
18 : #include "../Solver/SolverStats.h"
19 :
20 : #include "klee/ExecutionState.h"
21 : #include "klee/Expr.h"
22 : #include "klee/Interpreter.h"
23 : #include "klee/Machine.h"
24 : #include "klee/Memory.h"
25 : #include "klee/TimerStatIncrementer.h"
26 : #include "klee/util/Assignment.h"
27 : #include "klee/util/ExprPPrinter.h"
28 : #include "klee/util/ExprUtil.h"
29 : #include "klee/Internal/ADT/BOut.h"
30 : #include "klee/Internal/ADT/RNG.h"
31 : #include "klee/Internal/Module/Cell.h"
32 : #include "klee/Internal/Module/InstructionInfoTable.h"
33 : #include "klee/Internal/Module/KInstruction.h"
34 : #include "klee/Internal/Module/KModule.h"
35 : #include "klee/Internal/Support/FloatEvaluation.h"
36 : #include "klee/Internal/System/Time.h"
37 :
38 : #include "llvm/Attributes.h"
39 : #include "llvm/BasicBlock.h"
40 : #include "llvm/Constants.h"
41 : #include "llvm/Function.h"
42 : #include "llvm/Instructions.h"
43 : #include "llvm/IntrinsicInst.h"
44 : #include "llvm/Module.h"
45 : #include "llvm/Support/CallSite.h"
46 : #include "llvm/Support/CommandLine.h"
47 : #include "llvm/Support/GetElementPtrTypeIterator.h"
48 : #include "llvm/System/Process.h"
49 : #include "llvm/Target/TargetData.h"
50 :
51 : #include <cassert>
52 : #include <algorithm>
53 : #include <iostream>
54 : #include <iomanip>
55 : #include <fstream>
56 : #include <sstream>
57 : #include <vector>
58 : #include <string>
59 :
60 : #include <sys/mman.h>
61 :
62 : #include <errno.h>
63 : #include <cxxabi.h>
64 :
65 : #include "klee/Internal/FIXME/sugar.h"
66 :
67 : using namespace llvm;
68 : using namespace klee;
69 :
70 : // omg really hard to share cl opts across files ...
71 : bool WriteTraces = false;
72 :
73 : namespace {
74 : cl::opt<bool>
75 103: DumpStatesOnHalt("dump-states-on-halt",
76 206: cl::init(true));
77 :
78 : cl::opt<bool>
79 103: NoPreferCex("no-prefer-cex",
80 206: cl::init(false));
81 :
82 : cl::opt<bool>
83 103: UseAsmAddresses("use-asm-addresses",
84 206: cl::init(false));
85 :
86 : cl::opt<bool>
87 103: RandomizeFork("randomize-fork",
88 103: cl::init(false));
89 :
90 : cl::opt<bool>
91 103: AllowExternalSymCalls("allow-external-sym-calls",
92 103: cl::init(false));
93 :
94 : cl::opt<bool>
95 103: DebugPrintInstructions("debug-print-instructions",
96 : cl::desc("Print instructions during execution."));
97 :
98 : cl::opt<bool>
99 103: DebugCheckForImpliedValues("debug-check-for-implied-values");
100 :
101 :
102 : cl::opt<bool>
103 103: SimplifySymIndices("simplify-sym-indices",
104 206: cl::init(false));
105 :
106 : cl::opt<unsigned>
107 103: MaxSymArraySize("max-sym-array-size",
108 103: cl::init(0));
109 :
110 : cl::opt<bool>
111 103: DebugValidateSolver("debug-validate-solver",
112 103: cl::init(false));
113 :
114 : cl::opt<bool>
115 103: SuppressExternalWarnings("suppress-external-warnings");
116 :
117 : cl::opt<bool>
118 103: AllExternalWarnings("all-external-warnings");
119 :
120 : cl::opt<bool>
121 103: OnlyOutputStatesCoveringNew("only-output-states-covering-new",
122 103: cl::init(false));
123 :
124 : cl::opt<bool>
125 103: AlwaysOutputSeeds("always-output-seeds",
126 206: cl::init(true));
127 :
128 : cl::opt<bool>
129 103: UseFastCexSolver("use-fast-cex-solver",
130 206: cl::init(false));
131 :
132 : cl::opt<bool>
133 103: UseIndependentSolver("use-independent-solver",
134 : cl::init(true),
135 103: cl::desc("Use constraint independence"));
136 :
137 : cl::opt<bool>
138 103: EmitAllErrors("emit-all-errors",
139 : cl::init(false),
140 : cl::desc("Generate tests cases for all errors "
141 103: "(default=one per (error,instruction) pair)"));
142 :
143 : cl::opt<bool>
144 103: UseCexCache("use-cex-cache",
145 : cl::init(true),
146 103: cl::desc("Use counterexample caching"));
147 :
148 : cl::opt<bool>
149 103: UseQueryLog("use-query-log",
150 206: cl::init(false));
151 :
152 : cl::opt<bool>
153 103: UseQueryPCLog("use-query-pc-log",
154 103: cl::init(false));
155 :
156 : cl::opt<bool>
157 103: UseSTPQueryLog("use-stp-query-log",
158 206: cl::init(false));
159 :
160 : cl::opt<bool>
161 103: UseSTPQueryPCLog("use-stp-query-pc-log",
162 206: cl::init(false));
163 :
164 : cl::opt<bool>
165 103: NoExternals("no-externals",
166 : cl::desc("Do not allow external functin calls"));
167 :
168 : cl::opt<bool>
169 103: UseCache("use-cache",
170 : cl::init(true),
171 103: cl::desc("Use validity caching"));
172 :
173 : cl::opt<bool>
174 103: OnlyReplaySeeds("only-replay-seeds",
175 : cl::desc("Discard states that do not have a seed."));
176 :
177 : cl::opt<bool>
178 103: OnlySeed("only-seed",
179 : cl::desc("Stop execution after seeding is done without doing regular search."));
180 :
181 : cl::opt<bool>
182 103: AllowSeedExtension("allow-seed-extension",
183 : cl::desc("Allow extra (unbound) values to become symbolic during seeding."));
184 :
185 : cl::opt<bool>
186 103: ZeroSeedExtension("zero-seed-extension");
187 :
188 : cl::opt<bool>
189 103: AllowSeedTruncation("allow-seed-truncation",
190 : cl::desc("Allow smaller buffers than in seeds."));
191 :
192 : cl::opt<bool>
193 103: NamedSeedMatching("named-seed-matching",
194 : cl::desc("Use names to match symbolic objects to inputs."));
195 :
196 : cl::opt<double>
197 206: MaxStaticForkPct("max-static-fork-pct", cl::init(1.));
198 : cl::opt<double>
199 206: MaxStaticSolvePct("max-static-solve-pct", cl::init(1.));
200 : cl::opt<double>
201 206: MaxStaticCPForkPct("max-static-cpfork-pct", cl::init(1.));
202 : cl::opt<double>
203 206: MaxStaticCPSolvePct("max-static-cpsolve-pct", cl::init(1.));
204 :
205 : cl::opt<double>
206 103: MaxInstructionTime("max-instruction-time",
207 : cl::desc("Only allow a single instruction to take this much time (default=0 (off))"),
208 103: cl::init(0));
209 :
210 : cl::opt<double>
211 103: SeedTime("seed-time",
212 : cl::desc("Amount of time to dedicate to seeds, before normal search (default=0 (off))"),
213 103: cl::init(0));
214 :
215 : cl::opt<double>
216 103: MaxSTPTime("max-stp-time",
217 : cl::desc("Maximum amount of time for a single query (default=120s)"),
218 103: cl::init(120.0));
219 :
220 : cl::opt<unsigned int>
221 103: StopAfterNInstructions("stop-after-n-instructions",
222 : cl::desc("Stop execution after specified number of instructions (0=off)"),
223 103: cl::init(0));
224 :
225 : cl::opt<unsigned>
226 103: MaxForks("max-forks",
227 : cl::desc("Only fork this many times (-1=off)"),
228 103: cl::init(~0u));
229 :
230 : cl::opt<unsigned>
231 103: MaxDepth("max-depth",
232 : cl::desc("Only allow this many symbolic branches (0=off)"),
233 103: cl::init(0));
234 :
235 : cl::opt<unsigned>
236 103: MaxMemory("max-memory",
237 : cl::desc("Refuse to fork when more above this about of memory (in MB, 0=off)"),
238 103: cl::init(0));
239 :
240 : cl::opt<bool>
241 103: MaxMemoryInhibit("max-memory-inhibit",
242 : cl::desc("Inhibit forking at memory cap (vs. random terminat)"),
243 103: cl::init(true));
244 :
245 : // use 'external storage' because also needed by tools/klee/main.cpp
246 : cl::opt<bool, true>
247 103: WriteTracesProxy("write-traces",
248 : cl::desc("Write .trace file for each terminated state"),
249 : cl::location(WriteTraces),
250 103: cl::init(false));
251 :
252 : cl::opt<bool>
253 103: UseForkedSTP("use-forked-stp",
254 : cl::desc("Run STP in forked process"));
255 : }
256 :
257 :
258 : static void *theMMap = 0;
259 : static unsigned theMMapSize = 0;
260 :
261 : namespace klee {
262 103: RNG theRNG;
263 : }
264 :
265 : Solver *constructSolverChain(STPSolver *stpSolver,
266 : std::string queryLogPath,
267 : std::string stpQueryLogPath,
268 : std::string queryPCLogPath,
269 103: std::string stpQueryPCLogPath) {
270 103: Solver *solver = stpSolver;
271 :
0: branch 0 not taken
103: branch 1 taken
272 103: if (UseSTPQueryLog)
273 : solver = createLoggingSolver(solver,
274 0: stpQueryLogPath);
275 :
0: branch 0 not taken
103: branch 1 taken
276 103: if (UseSTPQueryPCLog)
277 : solver = createPCLoggingSolver(solver,
278 0: stpQueryLogPath);
279 :
1: branch 0 taken
102: branch 1 taken
280 103: if (UseFastCexSolver)
281 1: solver = createFastCexSolver(solver);
282 :
103: branch 0 taken
0: branch 1 not taken
283 103: if (UseCexCache)
284 103: solver = createCexCachingSolver(solver);
285 :
103: branch 0 taken
0: branch 1 not taken
286 103: if (UseCache)
287 103: solver = createCachingSolver(solver);
288 :
103: branch 0 taken
0: branch 1 not taken
289 103: if (UseIndependentSolver)
290 103: solver = createIndependentSolver(solver);
291 :
1: branch 0 taken
102: branch 1 taken
292 103: if (DebugValidateSolver)
293 1: solver = createValidatingSolver(solver, stpSolver);
294 :
2: branch 0 taken
101: branch 1 taken
295 103: if (UseQueryLog)
296 : solver = createLoggingSolver(solver,
297 2: queryLogPath);
298 :
1: branch 0 taken
102: branch 1 taken
299 103: if (UseQueryPCLog)
300 : solver = createPCLoggingSolver(solver,
301 1: queryPCLogPath);
302 :
303 103: return solver;
304 : }
305 :
306 : Executor::Executor(const InterpreterOptions &opts,
307 103: InterpreterHandler *ih)
308 : : Interpreter(opts),
309 : kmodule(0),
310 : interpreterHandler(ih),
311 : searcher(0),
312 : externalDispatcher(new ExternalDispatcher()),
313 : statsTracker(0),
314 : pathWriter(0),
315 : symPathWriter(0),
316 : specialFunctionHandler(0),
317 : processTree(0),
318 : replayOut(0),
319 : replayPath(0),
320 : usingSeeds(0),
321 : atMemoryLimit(false),
322 : inhibitForking(false),
323 : haltExecution(false),
324 : ivcEnabled(false),
325 1133: stpTimeout(std::min(MaxSTPTime,MaxInstructionTime)) {
326 103: STPSolver *stpSolver = new STPSolver(UseForkedSTP);
327 : Solver *solver =
328 : constructSolverChain(stpSolver,
329 : interpreterHandler->getOutputFilename("queries.qlog"),
330 : interpreterHandler->getOutputFilename("stp-queries.qlog"),
331 : interpreterHandler->getOutputFilename("queries.pc"),
332 824: interpreterHandler->getOutputFilename("stp-queries.pc"));
333 :
334 206: this->solver = new TimingSolver(solver, stpSolver);
335 :
336 206: memory = new MemoryManager();
337 103: }
338 :
339 :
340 : const Module *Executor::setModule(llvm::Module *module,
341 : const ModuleOptions &opts,
342 103: const std::vector<std::string> &excludeCovFiles) {
0: branch 0 not taken
103: branch 1 taken
343 103: assert(!kmodule && module && "can only register one module"); // XXX gross
344 :
345 103: kmodule = new KModule(module);
346 :
347 103: specialFunctionHandler = new SpecialFunctionHandler(*this);
348 :
349 103: specialFunctionHandler->prepare();
350 103: kmodule->prepare(opts, interpreterHandler);
351 103: specialFunctionHandler->bind();
352 :
103: branch 1 taken
0: branch 2 not taken
353 103: if (StatsTracker::useStatistics()) {
354 : statsTracker = new StatsTracker(*this,
355 : interpreterHandler->getOutputFilename("assembly.ll"),
356 : excludeCovFiles,
357 206: userSearcherRequiresMD2U());
358 : }
359 :
360 103: return module;
361 : }
362 :
363 103: Executor::~Executor() {
103: branch 0 taken
0: branch 1 not taken
103: branch 4 taken
103: branch 5 taken
0: branch 8 not taken
0: branch 9 not taken
364 103: delete memory;
103: branch 0 taken
0: branch 1 not taken
103: branch 4 taken
103: branch 5 taken
0: branch 8 not taken
0: branch 9 not taken
365 103: delete externalDispatcher;
0: branch 0 not taken
103: branch 1 taken
103: branch 2 taken
103: branch 3 taken
103: branch 4 taken
103: branch 5 taken
366 103: if (processTree)
0: branch 0 not taken
0: branch 1 not taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 8 not taken
0: branch 9 not taken
367 0: delete processTree;
103: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
368 103: if (specialFunctionHandler)
103: branch 0 taken
0: branch 1 not taken
103: branch 3 taken
103: branch 4 taken
0: branch 6 not taken
0: branch 7 not taken
369 206: delete specialFunctionHandler;
103: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
370 103: if (statsTracker)
103: branch 0 taken
0: branch 1 not taken
103: branch 4 taken
103: branch 5 taken
0: branch 8 not taken
0: branch 9 not taken
371 103: delete statsTracker;
103: branch 0 taken
0: branch 1 not taken
103: branch 4 taken
103: branch 5 taken
0: branch 8 not taken
0: branch 9 not taken
372 103: delete solver;
103: branch 0 taken
0: branch 1 not taken
103: branch 4 taken
103: branch 5 taken
0: branch 8 not taken
0: branch 9 not taken
373 103: delete kmodule;
103: branch 1 taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
0: branch 9 not taken
0: branch 10 not taken
374 927: }
375 :
376 : /***/
377 :
378 : void Executor::initializeGlobalObject(ExecutionState &state, ObjectState *os,
379 : Constant *c,
380 587651: unsigned offset) {
381 587651: TargetData *targetData = kmodule->targetData;
0: branch 0 not taken
587651: branch 1 taken
382 587651: if (ConstantVector *cp = dyn_cast<ConstantVector>(c)) {
383 : unsigned elementSize =
384 0: targetData->getTypeStoreSize(cp->getType()->getElementType());
0: branch 0 not taken
0: branch 1 not taken
385 0: for (unsigned i=0, e=cp->getNumOperands(); i != e; ++i)
386 : initializeGlobalObject(state, os, cp->getOperand(i),
387 0: offset + i*elementSize);
62: branch 0 taken
587589: branch 1 taken
388 587651: } else if (isa<ConstantAggregateZero>(c)) {
389 124: unsigned i, size = targetData->getTypeStoreSize(c->getType());
12114: branch 0 taken
62: branch 1 taken
390 12176: for (i=0; i<size; i++)
391 12114: os->write8(offset+i, (uint8_t) 0);
4639: branch 0 taken
582950: branch 1 taken
392 587589: } else if (ConstantArray *ca = dyn_cast<ConstantArray>(c)) {
393 : unsigned elementSize =
394 9278: targetData->getTypeStoreSize(ca->getType()->getElementType());
542447: branch 0 taken
4639: branch 1 taken
395 551725: for (unsigned i=0, e=ca->getNumOperands(); i != e; ++i)
396 : initializeGlobalObject(state, os, ca->getOperand(i),
397 542447: offset + i*elementSize);
3923: branch 0 taken
579027: branch 1 taken
398 582950: } else if (ConstantStruct *cs = dyn_cast<ConstantStruct>(c)) {
399 : const StructLayout *sl =
400 3923: targetData->getStructLayout(cast<StructType>(cs->getType()));
37011: branch 0 taken
3923: branch 1 taken
401 44857: for (unsigned i=0, e=cs->getNumOperands(); i != e; ++i)
402 : initializeGlobalObject(state, os, cs->getOperand(i),
403 37011: offset + sl->getElementOffset(i));
404 : } else {
405 579027: MemoryObject *referent = 0;
406 :
407 579027: os->write(offset, evalConstant(c, &referent));
408 :
409 : #ifdef KLEE_TRACK_REFERENTS
410 : if (referent)
411 : writeReferent(state, os, ConstantExpr::create(offset, Expr::Int32),
412 : referent);
413 : #endif
414 : }
415 587651: }
416 :
417 : MemoryObject * Executor::addExternalObject(ExecutionState &state,
418 721: void *addr, unsigned size, MemoryObject *referent, bool isReadOnly) {
419 721: MemoryObject *mo = memory->allocateFixed((uint64_t) (unsigned long) addr, size, 0);
420 721: ObjectState *os = bindObjectInState(state, mo, false);
397168: branch 0 taken
721: branch 1 taken
421 397889: for(unsigned i = 0; i < size; i++)
422 397168: os->write8(i, ((uint8_t*)addr)[i]);
618: branch 0 taken
103: branch 1 taken
423 721: if(isReadOnly)
424 : os->setReadOnly(true);
425 :
426 : #ifdef KLEE_TRACK_REFERENTS
427 : if (referent)
428 : writeReferent(state, os, ConstantExpr::create(0, Expr::Int32), referent);
429 : #endif
430 721: return mo;
431 : }
432 :
433 103: void Executor::initializeGlobals(ExecutionState &state) {
434 103: Module *m = kmodule->module;
435 :
3: branch 0 taken
100: branch 1 taken
436 103: if (m->getModuleInlineAsm() != "")
437 3: klee_warning("executable has module level assembly (ignoring)");
438 :
439 : assert(m->lib_begin() == m->lib_end() &&
0: branch 0 not taken
103: branch 1 taken
440 103: "XXX do not support dependent libraries");
441 :
442 : // represent function globals using the address of the actual llvm function
443 : // object. given that we use malloc to allocate memory in states this also
444 : // ensures that we won't conflict. we don't need to allocate a memory object
445 : // since reading/writing via a function pointer is unsupported anyway.
1088: branch 2 taken
103: branch 3 taken
446 2279: foreach(i, m->begin(), m->end()) {
447 1088: Function *f = i;
448 : ref<Expr> addr(0);
449 :
450 : // If the symbol has external weak linkage then it is implicitly
451 : // not defined in this module; if it isn't resolvable then it
452 : // should be null.
1: branch 0 taken
1087: branch 1 taken
1: branch 4 taken
0: branch 5 not taken
1: branch 6 taken
1087: branch 7 taken
1: branch 9 taken
1087: branch 10 taken
453 2176: if (f->hasExternalWeakLinkage() &&
454 : !externalDispatcher->resolveSymbol(f->getName())) {
455 1: addr = Expr::createPointer(0);
456 : } else {
457 1087: addr = Expr::createPointer((unsigned long) (void*) f);
458 1087: legalFunctions.insert(f);
459 : }
460 :
461 3264: globalAddresses.insert(std::make_pair(f, addr));
462 : }
463 :
464 : #ifndef WINDOWS
465 : #ifndef DARWIN
466 : /* From /usr/include/errno.h: it [errno] is a per-thread variable. */
467 103: int *errno_addr = __errno_location();
468 103: addExternalObject(state, (void *)errno_addr, sizeof *errno_addr, 0, false);
469 :
470 : /* from /usr/include/ctype.h:
471 : These point into arrays of 384, so they can be indexed by any `unsigned
472 : char' value [0,255]; by EOF (-1); or by any `signed char' value
473 : [-128,-1). ISO C requires that the ctype functions work for `unsigned */
474 : // XXX: there is some confusion over whether starts at *addr or *addr-128
475 103: let(addr, __ctype_b_loc());
476 103: MemoryObject *ref = 0;
477 103: ref = addExternalObject(state, (void *)(*addr-128), 384 * sizeof **addr, 0, true);
478 103: addExternalObject(state, addr, 4, ref, true);
479 :
480 103: let(lower_addr, __ctype_tolower_loc());
481 103: ref = addExternalObject(state, (void *)(*lower_addr-128), 384 * sizeof **lower_addr, 0, true);
482 103: addExternalObject(state, lower_addr, 4, ref, true);
483 :
484 103: let(upper_addr, __ctype_toupper_loc());
485 103: ref = addExternalObject(state, (void *)(*upper_addr-128), 384 * sizeof **upper_addr, 0, true);
486 103: addExternalObject(state, upper_addr, 4, ref, true);
487 : #endif
488 : #endif
489 :
490 : // allocate and initialize globals, done in two passes since we may
491 : // need address of a global in order to initialize some other one.
492 :
493 : // allocate memory objects for all globals
8205: branch 1 taken
103: branch 2 taken
494 16616: for (Module::const_global_iterator i = m->global_begin(),
495 103: e = m->global_end();
496 : i != e; ++i) {
12: branch 1 taken
8193: branch 2 taken
497 8205: if (i->isDeclaration()) {
498 : // XXX: this is not done. It does not handle:
499 : // extern T x[];
500 : // declarations since we are not given the size. I think we have
501 : // to revert back to the fucking nm/readelf hack to do so. DWD?
502 :
503 36: const Type *ty = i->getType()->getElementType();
504 12: const std::string &name = i->getName();
505 12: uint64_t size = kmodule->targetData->getTypeStoreSize(ty);
506 :
507 : // XXX - DWD - hardcode some things until we decide how to fix.
508 : #ifndef WINDOWS
1: branch 0 taken
11: branch 1 taken
509 12: if (name == "_ZTVN10__cxxabiv117__class_type_infoE") {
510 1: size = 0x2C;
1: branch 0 taken
10: branch 1 taken
511 11: } else if (name == "_ZTVN10__cxxabiv120__si_class_type_infoE") {
512 1: size = 0x2C;
0: branch 0 not taken
10: branch 1 taken
513 10: } else if (name == "_ZTVN10__cxxabiv121__vmi_class_type_infoE") {
514 0: size = 0x2C;
515 : }
516 : #endif
517 :
0: branch 0 not taken
12: branch 1 taken
518 12: if (size == 0) {
519 : llvm::cerr << "Unable to find size for global variable: " << i->getName()
520 0: << " (use will result in out of bounds access)\n";
521 : }
522 :
523 12: MemoryObject *mo = memory->allocate(size, false, true, i);
524 12: ObjectState *os = bindObjectInState(state, mo, false);
525 24: globalObjects.insert(std::make_pair(i, mo));
526 36: globalAddresses.insert(std::make_pair(i, mo->getBaseExpr()));
527 :
528 : // Program already running = object already initialized. Read
529 : // concrete value and write it to our copy.
12: branch 0 taken
0: branch 1 not taken
530 12: if (size) {
531 : void *addr;
3: branch 0 taken
9: branch 1 taken
532 12: if (name=="__dso_handle") {
533 : extern void *__dso_handle __attribute__ ((__weak__));
534 3: addr = &__dso_handle; // wtf ?
535 : } else {
536 9: addr = externalDispatcher->resolveSymbol(name);
537 : }
0: branch 0 not taken
12: branch 1 taken
538 12: if (!addr)
539 : klee_error("unable to load symbol(%s) while initializing globals.",
540 0: name.c_str());
541 :
128: branch 0 taken
12: branch 1 taken
542 140: for (unsigned offset=0; offset<mo->size; offset++)
543 128: os->write8(offset, ((unsigned char*)addr)[offset]);
544 12: }
545 : } else {
546 8193: const std::string &name = i->getName();
547 24579: const Type *ty = i->getType()->getElementType();
548 8193: uint64_t size = kmodule->targetData->getTypeStoreSize(ty);
549 8193: MemoryObject *mo = 0;
550 :
38: branch 0 taken
8155: branch 1 taken
2: branch 2 taken
36: branch 3 taken
2: branch 4 taken
8191: branch 5 taken
551 8231: if (UseAsmAddresses && name[0]=='\01') {
552 : char *end;
553 2: uint64_t address = ::strtoll(name.c_str()+1, &end, 0);
554 :
2: branch 0 taken
0: branch 1 not taken
1: branch 2 taken
1: branch 3 taken
555 2: if (end && *end == '\0') {
556 : klee_message("NOTE: allocated global at asm specified address: %#08llx"
557 : " (%llu bytes)",
558 1: address, size);
559 1: mo = memory->allocateFixed(address, size, &*i);
560 1: mo->isUserSpecified = true; // XXX hack;
561 : }
562 : }
563 :
8192: branch 0 taken
1: branch 1 taken
564 8193: if (!mo)
565 8192: mo = memory->allocate(size, false, true, &*i);
0: branch 0 not taken
8193: branch 1 taken
566 8193: assert(mo && "out of memory");
567 8193: ObjectState *os = bindObjectInState(state, mo, false);
568 16386: globalObjects.insert(std::make_pair(i, mo));
569 24579: globalAddresses.insert(std::make_pair(i, mo->getBaseExpr()));
570 :
0: branch 0 not taken
8193: branch 1 taken
571 8193: if (!i->hasInitializer())
572 0: os->initializeToRandom();
573 : }
574 : }
575 :
576 : // link aliases to their definitions (if bound)
10: branch 1 taken
103: branch 2 taken
577 226: foreach(i, m->alias_begin(), m->alias_end()) {
578 : // XXX referent is ignored here, no place to put it. grrrr.
579 :
580 : // Map the alias to its aliasee's address. This works because we have
581 : // addresses for everything, even undefined functions.
582 30: globalAddresses.insert(std::make_pair(i, evalConstant(i->getAliasee(), 0)));
583 : }
584 :
585 : // once all objects are allocated, do the actual initialization
8205: branch 1 taken
103: branch 2 taken
586 16616: for (Module::const_global_iterator i = m->global_begin(),
587 103: e = m->global_end();
588 : i != e; ++i) {
8193: branch 0 taken
12: branch 1 taken
589 8205: if (i->hasInitializer()) {
590 16386: MemoryObject *mo = globalObjects.find(i)->second;
591 8193: const ObjectState *os = state.addressSpace.findObject(mo);
0: branch 0 not taken
8193: branch 1 taken
592 8193: assert(os);
593 8193: ObjectState *wos = state.addressSpace.getWriteable(mo, os);
594 :
595 8193: initializeGlobalObject(state, wos, i->getInitializer(), 0);
596 : // if(i->isConstant()) os->setReadOnly(true);
597 : }
598 : }
599 103: }
600 :
601 : void Executor::branch(ExecutionState &state,
602 : const std::vector< ref<Expr> > &conditions,
603 76: std::vector<ExecutionState*> &result) {
604 : TimerStatIncrementer timer(stats::forkTime);
605 76: unsigned N = conditions.size();
0: branch 0 not taken
76: branch 1 taken
606 76: assert(N);
607 :
608 76: stats::forks += N-1;
609 :
610 : // XXX do proper balance or keep random?
611 76: result.push_back(&state);
128: branch 0 taken
76: branch 1 taken
612 204: for (unsigned i=1; i<N; ++i) {
613 256: ExecutionState *es = result[theRNG.getInt32() % i];
614 128: ExecutionState *ns = es->branch();
615 128: addedStates.insert(ns);
616 : result.push_back(ns);
617 128: es->ptreeNode->data = 0;
618 128: let(res, processTree->split(es->ptreeNode, ns, es));
619 128: ns->ptreeNode = res.first;
620 128: es->ptreeNode = res.second;
621 : }
622 :
623 : // If necessary redistribute seeds to match conditions, killing
624 : // states if necessary due to OnlyReplaySeeds (inefficient but
625 : // simple).
626 76: let(it, seedMap.find(&state));
0: branch 0 not taken
76: branch 1 taken
627 152: if (it != seedMap.end()) {
628 0: std::vector<SeedInfo> seeds = it->second;
629 0: seedMap.erase(it);
630 :
631 : // Assume each seed only satisfies one condition (necessarily true
632 : // when conditions are mutually exclusive and their conjunction is
633 : // a tautology).
0: branch 0 not taken
0: branch 1 not taken
634 0: foreach(siit, seeds.begin(), seeds.end()) {
635 : unsigned i;
0: branch 2 not taken
0: branch 3 not taken
636 0: for (i=0; i<N; ++i) {
637 : ref<Expr> res;
638 : bool success =
639 : solver->getValue(state, siit->assignment.evaluate(conditions[i]),
640 0: res);
0: branch 0 not taken
0: branch 1 not taken
641 0: assert(success && "FIXME: Unhandled solver failure");
0: branch 1 not taken
0: branch 2 not taken
642 0: if (res.getConstantValue())
643 0: break;
644 : }
645 :
646 : // If we didn't find a satisfying condition randomly pick one
647 : // (the seed will be patched).
0: branch 0 not taken
0: branch 1 not taken
648 0: if (i==N)
649 0: i = theRNG.getInt32() % N;
650 :
651 0: seedMap[result[i]].push_back(*siit);
652 : }
653 :
0: branch 0 not taken
0: branch 1 not taken
654 0: if (OnlyReplaySeeds) {
0: branch 0 not taken
0: branch 1 not taken
655 0: for (unsigned i=0; i<N; ++i) {
0: branch 0 not taken
0: branch 1 not taken
656 0: if (!seedMap.count(result[i])) {
657 0: terminateState(*result[i]);
658 0: result[i] = NULL;
659 : }
660 : }
661 0: }
662 : }
663 :
204: branch 0 taken
76: branch 1 taken
664 280: for (unsigned i=0; i<N; ++i)
204: branch 0 taken
0: branch 1 not taken
665 204: if (result[i])
666 280: addConstraint(*result[i], conditions[i]);
667 76: }
668 :
669 : Executor::StatePair
670 848044: Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) {
671 : Solver::Validity res;
672 848044: let(it, seedMap.find(¤t));
673 1696088: bool isSeeding = it != seedMap.end();
674 :
848035: branch 0 taken
9: branch 1 taken
1283: branch 3 taken
846752: branch 4 taken
1283: branch 5 taken
0: branch 6 not taken
1283: branch 7 taken
0: branch 8 not taken
1283: branch 9 taken
0: branch 10 not taken
0: branch 11 not taken
1283: branch 12 taken
0: branch 14 not taken
0: branch 15 not taken
0: branch 16 not taken
848044: branch 17 taken
675 853176: if (!isSeeding &&
676 : !condition.isConstant() &&
677 : (MaxStaticForkPct!=1. || MaxStaticSolvePct != 1. ||
678 : MaxStaticCPForkPct!=1. || MaxStaticCPSolvePct != 1.) &&
679 : statsTracker->elapsed() > 60.) {
680 0: StatisticManager &sm = *theStatisticManager;
681 0: CallPathNode *cpn = current.stack.back().callPathNode;
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
0: branch 7 not taken
0: branch 8 not taken
0: branch 9 not taken
0: branch 10 not taken
0: branch 11 not taken
0: branch 12 not taken
0: branch 13 not taken
0: branch 14 not taken
0: branch 15 not taken
0: branch 16 not taken
0: branch 17 not taken
0: branch 18 not taken
0: branch 19 not taken
0: branch 20 not taken
0: branch 21 not taken
682 0: if ((MaxStaticForkPct<1. &&
683 : sm.getIndexedValue(stats::forks, sm.getIndex()) >
684 : stats::forks*MaxStaticForkPct) ||
685 : (MaxStaticCPForkPct<1. &&
686 : cpn && (cpn->statistics.getValue(stats::forks) >
687 : stats::forks*MaxStaticCPForkPct)) ||
688 : (MaxStaticSolvePct<1 &&
689 : sm.getIndexedValue(stats::solverTime, sm.getIndex()) >
690 : stats::solverTime*MaxStaticSolvePct) ||
691 : (MaxStaticCPForkPct<1. &&
692 : cpn && (cpn->statistics.getValue(stats::solverTime) >
693 : stats::solverTime*MaxStaticCPSolvePct))) {
694 : ref<Expr> value;
695 0: bool success = solver->getValue(current, condition, value);
0: branch 0 not taken
0: branch 1 not taken
696 0: assert(success && "FIXME: Unhandled solver failure");
697 0: addConstraint(current, EqExpr::create(value, condition));
698 0: condition = value;
699 : }
700 : }
701 :
702 848044: double timeout = stpTimeout;
9: branch 0 taken
848035: branch 1 taken
703 848044: if (isSeeding)
704 18: timeout *= it->second.size();
705 848044: solver->setTimeout(timeout);
706 848044: bool success = solver->evaluate(current, condition, res);
707 848044: solver->setTimeout(0);
0: branch 0 not taken
848044: branch 1 taken
708 848044: if (!success) {
709 0: current.pc = current.prevPC;
710 0: terminateStateEarly(current, "query timed out");
711 0: return StatePair(0, 0);
712 : }
713 :
848035: branch 0 taken
9: branch 1 taken
714 848044: if (!isSeeding) {
6: branch 0 taken
848029: branch 1 taken
5: branch 2 taken
1: branch 3 taken
715 848035: if (replayPath && !isInternal) {
716 : assert(replayPosition<replayPath->size() &&
0: branch 0 not taken
5: branch 1 taken
717 10: "ran out of branches in replay path mode");
718 10: bool branch = (*replayPath)[replayPosition++];
719 :
1: branch 0 taken
4: branch 1 taken
720 5: if (res==Solver::True) {
0: branch 0 not taken
1: branch 1 taken
721 1: assert(branch && "hit invalid branch in replay path mode");
1: branch 0 taken
3: branch 1 taken
722 4: } else if (res==Solver::False) {
0: branch 0 not taken
1: branch 1 taken
723 1: assert(!branch && "hit invalid branch in replay path mode");
724 : } else {
725 : // add constraints
2: branch 0 taken
1: branch 1 taken
726 3: if(branch) {
727 2: res = Solver::True;
728 2: addConstraint(current, condition);
729 : } else {
730 1: res = Solver::False;
731 1: addConstraint(current, Expr::createNot(condition));
732 : }
733 : }
559: branch 0 taken
847471: branch 1 taken
734 848030: } else if (res==Solver::Unknown) {
0: branch 0 not taken
559: branch 1 taken
735 559: assert(!replayOut && "in replay mode, only one branch can be true.");
736 :
559: branch 0 taken
0: branch 1 not taken
559: branch 2 taken
0: branch 3 not taken
559: branch 4 taken
0: branch 5 not taken
559: branch 6 taken
0: branch 7 not taken
0: branch 8 not taken
559: branch 9 taken
559: branch 10 taken
559: branch 11 taken
0: branch 12 not taken
559: branch 13 taken
737 1118: if ((MaxMemoryInhibit && atMemoryLimit) ||
738 : current.forkDisabled ||
739 : inhibitForking ||
740 : (MaxForks!=~0u && stats::forks >= MaxForks)) {
741 : TimerStatIncrementer timer(stats::forkTime);
0: branch 1 not taken
0: branch 2 not taken
742 0: if (theRNG.getBool()) {
743 0: addConstraint(current, condition);
744 0: res = Solver::True;
745 : } else {
746 0: addConstraint(current, Expr::createNot(condition));
747 0: res = Solver::False;
748 0: }
749 : }
750 : }
751 : }
752 :
753 : // Fix branch in only-replay-seed mode, if we don't have both true
754 : // and false seeds.
9: branch 0 taken
848035: branch 1 taken
9: branch 2 taken
0: branch 3 not taken
9: branch 4 taken
0: branch 5 not taken
4: branch 6 taken
5: branch 7 taken
4: branch 8 taken
848040: branch 9 taken
755 848053: if (isSeeding &&
756 : (current.forkDisabled || OnlyReplaySeeds) &&
757 : res == Solver::Unknown) {
758 4: bool trueSeed=false, falseSeed=false;
759 : // Is seed extension still ok here?
4: branch 2 taken
4: branch 3 taken
760 24: foreach(siit, it->second.begin(), it->second.end()) {
761 : ref<Expr> res;
762 : bool success =
763 4: solver->getValue(current, siit->assignment.evaluate(condition), res);
0: branch 0 not taken
4: branch 1 taken
764 4: assert(success && "FIXME: Unhandled solver failure");
4: branch 1 taken
0: branch 2 not taken
765 4: if (res.isConstant()) {
4: branch 1 taken
0: branch 2 not taken
766 4: if (res.getConstantValue()) {
767 4: trueSeed = true;
768 : } else {
769 0: falseSeed = true;
770 : }
4: branch 0 taken
0: branch 1 not taken
4: branch 2 taken
0: branch 3 not taken
771 4: if (trueSeed && falseSeed)
772 0: break;
773 : }
774 : }
4: branch 0 taken
0: branch 1 not taken
4: branch 2 taken
0: branch 3 not taken
775 4: if (!(trueSeed && falseSeed)) {
0: branch 0 not taken
4: branch 1 taken
4: branch 2 taken
4: branch 3 taken
776 4: assert(trueSeed || falseSeed);
777 :
4: branch 0 taken
0: branch 1 not taken
778 4: res = trueSeed ? Solver::True : Solver::False;
4: branch 0 taken
0: branch 1 not taken
0: branch 5 not taken
4: branch 6 taken
779 4: addConstraint(current, trueSeed ? condition : Expr::createNot(condition));
780 : }
781 : }
782 :
783 :
784 : // XXX - even if the constraint is provable one way or the other we
785 : // can probably benefit by adding this constraint and allowing it to
786 : // reduce the other constraints. For example, if we do a binary
787 : // search on a particular value, and then see a comparison against
788 : // the value it has been fixed at, we should take this as a nice
789 : // hint to just use the single constraint instead of all the binary
790 : // search ones. If that makes sense.
840802: branch 0 taken
7242: branch 1 taken
791 848044: if (res==Solver::True) {
840655: branch 0 taken
147: branch 1 taken
792 840802: if (!isInternal) {
0: branch 0 not taken
840655: branch 1 taken
793 840655: if (pathWriter) {
794 0: current.pathOS << "1";
795 : }
796 :
797 : // only track NON-internal branches
0: branch 1 not taken
840655: branch 2 taken
798 840655: if (trackBranchSeqDetails()) {
799 0: current.branchSeqHandleStateBranch(current.prevPC->info->id, true, false);
800 : }
801 : }
802 :
803 840802: return StatePair(¤t, 0);
6683: branch 0 taken
559: branch 1 taken
804 7242: } else if (res==Solver::False) {
6652: branch 0 taken
31: branch 1 taken
805 6683: if (!isInternal) {
0: branch 0 not taken
6652: branch 1 taken
806 6652: if (pathWriter) {
807 0: current.pathOS << "0";
808 : }
809 :
810 : // only track NON-internal branches
0: branch 1 not taken
6652: branch 2 taken
811 6652: if (trackBranchSeqDetails()) {
812 0: current.branchSeqHandleStateBranch(current.prevPC->info->id, false, false);
813 : }
814 : }
815 :
816 6683: return StatePair(0, ¤t);
817 : } else {
818 : TimerStatIncrementer timer(stats::forkTime);
819 559: ExecutionState *falseState, *trueState = ¤t;
820 :
821 : ++stats::forks;
822 :
823 559: falseState = trueState->branch();
824 559: addedStates.insert(falseState);
825 :
0: branch 0 not taken
559: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
559: branch 6 taken
826 559: if (RandomizeFork && theRNG.getBool())
827 : std::swap(trueState, falseState);
828 :
0: branch 0 not taken
559: branch 1 taken
829 1118: if (it != seedMap.end()) {
830 0: std::vector<SeedInfo> seeds = it->second;
831 0: it->second.clear();
832 0: std::vector<SeedInfo> &trueSeeds = seedMap[trueState];
833 0: std::vector<SeedInfo> &falseSeeds = seedMap[falseState];
0: branch 1 not taken
0: branch 2 not taken
834 0: foreach(siit, seeds.begin(), seeds.end()) {
835 : ref<Expr> res;
836 : bool success =
837 0: solver->getValue(current, siit->assignment.evaluate(condition), res);
0: branch 0 not taken
0: branch 1 not taken
838 0: assert(success && "FIXME: Unhandled solver failure");
0: branch 1 not taken
0: branch 2 not taken
839 0: if (res.getConstantValue()) {
840 0: trueSeeds.push_back(*siit);
841 : } else {
842 0: falseSeeds.push_back(*siit);
843 : }
844 : }
845 :
846 0: bool swapInfo = false;
0: branch 0 not taken
0: branch 1 not taken
847 0: if (trueSeeds.empty()) {
0: branch 0 not taken
0: branch 1 not taken
848 0: if (¤t == trueState) swapInfo = true;
849 0: seedMap.erase(trueState);
850 : }
0: branch 0 not taken
0: branch 1 not taken
851 0: if (falseSeeds.empty()) {
0: branch 0 not taken
0: branch 1 not taken
852 0: if (¤t == falseState) swapInfo = true;
853 0: seedMap.erase(falseState);
854 : }
0: branch 0 not taken
0: branch 1 not taken
855 0: if (swapInfo) {
856 0: std::swap(trueState->coveredNew, falseState->coveredNew);
857 0: std::swap(trueState->coveredLines, falseState->coveredLines);
858 0: }
859 : }
860 :
861 559: current.ptreeNode->data = 0;
862 559: let(res, processTree->split(current.ptreeNode, falseState, trueState));
863 559: falseState->ptreeNode = res.first;
864 559: trueState->ptreeNode = res.second;
865 :
539: branch 0 taken
20: branch 1 taken
866 559: if (!isInternal) {
0: branch 0 not taken
539: branch 1 taken
867 539: if (pathWriter) {
868 0: falseState->pathOS = pathWriter->open(current.pathOS);
869 0: trueState->pathOS << "1";
870 0: falseState->pathOS << "0";
871 : }
0: branch 0 not taken
539: branch 1 taken
872 539: if (symPathWriter) {
873 0: falseState->symPathOS = symPathWriter->open(current.symPathOS);
874 0: trueState->symPathOS << "1";
875 0: falseState->symPathOS << "0";
876 : }
877 :
878 : // only track NON-internal branches
0: branch 1 not taken
539: branch 2 taken
879 539: if (trackBranchSeqDetails()) {
880 0: trueState->branchSeqHandleStateBranch(current.prevPC->info->id, true, true);
881 0: falseState->branchSeqHandleStateBranch(current.prevPC->info->id, false, true);
882 : }
883 : }
884 :
885 559: addConstraint(*trueState, condition);
886 559: addConstraint(*falseState, Expr::createNot(condition));
887 :
888 : // Kinda gross, do we even really still want this option?
0: branch 0 not taken
559: branch 1 taken
559: branch 2 taken
559: branch 3 taken
0: branch 4 not taken
559: branch 5 taken
889 559: if (MaxDepth && MaxDepth<=trueState->depth) {
890 0: terminateStateEarly(*trueState, "max-depth exceeded");
891 0: terminateStateEarly(*falseState, "max-depth exceeded");
892 0: return StatePair(0, 0);
893 : }
894 :
895 559: return StatePair(trueState, falseState);
896 : }
897 : }
898 :
899 1355: void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
0: branch 1 not taken
1355: branch 2 taken
900 1355: if (condition.isConstant()) {
901 : assert(condition.getConstantValue() &&
0: branch 1 not taken
0: branch 2 not taken
902 0: "attempt to add invalid constraint");
903 : return;
904 : }
905 :
906 : // Check to see if this constraint violates seeds.
907 1355: let(it, seedMap.find(&state));
4: branch 0 taken
1351: branch 1 taken
908 2710: if (it != seedMap.end()) {
909 4: bool warn = false;
4: branch 0 taken
4: branch 1 taken
910 20: foreach(siit, it->second.begin(), it->second.end()) {
911 : bool res;
912 : bool success =
913 4: solver->mustBeFalse(state, siit->assignment.evaluate(condition), res);
0: branch 0 not taken
4: branch 1 taken
914 4: assert(success && "FIXME: Unhandled solver failure");
0: branch 0 not taken
4: branch 1 taken
915 4: if (res) {
916 0: siit->patchSeed(state, condition, solver);
917 0: warn = true;
918 : }
919 : }
0: branch 0 not taken
4: branch 1 taken
920 4: if (warn)
921 0: klee_warning("seeds patched for violating constraint");
922 : }
923 :
924 1355: state.addConstraint(condition);
0: branch 0 not taken
1355: branch 1 taken
925 1355: if (ivcEnabled)
926 0: doImpliedValueConcretization(state, condition, ref<Expr>(1, Expr::Bool));
927 : }
928 :
929 624413: ref<Expr> Executor::evalConstant(Constant *c, MemoryObject **referent) {
930 : #ifdef KLEE_TRACK_REFERENTS
931 : // DRE: Or we could check this at each point. Not sure cleanest. DWD?
932 : #else
933 624413: referent = 0;
934 : #endif
935 :
16967: branch 0 taken
607446: branch 1 taken
936 624413: if (llvm::ConstantExpr *ce = dyn_cast<llvm::ConstantExpr>(c)) {
937 16967: ref<Expr> e = evalConstantExpr(ce, referent);
0: branch 0 not taken
16967: branch 1 taken
16967: branch 2 taken
16967: branch 3 taken
16967: branch 4 taken
16967: branch 5 taken
0: branch 6 not taken
16967: branch 7 taken
938 16967: if (referent && !*referent
939 : && ce->getOpcode() == Instruction::GetElementPtr)
940 0: assert(0 && "XXX: Have a getelementptr but no referent!");
941 33934: return e;
942 : } else {
588338: branch 0 taken
19108: branch 1 taken
943 607446: if (const ConstantInt *ci = dyn_cast<ConstantInt>(c)) {
1046: branch 0 taken
245368: branch 1 taken
295625: branch 2 taken
37531: branch 3 taken
8768: branch 4 taken
0: branch 5 not taken
944 588338: switch(ci->getBitWidth()) {
945 3138: case 1: return ConstantExpr::create(ci->getZExtValue(), Expr::Bool);
946 736104: case 8: return ConstantExpr::create(ci->getZExtValue(), Expr::Int8);
947 886875: case 16: return ConstantExpr::create(ci->getZExtValue(), Expr::Int16);
948 112593: case 32: return ConstantExpr::create(ci->getZExtValue(), Expr::Int32);
949 26304: case 64: return ConstantExpr::create(ci->getZExtValue(), Expr::Int64);
950 : default:
951 0: assert(0 && "XXX arbitrary bit width constants unhandled");
952 : }
3: branch 0 taken
19105: branch 1 taken
953 19108: } else if (const ConstantFP *cf = dyn_cast<ConstantFP>(c)) {
0: branch 0 not taken
1: branch 1 taken
2: branch 2 taken
0: branch 3 not taken
954 6: switch(cf->getType()->getTypeID()) {
955 : case Type::FloatTyID: {
956 0: float f = cf->getValueAPF().convertToFloat();
957 0: return ConstantExpr::create(floats::FloatAsUInt64(f), Expr::Int32);
958 : }
959 : case Type::DoubleTyID: {
960 1: double d = cf->getValueAPF().convertToDouble();
961 2: return ConstantExpr::create(floats::DoubleAsUInt64(d), Expr::Int64);
962 : }
963 : case Type::X86_FP80TyID: {
964 : // FIXME: This is really broken, but for now we just convert
965 : // to a double. This isn't going to work at all in general,
966 : // but we need support for wide constants.
967 2: APFloat apf = cf->getValueAPF();
968 : bool ignored;
969 : APFloat::opStatus r = apf.convert(APFloat::IEEEdouble,
970 : APFloat::rmNearestTiesToAway,
971 2: &ignored);
972 : (void) r;
973 : //assert(!(r & APFloat::opOverflow) && !(r & APFloat::opUnderflow) &&
974 : // "Overflow/underflow while converting from FP80 (x87) to 64-bit double");
975 2: double d = apf.convertToDouble();
976 4: return ConstantExpr::create(floats::DoubleAsUInt64(d), Expr::Int64);
977 : }
978 : default:
979 : llvm::cerr << "Constant of type " << cf->getType()->getDescription()
980 0: << " not supported\n";
981 : llvm::cerr << "Constant used at ";
982 0: KConstant *kc = kmodule->getKConstant((Constant*) cf);
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
983 0: if (kc && kc->ki && kc->ki->info)
984 0: llvm::cerr << kc->ki->info->file << ":" << kc->ki->info->line << "\n";
985 : else llvm::cerr << "<unknown>\n";
986 :
987 0: assert(0 && "Arbitrary bit width floating point constants unsupported");
988 : }
17756: branch 0 taken
1349: branch 1 taken
989 19105: } else if (const GlobalValue *gv = dyn_cast<GlobalValue>(c)) {
0: branch 0 not taken
17756: branch 1 taken
990 17756: if(referent) {
991 0: let(mt, globalObjects.find(gv));
992 :
993 : // XXX:DRE: need to check that it's a legal function. For tainting
994 : // possibly figure out a good value?
0: branch 0 not taken
0: branch 1 not taken
995 0: if(mt == globalObjects.end()) {
996 0: *referent = 0;
0: branch 0 not taken
0: branch 1 not taken
997 0: assert(isa<Function>(gv) && "not function: what to do?");
998 : } else {
0: branch 0 not taken
0: branch 1 not taken
999 0: assert(mt != globalObjects.end());
1000 0: *referent = mt->second;
1001 :
1002 : // FIXME: This was tied to debug_referents.
1003 : //llvm::cerr << "trying to eval: " << *gv << " got ref="
1004 : // << *referent << "\n";
0: branch 0 not taken
0: branch 1 not taken
1005 0: assert(*referent && "How can this be null?");
1006 : }
1007 : }
1008 17756: let(it, globalAddresses.find(gv));
0: branch 0 not taken
17756: branch 1 taken
1009 35512: assert(it != globalAddresses.end());
1010 35512: return it->second;
1349: branch 0 taken
0: branch 1 not taken
1011 1349: } else if (isa<ConstantPointerNull>(c)) {
1012 1349: return Expr::createPointer(0);
0: branch 0 not taken
0: branch 1 not taken
1013 0: } else if (isa<UndefValue>(c)) {
1014 0: return ConstantExpr::create(0, Expr::getWidthForLLVMType(c->getType()));
1015 : } else {
1016 : // Constant{AggregateZero,Array,Struct,Vector}
1017 0: assert(0 && "invalid argument to evalConstant()");
1018 : }
1019 : }
1020 : }
1021 :
1022 : ref<Expr> Executor::eval(KInstruction *ki,
1023 : unsigned index,
1024 : ExecutionState &state,
1025 17574165: MemoryObject **referent) {
1026 : #ifdef KLEE_TRACK_REFERENTS
1027 : #else
1028 17574165: referent = 0;
1029 : #endif
1030 :
0: branch 0 not taken
17574165: branch 1 taken
1031 35148330: assert(index < ki->inst->getNumOperands());
1032 17574165: int vnumber = ki->operands[index];
1033 :
1034 : // Determine if this is a constant or not.
9985871: branch 0 taken
7588294: branch 1 taken
1035 17574165: if (vnumber < 0) {
1036 9985871: unsigned index = -vnumber - 2;
1037 9985871: Cell &c = kmodule->constantTable[index];
1038 : #ifdef KLEE_TRACK_REFERENTS
1039 : if (referent)
1040 : *referent = c.referent;
1041 : #endif
1042 9985871: return c.value;
1043 : } else {
1044 7588294: unsigned index = vnumber;
1045 15176588: StackFrame &sf = state.stack.back();
1046 7588294: Cell &c = sf.locals[index];
1047 : #ifdef KLEE_TRACK_REFERENTS
1048 : if (referent)
1049 : *referent = c.referent;
1050 : #endif
1051 7588294: return c.value;
1052 : }
1053 : }
1054 :
1055 4942892: void Executor::bindLocal(KInstruction *target, ExecutionState &state, ref<Expr> value, MemoryObject *referent) {
1056 9885784: StackFrame &sf = state.stack.back();
1057 4942892: unsigned reg = target->dest;
1058 4942892: Cell &c = sf.locals[reg];
1059 4942892: c.value = value;
1060 : #ifdef KLEE_TRACK_REFERENTS
1061 : c.referent = referent;
1062 : #endif
1063 4942892: }
1064 :
1065 3975: void Executor::bindArgument(KFunction *kf, unsigned index, ExecutionState &state, ref<Expr> value, MemoryObject *referent) {
1066 7950: StackFrame &sf = state.stack.back();
1067 3975: unsigned reg = kf->getArgRegister(index);
1068 3975: Cell &c = sf.locals[reg];
1069 3975: c.value = value;
1070 : #ifdef KLEE_TRACK_REFERENTS
1071 : c.referent = referent;
1072 : #endif
1073 3975: }
1074 :
1075 : ref<Expr> Executor::toUnique(const ExecutionState &state,
1076 757656: ref<Expr> &e) {
1077 757656: ref<Expr> result = e;
1078 :
258: branch 1 taken
757398: branch 2 taken
1079 757656: if (!e.isConstant()) {
1080 : ref<Expr> value(0);
1081 258: bool isTrue = false;
1082 :
1083 258: solver->setTimeout(stpTimeout);
258: branch 1 taken
0: branch 2 not taken
258: branch 5 taken
0: branch 6 not taken
182: branch 7 taken
76: branch 8 taken
258: branch 9 taken
0: branch 10 not taken
258: branch 12 taken
0: branch 13 not taken
182: branch 15 taken
76: branch 16 taken
1084 516: if (solver->getValue(state, e, value) &&
1085 : solver->mustBeTrue(state, EqExpr::create(e, value), isTrue) &&
1086 : isTrue)
1087 182: result = value;
1088 516: solver->setTimeout(0);
1089 : }
1090 :
1091 : return result;
1092 : }
1093 :
1094 :
1095 : /* Concretize the given expression, and return a possible constant value.
1096 : 'reason' is just a documentation string stating the reason for concretization. */
1097 : ref<Expr> Executor::toConstant(ExecutionState &state,
1098 : ref<Expr> e,
1099 2: const char *reason) {
1100 2: e = state.constraints.simplifyExpr(e);
0: branch 1 not taken
2: branch 2 taken
1101 2: if (!e.isConstant()) {
1102 : ref<Expr> value;
1103 0: bool success = solver->getValue(state, e, value);
0: branch 0 not taken
0: branch 1 not taken
1104 0: assert(success && "FIXME: Unhandled solver failure");
1105 :
1106 0: std::ostringstream os;
1107 : os << "silently concretizing (reason: " << reason << ") expression " << e
1108 : << " to value " << value
1109 0: << " (" << (*(state.pc)).info->file << ":" << (*(state.pc)).info->line << ")";
1110 :
0: branch 0 not taken
0: branch 1 not taken
1111 0: if (AllExternalWarnings)
1112 0: klee_warning(reason, os.str().c_str());
1113 : else
1114 0: klee_warning_once(reason, "%s", os.str().c_str());
1115 :
1116 0: addConstraint(state, EqExpr::create(e, value));
1117 :
1118 0: return value;
1119 : } else {
1120 2: return e;
1121 : }
1122 : }
1123 :
1124 : void Executor::executeGetValue(ExecutionState &state,
1125 : ref<Expr> e,
1126 3: KInstruction *target) {
1127 3: e = state.constraints.simplifyExpr(e);
1128 3: let(it, seedMap.find(&state));
0: branch 0 not taken
3: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
3: branch 5 taken
0: branch 6 not taken
1129 6: if (it==seedMap.end() || e.isConstant()) {
1130 : ref<Expr> value;
1131 3: bool success = solver->getValue(state, e, value);
0: branch 0 not taken
3: branch 1 taken
1132 3: assert(success && "FIXME: Unhandled solver failure");
1133 3: bindLocal(target, state, value);
1134 : } else {
1135 : std::set< ref<Expr> > values;
0: branch 1 not taken
0: branch 2 not taken
1136 0: foreach(siit, it->second.begin(), it->second.end()) {
1137 : ref<Expr> value;
1138 : bool success =
1139 0: solver->getValue(state, siit->assignment.evaluate(e), value);
0: branch 0 not taken
0: branch 1 not taken
1140 0: assert(success && "FIXME: Unhandled solver failure");
1141 : values.insert(value);
1142 : }
1143 :
1144 : std::vector< ref<Expr> > conditions;
0: branch 0 not taken
0: branch 1 not taken
1145 0: foreach(vit, values.begin(), values.end())
1146 0: conditions.push_back(EqExpr::create(e, *vit));
1147 :
1148 : std::vector<ExecutionState*> branches;
1149 0: branch(state, conditions, branches);
1150 :
1151 : let(bit, branches.begin());
0: branch 0 not taken
0: branch 1 not taken
1152 0: foreach(vit, values.begin(), values.end()) {
1153 0: ExecutionState *es = *bit;
0: branch 0 not taken
0: branch 1 not taken
1154 0: if (es)
1155 0: bindLocal(target, *es, *vit);
1156 : ++bit;
1157 0: }
1158 : }
1159 3: }
1160 :
1161 10391933: void Executor::stepInstruction(ExecutionState &state) {
0: branch 0 not taken
10391933: branch 1 taken
1162 10391933: if (DebugPrintInstructions) {
1163 0: printFileLine(state, state.pc);
1164 0: llvm::cerr << std::setw(10) << stats::instructions << " " << *state.pc->inst;
1165 : }
1166 :
10391933: branch 0 taken
0: branch 1 not taken
1167 10391933: if (statsTracker)
1168 10391933: statsTracker->stepInstruction(state);
1169 :
1170 : ++stats::instructions;
1171 10391933: state.prevPC = state.pc;
1172 10391933: ++state.pc;
1173 :
1: branch 0 taken
10391932: branch 1 taken
1174 10391933: if (stats::instructions==StopAfterNInstructions)
1175 1: haltExecution = true;
1176 10391933: }
1177 :
1178 : void Executor::executeCall(ExecutionState &state,
1179 : KInstruction *ki,
1180 : Function *f,
1181 : std::vector< ref<Expr> > &arguments,
1182 3010898: const std::vector<MemoryObject*> &argReferents) {
0: branch 0 not taken
3010898: branch 1 taken
1183 3010898: if (WriteTraces) {
1184 : // don't print out special debug stop point 'function' calls
0: branch 1 not taken
0: branch 2 not taken
1185 0: if (f->getIntrinsicID() != Intrinsic::dbg_stoppoint) {
1186 0: const std::string& calleeFuncName = f->getName();
1187 0: state.exeTraceMgr.addEvent(new FunctionCallTraceEvent(state, ki, calleeFuncName));
1188 : }
1189 : }
1190 :
1191 3010898: Instruction *i = ki->inst;
3010898: branch 0 taken
0: branch 1 not taken
3009945: branch 3 taken
953: branch 4 taken
3009945: branch 5 taken
953: branch 6 taken
1192 3010898: if (f && f->isDeclaration()) {
525254: branch 0 taken
2484691: branch 1 taken
1193 3009945: if (f!=kmodule->dbgStopPointFn) { // special case speed hack
525243: branch 1 taken
6: branch 2 taken
0: branch 3 not taken
5: branch 4 taken
1194 525254: switch(f->getIntrinsicID()) {
1195 : case Intrinsic::dbg_stoppoint:
1196 : case Intrinsic::dbg_region_start:
1197 : case Intrinsic::dbg_region_end:
1198 : case Intrinsic::dbg_func_start:
1199 : case Intrinsic::dbg_declare:
1200 : case Intrinsic::not_intrinsic:
1201 : #if 1
1202 : //XXX:DRE: need the referent for this one single call: rather than
1203 : //change the infrastructure we just special case.
0: branch 2 not taken
525243: branch 3 taken
1204 1050486: if(f->getName() == "klee_points_to_obj")
1205 0: handlePointsToObj(state, ki, arguments, argReferents);
1206 : else
1207 : #endif
1208 : // state may be destroyed by this call, cannot touch
1209 525243: callExternalFunction(state, ki, f, arguments);
1210 : break;
1211 :
1212 : // vararg is handled by caller and intrinsic lowering,
1213 : // see comment for ExecutionState::varargs
1214 : case Intrinsic::vastart: {
1215 12: StackFrame &sf = state.stack.back();
0: branch 0 not taken
6: branch 1 taken
1216 6: assert(sf.varargs && "vastart called in function with no vararg object");
1217 : #ifdef KLEE_TRACK_REFERENTS
1218 : executeMemoryOperation(state, true, arguments[0], argReferents[0], sf.varargs->getBaseExpr(), sf.varargs, 0);
1219 : #else
1220 12: executeMemoryOperation(state, true, arguments[0], 0, sf.varargs->getBaseExpr(), 0, 0);
1221 : #endif
1222 6: break;
1223 : }
1224 : case Intrinsic::vaend: // va_end is a noop for the interpreter
1225 : break;
1226 :
1227 : case Intrinsic::vacopy: // should be lowered
1228 : default:
1229 0: klee_error("unknown intrinsic: %s", f->getName().c_str());
1230 : }
1231 : }
1232 :
0: branch 0 not taken
3009945: branch 1 taken
1233 3009945: if (InvokeInst *ii = dyn_cast<InvokeInst>(i)) {
1234 0: transferToBasicBlock(ii->getNormalDest(), i->getParent(), state);
1235 : }
1236 : } else {
1237 : // XXX not really happy about this reliance on prevPC but is ok I
1238 : // guess. This just done to avoid having to pass KInstIterator
1239 : // everywhere instead of the actual instruction, since we can't
1240 : // make a KInstIterator from just an instruction (unlike LLVM).
1241 953: KFunction *kf = kmodule->functionMap[f];
1242 1906: state.pushFrame(state.prevPC, kf);
1243 2859: state.pc = kf->instructions;
1244 :
953: branch 0 taken
0: branch 1 not taken
1245 953: if (statsTracker)
1246 2859: statsTracker->framePushed(state, &state.stack[state.stack.size()-2]);
1247 :
1248 953: unsigned callingArgs = arguments.size();
1249 953: unsigned funcArgs = f->arg_size();
948: branch 1 taken
5: branch 2 taken
1250 953: if (!f->isVarArg()) {
3: branch 0 taken
945: branch 1 taken
1251 948: if (callingArgs > funcArgs) {
1252 : klee_warning_once(f, "calling %s with extra arguments.",
1253 6: f->getName().c_str());
0: branch 0 not taken
945: branch 1 taken
1254 945: } else if (callingArgs < funcArgs) {
1255 : terminateStateOnError(state, "calling function with too few arguments",
1256 0: "user.err");
1257 : return;
1258 : }
1259 : } else {
0: branch 0 not taken
5: branch 1 taken
1260 5: if (callingArgs < funcArgs) {
1261 : terminateStateOnError(state, "calling function with too few arguments",
1262 0: "user.err");
1263 : return;
1264 : }
1265 :
1266 10: StackFrame &sf = state.stack.back();
1267 5: unsigned size = 0;
20: branch 0 taken
5: branch 1 taken
1268 25: for (unsigned i = funcArgs; i < callingArgs; i++)
1269 40: size += Expr::getMinBytesForWidth(arguments[i].getWidth());
1270 :
1271 : MemoryObject *mo = sf.varargs = memory->allocate(size, true, false,
1272 10: state.prevPC->inst);
0: branch 0 not taken
5: branch 1 taken
1273 5: if (!mo) {
1274 0: terminateStateOnExecError(state, "out of memory (varargs)");
1275 : return;
1276 : }
1277 5: ObjectState *os = bindObjectInState(state, mo, true);
1278 5: unsigned offset = 0;
20: branch 0 taken
5: branch 1 taken
1279 25: for (unsigned i = funcArgs; i < callingArgs; i++) {
1280 : // XXX: DRE: i think we bind memory objects here?
1281 20: os->write(offset, arguments[i]);
1282 20: if(argReferents[i])
1283 : writeReferent(state, os,
1284 : ConstantExpr::create(offset, Expr::Int32), argReferents[i]);
1285 :
1286 40: offset += Expr::getMinBytesForWidth(arguments[i].getWidth());
1287 : }
1288 : }
1289 :
1290 953: unsigned numFormals = f->arg_size();
3899: branch 0 taken
953: branch 1 taken
1291 4852: for (unsigned i=0; i<numFormals; ++i)
1292 7798: bindArgument(kf, i, state, arguments[i], argReferents[i]);
1293 : }
1294 : }
1295 :
1296 : void Executor::transferToBasicBlock(BasicBlock *dst, BasicBlock *src,
1297 1693730: ExecutionState &state) {
1298 : // Note that in general phi nodes can reuse phi values from the same
1299 : // block but the incoming value is the eval() result *before* the
1300 : // execution of any phi nodes. this is pathological and doesn't
1301 : // really seem to occur, but just in case we run the PhiCleanerPass
1302 : // which makes sure this cannot happen and so it is safe to just
1303 : // eval things in order. The PhiCleanerPass also makes sure that all
1304 : // incoming blocks have the same order for each PHINode so we only
1305 : // have to compute the index once.
1306 : //
1307 : // With that done we simply set an index in the state so that PHI
1308 : // instructions know which argument to eval, set the pc, and continue.
1309 :
1310 : // XXX this lookup has to go ?
1311 3387460: KFunction *kf = state.stack.back().kf;
1312 3387460: unsigned entry = kf->basicBlockEntry[dst];
1313 5081190: state.pc = &kf->instructions[entry];
970: branch 0 taken
1692760: branch 1 taken
1314 5081190: if (state.pc->inst->getOpcode() == Instruction::PHI) {
1315 1940: PHINode *first = static_cast<PHINode*>(state.pc->inst);
1316 970: state.incomingBBIndex = first->getBasicBlockIndex(src);
1317 : }
1318 1693730: }
1319 :
1320 0: void Executor::printFileLine(ExecutionState &state, KInstruction *ki) {
1321 0: const InstructionInfo &ii = *ki->info;
0: branch 0 not taken
0: branch 1 not taken
1322 0: if (ii.file != "")
1323 0: llvm::cerr << " " << ii.file << ":" << ii.line << ":";
1324 : else
1325 : llvm::cerr << " [no debug info]:";
1326 0: }
1327 :
1328 :
1329 3010898: Function* Executor::getCalledFunction(CallSite &cs, ExecutionState &state) {
1330 3010898: Function *f = cs.getCalledFunction();
1331 :
3010735: branch 0 taken
163: branch 1 taken
1332 3010898: if (f) {
1333 3010735: std::string alias = state.getFnAlias(f->getName());
4: branch 0 taken
3010731: branch 1 taken
1334 3010735: if (alias != "") {
1335 : //llvm::cerr << f->getName() << "() is aliased with " << alias << "()\n";
1336 4: llvm::Module* currModule = kmodule->module;
1337 4: Function* old_f = f;
1338 4: f = currModule->getFunction(alias);
0: branch 0 not taken
4: branch 1 taken
1339 4: if (!f) {
1340 0: llvm::cerr << "Function " << alias << "(), alias for " << old_f->getName() << " not found!\n";
0: branch 0 not taken
0: branch 1 not taken
1341 0: assert(f && "function alias not found");
1342 : }
1343 3010735: }
1344 : }
1345 :
1346 3010898: return f;
1347 : }
1348 :
1349 :
1350 10391932: void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
1351 10391932: Instruction *i = ki->inst;
2147: branch 0 taken
1: branch 1 taken
1692219: branch 2 taken
841: branch 3 taken
0: branch 4 not taken
3010898: branch 5 taken
1022: branch 6 taken
348: branch 7 taken
0: branch 8 not taken
1142500: branch 9 taken
1620: branch 10 taken
261: branch 11 taken
5: branch 12 taken
3: branch 13 taken
4: branch 14 taken
0: branch 15 not taken
3249: branch 16 taken
1024: branch 17 taken
167: branch 18 taken
430: branch 19 taken
535: branch 20 taken
0: branch 21 not taken
853286: branch 22 taken
230997: branch 23 taken
2: branch 24 taken
2137042: branch 25 taken
1268872: branch 26 taken
21654: branch 27 taken
10640: branch 28 taken
7836: branch 29 taken
33: branch 30 taken
7: branch 31 taken
2069: branch 32 taken
2220: branch 33 taken
0: branch 34 not taken
0: branch 35 not taken
0: branch 36 not taken
0: branch 37 not taken
0: branch 38 not taken
0: branch 39 not taken
0: branch 40 not taken
0: branch 41 not taken
0: branch 42 not taken
0: branch 43 not taken
0: branch 44 not taken
1352 20783864: switch (i->getOpcode()) {
1353 : // Control flow
1354 : case Instruction::Ret: {
1355 2147: ReturnInst *ri = cast<ReturnInst>(i);
1356 4294: KInstIterator kcaller = state.stack.back().caller;
1511: branch 0 taken
636: branch 1 taken
1357 3658: Instruction *caller = kcaller ? kcaller->inst : 0;
1358 2147: bool isVoidReturn = (ri->getNumOperands() == 0);
1359 : ref<Expr> result(0,Expr::Bool);
1360 2147: MemoryObject *resultReferent = 0;
1361 :
0: branch 0 not taken
2147: branch 1 taken
1362 2147: if (WriteTraces) {
1363 0: state.exeTraceMgr.addEvent(new FunctionReturnTraceEvent(state, ki));
1364 : }
1365 :
1819: branch 0 taken
328: branch 1 taken
1366 2147: if (!isVoidReturn) {
1367 1819: result = eval(ki, 0, state, &resultReferent);
1368 : }
1369 :
636: branch 0 taken
1511: branch 1 taken
1370 4294: if (state.stack.size() <= 1) {
0: branch 0 not taken
636: branch 1 taken
1371 636: assert(!caller && "caller set on initial stack frame");
1372 636: terminateStateOnExit(state);
1373 : } else {
1374 1511: state.popFrame();
1375 :
1511: branch 0 taken
0: branch 1 not taken
1376 1511: if (statsTracker)
1377 1511: statsTracker->framePopped(state);
1378 :
2: branch 0 taken
1509: branch 1 taken
1379 1511: if (InvokeInst *ii = dyn_cast<InvokeInst>(caller)) {
1380 4: transferToBasicBlock(ii->getNormalDest(), caller->getParent(), state);
1381 : } else {
1382 1509: state.pc = kcaller;
1383 1509: ++state.pc;
1384 : }
1385 :
1183: branch 0 taken
328: branch 1 taken
1386 1511: if (!isVoidReturn) {
1387 2366: const Type *t = caller->getType();
1183: branch 0 taken
0: branch 1 not taken
1388 1183: if (t != Type::VoidTy) {
1389 : // may need to do coercion due to bitcasts
1390 1183: Expr::Width from = result.getWidth();
1391 1183: Expr::Width to = Expr::getWidthForLLVMType(t);
1392 :
0: branch 0 not taken
1183: branch 1 taken
1393 1183: if (from != to) {
1394 : CallSite cs = (isa<InvokeInst>(caller) ? CallSite(cast<InvokeInst>(caller)) :
0: branch 0 not taken
0: branch 1 not taken
1395 0: CallSite(cast<CallInst>(caller)));
1396 :
1397 : // XXX need to check other param attrs ?
0: branch 1 not taken
0: branch 2 not taken
1398 0: if (cs.paramHasAttr(0, llvm::Attribute::SExt)) {
1399 0: result = SExtExpr::create(result, to);
1400 : } else {
1401 0: result = ZExtExpr::create(result, to);
1402 : }
1403 : }
1404 :
1405 2366: bindLocal(kcaller, state, result, resultReferent);
1406 : }
1407 : } else {
1408 : // We check that the return value has no users instead of
1409 : // checking the type, since C defaults to returning int for
1410 : // undeclared functions.
0: branch 0 not taken
328: branch 1 taken
1411 656: if (!caller->use_empty()) {
1412 0: terminateStateOnExecError(state, "return void when caller expected a result");
1413 : }
1414 : }
1415 : }
1416 2147: break;
1417 : }
1418 : case Instruction::Unwind: {
1419 : for (;;) {
1420 3: KInstruction *kcaller = state.stack.back().caller;
1421 1: state.popFrame();
1422 :
1: branch 0 taken
0: branch 1 not taken
1423 1: if (statsTracker)
1424 1: statsTracker->framePopped(state);
1425 :
0: branch 0 not taken
1: branch 1 taken
1426 2: if (state.stack.empty()) {
1427 0: terminateStateOnExecError(state, "unwind from initial stack frame");
1428 : break;
1429 : } else {
1430 1: Instruction *caller = kcaller->inst;
0: branch 0 not taken
1: branch 1 taken
1431 1: if (InvokeInst *ii = dyn_cast<InvokeInst>(caller)) {
1432 2: transferToBasicBlock(ii->getUnwindDest(), caller->getParent(), state);
1433 1: break;
1434 : }
1435 : }
1436 : }
1437 : break;
1438 : }
1439 : case Instruction::Br: {
1440 1692219: BranchInst *bi = cast<BranchInst>(i);
844373: branch 0 taken
847846: branch 1 taken
1441 1692219: if (bi->isUnconditional()) {
1442 1688746: transferToBasicBlock(bi->getSuccessor(0), bi->getParent(), state);
1443 : } else {
1444 : // FIXME: Find a way that we don't have this hidden dependency.
1445 : assert(bi->getCondition() == bi->getOperand(0) &&
0: branch 2 not taken
847846: branch 3 taken
1446 847846: "Wrong operand index!");
1447 847846: ref<Expr> cond = eval(ki, 0, state);
1448 847846: Executor::StatePair branches = fork(state, cond, false);
1449 :
0: branch 0 not taken
847846: branch 1 taken
1450 847846: if (WriteTraces) {
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
1451 0: bool isTwoWay = (branches.first && branches.second);
1452 :
0: branch 0 not taken
0: branch 1 not taken
1453 0: if (branches.first) {
1454 : branches.first->exeTraceMgr.addEvent(
1455 0: new BranchTraceEvent(state, ki, true, isTwoWay));
1456 : }
1457 :
0: branch 0 not taken
0: branch 1 not taken
1458 0: if (branches.second) {
1459 : branches.second->exeTraceMgr.addEvent(
1460 0: new BranchTraceEvent(state, ki, false, isTwoWay));
1461 : }
1462 : }
1463 :
1464 : // NOTE: There is a hidden dependency here, markBranchVisited
1465 : // requires that we still be in the context of the branch
1466 : // instruction (it reuses its statistic id). Should be cleaned
1467 : // up with convenient instruction specific data.
847846: branch 0 taken
0: branch 1 not taken
847846: branch 2 taken
0: branch 3 not taken
847846: branch 4 taken
0: branch 5 not taken
1468 1695692: if (statsTracker && state.stack.back().kf->trackCoverage)
1469 847846: statsTracker->markBranchVisited(branches.first, branches.second);
1470 :
841194: branch 0 taken
6652: branch 1 taken
1471 847846: if (branches.first)
1472 1682388: transferToBasicBlock(bi->getSuccessor(0), bi->getParent(), *branches.first);
7191: branch 0 taken
840655: branch 1 taken
1473 847846: if (branches.second)
1474 14382: transferToBasicBlock(bi->getSuccessor(1), bi->getParent(), *branches.second);
1475 : }
1476 : break;
1477 : }
1478 : case Instruction::Switch: {
1479 841: SwitchInst *si = cast<SwitchInst>(i);
1480 841: ref<Expr> cond = eval(ki, 0, state);
1481 841: unsigned cases = si->getNumCases();
1482 1682: BasicBlock *bb = si->getParent();
1483 :
1484 841: cond = toUnique(state, cond);
765: branch 1 taken
76: branch 2 taken
1485 841: if (cond.isConstant()) {
1486 : // Somewhat gross to create these all the time, but fine till we
1487 : // switch to an internal rep.
1488 : ConstantInt *ci = ConstantInt::get(si->getCondition()->getType(),
1489 1530: cond.getConstantValue());
1490 765: unsigned index = si->findCaseValue(ci);
1491 1530: transferToBasicBlock(si->getSuccessor(index), si->getParent(), state);
1492 : } else {
1493 : std::map<BasicBlock*, ref<Expr> > targets;
1494 : ref<Expr> isDefault(1,Expr::Bool);
879: branch 2 taken
76: branch 3 taken
1495 955: for (unsigned i=1; i<cases; ++i) {
1496 879: ref<Expr> value = evalConstant(si->getCaseValue(i), 0);
1497 879: ref<Expr> match = EqExpr::create(cond, value);
1498 879: isDefault = AndExpr::create(isDefault, Expr::createNot(match));
1499 : bool result;
1500 879: bool success = solver->mayBeTrue(state, match, result);
0: branch 0 not taken
879: branch 1 taken
1501 879: assert(success && "FIXME: Unhandled solver failure");
246: branch 0 taken
633: branch 1 taken
1502 879: if (result) {
1503 738: let(it, targets.insert(std::make_pair(si->getSuccessor(i),
1504 : ref<Expr>(0,Expr::Bool))).first);
1505 492: it->second = OrExpr::create(match, it->second);
1506 : }
1507 : }
1508 : bool res;
1509 76: bool success = solver->mayBeTrue(state, isDefault, res);
0: branch 0 not taken
76: branch 1 taken
1510 76: assert(success && "FIXME: Unhandled solver failure");
61: branch 0 taken
15: branch 1 taken
1511 76: if (res)
1512 183: targets.insert(std::make_pair(si->getSuccessor(0), isDefault));
1513 :
1514 : std::vector< ref<Expr> > conditions;
204: branch 0 taken
76: branch 1 taken
1515 356: foreach(it, targets.begin(), targets.end())
1516 204: conditions.push_back(it->second);
1517 :
1518 : std::vector<ExecutionState*> branches;
1519 76: branch(state, conditions, branches);
1520 :
1521 : let(bit, branches.begin());
204: branch 0 taken
76: branch 1 taken
1522 356: foreach(it, targets.begin(), targets.end()) {
1523 204: ExecutionState *es = *bit;
204: branch 0 taken
0: branch 1 not taken
1524 204: if (es)
1525 204: transferToBasicBlock(it->first, bb, *es);
1526 : ++bit;
1527 76: }
1528 : }
1529 841: break;
1530 : }
1531 : case Instruction::Unreachable:
1532 : // Note that this is not necessarily an internal bug, llvm will
1533 : // generate unreachable instructions in cases where it knows the
1534 : // program will crash. So it is effectively a SEGV or internal
1535 : // error.
1536 0: terminateStateOnExecError(state, "reached \"unreachable\" instruction");
1537 : break;
1538 :
1539 : case Instruction::Invoke:
1540 : case Instruction::Call: {
1541 : CallSite cs;
1542 : unsigned argStart;
3010895: branch 0 taken
3: branch 1 taken
1543 6021796: if (i->getOpcode()==Instruction::Call) {
1544 3010895: cs = CallSite(cast<CallInst>(i));
1545 3010895: argStart = 1;
1546 : } else {
1547 3: cs = CallSite(cast<InvokeInst>(i));
1548 3: argStart = 3;
1549 : }
1550 :
1551 3010898: unsigned numArgs = cs.arg_size();
1552 3010898: Function *f = getCalledFunction(cs, state);
1553 :
1554 : // evaluate arguments
1555 : std::vector< ref<Expr> > arguments;
1556 3010898: arguments.reserve(numArgs);
1557 :
1558 : // XXX:DRE: track when pass to function: we do this even w/o
1559 : // referent tracking to keep the code a bit cleaner. Easy to
1560 : // option it. DWD?
1561 : std::vector< MemoryObject * > argReferents;
1562 3010898: argReferents.reserve(numArgs);
1563 :
7983570: branch 0 taken
3010898: branch 1 taken
1564 10994468: for (unsigned j=0; j<numArgs; ++j) {
1565 7983570: MemoryObject *ref = 0;
1566 7983570: arguments.push_back(eval(ki, argStart+j, state, &ref));
1567 : argReferents.push_back(ref);
1568 : }
1569 :
163: branch 0 taken
3010735: branch 1 taken
1570 3010898: if (!f) {
1571 : // special case the call with a bitcast case
1572 163: Value *fp = cs.getCalledValue();
1573 163: llvm::ConstantExpr *ce = dyn_cast<llvm::ConstantExpr>(fp);
1574 :
147: branch 0 taken
16: branch 1 taken
147: branch 2 taken
0: branch 3 not taken
147: branch 4 taken
16: branch 5 taken
1575 310: if (ce && ce->getOpcode()==Instruction::BitCast) {
1576 294: f = dyn_cast<Function>(ce->getOperand(0));
0: branch 0 not taken
147: branch 1 taken
1577 147: assert(f && "XXX unrecognized constant expression in call");
1578 : const FunctionType *fType =
1579 588: dyn_cast<FunctionType>(cast<PointerType>(f->getType())->getElementType());
1580 : const FunctionType *ceType =
1581 588: dyn_cast<FunctionType>(cast<PointerType>(ce->getType())->getElementType());
0: branch 0 not taken
147: branch 1 taken
1582 147: assert(fType && ceType && "unable to get function type");
1583 :
1584 : // XXX check result coercion
1585 :
1586 : // XXX this really needs thought and validation
1587 147: unsigned i=0;
350: branch 0 taken
147: branch 1 taken
1588 644: foreach(ai, arguments.begin(), arguments.end()) {
1589 350: Expr::Width to, from = (*ai).getWidth();
1590 :
346: branch 0 taken
4: branch 1 taken
1591 350: if (i<fType->getNumParams()) {
1592 346: to = Expr::getWidthForLLVMType(fType->getParamType(i));
1593 :
1: branch 0 taken
345: branch 1 taken
1594 346: if (from != to) {
1595 : // XXX need to check other param attrs ?
0: branch 1 not taken
1: branch 2 taken
1596 1: if (cs.paramHasAttr(i+1, llvm::Attribute::SExt)) {
1597 0: arguments[i] = SExtExpr::create(arguments[i], to);
1598 : } else {
1599 2: arguments[i] = ZExtExpr::create(arguments[i], to);
1600 : }
1601 : }
1602 : }
1603 :
1604 350: i++;
1605 : }
0: branch 0 not taken
16: branch 1 taken
1606 16: } else if (isa<InlineAsm>(fp)) {
1607 0: terminateStateOnExecError(state, "inline assembly is unsupported");
1608 : break;
1609 : }
1610 : }
1611 :
3010882: branch 0 taken
16: branch 1 taken
1612 3010898: if (f) {
1613 3010882: executeCall(state, ki, f, arguments, argReferents);
1614 : } else {
1615 16: ref<Expr> v = eval(ki, 0, state);
1616 :
1617 16: ExecutionState *free = &state;
1618 16: bool hasInvalid = false, first = true;
1619 :
1620 : /* XXX This is wasteful, no need to do a full evaluate since we
1621 : have already got a value. But in the end the caches should
1622 : handle it for us, albeit with some overhead. */
0: branch 0 not taken
16: branch 1 taken
1623 16: do {
1624 : ref<Expr> value;
1625 16: bool success = solver->getValue(*free, v, value);
0: branch 0 not taken
16: branch 1 taken
1626 16: assert(success && "FIXME: Unhandled solver failure");
1627 16: StatePair res = fork(*free, EqExpr::create(v, value), true);
16: branch 0 taken
0: branch 1 not taken
1628 16: if (res.first) {
1629 16: void *addr = (void*) (unsigned long) value.getConstantValue();
1630 16: let(it, legalFunctions.find(addr));
16: branch 0 taken
0: branch 1 not taken
1631 32: if (it != legalFunctions.end()) {
1632 16: f = (Function*) addr;
1633 :
1634 : // Don't give warning on unique resolution
16: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
16: branch 3 taken
1635 16: if (res.second || !first)
1636 : klee_warning_once(addr, "resolved symbolic function pointer to: %s",
1637 0: f->getName().c_str());
1638 :
1639 16: executeCall(*res.first, ki, f, arguments, argReferents);
1640 : } else {
0: branch 0 not taken
0: branch 1 not taken
1641 0: if (!hasInvalid) {
1642 0: terminateStateOnExecError(state, "invalid function pointer");
1643 0: hasInvalid = true;
1644 : }
1645 : }
1646 : }
1647 :
1648 16: first = false;
1649 16: free = res.second;
1650 16: } while (free);
1651 : }
1652 3010898: break;
1653 : }
1654 : case Instruction::PHI: {
1655 1022: MemoryObject *referent = 0;
1656 1022: ref<Expr> result = eval(ki, state.incomingBBIndex * 2, state, &referent);
1657 2044: bindLocal(ki, state, result, referent);
1658 1022: break;
1659 : }
1660 :
1661 : // Special instructions
1662 : case Instruction::Select: {
1663 348: SelectInst *SI = cast<SelectInst>(ki->inst);
1664 : assert(SI->getCondition() == SI->getOperand(0) &&
0: branch 1 not taken
348: branch 2 taken
1665 348: "Wrong operand index!");
1666 348: MemoryObject *lref = 0, *rref = 0;
1667 348: ref<Expr> cond = eval(ki, 0, state);
1668 348: ref<Expr> tExpr = eval(ki, 1, state, &lref);
1669 348: ref<Expr> fExpr = eval(ki, 2, state, &rref);
1670 348: ref<Expr> result = SelectExpr::create(cond, tExpr, fExpr);
1671 : // XXX:DRE: This isn't really going to work? Can do "X ? p : q"
1672 : // where p and q point to different things.
1673 696: bindLocal(ki, state, result, selectReferent(lref, rref));
1674 348: break;
1675 : }
1676 :
1677 : case Instruction::VAArg:
1678 0: terminateStateOnExecError(state, "unexpected VAArg instruction");
1679 : break;
1680 :
1681 : // Arithmetic / logical
1682 : #define FP_CONSTANT_BINOP(op, type, l, r, target, state) \
1683 : bindLocal(target, state, \
1684 : ref<Expr>(op(toConstant(state, l, "floating point").getConstantValue(), \
1685 : toConstant(state, r, "floating point").getConstantValue(), \
1686 : type), type))
1687 : case Instruction::Add: {
1688 1142500: MemoryObject *lref=0, *rref=0, *referent=0;
1689 1142500: BinaryOperator *bi = cast<BinaryOperator>(i);
1690 1142500: ref<Expr> left = eval(ki, 0, state, &lref);
1691 1142500: ref<Expr> right = eval(ki, 1, state, &rref);
1692 1142500: referent = selectReferent(lref, rref);
1693 :
1142499: branch 0 taken
1: branch 1 taken
1694 2285000: if( bi->getType()->getTypeID() == llvm::Type::IntegerTyID ) {
1695 1142499: bindLocal(ki, state, AddExpr::create(left, right), referent);
1696 : } else {
0: branch 0 not taken
1: branch 1 taken
1697 1: assert(!referent && "Not supporting FP on referent stuff");
1698 2: Expr::Width type = Expr::getWidthForLLVMType(bi->getType());
1699 3: FP_CONSTANT_BINOP(floats::add, type, left, right, ki, state);
1700 : }
1701 :
1702 1142500: break;
1703 : }
1704 :
1705 : case Instruction::Sub: {
1706 1620: MemoryObject *lref=0, *rref=0, *referent=0;
1707 1620: BinaryOperator *bi = cast<BinaryOperator>(i);
1708 1620: ref<Expr> left = eval(ki, 0, state, &lref);
1709 1620: ref<Expr> right = eval(ki, 1, state, &rref);
1710 1620: referent = selectReferent(lref, rref);
1711 :
1620: branch 0 taken
0: branch 1 not taken
1712 3240: if( bi->getType()->getTypeID() == llvm::Type::IntegerTyID ) {
1713 1620: bindLocal(ki, state, SubExpr::create(left, right), referent);
1714 : } else {
0: branch 0 not taken
0: branch 1 not taken
1715 0: assert(!referent && "Not supporting FP on referent stuff");
1716 0: Expr::Width type = Expr::getWidthForLLVMType(bi->getType());
1717 0: FP_CONSTANT_BINOP(floats::sub, type, left, right, ki, state);
1718 : }
1719 :
1720 1620: break;
1721 : }
1722 :
1723 : case Instruction::Mul: {
1724 261: BinaryOperator *bi = cast<BinaryOperator>(i);
1725 261: ref<Expr> left = eval(ki, 0, state);
1726 261: ref<Expr> right = eval(ki, 1, state);
1727 :
261: branch 0 taken
0: branch 1 not taken
1728 522: if( bi->getType()->getTypeID() == llvm::Type::IntegerTyID ) {
1729 261: bindLocal(ki, state, MulExpr::create(left, right));
1730 : } else {
1731 0: Expr::Width type = Expr::getWidthForLLVMType(bi->getType());
1732 0: FP_CONSTANT_BINOP(floats::mul, type, left, right, ki, state);
1733 : }
1734 :
1735 261: break;
1736 : }
1737 :
1738 : case Instruction::UDiv: {
1739 5: ref<Expr> left = eval(ki, 0, state);
1740 5: ref<Expr> right = eval(ki, 1, state);
1741 5: ref<Expr> result = UDivExpr::create(left, right);
1742 5: bindLocal(ki, state, result);
1743 5: break;
1744 : }
1745 :
1746 : case Instruction::SDiv: {
1747 3: ref<Expr> left = eval(ki, 0, state);
1748 3: ref<Expr> right = eval(ki, 1, state);
1749 3: ref<Expr> result = SDivExpr::create(left, right);
1750 3: bindLocal(ki, state, result);
1751 3: break;
1752 : }
1753 :
1754 : case Instruction::URem: {
1755 4: ref<Expr> left = eval(ki, 0, state);
1756 4: ref<Expr> right = eval(ki, 1, state);
1757 4: ref<Expr> result = URemExpr::create(left, right);
1758 4: bindLocal(ki, state, result);
1759 4: break;
1760 : }
1761 :
1762 : case Instruction::SRem: {
1763 0: ref<Expr> left = eval(ki, 0, state);
1764 0: ref<Expr> right = eval(ki, 1, state);
1765 0: ref<Expr> result = SRemExpr::create(left, right);
1766 0: bindLocal(ki, state, result);
1767 0: break;
1768 : }
1769 :
1770 : // DRE: the following three instructions shouldn't influence referent
1771 : // tracking. However, people do weird things, so we do too: pointers
1772 : // are integers, yo! We draw the line (sensibly?) at various
1773 : // shift operations.
1774 : case Instruction::And: {
1775 3249: MemoryObject *lref=0, *rref=0;
1776 3249: ref<Expr> left = eval(ki, 0, state, &lref);
1777 3249: ref<Expr> right = eval(ki, 1, state, &rref);
1778 3249: ref<Expr> result = AndExpr::create(left, right);
1779 6498: bindLocal(ki, state, result, selectReferent(lref, rref));
1780 3249: break;
1781 : }
1782 :
1783 : case Instruction::Or: {
1784 1024: MemoryObject *lref=0, *rref=0;
1785 1024: ref<Expr> left = eval(ki, 0, state, &lref);
1786 1024: ref<Expr> right = eval(ki, 1, state, &rref);
1787 1024: ref<Expr> result = OrExpr::create(left, right);
1788 2048: bindLocal(ki, state, result, selectReferent(lref, rref));
1789 1024: break;
1790 : }
1791 :
1792 : case Instruction::Xor: {
1793 167: MemoryObject *lref=0, *rref=0;
1794 167: ref<Expr> left = eval(ki, 0, state, &lref);
1795 167: ref<Expr> right = eval(ki, 1, state, &rref);
1796 167: ref<Expr> result = XorExpr::create(left, right);
1797 334: bindLocal(ki, state, result, selectReferent(lref, rref));
1798 167: break;
1799 : }
1800 :
1801 : case Instruction::Shl: {
1802 430: ref<Expr> left = eval(ki, 0, state);
1803 430: ref<Expr> right = eval(ki, 1, state);
1804 430: ref<Expr> result = ShlExpr::create(left, right);
1805 430: bindLocal(ki, state, result);
1806 430: break;
1807 : }
1808 :
1809 : case Instruction::LShr: {
1810 535: ref<Expr> left = eval(ki, 0, state);
1811 535: ref<Expr> right = eval(ki, 1, state);
1812 535: ref<Expr> result = LShrExpr::create(left, right);
1813 535: bindLocal(ki, state, result);
1814 535: break;
1815 : }
1816 :
1817 : case Instruction::AShr: {
1818 0: ref<Expr> left = eval(ki, 0, state);
1819 0: ref<Expr> right = eval(ki, 1, state);
1820 0: ref<Expr> result = AShrExpr::create(left, right);
1821 0: bindLocal(ki, state, result);
1822 0: break;
1823 : }
1824 :
1825 : // Compare
1826 :
1827 : case Instruction::ICmp: {
1828 853286: CmpInst *ci = cast<CmpInst>(i);
1829 853286: ICmpInst *ii = cast<ICmpInst>(ci);
1830 :
7540: branch 0 taken
7513: branch 1 taken
367: branch 2 taken
120: branch 3 taken
359: branch 4 taken
8781: branch 5 taken
555: branch 6 taken
228: branch 7 taken
709: branch 8 taken
827114: branch 9 taken
0: branch 10 not taken
1831 1706572: switch(ii->getPredicate()) {
1832 : case ICmpInst::ICMP_EQ: {
1833 7540: ref<Expr> left = eval(ki, 0, state);
1834 7540: ref<Expr> right = eval(ki, 1, state);
1835 7540: ref<Expr> result = EqExpr::create(left, right);
1836 7540: bindLocal(ki, state, result);
1837 7540: break;
1838 : }
1839 :
1840 : case ICmpInst::ICMP_NE: {
1841 7513: ref<Expr> left = eval(ki, 0, state);
1842 7513: ref<Expr> right = eval(ki, 1, state);
1843 7513: ref<Expr> result = NeExpr::create(left, right);
1844 7513: bindLocal(ki, state, result);
1845 7513: break;
1846 : }
1847 :
1848 : case ICmpInst::ICMP_UGT: {
1849 367: ref<Expr> left = eval(ki, 0, state);
1850 367: ref<Expr> right = eval(ki, 1, state);
1851 367: ref<Expr> result = UgtExpr::create(left, right);
1852 367: bindLocal(ki, state,result);
1853 367: break;
1854 : }
1855 :
1856 : case ICmpInst::ICMP_UGE: {
1857 120: ref<Expr> left = eval(ki, 0, state);
1858 120: ref<Expr> right = eval(ki, 1, state);
1859 120: ref<Expr> result = UgeExpr::create(left, right);
1860 120: bindLocal(ki, state, result);
1861 120: break;
1862 : }
1863 :
1864 : case ICmpInst::ICMP_ULT: {
1865 359: ref<Expr> left = eval(ki, 0, state);
1866 359: ref<Expr> right = eval(ki, 1, state);
1867 359: ref<Expr> result = UltExpr::create(left, right);
1868 359: bindLocal(ki, state, result);
1869 359: break;
1870 : }
1871 :
1872 : case ICmpInst::ICMP_ULE: {
1873 8781: ref<Expr> left = eval(ki, 0, state);
1874 8781: ref<Expr> right = eval(ki, 1, state);
1875 8781: ref<Expr> result = UleExpr::create(left, right);
1876 8781: bindLocal(ki, state, result);
1877 8781: break;
1878 : }
1879 :
1880 : case ICmpInst::ICMP_SGT: {
1881 555: ref<Expr> left = eval(ki, 0, state);
1882 555: ref<Expr> right = eval(ki, 1, state);
1883 555: ref<Expr> result = SgtExpr::create(left, right);
1884 555: bindLocal(ki, state, result);
1885 555: break;
1886 : }
1887 :
1888 : case ICmpInst::ICMP_SGE: {
1889 228: ref<Expr> left = eval(ki, 0, state);
1890 228: ref<Expr> right = eval(ki, 1, state);
1891 228: ref<Expr> result = SgeExpr::create(left, right);
1892 228: bindLocal(ki, state, result);
1893 228: break;
1894 : }
1895 :
1896 : case ICmpInst::ICMP_SLT: {
1897 709: ref<Expr> left = eval(ki, 0, state);
1898 709: ref<Expr> right = eval(ki, 1, state);
1899 709: ref<Expr> result = SltExpr::create(left, right);
1900 709: bindLocal(ki, state, result);
1901 709: break;
1902 : }
1903 :
1904 : case ICmpInst::ICMP_SLE: {
1905 827114: ref<Expr> left = eval(ki, 0, state);
1906 827114: ref<Expr> right = eval(ki, 1, state);
1907 827114: ref<Expr> result = SleExpr::create(left, right);
1908 827114: bindLocal(ki, state, result);
1909 827114: break;
1910 : }
1911 :
1912 : default:
1913 0: terminateStateOnExecError(state, "invalid ICmp predicate");
1914 : }
1915 : break;
1916 : }
1917 :
1918 : // Memory instructions...
1919 : case Instruction::Alloca:
1920 : case Instruction::Malloc: {
1921 230997: AllocationInst *ai = cast<AllocationInst>(i);
1922 : unsigned elementSize =
1923 230997: kmodule->targetData->getTypeStoreSize(ai->getAllocatedType());
1924 230997: ref<Expr> size = Expr::createPointer(elementSize);
0: branch 1 not taken
230997: branch 2 taken
1925 230997: if (ai->isArrayAllocation()) {
1926 : // XXX coerce?
1927 0: ref<Expr> count = eval(ki, 0, state);
1928 0: size = MulExpr::create(count, size);
1929 : }
1930 461994: bool isLocal = i->getOpcode()==Instruction::Alloca;
1931 461994: executeAlloc(state, size, isLocal, ki);
1932 230997: break;
1933 : }
1934 : case Instruction::Free: {
1935 2: executeFree(state, eval(ki, 0, state));
1936 2: break;
1937 : }
1938 :
1939 : case Instruction::Load: {
1940 2137042: LoadInst *li = cast<LoadInst>(i);
1941 2137042: MemoryObject *referent = 0;
1942 2137042: ref<Expr> base = eval(ki, 0, state, &referent);
2137042: branch 0 taken
0: branch 1 not taken
1943 2137042: if(!referent)
1944 4274084: referent = recoverReferent(state, base, li->getOperand(0));
1945 4274084: executeMemoryOperation(state, false, base, referent, 0, 0, ki);
1946 2137042: break;
1947 : }
1948 : case Instruction::Store: {
1949 1268872: StoreInst *si = cast<StoreInst>(i);
1950 1268872: MemoryObject *baseReferent = 0, *valueReferent = 0;
1951 :
1952 1268872: ref<Expr> base = eval(ki, 1, state, &baseReferent);
1268872: branch 0 taken
0: branch 1 not taken
1953 1268872: if(!baseReferent)
1954 2537744: baseReferent = recoverReferent(state, base, si->getOperand(1));
1955 :
1956 : // XXX: what about value?
1957 1268872: ref<Expr> value = eval(ki, 0, state, &valueReferent);
1958 :
1959 : executeMemoryOperation(state, true, base, baseReferent,
1960 3806616: value, valueReferent, 0);
1961 1268872: break;
1962 : }
1963 :
1964 : case Instruction::GetElementPtr: {
1965 21654: KGEPInstruction *kgepi = static_cast<KGEPInstruction*>(ki);
1966 21654: MemoryObject *referent = 0;
1967 21654: ref<Expr> base = eval(ki, 0, state, &referent);
1968 :
21654: branch 0 taken
0: branch 1 not taken
1969 21654: if (!referent)
1970 43308: referent = recoverReferent(state, base, i->getOperand(0));
1971 :
12592: branch 1 taken
21654: branch 2 taken
1972 90146: foreach(it, kgepi->indices.begin(), kgepi->indices.end()) {
1973 12592: unsigned elementSize = it->second;
1974 12592: ref<Expr> index = eval(ki, it->first, state);
1975 : base = AddExpr::create(base,
1976 : MulExpr::create(Expr::createCoerceToPointerType(index),
1977 25184: Expr::createPointer(elementSize)));
1978 : }
8256: branch 0 taken
13398: branch 1 taken
1979 21654: if (kgepi->offset)
1980 : base = AddExpr::create(base,
1981 8256: Expr::createPointer(kgepi->offset));
1982 43308: bindLocal(ki, state, base, referent);
1983 21654: break;
1984 : }
1985 :
1986 : // Conversion
1987 : case Instruction::Trunc: {
1988 10640: CastInst *ci = cast<CastInst>(i);
1989 : ref<Expr> result = ExtractExpr::createByteOff(eval(ki, 0, state),
1990 : 0,
1991 21280: Expr::getWidthForLLVMType(ci->getType()));
1992 10640: bindLocal(ki, state, result);
1993 10640: break;
1994 : }
1995 : case Instruction::ZExt: {
1996 7836: CastInst *ci = cast<CastInst>(i);
1997 : ref<Expr> result = ZExtExpr::create(eval(ki, 0, state),
1998 15672: Expr::getWidthForLLVMType(ci->getType()));
1999 7836: bindLocal(ki, state, result);
2000 7836: break;
2001 : }
2002 : case Instruction::SExt: {
2003 33: CastInst *ci = cast<CastInst>(i);
2004 : ref<Expr> result = SExtExpr::create(eval(ki, 0, state),
2005 66: Expr::getWidthForLLVMType(ci->getType()));
2006 33: bindLocal(ki, state, result);
2007 33: break;
2008 : }
2009 :
2010 : case Instruction::IntToPtr: {
2011 7: CastInst *ci = cast<CastInst>(i);
2012 14: Expr::Width pType = Expr::getWidthForLLVMType(ci->getType());
2013 7: MemoryObject *referent = 0;
2014 7: ref<Expr> arg = eval(ki, 0, state, &referent);
2015 :
2016 : #ifdef KLEE_TRACK_REFERENTS
2017 : // DRE: "safety net" to try to recover referents.
2018 : if (!referent) {
2019 : if(!arg.isConstant()) {
2020 : assert(0 && "FIXME: Lost referent. Think about resolution.\n");
2021 : } else {
2022 : ObjectPair op;
2023 : bool success;
2024 : assert(state.addressSpace.resolveOne(state, solver, arg, op, success) &&
2025 : "timeout");
2026 : assert(success && "out of bounds / multiple resolution unhandled");
2027 : referent = (MemoryObject*) op.first;
2028 : assert(solver->mustBeTrue(state,
2029 : referent->getBoundsCheckPointer(arg)) &&
2030 : "out of bounds unhandled");
2031 : assert(referent && "Lost referent: FIXME!");
2032 : }
2033 : }
2034 : #endif
2035 :
2036 7: bindLocal(ki, state, ZExtExpr::create(arg, pType), referent);
2037 7: break;
2038 : }
2039 : case Instruction::PtrToInt: {
2040 2069: CastInst *ci = cast<CastInst>(i);
2041 4138: Expr::Width iType = Expr::getWidthForLLVMType(ci->getType());
2042 2069: MemoryObject *referent = 0;
2043 2069: ref<Expr> arg = eval(ki, 0, state, &referent);
2044 :
2045 2069: bindLocal(ki, state, ZExtExpr::create(arg, iType), referent);
2046 2069: break;
2047 : }
2048 :
2049 : case Instruction::BitCast: {
2050 2220: MemoryObject *referent = 0;
2051 2220: ref<Expr> result = eval(ki, 0, state, &referent);
2052 4440: bindLocal(ki, state, result, referent);
2053 2220: break;
2054 : }
2055 :
2056 : // Floating Point specific instructions
2057 : case Instruction::FPTrunc: {
2058 0: FPTruncInst *fi = cast<FPTruncInst>(i);
2059 0: Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
2060 : ref<Expr> arg = toConstant(state, eval(ki, 0, state),
2061 0: "floating point");
2062 : uint64_t value = floats::trunc(arg.getConstantValue(),
2063 : resultType,
2064 0: arg.getWidth());
2065 : ref<Expr> result(value, resultType);
2066 0: bindLocal(ki, state, result);
2067 0: break;
2068 : }
2069 :
2070 : case Instruction::FPExt: {
2071 0: FPExtInst *fi = cast<FPExtInst>(i);
2072 0: Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
2073 : ref<Expr> arg = toConstant(state, eval(ki, 0, state),
2074 0: "floating point");
2075 : uint64_t value = floats::ext(arg.getConstantValue(),
2076 : resultType,
2077 0: arg.getWidth());
2078 : ref<Expr> result(value, resultType);
2079 0: bindLocal(ki, state, result);
2080 0: break;
2081 : }
2082 :
2083 : case Instruction::FPToUI: {
2084 0: FPToUIInst *fi = cast<FPToUIInst>(i);
2085 0: Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
2086 : ref<Expr> arg = toConstant(state, eval(ki, 0, state),
2087 0: "floating point");
2088 : uint64_t value = floats::toUnsignedInt(arg.getConstantValue(),
2089 : resultType,
2090 0: arg.getWidth());
2091 : ref<Expr> result(value, resultType);
2092 0: bindLocal(ki, state, result);
2093 0: break;
2094 : }
2095 :
2096 : case Instruction::FPToSI: {
2097 0: FPToSIInst *fi = cast<FPToSIInst>(i);
2098 0: Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
2099 : ref<Expr> arg = toConstant(state, eval(ki, 0, state),
2100 0: "floating point");
2101 : uint64_t value = floats::toSignedInt(arg.getConstantValue(),
2102 : resultType,
2103 0: arg.getWidth());
2104 : ref<Expr> result(value, resultType);
2105 0: bindLocal(ki, state, result);
2106 0: break;
2107 : }
2108 :
2109 : case Instruction::UIToFP: {
2110 0: UIToFPInst *fi = cast<UIToFPInst>(i);
2111 0: Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
2112 : ref<Expr> arg = toConstant(state, eval(ki, 0, state),
2113 0: "floating point");
2114 : uint64_t value = floats::UnsignedIntToFP(arg.getConstantValue(),
2115 0: resultType);
2116 : ref<Expr> result(value, resultType);
2117 0: bindLocal(ki, state, result);
2118 0: break;
2119 : }
2120 :
2121 : case Instruction::SIToFP: {
2122 0: SIToFPInst *fi = cast<SIToFPInst>(i);
2123 0: Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
2124 : ref<Expr> arg = toConstant(state, eval(ki, 0, state),
2125 0: "floating point");
2126 : uint64_t value = floats::SignedIntToFP(arg.getConstantValue(),
2127 : resultType,
2128 0: arg.getWidth());
2129 : ref<Expr> result(value, resultType);
2130 0: bindLocal(ki, state, result);
2131 0: break;
2132 : }
2133 :
2134 : case Instruction::FCmp: {
2135 0: FCmpInst *fi = cast<FCmpInst>(i);
2136 0: Expr::Width resultType = Expr::getWidthForLLVMType(fi->getType());
2137 : ref<Expr> left = toConstant(state, eval(ki, 0, state),
2138 0: "floating point");
2139 : ref<Expr> right = toConstant(state, eval(ki, 1, state),
2140 0: "floating point");
2141 0: uint64_t leftVal = left.getConstantValue();
2142 0: uint64_t rightVal = right.getConstantValue();
2143 :
2144 : //determine whether the operands are NANs
2145 0: unsigned inWidth = left.getWidth();
2146 0: bool leftIsNaN = floats::isNaN( leftVal, inWidth );
2147 0: bool rightIsNaN = floats::isNaN( rightVal, inWidth );
2148 :
2149 : //handle NAN based on whether the predicate is "ordered" or "unordered"
2150 0: uint64_t ret = (uint64_t)-1;
2151 0: bool done = false;
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
2152 0: switch( fi->getPredicate() ) {
2153 : //predicates which only care about whether or not the operands are NaNs
2154 : case FCmpInst::FCMP_ORD:
2155 0: done = true;
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
2156 0: ret = !leftIsNaN && !rightIsNaN;
2157 0: break;
2158 :
2159 : case FCmpInst::FCMP_UNO:
2160 0: done = true;
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
2161 0: ret = leftIsNaN || rightIsNaN;
2162 0: break;
2163 :
2164 : //ordered comparisons return false if either operand is NaN
2165 : case FCmpInst::FCMP_OEQ:
2166 : case FCmpInst::FCMP_OGT:
2167 : case FCmpInst::FCMP_OGE:
2168 : case FCmpInst::FCMP_OLT:
2169 : case FCmpInst::FCMP_OLE:
2170 : case FCmpInst::FCMP_ONE:
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
2171 0: if( !leftIsNaN && !rightIsNaN) //only fall through and return false if there are NaN(s)
2172 0: break;
2173 :
2174 : case FCmpInst::FCMP_FALSE: { //always return false for this predicate
2175 0: done = true;
2176 0: ret = false;
2177 0: break;
2178 : }
2179 :
2180 : //unordered comparisons return true if either operand is NaN
2181 : case FCmpInst::FCMP_UEQ:
2182 : case FCmpInst::FCMP_UGT:
2183 : case FCmpInst::FCMP_UGE:
2184 : case FCmpInst::FCMP_ULT:
2185 : case FCmpInst::FCMP_ULE:
2186 : case FCmpInst::FCMP_UNE:
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
2187 0: if( !leftIsNaN && !rightIsNaN) //only fall through and return true if there are NaN(s)
2188 0: break;
2189 :
2190 : case FCmpInst::FCMP_TRUE: //always return true for this predicate
2191 0: done = true;
2192 0: ret = true;
2193 :
2194 : default:
2195 : case FCmpInst::BAD_FCMP_PREDICATE: /* will fall through and trigger fatal in the next switch */
2196 : break;
2197 : }
2198 :
2199 : //if not done, then we need to actually do a comparison to get the result
0: branch 0 not taken
0: branch 1 not taken
2200 0: if( !done ) {
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
2201 0: switch( fi->getPredicate() ) {
2202 : //ordered comparisons return false if either operand is NaN
2203 : case FCmpInst::FCMP_OEQ:
2204 : case FCmpInst::FCMP_UEQ:
2205 0: ret = floats::eq( leftVal, rightVal, inWidth );
2206 0: break;
2207 :
2208 : case FCmpInst::FCMP_OGT:
2209 : case FCmpInst::FCMP_UGT:
2210 0: ret = floats::gt( leftVal, rightVal, inWidth );
2211 0: break;
2212 :
2213 : case FCmpInst::FCMP_OGE:
2214 : case FCmpInst::FCMP_UGE:
2215 0: ret = floats::ge( leftVal, rightVal, inWidth );
2216 0: break;
2217 :
2218 : case FCmpInst::FCMP_OLT:
2219 : case FCmpInst::FCMP_ULT:
2220 0: ret = floats::lt( leftVal, rightVal, inWidth );
2221 0: break;
2222 :
2223 : case FCmpInst::FCMP_OLE:
2224 : case FCmpInst::FCMP_ULE:
2225 0: ret = floats::le( leftVal, rightVal, inWidth );
2226 0: break;
2227 :
2228 : case FCmpInst::FCMP_ONE:
2229 : case FCmpInst::FCMP_UNE:
2230 0: ret = floats::ne( leftVal, rightVal, inWidth );
2231 0: break;
2232 :
2233 : default:
2234 0: terminateStateOnExecError(state, "invalid FCmp predicate");
2235 : }
2236 : }
2237 :
2238 : ref<Expr> result(ret, resultType);
2239 0: bindLocal(ki, state, result);
2240 0: break;
2241 : }
2242 :
2243 : case Instruction::FDiv: {
2244 0: BinaryOperator *bi = cast<BinaryOperator>(i);
2245 :
2246 0: ref<Expr> dividend = eval(ki, 0, state);
2247 0: ref<Expr> divisor = eval(ki, 1, state);
2248 0: Expr::Width type = Expr::getWidthForLLVMType(bi->getType());
2249 0: FP_CONSTANT_BINOP(floats::div, type, dividend, divisor, ki, state);
2250 0: break;
2251 : }
2252 :
2253 : case Instruction::FRem: {
2254 0: BinaryOperator *bi = cast<BinaryOperator>(i);
2255 :
2256 0: ref<Expr> dividend = eval(ki, 0, state);
2257 0: ref<Expr> divisor = eval(ki, 1, state);
2258 0: Expr::Width type = Expr::getWidthForLLVMType(bi->getType());
2259 0: FP_CONSTANT_BINOP(floats::mod, type, dividend, divisor, ki, state);
2260 0: break;
2261 : }
2262 :
2263 :
2264 : // Other instructions...
2265 : // Unhandled
2266 : case Instruction::ExtractElement:
2267 : case Instruction::InsertElement:
2268 : case Instruction::ShuffleVector:
2269 : terminateStateOnError(state, "XXX vector instructions unhandled",
2270 0: "xxx.err");
2271 : break;
2272 :
2273 : default:
2274 0: terminateStateOnExecError(state, "invalid instruction");
2275 : break;
2276 : }
2277 10391932: }
2278 :
2279 10391933: void Executor::updateStates(ExecutionState *current) {
10391867: branch 0 taken
66: branch 1 taken
2280 10391933: if (searcher) {
2281 10391867: searcher->update(current, addedStates, removedStates);
2282 : }
2283 :
2284 31175799: states.insert(addedStates.begin(), addedStates.end());
2285 10391933: addedStates.clear();
2286 :
785: branch 0 taken
10391933: branch 1 taken
2287 31176584: foreach(it, removedStates.begin(), removedStates.end()) {
2288 785: ExecutionState *es = *it;
2289 785: let(it2, states.find(es));
0: branch 0 not taken
785: branch 1 taken
2290 1570: assert(it2!=states.end());
2291 785: states.erase(it2);
2292 785: let(it3, seedMap.find(es));
1: branch 0 taken
784: branch 1 taken
2293 1570: if (it3 != seedMap.end()) {
2294 1: seedMap.erase(it3);
2295 : }
2296 785: processTree->remove(es->ptreeNode);
785: branch 0 taken
0: branch 1 not taken
2297 785: delete es;
2298 : }
2299 10391933: removedStates.clear();
2300 10391933: }
2301 :
2302 92853: void Executor::bindInstructionConstants(KInstruction *KI) {
2303 185706: GetElementPtrInst *gepi = dyn_cast<GetElementPtrInst>(KI->inst);
88792: branch 0 taken
4061: branch 1 taken
2304 92853: if (!gepi)
2305 88792: return;
2306 :
2307 4061: KGEPInstruction *kgepi = static_cast<KGEPInstruction*>(KI);
2308 4061: ref<Expr> constantOffset = Expr::createPointer(0);
2309 4061: unsigned index = 1;
5621: branch 0 taken
4061: branch 1 taken
2310 17804: for (gep_type_iterator ii = gep_type_begin(gepi), ie = gep_type_end(gepi);
2311 : ii != ie; ++ii) {
968: branch 0 taken
4653: branch 1 taken
2312 11242: if (const StructType *st = dyn_cast<StructType>(*ii)) {
2313 : const StructLayout *sl =
2314 968: kmodule->targetData->getStructLayout(st);
2315 968: const ConstantInt *ci = cast<ConstantInt>(ii.getOperand());
2316 : ref<Expr> addend = Expr::createPointer(sl->getElementOffset((unsigned)
2317 968: ci->getZExtValue()));
2318 968: constantOffset = AddExpr::create(constantOffset, addend);
2319 : } else {
2320 4653: const SequentialType *st = cast<SequentialType>(*ii);
2321 : unsigned elementSize =
2322 4653: kmodule->targetData->getTypeStoreSize(st->getElementType());
2323 4653: Value *operand = ii.getOperand();
3263: branch 0 taken
1390: branch 1 taken
2324 4653: if (Constant *c = dyn_cast<Constant>(operand)) {
2325 3263: ref<Expr> index = evalConstant(c);
2326 : ref<Expr> addend = MulExpr::create(Expr::createCoerceToPointerType(index),
2327 6526: Expr::createPointer(elementSize));
2328 3263: constantOffset = AddExpr::create(constantOffset, addend);
2329 : } else {
2330 2780: kgepi->indices.push_back(std::make_pair(index, elementSize));
2331 : }
2332 : }
2333 5621: index++;
2334 : }
0: branch 1 not taken
4061: branch 2 taken
2335 4061: assert(constantOffset.isConstant());
2336 4061: kgepi->offset = constantOffset.getConstantValue();
2337 : }
2338 :
2339 103: void Executor::bindModuleConstants() {
520: branch 0 taken
103: branch 1 taken
2340 829: foreach(it, kmodule->functions.begin(), kmodule->functions.end()) {
2341 520: KFunction *kf = *it;
92853: branch 0 taken
520: branch 1 taken
2342 93373: for (unsigned i=0; i<kf->numInstructions; ++i)
2343 92853: bindInstructionConstants(kf->instructions[i]);
2344 : }
2345 :
4762: branch 1 taken
103: branch 2 taken
2346 4968: kmodule->constantTable = new Cell[kmodule->constants.size()];
4762: branch 0 taken
103: branch 1 taken
2347 9730: for (unsigned i=0; i<kmodule->constants.size(); ++i) {
2348 4762: Cell &c = kmodule->constantTable[i];
2349 : #ifdef KLEE_TRACK_REFERENTS
2350 : MemoryObject **referentp = &c.referent;
2351 : #else
2352 4762: MemoryObject *referent, **referentp = &referent;
2353 : #endif
2354 9524: c.value = evalConstant(kmodule->constants[i], referentp);
2355 : }
2356 103: }
2357 :
2358 103: void Executor::run(ExecutionState &initialState) {
2359 103: bindModuleConstants();
2360 :
2361 : // Delay init till now so that ticks don't accrue during
2362 : // optimization and such.
2363 103: initTimers();
2364 :
2365 103: states.insert(&initialState);
2366 :
1: branch 0 taken
102: branch 1 taken
2367 103: if (usingSeeds) {
2368 1: std::vector<SeedInfo> &v = seedMap[&initialState];
2369 :
1: branch 0 taken
1: branch 1 taken
2370 4: foreach(it, usingSeeds->begin(), usingSeeds->end()) {
2371 2: v.push_back(SeedInfo(*it));
2372 : }
2373 :
2374 2: int lastNumSeeds = usingSeeds->size()+10;
2375 1: double lastTime, startTime = lastTime = util::getWallTime();
2376 1: ExecutionState *lastState = 0;
65: branch 0 taken
1: branch 1 taken
2377 133: while (!seedMap.empty()) {
65: branch 0 taken
0: branch 1 not taken
2378 65: if (haltExecution) goto dump;
2379 :
2380 65: let(it, seedMap.upper_bound(lastState));
64: branch 0 taken
1: branch 1 taken
2381 130: if (it == seedMap.end())
2382 128: it = seedMap.begin();
2383 65: lastState = it->first;
2384 130: unsigned numSeeds = it->second.size();
2385 65: ExecutionState &state = *lastState;
2386 130: KInstruction *ki = state.pc;
2387 65: stepInstruction(state);
2388 :
2389 65: executeInstruction(state, ki);
2390 65: processTimers(&state, MaxInstructionTime * numSeeds);
2391 65: updateStates(&state);
2392 :
0: branch 0 not taken
65: branch 1 taken
2393 65: if ((stats::instructions % 1000) == 0) {
2394 0: int numSeeds = 0, numStates = 0;
0: branch 0 not taken
0: branch 1 not taken
2395 0: foreach(it, seedMap.begin(), seedMap.end()) {
2396 0: numSeeds += it->second.size();
2397 0: numStates++;
2398 : }
2399 0: double time = util::getWallTime();
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
2400 0: if (SeedTime>0. && time > startTime + SeedTime) {
2401 : klee_warning("seed time expired, %d seeds remain over %d states",
2402 0: numSeeds, numStates);
2403 0: break;
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
2404 0: } else if (numSeeds<=lastNumSeeds-10 ||
2405 : time >= lastTime+10) {
2406 0: lastTime = time;
2407 0: lastNumSeeds = numSeeds;
2408 : klee_message("%d seeds remaining over: %d states",
2409 0: numSeeds, numStates);
2410 : }
2411 : }
2412 : }
2413 :
2414 2: klee_message("seeding done (%d states remain)", (int) states.size());
2415 :
2416 : // XXX total hack, just because I like non uniform better but want
2417 : // seed results to be equally weighted.
0: branch 0 not taken
1: branch 1 taken
2418 3: foreach(it, states.begin(), states.end()) {
2419 0: (*it)->weight = 1.;
2420 : }
2421 :
0: branch 0 not taken
1: branch 1 taken
2422 1: if (OnlySeed)
2423 0: goto dump;
2424 : }
2425 :
2426 103: searcher = constructUserSearcher(*this);
2427 :
2428 206: searcher->update(0, states, std::set<ExecutionState*>());
2429 :
10391868: branch 0 taken
102: branch 1 taken
10391867: branch 2 taken
1: branch 3 taken
10391867: branch 4 taken
103: branch 5 taken
2430 20783940: while (!states.empty() && !haltExecution) {
2431 10391867: ExecutionState &state = searcher->selectState();
2432 20783734: KInstruction *ki = state.pc;
2433 10391867: stepInstruction(state);
2434 :
2435 10391867: executeInstruction(state, ki);
2436 10391867: processTimers(&state, MaxInstructionTime);
2437 :
9699328: branch 0 taken
692539: branch 1 taken
2438 10391867: if (MaxMemory) {
148: branch 0 taken
9699180: branch 1 taken
2439 9699328: if ((stats::instructions & 0xFFFF) == 0) {
2440 : // We need to avoid calling GetMallocUsage() often because it
2441 : // is O(elts on freelist). This is really bad since we start
2442 : // to pummel the freelist once we hit the memory cap.
2443 148: unsigned mbs = sys::Process::GetTotalMemoryUsage() >> 20;
2444 :
125: branch 0 taken
23: branch 1 taken
2445 148: if (mbs > MaxMemory) {
2: branch 0 taken
123: branch 1 taken
2446 125: if (mbs > MaxMemory + 100) {
2447 : // just guess at how many to kill
2448 4: unsigned numStates = states.size();
2449 4: unsigned toKill = std::max(1U, numStates - numStates*MaxMemory/mbs);
2450 :
2: branch 0 taken
0: branch 1 not taken
2451 2: if (MaxMemoryInhibit)
2452 : klee_warning("killing %d states (over memory cap)",
2453 2: toKill);
2454 :
2455 6: std::vector<ExecutionState*> arr(states.begin(), states.end());
2: branch 0 taken
2: branch 1 taken
2456 6: for (unsigned i=0,N=arr.size(); N && i<toKill; ++i,--N) {
2457 2: unsigned idx = rand() % N;
2458 :
2459 : // Make two pulls to try and not hit a state that
2460 : // covered new code.
2: branch 0 taken
0: branch 1 not taken
2461 2: if (arr[idx]->coveredNew)
2462 2: idx = rand() % N;
2463 :
2464 2: std::swap(arr[idx], arr[N-1]);
2465 4: terminateStateEarly(*arr[N-1], "memory limit");
2466 2: }
2467 : }
2468 125: atMemoryLimit = true;
2469 : } else {
2470 23: atMemoryLimit = false;
2471 : }
2472 : }
2473 : }
2474 :
2475 10391867: updateStates(&state);
2476 : }
2477 :
103: branch 0 taken
0: branch 1 not taken
2478 103: delete searcher;
2479 103: searcher = 0;
2480 :
2481 : dump:
103: branch 0 taken
0: branch 1 not taken
1: branch 2 taken
102: branch 3 taken
1: branch 4 taken
102: branch 5 taken
2482 206: if (DumpStatesOnHalt && !states.empty()) {
2483 : llvm::cerr << "KLEE: halting execution, dumping remaining states\n";
1: branch 0 taken
1: branch 1 taken
2484 5: foreach(it, states.begin(), states.end()) {
2485 1: ExecutionState &state = **it;
2486 1: stepInstruction(state); // keep stats rolling
2487 1: terminateStateEarly(state, "execution halting");
2488 : }
2489 1: updateStates(0);
2490 : }
2491 103: }
2492 :
2493 : std::string Executor::getAddressInfo(ExecutionState &state,
2494 19: ref<Expr> address) const{
2495 19: std::ostringstream info;
2496 19: info << "\taddress: " << address << "\n";
2497 : uint64_t example;
14: branch 1 taken
5: branch 2 taken
2498 19: if (address.isConstant()) {
2499 14: example = address.getConstantValue();
2500 : } else {
2501 : ref<Expr> value;
2502 5: bool success = solver->getValue(state, address, value);
0: branch 0 not taken
5: branch 1 taken
2503 5: assert(success && "FIXME: Unhandled solver failure");
2504 5: example = value.getConstantValue();
2505 10: info << "\texample: " << example << "\n";
2506 10: let(res, solver->getRange(state, address));
2507 10: info << "\trange: [" << res.first << ", " << res.second <<"]\n";
2508 : }
2509 :
2510 19: MemoryObject hack((unsigned) example);
2511 19: let(lower, state.addressSpace.objects.upper_bound(&hack));
2512 19: info << "\tnext: ";
2: branch 1 taken
17: branch 2 taken
2513 38: if (lower==state.addressSpace.objects.end()) {
2514 2: info << "none\n";
2515 : } else {
2516 17: const MemoryObject *mo = lower->first;
2517 : info << "object at " << mo->address
2518 51: << " of size " << mo->size << "\n";
2519 : }
16: branch 1 taken
3: branch 2 taken
2520 38: if (lower!=state.addressSpace.objects.begin()) {
2521 : --lower;
2522 16: info << "\tprev: ";
0: branch 1 not taken
16: branch 2 taken
2523 32: if (lower==state.addressSpace.objects.end()) {
2524 0: info << "none\n";
2525 : } else {
2526 16: const MemoryObject *mo = lower->first;
2527 : info << "object at " << mo->address
2528 48: << " of size " << mo->size << "\n";
2529 : }
2530 : }
2531 :
2532 19: return info.str();
2533 : }
2534 :
2535 790: void Executor::terminateState(ExecutionState &state) {
1: branch 0 taken
789: branch 1 taken
0: branch 2 not taken
1: branch 3 taken
2536 790: if (replayOut && replayPosition!=replayOut->numObjects) {
2537 0: klee_warning_once(replayOut, "replay did not consume all objects in .bout input.");
2538 : }
2539 :
2540 790: interpreterHandler->incPathsExplored();
2541 :
0: branch 1 not taken
790: branch 2 taken
2542 790: if (trackBranchSeqDetails()) {
2543 0: statsTracker->writeStateTerminationCounts(state);
2544 : }
2545 :
2546 : //klee_message_to_file("Finished exploring path %u",
2547 : // interpreterHandler->getNumPathsExplored());
2548 :
2549 790: let(it, addedStates.find(&state));
785: branch 0 taken
5: branch 1 taken
2550 1580: if (it==addedStates.end()) {
2551 785: state.pc = state.prevPC;
2552 :
2553 785: removedStates.insert(&state);
2554 : } else {
2555 : // never reached searcher, just delete immediately
2556 5: let(it3, seedMap.find(&state));
0: branch 0 not taken
5: branch 1 taken
2557 10: if (it3 != seedMap.end())
2558 0: seedMap.erase(it3);
2559 5: addedStates.erase(it);
2560 5: processTree->remove(state.ptreeNode);
5: branch 0 taken
0: branch 1 not taken
2561 5: delete &state;
2562 : }
2563 790: }
2564 :
2565 3: void Executor::terminateStateEarly(ExecutionState &state, std::string message) {
0: branch 0 not taken
3: branch 1 taken
3: branch 2 taken
3: branch 3 taken
3: branch 4 taken
3: branch 5 taken
3: branch 6 taken
3: branch 7 taken
3: branch 8 taken
0: branch 9 not taken
2566 3: if (!OnlyOutputStatesCoveringNew || state.coveredNew ||
2567 : (AlwaysOutputSeeds && seedMap.count(&state)))
2568 6: interpreterHandler->processTestCase(state, (message + "\n").c_str(), "early");
2569 3: terminateState(state);
2570 3: }
2571 :
2572 641: void Executor::terminateStateOnExit(ExecutionState &state) {
1: branch 0 taken
640: branch 1 taken
0: branch 2 not taken
1: branch 3 taken
1: branch 4 taken
1: branch 5 taken
1: branch 6 taken
1: branch 7 taken
641: branch 8 taken
0: branch 9 not taken
2573 641: if (!OnlyOutputStatesCoveringNew || state.coveredNew ||
2574 : (AlwaysOutputSeeds && seedMap.count(&state)))
2575 641: interpreterHandler->processTestCase(state, 0, 0);
2576 641: terminateState(state);
2577 641: }
2578 :
2579 : void Executor::terminateStateOnError(ExecutionState &state,
2580 : const std::string &message,
2581 : const std::string &suffix,
2582 27: const std::string &info) {
20: branch 0 taken
7: branch 1 taken
20: branch 3 taken
0: branch 4 not taken
2583 47: static std::set< std::pair<Instruction*, std::string> > emittedErrors;
2584 54: const InstructionInfo &ii = *state.prevPC->info;
2585 :
22: branch 0 taken
5: branch 1 taken
22: branch 3 taken
0: branch 4 not taken
22: branch 5 taken
5: branch 6 taken
22: branch 7 taken
5: branch 8 taken
27: branch 10 taken
0: branch 11 not taken
2586 147: if (EmitAllErrors ||
2587 : emittedErrors.insert(std::make_pair(state.prevPC->inst,message)).second) {
8: branch 0 taken
19: branch 1 taken
2588 54: if (ii.file != "") {
2589 16: klee_message("ERROR: %s:%d: %s", ii.file.c_str(), ii.line, message.c_str());
2590 : } else {
2591 19: klee_message("ERROR: %s", message.c_str());
2592 : }
22: branch 0 taken
5: branch 1 taken
2593 27: if (!EmitAllErrors)
2594 22: klee_message("NOTE: now ignoring this error at this location");
2595 :
2596 27: std::ostringstream msg;
2597 27: msg << "Error: " << message << "\n";
8: branch 0 taken
19: branch 1 taken
2598 54: if (ii.file != "") {
2599 8: msg << "File: " << ii.file << "\n";
2600 16: msg << "Line: " << ii.line << "\n";
2601 : }
2602 27: msg << "Stack: \n";
2603 27: unsigned idx = 0;
2604 54: const KInstruction *target = state.prevPC;
33: branch 0 taken
27: branch 1 taken
2605 141: foreach(it, state.stack.rbegin(), state.stack.rend()) {
2606 33: StackFrame &sf = *it;
2607 33: Function *f = sf.kf->function;
2608 33: const InstructionInfo &ii = *target->info;
2609 : msg << "\t#" << idx++
2610 : << " " << std::setw(8) << std::setfill('0') << ii.assemblyLine
2611 165: << " in " << f->getName() << " (";
2612 : // Yawn, we could go up and print varargs if we wanted to.
2613 33: unsigned index = 0;
10: branch 2 taken
33: branch 3 taken
2614 86: foreach(ai, f->arg_begin(), f->arg_end()) {
3: branch 0 taken
7: branch 1 taken
2615 10: if (ai!=f->arg_begin()) msg << ", ";
2616 :
2617 10: msg << ai->getName();
2618 : // XXX should go through function
2619 20: ref<Expr> value = sf.locals[sf.kf->getArgRegister(index++)].value;
9: branch 1 taken
1: branch 2 taken
2620 10: if (value.isConstant())
2621 9: msg << "=" << value;
2622 : }
2623 33: msg << ")";
10: branch 0 taken
23: branch 1 taken
2624 66: if (ii.file != "")
2625 10: msg << " at " << ii.file << ":" << ii.line;
2626 33: msg << "\n";
2627 66: target = sf.caller;
2628 : }
2629 :
19: branch 0 taken
8: branch 1 taken
2630 27: if (info != "")
2631 19: msg << "Info: \n" << info;
2632 81: interpreterHandler->processTestCase(state, msg.str().c_str(), suffix.c_str());
2633 : }
2634 :
2635 27: terminateState(state);
2636 27: }
2637 :
2638 : // XXX shoot me
2639 : static const char *okExternalsList[] = { "printf",
2640 : "fprintf",
2641 : "puts",
2642 : "getpid" };
2643 103: static std::set<std::string> okExternals(okExternalsList,
2644 : okExternalsList +
2645 103: (sizeof(okExternalsList)/sizeof(okExternalsList[0])));
2646 :
2647 : void Executor::callExternalFunction(ExecutionState &state,
2648 : KInstruction *target,
2649 : Function *function,
2650 525243: std::vector< ref<Expr> > &arguments) {
2651 : // check if specialFunctionHandler wants it
524955: branch 1 taken
288: branch 2 taken
2652 525243: if (specialFunctionHandler->handle(state, function, target, arguments))
2653 524955: return;
2654 :
0: branch 0 not taken
288: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
288: branch 6 taken
0: branch 8 not taken
288: branch 9 taken
2655 576: if (NoExternals && !okExternals.count(function->getName())) {
2656 0: llvm::cerr << "KLEE:ERROR: Calling not-OK external function : " << function->getName() << "\n";
2657 0: terminateStateOnError(state, "externals disallowed", "user.err");
2658 : return;
2659 : }
2660 :
2661 : // normal external function handling path
2662 288: uint64_t *args = (uint64_t*) alloca(sizeof(*args) * (arguments.size() + 1));
2663 288: memset(args, 0, sizeof(*args) * (arguments.size() + 1));
2664 :
2665 288: unsigned i = 1;
643: branch 0 taken
288: branch 1 taken
2666 1862: for (std::vector<ref<Expr> >::iterator ai = arguments.begin(), ae = arguments.end();
2667 : ai!=ae; ++ai, ++i) {
144: branch 0 taken
499: branch 1 taken
2668 643: if (AllowExternalSymCalls) { // don't bother checking uniqueness
2669 : ref<Expr> ce;
2670 144: bool success = solver->getValue(state, *ai, ce);
0: branch 0 not taken
144: branch 1 taken
2671 144: assert(success && "FIXME: Unhandled solver failure");
2672 144: static_cast<ConstantExpr*>(ce.get())->toMemory((void*) &args[i]);
2673 : } else {
2674 499: ref<Expr> arg = toUnique(state, *ai);
499: branch 1 taken
0: branch 2 not taken
2675 499: if (arg.isConstant()) {
2676 : // XXX kick toMemory functions from here
2677 499: static_cast<ConstantExpr*>(arg.get())->toMemory((void*) &args[i]);
2678 : } else {
2679 0: std::string msg = "external call with symbolic argument: " + function->getName();
2680 0: terminateStateOnExecError(state, msg);
2681 0: return;
2682 499: }
2683 : }
2684 : }
2685 :
2686 288: state.addressSpace.copyOutConcretes();
2687 :
288: branch 0 taken
0: branch 1 not taken
2688 288: if (!SuppressExternalWarnings) {
2689 288: std::ostringstream os;
2690 576: os << "calling external: " << function->getName().c_str() << "(";
643: branch 0 taken
288: branch 1 taken
2691 1862: for (unsigned i=0; i<arguments.size(); i++) {
2692 643: os << arguments[i];
360: branch 0 taken
283: branch 1 taken
2693 643: if (i != arguments.size()-1)
2694 360: os << ", ";
2695 : }
2696 288: os << ")";
2697 :
0: branch 0 not taken
288: branch 1 taken
2698 288: if (AllExternalWarnings)
2699 0: klee_warning("%s", os.str().c_str());
2700 : else
2701 576: klee_warning_once(function, "%s", os.str().c_str());
2702 : }
2703 :
2704 288: bool success = externalDispatcher->executeCall(function, target->inst, args);
1: branch 0 taken
287: branch 1 taken
2705 288: if (!success) {
2706 3: terminateStateOnError(state, "failed external call: " + function->getName(), "external.err");
2707 : return;
2708 : }
2709 :
0: branch 1 not taken
287: branch 2 taken
2710 287: if (!state.addressSpace.copyInConcretes()) {
2711 0: terminateStateOnError(state, "external modified read-only object", "external.err");
2712 : return;
2713 : }
2714 :
2715 : // XXX:DRE: get best-guess referent after calling external.
2716 574: const Type *resultType = target->inst->getType();
287: branch 0 taken
0: branch 1 not taken
2717 287: if (resultType != Type::VoidTy) {
2718 574: ref<Expr> e = ConstantExpr::fromMemory((void*) args, Expr::getWidthForLLVMType(resultType));
2719 :
2720 : #ifdef KLEE_TRACK_REFERENTS
2721 : ObjectPair op(0,0);
2722 : bool success;
2723 : assert(state.addressSpace.resolveOne(state, solver, e, op, success) &&
2724 : "timeout");
2725 : if (success)
2726 : bindLocal(target, state, e, (MemoryObject*) op.first);
2727 : #else
2728 287: bindLocal(target, state, e);
2729 : #endif
2730 : }
2731 : }
2732 :
2733 : /***/
2734 :
2735 : ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state,
2736 3: ref<Expr> e) {
2737 3: unsigned n = interpreterOpts.MakeConcreteSymbolic;
3: branch 0 taken
0: branch 1 not taken
3: branch 2 taken
0: branch 3 not taken
0: branch 4 not taken
3: branch 5 taken
2738 3: if (!n || replayOut || replayPath)
2739 0: return e;
2740 :
2741 : // right now, we don't replace symbolics (is there any reason too?)
1: branch 1 taken
2: branch 2 taken
2742 3: if (!e.isConstant())
2743 1: return e;
2744 :
0: branch 0 not taken
2: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
2: branch 6 taken
2745 2: if (n != 1 && random() % n)
2746 0: return e;
2747 :
2748 : // create a new fresh location, assert it is equal to concrete value in e
2749 : // and return it.
2750 :
2751 : const MemoryObject *mo = memory->allocate(Expr::getMinBytesForWidth(e.getWidth()),
2752 : false, false,
2753 6: state.prevPC->inst);
0: branch 0 not taken
2: branch 1 taken
2754 2: assert(mo && "out of memory");
2755 2: ref<Expr> res = Expr::createTempRead(mo, e.getWidth());
2756 2: ref<Expr> eq = NotOptimizedExpr::create(EqExpr::create(e, res));
2757 : llvm::cerr << "Making symbolic: " << eq << "\n";
2758 2: state.addConstraint(eq);
2759 4: return res;
2760 : }
2761 :
2762 : ObjectState *Executor::bindObjectInState(ExecutionState &state, const MemoryObject *mo,
2763 766579: bool isLocal) {
2764 766579: ObjectState *os = new ObjectState(mo, mo->size);
2765 766579: state.addressSpace.bindObject(mo, os);
2766 :
2767 : // Its possible that multiple bindings of the same mo in the state
2768 : // will put multiple copies on this list, but it doesn't really
2769 : // matter because all we use this list for is to unbind the object
2770 : // on function return.
231001: branch 0 taken
535578: branch 1 taken
2771 766579: if (isLocal)
2772 462002: state.stack.back().allocas.push_back(mo);
2773 :
2774 766579: return os;
2775 : }
2776 :
2777 : void Executor::executeAllocN(ExecutionState &state,
2778 : uint64_t nelems,
2779 : uint64_t size,
2780 : uint64_t alignment,
2781 : bool isLocal,
2782 0: KInstruction *target) {
2783 : #if 0
2784 : // over-allocate so that we can properly align the whole buffer
2785 : uint64_t address = (uint64_t) (unsigned) malloc(nelems * size + alignment - 1);
2786 : address += (alignment - address % alignment);
2787 : #else
2788 : theMMap =
2789 : mmap((void*) 0x90000000,
2790 : nelems*size, PROT_READ|PROT_WRITE,
2791 : MAP_PRIVATE
2792 : #ifdef MAP_ANONYMOUS
2793 : |MAP_ANONYMOUS
2794 : #endif
2795 0: , 0, 0);
2796 0: uint64_t address = (uintptr_t) theMMap;
2797 0: theMMapSize = nelems*size;
2798 : #endif
2799 :
0: branch 0 not taken
0: branch 1 not taken
2800 0: for (unsigned i = 0; i < nelems; i++) {
2801 0: MemoryObject *mo = memory->allocateFixed(address + i*size, size, state.prevPC->inst);
2802 0: ObjectState *os = bindObjectInState(state, mo, isLocal);
2803 0: os->initializeToRandom();
2804 :
2805 : // bind the local to the first memory object in the whole array
0: branch 0 not taken
0: branch 1 not taken
2806 0: if (i == 0)
2807 0: bindLocal(target, state, mo->getBaseExpr(), mo);
2808 : }
2809 :
2810 : llvm::cerr << "KLEE: allocN at: " << address << "\n";
2811 0: }
2812 :
2813 : void Executor::executeAlloc(ExecutionState &state,
2814 : ref<Expr> size,
2815 : bool isLocal,
2816 : KInstruction *target,
2817 : bool zeroMemory,
2818 755460: const ObjectState *reallocFrom) {
2819 755460: size = toUnique(state, size);
755460: branch 1 taken
0: branch 2 not taken
2820 755460: if (size.isConstant()) {
2821 : MemoryObject *mo = memory->allocate(size.getConstantValue(), isLocal, false,
2822 1510920: state.prevPC->inst);
1: branch 0 taken
755459: branch 1 taken
2823 755460: if (!mo) {
2824 1: bindLocal(target, state, ref<Expr>(0, kMachinePointerType));
2825 : } else {
2826 755459: ObjectState *os = bindObjectInState(state, mo, isLocal);
0: branch 0 not taken
755459: branch 1 taken
2827 755459: if (zeroMemory) {
2828 0: os->initializeToZero();
2829 : } else {
2830 755459: os->initializeToRandom();
2831 : }
2832 755459: ref<Expr> result = mo->getBaseExpr();
2833 755459: bindLocal(target, state, result, mo);
2834 :
2: branch 0 taken
755457: branch 1 taken
2835 755459: if (reallocFrom) {
2836 4: unsigned count = std::min(reallocFrom->size, os->size);
12: branch 0 taken
2: branch 1 taken
2837 14: for (unsigned i=0; i<count; i++)
2838 12: os->write(i, reallocFrom->read8(i));
2839 2: state.addressSpace.unbindObject(reallocFrom->updates.root);
2840 755459: }
2841 : }
2842 : } else {
2843 : // XXX For now we just pick a size. Ideally we would support
2844 : // symbolic sizes fully but even if we don't it would be better to
2845 : // "smartly" pick a value, for example we could fork and pick the
2846 : // min and max values and perhaps some intermediate (reasonable
2847 : // value).
2848 : //
2849 : // It would also be nice to recognize the case when size has
2850 : // exactly two values and just fork (but we need to get rid of
2851 : // return argument first). This shows up in pcre when llvm
2852 : // collapses the size expression with a select.
2853 :
2854 : ref<Expr> example;
2855 0: bool success = solver->getValue(state, size, example);
0: branch 0 not taken
0: branch 1 not taken
2856 0: assert(success && "FIXME: Unhandled solver failure");
2857 :
2858 : // Try and start with a small example
0: branch 3 not taken
0: branch 4 not taken
2859 0: while (example.getConstantValue()>128) {
2860 : ref<Expr> tmp = ref<Expr>(example.getConstantValue() >> 1,
2861 0: example.getWidth());
2862 : bool res;
2863 0: bool success = solver->mayBeTrue(state, EqExpr::create(tmp, size), res);
0: branch 0 not taken
0: branch 1 not taken
2864 0: assert(success && "FIXME: Unhandled solver failure");
0: branch 0 not taken
0: branch 1 not taken
2865 0: if (!res)
2866 0: break;
2867 0: example = tmp;
2868 : }
2869 :
2870 0: StatePair fixedSize = fork(state, EqExpr::create(example, size), true);
2871 :
0: branch 0 not taken
0: branch 1 not taken
2872 0: if (fixedSize.second) {
2873 : // Check for exactly two values
2874 : ref<Expr> tmp;
2875 0: bool success = solver->getValue(*fixedSize.second, size, tmp);
0: branch 0 not taken
0: branch 1 not taken
2876 0: assert(success && "FIXME: Unhandled solver failure");
2877 : bool res;
2878 : success = solver->mustBeTrue(*fixedSize.second,
2879 : EqExpr::create(tmp, size),
2880 0: res);
0: branch 0 not taken
0: branch 1 not taken
2881 0: assert(success && "FIXME: Unhandled solver failure");
0: branch 0 not taken
0: branch 1 not taken
2882 0: if (res) {
2883 : executeAlloc(*fixedSize.second, tmp, isLocal,
2884 0: target, zeroMemory, reallocFrom);
2885 : } else {
2886 : // See if a *really* big value is possible. If so assume
2887 : // malloc will fail for it, so lets fork and return 0.
2888 : StatePair hugeSize = fork(*fixedSize.second,
2889 : UltExpr::create(ref<Expr>(1<<31, Expr::Int32), size),
2890 0: true);
0: branch 0 not taken
0: branch 1 not taken
2891 0: if (hugeSize.first) {
2892 0: klee_message("NOTE: found huge malloc, returing 0");
2893 0: bindLocal(target, *hugeSize.first, ref<Expr>(0,kMachinePointerType));
2894 : }
2895 :
0: branch 0 not taken
0: branch 1 not taken
2896 0: if (hugeSize.second) {
2897 0: std::ostringstream info;
2898 0: ExprPPrinter::printOne(info, " size expr", size);
2899 0: info << " concretization : " << example << "\n";
2900 0: info << " unbound example: " << tmp << "\n";
2901 : terminateStateOnError(*hugeSize.second,
2902 : "concretized symbolic size",
2903 : "model.err",
2904 0: info.str());
2905 : }
2906 0: }
2907 : }
2908 :
0: branch 0 not taken
0: branch 1 not taken
2909 0: if (fixedSize.first) // can be zero when fork fails
2910 : executeAlloc(*fixedSize.first, example, isLocal,
2911 0: target, zeroMemory, reallocFrom);
2912 : }
2913 755460: }
2914 :
2915 : void Executor::executeFree(ExecutionState &state,
2916 : ref<Expr> address,
2917 35: KInstruction *target) {
2918 35: StatePair zeroPointer = fork(state, Expr::createIsZero(address), true);
7: branch 0 taken
28: branch 1 taken
2919 35: if (zeroPointer.first) {
1: branch 0 taken
6: branch 1 taken
2920 7: if (target)
2921 1: bindLocal(target, *zeroPointer.first, Expr::createPointer(0));
2922 : }
31: branch 0 taken
4: branch 1 taken
2923 35: if (zeroPointer.second) { // address != 0
2924 : ExactResolutionList rl;
2925 62: resolveExact(*zeroPointer.second, address, rl, "free");
2926 :
33: branch 0 taken
31: branch 1 taken
2927 95: foreach(it, rl.begin(), rl.end()) {
2928 33: const MemoryObject *mo = it->first.first;
1: branch 0 taken
32: branch 1 taken
2929 33: if (mo->isLocal) {
2930 : terminateStateOnError(*it->second,
2931 : "free of alloca",
2932 : "free.err",
2933 6: getAddressInfo(*it->second, address));
1: branch 0 taken
31: branch 1 taken
2934 32: } else if (mo->isGlobal) {
2935 : terminateStateOnError(*it->second,
2936 : "free of global",
2937 : "free.err",
2938 6: getAddressInfo(*it->second, address));
2939 : } else {
2940 31: it->second->addressSpace.unbindObject(mo);
2: branch 0 taken
29: branch 1 taken
2941 31: if (target)
2942 4: bindLocal(target, *it->second, Expr::createPointer(0));
2943 : }
2944 : }
2945 : }
2946 35: }
2947 :
2948 : void Executor::resolveExact(ExecutionState &state,
2949 : ref<Expr> p,
2950 : ExactResolutionList &results,
2951 127: const std::string &name) {
2952 : // XXX we may want to be capping this?
2953 : ResolutionList rl;
2954 127: state.addressSpace.resolve(state, solver, p, rl);
2955 :
2956 127: ExecutionState *unbound = &state;
130: branch 2 taken
3: branch 3 taken
2957 390: foreach(it, rl.begin(), rl.end()) {
2958 130: ref<Expr> inBounds = EqExpr::create(p, it->first->getBaseExpr());
2959 :
2960 130: StatePair branches = fork(*unbound, inBounds, true);
2961 :
130: branch 0 taken
0: branch 1 not taken
2962 130: if (branches.first)
2963 260: results.push_back(std::make_pair(*it, branches.first));
2964 :
2965 130: unbound = branches.second;
6: branch 0 taken
124: branch 1 taken
2966 130: if (!unbound) // Fork failure
2967 124: break;
2968 : }
2969 :
3: branch 0 taken
124: branch 1 taken
2970 127: if (unbound) {
2971 : terminateStateOnError(*unbound,
2972 : "memory error: invalid pointer: " + name,
2973 : "ptr.err",
2974 9: getAddressInfo(*unbound, p));
2975 : }
2976 127: }
2977 :
2978 : void Executor::executeMemoryOperation(ExecutionState &state,
2979 : bool isWrite,
2980 : ref<Expr> address,
2981 : MemoryObject *addressReferent,
2982 : ref<Expr> value /* undef if read */,
2983 : MemoryObject *valueReferent,
2984 3405920: KInstruction *target /* undef if write */) {
2985 : Expr::Width type = (isWrite ? value.getWidth() :
1268878: branch 0 taken
2137042: branch 1 taken
2986 5542962: Expr::getWidthForLLVMType(target->inst->getType()));
2987 3405920: unsigned bytes = Expr::getMinBytesForWidth(type);
2988 :
0: branch 0 not taken
3405920: branch 1 taken
2989 3405920: if (SimplifySymIndices) {
0: branch 1 not taken
0: branch 2 not taken
2990 0: if (!address.isConstant())
2991 0: address = state.constraints.simplifyExpr(address);
0: branch 0 not taken
0: branch 1 not taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 6 not taken
2992 0: if (isWrite && !value.isConstant())
2993 0: value = state.constraints.simplifyExpr(value);
2994 : }
2995 :
2996 : // fast path: single in-bounds resolution
2997 : ObjectPair op;
2998 : bool success;
2999 3405920: solver->setTimeout(stpTimeout);
0: branch 2 not taken
3405920: branch 3 taken
3000 3405920: if (!state.addressSpace.resolveOne(state, solver, address, op, success)) {
3001 0: address = toConstant(state, address, "resolveOne failure");
3002 0: success = state.addressSpace.resolveOne(address.getConstantValue(), op);
3003 : }
3004 3405920: solver->setTimeout(0);
3005 :
3405911: branch 0 taken
9: branch 1 taken
3006 3405920: if (success) {
3007 3405911: const MemoryObject *mo = op.first;
3008 :
0: branch 0 not taken
3405911: branch 1 taken
3405911: branch 2 taken
3405911: branch 3 taken
0: branch 4 not taken
3405911: branch 5 taken
3009 3405911: if (MaxSymArraySize && mo->size>=MaxSymArraySize) {
3010 0: address = toConstant(state, address, "max-sym-array-size");
3011 : }
3012 :
3013 3405911: ref<Expr> offset = mo->getOffsetExpr(address);
3014 :
3015 : bool inBounds;
3016 3405911: solver->setTimeout(stpTimeout);
3017 : bool success = solver->mustBeTrue(state,
3018 : mo->getBoundsCheckOffset(offset, bytes),
3019 3405911: inBounds);
3020 3405911: solver->setTimeout(0);
0: branch 0 not taken
3405911: branch 1 taken
3021 3405911: if (!success) {
3022 0: state.pc = state.prevPC;
3023 0: terminateStateEarly(state, "query timed out");
3024 3405906: return;
3025 : }
3026 :
3405906: branch 0 taken
5: branch 1 taken
3027 3405911: if (inBounds) {
3028 : #ifdef KLEE_TRACK_REFERENTS
3029 : // DRE: referent if we are working correctly, for non-errors mo should
3030 : // always be the same as addressReferent
3031 : if (addressReferent != op.first) {
3032 : const InstructionInfo &ii = *state.pc->info;
3033 : llvm::cerr << "XXX:" << ii.file << ":" << ii.line
3034 : << ": no referent for "
3035 : << std::hex << address << std::dec
3036 : << "inst=" << *state.prevPC->inst << "\n";
3037 : assert(0 && "Check this out");
3038 : }
3039 : #endif
3040 :
3041 3405906: const ObjectState *os = op.second;
1268872: branch 0 taken
2137034: branch 1 taken
3042 3405906: if (isWrite) {
0: branch 0 not taken
1268872: branch 1 taken
3043 1268872: if (os->readOnly) {
3044 : terminateStateOnError(state,
3045 : "memory error: object read only",
3046 0: "readonly.err");
3047 : } else {
3048 1268872: ObjectState *wos = state.addressSpace.getWriteable(mo, os);
3049 1268872: wos->write(offset, value);
3050 :
3051 : if (valueReferent)
3052 : writeReferent(state, wos, offset, valueReferent);
3053 : }
3054 : } else {
3055 2137034: ref<Expr> result = os->read(offset, type);
3056 :
3057 2137034: MemoryObject *referent = 0;
3058 : #ifdef KLEE_TRACK_REFERENTS
3059 : if (os->referents) {
3060 : ref<Expr> r = os->referents->read(offset, kMachinePointerType);
3061 : if(!r) {
3062 : llvm::cerr << "XXX: lost referent for " << address << "\n";
3063 : assert(0 && "Check this out.");
3064 : } else {
3065 : r = solver->getValue(state, r);
3066 : assert(r.isConstant());
3067 : referent = (MemoryObject *)r.getConstantValue();
3068 : // XXX:DRE: this demand doesn't work: for a structure if we
3069 : // store a pointer in it can also store non-pointers...
3070 : // assert(referent && "lost referent?");
3071 : }
3072 : }
3073 : #endif
3074 :
3: branch 0 taken
2137031: branch 1 taken
3075 2137034: if (interpreterOpts.MakeConcreteSymbolic)
3076 3: result = replaceReadWithSymbolic(state, result);
3077 :
3078 2137034: bindLocal(target, state, result, referent);
3079 : }
3080 :
3081 : return;
3082 5: }
3083 : }
3084 :
3085 : // we are on an error path (no resolution, multiple resolution, one
3086 : // resolution with out of bounds)
3087 :
3088 : #ifdef KLEE_TRACK_REFERENTS
3089 : // If error, force it to be right.
3090 : if (!state.underConstrained) {
3091 : assert(0 && "Multiple resolution: think about.");
3092 : } else {
3093 : const MemoryObject *mo = addressReferent;
3094 : assert(mo && "Null ref?");
3095 : ref<Expr> inBounds = mo->getBoundsCheckPointer(address, bytes);
3096 :
3097 : if(solver->mustBeTrue(state, Expr::createNot(inBounds))) {
3098 : llvm::cerr << "load/store must be out of bounds for instruction: "
3099 : << *state.prevPC->inst << "\n";
3100 : terminateStateOnError(state,
3101 : "memory error: must be out of bounds",
3102 : "ptr.err");
3103 : return;
3104 : }
3105 : printFileLine(state, state.pc);
3106 : llvm::cerr << "TAINT: skipping out of bounds: adding constraint:"
3107 : << inBounds << " address=" << address
3108 : << " ref=" << mo << "\n";
3109 : addConstraint(state, inBounds);
3110 : // redo!
3111 : executeMemoryOperation(state, isWrite, address, addressReferent,
3112 : value, valueReferent, target);
3113 : return;
3114 : // XXX: FIXME
3115 : // state.addConstraint(getNoOverflowExpr(inBounds));
3116 : }
3117 : #endif
3118 :
3119 : ResolutionList rl;
3120 14: solver->setTimeout(stpTimeout);
3121 : bool incomplete = state.addressSpace.resolve(state, solver, address, rl,
3122 28: 0, stpTimeout);
3123 14: solver->setTimeout(0);
3124 :
3125 : // XXX there is some query wasteage here. who cares?
3126 14: ExecutionState *unbound = &state;
3127 :
11: branch 2 taken
12: branch 3 taken
3128 48: foreach (i, rl.begin(), rl.end()) {
3129 11: const MemoryObject *mo = i->first;
3130 11: const ObjectState *os = i->second;
3131 11: ref<Expr> inBounds = mo->getBoundsCheckPointer(address, bytes);
3132 :
3133 11: StatePair branches = fork(*unbound, inBounds, true);
3134 11: ExecutionState *bound = branches.first;
3135 :
3136 : // bound can be 0 on failure or overlapped
11: branch 0 taken
0: branch 1 not taken
3137 11: if (bound) {
7: branch 0 taken
4: branch 1 taken
3138 11: if (isWrite) {
0: branch 0 not taken
7: branch 1 taken
3139 7: if (os->readOnly) {
3140 : terminateStateOnError(*bound,
3141 : "memory error: object read only",
3142 0: "readonly.err");
3143 : } else {
3144 7: ObjectState *wos = bound->addressSpace.getWriteable(mo, os);
3145 7: wos->write(mo->getOffsetExpr(address), value);
3146 : }
3147 : } else {
3148 4: ref<Expr> result = os->read(mo->getOffsetExpr(address), type);
3149 4: bindLocal(target, *bound, result);
3150 : }
3151 : }
3152 :
3153 11: unbound = branches.second;
9: branch 0 taken
2: branch 1 taken
3154 11: if (!unbound)
3155 2: break;
3156 : }
3157 :
3158 : // XXX should we distinguish out of bounds and overlapped cases?
12: branch 0 taken
2: branch 1 taken
3159 14: if (unbound) {
0: branch 0 not taken
12: branch 1 taken
3160 12: if (incomplete) {
3161 0: terminateStateEarly(*unbound, "query timed out (resolve)");
3162 : } else {
3163 : terminateStateOnError(*unbound,
3164 : "memory error: out of bound pointer",
3165 : "ptr.err",
3166 60: getAddressInfo(*unbound, address));
3167 : }
3168 : }
3169 : }
3170 :
3171 91: void Executor::executeMakeSymbolic(ExecutionState &state, const MemoryObject *mo) {
3172 : // make a new one and rebind, we use bind here because we want to
3173 : // create a flat out new state, not a copy. although I'm not really
3174 : // sure it matters.
3175 91: ObjectState *os = bindObjectInState(state, mo, false);
90: branch 0 taken
1: branch 1 taken
3176 91: if (!replayOut) {
3177 90: os->makeSymbolic();
3178 90: state.addSymbolic(mo);
3179 :
3180 90: let(it, seedMap.find(&state));
4: branch 0 taken
86: branch 1 taken
3181 180: if (it!=seedMap.end()) { // In seed mode we need to add this as a
3182 : // binding.
4: branch 0 taken
4: branch 1 taken
3183 20: foreach(siit, it->second.begin(), it->second.end()) {
3184 4: SeedInfo &si = *siit;
3185 : BOutObject *obj = si.getNextInput(mo,
3186 4: NamedSeedMatching);
3187 :
0: branch 0 not taken
4: branch 1 taken
3188 4: if (!obj) {
0: branch 0 not taken
0: branch 1 not taken
3189 0: if (ZeroSeedExtension) {
3190 0: std::vector<unsigned char> &values = si.assignment.bindings[mo];
3191 0: values = std::vector<unsigned char>(mo->size, '\0');
0: branch 0 not taken
0: branch 1 not taken
3192 0: } else if (!AllowSeedExtension) {
3193 : terminateStateOnError(state,
3194 : "ran out of inputs during seeding",
3195 0: "user.err");
3196 : break;
3197 : }
3198 : } else {
0: branch 0 not taken
4: branch 1 taken
4: branch 2 taken
4: branch 3 taken
4: branch 4 taken
4: branch 5 taken
4: branch 6 taken
4: branch 7 taken
4: branch 8 taken
4: branch 9 taken
4: branch 10 taken
4: branch 11 taken
0: branch 12 not taken
4: branch 13 taken
3199 4: if (obj->numBytes != mo->size &&
3200 : ((!(AllowSeedExtension || ZeroSeedExtension)
3201 : && obj->numBytes < mo->size) ||
3202 : (!AllowSeedTruncation && obj->numBytes > mo->size))) {
3203 0: std::stringstream msg;
3204 : msg << "replace size mismatch: "
3205 : << mo->name << "[" << mo->size << "]"
3206 : << " vs " << obj->name << "[" << obj->numBytes << "]"
3207 0: << " in bout\n";
3208 :
3209 : terminateStateOnError(state,
3210 : msg.str(),
3211 0: "user.err");
3212 0: break;
3213 : } else {
3214 4: std::vector<unsigned char> &values = si.assignment.bindings[mo];
3215 : values.insert(values.begin(), obj->bytes,
3216 12: obj->bytes + std::min(obj->numBytes, mo->size));
0: branch 0 not taken
4: branch 1 taken
3217 4: if (ZeroSeedExtension) {
0: branch 0 not taken
0: branch 1 not taken
3218 0: for (unsigned i=obj->numBytes; i<mo->size; ++i)
3219 0: values.push_back('\0');
3220 : }
3221 : }
3222 : }
3223 : }
3224 : }
3225 : } else {
0: branch 0 not taken
1: branch 1 taken
3226 1: if (replayPosition >= replayOut->numObjects) {
3227 0: terminateStateOnError(state, "replay count mismatch", "user.err");
3228 : } else {
3229 1: BOutObject *obj = &replayOut->objects[replayPosition++];
0: branch 0 not taken
1: branch 1 taken
3230 1: if (obj->numBytes != mo->size) {
3231 0: terminateStateOnError(state, "replay size mismatch", "user.err");
3232 : } else {
4: branch 0 taken
1: branch 1 taken
3233 5: for (unsigned i=0; i<mo->size; i++)
3234 4: os->write8(i, obj->bytes[i]);
3235 : }
3236 : }
3237 : }
3238 91: }
3239 :
3240 : /***/
3241 :
3242 : void Executor::runFunctionAsMain(Function *f,
3243 : int argc,
3244 : char **argv,
3245 103: char **envp) {
3246 : std::vector<ref<Expr> > arguments;
3247 :
3248 : // force deterministic initialization of memory objects
3249 103: srand(1);
3250 103: srandom(1);
3251 :
3252 103: MemoryObject *argvMO = 0;
3253 :
3254 : // In order to make uclibc happy and be closer to what the system is
3255 : // doing we lay out the environments at the end of the argv array
3256 : // (both are terminated by a null). There is also a final terminating
3257 : // null that uclibc seems to expect, possibly the ELF header?
3258 :
3259 : int envc;
5768: branch 0 taken
103: branch 1 taken
3260 103: for (envc=0; envp[envc]; ++envc) ;
3261 :
3262 103: KFunction *kf = kmodule->functionMap[f];
0: branch 0 not taken
103: branch 1 taken
3263 103: assert(kf);
3264 206: Function::arg_iterator ai = f->arg_begin(), ae = f->arg_end();
39: branch 0 taken
64: branch 1 taken
3265 103: if (ai!=ae) {
3266 78: arguments.push_back(ref<Expr>(argc, Expr::Int32));
3267 :
36: branch 1 taken
3: branch 2 taken
3268 78: if (++ai!=ae) {
3269 : argvMO = memory->allocate((argc+1+envc+1+1) * kMachinePointerSize, false, true,
3270 72: f->begin()->begin());
3271 :
3272 36: arguments.push_back(argvMO->getBaseExpr());
3273 :
1: branch 1 taken
35: branch 2 taken
3274 72: if (++ai!=ae) {
3275 1: uint64_t envp_start = argvMO->address + (argc+1)*kMachinePointerSize;
3276 1: arguments.push_back(Expr::createPointer(envp_start));
3277 :
0: branch 1 not taken
1: branch 2 taken
3278 2: if (++ai!=ae)
3279 0: klee_error("invalid main function (expect 0-3 arguments)");
3280 : }
3281 : }
3282 : }
3283 :
3284 103: ExecutionState *state = new ExecutionState(kmodule->functionMap[f]);
3285 :
0: branch 0 not taken
103: branch 1 taken
3286 103: if (pathWriter)
3287 0: state->pathOS = pathWriter->open();
0: branch 0 not taken
103: branch 1 taken
3288 103: if (symPathWriter)
3289 0: state->symPathOS = symPathWriter->open();
3290 :
3291 :
103: branch 0 taken
0: branch 1 not taken
3292 103: if (statsTracker)
3293 103: statsTracker->framePushed(*state, 0);
3294 :
0: branch 1 not taken
103: branch 2 taken
3295 103: assert(arguments.size() == f->arg_size() && "wrong number of arguments");
3296 103: unsigned i=0;
76: branch 1 taken
103: branch 2 taken
3297 564: foreach(ai, f->arg_begin(), f->arg_end()) {
3298 : #ifdef KLEE_TRACK_REFERENTS
3299 : if (arguments[i] == argvMO->getBaseExpr())
3300 : bindArgument(kf, i, *state, arguments[i], argvMO);
3301 : else
3302 : bindArgument(kf, i, *state, arguments[i]);
3303 : #else
3304 76: bindArgument(kf, i, *state, arguments[i]);
3305 : #endif
3306 76: ++i;
3307 : }
3308 :
36: branch 0 taken
67: branch 1 taken
3309 103: if (argvMO) {
3310 36: ObjectState *argvOS = bindObjectInState(*state, argvMO, false);
3311 :
2169: branch 0 taken
36: branch 1 taken
3312 2205: for (int i=0; i<argc+1+envc+1+1; i++) {
3313 : MemoryObject *arg;
3314 :
2133: branch 0 taken
36: branch 1 taken
72: branch 2 taken
2061: branch 3 taken
3315 2277: if (i==argc || i>=argc+1+envc) {
3316 108: arg = 0;
3317 : } else {
45: branch 0 taken
2016: branch 1 taken
3318 2061: char *s = i<argc ? argv[i] : envp[i-(argc+1)];
3319 2061: int j, len = strlen(s);
3320 :
3321 4122: arg = memory->allocate(len+1, false, true, state->pc->inst);
3322 2061: ObjectState *os = bindObjectInState(*state, arg, false);
139877: branch 0 taken
2061: branch 1 taken
3323 141938: for (j=0; j<len+1; j++)
3324 139877: os->write8(j, s[j]);
3325 : }
3326 :
2061: branch 0 taken
108: branch 1 taken
3327 2169: if (arg) {
3328 2061: argvOS->write(i * kMachinePointerSize, arg->getBaseExpr());
3329 : #ifdef KLEE_TRACK_REFERENTS
3330 : writeReferent(*state, argvOS,
3331 : ConstantExpr::create(i*kMachinePointerSize,Expr::Int32),arg);
3332 : #endif
3333 : } else {
3334 108: argvOS->write(i * kMachinePointerSize, Expr::createPointer(0));
3335 : #ifdef KLEE_TRACK_REFERENTS
3336 : writeReferent(*state, argvOS,
3337 : ConstantExpr::create(i*kMachinePointerSize,Expr::Int32), 0);
3338 : #endif
3339 : }
3340 : }
3341 : }
3342 :
3343 103: initializeGlobals(*state);
3344 :
3345 103: processTree = new PTree(state);
3346 103: state->ptreeNode = processTree->root;
3347 103: run(*state);
103: branch 0 taken
0: branch 1 not taken
3348 103: delete processTree;
3349 103: processTree = 0;
3350 :
3351 : // hack to clear memory objects
103: branch 0 taken
0: branch 1 not taken
3352 103: delete memory;
3353 206: memory = new MemoryManager();
3354 :
3355 103: globalObjects.clear();
3356 103: globalAddresses.clear();
3357 :
103: branch 0 taken
0: branch 1 not taken
3358 103: if (statsTracker)
3359 103: statsTracker->done();
3360 :
0: branch 0 not taken
103: branch 1 taken
3361 103: if (theMMap) {
3362 0: munmap(theMMap, theMMapSize);
3363 0: theMMap = 0;
3364 103: }
3365 103: }
3366 :
3367 0: unsigned Executor::getPathStreamID(const ExecutionState &state) {
0: branch 0 not taken
0: branch 1 not taken
3368 0: assert(pathWriter);
3369 0: return state.pathOS.getID();
3370 : }
3371 :
3372 0: unsigned Executor::getSymbolicPathStreamID(const ExecutionState &state) {
0: branch 0 not taken
0: branch 1 not taken
3373 0: assert(symPathWriter);
3374 0: return state.symPathOS.getID();
3375 : }
3376 :
3377 : void Executor::getConstraintLog(const ExecutionState &state,
3378 : std::string &res,
3379 30: bool asCVC) {
1: branch 0 taken
29: branch 1 taken
3380 30: if (asCVC) {
3381 2: Query query(state.constraints, ref<Expr>(0, Expr::Bool));
3382 1: char *log = solver->stpSolver->getConstraintLog(query);
3383 2: res = std::string(log);
3384 1: free(log);
3385 : } else {
3386 29: std::ostringstream info;
3387 29: ExprPPrinter::printConstraints(info, state.constraints);
3388 58: res = info.str();
3389 : }
3390 30: }
3391 :
3392 : bool Executor::getSymbolicSolution(const ExecutionState &state,
3393 : std::vector<
3394 : std::pair<std::string,
3395 : std::vector<unsigned char> > >
3396 663: &res) {
3397 663: solver->setTimeout(stpTimeout);
3398 :
3399 663: ExecutionState tmp(state);
663: branch 0 taken
0: branch 1 not taken
3400 663: if (!NoPreferCex) {
845: branch 0 taken
663: branch 1 taken
3401 2834: foreach(oi, state.symbolics.begin(), state.symbolics.end()) {
3402 845: const MemoryObject *mo = *oi;
3403 845: let(pi, mo->cexPreferences.begin());
3404 845: let(pie, mo->cexPreferences.end());
3: branch 0 taken
845: branch 1 taken
3405 1693: for (; pi!=pie; ++pi) {
3406 : bool mustBeTrue;
3407 3: bool success = solver->mustBeTrue(tmp, Expr::createNot(*pi), mustBeTrue);
3: branch 0 taken
0: branch 1 not taken
3408 3: if (!success) break;
3: branch 0 taken
0: branch 1 not taken
3409 6: if (!mustBeTrue) tmp.addConstraint(*pi);
3410 : }
845: branch 0 taken
0: branch 1 not taken
3411 845: if (pi!=pie) break;
3412 : }
3413 : }
3414 :
3415 : std::vector< std::vector<unsigned char> > values;
3416 663: bool success = solver->getInitialValues(tmp, state.symbolics, values);
3417 663: solver->setTimeout(0);
0: branch 0 not taken
663: branch 1 taken
3418 663: if (!success) {
3419 0: klee_warning("unable to compute initial values (invalid constraints?)!");
3420 : ExprPPrinter::printQuery(std::cerr,
3421 : state.constraints,
3422 0: ref<Expr>(0,Expr::Bool));
3423 0: return false;
3424 : }
3425 :
3426 : let(vi, values.begin());
845: branch 0 taken
663: branch 1 taken
3427 3497: foreach(oi, state.symbolics.begin(), state.symbolics.end()) {
3428 2535: res.push_back(std::make_pair((*oi)->name, *vi));
3429 : ++vi;
3430 : }
3431 1326: return true;
3432 : }
3433 :
3434 : void Executor::getCoveredLines(const ExecutionState &state,
3435 2: std::map<const std::string*, std::set<unsigned> > &res) {
3436 2: res = state.coveredLines;
3437 2: }
3438 :
3439 : void Executor::doImpliedValueConcretization(ExecutionState &state,
3440 : ref<Expr> e,
3441 0: ref<Expr> value) {
0: branch 1 not taken
0: branch 2 not taken
3442 0: assert(value.isConstant() && "non-constant passed in place of constant");
3443 :
0: branch 0 not taken
0: branch 1 not taken
3444 0: if (DebugCheckForImpliedValues)
3445 0: ImpliedValue::checkForImpliedValues(solver->solver, e, value);
3446 :
3447 : ImpliedValueList results;
3448 0: ImpliedValue::getImpliedValues(e, value, results);
0: branch 0 not taken
0: branch 1 not taken
3449 0: foreach(it, results.begin(), results.end()) {
3450 0: ReadExpr *re = it->first.get();
3451 :
0: branch 1 not taken
0: branch 2 not taken
3452 0: if (re->index.isConstant()) {
3453 0: const MemoryObject *mo = re->updates.root;
3454 0: const ObjectState *os = state.addressSpace.findObject(mo);
3455 :
0: branch 0 not taken
0: branch 1 not taken
3456 0: if (!os) {
3457 : // object has been free'd, no need to concretize (although as
3458 : // in other cases we would like to concretize the outstanding
3459 : // reads, but we have no facility for that yet)
3460 : } else {
0: branch 0 not taken
0: branch 1 not taken
3461 0: assert(!os->readOnly && "not possible? read only object with static read?");
3462 0: ObjectState *wos = state.addressSpace.getWriteable(mo, os);
3463 0: wos->write(re->index.getConstantValue(), it->second);
3464 : }
3465 : }
3466 : }
3467 0: }
3468 :
3469 : ///
3470 :
3471 : Interpreter *Interpreter::create(const InterpreterOptions &opts,
3472 103: InterpreterHandler *ih) {
3473 103: return new Executor(opts, ih);
103: branch 0 taken
0: branch 1 not taken
103: branch 2 taken
0: branch 3 not taken
3474 309: }
Generated: 2009-05-17 22:47 by zcov