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.

Author: rurban

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)

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(
     "$<TARGET_FILE:driver>"

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()

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()

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)
 

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"

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
 

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()
+

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)

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)