From 330b9cfe5a1bb145f83264eaba496b30bc6eee4d Mon Sep 17 00:00:00 2001 From: Reini Urban Date: Sun, 4 Apr 2021 21:23:31 +0200 Subject: [PATCH 1/4] WIP Enable IPO / LTO and -O3 LTO and -O3 give a good performance improvement. I would not recommend -O3 with bad compiler versions though, such as gcc-9. WIP: GLOBAL properties are not enough, add the IPO property to all targets. Which leads to various problems still. --- CMakeLists.txt | 21 ++++++++++++++++++++- regression/invariants/CMakeLists.txt | 3 +++ scripts/glucose_CMakeLists.txt | 4 ++++ scripts/minisat2_CMakeLists.txt | 4 ++++ src/CMakeLists.txt | 6 ++++++ src/ansi-c/CMakeLists.txt | 4 ++++ src/config.inc | 5 ++++- src/goto-symex/CMakeLists.txt | 5 +++++ src/memory-analyzer/CMakeLists.txt | 1 + src/solvers/CMakeLists.txt | 11 ++++++++++- 10 files changed, 61 insertions(+), 3 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index bc86e39eea8..39f4de05d56 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,21 @@ 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) +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..2a960ba23ae 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,7 +107,7 @@ 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 ) @@ -117,6 +120,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 +149,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) From cfb585bf164c9cbbef6ba30316a5633924d5a8fb Mon Sep 17 00:00:00 2001 From: Reini Urban Date: Tue, 6 Apr 2021 16:52:14 +0200 Subject: [PATCH 2/4] Add -march=native for gcc-compat on Intel not valid on arm or other archs. Only for gcc-compatible compilers. 30% faster on small samples than -flto --- CMakeLists.txt | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 39f4de05d56..6ca89083be6 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -206,6 +206,21 @@ 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() From 9737d59f523491b45d74713360dab6e4a60afc7b Mon Sep 17 00:00:00 2001 From: Reini Urban Date: Wed, 7 Apr 2021 15:42:47 +0200 Subject: [PATCH 3/4] Pass CXXFLAGS to CaDiCaL also --- src/solvers/CMakeLists.txt | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index 2a960ba23ae..819b1f6659e 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -112,7 +112,15 @@ elseif("${sat_impl}" STREQUAL "cadical") ) 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 From e0a69da3ec54bb43de578b596a583c95a5f23ded Mon Sep 17 00:00:00 2001 From: Reini Urban Date: Tue, 6 Apr 2021 09:46:14 +0200 Subject: [PATCH 4/4] Fix generate_version_cpp target Create version.cpp in the src dir, where it is picked up. And not in the build dir. Update only if different to avoid needless recompilations. Repro: check bin/cbmc --version for the correct version. --- src/util/CMakeLists.txt | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) 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 )