diff options
| -rw-r--r-- | include/klee/Core/Interpreter.h | 8 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 3 | ||||
| -rw-r--r-- | tools/klee/main.cpp | 33 |
3 files changed, 33 insertions, 11 deletions
diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h index de64030d..541881a9 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -54,14 +54,16 @@ public: struct ModuleOptions { std::string LibraryDir; std::string EntryPoint; + std::string OptSuffix; bool Optimize; bool CheckDivZero; bool CheckOvershift; ModuleOptions(const std::string &_LibraryDir, - const std::string &_EntryPoint, bool _Optimize, - bool _CheckDivZero, bool _CheckOvershift) - : LibraryDir(_LibraryDir), EntryPoint(_EntryPoint), Optimize(_Optimize), + const std::string &_EntryPoint, const std::string &_OptSuffix, + bool _Optimize, bool _CheckDivZero, bool _CheckOvershift) + : LibraryDir(_LibraryDir), EntryPoint(_EntryPoint), + OptSuffix(_OptSuffix), Optimize(_Optimize), CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift) {} }; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index ea386cfd..e3e33aa2 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -520,7 +520,8 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &modules, // Link with KLEE intrinsics library before running any optimizations SmallString<128> LibPath(opts.LibraryDir); - llvm::sys::path::append(LibPath, "libkleeRuntimeIntrinsic.bca"); + llvm::sys::path::append(LibPath, + "libkleeRuntimeIntrinsic" + opts.OptSuffix + ".bca"); std::string error; if (!klee::loadFile(LibPath.str(), modules[0]->getContext(), modules, error)) { diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 44fa4cc5..589cc9a2 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -195,6 +195,12 @@ namespace { cl::init(false), cl::cat(LinkCat)); + cl::opt<std::string> RuntimeBuild( + "runtime-build", + cl::desc("Link with versions of the runtime library that were built with " + "the provided configuration (default=" RUNTIME_CONFIGURATION + ")."), + cl::init(RUNTIME_CONFIGURATION), cl::cat(LinkCat)); /*** Checks options ***/ @@ -667,8 +673,7 @@ std::string KleeHandler::getRunTimeLibraryPath(const char *argv0) { KLEE_DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() << "Using build directory KLEE library runtime :"); libDir = KLEE_DIR; - llvm::sys::path::append(libDir,RUNTIME_CONFIGURATION); - llvm::sys::path::append(libDir,"lib"); + llvm::sys::path::append(libDir, "runtime/lib"); } KLEE_DEBUG_WITH_TYPE("klee_runtime", llvm::dbgs() << @@ -1239,18 +1244,30 @@ int main(int argc, char **argv, char **envp) { } llvm::Module *mainModule = M.get(); + + // Detect architecture + std::string opt_suffix = "64"; // Fall back to 64bit + if (mainModule->getTargetTriple().find("i686") != std::string::npos || + mainModule->getTargetTriple().find("i586") != std::string::npos || + mainModule->getTargetTriple().find("i486") != std::string::npos || + mainModule->getTargetTriple().find("i386") != std::string::npos) + opt_suffix = "32"; + + // Add additional user-selected suffix + opt_suffix += "_" + RuntimeBuild.getValue(); + // Push the module as the first entry loadedModules.emplace_back(std::move(M)); std::string LibraryDir = KleeHandler::getRunTimeLibraryPath(argv[0]); - Interpreter::ModuleOptions Opts(LibraryDir.c_str(), EntryPoint, + Interpreter::ModuleOptions Opts(LibraryDir.c_str(), EntryPoint, opt_suffix, /*Optimize=*/OptimizeModule, /*CheckDivZero=*/CheckDivZero, /*CheckOvershift=*/CheckOvershift); if (WithPOSIXRuntime) { SmallString<128> Path(Opts.LibraryDir); - llvm::sys::path::append(Path, "libkleeRuntimePOSIX.bca"); + llvm::sys::path::append(Path, "libkleeRuntimePOSIX" + opt_suffix + ".bca"); klee_message("NOTE: Using POSIX model: %s", Path.c_str()); if (!klee::loadFile(Path.c_str(), mainModule->getContext(), loadedModules, errorMsg)) @@ -1274,7 +1291,7 @@ int main(int argc, char **argv, char **envp) { klee_message("NOTE: Using libcxx : %s", LibcxxBC.c_str()); #ifdef SUPPORT_KLEE_EH_CXX SmallString<128> EhCxxPath(Opts.LibraryDir); - llvm::sys::path::append(EhCxxPath, "libklee-eh-cxx.bca"); + llvm::sys::path::append(EhCxxPath, "libkleeeh-cxx" + opt_suffix + ".bca"); if (!klee::loadFile(EhCxxPath.c_str(), mainModule->getContext(), loadedModules, errorMsg)) klee_error("error loading libklee-eh-cxx '%s': %s", EhCxxPath.c_str(), @@ -1287,7 +1304,8 @@ int main(int argc, char **argv, char **envp) { case LibcType::KleeLibc: { // FIXME: Find a reasonable solution for this. SmallString<128> Path(Opts.LibraryDir); - llvm::sys::path::append(Path, "libklee-libc.bca"); + llvm::sys::path::append(Path, + "libkleeRuntimeKLEELibc" + opt_suffix + ".bca"); if (!klee::loadFile(Path.c_str(), mainModule->getContext(), loadedModules, errorMsg)) klee_error("error loading klee libc '%s': %s", Path.c_str(), @@ -1296,7 +1314,8 @@ int main(int argc, char **argv, char **envp) { /* Falls through. */ case LibcType::FreeStandingLibc: { SmallString<128> Path(Opts.LibraryDir); - llvm::sys::path::append(Path, "libkleeRuntimeFreeStanding.bca"); + llvm::sys::path::append(Path, + "libkleeRuntimeFreeStanding" + opt_suffix + ".bca"); if (!klee::loadFile(Path.c_str(), mainModule->getContext(), loadedModules, errorMsg)) klee_error("error loading free standing support '%s': %s", Path.c_str(), |