diff --git a/CMakeLists.txt b/CMakeLists.txt index bc86e39eea8..6ca89083be6 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -59,7 +59,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR "${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU" ) # Ensure NDEBUG is not set for release builds - set(CMAKE_CXX_FLAGS_RELEASE "-O2") + set(CMAKE_CXX_FLAGS_RELEASE "-O3") set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g") # Enable lots of warnings set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wno-deprecated-declarations -Wswitch-enum") @@ -180,6 +180,10 @@ function(cprover_default_properties) CXX_STANDARD ${CBMC_CXX_STANDARD} CXX_STANDARD_REQUIRED ${CBMC_CXX_STANDARD_REQUIRED} XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY ${CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY}) + + if(ipo_supported) + set_property(TARGET ${ARGN} PROPERTY INTERPROCEDURAL_OPTIMIZATION True) + endif() endfunction() if(CMAKE_SYSTEM_NAME STREQUAL Linux) @@ -191,6 +195,36 @@ endif() option(WITH_MEMORY_ANALYZER "build the memory analyzer" ${WITH_MEMORY_ANALYZER_DEFAULT}) +if((CMAKE_MAJOR_VERSION EQUAL 3 AND CMAKE_MINOR_VERSION GREATER_EQUAL 9) + AND (CMAKE_BUILD_TYPE STREQUAL "Release")) + cmake_policy(SET CMP0069 NEW) + include(CheckIPOSupported) + check_ipo_supported(RESULT ipo_supported OUTPUT error LANGUAGES CXX) +endif() + +if(ipo_supported) + message(STATUS "IPO / LTO enabled") + set_property(GLOBAL PROPERTY INTERPROCEDURAL_OPTIMIZATION True) + add_definitions(-DLTO) + if ((CMAKE_SYSTEM_PROCESSOR STREQUAL "x86_64") + OR (CMAKE_SYSTEM_PROCESSOR STREQUAL "i386") + OR (CMAKE_SYSTEM_PROCESSOR STREQUAL "i586") + OR (CMAKE_SYSTEM_PROCESSOR STREQUAL "i686") + OR (CMAKE_SYSTEM_PROCESSOR STREQUAL "amd64") # freebsd + OR (CMAKE_SYSTEM_PROCESSOR STREQUAL "AMD64") # windows + OR (CMAKE_SYSTEM_PROCESSOR STREQUAL "x86")) + set(PROCESSOR_FAMILY "Intel") + if(CMAKE_COMPILER_IS_GNUCC + OR (CMAKE_CXX_COMPILER_ID STREQUAL AppleClang) + OR (CMAKE_CXX_COMPILER_ID STREQUAL Clang) + OR (CMAKE_CXX_COMPILER_ID STREQUAL Intel)) + add_definitions(-march=native) + endif() + endif() +else() + message(STATUS "IPO / LTO not supported: <${error}>") +endif() + add_subdirectory(src) add_subdirectory(regression) add_subdirectory(unit) diff --git a/regression/invariants/CMakeLists.txt b/regression/invariants/CMakeLists.txt index 6e788e13330..eab6d1f8a61 100644 --- a/regression/invariants/CMakeLists.txt +++ b/regression/invariants/CMakeLists.txt @@ -1,5 +1,8 @@ add_executable(driver driver.cpp) target_link_libraries(driver big-int util) +if(ipo_supported) + set_property(TARGET driver PROPERTY INTERPROCEDURAL_OPTIMIZATION True) +endif() add_test_pl_tests( "$" diff --git a/scripts/glucose_CMakeLists.txt b/scripts/glucose_CMakeLists.txt index b2116ce91f4..798cb5432d1 100644 --- a/scripts/glucose_CMakeLists.txt +++ b/scripts/glucose_CMakeLists.txt @@ -14,6 +14,10 @@ set_target_properties( XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening" ) +if(ipo_supported) + set_property(TARGET minisat2-condensed PROPERTY INTERPROCEDURAL_OPTIMIZATION True) +endif() + if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") target_compile_options(glucose-condensed PUBLIC /w) endif() diff --git a/scripts/minisat2_CMakeLists.txt b/scripts/minisat2_CMakeLists.txt index 963bc0a6d1d..4a9277ee2cb 100644 --- a/scripts/minisat2_CMakeLists.txt +++ b/scripts/minisat2_CMakeLists.txt @@ -14,6 +14,10 @@ set_target_properties( XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening" ) +if(ipo_supported) + set_property(TARGET minisat2-condensed PROPERTY INTERPROCEDURAL_OPTIMIZATION True) +endif() + if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") target_compile_options(minisat2-condensed PUBLIC /w) endif() diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1aebe8412a0..c9f66c536de 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -93,6 +93,12 @@ macro(add_if_library target name) string(REGEX REPLACE "-" "_" define ${upper_name}) target_compile_definitions(${target} PUBLIC HAVE_${define}) + if(ipo_supported) + set_property(TARGET ${name} PROPERTY INTERPROCEDURAL_OPTIMIZATION True) + endif() + endif() + if(ipo_supported) + set_property(TARGET ${target} PROPERTY INTERPROCEDURAL_OPTIMIZATION True) endif() endmacro(add_if_library) diff --git a/src/ansi-c/CMakeLists.txt b/src/ansi-c/CMakeLists.txt index 5981efeb723..8fb6ba51af8 100644 --- a/src/ansi-c/CMakeLists.txt +++ b/src/ansi-c/CMakeLists.txt @@ -10,6 +10,10 @@ add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc" DEPENDS converter ${ansi_c_library_sources}) add_executable(file_converter file_converter.cpp) +if(ipo_supported) + set_property(TARGET converter PROPERTY INTERPROCEDURAL_OPTIMIZATION True) + set_property(TARGET file_converter PROPERTY INTERPROCEDURAL_OPTIMIZATION True) +endif() function(make_inc name) add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/${name}.inc" diff --git a/src/config.inc b/src/config.inc index 0625bd3cb6d..abb0e608f7c 100644 --- a/src/config.inc +++ b/src/config.inc @@ -14,9 +14,12 @@ ifeq ($(CPROVER_WITH_PROFILING),1) endif # Select optimisation or debug info -#CXXFLAGS += -O2 -DNDEBUG +#CXXFLAGS += -O3 -DNDEBUG -flto -DLTO #CXXFLAGS += -O0 -g +# Matching -flto above +#LINKFLAGS = -ftlo + # With GCC this adds function names in stack backtraces #LINKFLAGS = -rdynamic diff --git a/src/goto-symex/CMakeLists.txt b/src/goto-symex/CMakeLists.txt index 303a48feb99..3af49219ace 100644 --- a/src/goto-symex/CMakeLists.txt +++ b/src/goto-symex/CMakeLists.txt @@ -8,3 +8,8 @@ if(CMAKE_USE_CUDD) endif() target_link_libraries(goto-symex util) + +if(ipo_supported) + set_property(TARGET goto-symex PROPERTY INTERPROCEDURAL_OPTIMIZATION True) +endif() + diff --git a/src/memory-analyzer/CMakeLists.txt b/src/memory-analyzer/CMakeLists.txt index 39474f444d9..6a153cd0777 100644 --- a/src/memory-analyzer/CMakeLists.txt +++ b/src/memory-analyzer/CMakeLists.txt @@ -16,6 +16,7 @@ target_link_libraries(memory-analyzer-lib # Executable add_executable(memory-analyzer memory_analyzer_main.cpp) + target_link_libraries(memory-analyzer memory-analyzer-lib) cprover_default_properties(memory-analyzer memory-analyzer-lib) diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index d55ec09ffa7..819b1f6659e 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -54,6 +54,9 @@ list(REMOVE_ITEM sources ) add_library(solvers ${sources}) +if(ipo_supported) + set_property(TARGET solvers PROPERTY INTERPROCEDURAL_OPTIMIZATION True) +endif() include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake") @@ -104,12 +107,20 @@ elseif("${sat_impl}" STREQUAL "cadical") download_project(PROJ cadical URL https://github.com/arminbiere/cadical/archive/rel-1.3.0.tar.gz PATCH_COMMAND true - COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s -j + COMMAND CXX="${CMAKE_CXX_COMPILER}" CXXFLAGS="${CMAKE_CXX_FLAGS}" ./configure -O3 -s -j URL_MD5 5bd15d1e198d2e904a8af8b7873dd341 ) message(STATUS "Building CaDiCaL") - execute_process(COMMAND make WORKING_DIRECTORY ${cadical_SOURCE_DIR}) + if("${CMAKE_BUILD_TYPE}" STREQUAL "Release") + execute_process(COMMAND make CXXFLAGS="${CMAKE_CXX_FLAGS_RELEASE}" + WORKING_DIRECTORY "${cadical_SOURCE_DIR}") + elseif("${CMAKE_BUILD_TYPE}" STREQUAL "RelWithDebInfo") + execute_process(COMMAND make CXXFLAGS="${CMAKE_CXX_FLAGS_RELWITHDEBINFO}" + WORKING_DIRECTORY "${cadical_SOURCE_DIR}") + else() + execute_process(COMMAND make WORKING_DIRECTORY ${cadical_SOURCE_DIR}) + endif() target_compile_definitions(solvers PUBLIC SATCHECK_CADICAL HAVE_CADICAL @@ -117,6 +128,9 @@ elseif("${sat_impl}" STREQUAL "cadical") add_library(cadical STATIC IMPORTED) + if(ipo_supported) + set_property(TARGET cadical PROPERTY INTERPROCEDURAL_OPTIMIZATION True) + endif() set_target_properties( cadical PROPERTIES IMPORTED_LOCATION ${cadical_SOURCE_DIR}/build/libcadical.a @@ -143,5 +157,8 @@ endif() # Executable add_executable(smt2_solver smt2/smt2_solver.cpp) target_link_libraries(smt2_solver solvers) +if(ipo_supported) + set_property(TARGET smt2_solver PROPERTY INTERPROCEDURAL_OPTIMIZATION True) +endif() generic_includes(solvers) diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 6d693238a2a..cd564c6372e 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -14,7 +14,11 @@ if(GIT_FOUND) OUTPUT_STRIP_TRAILING_WHITESPACE WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} ) - configure_file(\${CUR}/version.cpp.in version.cpp) + configure_file(${CMAKE_CURRENT_BINARY_DIR}/version.cpp.in ${CMAKE_CURRENT_BINARY_DIR}/version.cpp.tmp) + execute_process( + COMMAND ${CMAKE_COMMAND} -E copy_if_different ${CMAKE_CURRENT_BINARY_DIR}/version.cpp.tmp version.cpp + WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} + ) " ) else() @@ -24,7 +28,11 @@ else() config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\") string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v}) set(GIT_INFO \"n/a\") - configure_file(\${CUR}/version.cpp.in version.cpp) + configure_file(${CMAKE_CURRENT_BINARY_DIR}/version.cpp.in ${CMAKE_CURRENT_BINARY_DIR}/version.cpp.tmp) + execute_process( + COMMAND ${CMAKE_COMMAND} -E copy_if_different ${CMAKE_CURRENT_BINARY_DIR}/version.cpp.tmp version.cpp + WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} + ) " ) endif() @@ -33,10 +41,9 @@ file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/version.cpp.in "const char *CBMC_VERSION=\"@CBMC_RELEASE@ (@GIT_INFO@)\";\n") add_custom_target( generate_version_cpp - BYPRODUCTS version.cpp + BYPRODUCTS ${CBMC_SOURCE_DIR}/util/version.cpp COMMAND ${CMAKE_COMMAND} -D CBMC_SOURCE_DIR=${CBMC_SOURCE_DIR} - -D CUR=${CMAKE_CURRENT_BINARY_DIR} -P ${CMAKE_BINARY_DIR}/version.cmake )