From 4cc2b292c0cc8759da7a525e63dbfefdb06d6a01 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 28 Apr 2017 17:59:04 +0100
Subject: [PATCH 01/12] [CMake] Remove compiler flag overrides and support for
 C language.

The setting of overrides was broken (the CXX flags were not set but
the C flags were) and we aren't even using the C compiler any more.

The C compiler is used by the example C project but that is built
as an external project now so we don't need C support anymore.

The setting of defaults was also very fragile. CMake has quite
complicated support here (e.g. MSVC with a clang based tool chain) which
would likely not work properly with the override approach as it existed.

This means we loose some of the custom linker flags we were setting for
MSVC but we were never doing a great job of replicating the exact set of
flags used in the old build system anyway. Subsequent commits will
gradually fix this.
---
 CMakeLists.txt                                |  4 +-
 .../cmake/cmake/compiler_flags_override.cmake | 43 -------------------
 2 files changed, 1 insertion(+), 46 deletions(-)
 delete mode 100644 contrib/cmake/cmake/compiler_flags_override.cmake

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 47a081e75..ab3976aea 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -24,9 +24,7 @@ if (NOT (EXISTS "${CMAKE_SOURCE_DIR}/src/CMakeLists.txt"))
           "``python contrib/cmake/bootstrap.py create``")
 endif()
 
-# This overrides the default flags for the different CMAKE_BUILD_TYPEs
-set(CMAKE_USER_MAKE_RULES_OVERRIDE "${CMAKE_CURRENT_SOURCE_DIR}/cmake/compiler_flags_override.cmake")
-project(Z3 C CXX)
+project(Z3 CXX)
 
 ################################################################################
 # Project version
diff --git a/contrib/cmake/cmake/compiler_flags_override.cmake b/contrib/cmake/cmake/compiler_flags_override.cmake
deleted file mode 100644
index c6005396b..000000000
--- a/contrib/cmake/cmake/compiler_flags_override.cmake
+++ /dev/null
@@ -1,43 +0,0 @@
-# This file overrides the default compiler flags for CMake's built-in
-# configurations (CMAKE_BUILD_TYPE). Most compiler flags should not be set here.
-# The main purpose is to have very fine grained control of the compiler flags.
-if (CMAKE_C_COMPILER_ID)
-  set(_lang C)
-elseif(CMAKE_CXX_COMPILER_ID)
-  set(_lang CXX)
-else()
-  message(FATAL_ERROR "Unknown language")
-endif()
-
-# TODO: The value of doing this is debatable. The flags set here are pretty
-# much the CMake defaults now (they didn't use to be) and makes extra work for
-# us when supporting different compilers. Perhaps we should move the remaining
-# code that sets non-default flags out into the CMakeLists.txt files and remove
-# any overrides here?
-if (("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "GNU"))
-  # Taken from Modules/Compiler/GNU.cmake
-  set(CMAKE_${_lang}_FLAGS_INIT "")
-  set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "-g -O0")
-  set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "-Os -DNDEBUG")
-  set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "-O3 -DNDEBUG")
-  set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "-O2 -g -DNDEBUG")
-  # FIXME: Remove "x.." when CMP0054 is set to NEW
-elseif ("x${CMAKE_${_lang}_COMPILER_ID}" STREQUAL "xMSVC")
-  # FIXME: Perhaps we should be using /MD instead?
-  set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "/MTd /Zi /Ob0 /Od /RTC1")
-  set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT     "/MT /O1 /Ob1 /D NDEBUG")
-  set(CMAKE_${_lang}_FLAGS_RELEASE_INIT        "/MT /O2 /Ob2 /D NDEBUG")
-  set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "/MT /Zi /O2 /Ob1 /D NDEBUG")
-  # Override linker flags (see Windows-MSVC.cmake for CMake's defaults)
-  # The stack size comes from the Python build system.
-  set(_msvc_stack_size "8388608")
-  set(CMAKE_EXE_LINKER_FLAGS_DEBUG_INIT "/debug /INCREMENTAL:NO /STACK:${_msvc_stack_size}")
-  set(CMAKE_EXE_LINKER_FLAGS_RELWITHDEBINFO_INIT "/debug /INCREMENTAL:NO /STACK:${_msvc_stack_size}")
-  set(CMAKE_EXE_LINKER_FLAGS_MINSIZEREL_INIT "/INCREMENTAL:NO /STACK:${_msvc_stack_size}")
-  set(CMAKE_EXE_LINKER_FLAGS_RELEASE_INIT "/INCREMENTAL:NO /STACK:${_msvc_stack_size}")
-  unset(_msvc_stack_size)
-else()
-  message(FATAL_ERROR "Overrides not set for ${_lang} compiler \"${CMAKE_${_lang}_COMPILER_ID}\"")
-endif()
-
-unset(_lang)

