Make Uclibc support a runtime option, not a compile-time one.

6 files changed, 14 insertions, 41 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index a92c2f2e..16e33ea9 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -507,11 +507,6 @@ file(MAKE_DIRECTORY ${KLEE_RUNTIME_DIRECTORY})
 option(ENABLE_POSIX_RUNTIME "Enable KLEE's POSIX runtime" OFF)
 if (ENABLE_POSIX_RUNTIME)
   message(STATUS "POSIX runtime enabled")
-  if (NOT ENABLE_KLEE_UCLIBC)
-    message(WARNING "Enabling POSIX runtime without klee-uclibc support."
-      "The runtime might not work without it. Pass `-DENABLE_KLEE_UCLIBC=ON`"
-      " to enable klee-uclibc support.")
-  endif()
 else()
   message(STATUS "POSIX runtime disabled")
 endif()
@@ -519,38 +514,25 @@ endif()
 ################################################################################
 # KLEE uclibc support
 ################################################################################
-option(ENABLE_KLEE_UCLIBC "Enable support for klee-uclibc" OFF)
-if (ENABLE_KLEE_UCLIBC)
-  message(STATUS "klee-uclibc support enabled")
-  set(SUPPORT_KLEE_UCLIBC 1) # For config.h
-  set(KLEE_UCLIBC_PATH "" CACHE PATH "Path to klee-uclibc root directory")
-  if (NOT IS_DIRECTORY "${KLEE_UCLIBC_PATH}")
-    message(FATAL_ERROR
-      "KLEE_UCLIBC_PATH (\"${KLEE_UCLIBC_PATH}\") is not a valid directory.\n"
-      "Try passing -DKLEE_UCLIBC_PATH=<path> to cmake where <path> is the path"
-      " to the root of the klee-uclibc directory.")
-  endif()
-
+set(KLEE_UCLIBC_PATH "" CACHE PATH "Path to klee-uclibc root directory")
+set(KLEE_UCLIBC_BCA_NAME "klee-uclibc.bca")
+list(APPEND KLEE_COMPONENT_CXX_DEFINES
+    -DKLEE_UCLIBC_BCA_NAME=\"${KLEE_UCLIBC_BCA_NAME}\")
+if (NOT KLEE_UCLIBC_PATH STREQUAL "")
   # Find the C library bitcode archive
-  set(KLEE_UCLIBC_BCA_NAME "klee-uclibc.bca")
   set(KLEE_UCLIBC_C_BCA "${KLEE_UCLIBC_PATH}/lib/libc.a")
   if (NOT EXISTS "${KLEE_UCLIBC_C_BCA}")
     message(FATAL_ERROR
-      "klee-uclibc library not found at \"${KLEE_UCLIBC_C_BCA}\"")
+      "klee-uclibc library not found at \"${KLEE_UCLIBC_C_BCA}\". Set KLEE_UCLIBC_PATH to klee-uclibc root directory or empty string.")
   endif()
   message(STATUS "Found klee-uclibc library: \"${KLEE_UCLIBC_C_BCA}\"")
-
   # Copy KLEE_UCLIBC_C_BCA so KLEE can find it where it is expected.
   execute_process(COMMAND ${CMAKE_COMMAND} -E copy
     "${KLEE_UCLIBC_C_BCA}"
     "${KLEE_RUNTIME_DIRECTORY}/${KLEE_UCLIBC_BCA_NAME}"
   )
