Skip to content

Commit 97887a1

Browse files
committed
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. See the next commit to fix yyalloc name collisions.
1 parent 3e295e4 commit 97887a1

File tree

9 files changed

+65
-4
lines changed

9 files changed

+65
-4
lines changed

CMakeLists.txt

Lines changed: 21 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
7373

7474
if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU")
7575
# Ensure NDEBUG is not set for release builds
76-
set(CMAKE_CXX_FLAGS_RELEASE "-O2")
76+
set(CMAKE_CXX_FLAGS_RELEASE "-O3")
7777
set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g")
7878
# Enable lots of warnings
7979
set(CMAKE_CXX_FLAGS
@@ -212,6 +212,10 @@ function(cprover_default_properties)
212212
CXX_STANDARD ${CBMC_CXX_STANDARD}
213213
CXX_STANDARD_REQUIRED ${CBMC_CXX_STANDARD_REQUIRED}
214214
XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY ${CBMC_XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY})
215+
216+
if(ipo_supported)
217+
set_property(TARGET ${ARGN} PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
218+
endif()
215219
endfunction()
216220

217221
if(CMAKE_SYSTEM_NAME STREQUAL Linux AND
@@ -225,6 +229,22 @@ endif()
225229
option(WITH_MEMORY_ANALYZER
226230
"build the memory analyzer" ${WITH_MEMORY_ANALYZER_DEFAULT})
227231

232+
# Our requirement is 3.8
233+
if((CMAKE_MAJOR_VERSION GREATER_EQUAL 4 OR CMAKE_MINOR_VERSION GREATER_EQUAL 9)
234+
AND (CMAKE_BUILD_TYPE STREQUAL "Release"))
235+
cmake_policy(SET CMP0069 NEW)
236+
include(CheckIPOSupported)
237+
check_ipo_supported(RESULT ipo_supported OUTPUT error LANGUAGES CXX)
238+
endif()
239+
240+
if(ipo_supported)
241+
message(STATUS "IPO / LTO enabled")
242+
set_property(GLOBAL PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
243+
add_definitions(-DLTO)
244+
else()
245+
message(STATUS "IPO / LTO not supported: <${error}>")
246+
endif()
247+
228248
add_subdirectory(src)
229249
add_subdirectory(regression)
230250
add_subdirectory(unit)

regression/invariants/CMakeLists.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,8 @@
11
add_executable(driver driver.cpp)
22
target_link_libraries(driver big-int util)
3+
if(ipo_supported)
4+
set_property(TARGET driver PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
5+
endif()
36

47
add_test_pl_tests(
58
"$<TARGET_FILE:driver>"

scripts/glucose_CMakeLists.txt

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,10 @@ set_target_properties(
1515
XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
1616
)
1717

18+
if(ipo_supported)
19+
set_property(TARGET glucose-condensed PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
20+
endif()
21+
1822
if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
1923
target_compile_options(glucose-condensed PUBLIC /w)
2024
endif()

scripts/minisat2_CMakeLists.txt

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,10 @@ set_target_properties(
1616
XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
1717
)
1818

19+
if(ipo_supported)
20+
set_property(TARGET minisat2-condensed PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
21+
endif()
22+
1923
if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
2024
target_compile_options(minisat2-condensed PUBLIC /w)
2125
endif()

src/CMakeLists.txt

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,12 @@ macro(add_if_library target name)
8484
string(REGEX REPLACE "-" "_" define ${upper_name})
8585

8686
target_compile_definitions(${target} PUBLIC HAVE_${define})
87+
if(ipo_supported)
88+
set_property(TARGET ${name} PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
89+
endif()
90+
endif()
91+
if(ipo_supported)
92+
set_property(TARGET ${target} PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
8793
endif()
8894
endmacro(add_if_library)
8995

src/ansi-c/CMakeLists.txt

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,10 @@ add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
1010
DEPENDS converter ${ansi_c_library_sources})
1111

1212
add_executable(file_converter file_converter.cpp)
13+
if(ipo_supported)
14+
set_property(TARGET converter PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
15+
set_property(TARGET file_converter PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
16+
endif()
1317

1418
function(make_inc name)
1519
get_filename_component(inc_path "${CMAKE_CURRENT_BINARY_DIR}/${name}.inc" DIRECTORY)
@@ -53,9 +57,10 @@ add_custom_command(
5357
)
5458

5559
if(NOT "${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
60+
if(NOT ipo_supported)
5661
add_custom_target(c_library_check
57-
DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
58-
)
62+
DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp)
63+
endif()
5964
endif()
6065

6166
################################################################################

src/config.inc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,12 @@ ifeq ($(CPROVER_WITH_PROFILING),1)
1717
endif
1818

1919
# Select optimisation or debug info
20-
#CXXFLAGS += -O2 -DNDEBUG
20+
#CXXFLAGS += -O3 -DNDEBUG -flto -DLTO
2121
#CXXFLAGS += -O0 -g
2222

23+
# Matching -flto above
24+
#LINKFLAGS = -ftlo
25+
2326
# With GCC this adds function names in stack backtraces
2427
#LINKFLAGS = -rdynamic
2528

src/goto-symex/CMakeLists.txt

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,7 @@ if(CMAKE_USE_CUDD)
88
endif()
99

1010
target_link_libraries(goto-symex util)
11+
12+
if(ipo_supported)
13+
set_property(TARGET goto-symex PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
14+
endif()

src/solvers/CMakeLists.txt

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,9 @@ list(REMOVE_ITEM sources
5858
)
5959

6060
add_library(solvers ${sources})
61+
if(ipo_supported)
62+
set_property(TARGET solvers PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
63+
endif()
6164

6265
include("${CBMC_SOURCE_DIR}/cmake/DownloadProject.cmake")
6366

@@ -158,6 +161,9 @@ foreach(SOLVER ${sat_impl})
158161
)
159162

160163
add_library(cadical_ipasir STATIC IMPORTED)
164+
if(ipo_supported)
165+
set_property(TARGET cadical_ipasir PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
166+
endif()
161167
set_property(TARGET cadical_ipasir
162168
PROPERTY IMPORTED_LOCATION ${cadical_SOURCE_DIR}/build/libcadical.a
163169
)
@@ -203,6 +209,9 @@ foreach(SOLVER ${sat_impl})
203209
)
204210

205211
add_library(ipasir_custom STATIC IMPORTED)
212+
if(ipo_supported)
213+
set_property(TARGET cadical_custom PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
214+
endif()
206215
set_property(TARGET ipasir_custom
207216
PROPERTY IMPORTED_LOCATION ${IPASIR_LIB}
208217
)
@@ -228,5 +237,8 @@ endif()
228237
# Executable
229238
add_executable(smt2_solver smt2/smt2_solver.cpp)
230239
target_link_libraries(smt2_solver solvers)
240+
if(ipo_supported)
241+
set_property(TARGET smt2_solver PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
242+
endif()
231243

232244
generic_includes(solvers)

0 commit comments

Comments
 (0)