Enable IPO / LTO and -O3

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
@@ -103,9 +103,10 @@ endif()
 
 set(enable_cbmc_tests on CACHE BOOL "Whether CBMC tests should be enabled")
 
-set(sat_impl "minisat2" CACHE STRING
-    "This setting controls the SAT library which is used. Valid values are
-    'minisat2', 'glucose', 'cadical', 'ipasir-cadical' or 'ipasir-custom'"
+set(sat_impl "minisat2;glucose,cadical" CACHE STRING
+    "This setting control the SAT libraries which are used. Valid values are
+'minisat2', 'glucose', 'cadical', 'ipasir-cadical' or 'ipasir-custom'.
+Use multiple solvers ; seperated"
 )
 
 if(${enable_cbmc_tests})
@@ -122,8 +123,12 @@ if(DEFINED CMAKE_USE_CUDD)
 
     if(NOT EXISTS ${cudd_SOURCE_DIR}/Makefile)
         message(STATUS "Configuring Cudd-3.0.0")
-        execute_process(COMMAND ./configure WORKING_DIRECTORY ${cudd_SOURCE_DIR})
+        execute_process(COMMAND ./configure HAVE_DOXYGEN=FALSE WORKING_DIRECTORY ${cudd_SOURCE_DIR})
     endif()
+    message(STATUS "Patching Cudd-3.0.0")
+    execute_process(
+        COMMAND patch -N -p0 -i ${CMAKE_CURRENT_SOURCE_DIR}/scripts/cudd-3.0.0-postconfig.patch
+        WORKING_DIRECTORY ${cudd_SOURCE_DIR})
     message(STATUS "Building Cudd-3.0.0")
     execute_process(COMMAND make WORKING_DIRECTORY ${cudd_SOURCE_DIR})
 
@@ -209,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
@@ -222,6 +231,24 @@ 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()
+
+find_program(SED sed gsed)
+
 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/cudd-3.0.0-postconfig.patch

@@ -0,0 +1,15 @@
+--- config.status~	2024-10-31 10:58:14.082473342 +0100
++++ config.status	2024-10-31 10:59:32.373999679 +0100
+@@ -891,9 +891,9 @@
+ S["HAVE_PDFLATEX_TRUE"]=""
+ S["MAKEINDEX"]="makeindex"
+ S["PDFLATEX"]="pdflatex"
+-S["HAVE_DOXYGEN_FALSE"]="#"
+-S["HAVE_DOXYGEN_TRUE"]=""
+-S["DOXYGEN"]="doxygen"
++S["HAVE_DOXYGEN_FALSE"]=""
++S["HAVE_DOXYGEN_TRUE"]="#"
++S["DOXYGEN"]=""
+ S["CROSS_COMPILING_FALSE"]=""
+ S["CROSS_COMPILING_TRUE"]="#"
+ S["CXXCPP"]="g++ -E"

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

@@ -23,6 +23,8 @@ macro(generic_bison name)
     endif()
 
     set(bison_source "${name}_y.tab.cpp")
+    set_source_files_properties(${bison_source} PROPERTIES
+      COMPILE_FLAGS "-Dyyalloc=${name}_yyalloc -Dyysymbol_kind_t=${name}_yysymbol_kind_t -Dyytokentype=${name}_yytokentype")
     if(EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${bison_source}")
         message(FATAL_ERROR "Generated file ${bison_source} found in source tree. If you previously built with `make`, run `make clean` and try again")
     endif()
@@ -37,10 +39,15 @@ macro(generic_bison name)
         COMPILE_FLAGS "${bison_warnings_as_errors} -pyy${name}"
     )
     set(renamed_parser_header "${CMAKE_CURRENT_BINARY_DIR}/${bison_header}")
-    add_custom_command(OUTPUT "${renamed_parser_header}"
-        COMMAND "${CMAKE_COMMAND}" -E copy "${BISON_parser_OUTPUT_HEADER}" "${renamed_parser_header}"
-        MAIN_DEPENDENCY "${BISON_parser_OUTPUT_HEADER}"
-    )
+    if(${SED} STREQUAL "SED-NOTFOUND")
+      add_custom_command(OUTPUT "${renamed_parser_header}"
+          COMMAND "${CMAKE_COMMAND}" -E copy "${BISON_parser_OUTPUT_HEADER}" "${renamed_parser_header}"
+          MAIN_DEPENDENCY "${BISON_parser_OUTPUT_HEADER}")
+    else()
+      add_custom_command(OUTPUT "${renamed_parser_header}"
+          COMMAND ${SED} -e "s,enum yytokentype,enum yytokentype_${name}," <${BISON_parser_OUTPUT_HEADER} >${renamed_parser_header}
+          MAIN_DEPENDENCY "${BISON_parser_OUTPUT_HEADER}")
+    endif()
     list(REMOVE_ITEM BISON_parser_OUTPUTS "${BISON_parser_OUTPUT_HEADER}")
     list(APPEND BISON_parser_OUTPUTS "${renamed_parser_header}")
 endmacro(generic_bison)
@@ -58,6 +65,13 @@ macro(generic_flex name)
         "${CMAKE_CURRENT_BINARY_DIR}/${name}_lex.yy.cpp"
         COMPILE_FLAGS "-Pyy${name}"
     )
+    if(NOT ${SED} STREQUAL "SED-NOTFOUND")
+      set(new_flex_source "${CMAKE_CURRENT_BINARY_DIR}/${name}_lex_sed.yy.cpp")
+      add_custom_command(OUTPUT "${new_flex_source}"
+          COMMAND ${SED} -e "s,struct yyguts_t,struct yy${name}guts_t,g" <${FLEX_scanner_OUTPUTS} >${new_flex_source}
+          MAIN_DEPENDENCY "${FLEX_scanner_OUTPUTS}")
+      set(FLEX_scanner_OUTPUTS "${new_flex_source}")
+    endif()
 endmacro(generic_flex)
 
 #   Set the public include locations for a target.
@@ -84,6 +98,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/ansi-c/Makefile

@@ -104,11 +104,15 @@ all: ansi-c$(LIBEXT)
 
 ansi_c_y.tab.cpp: parser.y
 	$(YACC) $(YFLAGS) -pyyansi_c parser.y --defines=ansi_c_y.tab.h -o $@
+	$(SED) -e's,enum yytokentype,enum yytokentype_ansi,' \
+	  <ansi_c_y.tab.h >ansi_c_y.tab.h.tmp && \
+	  mv ansi_c_y.tab.h.tmp ansi_c_y.tab.h
 
 ansi_c_y.tab.h: ansi_c_y.tab.cpp
 
 ansi_c_lex.yy.cpp: scanner.l
 	$(LEX) -Pyyansi_c -o$@ scanner.l
+	$(SED) -e's,struct yyguts_t,struct yyansiguts_t,g' <$@ >[email protected] && mv [email protected] $@
 
 # extra dependencies
 ansi_c_y.tab$(OBJEXT): ansi_c_y.tab.cpp ansi_c_y.tab.h