klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
main.cpp
Go to the documentation of this file.
1 /* -*- mode: c++; c-basic-offset: 2; -*- */
2 
3 // FIXME: This does not belong here.
4 #include "../lib/Core/Common.h"
5 
6 #include "klee/ExecutionState.h"
7 #include "klee/Expr.h"
8 #include "klee/Interpreter.h"
9 #include "klee/Statistics.h"
10 #include "klee/Config/Version.h"
15 
16 #if LLVM_VERSION_CODE > LLVM_VERSION(3, 2)
17 #include "llvm/IR/Constants.h"
18 #include "llvm/IR/Module.h"
19 #include "llvm/IR/Type.h"
20 #include "llvm/IR/InstrTypes.h"
21 #include "llvm/IR/Instruction.h"
22 #include "llvm/IR/Instructions.h"
23 #include "llvm/IR/LLVMContext.h"
24 #else
25 #include "llvm/Constants.h"
26 #include "llvm/Module.h"
27 #include "llvm/Type.h"
28 #include "llvm/InstrTypes.h"
29 #include "llvm/Instruction.h"
30 #include "llvm/Instructions.h"
31 #include "llvm/LLVMContext.h"
32 #include "llvm/Support/FileSystem.h"
33 #endif
34 #include "llvm/Support/FileSystem.h"
35 #include "llvm/Bitcode/ReaderWriter.h"
36 #include "llvm/Support/CommandLine.h"
37 #include "llvm/Support/Debug.h"
38 #include "llvm/Support/ManagedStatic.h"
39 #include "llvm/Support/MemoryBuffer.h"
40 #include "llvm/Support/raw_ostream.h"
41 
42 // FIXME: Ugh, this is gross. But otherwise our config.h conflicts with LLVMs.
43 #undef PACKAGE_BUGREPORT
44 #undef PACKAGE_NAME
45 #undef PACKAGE_STRING
46 #undef PACKAGE_TARNAME
47 #undef PACKAGE_VERSION
48 #if LLVM_VERSION_CODE < LLVM_VERSION(3, 0)
49 #include "llvm/Target/TargetSelect.h"
50 #else
51 #include "llvm/Support/TargetSelect.h"
52 #endif
53 #include "llvm/Support/Signals.h"
54 #include "llvm/Support/system_error.h"
55 
56 #include <dirent.h>
57 #include <signal.h>
58 #include <unistd.h>
59 #include <sys/stat.h>
60 #include <sys/wait.h>
61 
62 #include <cerrno>
63 #include <fstream>
64 #include <iomanip>
65 #include <iterator>
66 #include <sstream>
67 
68 
69 using namespace llvm;
70 using namespace klee;
71 
72 namespace {
73  cl::opt<std::string>
74  InputFile(cl::desc("<input bytecode>"), cl::Positional, cl::init("-"));
75 
76  cl::opt<std::string>
77  RunInDir("run-in", cl::desc("Change to the given directory prior to executing"));
78 
79  cl::opt<std::string>
80  Environ("environ", cl::desc("Parse environ from given file (in \"env\" format)"));
81 
82  cl::list<std::string>
83  InputArgv(cl::ConsumeAfter,
84  cl::desc("<program arguments>..."));
85 
86  cl::opt<bool>
87  NoOutput("no-output",
88  cl::desc("Don't generate test files"));
89 
90  cl::opt<bool>
91  WarnAllExternals("warn-all-externals",
92  cl::desc("Give initial warning for all externals."));
93 
94  cl::opt<bool>
95  WriteCVCs("write-cvcs",
96  cl::desc("Write .cvc files for each test case"));
97 
98  cl::opt<bool>
99  WritePCs("write-pcs",
100  cl::desc("Write .pc files for each test case"));
101 
102  cl::opt<bool>
103  WriteSMT2s("write-smt2s",
104  cl::desc("Write .smt2 (SMT-LIBv2) files for each test case"));
105 
106  cl::opt<bool>
107  WriteCov("write-cov",
108  cl::desc("Write coverage information for each test case"));
109 
110  cl::opt<bool>
111  WriteTestInfo("write-test-info",
112  cl::desc("Write additional test case information"));
113 
114  cl::opt<bool>
115  WritePaths("write-paths",
116  cl::desc("Write .path files for each test case"));
117 
118  cl::opt<bool>
119  WriteSymPaths("write-sym-paths",
120  cl::desc("Write .sym.path files for each test case"));
121 
122  cl::opt<bool>
123  ExitOnError("exit-on-error",
124  cl::desc("Exit if errors occur"));
125 
126 
127  enum LibcType {
128  NoLibc, KleeLibc, UcLibc
129  };
130 
131  cl::opt<LibcType>
132  Libc("libc",
133  cl::desc("Choose libc version (none by default)."),
134  cl::values(clEnumValN(NoLibc, "none", "Don't link in a libc"),
135  clEnumValN(KleeLibc, "klee", "Link in klee libc"),
136  clEnumValN(UcLibc, "uclibc", "Link in uclibc (adapted for klee)"),
137  clEnumValEnd),
138  cl::init(NoLibc));
139 
140 
141  cl::opt<bool>
142  WithPOSIXRuntime("posix-runtime",
143  cl::desc("Link with POSIX runtime. Options that can be passed as arguments to the programs are: --sym-argv <max-len> --sym-argvs <min-argvs> <max-argvs> <max-len> + file model options"),
144  cl::init(false));
145 
146  cl::opt<bool>
147  OptimizeModule("optimize",
148  cl::desc("Optimize before execution"),
149  cl::init(false));
150 
151  cl::opt<bool>
152  CheckDivZero("check-div-zero",
153  cl::desc("Inject checks for division-by-zero"),
154  cl::init(true));
155 
156  cl::opt<bool>
157  CheckOvershift("check-overshift",
158  cl::desc("Inject checks for overshift"),
159  cl::init(true));
160 
161  cl::opt<std::string>
162  OutputDir("output-dir",
163  cl::desc("Directory to write results in (defaults to klee-out-N)"),
164  cl::init(""));
165 
166  // this is a fake entry, its automagically handled
167  cl::list<std::string>
168  ReadArgsFilesFake("read-args",
169  cl::desc("File to read arguments from (one arg per line)"));
170 
171  cl::opt<bool>
172  ReplayKeepSymbolic("replay-keep-symbolic",
173  cl::desc("Replay the test cases only by asserting "
174  "the bytes, not necessarily making them concrete."));
175 
176  cl::list<std::string>
177  ReplayOutFile("replay-out",
178  cl::desc("Specify an out file to replay"),
179  cl::value_desc("out file"));
180 
181  cl::list<std::string>
182  ReplayOutDir("replay-out-dir",
183  cl::desc("Specify a directory to replay .out files from"),
184  cl::value_desc("output directory"));
185 
186  cl::opt<std::string>
187  ReplayPathFile("replay-path",
188  cl::desc("Specify a path file to replay"),
189  cl::value_desc("path file"));
190 
191  cl::list<std::string>
192  SeedOutFile("seed-out");
193 
194  cl::list<std::string>
195  SeedOutDir("seed-out-dir");
196 
197  cl::opt<unsigned>
198  MakeConcreteSymbolic("make-concrete-symbolic",
199  cl::desc("Probabilistic rate at which to make concrete reads symbolic, "
200  "i.e. approximately 1 in n concrete reads will be made symbolic (0=off, 1=all). "
201  "Used for testing."),
202  cl::init(0));
203 
204  cl::opt<unsigned>
205  StopAfterNTests("stop-after-n-tests",
206  cl::desc("Stop execution after generating the given number of tests. Extra tests corresponding to partially explored paths will also be dumped."),
207  cl::init(0));
208 
209  cl::opt<bool>
210  Watchdog("watchdog",
211  cl::desc("Use a watchdog process to enforce --max-time."),
212  cl::init(0));
213 }
214 
215 extern cl::opt<double> MaxTime;
216 
217 /***/
218 
220 private:
223  llvm::raw_ostream *m_infoFile;
224 
225  SmallString<128> m_outputDirectory;
226 
227  unsigned m_testIndex; // number of tests written so far
228  unsigned m_pathsExplored; // number of paths explored so far
229 
230  // used for writing .ktest files
231  int m_argc;
232  char **m_argv;
233 
234 public:
235  KleeHandler(int argc, char **argv);
236  ~KleeHandler();
237 
238  llvm::raw_ostream &getInfoStream() const { return *m_infoFile; }
239  unsigned getNumTestCases() { return m_testIndex; }
240  unsigned getNumPathsExplored() { return m_pathsExplored; }
241  void incPathsExplored() { m_pathsExplored++; }
242 
243  void setInterpreter(Interpreter *i);
244 
245  void processTestCase(const ExecutionState &state,
246  const char *errorMessage,
247  const char *errorSuffix);
248 
249  std::string getOutputFilename(const std::string &filename);
250  llvm::raw_fd_ostream *openOutputFile(const std::string &filename);
251  std::string getTestFilename(const std::string &suffix, unsigned id);
252  llvm::raw_fd_ostream *openTestFile(const std::string &suffix, unsigned id);
253 
254  // load a .out file
255  static void loadOutFile(std::string name,
256  std::vector<unsigned char> &buffer);
257 
258  // load a .path file
259  static void loadPathFile(std::string name,
260  std::vector<bool> &buffer);
261 
262  static void getOutFiles(std::string path,
263  std::vector<std::string> &results);
264 
265  static std::string getRunTimeLibraryPath(const char *argv0);
266 };
267 
268 KleeHandler::KleeHandler(int argc, char **argv)
269  : m_interpreter(0),
270  m_pathWriter(0),
271  m_symPathWriter(0),
272  m_infoFile(0),
273  m_outputDirectory(),
274  m_testIndex(0),
275  m_pathsExplored(0),
276  m_argc(argc),
277  m_argv(argv) {
278 
279  // create output directory (OutputDir or "klee-out-<i>")
280  bool dir_given = OutputDir != "";
281  SmallString<128> directory(dir_given ? OutputDir : InputFile);
282 
283  error_code ec;
284  if (!dir_given) sys::path::remove_filename(directory);
285  if ((ec = sys::fs::make_absolute(directory)) != errc::success)
286  klee_error("unable to determine absolute path: %s", ec.message().c_str());
287 
288  if (dir_given) {
289  // OutputDir
290  if (mkdir(directory.c_str(), 0775) < 0)
291  klee_error("cannot create \"%s\": %s", directory.c_str(), strerror(errno));
292 
293  m_outputDirectory = directory;
294  } else {
295  // "klee-out-<i>"
296  int i = 0;
297  for (; i <= INT_MAX; ++i) {
298  SmallString<128> d(directory);
299  llvm::sys::path::append(d, "klee-out-");
300  raw_svector_ostream ds(d); ds << i; ds.flush();
301 
302  // create directory and try to link klee-last
303  if (mkdir(d.c_str(), 0775) == 0) {
304  m_outputDirectory = d;
305 
306  SmallString<128> klee_last(directory);
307  llvm::sys::path::append(klee_last, "klee-last");
308 
309  if (((unlink(klee_last.c_str()) < 0) && (errno != ENOENT)) ||
310  symlink(m_outputDirectory.c_str(), klee_last.c_str()) < 0) {
311 
312  klee_warning("cannot create klee-last symlink: %s", strerror(errno));
313  }
314 
315  break;
316  }
317 
318  // otherwise try again or exit on error
319  if (errno != EEXIST)
320  klee_error("cannot create \"%s\": %s", m_outputDirectory.c_str(), strerror(errno));
321  }
322  if (i == INT_MAX && m_outputDirectory.str().equals(""))
323  klee_error("cannot create output directory: index out of range");
324  }
325 
326  klee_message("output directory is \"%s\"", m_outputDirectory.c_str());
327 
328  // open warnings.txt
329  std::string file_path = getOutputFilename("warnings.txt");
330  if ((klee_warning_file = fopen(file_path.c_str(), "w")) == NULL)
331  klee_error("cannot open file \"%s\": %s", file_path.c_str(), strerror(errno));
332 
333  // open messages.txt
334  file_path = getOutputFilename("messages.txt");
335  if ((klee_message_file = fopen(file_path.c_str(), "w")) == NULL)
336  klee_error("cannot open file \"%s\": %s", file_path.c_str(), strerror(errno));
337 
338  // open info
339  m_infoFile = openOutputFile("info");
340 }
341 
343  if (m_pathWriter) delete m_pathWriter;
344  if (m_symPathWriter) delete m_symPathWriter;
345  fclose(klee_warning_file);
346  fclose(klee_message_file);
347  delete m_infoFile;
348 }
349 
351  m_interpreter = i;
352 
353  if (WritePaths) {
355  assert(m_pathWriter->good());
357  }
358 
359  if (WriteSymPaths) {
360  m_symPathWriter = new TreeStreamWriter(getOutputFilename("symPaths.ts"));
361  assert(m_symPathWriter->good());
363  }
364 }
365 
366 std::string KleeHandler::getOutputFilename(const std::string &filename) {
367  SmallString<128> path = m_outputDirectory;
368  sys::path::append(path,filename);
369  return path.str();
370 }
371 
372 llvm::raw_fd_ostream *KleeHandler::openOutputFile(const std::string &filename) {
373  llvm::raw_fd_ostream *f;
374  std::string Error;
375  std::string path = getOutputFilename(filename);
376 #if LLVM_VERSION_CODE >= LLVM_VERSION(3,0)
377  f = new llvm::raw_fd_ostream(path.c_str(), Error, llvm::sys::fs::F_Binary);
378 #else
379  f = new llvm::raw_fd_ostream(path.c_str(), Error, llvm::raw_fd_ostream::F_Binary);
380 #endif
381  if (!Error.empty()) {
382  klee_error("error opening file \"%s\". KLEE may have run out of file "
383  "descriptors: try to increase the maximum number of open file "
384  "descriptors by using ulimit (%s).",
385  filename.c_str(), Error.c_str());
386  delete f;
387  f = NULL;
388  }
389 
390  return f;
391 }
392 
393 std::string KleeHandler::getTestFilename(const std::string &suffix, unsigned id) {
394  std::stringstream filename;
395  filename << "test" << std::setfill('0') << std::setw(6) << id << '.' << suffix;
396  return filename.str();
397 }
398 
399 llvm::raw_fd_ostream *KleeHandler::openTestFile(const std::string &suffix,
400  unsigned id) {
401  return openOutputFile(getTestFilename(suffix, id));
402 }
403 
404 
405 /* Outputs all files (.ktest, .pc, .cov etc.) describing a test case */
407  const char *errorMessage,
408  const char *errorSuffix) {
409  if (errorMessage && ExitOnError) {
410  llvm::errs() << "EXITING ON ERROR:\n" << errorMessage << "\n";
411  exit(1);
412  }
413 
414  if (!NoOutput) {
415  std::vector< std::pair<std::string, std::vector<unsigned char> > > out;
416  bool success = m_interpreter->getSymbolicSolution(state, out);
417 
418  if (!success)
419  klee_warning("unable to get symbolic solution, losing test case");
420 
421  double start_time = util::getWallTime();
422 
423  unsigned id = ++m_testIndex;
424 
425  if (success) {
426  KTest b;
427  b.numArgs = m_argc;
428  b.args = m_argv;
429  b.symArgvs = 0;
430  b.symArgvLen = 0;
431  b.numObjects = out.size();
432  b.objects = new KTestObject[b.numObjects];
433  assert(b.objects);
434  for (unsigned i=0; i<b.numObjects; i++) {
435  KTestObject *o = &b.objects[i];
436  o->name = const_cast<char*>(out[i].first.c_str());
437  o->numBytes = out[i].second.size();
438  o->bytes = new unsigned char[o->numBytes];
439  assert(o->bytes);
440  std::copy(out[i].second.begin(), out[i].second.end(), o->bytes);
441  }
442 
443  if (!kTest_toFile(&b, getOutputFilename(getTestFilename("ktest", id)).c_str())) {
444  klee_warning("unable to write output test case, losing it");
445  }
446 
447  for (unsigned i=0; i<b.numObjects; i++)
448  delete[] b.objects[i].bytes;
449  delete[] b.objects;
450  }
451 
452  if (errorMessage) {
453  llvm::raw_ostream *f = openTestFile(errorSuffix, id);
454  *f << errorMessage;
455  delete f;
456  }
457 
458  if (m_pathWriter) {
459  std::vector<unsigned char> concreteBranches;
461  concreteBranches);
462  llvm::raw_fd_ostream *f = openTestFile("path", id);
463  for (std::vector<unsigned char>::iterator I = concreteBranches.begin(),
464  E = concreteBranches.end();
465  I != E; ++I) {
466  *f << *I << "\n";
467  }
468  delete f;
469  }
470 
471  if (errorMessage || WritePCs) {
472  std::string constraints;
473  m_interpreter->getConstraintLog(state, constraints,Interpreter::KQUERY);
474  llvm::raw_ostream *f = openTestFile("pc", id);
475  *f << constraints;
476  delete f;
477  }
478 
479  if (WriteCVCs) {
480  std::string constraints;
481  m_interpreter->getConstraintLog(state, constraints, Interpreter::STP);
482  llvm::raw_ostream *f = openTestFile("cvc", id);
483  *f << constraints;
484  delete f;
485  }
486 
487  if(WriteSMT2s) {
488  std::string constraints;
489  m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2);
490  llvm::raw_ostream *f = openTestFile("smt2", id);
491  *f << constraints;
492  delete f;
493  }
494 
495  if (m_symPathWriter) {
496  std::vector<unsigned char> symbolicBranches;
498  symbolicBranches);
499  llvm::raw_fd_ostream *f = openTestFile("sym.path", id);
500  for (std::vector<unsigned char>::iterator I = symbolicBranches.begin(), E = symbolicBranches.end(); I!=E; ++I) {
501  *f << *I << "\n";
502  }
503  delete f;
504  }
505 
506  if (WriteCov) {
507  std::map<const std::string*, std::set<unsigned> > cov;
508  m_interpreter->getCoveredLines(state, cov);
509  llvm::raw_ostream *f = openTestFile("cov", id);
510  for (std::map<const std::string*, std::set<unsigned> >::iterator
511  it = cov.begin(), ie = cov.end();
512  it != ie; ++it) {
513  for (std::set<unsigned>::iterator
514  it2 = it->second.begin(), ie = it->second.end();
515  it2 != ie; ++it2)
516  *f << *it->first << ":" << *it2 << "\n";
517  }
518  delete f;
519  }
520 
521  if (m_testIndex == StopAfterNTests)
523 
524  if (WriteTestInfo) {
525  double elapsed_time = util::getWallTime() - start_time;
526  llvm::raw_ostream *f = openTestFile("info", id);
527  *f << "Time to generate test case: "
528  << elapsed_time << "s\n";
529  delete f;
530  }
531  }
532 }
533 
534  // load a .path file
535 void KleeHandler::loadPathFile(std::string name,
536  std::vector<bool> &buffer) {
537  std::ifstream f(name.c_str(), std::ios::in | std::ios::binary);
538 
539  if (!f.good())
540  assert(0 && "unable to open path file");
541 
542  while (f.good()) {
543  unsigned value;
544  f >> value;
545  buffer.push_back(!!value);
546  f.get();
547  }
548 }
549 
550 void KleeHandler::getOutFiles(std::string path,
551  std::vector<std::string> &results) {
552  error_code ec;
553  for (llvm::sys::fs::directory_iterator i(path,ec),e; i!=e && !ec; i.increment(ec)){
554  std::string f = (*i).path();
555  if (f.substr(f.size()-6,f.size()) == ".ktest") {
556  results.push_back(f);
557  }
558  }
559 
560  if (ec) {
561  llvm::errs() << "ERROR: unable to read output directory: " << path << ": "
562  << ec.message() << "\n";
563  exit(1);
564  }
565 }
566 
567 std::string KleeHandler::getRunTimeLibraryPath(const char *argv0) {
568  // Take any function from the execution binary but not main (as not allowed by
569  // C++ standard)
570  void *MainExecAddr = (void *)(intptr_t)getRunTimeLibraryPath;
571  SmallString<128> toolRoot(
572  #if LLVM_VERSION_CODE >= LLVM_VERSION(3,4)
573  llvm::sys::fs::getMainExecutable(argv0, MainExecAddr)
574  #else
575  llvm::sys::Path::GetMainExecutable(argv0, MainExecAddr).str()
576  #endif
577  );
578 
579  // Strip off executable so we have a directory path
580  llvm::sys::path::remove_filename(toolRoot);
581 
582  SmallString<128> libDir;
583 
584  if ( strcmp(toolRoot.c_str(), KLEE_INSTALL_BIN_DIR ) == 0)
585  {
586  DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() <<
587  "Using installed KLEE library runtime: ");
588  libDir = KLEE_INSTALL_LIB_DIR ;
589  }
590  else
591  {
592  DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() <<
593  "Using build directory KLEE library runtime :");
594  libDir = KLEE_DIR;
595  llvm::sys::path::append(libDir,RUNTIME_CONFIGURATION);
596  llvm::sys::path::append(libDir,"lib");
597  }
598 
599  DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() <<
600  libDir.c_str() << "\n");
601  return libDir.str();
602 }
603 
604 //===----------------------------------------------------------------------===//
605 // main Driver function
606 //
607 #if ENABLE_STPLOG == 1
608 extern "C" void STPLOG_init(const char *);
609 #endif
610 
611 static std::string strip(std::string &in) {
612  unsigned len = in.size();
613  unsigned lead = 0, trail = len;
614  while (lead<len && isspace(in[lead]))
615  ++lead;
616  while (trail>lead && isspace(in[trail-1]))
617  --trail;
618  return in.substr(lead, trail-lead);
619 }
620 
621 static void readArgumentsFromFile(char *file, std::vector<std::string> &results) {
622  std::ifstream f(file);
623  assert(f.is_open() && "unable to open input for reading arguments");
624  while (!f.eof()) {
625  std::string line;
626  std::getline(f, line);
627  line = strip(line);
628  if (!line.empty())
629  results.push_back(line);
630  }
631  f.close();
632 }
633 
634 static void parseArguments(int argc, char **argv) {
635  std::vector<std::string> arguments;
636 
637  for (int i=1; i<argc; i++) {
638  if (!strcmp(argv[i],"--read-args") && i+1<argc) {
639  readArgumentsFromFile(argv[++i], arguments);
640  } else {
641  arguments.push_back(argv[i]);
642  }
643  }
644 
645  int numArgs = arguments.size() + 1;
646  const char **argArray = new const char*[numArgs+1];
647  argArray[0] = argv[0];
648  argArray[numArgs] = 0;
649  for (int i=1; i<numArgs; i++) {
650  argArray[i] = arguments[i-1].c_str();
651  }
652 
653 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
654  cl::ParseCommandLineOptions(numArgs, (const char**) argArray, " klee\n");
655 #else
656  cl::ParseCommandLineOptions(numArgs, (char**) argArray, " klee\n");
657 #endif
658  delete[] argArray;
659 }
660 
661 
662 
663 static int initEnv(Module *mainModule) {
664 
665  /*
666  nArgcP = alloc oldArgc->getType()
667  nArgvV = alloc oldArgv->getType()
668  store oldArgc nArgcP
669  store oldArgv nArgvP
670  klee_init_environment(nArgcP, nArgvP)
671  nArgc = load nArgcP
672  nArgv = load nArgvP
673  oldArgc->replaceAllUsesWith(nArgc)
674  oldArgv->replaceAllUsesWith(nArgv)
675  */
676 
677  Function *mainFn = mainModule->getFunction("main");
678 
679  if (mainFn->arg_size() < 2) {
680  klee_error("Cannot handle ""--posix-runtime"" when main() has less than two arguments.\n");
681  }
682 
683  Instruction* firstInst = mainFn->begin()->begin();
684 
685  Value* oldArgc = mainFn->arg_begin();
686  Value* oldArgv = ++mainFn->arg_begin();
687 
688  AllocaInst* argcPtr =
689  new AllocaInst(oldArgc->getType(), "argcPtr", firstInst);
690  AllocaInst* argvPtr =
691  new AllocaInst(oldArgv->getType(), "argvPtr", firstInst);
692 
693  /* Insert void klee_init_env(int* argc, char*** argv) */
694  std::vector<const Type*> params;
695  params.push_back(Type::getInt32Ty(getGlobalContext()));
696  params.push_back(Type::getInt32Ty(getGlobalContext()));
697  Function* initEnvFn =
698  cast<Function>(mainModule->getOrInsertFunction("klee_init_env",
699  Type::getVoidTy(getGlobalContext()),
700  argcPtr->getType(),
701  argvPtr->getType(),
702  NULL));
703  assert(initEnvFn);
704  std::vector<Value*> args;
705  args.push_back(argcPtr);
706  args.push_back(argvPtr);
707 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 0)
708  Instruction* initEnvCall = CallInst::Create(initEnvFn, args,
709  "", firstInst);
710 #else
711  Instruction* initEnvCall = CallInst::Create(initEnvFn, args.begin(), args.end(),
712  "", firstInst);
713 #endif
714  Value *argc = new LoadInst(argcPtr, "newArgc", firstInst);
715  Value *argv = new LoadInst(argvPtr, "newArgv", firstInst);
716 
717  oldArgc->replaceAllUsesWith(argc);
718  oldArgv->replaceAllUsesWith(argv);
719 
720  new StoreInst(oldArgc, argcPtr, initEnvCall);
721  new StoreInst(oldArgv, argvPtr, initEnvCall);
722 
723  return 0;
724 }
725 
726 
727 // This is a terrible hack until we get some real modeling of the
728 // system. All we do is check the undefined symbols and warn about
729 // any "unrecognized" externals and about any obviously unsafe ones.
730 
731 // Symbols we explicitly support
732 static const char *modelledExternals[] = {
733  "_ZTVN10__cxxabiv117__class_type_infoE",
734  "_ZTVN10__cxxabiv120__si_class_type_infoE",
735  "_ZTVN10__cxxabiv121__vmi_class_type_infoE",
736 
737  // special functions
738  "_assert",
739  "__assert_fail",
740  "__assert_rtn",
741  "calloc",
742  "_exit",
743  "exit",
744  "free",
745  "abort",
746  "klee_abort",
747  "klee_assume",
748  "klee_check_memory_access",
749  "klee_define_fixed_object",
750  "klee_get_errno",
751  "klee_get_valuef",
752  "klee_get_valued",
753  "klee_get_valuel",
754  "klee_get_valuell",
755  "klee_get_value_i32",
756  "klee_get_value_i64",
757  "klee_get_obj_size",
758  "klee_is_symbolic",
759  "klee_make_symbolic",
760  "klee_mark_global",
761  "klee_merge",
762  "klee_prefer_cex",
763  "klee_print_expr",
764  "klee_print_range",
765  "klee_report_error",
766  "klee_set_forking",
767  "klee_silent_exit",
768  "klee_warning",
769  "klee_warning_once",
770  "klee_alias_function",
771  "klee_stack_trace",
772 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
773  "llvm.dbg.declare",
774  "llvm.dbg.value",
775 #endif
776  "llvm.va_start",
777  "llvm.va_end",
778  "malloc",
779  "realloc",
780  "_ZdaPv",
781  "_ZdlPv",
782  "_Znaj",
783  "_Znwj",
784  "_Znam",
785  "_Znwm",
786 };
787 // Symbols we aren't going to warn about
788 static const char *dontCareExternals[] = {
789 #if 0
790  // stdio
791  "fprintf",
792  "fflush",
793  "fopen",
794  "fclose",
795  "fputs_unlocked",
796  "putchar_unlocked",
797  "vfprintf",
798  "fwrite",
799  "puts",
800  "printf",
801  "stdin",
802  "stdout",
803  "stderr",
804  "_stdio_term",
805  "__errno_location",
806  "fstat",
807 #endif
808 
809  // static information, pretty ok to return
810  "getegid",
811  "geteuid",
812  "getgid",
813  "getuid",
814  "getpid",
815  "gethostname",
816  "getpgrp",
817  "getppid",
818  "getpagesize",
819  "getpriority",
820  "getgroups",
821  "getdtablesize",
822  "getrlimit",
823  "getrlimit64",
824  "getcwd",
825  "getwd",
826  "gettimeofday",
827  "uname",
828 
829  // fp stuff we just don't worry about yet
830  "frexp",
831  "ldexp",
832  "__isnan",
833  "__signbit",
834 };
835 // Extra symbols we aren't going to warn about with klee-libc
836 static const char *dontCareKlee[] = {
837  "__ctype_b_loc",
838  "__ctype_get_mb_cur_max",
839 
840  // io system calls
841  "open",
842  "write",
843  "read",
844  "close",
845 };
846 // Extra symbols we aren't going to warn about with uclibc
847 static const char *dontCareUclibc[] = {
848  "__dso_handle",
849 
850  // Don't warn about these since we explicitly commented them out of
851  // uclibc.
852  "printf",
853  "vprintf"
854 };
855 // Symbols we consider unsafe
856 static const char *unsafeExternals[] = {
857  "fork", // oh lord
858  "exec", // heaven help us
859  "error", // calls _exit
860  "raise", // yeah
861  "kill", // mmmhmmm
862 };
863 #define NELEMS(array) (sizeof(array)/sizeof(array[0]))
864 void externalsAndGlobalsCheck(const Module *m) {
865  std::map<std::string, bool> externals;
866  std::set<std::string> modelled(modelledExternals,
868  std::set<std::string> dontCare(dontCareExternals,
870  std::set<std::string> unsafe(unsafeExternals,
872 
873  switch (Libc) {
874  case KleeLibc:
875  dontCare.insert(dontCareKlee, dontCareKlee+NELEMS(dontCareKlee));
876  break;
877  case UcLibc:
878  dontCare.insert(dontCareUclibc,
880  break;
881  case NoLibc: /* silence compiler warning */
882  break;
883  }
884 
885 
886  if (WithPOSIXRuntime)
887  dontCare.insert("syscall");
888 
889  for (Module::const_iterator fnIt = m->begin(), fn_ie = m->end();
890  fnIt != fn_ie; ++fnIt) {
891  if (fnIt->isDeclaration() && !fnIt->use_empty())
892  externals.insert(std::make_pair(fnIt->getName(), false));
893  for (Function::const_iterator bbIt = fnIt->begin(), bb_ie = fnIt->end();
894  bbIt != bb_ie; ++bbIt) {
895  for (BasicBlock::const_iterator it = bbIt->begin(), ie = bbIt->end();
896  it != ie; ++it) {
897  if (const CallInst *ci = dyn_cast<CallInst>(it)) {
898  if (isa<InlineAsm>(ci->getCalledValue())) {
899  klee_warning_once(&*fnIt,
900  "function \"%s\" has inline asm",
901  fnIt->getName().data());
902  }
903  }
904  }
905  }
906  }
907  for (Module::const_global_iterator
908  it = m->global_begin(), ie = m->global_end();
909  it != ie; ++it)
910  if (it->isDeclaration() && !it->use_empty())
911  externals.insert(std::make_pair(it->getName(), true));
912  // and remove aliases (they define the symbol after global
913  // initialization)
914  for (Module::const_alias_iterator
915  it = m->alias_begin(), ie = m->alias_end();
916  it != ie; ++it) {
917  std::map<std::string, bool>::iterator it2 =
918  externals.find(it->getName());
919  if (it2!=externals.end())
920  externals.erase(it2);
921  }
922 
923  std::map<std::string, bool> foundUnsafe;
924  for (std::map<std::string, bool>::iterator
925  it = externals.begin(), ie = externals.end();
926  it != ie; ++it) {
927  const std::string &ext = it->first;
928  if (!modelled.count(ext) && (WarnAllExternals ||
929  !dontCare.count(ext))) {
930  if (unsafe.count(ext)) {
931  foundUnsafe.insert(*it);
932  } else {
933  klee_warning("undefined reference to %s: %s",
934  it->second ? "variable" : "function",
935  ext.c_str());
936  }
937  }
938  }
939 
940  for (std::map<std::string, bool>::iterator
941  it = foundUnsafe.begin(), ie = foundUnsafe.end();
942  it != ie; ++it) {
943  const std::string &ext = it->first;
944  klee_warning("undefined reference to %s: %s (UNSAFE)!",
945  it->second ? "variable" : "function",
946  ext.c_str());
947  }
948 }
949 
951 
952 static bool interrupted = false;
953 
954 // Pulled out so it can be easily called from a debugger.
955 extern "C"
958 }
959 
960 extern "C"
961 void stop_forking() {
963 }
964 
965 static void interrupt_handle() {
966  if (!interrupted && theInterpreter) {
967  llvm::errs() << "KLEE: ctrl-c detected, requesting interpreter to halt.\n";
968  halt_execution();
969  sys::SetInterruptFunction(interrupt_handle);
970  } else {
971  llvm::errs() << "KLEE: ctrl-c detected, exiting.\n";
972  exit(1);
973  }
974  interrupted = true;
975 }
976 
978  // just wait for the child to finish
979 }
980 
981 // This is a temporary hack. If the running process has access to
982 // externals then it can disable interrupts, which screws up the
983 // normal "nice" watchdog termination process. We try to request the
984 // interpreter to halt using this mechanism as a last resort to save
985 // the state data before going ahead and killing it.
986 static void halt_via_gdb(int pid) {
987  char buffer[256];
988  sprintf(buffer,
989  "gdb --batch --eval-command=\"p halt_execution()\" "
990  "--eval-command=detach --pid=%d &> /dev/null",
991  pid);
992  // fprintf(stderr, "KLEE: WATCHDOG: running: %s\n", buffer);
993  if (system(buffer)==-1)
994  perror("system");
995 }
996 
997 // returns the end of the string put in buf
998 static char *format_tdiff(char *buf, long seconds)
999 {
1000  assert(seconds >= 0);
1001 
1002  long minutes = seconds / 60; seconds %= 60;
1003  long hours = minutes / 60; minutes %= 60;
1004  long days = hours / 24; hours %= 24;
1005 
1006  buf = strrchr(buf, '\0');
1007  if (days > 0) buf += sprintf(buf, "%ld days, ", days);
1008  buf += sprintf(buf, "%02ld:%02ld:%02ld", hours, minutes, seconds);
1009  return buf;
1010 }
1011 
1012 #ifndef SUPPORT_KLEE_UCLIBC
1013 static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir) {
1014  fprintf(stderr, "error: invalid libc, no uclibc support!\n");
1015  exit(1);
1016  return 0;
1017 }
1018 #else
1019 static void replaceOrRenameFunction(llvm::Module *module,
1020  const char *old_name, const char *new_name)
1021 {
1022  Function *f, *f2;
1023  f = module->getFunction(new_name);
1024  f2 = module->getFunction(old_name);
1025  if (f2) {
1026  if (f) {
1027  f2->replaceAllUsesWith(f);
1028  f2->eraseFromParent();
1029  } else {
1030  f2->setName(new_name);
1031  assert(f2->getName() == new_name);
1032  }
1033  }
1034 }
1035 static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir) {
1036  // Ensure that klee-uclibc exists
1037  SmallString<128> uclibcBCA(libDir);
1038  llvm::sys::path::append(uclibcBCA, KLEE_UCLIBC_BCA_NAME);
1039 
1040  bool uclibcExists=false;
1041  llvm::sys::fs::exists(uclibcBCA.c_str(), uclibcExists);
1042  if (!uclibcExists)
1043  klee_error("Cannot find klee-uclibc : %s", uclibcBCA.c_str());
1044 
1045  Function *f;
1046  // force import of __uClibc_main
1047  mainModule->getOrInsertFunction("__uClibc_main",
1048  FunctionType::get(Type::getVoidTy(getGlobalContext()),
1049  std::vector<LLVM_TYPE_Q Type*>(),
1050  true));
1051 
1052  // force various imports
1053  if (WithPOSIXRuntime) {
1054  LLVM_TYPE_Q llvm::Type *i8Ty = Type::getInt8Ty(getGlobalContext());
1055  mainModule->getOrInsertFunction("realpath",
1056  PointerType::getUnqual(i8Ty),
1057  PointerType::getUnqual(i8Ty),
1058  PointerType::getUnqual(i8Ty),
1059  NULL);
1060  mainModule->getOrInsertFunction("getutent",
1061  PointerType::getUnqual(i8Ty),
1062  NULL);
1063  mainModule->getOrInsertFunction("__fgetc_unlocked",
1064  Type::getInt32Ty(getGlobalContext()),
1065  PointerType::getUnqual(i8Ty),
1066  NULL);
1067  mainModule->getOrInsertFunction("__fputc_unlocked",
1068  Type::getInt32Ty(getGlobalContext()),
1069  Type::getInt32Ty(getGlobalContext()),
1070  PointerType::getUnqual(i8Ty),
1071  NULL);
1072  }
1073 
1074  f = mainModule->getFunction("__ctype_get_mb_cur_max");
1075  if (f) f->setName("_stdlib_mb_cur_max");
1076 
1077  // Strip of asm prefixes for 64 bit versions because they are not
1078  // present in uclibc and we want to make sure stuff will get
1079  // linked. In the off chance that both prefixed and unprefixed
1080  // versions are present in the module, make sure we don't create a
1081  // naming conflict.
1082  for (Module::iterator fi = mainModule->begin(), fe = mainModule->end();
1083  fi != fe; ++fi) {
1084  Function *f = fi;
1085  const std::string &name = f->getName();
1086  if (name[0]=='\01') {
1087  unsigned size = name.size();
1088  if (name[size-2]=='6' && name[size-1]=='4') {
1089  std::string unprefixed = name.substr(1);
1090 
1091  // See if the unprefixed version exists.
1092  if (Function *f2 = mainModule->getFunction(unprefixed)) {
1093  f->replaceAllUsesWith(f2);
1094  f->eraseFromParent();
1095  } else {
1096  f->setName(unprefixed);
1097  }
1098  }
1099  }
1100  }
1101 
1102  mainModule = klee::linkWithLibrary(mainModule, uclibcBCA.c_str());
1103  assert(mainModule && "unable to link with uclibc");
1104 
1105 
1106  replaceOrRenameFunction(mainModule, "__libc_open", "open");
1107  replaceOrRenameFunction(mainModule, "__libc_fcntl", "fcntl");
1108 
1109 
1110  // XXX we need to rearchitect so this can also be used with
1111  // programs externally linked with uclibc.
1112 
1113  // We now need to swap things so that __uClibc_main is the entry
1114  // point, in such a way that the arguments are passed to
1115  // __uClibc_main correctly. We do this by renaming the user main
1116  // and generating a stub function to call __uClibc_main. There is
1117  // also an implicit cooperation in that runFunctionAsMain sets up
1118  // the environment arguments to what uclibc expects (following
1119  // argv), since it does not explicitly take an envp argument.
1120  Function *userMainFn = mainModule->getFunction("main");
1121  assert(userMainFn && "unable to get user main");
1122  Function *uclibcMainFn = mainModule->getFunction("__uClibc_main");
1123  assert(uclibcMainFn && "unable to get uclibc main");
1124  userMainFn->setName("__user_main");
1125 
1126  const FunctionType *ft = uclibcMainFn->getFunctionType();
1127  assert(ft->getNumParams() == 7);
1128 
1129  std::vector<LLVM_TYPE_Q Type*> fArgs;
1130  fArgs.push_back(ft->getParamType(1)); // argc
1131  fArgs.push_back(ft->getParamType(2)); // argv
1132  Function *stub = Function::Create(FunctionType::get(Type::getInt32Ty(getGlobalContext()), fArgs, false),
1133  GlobalVariable::ExternalLinkage,
1134  "main",
1135  mainModule);
1136  BasicBlock *bb = BasicBlock::Create(getGlobalContext(), "entry", stub);
1137 
1138  std::vector<llvm::Value*> args;
1139  args.push_back(llvm::ConstantExpr::getBitCast(userMainFn,
1140  ft->getParamType(0)));
1141  args.push_back(stub->arg_begin()); // argc
1142  args.push_back(++stub->arg_begin()); // argv
1143  args.push_back(Constant::getNullValue(ft->getParamType(3))); // app_init
1144  args.push_back(Constant::getNullValue(ft->getParamType(4))); // app_fini
1145  args.push_back(Constant::getNullValue(ft->getParamType(5))); // rtld_fini
1146  args.push_back(Constant::getNullValue(ft->getParamType(6))); // stack_end
1147 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 0)
1148  CallInst::Create(uclibcMainFn, args, "", bb);
1149 #else
1150  CallInst::Create(uclibcMainFn, args.begin(), args.end(), "", bb);
1151 #endif
1152 
1153  new UnreachableInst(getGlobalContext(), bb);
1154 
1155  klee_message("NOTE: Using klee-uclibc : %s", uclibcBCA.c_str());
1156  return mainModule;
1157 }
1158 #endif
1159 
1160 int main(int argc, char **argv, char **envp) {
1161 #if ENABLE_STPLOG == 1
1162  STPLOG_init("stplog.c");
1163 #endif
1164 
1165  atexit(llvm_shutdown); // Call llvm_shutdown() on exit.
1166 
1167  llvm::InitializeNativeTarget();
1168 
1169  parseArguments(argc, argv);
1170  sys::PrintStackTraceOnErrorSignal();
1171 
1172  if (Watchdog) {
1173  if (MaxTime==0) {
1174  klee_error("--watchdog used without --max-time");
1175  }
1176 
1177  int pid = fork();
1178  if (pid<0) {
1179  klee_error("unable to fork watchdog");
1180  } else if (pid) {
1181  fprintf(stderr, "KLEE: WATCHDOG: watching %d\n", pid);
1182  fflush(stderr);
1183  sys::SetInterruptFunction(interrupt_handle_watchdog);
1184 
1185  double nextStep = util::getWallTime() + MaxTime*1.1;
1186  int level = 0;
1187 
1188  // Simple stupid code...
1189  while (1) {
1190  sleep(1);
1191 
1192  int status, res = waitpid(pid, &status, WNOHANG);
1193 
1194  if (res < 0) {
1195  if (errno==ECHILD) { // No child, no need to watch but
1196  // return error since we didn't catch
1197  // the exit.
1198  fprintf(stderr, "KLEE: watchdog exiting (no child)\n");
1199  return 1;
1200  } else if (errno!=EINTR) {
1201  perror("watchdog waitpid");
1202  exit(1);
1203  }
1204  } else if (res==pid && WIFEXITED(status)) {
1205  return WEXITSTATUS(status);
1206  } else {
1207  double time = util::getWallTime();
1208 
1209  if (time > nextStep) {
1210  ++level;
1211 
1212  if (level==1) {
1213  fprintf(stderr, "KLEE: WATCHDOG: time expired, attempting halt via INT\n");
1214  kill(pid, SIGINT);
1215  } else if (level==2) {
1216  fprintf(stderr, "KLEE: WATCHDOG: time expired, attempting halt via gdb\n");
1217  halt_via_gdb(pid);
1218  } else {
1219  fprintf(stderr, "KLEE: WATCHDOG: kill(9)ing child (I tried to be nice)\n");
1220  kill(pid, SIGKILL);
1221  return 1; // what more can we do
1222  }
1223 
1224  // Ideally this triggers a dump, which may take a while,
1225  // so try and give the process extra time to clean up.
1226  nextStep = util::getWallTime() + std::max(15., MaxTime*.1);
1227  }
1228  }
1229  }
1230 
1231  return 0;
1232  }
1233  }
1234 
1235  sys::SetInterruptFunction(interrupt_handle);
1236 
1237  // Load the bytecode...
1238  std::string ErrorMsg;
1239  Module *mainModule = 0;
1240  OwningPtr<MemoryBuffer> BufferPtr;
1241  error_code ec=MemoryBuffer::getFileOrSTDIN(InputFile.c_str(), BufferPtr);
1242  if (ec) {
1243  klee_error("error loading program '%s': %s", InputFile.c_str(),
1244  ec.message().c_str());
1245  }
1246  mainModule = getLazyBitcodeModule(BufferPtr.get(), getGlobalContext(), &ErrorMsg);
1247 
1248  if (mainModule) {
1249  if (mainModule->MaterializeAllPermanently(&ErrorMsg)) {
1250  delete mainModule;
1251  mainModule = 0;
1252  }
1253  }
1254  if (!mainModule)
1255  klee_error("error loading program '%s': %s", InputFile.c_str(),
1256  ErrorMsg.c_str());
1257 
1258  if (WithPOSIXRuntime) {
1259  int r = initEnv(mainModule);
1260  if (r != 0)
1261  return r;
1262  }
1263 
1264  std::string LibraryDir = KleeHandler::getRunTimeLibraryPath(argv[0]);
1265  Interpreter::ModuleOptions Opts(LibraryDir.c_str(),
1266  /*Optimize=*/OptimizeModule,
1267  /*CheckDivZero=*/CheckDivZero,
1268  /*CheckOvershift=*/CheckOvershift);
1269 
1270  switch (Libc) {
1271  case NoLibc: /* silence compiler warning */
1272  break;
1273 
1274  case KleeLibc: {
1275  // FIXME: Find a reasonable solution for this.
1276  SmallString<128> Path(Opts.LibraryDir);
1277 #if LLVM_VERSION_CODE >= LLVM_VERSION(3,3)
1278  llvm::sys::path::append(Path, "klee-libc.bc");
1279 #else
1280  llvm::sys::path::append(Path, "libklee-libc.bca");
1281 #endif
1282  mainModule = klee::linkWithLibrary(mainModule, Path.c_str());
1283  assert(mainModule && "unable to link with klee-libc");
1284  break;
1285  }
1286 
1287  case UcLibc:
1288  mainModule = linkWithUclibc(mainModule, LibraryDir);
1289  break;
1290  }
1291 
1292  if (WithPOSIXRuntime) {
1293  SmallString<128> Path(Opts.LibraryDir);
1294  llvm::sys::path::append(Path, "libkleeRuntimePOSIX.bca");
1295  klee_message("NOTE: Using model: %s", Path.c_str());
1296  mainModule = klee::linkWithLibrary(mainModule, Path.c_str());
1297  assert(mainModule && "unable to link with simple model");
1298  }
1299 
1300  // Get the desired main function. klee_main initializes uClibc
1301  // locale and other data and then calls main.
1302  Function *mainFn = mainModule->getFunction("main");
1303  if (!mainFn) {
1304  llvm::errs() << "'main' function not found in module.\n";
1305  return -1;
1306  }
1307 
1308  // FIXME: Change me to std types.
1309  int pArgc;
1310  char **pArgv;
1311  char **pEnvp;
1312  if (Environ != "") {
1313  std::vector<std::string> items;
1314  std::ifstream f(Environ.c_str());
1315  if (!f.good())
1316  klee_error("unable to open --environ file: %s", Environ.c_str());
1317  while (!f.eof()) {
1318  std::string line;
1319  std::getline(f, line);
1320  line = strip(line);
1321  if (!line.empty())
1322  items.push_back(line);
1323  }
1324  f.close();
1325  pEnvp = new char *[items.size()+1];
1326  unsigned i=0;
1327  for (; i != items.size(); ++i)
1328  pEnvp[i] = strdup(items[i].c_str());
1329  pEnvp[i] = 0;
1330  } else {
1331  pEnvp = envp;
1332  }
1333 
1334  pArgc = InputArgv.size() + 1;
1335  pArgv = new char *[pArgc];
1336  for (unsigned i=0; i<InputArgv.size()+1; i++) {
1337  std::string &arg = (i==0 ? InputFile : InputArgv[i-1]);
1338  unsigned size = arg.size() + 1;
1339  char *pArg = new char[size];
1340 
1341  std::copy(arg.begin(), arg.end(), pArg);
1342  pArg[size - 1] = 0;
1343 
1344  pArgv[i] = pArg;
1345  }
1346 
1347  std::vector<bool> replayPath;
1348 
1349  if (ReplayPathFile != "") {
1350  KleeHandler::loadPathFile(ReplayPathFile, replayPath);
1351  }
1352 
1354  IOpts.MakeConcreteSymbolic = MakeConcreteSymbolic;
1355  KleeHandler *handler = new KleeHandler(pArgc, pArgv);
1356  Interpreter *interpreter =
1357  theInterpreter = Interpreter::create(IOpts, handler);
1358  handler->setInterpreter(interpreter);
1359 
1360  llvm::raw_ostream &infoFile = handler->getInfoStream();
1361  for (int i=0; i<argc; i++) {
1362  infoFile << argv[i] << (i+1<argc ? " ":"\n");
1363  }
1364  infoFile << "PID: " << getpid() << "\n";
1365 
1366  const Module *finalModule =
1367  interpreter->setModule(mainModule, Opts);
1368  externalsAndGlobalsCheck(finalModule);
1369 
1370  if (ReplayPathFile != "") {
1371  interpreter->setReplayPath(&replayPath);
1372  }
1373 
1374  char buf[256];
1375  time_t t[2];
1376  t[0] = time(NULL);
1377  strftime(buf, sizeof(buf), "Started: %Y-%m-%d %H:%M:%S\n", localtime(&t[0]));
1378  infoFile << buf;
1379  infoFile.flush();
1380 
1381  if (!ReplayOutDir.empty() || !ReplayOutFile.empty()) {
1382  assert(SeedOutFile.empty());
1383  assert(SeedOutDir.empty());
1384 
1385  std::vector<std::string> outFiles = ReplayOutFile;
1386  for (std::vector<std::string>::iterator
1387  it = ReplayOutDir.begin(), ie = ReplayOutDir.end();
1388  it != ie; ++it)
1389  KleeHandler::getOutFiles(*it, outFiles);
1390  std::vector<KTest*> kTests;
1391  for (std::vector<std::string>::iterator
1392  it = outFiles.begin(), ie = outFiles.end();
1393  it != ie; ++it) {
1394  KTest *out = kTest_fromFile(it->c_str());
1395  if (out) {
1396  kTests.push_back(out);
1397  } else {
1398  llvm::errs() << "KLEE: unable to open: " << *it << "\n";
1399  }
1400  }
1401 
1402  if (RunInDir != "") {
1403  int res = chdir(RunInDir.c_str());
1404  if (res < 0) {
1405  klee_error("Unable to change directory to: %s", RunInDir.c_str());
1406  }
1407  }
1408 
1409  unsigned i=0;
1410  for (std::vector<KTest*>::iterator
1411  it = kTests.begin(), ie = kTests.end();
1412  it != ie; ++it) {
1413  KTest *out = *it;
1414  interpreter->setReplayOut(out);
1415  llvm::errs() << "KLEE: replaying: " << *it << " (" << kTest_numBytes(out)
1416  << " bytes)"
1417  << " (" << ++i << "/" << outFiles.size() << ")\n";
1418  // XXX should put envp in .ktest ?
1419  interpreter->runFunctionAsMain(mainFn, out->numArgs, out->args, pEnvp);
1420  if (interrupted) break;
1421  }
1422  interpreter->setReplayOut(0);
1423  while (!kTests.empty()) {
1424  kTest_free(kTests.back());
1425  kTests.pop_back();
1426  }
1427  } else {
1428  std::vector<KTest *> seeds;
1429  for (std::vector<std::string>::iterator
1430  it = SeedOutFile.begin(), ie = SeedOutFile.end();
1431  it != ie; ++it) {
1432  KTest *out = kTest_fromFile(it->c_str());
1433  if (!out) {
1434  llvm::errs() << "KLEE: unable to open: " << *it << "\n";
1435  exit(1);
1436  }
1437  seeds.push_back(out);
1438  }
1439  for (std::vector<std::string>::iterator
1440  it = SeedOutDir.begin(), ie = SeedOutDir.end();
1441  it != ie; ++it) {
1442  std::vector<std::string> outFiles;
1443  KleeHandler::getOutFiles(*it, outFiles);
1444  for (std::vector<std::string>::iterator
1445  it2 = outFiles.begin(), ie = outFiles.end();
1446  it2 != ie; ++it2) {
1447  KTest *out = kTest_fromFile(it2->c_str());
1448  if (!out) {
1449  llvm::errs() << "KLEE: unable to open: " << *it2 << "\n";
1450  exit(1);
1451  }
1452  seeds.push_back(out);
1453  }
1454  if (outFiles.empty()) {
1455  llvm::errs() << "KLEE: seeds directory is empty: " << *it << "\n";
1456  exit(1);
1457  }
1458  }
1459 
1460  if (!seeds.empty()) {
1461  llvm::errs() << "KLEE: using " << seeds.size() << " seeds\n";
1462  interpreter->useSeeds(&seeds);
1463  }
1464  if (RunInDir != "") {
1465  int res = chdir(RunInDir.c_str());
1466  if (res < 0) {
1467  klee_error("Unable to change directory to: %s", RunInDir.c_str());
1468  }
1469  }
1470  interpreter->runFunctionAsMain(mainFn, pArgc, pArgv, pEnvp);
1471 
1472  while (!seeds.empty()) {
1473  kTest_free(seeds.back());
1474  seeds.pop_back();
1475  }
1476  }
1477 
1478  t[1] = time(NULL);
1479  strftime(buf, sizeof(buf), "Finished: %Y-%m-%d %H:%M:%S\n", localtime(&t[1]));
1480  infoFile << buf;
1481 
1482  strcpy(buf, "Elapsed: ");
1483  strcpy(format_tdiff(buf, t[1] - t[0]), "\n");
1484  infoFile << buf;
1485 
1486  // Free all the args.
1487  for (unsigned i=0; i<InputArgv.size()+1; i++)
1488  delete[] pArgv[i];
1489  delete[] pArgv;
1490 
1491  delete interpreter;
1492 
1493  uint64_t queries =
1495  uint64_t queriesValid =
1496  *theStatisticManager->getStatisticByName("QueriesValid");
1497  uint64_t queriesInvalid =
1498  *theStatisticManager->getStatisticByName("QueriesInvalid");
1499  uint64_t queryCounterexamples =
1500  *theStatisticManager->getStatisticByName("QueriesCEX");
1501  uint64_t queryConstructs =
1502  *theStatisticManager->getStatisticByName("QueriesConstructs");
1503  uint64_t instructions =
1504  *theStatisticManager->getStatisticByName("Instructions");
1505  uint64_t forks =
1507 
1508  handler->getInfoStream()
1509  << "KLEE: done: explored paths = " << 1 + forks << "\n";
1510 
1511  // Write some extra information in the info file which users won't
1512  // necessarily care about or understand.
1513  if (queries)
1514  handler->getInfoStream()
1515  << "KLEE: done: avg. constructs per query = "
1516  << queryConstructs / queries << "\n";
1517  handler->getInfoStream()
1518  << "KLEE: done: total queries = " << queries << "\n"
1519  << "KLEE: done: valid queries = " << queriesValid << "\n"
1520  << "KLEE: done: invalid queries = " << queriesInvalid << "\n"
1521  << "KLEE: done: query cex = " << queryCounterexamples << "\n";
1522 
1523  std::stringstream stats;
1524  stats << "\n";
1525  stats << "KLEE: done: total instructions = "
1526  << instructions << "\n";
1527  stats << "KLEE: done: completed paths = "
1528  << handler->getNumPathsExplored() << "\n";
1529  stats << "KLEE: done: generated tests = "
1530  << handler->getNumTestCases() << "\n";
1531  llvm::errs() << stats.str();
1532  handler->getInfoStream() << stats.str();
1533 
1534  BufferPtr.take();
1535  delete handler;
1536 
1537  return 0;
1538 }
virtual void getConstraintLog(const ExecutionState &state, std::string &res, LogType logFormat=STP)=0
Definition: KTest.h:26
#define NELEMS(array)
Definition: main.cpp:863
unsigned symArgvs
Definition: KTest.h:33
llvm::raw_ostream * m_infoFile
Definition: main.cpp:223
virtual void useSeeds(const std::vector< struct KTest * > *seeds)=0
virtual const llvm::Module * setModule(llvm::Module *module, const ModuleOptions &opts)=0
int const char const char * suffix
Definition: klee.h:68
~KleeHandler()
Definition: main.cpp:342
virtual void setReplayPath(const std::vector< bool > *path)=0
static char * format_tdiff(char *buf, long seconds)
Definition: main.cpp:998
FILE * klee_message_file
Definition: Common.cpp:23
virtual void setInhibitForking(bool value)=0
void klee_error(const char *msg,...) __attribute__((format(printf
Definition: Common.cpp:73
static const char * dontCareKlee[]
Definition: main.cpp:836
static llvm::Module * linkWithUclibc(llvm::Module *mainModule, StringRef libDir)
Definition: main.cpp:1013
StatisticManager * theStatisticManager
Definition: Statistics.cpp:57
uint64_t ext(uint64_t l, unsigned outWidth, unsigned inWidth)
void klee_warning_once(char *name)
Definition: klee-replay.c:394
void incPathsExplored()
Definition: main.cpp:241
void klee_warning(char *name)
Definition: klee-replay.c:390
static void halt_via_gdb(int pid)
Definition: main.cpp:986
int m_argc
Definition: main.cpp:231
virtual unsigned getPathStreamID(const ExecutionState &state)=0
SmallString< 128 > m_outputDirectory
Definition: main.cpp:225
std::string getTestFilename(const std::string &suffix, unsigned id)
Definition: main.cpp:393
virtual void setHaltExecution(bool value)=0
Statistic queriesValid
unsigned numBytes
Definition: KTest.h:21
llvm::Module * linkWithLibrary(llvm::Module *module, const std::string &libraryName)
Link a module with a specified bitcode archive.
TreeStreamWriter * m_pathWriter
Definition: main.cpp:222
unsigned getNumTestCases()
Definition: main.cpp:239
virtual void setSymbolicPathWriter(TreeStreamWriter *tsw)=0
unsigned kTest_numBytes(KTest *bo)
Definition: KTest.cpp:222
static const char * dontCareUclibc[]
Definition: main.cpp:847
unsigned getNumPathsExplored()
Definition: main.cpp:240
double getWallTime()
Definition: Time.cpp:24
unsigned numArgs
Definition: KTest.h:30
Statistic queries
unsigned numObjects
Definition: KTest.h:36
static const char * modelledExternals[]
Definition: main.cpp:732
char ** m_argv
Definition: main.cpp:232
static void interrupt_handle_watchdog()
Definition: main.cpp:977
llvm::raw_fd_ostream * openTestFile(const std::string &suffix, unsigned id)
Definition: main.cpp:399
unsigned m_testIndex
Definition: main.cpp:227
static void getOutFiles(std::string path, std::vector< std::string > &results)
Definition: main.cpp:550
Statistic * getStatisticByName(const std::string &name) const
Definition: Statistics.cpp:50
std::string getOutputFilename(const std::string &filename)
Definition: main.cpp:366
char ** args
Definition: KTest.h:31
virtual void setPathWriter(TreeStreamWriter *tsw)=0
#define LLVM_VERSION_CODE
Definition: Version.h:16
void halt_execution()
Definition: main.cpp:956
#define LLVM_VERSION(major, minor)
Definition: Version.h:15
int kTest_toFile(KTest *bo, const char *path)
Definition: KTest.cpp:178
LibcType
Definition: main.cpp:127
virtual bool getSymbolicSolution(const ExecutionState &state, std::vector< std::pair< std::string, std::vector< unsigned char > > > &res)=0
llvm::raw_ostream & getInfoStream() const
Definition: main.cpp:238
unsigned char * bytes
Definition: KTest.h:22
void stop_forking()
Definition: main.cpp:961
virtual void runFunctionAsMain(llvm::Function *f, int argc, char **argv, char **envp)=0
#define LLVM_TYPE_Q
Definition: Version.h:21
static std::string getRunTimeLibraryPath(const char *argv0)
Definition: main.cpp:567
void setInterpreter(Interpreter *i)
Definition: main.cpp:350
static void readArgumentsFromFile(char *file, std::vector< std::string > &results)
Definition: main.cpp:621
static std::string strip(std::string &in)
Definition: main.cpp:611
TreeStreamWriter * m_symPathWriter
Definition: main.cpp:222
virtual void setReplayOut(const struct KTest *out)=0
KTestObject * objects
Definition: KTest.h:37
unsigned symArgvLen
Definition: KTest.h:34
void readStream(TreeStreamID id, std::vector< unsigned char > &out)
Definition: TreeStream.cpp:101
static int initEnv(Module *mainModule)
Definition: main.cpp:663
KleeHandler(int argc, char **argv)
Definition: main.cpp:268
char * name
Definition: KTest.h:20
void externalsAndGlobalsCheck(const Module *m)
Definition: main.cpp:864
void klee_message(const char *msg,...) __attribute__((format(printf
Definition: Common.cpp:58
int main(int argc, char **argv)
Definition: main.cpp:449
static const char * dontCareExternals[]
Definition: main.cpp:788
cl::opt< double > MaxTime
virtual void getCoveredLines(const ExecutionState &state, std::map< const std::string *, std::set< unsigned > > &res)=0
static void loadPathFile(std::string name, std::vector< bool > &buffer)
Definition: main.cpp:535
int line
Definition: klee.h:68
static void interrupt_handle()
Definition: main.cpp:965
llvm::raw_fd_ostream * openOutputFile(const std::string &filename)
Definition: main.cpp:372
KTest * kTest_fromFile(const char *path)
Definition: KTest.cpp:94
Statistic queryCounterexamples
virtual unsigned getSymbolicPathStreamID(const ExecutionState &state)=0
Statistic forks
The number of process forks.
void processTestCase(const ExecutionState &state, const char *errorMessage, const char *errorSuffix)
Definition: main.cpp:406
static bool interrupted
Definition: main.cpp:952
static const char * unsafeExternals[]
Definition: main.cpp:856
Interpreter * m_interpreter
Definition: main.cpp:221
static void parseArguments(int argc, char **argv)
Definition: main.cpp:634
FILE * klee_warning_file
Definition: Common.cpp:22
void kTest_free(KTest *bo)
Definition: KTest.cpp:229
Statistic instructions
static Interpreter * theInterpreter
Definition: main.cpp:950
unsigned m_pathsExplored
Definition: main.cpp:228
Statistic queriesInvalid
Statistic queryConstructs