about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorOmer Anson <oaanson@gmail.com>2016-02-22 23:13:34 +0200
committerOmer Anson <oaanson@gmail.com>2016-02-25 20:52:39 +0200
commit66f53aac10962db150aec07b96f3b0a756eef28b (patch)
treebd9c2a0a225ebdd3a475158c4004b8a51f78f030
parentf76b6c5fe0ce8920ee6edb13802f857dae49e785 (diff)
downloadklee-66f53aac10962db150aec07b96f3b0a756eef28b.tar.gz
Added support to load libraries from command line
This allows a user to invoke klee with specific libraries to load from
command line. This is an attempt to allow klee to run on applications
linked to external libraries.

The libraries still have to be compiled specially for klee, in a manner
similar to klee-uclibc, i.e. archives (build with llvm-ar) of llvm IR
files.
-rw-r--r--test/Feature/LinkLLVMLib.c24
-rw-r--r--tools/klee/main.cpp13
2 files changed, 37 insertions, 0 deletions
diff --git a/test/Feature/LinkLLVMLib.c b/test/Feature/LinkLLVMLib.c
new file mode 100644
index 00000000..7639bfef
--- /dev/null
+++ b/test/Feature/LinkLLVMLib.c
@@ -0,0 +1,24 @@
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc -DLINK_LLVM_LIB_TEST_LIB
+// RUN: llvm-ar r %t1.a %t1.bc
+//
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t2.bc -DLINK_LLVM_LIB_TEST_EXEC
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --link-llvm-lib %t1.a --output-dir=%t.klee-out --emit-all-errors %t2.bc 2>&1 | FileCheck %s
+
+#ifdef LINK_LLVM_LIB_TEST_EXEC
+extern void printint(int d);
+
+int main(int argc, char * argv[]) {
+	printint(5);
+	// CHECK: KLEE: WARNING ONCE: calling external: printf
+	return 0;
+}
+#endif
+
+#ifdef LINK_LLVM_LIB_TEST_LIB
+#include <stdio.h>
+
+void printint(int d) {
+	printf("%d\n", d);
+}
+#endif
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 665cc842..0dfa4399 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -190,6 +190,11 @@ namespace {
   cl::list<std::string>
   SeedOutDir("seed-out-dir");
 
+  cl::list<std::string>
+  LinkLibraries("link-llvm-lib",
+		cl::desc("Link the given libraries before execution"),
+		cl::value_desc("library file"));
+
   cl::opt<unsigned>
   MakeConcreteSymbolic("make-concrete-symbolic",
                        cl::desc("Probabilistic rate at which to make concrete reads symbolic, "
@@ -1303,6 +1308,14 @@ int main(int argc, char **argv, char **envp) {
     assert(mainModule && "unable to link with simple model");
   }
 
+  std::vector<std::string>::iterator libs_it;
+  std::vector<std::string>::iterator libs_ie;
+  for (libs_it = LinkLibraries.begin(), libs_ie = LinkLibraries.end();
+          libs_it != libs_ie; ++libs_it) {
+    const char * libFilename = libs_it->c_str();
+    klee_message("Linking in library: %s.\n", libFilename);
+    mainModule = klee::linkWithLibrary(mainModule, libFilename);
+  }
   // Get the desired main function.  klee_main initializes uClibc
   // locale and other data and then calls main.
   Function *mainFn = mainModule->getFunction(EntryPoint);