about summary refs log tree commit diff homepage
path: root/tools
diff options
context:
space:
mode:
authorPavel Yatcheniy <yatcheniy.pavel@huawei.com>2021-01-28 17:51:04 +0300
committerCristian Cadar <c.cadar@imperial.ac.uk>2022-09-14 20:40:10 +0100
commit4ccb533158d40e15db9e9f2ade9bb28c3f83f38e (patch)
tree5086367ddc73b849c41d7621d41a00eacc895872 /tools
parent39f8069db879e1f859c60c821092452748b4ba37 (diff)
downloadklee-4ccb533158d40e15db9e9f2ade9bb28c3f83f38e.tar.gz
Support UBSan-enabled binaries
Diffstat (limited to 'tools')
-rw-r--r--tools/klee/main.cpp17
1 files changed, 13 insertions, 4 deletions
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index d94cdc76..7d938ab2 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -187,6 +187,10 @@ namespace {
                    cl::init(false),
                    cl::cat(LinkCat));
 
+  cl::opt<bool> WithUBSanRuntime("ubsan-runtime",
+                                 cl::desc("Link with UBSan runtime."),
+                                 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 "
@@ -794,10 +798,6 @@ static const char *modelledExternals[] = {
   "_Znwj",
   "_Znam",
   "_Znwm",
-  "__ubsan_handle_add_overflow",
-  "__ubsan_handle_sub_overflow",
-  "__ubsan_handle_mul_overflow",
-  "__ubsan_handle_divrem_overflow",
 };
 
 // Symbols we aren't going to warn about
@@ -1265,6 +1265,15 @@ int main(int argc, char **argv, char **envp) {
     preparePOSIX(loadedModules, libcPrefix);
   }
 
+  if (WithUBSanRuntime) {
+    SmallString<128> Path(Opts.LibraryDir);
+    llvm::sys::path::append(Path, "libkleeUBSan" + opt_suffix + ".bca");
+    if (!klee::loadFile(Path.c_str(), mainModule->getContext(), loadedModules,
+                        errorMsg))
+      klee_error("error loading UBSan support '%s': %s", Path.c_str(),
+                 errorMsg.c_str());
+  }
+
   if (Libcxx) {
 #ifndef SUPPORT_KLEE_LIBCXX
     klee_error("KLEE was not compiled with libc++ support");