From f568b2478ff743b735f5e1ab03325040ea320cc9 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 28 Apr 2017 21:30:36 +0100
Subject: [PATCH 02/12] [CMake] Report the various values of CMAKE_CXX_FLAGS,
 CMAKE_CXX_FLAGS_<CONFIG>, CMAKE_<TYPE>_LINKER_FLAGS, and
 CMAKE_<TYPE>_LINKER_FLAGS_<CONFIG>.

This is useful for debugging where some flags come from. Now that
we don't explicitly set the defaults it useful to see which default
values we are getting from CMake.
---
 CMakeLists.txt | 24 +++++++++++++++++++++++-
 1 file changed, 23 insertions(+), 1 deletion(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index ab3976aea..795a23320 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -153,13 +153,13 @@ set(Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS "")
 # Build type
 ################################################################################
 message(STATUS "CMake generator: ${CMAKE_GENERATOR}")
+set(available_build_types Debug Release RelWithDebInfo MinSizeRel)
 if (DEFINED CMAKE_CONFIGURATION_TYPES)
   # Multi-configuration build (e.g. Visual Studio and Xcode). Here
   # CMAKE_BUILD_TYPE doesn't matter
   message(STATUS "Available configurations: ${CMAKE_CONFIGURATION_TYPES}")
 else()
   # Single configuration generator (e.g. Unix Makefiles, Ninja)
-  set(available_build_types Debug Release RelWithDebInfo MinSizeRel)
   if(NOT CMAKE_BUILD_TYPE)
     message(STATUS "CMAKE_BUILD_TYPE is not set. Setting default")
     message(STATUS "The available build types are: ${available_build_types}")
@@ -374,6 +374,28 @@ if (BUILD_LIBZ3_SHARED)
   endif()
 endif()
 
+################################################################################
+# Report default CMake flags
+################################################################################
+# This is mainly for debugging.
+message(STATUS "CMAKE_CXX_FLAGS: \"${CMAKE_CXX_FLAGS}\"")
+message(STATUS "CMAKE_EXE_LINKER_FLAGS: \"${CMAKE_EXE_LINKER_FLAGS}\"")
+message(STATUS "CMAKE_STATIC_LINKER_FLAGS: \"${CMAKE_STATIC_LINKER_FLAGS}\"")
+message(STATUS "CMAKE_SHARED_LINKER_FLAGS: \"${CMAKE_SHARED_LINKER_FLAGS}\"")
+if (DEFINED CMAKE_CONFIGURATION_TYPES)
+  # Multi configuration generator
+  string(TOUPPER "${available_build_types}" build_types_to_report)
+else()
+  # Single configuration generator
+  string(TOUPPER "${CMAKE_BUILD_TYPE}" build_types_to_report)
+endif()
+foreach (_build_type ${build_types_to_report})
+  message(STATUS "CMAKE_CXX_FLAGS_${_build_type}: \"${CMAKE_CXX_FLAGS_${_build_type}}\"")
+  message(STATUS "CMAKE_EXE_LINKER_FLAGS_${_build_type}: \"${CMAKE_EXE_LINKER_FLAGS_${_build_type}}\"")
+  message(STATUS "CMAKE_SHARED_LINKER_FLAGS_${_build_type}: \"${CMAKE_SHARED_LINKER_FLAGS_${_build_type}}\"")
+  message(STATUS "CMAKE_STATIC_LINKER_FLAGS_${_build_type}: \"${CMAKE_STATIC_LINKER_FLAGS_${_build_type}}\"")
+endforeach()
+
 ################################################################################
 # Report Z3_COMPONENT flags
 ################################################################################

From fe1af4bcdb7c4f4d85874e449fae3db8cf0a49ad Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Fri, 28 Apr 2017 23:28:04 +0100
Subject: [PATCH 03/12] [CMake] Teach build system to pass `/fp:precise` to
 compiler when using MSVC. This is set by the old build system but we weren't
 setting it. This actually MSVC's default but in an effort to try to behave
 more like the old build system we will set it anyway.

---
 CMakeLists.txt                            | 9 +++++++++
 contrib/cmake/cmake/z3_add_cxx_flag.cmake | 1 +
 2 files changed, 10 insertions(+)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 795a23320..6e858a421 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -324,6 +324,15 @@ if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" ST
   unset(SSE_FLAGS)
 endif()
 
+# FIXME: Remove "x.." when CMP0054 is set to NEW
+if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+  # This is the default for MSVC already but to replicate the
+  # python/Makefile build system behaviour this flag is set
+  # explicitly.
+  z3_add_cxx_flag("/fp:precise" REQUIRED)
+endif()
+# There doesn't seem to be an equivalent for clang/gcc
+
 ################################################################################
 # Threading support
 ################################################################################
diff --git a/contrib/cmake/cmake/z3_add_cxx_flag.cmake b/contrib/cmake/cmake/z3_add_cxx_flag.cmake
index 0c56bb0f6..8bffd7de3 100644
--- a/contrib/cmake/cmake/z3_add_cxx_flag.cmake
+++ b/contrib/cmake/cmake/z3_add_cxx_flag.cmake
@@ -7,6 +7,7 @@ function(z3_add_cxx_flag flag)
   string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
   string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
   string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  string(REPLACE ":" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
   unset(HAS_${SANITIZED_FLAG_NAME})
   CHECK_CXX_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME})
   if (z3_add_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME})

