12 files changed, 186 insertions, 0 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt
index b40b9414..d5830869 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -612,6 +612,49 @@ else()
 endif()
 
 ################################################################################
+# KLEE libcxx support
+################################################################################
+option(ENABLE_KLEE_LIBCXX "Enable libcxx for klee" OFF)
+if (ENABLE_KLEE_LIBCXX)
+  message(STATUS "klee-libcxx support enabled")
+  set(SUPPORT_KLEE_LIBCXX 1) # For config.h
+  set(KLEE_LIBCXX_EXTERNAL_OBJECT "" CACHE PATH "Path to llvm libcxx shared object")
+  if (NOT EXISTS "${KLEE_LIBCXX_EXTERNAL_OBJECT}")
+    message(FATAL_ERROR
+      "${KLEE_LIBCXX_EXTERNAL_OBJECT} does not exist. Try passing -DKLEE_LIBCXX_EXTERNAL_OBJECT=<path>")
+  endif()
+
+  if (NOT IS_DIRECTORY "${KLEE_LIBCXX_INCLUDE_DIR}")
+    message(FATAL_ERROR
+      "${KLEE_LIBCXX_INCLUDE_DIR} does not exist. Try passing -DKLEE_LIBCXX_INCLUDE_DIR=<path>")
+  endif()
+
+  set(KLEE_LIBCXX_BC_NAME "libcxx.so.bc")
+
+  # Make a symlink to KLEE_LIBCXX_EXTERNAL_OBJECT so KLEE can find it where it
+  # is expected.
+  file(MAKE_DIRECTORY "${KLEE_RUNTIME_DIRECTORY}")
+  execute_process(COMMAND ${CMAKE_COMMAND} -E create_symlink
+    "${KLEE_LIBCXX_EXTERNAL_OBJECT}"
+    "${KLEE_RUNTIME_DIRECTORY}/${KLEE_LIBCXX_BC_NAME}"
+  )
+  list(APPEND KLEE_COMPONENT_CXX_DEFINES
+    -DKLEE_LIBCXX_BC_NAME=\"${KLEE_LIBCXX_BC_NAME}\")
+
+  # Add libcxx to the install target. We install the original
+  # file rather than the symlink because CMake would just copy the symlink
+  # rather than the file.
+  install(FILES "${KLEE_LIBCXX_EXTERNAL_OBJECT}"
+    DESTINATION "${KLEE_INSTALL_RUNTIME_DIR}"
+    RENAME "${KLEE_LIBCXX_BC_NAME}"
+    )
+
+else()
+  message(STATUS "libcxx support disabled")
+  set(SUPPORT_KLEE_LIBCXX 0) # For config.h
+endif()
+
+################################################################################
 # Sanitizer support
 ################################################################################
 message(STATUS "${CMAKE_CXX_FLAGS}")
diff --git a/include/klee/Config/config.h.cmin b/include/klee/Config/config.h.cmin
index a7890fe7..2f406471 100644
--- a/include/klee/Config/config.h.cmin
+++ b/include/klee/Config/config.h.cmin
@@ -86,6 +86,9 @@
 /* klee-uclibc is supported */
 #cmakedefine SUPPORT_KLEE_UCLIBC @SUPPORT_KLEE_UCLIBC@
 
+/* libcxx is supported */
+#cmakedefine SUPPORT_KLEE_LIBCXX @SUPPORT_KLEE_LIBCXX@
+
 /* Configuration type of KLEE's runtime libraries */
 #define RUNTIME_CONFIGURATION "@KLEE_RUNTIME_BUILD_TYPE@"
 
diff --git a/runtime/Intrinsic/dso_handle.c b/runtime/Intrinsic/dso_handle.c
new file mode 100644
index 00000000..0db2281f
--- /dev/null
+++ b/runtime/Intrinsic/dso_handle.c
@@ -0,0 +1 @@
+void* __dso_handle = 0;
diff --git a/test/CXX/symex/libc++/atexit.cpp b/test/CXX/symex/libc++/atexit.cpp
new file mode 100644
index 00000000..3d9e6834
--- /dev/null
+++ b/test/CXX/symex/libc++/atexit.cpp
@@ -0,0 +1,15 @@
+// RUN: sh %S/compile_with_libcxx.sh "%llvmgxx" "%s" "%S" "%t" "%klee" "%libcxx_include" | FileCheck %s
+//
+// CHECK: Returning from main
+// CHECK: atexit_1
+// CHECK: atexit_2
+
+#include <iostream>
+#include <cstdlib>
+
+int main(int argc, char** args){
+  auto atexithandler2 = std::atexit([](){std::cout << "atexit_2" << std::endl;});
+  auto atexithandler1 = std::atexit([](){std::cout << "atexit_1" << std::endl;});
+  std::cout << "Returning from main" << std::endl;
+  return 0;
+}
diff --git a/test/CXX/symex/libc++/compile_with_libcxx.sh b/test/CXX/symex/libc++/compile_with_libcxx.sh
new file mode 100644
index 00000000..8c45ec62
--- /dev/null
+++ b/test/CXX/symex/libc++/compile_with_libcxx.sh
@@ -0,0 +1,15 @@
+set -x
+set -e
+set -o
+set -u
+
+COMPILER=$1
+FILENAME=$2
+CURDIR=$3
+TMPNAME=$4
+KLEE=$5
+INCLUDE_DIR=$6
+
+$COMPILER $FILENAME -std=c++11 -I ${INCLUDE_DIR} -emit-llvm -O0 -c -g -nostdinc++ -o ${TMPNAME}.bc
+rm -rf ${TMPNAME}.klee-out
+$KLEE --output-dir=${TMPNAME}.klee-out --no-output --exit-on-error --libc=uclibc --use-libcxx ${TMPNAME}.bc 2>&1
diff --git a/test/CXX/symex/libc++/cout.cpp b/test/CXX/symex/libc++/cout.cpp
new file mode 100644
index 00000000..2539b67f
--- /dev/null
+++ b/test/CXX/symex/libc++/cout.cpp
@@ -0,0 +1,9 @@
+// RUN: sh %S/compile_with_libcxx.sh "%llvmgxx" "%s" "%S" "%t" "%klee" "%libcxx_include"
+
+#include <iostream>
+
+int main(int argc, char** args){
+  std::cout << "cout" << std::endl;
+  std::cerr << "cerr" << std::endl;
+  return 0;
+}
diff --git a/test/CXX/symex/libc++/cout_sym.cpp b/test/CXX/symex/libc++/cout_sym.cpp
new file mode 100644
index 00000000..52e59f05
--- /dev/null
+++ b/test/CXX/symex/libc++/cout_sym.cpp
@@ -0,0 +1,14 @@
+// RUN: sh %S/compile_with_libcxx.sh "%llvmgxx" "%s" "%S" "%t" "%klee" "%libcxx_include"
+
+#include <iostream>
+#include "klee/klee.h"
+
+int main(int argc, char** args){
+  int x = klee_int("x");
+  if (x > 0){
+    std::cout << "greater: " << x << std::endl;
+  } else {
+    std::cout << "lower: " << x << std::endl;
+  }
+  return 0;
+}
diff --git a/test/CXX/symex/libc++/dynamic_cast.cpp b/test/CXX/symex/libc++/dynamic_cast.cpp
new file mode 100644
index 00000000..53e5bc69
--- /dev/null
+++ b/test/CXX/symex/libc++/dynamic_cast.cpp
@@ -0,0 +1,50 @@
+// RUN: sh %S/compile_with_libcxx.sh "%llvmgxx" "%s" "%S" "%t" "%klee" "%libcxx_include"
+
+// Copied from 'http://en.cppreference.com/w/cpp/language/dynamic_cast'
+
+struct V {
+    virtual void f() {};  // must be polymorphic to use runtime-checked dynamic_cast
+};
+struct A : virtual V {};
+struct B : virtual V {
+  B(V* v, A* a) {
+    // casts during construction (see the call in the constructor of D below)
+    dynamic_cast<B*>(v); // well-defined: v of type V*, V base of B, results in B*
+    dynamic_cast<B*>(a); // undefined behavior: a has type A*, A not a base of B
+  }
+};
+struct D : A, B {
+    D() : B((A*)this, this) { }
+};
+
+struct Base {
+    virtual ~Base() {}
+};
+
+struct Derived: Base {
+    virtual void name() {}
+};
+
+int main()
+{
+    D d; // the most derived object
+    A& a = d; // upcast, dynamic_cast may be used, but unnecessary
+    D& new_d = dynamic_cast<D&>(a); // downcast
+    B& new_b = dynamic_cast<B&>(a); // sidecast
+
+
+    Base* b1 = new Base;
+    if(Derived* d = dynamic_cast<Derived*>(b1))
+    {
+        d->name(); // safe to call
+    }
+
+    Base* b2 = new Derived;
+    if(Derived* d = dynamic_cast<Derived*>(b2))
+    {
+        d->name(); // safe to call
+    }
+
+    delete b1;
+    delete b2;
+}
diff --git a/test/CXX/symex/libc++/vector.cpp b/test/CXX/symex/libc++/vector.cpp
new file mode 100644
index 00000000..27f5daba
--- /dev/null
+++ b/test/CXX/symex/libc++/vector.cpp
@@ -0,0 +1,12 @@
+// RUN: sh %S/compile_with_libcxx.sh "%llvmgxx" "%s" "%S" "%t" "%klee" "%libcxx_include" | FileCheck %s
+
+// CHECK: KLEE: done: completed paths = 1
+
+#include "klee/klee.h"
+#include <vector>
+
+int main(int argc, char **args) {
+  std::vector<int> a;
+  a.push_back(klee_int("Test"));
+  return a.at(0);
+}
diff --git a/test/lit.cfg b/test/lit.cfg
index 7c5ed220..1dafa911 100644
--- a/test/lit.cfg
+++ b/test/lit.cfg
@@ -155,6 +155,9 @@ config.substitutions.append(
   ('%gentmp', os.path.join(klee_src_root, 'scripts/genTempFiles.sh'))
 )
 
+config.substitutions.append(
+    ('%libcxx_include', getattr(config, 'libcxx_include_dir', None)))
+
 # Add feature for the LLVM version in use, so it can be tested in REQUIRES and
 # XFAIL checks. We also add "not-XXX" variants, for the same reason.
 known_llvm_versions = set(["3.4", "3.5", "3.6", "3.7", "3.8", "3.9"])
diff --git a/test/lit.site.cfg.in b/test/lit.site.cfg.in
index 7839b66e..e0827559 100644
--- a/test/lit.site.cfg.in
+++ b/test/lit.site.cfg.in
@@ -9,6 +9,8 @@ config.klee_obj_root = "@KLEE_BINARY_DIR@"
 config.klee_tools_dir = "@KLEE_TOOLS_DIR@"
 config.llvm_tools_dir = "@LLVM_TOOLS_DIR@"
 
+config.libcxx_include_dir = "@KLEE_LIBCXX_INCLUDE_DIR@"
+
 # Needed to check if a hack needs to be applied
 config.llvm_version_major = "@LLVM_VERSION_MAJOR@"
 config.llvm_version_minor = "@LLVM_VERSION_MINOR@"
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 9219134c..4e04dacc 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -287,6 +287,11 @@ namespace {
            cl::desc("Use a watchdog process to enforce --max-time."),
            cl::init(0),
            cl::cat(TerminationCat));
+
+  cl::opt<bool>
+  UseLibcxx("use-libcxx",
+           cl::desc("Link the llvm libc++ library into the bitcode"),
+           cl::init(0));
 }
 
 namespace klee {
@@ -1262,6 +1267,20 @@ int main(int argc, char **argv, char **envp) {
     preparePOSIX(loadedModules, libcPrefix);
   }
 
+  if (UseLibcxx) {
+#ifndef SUPPORT_KLEE_LIBCXX
+    klee_error("Klee was not compiled with libcxx support");
+#else
+    SmallString<128> LibcxxBC(Opts.LibraryDir);
+    llvm::sys::path::append(LibcxxBC, KLEE_LIBCXX_BC_NAME);
+    if (!klee::loadFile(LibcxxBC.c_str(), mainModule->getContext(), loadedModules,
+                        errorMsg))
+      klee_error("error loading free standing support '%s': %s",
+                 LibcxxBC.c_str(), errorMsg.c_str());
+    klee_message("NOTE: Using libcxx : %s", LibcxxBC.c_str());
+#endif
+  }
+
   switch (Libc) {
   case LibcType::KleeLibc: {
     // FIXME: Find a reasonable solution for this.