about summary refs log tree commit diff homepage
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(),