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.

Author: rurban

CMakeLists.txt

@@ -73,7 +73,7 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
 
 if("${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
@@ -214,6 +214,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 AND
@@ -227,6 +231,22 @@ endif()
 option(WITH_MEMORY_ANALYZER
   "build the memory analyzer" ${WITH_MEMORY_ANALYZER_DEFAULT})
 
+# Our requirement is 3.8
+if((CMAKE_MAJOR_VERSION GREATER_EQUAL 4 OR 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

@@ -15,6 +15,10 @@ set_target_properties(
     XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
 )
 
+if(ipo_supported)
+    set_property(TARGET glucose-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

@@ -16,6 +16,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

@@ -84,6 +84,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)
     get_filename_component(inc_path "${CMAKE_CURRENT_BINARY_DIR}/${name}.inc" DIRECTORY)
@@ -53,9 +57,10 @@ add_custom_command(
 )
 
 if(NOT "${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+  if(NOT ipo_supported)
     add_custom_target(c_library_check
-        DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
-)
+        DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp)
+  endif()
 endif()
 
 ################################################################################

src/config.inc

@@ -17,9 +17,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,7 @@ 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/solvers/CMakeLists.txt

@@ -58,6 +58,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")
 
@@ -177,6 +180,9 @@ foreach(SOLVER ${sat_impl})
         )
 
         add_library(cadical_ipasir STATIC IMPORTED)
+        if(ipo_supported)
+          set_property(TARGET cadical_ipasir PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
+        endif()
         set_property(TARGET cadical_ipasir
             PROPERTY IMPORTED_LOCATION ${cadical_SOURCE_DIR}/build/libcadical.a
         )
@@ -222,6 +228,9 @@ foreach(SOLVER ${sat_impl})
         )
 
         add_library(ipasir_custom STATIC IMPORTED)
+        if(ipo_supported)
+          set_property(TARGET cadical_custom PROPERTY INTERPROCEDURAL_OPTIMIZATION True)
+        endif()
         set_property(TARGET ipasir_custom
             PROPERTY IMPORTED_LOCATION ${IPASIR_LIB}
         )
@@ -247,5 +256,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)