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