From b2a89b4488d6665ba23c7cb3108ad4cb8c35f4dc Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Fri, 21 Sep 2018 16:27:26 -0700 Subject: [PATCH] cmake: Build fully static binaries with option --static. --- CMakeLists.txt | 52 ++++++++++++++--------------------- cmake/FindABC.cmake | 3 ++ cmake/FindANTLR.cmake | 3 ++ cmake/FindCLN.cmake | 3 ++ cmake/FindCaDiCaL.cmake | 3 ++ cmake/FindCryptoMiniSat.cmake | 3 ++ cmake/FindGLPK.cmake | 3 ++ cmake/FindGMP.cmake | 3 ++ cmake/FindLFSC.cmake | 3 ++ cmake/FindReadline.cmake | 40 +++++++++++++++++++++++++-- cmake/Helpers.cmake | 15 ---------- src/CMakeLists.txt | 51 +++++++++++++++++++++++++++++++--- src/main/CMakeLists.txt | 21 ++++++++++++-- 13 files changed, 148 insertions(+), 55 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 011ff2fe5..b733b65d1 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -173,15 +173,31 @@ if(ENABLE_BEST) cvc4_set_option(USE_READLINE ON) endif() -#-----------------------------------------------------------------------------# -# Static libraries +# Only enable unit testing if assertions are enabled. Otherwise, unit tests +# that expect AssertionException to be thrown will fail. +if(NOT ENABLE_ASSERTIONS) + set(ENABLE_UNIT_TESTING OFF) +endif() + +# Never build unit tests as static binaries, otherwise we'll end up with +# ~300MB per unit test. +if(ENABLE_UNIT_TESTING) + set(ENABLE_SHARED ON) +endif() +#-----------------------------------------------------------------------------# +# Shared/static libraries +# # This needs to be set before any find_package(...) command since we want to # search for static libraries with suffix .a. -if(NOT ENABLE_SHARED) - set(CMAKE_FIND_LIBRARY_SUFFIXES ".a") - set(CMAKE_EXE_LINKER_FLAGS "-static") + +if(ENABLE_SHARED) + set(BUILD_SHARED_LIBS ON) +else() + set(CMAKE_FIND_LIBRARY_SUFFIXES ".a ${CMAKE_FIND_LIBRARY_SUFFIXES}") set(BUILD_SHARED_LIBS OFF) + # This is required to force find_package(Boost) to use static libraries. + set(Boost_USE_STATIC_LIBS ON) endif() #-----------------------------------------------------------------------------# @@ -203,8 +219,6 @@ endif() set(GMP_HOME ${GMP_DIR}) find_package(GMP REQUIRED) -libcvc4_link_libraries(${GMP_LIBRARIES}) -libcvc4_include_directories(${GMP_INCLUDE_DIR}) if(ENABLE_ASAN) # -fsanitize=address requires CMAKE_REQUIRED_FLAGS to be explicitely set, @@ -220,9 +234,6 @@ if(ENABLE_ASSERTIONS) add_definitions(-DCVC4_ASSERTIONS) else() add_definitions(-DNDEBUG) - # Only enable unit testing if assertions are enabled. Otherwise, unit tests - # that expect AssertionException to be thrown will fail. - set(ENABLE_UNIT_TESTING OFF) endif() if(ENABLE_COVERAGE) @@ -293,13 +304,6 @@ endif() if(ENABLE_UNIT_TESTING) find_package(CxxTest REQUIRED) - # Force shared libs for unit tests, static libs with unit tests are not - # working right now. - set(ENABLE_SHARED ON) -endif() - -if(ENABLE_SHARED) - set(BUILD_SHARED_LIBS ON) endif() if(ENABLE_STATISTICS) @@ -308,31 +312,24 @@ endif() if(ENABLE_VALGRIND) find_package(Valgrind REQUIRED) - libcvc4_include_directories(${Valgrind_INCLUDE_DIR}) add_definitions(-DCVC4_VALGRIND) endif() if(USE_ABC) set(ABC_HOME "${ABC_DIR}") find_package(ABC REQUIRED) - libcvc4_link_libraries(${ABC_LIBRARIES}) - libcvc4_include_directories(${ABC_INCLUDE_DIR}) add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS}) endif() if(USE_CADICAL) set(CaDiCaL_HOME ${CADICAL_DIR}) find_package(CaDiCaL REQUIRED) - libcvc4_link_libraries(${CaDiCaL_LIBRARIES}) - libcvc4_include_directories(${CaDiCaL_INCLUDE_DIR}) add_definitions(-DCVC4_USE_CADICAL) endif() if(USE_CLN) set(GPL_LIBS "${GPL_LIBS} cln") find_package(CLN 1.2.2 REQUIRED) - libcvc4_link_libraries(${CLN_LIBRARIES}) - libcvc4_include_directories(${CLN_INCLUDE_DIR}) set(CVC4_USE_CLN_IMP 1) set(CVC4_USE_GMP_IMP 0) else() @@ -349,8 +346,6 @@ if(USE_CRYPTOMINISAT) endif() set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR}) find_package(CryptoMiniSat REQUIRED) - libcvc4_link_libraries(${CryptoMiniSat_LIBRARIES}) - libcvc4_include_directories(${CryptoMiniSat_INCLUDE_DIR}) add_definitions(-DCVC4_USE_CRYPTOMINISAT) endif() @@ -358,8 +353,6 @@ if(USE_GLPK) set(GPL_LIBS "${GPL_LIBS} glpk") set(GLPK_HOME ${GLPK_DIR}) find_package(GLPK REQUIRED) - libcvc4_link_libraries(${GLPK_LIBRARIES}) - libcvc4_include_directories(${GLPK_INCLUDE_DIR}) add_definitions(-DCVC4_USE_GLPK) endif() @@ -367,8 +360,6 @@ if(USE_LFSC) set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc) set(LFSC_HOME ${LFSC_DIR}) find_package(LFSC REQUIRED) - libcvc4_link_libraries(${LFSC_LIBRARIES}) - libcvc4_include_directories(${LFSC_INCLUDE_DIR}) add_definitions(-DCVC4_USE_LFSC) endif() @@ -384,7 +375,6 @@ endif() if(USE_SYMFPU) set(SymFPU_HOME ${SYMFPU_DIR}) find_package(SymFPU REQUIRED) - libcvc4_include_directories(${SymFPU_INCLUDE_DIR}) add_definitions(-DCVC4_USE_SYMFPU) set(CVC4_USE_SYMFPU 1) else() diff --git a/cmake/FindABC.cmake b/cmake/FindABC.cmake index 0a9cea950..c44019739 100644 --- a/cmake/FindABC.cmake +++ b/cmake/FindABC.cmake @@ -36,3 +36,6 @@ find_package_handle_standard_args(ABC ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS) mark_as_advanced(ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS) +if(ABC_LIBRARIES) + message(STATUS "Found ABC libs: ${ABC_LIBRARIES}") +endif() diff --git a/cmake/FindANTLR.cmake b/cmake/FindANTLR.cmake index 135668006..5f574247b 100644 --- a/cmake/FindANTLR.cmake +++ b/cmake/FindANTLR.cmake @@ -48,3 +48,6 @@ find_package_handle_standard_args( mark_as_advanced(ANTLR_BINARY ANTLR_INCLUDE_DIR ANTLR_LIBRARIES HAVE_ANTLR3_FILE_STREAM_NEW) +if(ANTLR_LIBRARIES) + message(STATUS "Found ANTLR libs: ${ANTLR_LIBRARIES}") +endif() diff --git a/cmake/FindCLN.cmake b/cmake/FindCLN.cmake index 2cb33eb7e..7b2e6f0f4 100644 --- a/cmake/FindCLN.cmake +++ b/cmake/FindCLN.cmake @@ -25,3 +25,6 @@ if(CLN_INCLUDE_DIR) VERSION_VAR CLN_VERSION) mark_as_advanced(CLN_INCLUDE_DIR CLN_LIBRARIES) endif() +if(CLN_LIBRARIES) + message(STATUS "Found CLN libs: ${CLN_LIBRARIES}") +endif() diff --git a/cmake/FindCaDiCaL.cmake b/cmake/FindCaDiCaL.cmake index 2976bb2bb..bd7de319a 100644 --- a/cmake/FindCaDiCaL.cmake +++ b/cmake/FindCaDiCaL.cmake @@ -32,3 +32,6 @@ find_package_handle_standard_args(CaDiCaL CaDiCaL_INCLUDE_DIR CaDiCaL_LIBRARIES) mark_as_advanced(CaDiCaL_INCLUDE_DIR CaDiCaL_LIBRARIES) +if(CaDiCaL_LIBRARIES) + message(STATUS "Found CaDiCaL libs: ${CaDiCaL_LIBRARIES}") +endif() diff --git a/cmake/FindCryptoMiniSat.cmake b/cmake/FindCryptoMiniSat.cmake index aecd92226..7806b242d 100644 --- a/cmake/FindCryptoMiniSat.cmake +++ b/cmake/FindCryptoMiniSat.cmake @@ -32,3 +32,6 @@ find_package_handle_standard_args(CryptoMiniSat CryptoMiniSat_INCLUDE_DIR CryptoMiniSat_LIBRARIES) mark_as_advanced(CryptoMiniSat_INCLUDE_DIR CryptoMiniSat_LIBRARIES) +if(CryptoMiniSat_LIBRARIES) + message(STATUS "Found CryptoMiniSat libs: ${CryptoMiniSat_LIBRARIES}") +endif() diff --git a/cmake/FindGLPK.cmake b/cmake/FindGLPK.cmake index e2b07faff..1587ca821 100644 --- a/cmake/FindGLPK.cmake +++ b/cmake/FindGLPK.cmake @@ -44,3 +44,6 @@ find_package_handle_standard_args(GLPK GLPK_INCLUDE_DIR GLPK_LIBRARIES) mark_as_advanced(GLPK_INCLUDE_DIR GLPK_LIBRARIES) +if(GLPK_LIBRARIES) + message(STATUS "Found GLPK libs: ${GLPK_LIBRARIES}") +endif() diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake index a835e2d5e..8125a583b 100644 --- a/cmake/FindGMP.cmake +++ b/cmake/FindGMP.cmake @@ -30,3 +30,6 @@ include(FindPackageHandleStandardArgs) find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES) mark_as_advanced(GMP_INCLUDE_DIR GMP_LIBRARIES) +if(GMP_LIBRARIES) + message(STATUS "Found GMP libs: ${GMP_LIBRARIES}") +endif() diff --git a/cmake/FindLFSC.cmake b/cmake/FindLFSC.cmake index 2e3118669..7a666839b 100644 --- a/cmake/FindLFSC.cmake +++ b/cmake/FindLFSC.cmake @@ -32,3 +32,6 @@ find_package_handle_standard_args(LFSC LFSC_INCLUDE_DIR LFSC_LIBRARIES) mark_as_advanced(LFSC_INCLUDE_DIR LFSC_LIBRARIES) +if(LFSC_LIBRARIES) + message(STATUS "Found LFSC libs: ${LFSC_LIBRARIES}") +endif() diff --git a/cmake/FindReadline.cmake b/cmake/FindReadline.cmake index 16dd72236..edac03027 100644 --- a/cmake/FindReadline.cmake +++ b/cmake/FindReadline.cmake @@ -8,12 +8,43 @@ find_path(Readline_INCLUDE_DIR NAMES readline/readline.h) find_library(Readline_LIBRARIES NAMES readline) -# Check which standard of readline is installed on the system. -# https://github.com/CVC4/CVC4/issues/702 +# Try to compile and link a simple program against readline. 'libs' can be +# used to specify additional required libraries. +function(try_compile_readline libs _result) + set(CMAKE_REQUIRED_QUIET TRUE) + set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES} ${libs}) + check_cxx_source_compiles( + " + #include + #include + int main() { readline(\"\"); return 0; } + " + ${_result} + ) + set(${_result} ${${_result}} PARENT_SCOPE) +endfunction() + if(Readline_INCLUDE_DIR) + # We only need to figure out readline's additional libraries dependencies if + # we compile static. + # Note: It might be the case that we need to check for more/other libraries + # depending on what the installed version of readline is linked against + # (e.g., termcap, ncurses, ...). + find_library(TINFO_LIBRARY tinfo) + try_compile_readline(${TINFO_LIBRARY} OK) + if(OK) + list(APPEND Readline_LIBRARIES ${TINFO_LIBRARY}) + else() + message(FATAL_ERROR + "Could not link against readline. " + "Check CMakeError.log for more details") + endif() + + # Check which standard of readline is installed on the system. + # https://github.com/CVC4/CVC4/issues/702 include(CheckCXXSourceCompiles) set(CMAKE_REQUIRED_QUIET TRUE) - set(CMAKE_REQUIRED_LIBRARIES readline) + set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES}) check_cxx_source_compiles( "#include #include @@ -33,3 +64,6 @@ mark_as_advanced( Readline_LIBRARIES Readline_COMPENTRY_FUNC_RETURNS_CHARPTR ) +if(Readline_LIBRARIES) + message(STATUS "Found Readline libs: ${Readline_LIBRARIES}") +endif() diff --git a/cmake/Helpers.cmake b/cmake/Helpers.cmake index ec7216452..692e32900 100644 --- a/cmake/Helpers.cmake +++ b/cmake/Helpers.cmake @@ -120,21 +120,6 @@ macro(print_config str var) endmacro() -#-----------------------------------------------------------------------------# -# libcvc4 helper macros - -# Collect all libraries that must be linked against libcvc4. These will be -# actually linked in src/CMakeLists.txt with target_link_libaries(...). -macro(libcvc4_link_libraries library) - set(LIBCVC4_LIBRARIES ${LIBCVC4_LIBRARIES} ${library}) -endmacro() - -# Collect all include directories that are required for libcvc4. These will be -# actually included in src/CMakeLists.txt with target_include_directories(...). -macro(libcvc4_include_directories dirs) - set(LIBCVC4_INCLUDES ${LIBCVC4_INCLUDES} ${dirs}) -endmacro() - # Collect all source files that are required to build libcvc4 in LIBCVC4_SRCS # or LIBCVC4_GEN_SRCS. If GENERATED is the first argument the sources are # added to LIBCVC4_GEN_SRCS. All sources are prepended with the absolute diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3e32ab7bf..96d462d96 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -660,7 +660,6 @@ include_directories(. ${CMAKE_CURRENT_BINARY_DIR}) add_subdirectory(base) add_subdirectory(expr) -add_subdirectory(main) add_subdirectory(options) add_subdirectory(parser) add_subdirectory(theory) @@ -672,6 +671,7 @@ add_subdirectory(util) set_source_files_properties(${LIBCVC4_GEN_SRCS} PROPERTIES GENERATED TRUE) add_library(cvc4 ${LIBCVC4_SRCS} ${LIBCVC4_GEN_SRCS}) +install(TARGETS cvc4 DESTINATION lib) set_target_properties(cvc4 PROPERTIES SOVERSION ${CVC4_SOVERSION}) target_compile_definitions(cvc4 @@ -682,10 +682,53 @@ target_compile_definitions(cvc4 ) # Add libcvc4 dependencies for generated sources. add_dependencies(cvc4 gen-expr gen-options gen-tags gen-theory) -target_link_libraries(cvc4 ${LIBCVC4_LIBRARIES}) -target_include_directories(cvc4 PUBLIC ${LIBCVC4_INCLUDES}) -install(TARGETS cvc4 DESTINATION lib) +# Add library/include dependencies +if(ENABLE_VALGRIND) + target_include_directories(cvc4 PUBLIC ${Valgrind_INCLUDE_DIR}) +endif() +if(USE_ABC) + target_link_libraries(cvc4 ${ABC_LIBRARIES}) + target_include_directories(cvc4 PUBLIC ${ABC_INCLUDE_DIR}) +endif() +if(USE_CADICAL) + target_link_libraries(cvc4 ${CaDiCaL_LIBRARIES}) + target_include_directories(cvc4 PUBLIC ${CaDiCaL_INCLUDE_DIR}) +endif() +if(USE_CLN) + target_link_libraries(cvc4 ${CLN_LIBRARIES}) + target_include_directories(cvc4 PUBLIC ${CLN_INCLUDE_DIR}) +endif() +if(USE_CRYPTOMINISAT) + target_link_libraries(cvc4 ${CryptoMiniSat_LIBRARIES}) + target_include_directories(cvc4 PUBLIC ${CryptoMiniSat_INCLUDE_DIR}) +endif() +if(USE_GLPK) + target_link_libraries(cvc4 ${GLPK_LIBRARIES}) + target_include_directories(cvc4 PUBLIC ${GLPK_INCLUDE_DIR}) +endif() +if(USE_LFSC) + target_link_libraries(cvc4 ${LFSC_LIBRARIES}) + target_include_directories(cvc4 PUBLIC ${LFSC_INCLUDE_DIR}) +endif() +if(USE_SYMFPU) + target_include_directories(cvc4 PUBLIC ${SymFPU_INCLUDE_DIR}) +endif() + +# Note: When linked statically GMP needs to be linked after CLN since CLN +# depends on GMP. +target_link_libraries(cvc4 ${GMP_LIBRARIES}) +target_include_directories(cvc4 PUBLIC ${GMP_INCLUDE_DIR}) + +#-----------------------------------------------------------------------------# +# Visit main subdirectory after creating target cvc4. For target main, we have +# to manually add library dependencies since we can't use +# target_link_libraries(...) with object libraries for cmake versions <= 3.12. +# Thus, we can only visit main as soon as all dependencies for cvc4 are set up. + +add_subdirectory(main) + +#-----------------------------------------------------------------------------# # Note: # We define all install commands for all public headers here in one # place so that we can easily remove them as soon as we enforce the new diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index 39c4b2779..30a246ba0 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -16,8 +16,8 @@ set(libmain_src_files add_library(main OBJECT ${libmain_src_files}) target_compile_definitions(main PRIVATE -D__BUILDING_CVC4DRIVER) -if(BUILD_SHARED_LIBS) - set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE 1) +if(ENABLE_SHARED) + set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE ON) endif() # We can't use target_link_libraries(...) here since this is only supported for @@ -26,6 +26,7 @@ endif() # dependencies are not propagated and we need to manually add the include # directories of libcvc4 to main. add_dependencies(main cvc4 cvc4parser gen-tokens) +get_target_property(LIBCVC4_INCLUDES cvc4 INCLUDE_DIRECTORIES) target_include_directories(main PRIVATE ${LIBCVC4_INCLUDES}) # main-test library is only used for linking against system and unit tests so @@ -46,6 +47,16 @@ set_target_properties(cvc4-bin target_link_libraries(cvc4-bin cvc4 cvc4parser) install(TARGETS cvc4-bin DESTINATION bin) +# In order to get a fully static executable we have to make sure that we also +# use the static system libraries. +# https://cmake.org/cmake/help/v3.0/prop_tgt/LINK_SEARCH_START_STATIC.html +# https://cmake.org/cmake/help/v3.0/prop_tgt/LINK_SEARCH_END_STATIC.html +if(NOT ENABLE_SHARED) + set_target_properties(cvc4-bin PROPERTIES LINK_FLAGS -static) + set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_START_STATIC ON) + set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_END_STATIC ON) +endif() + if(ENABLE_PORTFOLIO) set(pcvc4_src_files main.cpp @@ -66,6 +77,12 @@ if(ENABLE_PORTFOLIO) target_link_libraries(pcvc4-bin cvc4 cvc4parser ${Boost_LIBRARIES}) target_include_directories(pcvc4-bin PRIVATE ${Boost_INCLUDE_DIRS}) install(TARGETS pcvc4-bin DESTINATION bin) + + if(NOT ENABLE_SHARED) + set_target_properties(pcvc4-bin PROPERTIES LINK_FLAGS -static) + set_target_properties(pcvc4-bin PROPERTIES LINK_SEARCH_START_STATIC ON) + set_target_properties(pcvc4-bin PROPERTIES LINK_SEARCH_END_STATIC ON) + endif() endif() if(USE_READLINE) -- 2.30.2