From 106db2f916f4f6863511de1437a653346f778930 Mon Sep 17 00:00:00 2001 From: Vladislav Kalugin Date: Mon, 9 Oct 2023 14:59:10 +0300 Subject: [PATCH] Compile as lib for UTBot --- CMakeLists.txt | 20 ++++++++++- include/klee/Runner/run_klee.h | 6 ++++ lib/Basic/CMakeLists.txt | 5 +++ lib/CMakeLists.txt | 1 + lib/Core/CMakeLists.txt | 6 ++++ lib/Expr/CMakeLists.txt | 5 +++ lib/Module/CMakeLists.txt | 5 +++ lib/Runner/CMakeLists.txt | 27 ++++++++++++++ .../klee/main.cpp => lib/Runner/run_klee.cpp | 2 +- lib/Support/CMakeLists.txt | 5 +++ tools/klee/CMakeLists.txt | 12 ++----- tools/klee/klee.cpp | 5 +++ utbot-build.sh | 35 ------------------- 13 files changed, 87 insertions(+), 47 deletions(-) create mode 100644 include/klee/Runner/run_klee.h create mode 100644 lib/Runner/CMakeLists.txt rename tools/klee/main.cpp => lib/Runner/run_klee.cpp (99%) create mode 100644 tools/klee/klee.cpp delete mode 100755 utbot-build.sh diff --git a/CMakeLists.txt b/CMakeLists.txt index 18d853e189..83152bc938 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -679,6 +679,11 @@ set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) set(KLEE_UTILS_DIR ${CMAKE_SOURCE_DIR}/utils) +################################################################################ +# Set install destination paths for targets +################################################################################ +set(RUN_KLEE_MAIN_LIB_DEST "lib/run_klee") +set(RUN_KLEE_LIB_DEST "${RUN_KLEE_MAIN_LIB_DEST}/${CMAKE_BUILD_TYPE}") ################################################################################ # Report the value of various variables to aid debugging @@ -773,7 +778,20 @@ endif() ################################################################################ # Miscellaneous install ################################################################################ -install(FILES include/klee/klee.h DESTINATION include/klee) +install(FILES include/klee/klee.h include/klee/ADT/KTest.h DESTINATION include/klee) +INSTALL(FILES lib/Core/Executor.h DESTINATION include/klee/Core) +INSTALL(DIRECTORY include/klee/Expr DESTINATION include/klee) +INSTALL(DIRECTORY include/klee/Module DESTINATION include/klee) +INSTALL(DIRECTORY include/klee/Statistics DESTINATION include/klee) +INSTALL(DIRECTORY include/klee/Support DESTINATION include/klee) + +install(EXPORT run_klee + DESTINATION "${RUN_KLEE_LIB_DEST}" + ) + +install(FILES cmake/run_klee-config.cmake + DESTINATION "${RUN_KLEE_MAIN_LIB_DEST}" + ) ################################################################################ # Uninstall rule diff --git a/include/klee/Runner/run_klee.h b/include/klee/Runner/run_klee.h new file mode 100644 index 0000000000..14a4ce9925 --- /dev/null +++ b/include/klee/Runner/run_klee.h @@ -0,0 +1,6 @@ +#ifndef KLEE_RUN_KLEE_H +#define KLEE_RUN_KLEE_H + +int run_klee(int argc, char **argv, char **envp); + +#endif // KLEE_RUN_KLEE_H diff --git a/lib/Basic/CMakeLists.txt b/lib/Basic/CMakeLists.txt index db630893df..eb76ae427d 100644 --- a/lib/Basic/CMakeLists.txt +++ b/lib/Basic/CMakeLists.txt @@ -16,3 +16,8 @@ target_compile_options(kleeBasic PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) target_compile_definitions(kleeBasic PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) target_include_directories(kleeBasic PRIVATE ${KLEE_INCLUDE_DIRS}) + +install(TARGETS kleeBasic + EXPORT run_klee + DESTINATION "${RUN_KLEE_LIB_DEST}" +) diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt index 8a0749324a..93a4c20e92 100644 --- a/lib/CMakeLists.txt +++ b/lib/CMakeLists.txt @@ -12,3 +12,4 @@ add_subdirectory(Expr) add_subdirectory(Solver) add_subdirectory(Module) add_subdirectory(Core) +add_subdirectory(Runner) diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt index 9d94da9169..af666ee4c9 100644 --- a/lib/Core/CMakeLists.txt +++ b/lib/Core/CMakeLists.txt @@ -49,3 +49,9 @@ target_link_libraries(kleeCore PRIVATE ${SQLite3_LIBRARIES}) target_include_directories(kleeCore PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS} ${SQLite3_INCLUDE_DIRS}) target_compile_options(kleeCore PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) target_compile_definitions(kleeCore PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + +install(TARGETS kleeCore + EXPORT run_klee + DESTINATION "${RUN_KLEE_LIB_DEST}" +) + diff --git a/lib/Expr/CMakeLists.txt b/lib/Expr/CMakeLists.txt index 758a4ca743..fe87b1c356 100644 --- a/lib/Expr/CMakeLists.txt +++ b/lib/Expr/CMakeLists.txt @@ -36,3 +36,8 @@ llvm_config(kleaverExpr "${USE_LLVM_SHARED}" support) target_include_directories(kleaverExpr PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS}) target_compile_options(kleaverExpr PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) target_compile_definitions(kleaverExpr PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + +install(TARGETS kleaverExpr + EXPORT run_klee + DESTINATION "${RUN_KLEE_LIB_DEST}" +) diff --git a/lib/Module/CMakeLists.txt b/lib/Module/CMakeLists.txt index 42ef35556b..936c9cb5c7 100644 --- a/lib/Module/CMakeLists.txt +++ b/lib/Module/CMakeLists.txt @@ -57,3 +57,8 @@ target_link_libraries(kleeModule PRIVATE target_include_directories(kleeModule PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS}) target_compile_options(kleeModule PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) target_compile_definitions(kleeModule PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + +install(TARGETS kleeModule + EXPORT run_klee + DESTINATION "${RUN_KLEE_LIB_DEST}" +) diff --git a/lib/Runner/CMakeLists.txt b/lib/Runner/CMakeLists.txt new file mode 100644 index 0000000000..a83c1ce46c --- /dev/null +++ b/lib/Runner/CMakeLists.txt @@ -0,0 +1,27 @@ +add_library(kleeRunner + run_klee.cpp + ) + +set(KLEE_LIBS + kleeCore + ) + +set(RUN_KLEE_INCLUDE_DEST "include/run_klee") + +target_link_libraries(kleeRunner ${KLEE_LIBS}) +target_include_directories(kleeRunner PUBLIC ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS}) +target_compile_options(kleeRunner PUBLIC ${KLEE_COMPONENT_CXX_FLAGS}) +target_compile_definitions(kleeRunner PUBLIC ${KLEE_COMPONENT_CXX_DEFINES}) +set(run_klee_header_path ${PROJECT_SOURCE_DIR}/include/klee/Runner) +set(run_klee_headers ${run_klee_header_path}/run_klee.h) + +set_target_properties(kleeRunner PROPERTIES PUBLIC_HEADER "${run_klee_headers}") + +install(TARGETS kleeRunner + EXPORT run_klee DESTINATION "${RUN_KLEE_LIB_DEST}" + PUBLIC_HEADER DESTINATION "${RUN_KLEE_INCLUDE_DEST}" + ) + + +# The KLEE depends on the runtimes +add_dependencies(kleeRunner BuildKLEERuntimes) diff --git a/tools/klee/main.cpp b/lib/Runner/run_klee.cpp similarity index 99% rename from tools/klee/main.cpp rename to lib/Runner/run_klee.cpp index e9bb118371..60bcce8c84 100644 --- a/tools/klee/main.cpp +++ b/lib/Runner/run_klee.cpp @@ -1584,7 +1584,7 @@ void wait_until_any_child_dies( } } -int main(int argc, char **argv, char **envp) { +int run_klee(int argc, char **argv, char **envp) { if (theInterpreter) { theInterpreter = nullptr; } diff --git a/lib/Support/CMakeLists.txt b/lib/Support/CMakeLists.txt index 6e32058a96..ee579df373 100644 --- a/lib/Support/CMakeLists.txt +++ b/lib/Support/CMakeLists.txt @@ -25,3 +25,8 @@ target_link_libraries(kleeSupport PRIVATE ${ZLIB_LIBRARIES} ${TCMALLOC_LIBRARIES target_include_directories(kleeSupport PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS} ${TCMALLOC_INCLUDE_DIR}) target_compile_options(kleeSupport PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) target_compile_definitions(kleeSupport PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) + +install(TARGETS kleeSupport + EXPORT run_klee + DESTINATION "${RUN_KLEE_LIB_DEST}" +) diff --git a/tools/klee/CMakeLists.txt b/tools/klee/CMakeLists.txt index cabdfdfcbd..be43d0969e 100644 --- a/tools/klee/CMakeLists.txt +++ b/tools/klee/CMakeLists.txt @@ -7,18 +7,10 @@ # #===------------------------------------------------------------------------===# add_executable(klee - main.cpp + klee.cpp ) -set(KLEE_LIBS - kleeCore -) - -target_link_libraries(klee ${KLEE_LIBS}) -target_include_directories(klee PRIVATE ${KLEE_INCLUDE_DIRS} ${LLVM_INCLUDE_DIRS}) -target_compile_options(klee PRIVATE ${KLEE_COMPONENT_CXX_FLAGS}) -target_compile_definitions(klee PRIVATE ${KLEE_COMPONENT_CXX_DEFINES}) - +target_link_libraries(klee PUBLIC kleeRunner) install(TARGETS klee RUNTIME DESTINATION bin) diff --git a/tools/klee/klee.cpp b/tools/klee/klee.cpp new file mode 100644 index 0000000000..a6640bf9c1 --- /dev/null +++ b/tools/klee/klee.cpp @@ -0,0 +1,5 @@ +#include + +int main(int argc, char **argv, char **envp) { + return run_klee(argc, argv, envp); +} diff --git a/utbot-build.sh b/utbot-build.sh deleted file mode 100755 index 12f4182699..0000000000 --- a/utbot-build.sh +++ /dev/null @@ -1,35 +0,0 @@ -#!/bin/bash -# This script is used to build KLEE as UTBot backend - -set -e -set -o pipefail -mkdir -p build -cd build - -$UTBOT_CMAKE_BINARY -G Ninja \ - -DCMAKE_PREFIX_PATH=$UTBOT_INSTALL_DIR/lib/cmake/z3 \ - -DCMAKE_LIBRARY_PATH=$UTBOT_INSTALL_DIR/lib \ - -DCMAKE_INCLUDE_PATH=$UTBOT_INSTALL_DIR/include \ - -DENABLE_SOLVER_Z3=TRUE \ - -DENABLE_POSIX_RUNTIME=TRUE \ - -DENABLE_KLEE_UCLIBC=ON \ - -DKLEE_UCLIBC_PATH=$UTBOT_ALL/klee-uclibc \ - -DENABLE_FLOATING_POINT=TRUE \ - -DENABLE_FP_RUNTIME=TRUE \ - -DLLVM_CONFIG_BINARY=$UTBOT_INSTALL_DIR/bin/llvm-config \ - -DLLVMCC=/utbot_distr/install/bin/clang \ - -DLLVMCXX=/utbot_distr/install/bin/clang++ \ - -DENABLE_UNIT_TESTS=TRUE \ - -DENABLE_SYSTEM_TESTS=TRUE \ - -DGTEST_SRC_DIR=$UTBOT_ALL/gtest \ - -DGTEST_INCLUDE_DIR=$UTBOT_ALL/gtest/googletest/include \ - -DCMAKE_INSTALL_PREFIX=$UTBOT_ALL/klee \ - -DENABLE_KLEE_LIBCXX=TRUE \ - -DKLEE_LIBCXX_DIR=$UTBOT_ALL/libcxx/install \ - -DKLEE_LIBCXX_INCLUDE_DIR=$UTBOT_ALL/libcxx/install/include/c++/v1 \ - -DENABLE_KLEE_EH_CXX=TRUE \ - -DKLEE_LIBCXXABI_SRC_DIR=$UTBOT_ALL/libcxx/libcxxabi \ - .. - -$UTBOT_CMAKE_BINARY --build . -$UTBOT_CMAKE_BINARY --install .