Skip to content

Enable IPO / LTO and -O3 #6011

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 4 commits into from
Closed

Enable IPO / LTO and -O3 #6011

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
330b9cf
WIP Enable IPO / LTO and -O3
rurban Apr 4, 2021
cfb585b
Add -march=native for gcc-compat on Intel
rurban Apr 6, 2021
9737d59
Pass CXXFLAGS to CaDiCaL also
rurban Apr 7, 2021
e0a69da
Fix generate_version_cpp target
rurban Apr 6, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 35 additions & 1 deletion CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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")
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

CMake noob here: could we use set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -DLTO") instead?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, but this is easier. It only adds it to the Release flags anyway, because only there ipo_supported will be true.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Understood, but then I wasn't able to find a way to surface this to the CaDiCaL build configuration. You might know how to make this work?

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)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm a bit nervous of the -march=native - if I'm reading the CMake correctly (a big if :-) ) then this is enabled by default on release builds, but thats quite likely to cause problems building CBMC release distributions (or at least, be a trap waiting to cause problems). native means "use any instructions available on the build machine" I believe - but we've got no real guarantee that our build machines are not higher spec/newer CPUs/whatever than any of the downstream users of our binary packages, meaning they run the risk of getting illegal instruction crashes/traps from our released binaries. While we could override default options for our binary packaging, I'd feel much more comfortable if we didn't have to...

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

True. Packagers need to get rid of that somehow. Maybe only add it to CFLAGS and CXXFLAGS via env. The idea was to find sloppy visibility and alignment, and test it in develop. Also have locally fast binaries

endif()
endif()
else()
message(STATUS "IPO / LTO not supported: <${error}>")
endif()

add_subdirectory(src)
add_subdirectory(regression)
add_subdirectory(unit)
Expand Down
3 changes: 3 additions & 0 deletions regression/invariants/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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(
"$<TARGET_FILE:driver>"
Expand Down
4 changes: 4 additions & 0 deletions scripts/glucose_CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down
4 changes: 4 additions & 0 deletions scripts/minisat2_CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down
6 changes: 6 additions & 0 deletions src/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
4 changes: 4 additions & 0 deletions src/ansi-c/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
5 changes: 4 additions & 1 deletion src/config.inc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
5 changes: 5 additions & 0 deletions src/goto-symex/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()

1 change: 1 addition & 0 deletions src/memory-analyzer/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
21 changes: 19 additions & 2 deletions src/solvers/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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")

Expand Down Expand Up @@ -104,19 +107,30 @@ 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
)

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
Expand All @@ -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)
15 changes: 11 additions & 4 deletions src/util/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand All @@ -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()
Expand All @@ -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
)

Expand Down