diff options
-rw-r--r-- | CMakeLists.txt | 32 | ||||
-rw-r--r-- | README-CMake.md | 2 | ||||
-rw-r--r-- | include/klee/Config/config.h.cmin | 3 | ||||
-rw-r--r-- | scripts/build/p-klee.inc | 2 | ||||
-rw-r--r-- | test/CMakeLists.txt | 8 | ||||
-rw-r--r-- | tools/klee/main.cpp | 8 |
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. |