From fb403229bd7a2bc422afe574c98dd858035c42aa Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 29 Apr 2017 00:29:26 +0100
Subject: [PATCH 04/12] [CMake] CMake's default value for CMAKE_CXX_FLAGS
 includes `/W3` remove this so we can have fine grained control of warnings.

---
 contrib/cmake/cmake/compiler_warnings.cmake | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/contrib/cmake/cmake/compiler_warnings.cmake b/contrib/cmake/cmake/compiler_warnings.cmake
index c214e4464..e49e43947 100644
--- a/contrib/cmake/cmake/compiler_warnings.cmake
+++ b/contrib/cmake/cmake/compiler_warnings.cmake
@@ -15,6 +15,13 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
   # FIXME: Remove "x.." when CMP0054 is set to NEW
 elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
   list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS})
+
+  # CMake's default flags include /W3 already so remove them if
+  # they already exist.
+  if ("${CMAKE_CXX_FLAGS}" MATCHES "/W3")
+    string(REPLACE "/W3" "" _cmake_cxx_flags_remove_w3 "${CMAKE_CXX_FLAGS}")
+    set(CMAKE_CXX_FLAGS "${_cmake_cxx_flags_remove_w3}" CACHE STRING "" FORCE)
+  endif()
 else()
   message(AUTHOR_WARNING "Unknown compiler")
 endif()

From 0e1343e78db9d396240151af436a1a2028cc40fa Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 29 Apr 2017 01:21:49 +0100
Subject: [PATCH 05/12] [CMake] Add support for link time optimization (LTO).

This analogous to the `--optimize` flag in the Python/Makefile
build system except that we now support doing LTO with Clang/GCC
as well. However it is probably best to avoid doing LTO with
Clang or GCC for now because I see a bunch of warnings about
ODR violations when building with LTO.

LTO can be enabled with the new `LINK_TIME_OPTIMIZATION` option
which is off by default.
---
 CMakeLists.txt                         |  5 +++
 README-CMake.md                        |  1 +
 contrib/cmake/cmake/compiler_lto.cmake | 52 ++++++++++++++++++++++++++
 3 files changed, 58 insertions(+)
 create mode 100644 contrib/cmake/cmake/compiler_lto.cmake

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 6e858a421..8afc6339b 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -383,6 +383,11 @@ if (BUILD_LIBZ3_SHARED)
   endif()
 endif()
 
+################################################################################
+# Link time optimization
+################################################################################
+include(${CMAKE_SOURCE_DIR}/cmake/compiler_lto.cmake)
+
 ################################################################################
 # Report default CMake flags
 ################################################################################
diff --git a/README-CMake.md b/README-CMake.md
index 4bbbd36a8..9289d40f1 100644
--- a/README-CMake.md
+++ b/README-CMake.md
@@ -292,6 +292,7 @@ The following useful options can be passed to CMake whilst configuring.
     when running the ``install`` target.
 * ``ALWAYS_BUILD_DOCS`` - BOOL. If set to ``TRUE`` and ``BUILD_DOCUMENTATION`` is ``TRUE`` then documentation for API bindings will always be built.
     Disabling this is useful for faster incremental builds. The documentation can be manually built by invoking the ``api_docs`` target.
