diff --git a/CMakeLists.txt b/CMakeLists.txt index 1816ceaad..0a215b5a9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -234,6 +234,13 @@ endif () if (STORM_USE_LTO) set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto") + + # Fix for problems that occured when using LTO on gcc. This should be removed when it's + # not needed anymore as it makes the the already long link-step potentially longer. + if (STORM_COMPILER_GCC) + set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto-partition=none") + endif() + message(STATUS "Storm - Enabling link-time optimizations.") else() message(STATUS "Storm - Disabling link-time optimizations.") diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 4e56c4c04..3380b731e 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -364,12 +364,13 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_xerces.cmake) ## ############################################################# +if(STORM_USE_LTO) ExternalProject_Add( sylvan DOWNLOAD_COMMAND "" PREFIX "sylvan" SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan - CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DSYLVAN_BUILD_DOCS=OFF -DSYLVAN_BUILD_EXAMPLES=OFF -DCMAKE_BUILD_TYPE=Release -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DUSE_CARL=ON -Dcarl_INCLUDE_DIR=${carl_INCLUDE_DIR} -DSYLVAN_PORTABLE=${STORM_PORTABLE} -Dcarl_LIBRARIES=${carl_LIBRARIES} -DBUILD_SHARED_LIBS=OFF -DSYLVAN_BUILD_TESTS=OFF + CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DSYLVAN_BUILD_DOCS=OFF -DSYLVAN_BUILD_EXAMPLES=OFF -DCMAKE_BUILD_TYPE=Release -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DUSE_CARL=ON -Dcarl_INCLUDE_DIR=${carl_INCLUDE_DIR} -DSYLVAN_PORTABLE=${STORM_PORTABLE} -Dcarl_LIBRARIES=${carl_LIBRARIES} -DBUILD_SHARED_LIBS=OFF -DSYLVAN_BUILD_TESTS=OFF -DSYLVAN_USE_LTO=ON BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan BUILD_IN_SOURCE 0 INSTALL_COMMAND "" @@ -377,7 +378,26 @@ ExternalProject_Add( LOG_CONFIGURE ON LOG_BUILD ON BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/sylvan/src/libsylvan${STATIC_EXT} + BUILD_ALWAYS 1 ) +else() +ExternalProject_Add( + sylvan + DOWNLOAD_COMMAND "" + PREFIX "sylvan" + SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan + CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DSYLVAN_BUILD_DOCS=OFF -DSYLVAN_BUILD_EXAMPLES=OFF -DCMAKE_BUILD_TYPE=Release -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DUSE_CARL=ON -Dcarl_INCLUDE_DIR=${carl_INCLUDE_DIR} -DSYLVAN_PORTABLE=${STORM_PORTABLE} -Dcarl_LIBRARIES=${carl_LIBRARIES} -DBUILD_SHARED_LIBS=OFF -DSYLVAN_BUILD_TESTS=OFF -DSYLVAN_USE_LTO=OFF + BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan + BUILD_IN_SOURCE 0 + INSTALL_COMMAND "" + INSTALL_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan + LOG_CONFIGURE ON + LOG_BUILD ON + BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/sylvan/src/libsylvan${STATIC_EXT} + BUILD_ALWAYS 1 +) +endif() + ExternalProject_Get_Property(sylvan source_dir) ExternalProject_Get_Property(sylvan binary_dir) set(Sylvan_INCLUDE_DIR "${source_dir}/src") diff --git a/resources/3rdparty/sylvan/CMakeLists.txt b/resources/3rdparty/sylvan/CMakeLists.txt index c7a8d5a81..dae81eefe 100755 --- a/resources/3rdparty/sylvan/CMakeLists.txt +++ b/resources/3rdparty/sylvan/CMakeLists.txt @@ -1,12 +1,11 @@ cmake_minimum_required(VERSION 3.1) -project(sylvan VERSION 1.2.0) +project(sylvan LANGUAGES C CXX VERSION 1.2.0) set(PROJECT_DESCRIPTION "Sylvan, a parallel decision diagram library") set(PROJECT_URL "https://github.com/trolando/sylvan") message(STATUS "CMake build configuration for Sylvan ${PROJECT_VERSION}") -enable_language(C CXX) set(CMAKE_C_STANDARD 11) set(CMAKE_C_STANDARD_REQUIRED ON) @@ -34,6 +33,20 @@ if (NOT SYLVAN_PORTABLE) set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -march=native") endif() +if (SYLVAN_USE_LTO) + message(STATUS "Sylvan - Enabling LTO.") + set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -flto -flto-partition=none") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -flto -flto-partition=none") + + # For GCC, we need to set the ar/ranlib commands to use the gcc wrappers to account for LTO. + if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU") + message(STATUS "Sylvan - Setting ar/ranlib to account for LTO.") + set(CMAKE_AR gcc-ar CACHE FILEPATH "Archiver" FORCE) + set(CMAKE_RANLIB gcc-ranlib CACHE FILEPATH "Ranlib" FORCE) + message(STATUS "Sylvan - ar/ranlib are ${CMAKE_AR} and ${CMAKE_RANLIB}, respectively.") + endif() +endif() + option(WITH_COVERAGE "Add generation of test coverage" OFF) if(WITH_COVERAGE) set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -O0 -g -coverage")