Optionally enable interprocedural optimization (#7209)

This commit adds support for enabling interprocedural optimization. The
option is enabled by default for --best builds and cuts down our
executable size from about 33M to 20M.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index e9484986bc29d6ae1014a28e0ae9b2fe0c179bce..e2e24ecf13207d00d14c0b8ae0c3b7f559a231c7 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -20,6 +20,7 @@ cmake_minimum_required(VERSION 3.9)
 
 project(cvc5)
 
+include(CheckIPOSupported)
 include(GNUInstallDirs)
 
 set(CVC5_MAJOR   1) # Major component of the version of cvc5.
@@ -105,6 +106,7 @@ cvc5_option(ENABLE_SHARED         "Build as shared library")
 cvc5_option(ENABLE_STATIC_BINARY
             "Build static binaries with statically linked system libraries")
 cvc5_option(ENABLE_AUTO_DOWNLOAD  "Enable automatic download of dependencies")
+cvc5_option(ENABLE_IPO            "Enable interprocedural optimization")
 # >> 2-valued: ON OFF
 #    > for options where we don't need to detect if set by user (default: OFF)
 option(ENABLE_BEST             "Enable dependencies known to give best performance")
@@ -234,6 +236,14 @@ if ("${LD_VERSION}" MATCHES "GNU gold")
   message(STATUS "Using GNU gold linker.")
 endif ()
 
+#-----------------------------------------------------------------------------#
+# Use interprocedural optimization if requested
+
+if(ENABLE_IPO)
+  set(CMAKE_INTERPROCEDURAL_OPTIMIZATION TRUE)
+endif()
+
+
 #-----------------------------------------------------------------------------#
 # Option defaults (three-valued options (cvc5_option(...)))
 #
@@ -660,6 +670,7 @@ print_config("Static binary             " ${ENABLE_STATIC_BINARY})
 print_config("Python bindings           " ${BUILD_BINDINGS_PYTHON})
 print_config("Java bindings             " ${BUILD_BINDINGS_JAVA})
 print_config("Python2                   " ${USE_PYTHON2})
+print_config("Interprocedural opt.      " ${ENABLE_IPO})
 message("")
 print_config("ABC                       " ${USE_ABC})
 print_config("CryptoMiniSat             " ${USE_CRYPTOMINISAT} FOUND_SYSTEM ${CryptoMiniSat_FOUND_SYSTEM})

diff --git a/configure.sh b/configure.sh
index 9338caf6d5b66c5e86ee5003ef288188ea0863f7..0db8659cada7264c7b868a009c741791b05dc2bb 100755 (executable)
--- a/configure.sh
+++ b/configure.sh
@@ -20,7 +20,7 @@ General options;
   --prefix=STR             install directory
   --program-prefix=STR     prefix of binaries prepended on make install
   --name=STR               use custom build directory name (optionally: +path)
-  --best                   turn on dependencies known to give best performance
+  --best                   turn on dependencies and options known to give best performance
   --gpl                    permit GPL dependencies, if available
   --arm64                  cross-compile for Linux ARM 64 bit
   --win64                  cross-compile for Windows 64 bit
@@ -53,6 +53,7 @@ The following flags enable optional features (disable with --no-<option name>).
   --ubsan                  build with UBSan instrumentation
   --tsan                   build with TSan instrumentation
   --werror                 build with -Werror
+  --ipo                    build with interprocedural optimization
 
 Optional Packages:
 The following flags enable optional packages (disable with --no-<option name>).
@@ -141,6 +142,7 @@ valgrind=default
 win64=default
 arm64=default
 werror=default
+ipo=default
 
 abc_dir=default
 glpk_dir=default
@@ -171,11 +173,15 @@ do
 
     --werror) werror=ON;;
 
+    --ipo) ipo=ON;;
+    --no-ipo) ipo=OFF;;
+
     --assertions) assertions=ON;;
     --no-assertions) assertions=OFF;;
 
     # Best configuration
     --best)
+      ipo=ON
       abc=ON
       cln=ON
       cryptominisat=ON
@@ -330,6 +336,8 @@ fi
   && cmake_opts="$cmake_opts -DENABLE_UBSAN=$ubsan"
 [ $tsan != default ] \
   && cmake_opts="$cmake_opts -DENABLE_TSAN=$tsan"
+[ $ipo != default ] \
+  && cmake_opts="$cmake_opts -DENABLE_IPO=$ipo"
 [ $assertions != default ] \
   && cmake_opts="$cmake_opts -DENABLE_ASSERTIONS=$assertions"
 [ $comp_inc != default ] \