+* ``LINK_TIME_OPTIMIZATION`` - BOOL. If set to ``TRUE`` link time optimization will be enabled.
 
 On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface.
 
diff --git a/contrib/cmake/cmake/compiler_lto.cmake b/contrib/cmake/cmake/compiler_lto.cmake
new file mode 100644
index 000000000..b90890f59
--- /dev/null
+++ b/contrib/cmake/cmake/compiler_lto.cmake
@@ -0,0 +1,52 @@
+option(LINK_TIME_OPTIMIZATION "Use link time optimiziation" OFF)
+
+if (LINK_TIME_OPTIMIZATION)
+  message(STATUS "LTO enabled")
+  set(build_types_with_lto "RELEASE" "RELWITHDEBINFO")
+  if (DEFINED CMAKE_CONFIGURATION_TYPES)
+    # Multi configuration generator
+    message(STATUS "Note LTO is only enabled for the following configurations: ${build_types_with_lto}")
+  else()
+    # Single configuration generator
+    string(TOUPPER "${CMAKE_BUILD_TYPE}" _build_type_upper)
+    list(FIND build_types_with_lto "${_build_type_upper}" _index)
+    if ("${_index}" EQUAL -1)
+      message(FATAL_ERROR "Configuration ${CMAKE_BUILD_TYPE} does not support LTO."
+        "You should set LINK_TIME_OPTIMIZATION to OFF.")
+    endif()
+  endif()
+
+  set(_lto_compiler_flag "")
+  set(_lto_linker_flag "")
+  if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR
+      ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
+      set(_lto_compiler_flag "-flto")
+      set(_lto_linker_flag "-flto")
+  # FIXME: Remove "x.." when CMP0054 is set to NEW
+  elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+    set(_lto_compiler_flag "/GL")
+    set(_lto_linker_flag "/LTCG")
+  else()
+    message(FATAL_ERROR "Can't enable LTO for compiler \"${CMAKE_CXX_COMPILER_ID}\"."
+      "You should set LINK_TIME_OPTIMIZATION to OFF.")
+  endif()
+  CHECK_CXX_COMPILER_FLAG("${_lto_compiler_flag}" HAS_LTO)
+  if (NOT HAS_LTO)
+    message(FATAL_ERROR "Compiler does not support LTO")
+  endif()
+
+  foreach (_config ${build_types_with_lto})
+    # Set flags compiler and linker flags globally rather than using
+    # `Z3_COMPONENT_CXX_FLAGS` and `Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS`
+    # respectively.  We need per configuration compiler and linker flags. The
+    # `LINK_FLAGS` property (which we populate with
+    # `Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS`) doesn't seem to support generator
+    # expressions so we can't do `$<$<CONFIG:Release>:${_lto_linker_flag}>`.
+    set(CMAKE_CXX_FLAGS_${_config} "${CMAKE_CXX_FLAGS_${_config}} ${_lto_compiler_flag}")
+    set(CMAKE_EXE_LINKER_FLAGS_${_config} "${CMAKE_EXE_LINKER_FLAGS_${_config}} ${_lto_linker_flag}")
+    set(CMAKE_SHARED_LINKER_FLAGS_${_config} "${CMAKE_SHARED_LINKER_FLAGS_${_config}} ${_lto_linker_flag}")
+    set(CMAKE_STATIC_LINKER_FLAGS_${_config} "${CMAKE_STATIC_LINKER_FLAGS_${_config}} ${_lto_linker_flag}")
+  endforeach()
+else()
+  message(STATUS "LTO disabled")
+endif()

From 870be706e958f37d6bc7a0ca0347704b56a9c08d Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 29 Apr 2017 11:00:27 +0100
Subject: [PATCH 06/12] [CMake] Try to do a better job of matching the old
 build system's compiler defines and flags when using MSVC.

There are lots of defines and flags that I'm unsure about so in
some cases I've changed the behaviour slightly (if I'm confident
the behaviour in the old build system is wrong) or not added the
flag/define at all but just left comments noting what the old build
system did and why I disagree with the old build system's choices.
---
 CMakeLists.txt                               |   8 ++
 contrib/cmake/cmake/msvc_legacy_quirks.cmake | 112 +++++++++++++++++++
 2 files changed, 120 insertions(+)
 create mode 100644 contrib/cmake/cmake/msvc_legacy_quirks.cmake

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 8afc6339b..aa347ae66 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -388,6 +388,14 @@ endif()
 ################################################################################
 include(${CMAKE_SOURCE_DIR}/cmake/compiler_lto.cmake)
 