-  list(APPEND KLEE_COMPONENT_CXX_DEFINES
-    -DKLEE_UCLIBC_BCA_NAME=\"${KLEE_UCLIBC_BCA_NAME}\")
-
 else()
-  message(STATUS "klee-uclibc support disabled")
-  set(SUPPORT_KLEE_UCLIBC 0) # For config.h
+  message(STATUS "Skipping copying of klee-uclibc runtime")
 endif()
 
 ################################################################################
diff --git a/README-CMake.md b/README-CMake.md
index 71984e4d..4ea57421 100644
--- a/README-CMake.md
+++ b/README-CMake.md
@@ -49,8 +49,6 @@ cmake -DCMAKE_BUILD_TYPE=Release /path/to/klee/src
 
 * `ENABLE_KLEE_LIBCXX` (BOOLEAN) - Enable libc++ for klee.
 
-* `ENABLE_KLEE_UCLIBC` (BOOLEAN) - Enable support for klee-uclibc.
-
 * `ENABLE_POSIX_RUNTIME` (BOOLEAN) - Enable POSIX runtime.
 
 * `ENABLE_SOLVER_METASMT` (BOOLEAN) - Enable MetaSMT solver support.
diff --git a/include/klee/Config/config.h.cmin b/include/klee/Config/config.h.cmin
index 272b090a..b9fdf7c3 100644
--- a/include/klee/Config/config.h.cmin
+++ b/include/klee/Config/config.h.cmin
@@ -89,9 +89,6 @@
 /* Use Workaround for LLVM PR39177 (affecting LLVM 3.9 - 7.0.0) */
 #cmakedefine USE_WORKAROUND_LLVM_PR39177 @USE_WORKAROUND_LLVM_PR39177@
 
-/* klee-uclibc is supported */
-#cmakedefine SUPPORT_KLEE_UCLIBC @SUPPORT_KLEE_UCLIBC@
-
 /* libcxx is supported */
 #cmakedefine SUPPORT_KLEE_LIBCXX @SUPPORT_KLEE_LIBCXX@
 
diff --git a/scripts/build/p-klee.inc b/scripts/build/p-klee.inc
index 4137cac0..1c7d39a5 100644
--- a/scripts/build/p-klee.inc
+++ b/scripts/build/p-klee.inc
@@ -34,13 +34,11 @@ build_klee() {
 
   if [ "${UCLIBC_VERSION}" != "0" ]; then
     CMAKE_ARGUMENTS+=(
-      "-DENABLE_KLEE_UCLIBC=TRUE"
       "-DKLEE_UCLIBC_PATH=${BASE}/klee-uclibc-${LLVM_VERSION_SHORT}"
       "-DENABLE_POSIX_RUNTIME=TRUE"
     )
   else
     CMAKE_ARGUMENTS+=(
-      "-DENABLE_KLEE_UCLIBC=FALSE"
       "-DENABLE_POSIX_RUNTIME=FALSE"
     )
   fi
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index a62347c1..16d20e1c 100644
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -28,10 +28,16 @@ if (${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   set(NATIVE_CXX "${NATIVE_CXX} -isysroot ${MAC_OS_SDK_PATH}")
 endif()
 
+if (NOT KLEE_UCLIBC_PATH STREQUAL "")
+  set(SUPPORT_KLEE_UCLIBC 1)
+else()
+  set(SUPPORT_KLEE_UCLIBC 0)
+endif()
+
 # FIXME: Do this to avoid changing the template file that
 # is shared by both build systems.
 if (ENABLE_POSIX_RUNTIME)
-  if (ENABLE_KLEE_UCLIBC)
+  if (NOT KLEE_UCLIBC_PATH STREQUAL "")
     set(ENABLE_POSIX_RUNTIME 1)
   else()
     message(AUTHOR_WARNING
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 5984c2f9..c66b707d 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -1026,13 +1026,6 @@ static void halt_via_gdb(int pid) {
     perror("system");
 }
 
-#ifndef SUPPORT_KLEE_UCLIBC
-static void
-linkWithUclibc(StringRef libDir, std::string opt_suffix,
-               std::vector<std::unique_ptr<llvm::Module>> &modules) {
-  klee_error("invalid libc, no uclibc support!\n");
-}
-#else
 static void replaceOrRenameFunction(llvm::Module *module,
 		const char *old_name, const char *new_name)
 {
@@ -1149,7 +1142,6 @@ linkWithUclibc(StringRef libDir, std::string opt_suffix,
     klee_error("error loading the fortify library '%s': %s",
                FortifyPath.c_str(), errorMsg.c_str());
 }
-#endif
 
 int main(int argc, char **argv, char **envp) {
   atexit(llvm_shutdown);  // Call llvm_shutdown() on exit.