mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
Nikolaj Bjorner
commit
944dfbc6ef
|
|
@ -24,9 +24,8 @@ 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)
|
||||
set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
|
||||
project(Z3 CXX)
|
||||
|
||||
################################################################################
|
||||
# Project version
|
||||
|
|
@ -155,13 +154,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}")
|
||||
|
|
@ -326,6 +325,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
|
||||
################################################################################
|
||||
|
|
@ -376,6 +384,41 @@ if (BUILD_LIBZ3_SHARED)
|
|||
endif()
|
||||
endif()
|
||||
|
||||
################################################################################
|
||||
# Link time optimization
|
||||
################################################################################
|
||||
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
|
||||
################################################################################
|
||||
# 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
|
||||
################################################################################
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
52
contrib/cmake/cmake/compiler_lto.cmake
Normal file
52
contrib/cmake/cmake/compiler_lto.cmake
Normal file
|
|
@ -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()
|
||||
|
|
@ -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()
|
||||
|
|
@ -37,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()
|
||||
|
|
|
|||
14
contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake
Normal file
14
contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake
Normal file
|
|
@ -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()
|
||||
194
contrib/cmake/cmake/msvc_legacy_quirks.cmake
Normal file
194
contrib/cmake/cmake/msvc_legacy_quirks.cmake
Normal file
|
|
@ -0,0 +1,194 @@
|
|||
# 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)
|
||||
|
||||
################################################################################
|
||||
# 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()
|
||||
|
||||
# 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}")
|
||||
|
||||
# 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")
|
||||
|
||||
# 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()
|
||||
|
|
@ -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})
|
||||
|
|
|
|||
|
|
@ -25,6 +25,7 @@ static_features::static_features(ast_manager & m):
|
|||
m_bvutil(m),
|
||||
m_arrayutil(m),
|
||||
m_fpautil(m),
|
||||
m_sequtil(m),
|
||||
m_bfid(m.get_basic_family_id()),
|
||||
m_afid(m.mk_family_id("arith")),
|
||||
m_lfid(m.mk_family_id("label")),
|
||||
|
|
@ -77,6 +78,8 @@ void static_features::reset() {
|
|||
m_has_real = false;
|
||||
m_has_bv = false;
|
||||
m_has_fpa = false;
|
||||
m_has_str = false;
|
||||
m_has_seq_non_str = false;
|
||||
m_has_arrays = false;
|
||||
m_arith_k_sum .reset();
|
||||
m_num_arith_terms = 0;
|
||||
|
|
@ -279,6 +282,11 @@ void static_features::update_core(expr * e) {
|
|||
m_has_fpa = true;
|
||||
if (!m_has_arrays && m_arrayutil.is_array(e))
|
||||
m_has_arrays = true;
|
||||
if (!m_has_str && m_sequtil.str.is_string_term(e))
|
||||
m_has_str = true;
|
||||
if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e)) {
|
||||
m_has_seq_non_str = true;
|
||||
}
|
||||
if (is_app(e)) {
|
||||
family_id fid = to_app(e)->get_family_id();
|
||||
mark_theory(fid);
|
||||
|
|
|
|||
|
|
@ -24,6 +24,7 @@ Revision History:
|
|||
#include"bv_decl_plugin.h"
|
||||
#include"array_decl_plugin.h"
|
||||
#include"fpa_decl_plugin.h"
|
||||
#include"seq_decl_plugin.h"
|
||||
#include"map.h"
|
||||
|
||||
struct static_features {
|
||||
|
|
@ -32,6 +33,7 @@ struct static_features {
|
|||
bv_util m_bvutil;
|
||||
array_util m_arrayutil;
|
||||
fpa_util m_fpautil;
|
||||
seq_util m_sequtil;
|
||||
family_id m_bfid;
|
||||
family_id m_afid;
|
||||
family_id m_lfid;
|
||||
|
|
@ -77,6 +79,8 @@ struct static_features {
|
|||
bool m_has_real; //
|
||||
bool m_has_bv; //
|
||||
bool m_has_fpa; //
|
||||
bool m_has_str; // has String-typed terms
|
||||
bool m_has_seq_non_str; // has non-String-typed Sequence terms
|
||||
bool m_has_arrays; //
|
||||
rational m_arith_k_sum; // sum of the numerals in arith atoms.
|
||||
unsigned m_num_arith_terms;
|
||||
|
|
|
|||
|
|
@ -249,6 +249,7 @@ protected:
|
|||
array_util m_arutil;
|
||||
fpa_util m_futil;
|
||||
seq_util m_sutil;
|
||||
|
||||
datalog::dl_decl_util m_dlutil;
|
||||
|
||||
format_ns::format * pp_fdecl_name(symbol const & s, func_decls const & fs, func_decl * f, unsigned & len) {
|
||||
|
|
@ -277,6 +278,7 @@ public:
|
|||
virtual array_util & get_arutil() { return m_arutil; }
|
||||
virtual fpa_util & get_futil() { return m_futil; }
|
||||
virtual seq_util & get_sutil() { return m_sutil; }
|
||||
|
||||
virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
|
||||
virtual bool uses(symbol const & s) const {
|
||||
return
|
||||
|
|
@ -527,6 +529,9 @@ bool cmd_context::logic_has_fpa() const {
|
|||
return !has_logic() || smt_logics::logic_has_fpa(m_logic);
|
||||
}
|
||||
|
||||
bool cmd_context::logic_has_str() const {
|
||||
return !has_logic() || m_logic == "QF_S";
|
||||
}
|
||||
|
||||
bool cmd_context::logic_has_array() const {
|
||||
return !has_logic() || smt_logics::logic_has_array(m_logic);
|
||||
|
|
@ -568,7 +573,6 @@ void cmd_context::init_manager_core(bool new_manager) {
|
|||
load_plugin(symbol("seq"), logic_has_seq(), fids);
|
||||
load_plugin(symbol("fpa"), logic_has_fpa(), fids);
|
||||
load_plugin(symbol("pb"), logic_has_pb(), fids);
|
||||
|
||||
svector<family_id>::iterator it = fids.begin();
|
||||
svector<family_id>::iterator end = fids.end();
|
||||
for (; it != end; ++it) {
|
||||
|
|
@ -616,7 +620,6 @@ void cmd_context::init_external_manager() {
|
|||
init_manager_core(false);
|
||||
}
|
||||
|
||||
|
||||
bool cmd_context::set_logic(symbol const & s) {
|
||||
if (has_logic())
|
||||
throw cmd_exception("the logic has already been set");
|
||||
|
|
|
|||
|
|
@ -257,6 +257,7 @@ protected:
|
|||
bool logic_has_array() const;
|
||||
bool logic_has_datatype() const;
|
||||
bool logic_has_fpa() const;
|
||||
bool logic_has_str() const;
|
||||
|
||||
void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; }
|
||||
void print_unsupported_info(symbol const& s, int line, int pos) { if (s != symbol::null) diagnostic_stream() << "; " << s << " line: " << line << " position: " << pos << std::endl;}
|
||||
|
|
|
|||
Loading…
Reference in a new issue