+################################################################################
+# MSVC specific flags inherited from old build system
+################################################################################
+# FIXME: Remove "x.." when CMP0054 is set to NEW
+if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+  include(${CMAKE_SOURCE_DIR}/cmake/msvc_legacy_quirks.cmake)
+endif()
+
 ################################################################################
 # Report default CMake flags
 ################################################################################
diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake
new file mode 100644
index 000000000..050d34553
--- /dev/null
+++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake
@@ -0,0 +1,112 @@
+# This file ether sets or notes various compiler and linker flags for MSVC that
+# were defined by the old python/Makefile based build system but
+# don't obviously belong in the other sections in the CMake build system.
+
+################################################################################
+# Compiler definitions
+################################################################################
+# FIXME: All the commented out defines should be removed once
+# we are confident it is correct to not set them.
+set(Z3_MSVC_LEGACY_DEFINES
+  # Don't set `_DEBUG`. The old build sytem sets this but this
+  # is wrong. MSVC will set this depending on which runtime is being used.
+  # See https://msdn.microsoft.com/en-us/library/b0084kay.aspx
+  # _DEBUG
+
+  # The old build system only set `UNICODE` and `_UNICODE` for x86_64 release.
+  # That seems completly wrong so set it for all configurations.
+  # According to https://blogs.msdn.microsoft.com/oldnewthing/20040212-00/?p=40643/
+  # `UNICODE` affects Windows headers and `_UNICODE` affects C runtime header files.
+  # There is some discussion of this define at https://msdn.microsoft.com/en-us/library/dybsewaf.aspx
+  UNICODE
+  _UNICODE
+)
+
+if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
+  list(APPEND Z3_MSVC_LEGACY_DEFINES ""
+    # Don't set `_LIB`. The old build system sets this for x86_64 release
+    # build. This flag doesn't seem to be documented but a stackoverflow
+    # post hints that this is usually set when building a static library.
+    # See http://stackoverflow.com/questions/35034683/how-to-tell-if-current-project-is-dll-or-static-lib
+    # This seems wrong give that the old build system set this regardless
+    # whether or not libz3 was static or shared so its probably best
+    # to not set for now.
+    #$<$<CONFIG:Release>:_LIB>
+    #$<$<CONFIG:RelWithDebInfo>:_LIB>
+
+    # Don't set `_CONSOLE`. The old build system sets for all configurations
+    # except x86_64 release. It seems ( https://codeyarns.com/2010/12/02/visual-c-windows-and-console-subsystems/ )
+    # that `_CONSOLE` used to be defined by older Visual C++ environments.
+    # Setting this undocumented option seems like a bad idea so let's not do it.
+    #$<$<CONFIG:Debug:_CONSOLE>
+    #$<$<CONFIG:MinSizeRel:_CONSOLE>
+
+    # Don't set `ASYNC_COMMANDS`. The old build system sets this for x86_64
+    # release but this macro does not appear to be used anywhere and is not
+    # documented so don't set it for now.
+    #$<$<CONFIG:Release>:ASYNC_COMMANDS>
+    #$<$<CONFIG:RelWithDebInfo>:ASYNC_COMMANDS>
+  )
+else()
+  list(APPEND Z3_MSVC_LEGACY_DEFINES ""
+    # Don't set `_CONSOLE`. See reasoning above.
+    #_CONSOLE
+  )
+endif()
+
+# Note we don't set WIN32 or _WINDOWS because
+# CMake provides that for us. As a sanity check make sure the option
+# is present.
+if (NOT "${CMAKE_CXX_FLAGS}" MATCHES "/D[ ]*WIN32")
+  message(FATAL_ERROR "\"/D WIN32\" is missing")
+endif()
+if (NOT "${CMAKE_CXX_FLAGS}" MATCHES "/D[ ]*_WINDOWS")
+  message(FATAL_ERROR "\"/D _WINDOWS\" is missing")
+endif()
+
+list(APPEND Z3_COMPONENT_CXX_DEFINES ${Z3_MSVC_LEGACY_DEFINES})
+
+################################################################################
+# Compiler flags
+################################################################################
+# By default in MSVC this is on but the old build system set this explicitly so
+# for completeness set it too.
+# See https://msdn.microsoft.com/en-us/library/dh8che7s.aspx
+z3_add_cxx_flag("/Zc:wchar_t" REQUIRED)
+# By default in MSVC this on but the old build system set this explicitly so
+# for completeness set it too.
+z3_add_cxx_flag("/Zc:forScope" REQUIRED)
+
+# FIXME: We might want to move this out somewhere else if we decide
+# we want to set `-fno-omit-frame-pointer` for gcc/clang.
+# No omit frame pointer
+set(NO_OMIT_FRAME_POINTER_MSVC_FLAG "/Oy-")
+CHECK_CXX_COMPILER_FLAG(${NO_OMIT_FRAME_POINTER_MSVC_FLAG} HAS_MSVC_NO_OMIT_FRAME_POINTER)
+if (NOT HAS_MSVC_NO_OMIT_FRAME_POINTER)
+  message(FATAL_ERROR "${NO_OMIT_FRAME_POINTER_MSVC_FLAG} flag not supported")
+endif()
+
+# FIXME: This doesn't make a huge amount of sense but the old
+# build system kept the frame pointer for all configurations
+# except x86_64 release (I don't know why the frame pointer
+# is kept for i686 release).
+if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
+  list(APPEND Z3_COMPONENT_CXX_FLAGS
+    $<$<CONFIG:Debug>:${NO_OMIT_FRAME_POINTER_MSVC_FLAG}>
+    $<$<CONFIG:MinSizeRel>:${NO_OMIT_FRAME_POINTER_MSVC_FLAG}>
+  )
+else()
+  list(APPEND Z3_COMPONENT_CXX_FLAGS ${NO_OMIT_FRAME_POINTER_MSVC_FLAG})
+endif()
+
+if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" STREQUAL "i686"))
+  # Use __cdecl calling convention. Apparently this is MSVC's default
+  # but the old build system set it so for completeness set it too.
+  # See https://msdn.microsoft.com/en-us/library/46t77ak2.aspx
+  z3_add_cxx_flag("/Gd" REQUIRED)
+endif()
+
+# FIXME: The old build system explicitly disables code analysis.
+# I don't know why. Duplicate this behaviour for now.
+# See https://msdn.microsoft.com/en-us/library/ms173498.aspx
+z3_add_cxx_flag("/analyze-" REQUIRED)

