cmake: Build fully static binaries with option --static.

2 files changed, 66 insertions, 6 deletions

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)