klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
SpecialFunctionHandler.cpp
Go to the documentation of this file.
1 //===-- SpecialFunctionHandler.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 "Memory.h"
13 #include "SpecialFunctionHandler.h"
14 #include "TimingSolver.h"
15 
16 #include "klee/ExecutionState.h"
17 
20 
21 #include "Executor.h"
22 #include "MemoryManager.h"
23 
24 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
25 #include "llvm/IR/Module.h"
26 #else
27 #include "llvm/Module.h"
28 #endif
29 #include "llvm/ADT/Twine.h"
30 #include "llvm/Support/Debug.h"
31 
32 #include <errno.h>
33 
34 using namespace llvm;
35 using namespace klee;
36 
39 
41 
42 
43 
44 // FIXME: We are more or less committed to requiring an intrinsic
45 // library these days. We can move some of this stuff there,
46 // especially things like realloc which have complicated semantics
47 // w.r.t. forking. Among other things this makes delayed query
48 // dispatch easier to implement.
50 #define add(name, handler, ret) { name, \
51  &SpecialFunctionHandler::handler, \
52  false, ret, false }
53 #define addDNR(name, handler) { name, \
54  &SpecialFunctionHandler::handler, \
55  true, false, false }
56  addDNR("__assert_rtn", handleAssertFail),
57  addDNR("__assert_fail", handleAssertFail),
58  addDNR("_assert", handleAssert),
59  addDNR("abort", handleAbort),
60  addDNR("_exit", handleExit),
61  { "exit", &SpecialFunctionHandler::handleExit, true, false, true },
62  addDNR("klee_abort", handleAbort),
63  addDNR("klee_silent_exit", handleSilentExit),
64  addDNR("klee_report_error", handleReportError),
65 
66  add("calloc", handleCalloc, true),
67  add("free", handleFree, false),
68  add("klee_assume", handleAssume, false),
69  add("klee_check_memory_access", handleCheckMemoryAccess, false),
70  add("klee_get_valuef", handleGetValue, true),
71  add("klee_get_valued", handleGetValue, true),
72  add("klee_get_valuel", handleGetValue, true),
73  add("klee_get_valuell", handleGetValue, true),
74  add("klee_get_value_i32", handleGetValue, true),
75  add("klee_get_value_i64", handleGetValue, true),
76  add("klee_define_fixed_object", handleDefineFixedObject, false),
77  add("klee_get_obj_size", handleGetObjSize, true),
78  add("klee_get_errno", handleGetErrno, true),
79  add("klee_is_symbolic", handleIsSymbolic, true),
80  add("klee_make_symbolic", handleMakeSymbolic, false),
81  add("klee_mark_global", handleMarkGlobal, false),
82  add("klee_merge", handleMerge, false),
83  add("klee_prefer_cex", handlePreferCex, false),
84  add("klee_print_expr", handlePrintExpr, false),
85  add("klee_print_range", handlePrintRange, false),
86  add("klee_set_forking", handleSetForking, false),
87  add("klee_stack_trace", handleStackTrace, false),
88  add("klee_warning", handleWarning, false),
89  add("klee_warning_once", handleWarningOnce, false),
90  add("klee_alias_function", handleAliasFunction, false),
91  add("malloc", handleMalloc, true),
92  add("realloc", handleRealloc, true),
93 
94  // operator delete[](void*)
95  add("_ZdaPv", handleDeleteArray, false),
96  // operator delete(void*)
97  add("_ZdlPv", handleDelete, false),
98 
99  // operator new[](unsigned int)
100  add("_Znaj", handleNewArray, true),
101  // operator new(unsigned int)
102  add("_Znwj", handleNew, true),
103 
104  // FIXME-64: This is wrong for 64-bit long...
105 
106  // operator new[](unsigned long)
107  add("_Znam", handleNewArray, true),
108  // operator new(unsigned long)
109  add("_Znwm", handleNew, true),
110 
111 #undef addDNR
112 #undef add
113 };
114 
115 SpecialFunctionHandler::const_iterator SpecialFunctionHandler::begin() {
117 }
118 
119 SpecialFunctionHandler::const_iterator SpecialFunctionHandler::end() {
120  // NULL pointer is sentinel
122 }
123 
124 SpecialFunctionHandler::const_iterator& SpecialFunctionHandler::const_iterator::operator++() {
125  ++index;
126  if ( index >= SpecialFunctionHandler::size())
127  {
128  // Out of range, return .end()
129  base=0; // Sentinel
130  index=0;
131  }
132 
133  return *this;
134 }
135 
136 int SpecialFunctionHandler::size() {
137  return sizeof(handlerInfo)/sizeof(handlerInfo[0]);
138 }
139 
140 SpecialFunctionHandler::SpecialFunctionHandler(Executor &_executor)
141  : executor(_executor) {}
142 
143 
145  unsigned N = size();
146 
147  for (unsigned i=0; i<N; ++i) {
148  HandlerInfo &hi = handlerInfo[i];
149  Function *f = executor.kmodule->module->getFunction(hi.name);
150 
151  // No need to create if the function doesn't exist, since it cannot
152  // be called in that case.
153 
154  if (f && (!hi.doNotOverride || f->isDeclaration())) {
155  // Make sure NoReturn attribute is set, for optimization and
156  // coverage counting.
157  if (hi.doesNotReturn)
158 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
159  f->addFnAttr(Attribute::NoReturn);
160 #elif LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
161  f->addFnAttr(Attributes::NoReturn);
162 #else
163  f->addFnAttr(Attribute::NoReturn);
164 #endif
165 
166  // Change to a declaration since we handle internally (simplifies
167  // module and allows deleting dead code).
168  if (!f->isDeclaration())
169  f->deleteBody();
170  }
171  }
172 }
173 
175  unsigned N = sizeof(handlerInfo)/sizeof(handlerInfo[0]);
176 
177  for (unsigned i=0; i<N; ++i) {
178  HandlerInfo &hi = handlerInfo[i];
179  Function *f = executor.kmodule->module->getFunction(hi.name);
180 
181  if (f && (!hi.doNotOverride || f->isDeclaration()))
182  handlers[f] = std::make_pair(hi.handler, hi.hasReturnValue);
183  }
184 }
185 
186 
188  Function *f,
189  KInstruction *target,
190  std::vector< ref<Expr> > &arguments) {
191  handlers_ty::iterator it = handlers.find(f);
192  if (it != handlers.end()) {
193  Handler h = it->second.first;
194  bool hasReturnValue = it->second.second;
195  // FIXME: Check this... add test?
196  if (!hasReturnValue && !target->inst->use_empty()) {
198  "expected return value from void special function");
199  } else {
200  (this->*h)(state, target, arguments);
201  }
202  return true;
203  } else {
204  return false;
205  }
206 }
207 
208 /****/
209 
210 // reads a concrete string from memory
211 std::string
213  ref<Expr> addressExpr) {
214  ObjectPair op;
215  addressExpr = executor.toUnique(state, addressExpr);
216  ref<ConstantExpr> address = cast<ConstantExpr>(addressExpr);
217  if (!state.addressSpace.resolveOne(address, op))
218  assert(0 && "XXX out of bounds / multiple resolution unhandled");
219  bool res;
220  assert(executor.solver->mustBeTrue(state,
221  EqExpr::create(address,
222  op.first->getBaseExpr()),
223  res) &&
224  res &&
225  "XXX interior pointer unhandled");
226  const MemoryObject *mo = op.first;
227  const ObjectState *os = op.second;
228 
229  char *buf = new char[mo->size];
230 
231  unsigned i;
232  for (i = 0; i < mo->size - 1; i++) {
233  ref<Expr> cur = os->read8(i);
234  cur = executor.toUnique(state, cur);
235  assert(isa<ConstantExpr>(cur) &&
236  "hit symbolic char while reading concrete string");
237  buf[i] = cast<ConstantExpr>(cur)->getZExtValue(8);
238  }
239  buf[i] = 0;
240 
241  std::string result(buf);
242  delete[] buf;
243  return result;
244 }
245 
246 /****/
247 
248 void SpecialFunctionHandler::handleAbort(ExecutionState &state,
249  KInstruction *target,
250  std::vector<ref<Expr> > &arguments) {
251  assert(arguments.size()==0 && "invalid number of arguments to abort");
252 
253  //XXX:DRE:TAINT
254  if(state.underConstrained) {
255  llvm::errs() << "TAINT: skipping abort fail\n";
256  executor.terminateState(state);
257  } else {
258  executor.terminateStateOnError(state, "abort failure", "abort.err");
259  }
260 }
261 
262 void SpecialFunctionHandler::handleExit(ExecutionState &state,
263  KInstruction *target,
264  std::vector<ref<Expr> > &arguments) {
265  assert(arguments.size()==1 && "invalid number of arguments to exit");
267 }
268 
269 void SpecialFunctionHandler::handleSilentExit(ExecutionState &state,
270  KInstruction *target,
271  std::vector<ref<Expr> > &arguments) {
272  assert(arguments.size()==1 && "invalid number of arguments to exit");
273  executor.terminateState(state);
274 }
275 
276 void SpecialFunctionHandler::handleAliasFunction(ExecutionState &state,
277  KInstruction *target,
278  std::vector<ref<Expr> > &arguments) {
279  assert(arguments.size()==2 &&
280  "invalid number of arguments to klee_alias_function");
281  std::string old_fn = readStringAtAddress(state, arguments[0]);
282  std::string new_fn = readStringAtAddress(state, arguments[1]);
283  DEBUG_WITH_TYPE("alias_handling", llvm::errs() << "Replacing " << old_fn
284  << "() with " << new_fn << "()\n");
285  if (old_fn == new_fn)
286  state.removeFnAlias(old_fn);
287  else state.addFnAlias(old_fn, new_fn);
288 }
289 
290 void SpecialFunctionHandler::handleAssert(ExecutionState &state,
291  KInstruction *target,
292  std::vector<ref<Expr> > &arguments) {
293  assert(arguments.size()==3 && "invalid number of arguments to _assert");
294 
295  //XXX:DRE:TAINT
296  if(state.underConstrained) {
297  llvm::errs() << "TAINT: skipping assertion:"
298  << readStringAtAddress(state, arguments[0]) << "\n";
299  executor.terminateState(state);
300  } else
302  "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]),
303  "assert.err");
304 }
305 
306 void SpecialFunctionHandler::handleAssertFail(ExecutionState &state,
307  KInstruction *target,
308  std::vector<ref<Expr> > &arguments) {
309  assert(arguments.size()==4 && "invalid number of arguments to __assert_fail");
310 
311  //XXX:DRE:TAINT
312  if(state.underConstrained) {
313  llvm::errs() << "TAINT: skipping assertion:"
314  << readStringAtAddress(state, arguments[0]) << "\n";
315  executor.terminateState(state);
316  } else
318  "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]),
319  "assert.err");
320 }
321 
322 void SpecialFunctionHandler::handleReportError(ExecutionState &state,
323  KInstruction *target,
324  std::vector<ref<Expr> > &arguments) {
325  assert(arguments.size()==4 && "invalid number of arguments to klee_report_error");
326 
327  // arguments[0], arguments[1] are file, line
328 
329  //XXX:DRE:TAINT
330  if(state.underConstrained) {
331  llvm::errs() << "TAINT: skipping klee_report_error:"
332  << readStringAtAddress(state, arguments[2]) << ":"
333  << readStringAtAddress(state, arguments[3]) << "\n";
334  executor.terminateState(state);
335  } else
337  readStringAtAddress(state, arguments[2]),
338  readStringAtAddress(state, arguments[3]).c_str());
339 }
340 
341 void SpecialFunctionHandler::handleMerge(ExecutionState &state,
342  KInstruction *target,
343  std::vector<ref<Expr> > &arguments) {
344  // nop
345 }
346 
347 void SpecialFunctionHandler::handleNew(ExecutionState &state,
348  KInstruction *target,
349  std::vector<ref<Expr> > &arguments) {
350  // XXX should type check args
351  assert(arguments.size()==1 && "invalid number of arguments to new");
352 
353  executor.executeAlloc(state, arguments[0], false, target);
354 }
355 
356 void SpecialFunctionHandler::handleDelete(ExecutionState &state,
357  KInstruction *target,
358  std::vector<ref<Expr> > &arguments) {
359  // FIXME: Should check proper pairing with allocation type (malloc/free,
360  // new/delete, new[]/delete[]).
361 
362  // XXX should type check args
363  assert(arguments.size()==1 && "invalid number of arguments to delete");
364  executor.executeFree(state, arguments[0]);
365 }
366 
367 void SpecialFunctionHandler::handleNewArray(ExecutionState &state,
368  KInstruction *target,
369  std::vector<ref<Expr> > &arguments) {
370  // XXX should type check args
371  assert(arguments.size()==1 && "invalid number of arguments to new[]");
372  executor.executeAlloc(state, arguments[0], false, target);
373 }
374 
375 void SpecialFunctionHandler::handleDeleteArray(ExecutionState &state,
376  KInstruction *target,
377  std::vector<ref<Expr> > &arguments) {
378  // XXX should type check args
379  assert(arguments.size()==1 && "invalid number of arguments to delete[]");
380  executor.executeFree(state, arguments[0]);
381 }
382 
383 void SpecialFunctionHandler::handleMalloc(ExecutionState &state,
384  KInstruction *target,
385  std::vector<ref<Expr> > &arguments) {
386  // XXX should type check args
387  assert(arguments.size()==1 && "invalid number of arguments to malloc");
388  executor.executeAlloc(state, arguments[0], false, target);
389 }
390 
391 void SpecialFunctionHandler::handleAssume(ExecutionState &state,
392  KInstruction *target,
393  std::vector<ref<Expr> > &arguments) {
394  assert(arguments.size()==1 && "invalid number of arguments to klee_assume");
395 
396  ref<Expr> e = arguments[0];
397 
398  if (e->getWidth() != Expr::Bool)
399  e = NeExpr::create(e, ConstantExpr::create(0, e->getWidth()));
400 
401  bool res;
402  bool success = executor.solver->mustBeFalse(state, e, res);
403  assert(success && "FIXME: Unhandled solver failure");
404  if (res) {
406  "invalid klee_assume call (provably false)",
407  "user.err");
408  } else {
409  executor.addConstraint(state, e);
410  }
411 }
412 
413 void SpecialFunctionHandler::handleIsSymbolic(ExecutionState &state,
414  KInstruction *target,
415  std::vector<ref<Expr> > &arguments) {
416  assert(arguments.size()==1 && "invalid number of arguments to klee_is_symbolic");
417 
418  executor.bindLocal(target, state,
419  ConstantExpr::create(!isa<ConstantExpr>(arguments[0]),
420  Expr::Int32));
421 }
422 
423 void SpecialFunctionHandler::handlePreferCex(ExecutionState &state,
424  KInstruction *target,
425  std::vector<ref<Expr> > &arguments) {
426  assert(arguments.size()==2 &&
427  "invalid number of arguments to klee_prefex_cex");
428 
429  ref<Expr> cond = arguments[1];
430  if (cond->getWidth() != Expr::Bool)
431  cond = NeExpr::create(cond, ConstantExpr::alloc(0, cond->getWidth()));
432 
434  executor.resolveExact(state, arguments[0], rl, "prefex_cex");
435 
436  assert(rl.size() == 1 &&
437  "prefer_cex target must resolve to precisely one object");
438 
439  rl[0].first.first->cexPreferences.push_back(cond);
440 }
441 
442 void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state,
443  KInstruction *target,
444  std::vector<ref<Expr> > &arguments) {
445  assert(arguments.size()==2 &&
446  "invalid number of arguments to klee_print_expr");
447 
448  std::string msg_str = readStringAtAddress(state, arguments[0]);
449  llvm::errs() << msg_str << ":" << arguments[1] << "\n";
450 }
451 
452 void SpecialFunctionHandler::handleSetForking(ExecutionState &state,
453  KInstruction *target,
454  std::vector<ref<Expr> > &arguments) {
455  assert(arguments.size()==1 &&
456  "invalid number of arguments to klee_set_forking");
457  ref<Expr> value = executor.toUnique(state, arguments[0]);
458 
459  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
460  state.forkDisabled = CE->isZero();
461  } else {
463  "klee_set_forking requires a constant arg",
464  "user.err");
465  }
466 }
467 
468 void SpecialFunctionHandler::handleStackTrace(ExecutionState &state,
469  KInstruction *target,
470  std::vector<ref<Expr> > &arguments) {
471  state.dumpStack(outs());
472 }
473 
474 void SpecialFunctionHandler::handleWarning(ExecutionState &state,
475  KInstruction *target,
476  std::vector<ref<Expr> > &arguments) {
477  assert(arguments.size()==1 && "invalid number of arguments to klee_warning");
478 
479  std::string msg_str = readStringAtAddress(state, arguments[0]);
480  klee_warning("%s: %s", state.stack.back().kf->function->getName().data(),
481  msg_str.c_str());
482 }
483 
484 void SpecialFunctionHandler::handleWarningOnce(ExecutionState &state,
485  KInstruction *target,
486  std::vector<ref<Expr> > &arguments) {
487  assert(arguments.size()==1 &&
488  "invalid number of arguments to klee_warning_once");
489 
490  std::string msg_str = readStringAtAddress(state, arguments[0]);
491  klee_warning_once(0, "%s: %s", state.stack.back().kf->function->getName().data(),
492  msg_str.c_str());
493 }
494 
495 void SpecialFunctionHandler::handlePrintRange(ExecutionState &state,
496  KInstruction *target,
497  std::vector<ref<Expr> > &arguments) {
498  assert(arguments.size()==2 &&
499  "invalid number of arguments to klee_print_range");
500 
501  std::string msg_str = readStringAtAddress(state, arguments[0]);
502  llvm::errs() << msg_str << ":" << arguments[1];
503  if (!isa<ConstantExpr>(arguments[1])) {
504  // FIXME: Pull into a unique value method?
505  ref<ConstantExpr> value;
506  bool success = executor.solver->getValue(state, arguments[1], value);
507  assert(success && "FIXME: Unhandled solver failure");
508  bool res;
509  success = executor.solver->mustBeTrue(state,
510  EqExpr::create(arguments[1], value),
511  res);
512  assert(success && "FIXME: Unhandled solver failure");
513  if (res) {
514  llvm::errs() << " == " << value;
515  } else {
516  llvm::errs() << " ~= " << value;
517  std::pair< ref<Expr>, ref<Expr> > res =
518  executor.solver->getRange(state, arguments[1]);
519  llvm::errs() << " (in [" << res.first << ", " << res.second <<"])";
520  }
521  }
522  llvm::errs() << "\n";
523 }
524 
525 void SpecialFunctionHandler::handleGetObjSize(ExecutionState &state,
526  KInstruction *target,
527  std::vector<ref<Expr> > &arguments) {
528  // XXX should type check args
529  assert(arguments.size()==1 &&
530  "invalid number of arguments to klee_get_obj_size");
532  executor.resolveExact(state, arguments[0], rl, "klee_get_obj_size");
533  for (Executor::ExactResolutionList::iterator it = rl.begin(),
534  ie = rl.end(); it != ie; ++it) {
535  executor.bindLocal(target, *it->second,
536  ConstantExpr::create(it->first.first->size, Expr::Int32));
537  }
538 }
539 
540 void SpecialFunctionHandler::handleGetErrno(ExecutionState &state,
541  KInstruction *target,
542  std::vector<ref<Expr> > &arguments) {
543  // XXX should type check args
544  assert(arguments.size()==0 &&
545  "invalid number of arguments to klee_get_errno");
546  executor.bindLocal(target, state,
548 }
549 
550 void SpecialFunctionHandler::handleCalloc(ExecutionState &state,
551  KInstruction *target,
552  std::vector<ref<Expr> > &arguments) {
553  // XXX should type check args
554  assert(arguments.size()==2 &&
555  "invalid number of arguments to calloc");
556 
557  ref<Expr> size = MulExpr::create(arguments[0],
558  arguments[1]);
559  executor.executeAlloc(state, size, false, target, true);
560 }
561 
562 void SpecialFunctionHandler::handleRealloc(ExecutionState &state,
563  KInstruction *target,
564  std::vector<ref<Expr> > &arguments) {
565  // XXX should type check args
566  assert(arguments.size()==2 &&
567  "invalid number of arguments to realloc");
568  ref<Expr> address = arguments[0];
569  ref<Expr> size = arguments[1];
570 
571  Executor::StatePair zeroSize = executor.fork(state,
572  Expr::createIsZero(size),
573  true);
574 
575  if (zeroSize.first) { // size == 0
576  executor.executeFree(*zeroSize.first, address, target);
577  }
578  if (zeroSize.second) { // size != 0
579  Executor::StatePair zeroPointer = executor.fork(*zeroSize.second,
580  Expr::createIsZero(address),
581  true);
582 
583  if (zeroPointer.first) { // address == 0
584  executor.executeAlloc(*zeroPointer.first, size, false, target);
585  }
586  if (zeroPointer.second) { // address != 0
588  executor.resolveExact(*zeroPointer.second, address, rl, "realloc");
589 
590  for (Executor::ExactResolutionList::iterator it = rl.begin(),
591  ie = rl.end(); it != ie; ++it) {
592  executor.executeAlloc(*it->second, size, false, target, false,
593  it->first.second);
594  }
595  }
596  }
597 }
598 
599 void SpecialFunctionHandler::handleFree(ExecutionState &state,
600  KInstruction *target,
601  std::vector<ref<Expr> > &arguments) {
602  // XXX should type check args
603  assert(arguments.size()==1 &&
604  "invalid number of arguments to free");
605  executor.executeFree(state, arguments[0]);
606 }
607 
608 void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
609  KInstruction *target,
610  std::vector<ref<Expr> >
611  &arguments) {
612  assert(arguments.size()==2 &&
613  "invalid number of arguments to klee_check_memory_access");
614 
615  ref<Expr> address = executor.toUnique(state, arguments[0]);
616  ref<Expr> size = executor.toUnique(state, arguments[1]);
617  if (!isa<ConstantExpr>(address) || !isa<ConstantExpr>(size)) {
619  "check_memory_access requires constant args",
620  "user.err");
621  } else {
622  ObjectPair op;
623 
624  if (!state.addressSpace.resolveOne(cast<ConstantExpr>(address), op)) {
626  "check_memory_access: memory error",
627  "ptr.err",
628  executor.getAddressInfo(state, address));
629  } else {
630  ref<Expr> chk =
631  op.first->getBoundsCheckPointer(address,
632  cast<ConstantExpr>(size)->getZExtValue());
633  if (!chk->isTrue()) {
635  "check_memory_access: memory error",
636  "ptr.err",
637  executor.getAddressInfo(state, address));
638  }
639  }
640  }
641 }
642 
643 void SpecialFunctionHandler::handleGetValue(ExecutionState &state,
644  KInstruction *target,
645  std::vector<ref<Expr> > &arguments) {
646  assert(arguments.size()==1 &&
647  "invalid number of arguments to klee_get_value");
648 
649  executor.executeGetValue(state, arguments[0], target);
650 }
651 
652 void SpecialFunctionHandler::handleDefineFixedObject(ExecutionState &state,
653  KInstruction *target,
654  std::vector<ref<Expr> > &arguments) {
655  assert(arguments.size()==2 &&
656  "invalid number of arguments to klee_define_fixed_object");
657  assert(isa<ConstantExpr>(arguments[0]) &&
658  "expect constant address argument to klee_define_fixed_object");
659  assert(isa<ConstantExpr>(arguments[1]) &&
660  "expect constant size argument to klee_define_fixed_object");
661 
662  uint64_t address = cast<ConstantExpr>(arguments[0])->getZExtValue();
663  uint64_t size = cast<ConstantExpr>(arguments[1])->getZExtValue();
664  MemoryObject *mo = executor.memory->allocateFixed(address, size, state.prevPC->inst);
665  executor.bindObjectInState(state, mo, false);
666  mo->isUserSpecified = true; // XXX hack;
667 }
668 
669 void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
670  KInstruction *target,
671  std::vector<ref<Expr> > &arguments) {
672  std::string name;
673 
674  // FIXME: For backwards compatibility, we should eventually enforce the
675  // correct arguments.
676  if (arguments.size() == 2) {
677  name = "unnamed";
678  } else {
679  // FIXME: Should be a user.err, not an assert.
680  assert(arguments.size()==3 &&
681  "invalid number of arguments to klee_make_symbolic");
682  name = readStringAtAddress(state, arguments[2]);
683  }
684 
686  executor.resolveExact(state, arguments[0], rl, "make_symbolic");
687 
688  for (Executor::ExactResolutionList::iterator it = rl.begin(),
689  ie = rl.end(); it != ie; ++it) {
690  const MemoryObject *mo = it->first.first;
691  mo->setName(name);
692 
693  const ObjectState *old = it->first.second;
694  ExecutionState *s = it->second;
695 
696  if (old->readOnly) {
698  "cannot make readonly object symbolic",
699  "user.err");
700  return;
701  }
702 
703  // FIXME: Type coercion should be done consistently somewhere.
704  bool res;
705  bool success =
707  EqExpr::create(ZExtExpr::create(arguments[1],
708  Context::get().getPointerWidth()),
709  mo->getSizeExpr()),
710  res);
711  assert(success && "FIXME: Unhandled solver failure");
712 
713  if (res) {
714  executor.executeMakeSymbolic(*s, mo, name);
715  } else {
717  "wrong size given to klee_make_symbolic[_name]",
718  "user.err");
719  }
720  }
721 }
722 
723 void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state,
724  KInstruction *target,
725  std::vector<ref<Expr> > &arguments) {
726  assert(arguments.size()==1 &&
727  "invalid number of arguments to klee_mark_global");
728 
730  executor.resolveExact(state, arguments[0], rl, "mark_global");
731 
732  for (Executor::ExactResolutionList::iterator it = rl.begin(),
733  ie = rl.end(); it != ie; ++it) {
734  const MemoryObject *mo = it->first.first;
735  assert(!mo->isLocal);
736  mo->isGlobal = true;
737  }
738 }
739 
740 
void dumpStack(llvm::raw_ostream &out) const
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 executeFree(ExecutionState &state, ref< Expr > address, KInstruction *target=0)
Definition: Executor.cpp:3069
ObjectState * bindObjectInState(ExecutionState &state, const MemoryObject *mo, bool isLocal, const Array *array=0)
Definition: Executor.cpp:2942
std::pair< const MemoryObject *, const ObjectState * > ObjectPair
Definition: AddressSpace.h:24
#define addDNR(name, handler)
bool hasReturnValue
Intrinsic terminates the process.
void terminateState(ExecutionState &state)
Definition: Executor.cpp:2695
std::string getAddressInfo(ExecutionState &state, ref< Expr > address) const
Get textual information regarding a memory address.
Definition: Executor.cpp:2645
StatePair fork(ExecutionState &current, ref< Expr > condition, bool isInternal)
Definition: Executor.cpp:729
MemoryManager * memory
Definition: Executor.h:109
void executeGetValue(ExecutionState &state, ref< Expr > e, KInstruction *target)
Definition: Executor.cpp:1130
void(SpecialFunctionHandler::* Handler)(ExecutionState &state, KInstruction *target, std::vector< ref< Expr > > &arguments)
void terminateStateOnExit(ExecutionState &state)
Definition: Executor.cpp:2729
static const Width Int32
Definition: Expr.h:100
void addConstraint(ExecutionState &state, ref< Expr > condition)
Definition: Executor.cpp:956
bool resolveOne(const ref< ConstantExpr > &address, ObjectPair &result)
void addFnAlias(std::string old_fn, std::string new_fn)
void void void klee_warning(const char *msg,...) __attribute__((format(printf
Definition: Common.cpp:81
AddressSpace addressSpace
static const Context & get()
get - Return the global singleton instance of the Context.
Definition: Context.cpp:35
static ref< Expr > createIsZero(ref< Expr > e)
Definition: Expr.cpp:305
#define add(name, handler, ret)
void terminateStateOnError(ExecutionState &state, const llvm::Twine &message, const char *suffix, const llvm::Twine &longMessage="")
Definition: Executor.cpp:2778
ref< ConstantExpr > getSizeExpr() const
Definition: Memory.h:116
bool isTrue() const
isTrue - Is this the true expression.
Definition: Expr.h:1094
static ref< ConstantExpr > create(uint64_t v, Width w)
Definition: Expr.h:412
llvm::Instruction * inst
Definition: KInstruction.h:30
ref< Expr > toUnique(const ExecutionState &state, ref< Expr > &e)
Definition: Executor.cpp:1079
bool mustBeFalse(const ExecutionState &, ref< Expr >, bool &result)
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
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
void removeFnAlias(std::string fn)
TimingSolver * solver
Definition: Executor.h:108
bool mustBeTrue(const ExecutionState &, ref< Expr >, bool &result)
KModule * kmodule
Definition: Executor.h:101
std::vector< std::pair< std::pair< const MemoryObject *, const ObjectState * >, ExecutionState * > > ExactResolutionList
Definition: Executor.h:222
KInstIterator prevPC
bool forkDisabled
Disables forking, set by user code.
std::string readStringAtAddress(ExecutionState &state, ref< Expr > address)
void executeMakeSymbolic(ExecutionState &state, const MemoryObject *mo, const std::string &name)
Definition: Executor.cpp:3260
bool handle(ExecutionState &state, llvm::Function *f, KInstruction *target, std::vector< ref< Expr > > &arguments)
static const Width Bool
Definition: Expr.h:97
std::pair< ref< Expr >, ref< Expr > > getRange(const ExecutionState &, ref< Expr > query)
bool doNotOverride
Intrinsic has a return value.
MemoryObject * allocateFixed(uint64_t address, uint64_t size, const llvm::Value *allocSite)
bool getValue(const ExecutionState &, ref< Expr > expr, ref< ConstantExpr > &result)
llvm::Module * module
Definition: KModule.h:87
static SpecialFunctionHandler::HandlerInfo handlerInfo[]
ref< Expr > read8(unsigned offset) const
Definition: Memory.cpp:387
bool isUserSpecified
Definition: Memory.h:54
void bindLocal(KInstruction *target, ExecutionState &state, ref< Expr > value)
Definition: Executor.cpp:1069
void setName(std::string name) const
Definition: Memory.h:109
void resolveExact(ExecutionState &state, ref< Expr > p, ExactResolutionList &results, const std::string &name)
Definition: Executor.cpp:3103