From 5893aea60250c0e55475fd53326a0929a8028c8a Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 29 Apr 2017 12:12:54 +0100
Subject: [PATCH 07/12] [CMake] When building with MSVC and without
 `WARNINGS_AS_ERRORS` pass `/WX-` to MSVC. Although this is not necessary this
 duplicates the behaviour of the old build system.

---
 contrib/cmake/cmake/compiler_warnings.cmake | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/contrib/cmake/cmake/compiler_warnings.cmake b/contrib/cmake/cmake/compiler_warnings.cmake
index e49e43947..e02b28b2c 100644
--- a/contrib/cmake/cmake/compiler_warnings.cmake
+++ b/contrib/cmake/cmake/compiler_warnings.cmake
@@ -44,4 +44,11 @@ if (WARNINGS_AS_ERRORS)
   message(STATUS "Treating compiler warnings as errors")
 else()
   message(STATUS "Not treating compiler warnings as errors")
+  # FIXME: Remove "x.." when CMP0054 is set to NEW
+  if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+    # Warnings as errors is off by default for MSVC so setting this
+    # is not necessary but this duplicates the behaviour of the old
+    # build system.
+    list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX-")
+  endif()
 endif()

From c9aac0ba7787b98b3f2dd4268d252f434d3e2c1a Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 29 Apr 2017 12:48:49 +0100
Subject: [PATCH 08/12] [CMake] When building with MSVC try to disable
 incremental linking for all builds.

---
 contrib/cmake/cmake/msvc_legacy_quirks.cmake | 31 ++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake
index 050d34553..9411d112b 100644
--- a/contrib/cmake/cmake/msvc_legacy_quirks.cmake
+++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake
@@ -110,3 +110,34 @@ endif()
 # I don't know why. Duplicate this behaviour for now.
 # See https://msdn.microsoft.com/en-us/library/ms173498.aspx
 z3_add_cxx_flag("/analyze-" REQUIRED)
