aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2020-04-06 14:49:04 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2020-11-04 15:14:47 +0000
commit6bc2bf207cde155fa4abbdc5be4e92e766caa6d4 (patch)
tree162a683b2849603eedf8ca25f4b30b9719fe26b5
parent6156b4eeb9a429ccc370782d719d0d6c787a6f72 (diff)
downloadklee-6bc2bf207cde155fa4abbdc5be4e92e766caa6d4.tar.gz
Link to the different runtime libraries depending on the application to test.
Currently, only 32bit vs. 64bit is supported.
-rw-r--r--include/klee/Core/Interpreter.h8
-rw-r--r--lib/Core/Executor.cpp3
-rw-r--r--tools/klee/main.cpp33
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(),