diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/klee/main.cpp | 279 |
1 files changed, 139 insertions, 140 deletions
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index aba247e7..56471e84 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -78,56 +78,56 @@ namespace { Environ("environ", cl::desc("Parse environ from given file (in \"env\" format)")); cl::list<std::string> - InputArgv(cl::ConsumeAfter, + InputArgv(cl::ConsumeAfter, cl::desc("<program arguments>...")); cl::opt<bool> - NoOutput("no-output", + NoOutput("no-output", cl::desc("Don't generate test files")); - + cl::opt<bool> - WarnAllExternals("warn-all-externals", + WarnAllExternals("warn-all-externals", cl::desc("Give initial warning for all externals.")); - + cl::opt<bool> - WriteCVCs("write-cvcs", + WriteCVCs("write-cvcs", cl::desc("Write .cvc files for each test case")); cl::opt<bool> - WritePCs("write-pcs", + WritePCs("write-pcs", cl::desc("Write .pc files for each test case")); - + cl::opt<bool> WriteSMT2s("write-smt2s", cl::desc("Write .smt2 (SMT-LIBv2) files for each test case")); cl::opt<bool> - WriteCov("write-cov", + WriteCov("write-cov", cl::desc("Write coverage information for each test case")); - + cl::opt<bool> - WriteTestInfo("write-test-info", + WriteTestInfo("write-test-info", cl::desc("Write additional test case information")); - + cl::opt<bool> - WritePaths("write-paths", + WritePaths("write-paths", cl::desc("Write .path files for each test case")); - + cl::opt<bool> - WriteSymPaths("write-sym-paths", + WriteSymPaths("write-sym-paths", cl::desc("Write .sym.path files for each test case")); - + cl::opt<bool> - ExitOnError("exit-on-error", + ExitOnError("exit-on-error", cl::desc("Exit if errors occur")); - + enum LibcType { NoLibc, KleeLibc, UcLibc }; cl::opt<LibcType> - Libc("libc", + Libc("libc", cl::desc("Choose libc version (none by default)."), cl::values(clEnumValN(NoLibc, "none", "Don't link in a libc"), clEnumValN(KleeLibc, "klee", "Link in klee libc"), @@ -135,19 +135,19 @@ namespace { clEnumValEnd), cl::init(NoLibc)); - + cl::opt<bool> - WithPOSIXRuntime("posix-runtime", + WithPOSIXRuntime("posix-runtime", 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"), cl::init(false)); - + cl::opt<bool> - OptimizeModule("optimize", + OptimizeModule("optimize", cl::desc("Optimize before execution"), cl::init(false)); cl::opt<bool> - CheckDivZero("check-div-zero", + CheckDivZero("check-div-zero", cl::desc("Inject checks for division-by-zero"), cl::init(true)); @@ -157,15 +157,15 @@ namespace { cl::init(true)); cl::opt<std::string> - OutputDir("output-dir", + OutputDir("output-dir", cl::desc("Directory to write results in (defaults to klee-out-N)"), cl::init("")); cl::opt<bool> - ReplayKeepSymbolic("replay-keep-symbolic", + ReplayKeepSymbolic("replay-keep-symbolic", cl::desc("Replay the test cases only by asserting " "the bytes, not necessarily making them concrete.")); - + cl::list<std::string> ReplayOutFile("replay-out", cl::desc("Specify an out file to replay"), @@ -183,17 +183,17 @@ namespace { cl::list<std::string> SeedOutFile("seed-out"); - + cl::list<std::string> SeedOutDir("seed-out-dir"); - + cl::opt<unsigned> MakeConcreteSymbolic("make-concrete-symbolic", cl::desc("Probabilistic rate at which to make concrete reads symbolic, " "i.e. approximately 1 in n concrete reads will be made symbolic (0=off, 1=all). " "Used for testing."), cl::init(0)); - + cl::opt<unsigned> StopAfterNTests("stop-after-n-tests", cl::desc("Stop execution after generating the given number of tests. Extra tests corresponding to partially explored paths will also be dumped."), @@ -236,7 +236,7 @@ public: void setInterpreter(Interpreter *i); void processTestCase(const ExecutionState &state, - const char *errorMessage, + const char *errorMessage, const char *errorSuffix); std::string getOutputFilename(const std::string &filename); @@ -245,11 +245,11 @@ public: llvm::raw_fd_ostream *openTestFile(const std::string &suffix, unsigned id); // load a .out file - static void loadOutFile(std::string name, + static void loadOutFile(std::string name, std::vector<unsigned char> &buffer); // load a .path file - static void loadPathFile(std::string name, + static void loadPathFile(std::string name, std::vector<bool> &buffer); static void getOutFiles(std::string path, @@ -258,7 +258,7 @@ public: static std::string getRunTimeLibraryPath(const char *argv0); }; -KleeHandler::KleeHandler(int argc, char **argv) +KleeHandler::KleeHandler(int argc, char **argv) : m_interpreter(0), m_pathWriter(0), m_symPathWriter(0), @@ -404,7 +404,7 @@ llvm::raw_fd_ostream *KleeHandler::openTestFile(const std::string &suffix, /* Outputs all files (.ktest, .pc, .cov etc.) describing a test case */ void KleeHandler::processTestCase(const ExecutionState &state, - const char *errorMessage, + const char *errorMessage, const char *errorSuffix) { if (errorMessage && ExitOnError) { llvm::errs() << "EXITING ON ERROR:\n" << errorMessage << "\n"; @@ -423,7 +423,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, unsigned id = ++m_testIndex; if (success) { - KTest b; + KTest b; b.numArgs = m_argc; b.args = m_argv; b.symArgvs = 0; @@ -439,11 +439,11 @@ void KleeHandler::processTestCase(const ExecutionState &state, assert(o->bytes); std::copy(out[i].second.begin(), out[i].second.end(), o->bytes); } - + if (!kTest_toFile(&b, getOutputFilename(getTestFilename("ktest", id)).c_str())) { klee_warning("unable to write output test case, losing it"); } - + for (unsigned i=0; i<b.numObjects; i++) delete[] b.objects[i].bytes; delete[] b.objects; @@ -454,7 +454,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, *f << errorMessage; delete f; } - + if (m_pathWriter) { std::vector<unsigned char> concreteBranches; m_pathWriter->readStream(m_interpreter->getPathStreamID(state), @@ -467,7 +467,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, } delete f; } - + if (errorMessage || WritePCs) { std::string constraints; m_interpreter->getConstraintLog(state, constraints,Interpreter::KQUERY); @@ -483,9 +483,9 @@ void KleeHandler::processTestCase(const ExecutionState &state, *f << constraints; delete f; } - + if(WriteSMT2s) { - std::string constraints; + std::string constraints; m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2); llvm::raw_ostream *f = openTestFile("smt2", id); *f << constraints; @@ -524,7 +524,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, if (WriteTestInfo) { double elapsed_time = util::getWallTime() - start_time; llvm::raw_ostream *f = openTestFile("info", id); - *f << "Time to generate test case: " + *f << "Time to generate test case: " << elapsed_time << "s\n"; delete f; } @@ -532,7 +532,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, } // load a .path file -void KleeHandler::loadPathFile(std::string name, +void KleeHandler::loadPathFile(std::string name, std::vector<bool> &buffer) { std::ifstream f(name.c_str(), std::ios::in | std::ios::binary); @@ -648,7 +648,7 @@ static int initEnv(Module *mainModule) { */ Function *mainFn = mainModule->getFunction("main"); - + if (mainFn->arg_size() < 2) { klee_error("Cannot handle ""--posix-runtime"" when main() has less than two arguments.\n"); } @@ -657,23 +657,23 @@ static int initEnv(Module *mainModule) { Value* oldArgc = mainFn->arg_begin(); Value* oldArgv = ++mainFn->arg_begin(); - - AllocaInst* argcPtr = + + AllocaInst* argcPtr = new AllocaInst(oldArgc->getType(), "argcPtr", firstInst); - AllocaInst* argvPtr = + AllocaInst* argvPtr = new AllocaInst(oldArgv->getType(), "argvPtr", firstInst); /* Insert void klee_init_env(int* argc, char*** argv) */ std::vector<const Type*> params; params.push_back(Type::getInt32Ty(getGlobalContext())); params.push_back(Type::getInt32Ty(getGlobalContext())); - Function* initEnvFn = + Function* initEnvFn = cast<Function>(mainModule->getOrInsertFunction("klee_init_env", Type::getVoidTy(getGlobalContext()), argcPtr->getType(), argvPtr->getType(), NULL)); - assert(initEnvFn); + assert(initEnvFn); std::vector<Value*> args; args.push_back(argcPtr); args.push_back(argvPtr); @@ -681,12 +681,12 @@ static int initEnv(Module *mainModule) { Instruction* initEnvCall = CallInst::Create(initEnvFn, args, "", firstInst); #else - Instruction* initEnvCall = CallInst::Create(initEnvFn, args.begin(), args.end(), + Instruction* initEnvCall = CallInst::Create(initEnvFn, args.begin(), args.end(), "", firstInst); #endif Value *argc = new LoadInst(argcPtr, "newArgc", firstInst); Value *argv = new LoadInst(argvPtr, "newArgv", firstInst); - + oldArgc->replaceAllUsesWith(argc); oldArgv->replaceAllUsesWith(argv); @@ -708,54 +708,54 @@ static const char *modelledExternals[] = { "_ZTVN10__cxxabiv121__vmi_class_type_infoE", // special functions - "_assert", - "__assert_fail", - "__assert_rtn", - "calloc", - "_exit", - "exit", - "free", - "abort", - "klee_abort", - "klee_assume", + "_assert", + "__assert_fail", + "__assert_rtn", + "calloc", + "_exit", + "exit", + "free", + "abort", + "klee_abort", + "klee_assume", "klee_check_memory_access", "klee_define_fixed_object", - "klee_get_errno", + "klee_get_errno", "klee_get_valuef", "klee_get_valued", "klee_get_valuel", "klee_get_valuell", "klee_get_value_i32", "klee_get_value_i64", - "klee_get_obj_size", - "klee_is_symbolic", - "klee_make_symbolic", - "klee_mark_global", - "klee_merge", + "klee_get_obj_size", + "klee_is_symbolic", + "klee_make_symbolic", + "klee_mark_global", + "klee_merge", "klee_prefer_cex", - "klee_print_expr", - "klee_print_range", - "klee_report_error", + "klee_print_expr", + "klee_print_range", + "klee_report_error", "klee_set_forking", - "klee_silent_exit", - "klee_warning", - "klee_warning_once", + "klee_silent_exit", + "klee_warning", + "klee_warning_once", "klee_alias_function", "klee_stack_trace", #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1) "llvm.dbg.declare", "llvm.dbg.value", #endif - "llvm.va_start", - "llvm.va_end", - "malloc", - "realloc", - "_ZdaPv", - "_ZdlPv", - "_Znaj", - "_Znwj", - "_Znam", - "_Znwm", + "llvm.va_start", + "llvm.va_end", + "malloc", + "realloc", + "_ZdaPv", + "_ZdlPv", + "_Znaj", + "_Znwj", + "_Znam", + "_Znwm", "__ubsan_handle_add_overflow", "__ubsan_handle_sub_overflow", "__ubsan_handle_mul_overflow", @@ -804,7 +804,7 @@ static const char *dontCareExternals[] = { "uname", // fp stuff we just don't worry about yet - "frexp", + "frexp", "ldexp", "__isnan", "__signbit", @@ -840,15 +840,15 @@ static const char *unsafeExternals[] = { #define NELEMS(array) (sizeof(array)/sizeof(array[0])) void externalsAndGlobalsCheck(const Module *m) { std::map<std::string, bool> externals; - std::set<std::string> modelled(modelledExternals, + std::set<std::string> modelled(modelledExternals, modelledExternals+NELEMS(modelledExternals)); - std::set<std::string> dontCare(dontCareExternals, + std::set<std::string> dontCare(dontCareExternals, dontCareExternals+NELEMS(dontCareExternals)); - std::set<std::string> unsafe(unsafeExternals, + std::set<std::string> unsafe(unsafeExternals, unsafeExternals+NELEMS(unsafeExternals)); switch (Libc) { - case KleeLibc: + case KleeLibc: dontCare.insert(dontCareKlee, dontCareKlee+NELEMS(dontCareKlee)); break; case UcLibc: @@ -858,40 +858,39 @@ void externalsAndGlobalsCheck(const Module *m) { case NoLibc: /* silence compiler warning */ break; } - if (WithPOSIXRuntime) dontCare.insert("syscall"); - for (Module::const_iterator fnIt = m->begin(), fn_ie = m->end(); + for (Module::const_iterator fnIt = m->begin(), fn_ie = m->end(); fnIt != fn_ie; ++fnIt) { if (fnIt->isDeclaration() && !fnIt->use_empty()) externals.insert(std::make_pair(fnIt->getName(), false)); - for (Function::const_iterator bbIt = fnIt->begin(), bb_ie = fnIt->end(); + for (Function::const_iterator bbIt = fnIt->begin(), bb_ie = fnIt->end(); bbIt != bb_ie; ++bbIt) { - for (BasicBlock::const_iterator it = bbIt->begin(), ie = bbIt->end(); + for (BasicBlock::const_iterator it = bbIt->begin(), ie = bbIt->end(); it != ie; ++it) { if (const CallInst *ci = dyn_cast<CallInst>(it)) { if (isa<InlineAsm>(ci->getCalledValue())) { klee_warning_once(&*fnIt, - "function \"%s\" has inline asm", + "function \"%s\" has inline asm", fnIt->getName().data()); } } } } } - for (Module::const_global_iterator - it = m->global_begin(), ie = m->global_end(); + for (Module::const_global_iterator + it = m->global_begin(), ie = m->global_end(); it != ie; ++it) if (it->isDeclaration() && !it->use_empty()) externals.insert(std::make_pair(it->getName(), true)); // and remove aliases (they define the symbol after global // initialization) - for (Module::const_alias_iterator - it = m->alias_begin(), ie = m->alias_end(); + for (Module::const_alias_iterator + it = m->alias_begin(), ie = m->alias_end(); it != ie; ++it) { - std::map<std::string, bool>::iterator it2 = + std::map<std::string, bool>::iterator it2 = externals.find(it->getName()); if (it2!=externals.end()) externals.erase(it2); @@ -902,7 +901,7 @@ void externalsAndGlobalsCheck(const Module *m) { it = externals.begin(), ie = externals.end(); it != ie; ++it) { const std::string &ext = it->first; - if (!modelled.count(ext) && (WarnAllExternals || + if (!modelled.count(ext) && (WarnAllExternals || !dontCare.count(ext))) { if (unsafe.count(ext)) { foundUnsafe.insert(*it); @@ -962,12 +961,12 @@ static void interrupt_handle_watchdog() { // the state data before going ahead and killing it. static void halt_via_gdb(int pid) { char buffer[256]; - sprintf(buffer, + sprintf(buffer, "gdb --batch --eval-command=\"p halt_execution()\" " "--eval-command=detach --pid=%d &> /dev/null", pid); // fprintf(stderr, "KLEE: WATCHDOG: running: %s\n", buffer); - if (system(buffer)==-1) + if (system(buffer)==-1) perror("system"); } @@ -1025,7 +1024,7 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir) FunctionType::get(Type::getVoidTy(getGlobalContext()), std::vector<LLVM_TYPE_Q Type*>(), true)); - + // force various imports if (WithPOSIXRuntime) { LLVM_TYPE_Q llvm::Type *i8Ty = Type::getInt8Ty(getGlobalContext()); @@ -1075,7 +1074,7 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir) } } } - + mainModule = klee::linkWithLibrary(mainModule, uclibcBCA.c_str()); assert(mainModule && "unable to link with uclibc"); @@ -1097,9 +1096,9 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir) // the environment arguments to what uclibc expects (following // argv), since it does not explicitly take an envp argument. Function *userMainFn = mainModule->getFunction("main"); - assert(userMainFn && "unable to get user main"); + assert(userMainFn && "unable to get user main"); Function *uclibcMainFn = mainModule->getFunction("__uClibc_main"); - assert(uclibcMainFn && "unable to get uclibc main"); + assert(uclibcMainFn && "unable to get uclibc main"); userMainFn->setName("__user_main"); const FunctionType *ft = uclibcMainFn->getFunctionType(); @@ -1109,16 +1108,16 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir) fArgs.push_back(ft->getParamType(1)); // argc fArgs.push_back(ft->getParamType(2)); // argv Function *stub = Function::Create(FunctionType::get(Type::getInt32Ty(getGlobalContext()), fArgs, false), - GlobalVariable::ExternalLinkage, - "main", - mainModule); + GlobalVariable::ExternalLinkage, + "main", + mainModule); BasicBlock *bb = BasicBlock::Create(getGlobalContext(), "entry", stub); std::vector<llvm::Value*> args; - args.push_back(llvm::ConstantExpr::getBitCast(userMainFn, + args.push_back(llvm::ConstantExpr::getBitCast(userMainFn, ft->getParamType(0))); args.push_back(stub->arg_begin()); // argc - args.push_back(++stub->arg_begin()); // argv + args.push_back(++stub->arg_begin()); // argv args.push_back(Constant::getNullValue(ft->getParamType(3))); // app_init args.push_back(Constant::getNullValue(ft->getParamType(4))); // app_fini args.push_back(Constant::getNullValue(ft->getParamType(5))); // rtld_fini @@ -1128,7 +1127,7 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir) #else CallInst::Create(uclibcMainFn, args.begin(), args.end(), "", bb); #endif - + new UnreachableInst(getGlobalContext(), bb); klee_message("NOTE: Using klee-uclibc : %s", uclibcBCA.c_str()); @@ -1183,7 +1182,7 @@ int main(int argc, char **argv, char **envp) { if (time > nextStep) { ++level; - + if (level==1) { fprintf(stderr, "KLEE: WATCHDOG: time expired, attempting halt via INT\n"); kill(pid, SIGINT); @@ -1265,10 +1264,10 @@ int main(int argc, char **argv, char **envp) { std::string LibraryDir = KleeHandler::getRunTimeLibraryPath(argv[0]); Interpreter::ModuleOptions Opts(LibraryDir.c_str(), - /*Optimize=*/OptimizeModule, + /*Optimize=*/OptimizeModule, /*CheckDivZero=*/CheckDivZero, /*CheckOvershift=*/CheckOvershift); - + switch (Libc) { case NoLibc: /* silence compiler warning */ break; @@ -1297,7 +1296,7 @@ int main(int argc, char **argv, char **envp) { klee_message("NOTE: Using model: %s", Path.c_str()); mainModule = klee::linkWithLibrary(mainModule, Path.c_str()); assert(mainModule && "unable to link with simple model"); - } + } // Get the desired main function. klee_main initializes uClibc // locale and other data and then calls main. @@ -1333,16 +1332,16 @@ int main(int argc, char **argv, char **envp) { pEnvp = envp; } - pArgc = InputArgv.size() + 1; + pArgc = InputArgv.size() + 1; pArgv = new char *[pArgc]; for (unsigned i=0; i<InputArgv.size()+1; i++) { std::string &arg = (i==0 ? InputFile : InputArgv[i-1]); unsigned size = arg.size() + 1; char *pArg = new char[size]; - + std::copy(arg.begin(), arg.end(), pArg); pArg[size - 1] = 0; - + pArgv[i] = pArg; } @@ -1355,7 +1354,7 @@ int main(int argc, char **argv, char **envp) { Interpreter::InterpreterOptions IOpts; IOpts.MakeConcreteSymbolic = MakeConcreteSymbolic; KleeHandler *handler = new KleeHandler(pArgc, pArgv); - Interpreter *interpreter = + Interpreter *interpreter = theInterpreter = Interpreter::create(IOpts, handler); handler->setInterpreter(interpreter); @@ -1365,7 +1364,7 @@ int main(int argc, char **argv, char **envp) { } infoFile << "PID: " << getpid() << "\n"; - const Module *finalModule = + const Module *finalModule = interpreter->setModule(mainModule, Opts); externalsAndGlobalsCheck(finalModule); @@ -1388,7 +1387,7 @@ int main(int argc, char **argv, char **envp) { for (std::vector<std::string>::iterator it = ReplayOutDir.begin(), ie = ReplayOutDir.end(); it != ie; ++it) - KleeHandler::getOutFiles(*it, outFiles); + KleeHandler::getOutFiles(*it, outFiles); std::vector<KTest*> kTests; for (std::vector<std::string>::iterator it = outFiles.begin(), ie = outFiles.end(); @@ -1437,7 +1436,7 @@ int main(int argc, char **argv, char **envp) { exit(1); } seeds.push_back(out); - } + } for (std::vector<std::string>::iterator it = SeedOutDir.begin(), ie = SeedOutDir.end(); it != ie; ++it) { @@ -1458,7 +1457,7 @@ int main(int argc, char **argv, char **envp) { exit(1); } } - + if (!seeds.empty()) { llvm::errs() << "KLEE: using " << seeds.size() << " seeds\n"; interpreter->useSeeds(&seeds); @@ -1476,7 +1475,7 @@ int main(int argc, char **argv, char **envp) { seeds.pop_back(); } } - + t[1] = time(NULL); strftime(buf, sizeof(buf), "Finished: %Y-%m-%d %H:%M:%S\n", localtime(&t[1])); infoFile << buf; @@ -1492,31 +1491,31 @@ int main(int argc, char **argv, char **envp) { delete interpreter; - uint64_t queries = + uint64_t queries = *theStatisticManager->getStatisticByName("Queries"); - uint64_t queriesValid = + uint64_t queriesValid = *theStatisticManager->getStatisticByName("QueriesValid"); - uint64_t queriesInvalid = + uint64_t queriesInvalid = *theStatisticManager->getStatisticByName("QueriesInvalid"); - uint64_t queryCounterexamples = + uint64_t queryCounterexamples = *theStatisticManager->getStatisticByName("QueriesCEX"); - uint64_t queryConstructs = + uint64_t queryConstructs = *theStatisticManager->getStatisticByName("QueriesConstructs"); - uint64_t instructions = + uint64_t instructions = *theStatisticManager->getStatisticByName("Instructions"); - uint64_t forks = + uint64_t forks = *theStatisticManager->getStatisticByName("Forks"); - handler->getInfoStream() + handler->getInfoStream() << "KLEE: done: explored paths = " << 1 + forks << "\n"; // Write some extra information in the info file which users won't // necessarily care about or understand. if (queries) - handler->getInfoStream() - << "KLEE: done: avg. constructs per query = " - << queryConstructs / queries << "\n"; - handler->getInfoStream() + handler->getInfoStream() + << "KLEE: done: avg. constructs per query = " + << queryConstructs / queries << "\n"; + handler->getInfoStream() << "KLEE: done: total queries = " << queries << "\n" << "KLEE: done: valid queries = " << queriesValid << "\n" << "KLEE: done: invalid queries = " << queriesInvalid << "\n" @@ -1524,11 +1523,11 @@ int main(int argc, char **argv, char **envp) { std::stringstream stats; stats << "\n"; - stats << "KLEE: done: total instructions = " + stats << "KLEE: done: total instructions = " << instructions << "\n"; - stats << "KLEE: done: completed paths = " + stats << "KLEE: done: completed paths = " << handler->getNumPathsExplored() << "\n"; - stats << "KLEE: done: generated tests = " + stats << "KLEE: done: generated tests = " << handler->getNumTestCases() << "\n"; bool useColors = llvm::errs().is_displayed(); |