+
+################################################################################
+# Linker flags
+################################################################################
+
+# By default CMake enables incremental linking for Debug and RelWithDebInfo
+# builds. The old build sytem disables it for all builds so try to do the same
+# by changing all configurations if necessary
+
+string(TOUPPER "${available_build_types}" _build_types_as_upper)
+foreach (_build_type ${_build_types_as_upper})
+  foreach (t EXE SHARED STATIC)
+    set(_replacement "/INCREMENTAL:NO")
+    # Remove any existing incremental flags
+    string(REGEX REPLACE
+      "/INCREMENTAL:YES"
+      "${_replacement}"
+      _replaced_linker_flags
+      "${CMAKE_${t}_LINKER_FLAGS_${_build_type}}")
+    string(REGEX REPLACE
+      "(/INCREMENTAL$)|(/INCREMENTAL )"
+      "${_replacement} "
+      _replaced_linker_flags
+      "${_replaced_linker_flags}")
+    if (NOT "${_replaced_linker_flags}" MATCHES "${_replacement}")
+      # Flag not present. Add it
+      string(APPEND _replaced_linker_flags " ${_replacement}")
+    endif()
+    set(CMAKE_${t}_LINKER_FLAGS_${_build_type} "${_replaced_linker_flags}")
+  endforeach()
+endforeach()

From 364bcde6c1daa9efa4db30cad5fc179cc304d287 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 29 Apr 2017 13:28:44 +0100
Subject: [PATCH 09/12] [CMake] When building with MSVC pass the `/STACK:`
 argument to the linker like the old build system does.

---
 contrib/cmake/cmake/msvc_legacy_quirks.cmake | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake
index 9411d112b..d0ca00c83 100644
--- a/contrib/cmake/cmake/msvc_legacy_quirks.cmake
+++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake
@@ -118,7 +118,6 @@ z3_add_cxx_flag("/analyze-" REQUIRED)
 # By default CMake enables incremental linking for Debug and RelWithDebInfo
 # builds. The old build sytem disables it for all builds so try to do the same
 # by changing all configurations if necessary
-
 string(TOUPPER "${available_build_types}" _build_types_as_upper)
 foreach (_build_type ${_build_types_as_upper})
   foreach (t EXE SHARED STATIC)
@@ -141,3 +140,12 @@ foreach (_build_type ${_build_types_as_upper})
     set(CMAKE_${t}_LINKER_FLAGS_${_build_type} "${_replaced_linker_flags}")
   endforeach()
 endforeach()
+
+# The original build system passes `/STACK:` to the linker.
+# This size comes from the original build system.
+# FIXME: What is the rationale behind this?
+set(STACK_SIZE_MSVC_LINKER 8388608)
+# MSVC documentation (https://msdn.microsoft.com/en-us/library/35yc2tc3.aspx)
+# says this only matters for executables which is why this is not being
+# set for CMAKE_SHARED_LINKER_FLAGS or CMAKE_STATIC_LINKER_FLAGS.
+string(APPEND CMAKE_EXE_LINKER_FLAGS " /STACK:${STACK_SIZE_MSVC_LINKER}")

From d032dbcbb238e9be365d9b8057190d9f3f375def Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 29 Apr 2017 13:49:53 +0100
Subject: [PATCH 10/12] [CMake] When using MSVC set the `/SUBSYSTEM:` argument
 given to the linker. This mimics the behaviour of the old build system.

---
 contrib/cmake/cmake/msvc_legacy_quirks.cmake | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake
index d0ca00c83..f36a5bfb0 100644
--- a/contrib/cmake/cmake/msvc_legacy_quirks.cmake
+++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake
@@ -149,3 +149,13 @@ set(STACK_SIZE_MSVC_LINKER 8388608)
 # says this only matters for executables which is why this is not being
 # set for CMAKE_SHARED_LINKER_FLAGS or CMAKE_STATIC_LINKER_FLAGS.
 string(APPEND CMAKE_EXE_LINKER_FLAGS " /STACK:${STACK_SIZE_MSVC_LINKER}")
+
+# The original build system passes `/SUBSYSTEM:<X>` to the linker where `<X>`
+# depends on what is being linked. Where `<X>` is `CONSOLE` for executables
+# and `WINDOWS` for shard libraries.
+# We don't need to pass `/SUBSYSTEM:CONSOLE` because CMake will do this for
+# us when building executables because we don't pass the `WIN32` argument to
+# `add_executable()`.
+# FIXME: We probably don't need this. https://msdn.microsoft.com/en-us/library/fcc1zstk.aspx
+# suggests that `/SUBSYSTEM:` only matters for executables.
+string(APPEND CMAKE_SHARED_LINKER_FLAGS " /SUBSYSTEM:WINDOWS")

From 2a919cf16e7d6807a76fa2806d37486c7e7e04e5 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 29 Apr 2017 15:02:01 +0100
Subject: [PATCH 11/12] [CMake] Duplicate the remaining linker flags from the
 old build system.

---
 contrib/cmake/cmake/msvc_legacy_quirks.cmake | 33 ++++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake
index f36a5bfb0..2ca20277c 100644
--- a/contrib/cmake/cmake/msvc_legacy_quirks.cmake
+++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake
@@ -159,3 +159,36 @@ string(APPEND CMAKE_EXE_LINKER_FLAGS " /STACK:${STACK_SIZE_MSVC_LINKER}")
 # FIXME: We probably don't need this. https://msdn.microsoft.com/en-us/library/fcc1zstk.aspx
 # suggests that `/SUBSYSTEM:` only matters for executables.
 string(APPEND CMAKE_SHARED_LINKER_FLAGS " /SUBSYSTEM:WINDOWS")
+
+# FIXME: The following linker flags are weird. They are set in all configurations
+# in the old build system except release x86_64. We try to emulate this here but
+# this is likely the wrong thing to do.
+foreach (_build_type ${_build_types_as_upper})
+  if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64" AND
+      ("${_build_type}" STREQUAL "RELEASE" OR
+      "${_build_type}"  STREQUAL "RELWITHDEBINFO")
+      )
+    message(AUTHOR_WARNING "Skipping legacy linker MSVC options for x86_64 ${_build_type}")
+  else()
+    # Linker optimizations.
+    # See https://msdn.microsoft.com/en-us/library/bxwfs976.aspx
+    string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /OPT:REF /OPT:ICF")
+    string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /OPT:REF /OPT:ICF")
+
+    # FIXME: This is not necessary. This is MSVC's default.
+    # See https://msdn.microsoft.com/en-us/library/b1kw34cb.aspx
+    string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /TLBID:1")
+    string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /TLBID:1")
+
+    # FIXME: This is not necessary. This is MSVC's default.
+    # Address space layout randomization
+    # See https://msdn.microsoft.com/en-us/library/bb384887.aspx
+    string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /DYNAMICBASE")
+    string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /DYNAMICBASE:NO")
+
+    # FIXME: This is not necessary. This is MSVC's default.
+    # Indicate that the executable is compatible with DEP
+    # See https://msdn.microsoft.com/en-us/library/ms235442.aspx
+    string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /NXCOMPAT")
+  endif()
+endforeach()

From 6e07d6dd2d11c7c779640f7cdb9c234875454e88 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 29 Apr 2017 17:45:02 +0100
Subject: [PATCH 12/12] [CMake] Override CMake's default flags for GCC/Clang as
 we were doing before 4cc2b292c0cc8759da7a525e63dbfefdb06d6a01.

It's useful to be able to control the defaults and CMake's internal
logic for GCC/Clang is simple enough that doing this makes sense.

It would be nice to do the same for MSVC but CMake's internal
logic is more complicated so for now it's better that we just use
CMake's default.
---
 CMakeLists.txt                                     |  1 +
 .../cmake/cmake/cxx_compiler_flags_overrides.cmake | 14 ++++++++++++++
 2 files changed, 15 insertions(+)
 create mode 100644 contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake

diff --git a/CMakeLists.txt b/CMakeLists.txt
index aa347ae66..19c56a413 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -24,6 +24,7 @@ if (NOT (EXISTS "${CMAKE_SOURCE_DIR}/src/CMakeLists.txt"))
           "``python contrib/cmake/bootstrap.py create``")
 endif()
 
+set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
 project(Z3 CXX)
 
 ################################################################################
diff --git a/contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake b/contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake
new file mode 100644
index 000000000..59966f424
--- /dev/null
+++ b/contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake
@@ -0,0 +1,14 @@
+# This file overrides the default compiler flags for CMake's built-in
+# configurations (CMAKE_BUILD_TYPE). Most compiler flags should not be set here.
+# The main purpose is to have very fine grained control of the compiler flags.
+
+# We only override the defaults for Clang and GCC right now.
+# CMake's MSVC logic is complicated so for now it's better to just inherit CMake's defaults.
+if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
+  # Taken from Modules/Compiler/GNU.cmake
+  set(CMAKE_CXX_FLAGS_INIT "")
+  set(CMAKE_CXX_FLAGS_DEBUG_INIT "-g -O0")
+  set(CMAKE_CXX_FLAGS_MINSIZEREL_INIT "-Os -DNDEBUG")
+  set(CMAKE_CXX_FLAGS_RELEASE_INIT "-O3 -DNDEBUG")
+  set(CMAKE_CXX_FLAGS_RELWITHDEBINFO_INIT "-O2 -g -DNDEBUG")
+endif()