Setting up param tuning infrastructure in C++

BUILD.bazel

@@ -27,7 +27,7 @@ cmake(
     out_shared_libs = select({
         "@platforms//os:linux": ["libz3.so"],
         # "@platforms//os:osx": ["libz3.dylib"],    # FIXME: this is not working, libz3<version>.dylib is not copied
-        # "@platforms//os:windows": ["z3.dll"],     # TODO: test this
+        "@platforms//os:windows": ["libz3.dll"],
         "//conditions:default": ["@platforms//:incompatible"],
     }),
     visibility = ["//visibility:public"],
@@ -45,7 +45,7 @@ cmake(
     out_static_libs = select({
         "@platforms//os:linux": ["libz3.a"],
         "@platforms//os:osx": ["libz3.a"],
-        # "@platforms//os:windows": ["z3.lib"],     # TODO: test this
+        "@platforms//os:windows": ["libz3.lib"],     # MSVC with Control Flow Guard enabled by default
         "//conditions:default": ["@platforms//:incompatible"],
     }),
     visibility = ["//visibility:public"],

CMakeLists.txt

@@ -362,34 +362,75 @@ endif()
 include(${PROJECT_SOURCE_DIR}/cmake/compiler_lto.cmake)
 
 ################################################################################
-# Control flow integrity
+# Control flow integrity (Clang only)
 ################################################################################
-option(Z3_ENABLE_CFI "Enable control flow integrity checking" OFF)
+option(Z3_ENABLE_CFI "Enable Control Flow Integrity security checks" OFF)
 if (Z3_ENABLE_CFI)
-  set(build_types_with_cfi "RELEASE" "RELWITHDEBINFO")
+  if (NOT CMAKE_CXX_COMPILER_ID MATCHES "Clang")
+    message(FATAL_ERROR "Z3_ENABLE_CFI is only supported with Clang compiler. "
+      "Current compiler: ${CMAKE_CXX_COMPILER_ID}. "
+      "You should set Z3_ENABLE_CFI to OFF or use Clang to compile.")
+  endif()
+
   if (NOT Z3_LINK_TIME_OPTIMIZATION)
-    message(FATAL_ERROR "Cannot enable control flow integrity checking without link-time optimization."
+    message(FATAL_ERROR "Cannot enable Control Flow Integrity without link-time optimization. "
       "You should set Z3_LINK_TIME_OPTIMIZATION to ON or Z3_ENABLE_CFI to OFF.")
   endif()
+
+  set(build_types_with_cfi "RELEASE" "RELWITHDEBINFO")
   if (DEFINED CMAKE_CONFIGURATION_TYPES)
     # Multi configuration generator
     message(STATUS "Note CFI is only enabled for the following configurations: ${build_types_with_cfi}")
     # No need for else because this is the same as the set that LTO requires.
   endif()
-  if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
-    z3_add_cxx_flag("-fsanitize=cfi" REQUIRED)
-    z3_add_cxx_flag("-fsanitize-cfi-cross-dso" REQUIRED)
-  elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
-    z3_add_cxx_flag("/guard:cf" REQUIRED)
-    message(STATUS "Enabling CFI for MSVC")
-    foreach (_build_type ${build_types_with_cfi})
-      message(STATUS "Enabling CFI for MSVC")
-      string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /GUARD:CF")
-      string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /GUARD:CF")
-    endforeach()
+
+  message(STATUS "Enabling Control Flow Integrity (CFI) for Clang")
+  z3_add_cxx_flag("-fsanitize=cfi" REQUIRED)
+  z3_add_cxx_flag("-fsanitize-cfi-cross-dso" REQUIRED)
+endif()
+# End CFI section
+
+################################################################################
+# Control Flow Guard (MSVC only)
+################################################################################
+# Default CFG to ON for MSVC, OFF for other compilers.
+if (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
+  option(Z3_ENABLE_CFG "Enable Control Flow Guard security checks" ON)
+else()
+  option(Z3_ENABLE_CFG "Enable Control Flow Guard security checks" OFF)
+endif()
+
+if (Z3_ENABLE_CFG)
+  if (NOT CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
+    message(FATAL_ERROR "Z3_ENABLE_CFG is only supported with MSVC compiler. "
+      "Current compiler: ${CMAKE_CXX_COMPILER_ID}. "
+      "You should remove Z3_ENABLE_CFG or set it to OFF or use MSVC to compile.")
+  endif()
+
+  # Check for incompatible options (handle both / and - forms for robustness)
+  string(REGEX MATCH "[-/]ZI" _has_ZI "${CMAKE_CXX_FLAGS} ${CMAKE_CXX_FLAGS_DEBUG} ${CMAKE_CXX_FLAGS_RELEASE} ${CMAKE_CXX_FLAGS_RELWITHDEBINFO} ${CMAKE_CXX_FLAGS_MINSIZEREL}")
+  string(REGEX MATCH "[-/]clr" _has_clr "${CMAKE_CXX_FLAGS} ${CMAKE_CXX_FLAGS_DEBUG} ${CMAKE_CXX_FLAGS_RELEASE} ${CMAKE_CXX_FLAGS_RELWITHDEBINFO} ${CMAKE_CXX_FLAGS_MINSIZEREL}")
+
+  if(_has_ZI)
+    message(WARNING "/guard:cf is incompatible with /ZI (Edit and Continue debug information). "
+                   "Control Flow Guard will be disabled due to /ZI option.")
+  elseif(_has_clr)
+    message(WARNING "/guard:cf is incompatible with /clr (Common Language Runtime compilation). "
+                   "Control Flow Guard will be disabled due to /clr option.")
   else()
-    message(FATAL_ERROR "Can't enable control flow integrity for compiler \"${CMAKE_CXX_COMPILER_ID}\"."
-      "You should set Z3_ENABLE_CFI to OFF or use Clang or MSVC to compile.")
+    # Enable Control Flow Guard if no incompatible options are present
+    message(STATUS "Enabling Control Flow Guard (/guard:cf) and ASLR (/DYNAMICBASE) for MSVC")
+    z3_add_cxx_flag("/guard:cf" REQUIRED)
+    string(APPEND CMAKE_EXE_LINKER_FLAGS " /GUARD:CF /DYNAMICBASE")
+    string(APPEND CMAKE_SHARED_LINKER_FLAGS " /GUARD:CF /DYNAMICBASE")
+  endif()
+else()
+  if (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
+    # Explicitly disable Control Flow Guard when Z3_ENABLE_CFG is OFF
+    message(STATUS "Disabling Control Flow Guard (/guard:cf-) for MSVC")
+    z3_add_cxx_flag("/guard:cf-" REQUIRED)
+    string(APPEND CMAKE_EXE_LINKER_FLAGS " /GUARD:NO")
+    string(APPEND CMAKE_SHARED_LINKER_FLAGS " /GUARD:NO")
   endif()
 endif()
 

README-CMake.md

@@ -365,6 +365,35 @@ build type when invoking ``cmake`` by passing ``-DCMAKE_BUILD_TYPE=<build_type>`
 For multi-configuration generators (e.g. Visual Studio) you don't set the build type
 when invoking CMake and instead set the build type within Visual Studio itself.
 
+## MSVC Security Features
+
+When building with Microsoft Visual C++ (MSVC), Z3 automatically enables several security features by default:
+
+### Control Flow Guard (CFG)
+- **CMake Option**: `Z3_ENABLE_CFG` - Defaults to `ON` for MSVC builds
+- **Compiler flag**: `/guard:cf` - Automatically enabled when `Z3_ENABLE_CFG=ON`
+- **Linker flag**: `/GUARD:CF` - Automatically enabled when `Z3_ENABLE_CFG=ON`
+- **Purpose**: Control Flow Guard analyzes control flow for indirect call targets at compile time and inserts runtime verification code to detect attempts to compromise your code by redirecting control flow to attacker-controlled locations
+- **Note**: Automatically enables `/DYNAMICBASE` as required by `/GUARD:CF`
+
+### Address Space Layout Randomization (ASLR)
+- **Linker flag**: `/DYNAMICBASE` - Enabled when Control Flow Guard is active
+- **Purpose**: Randomizes memory layout to make exploitation more difficult
+- **Note**: Required for Control Flow Guard to function properly
+
+### Incompatibilities
+Control Flow Guard is incompatible with:
+- `/ZI` (Edit and Continue debug information format)
+- `/clr` (Common Language Runtime compilation)
+
+When these incompatible options are detected, Control Flow Guard will be automatically disabled with a warning message.
+
+### Disabling Control Flow Guard
+To disable Control Flow Guard, set the CMake option:
+```bash
+cmake -DZ3_ENABLE_CFG=OFF ../
+```
+
 ## Useful options
 
 The following useful options can be passed to CMake whilst configuring.
@@ -404,8 +433,11 @@ The following useful options can be passed to CMake whilst configuring.
 * ``Z3_ALWAYS_BUILD_DOCS`` - BOOL. If set to ``TRUE`` and ``Z3_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.
 * ``Z3_LINK_TIME_OPTIMIZATION`` - BOOL. If set to ``TRUE`` link time optimization will be enabled.
-* ``Z3_ENABLE_CFI`` - BOOL. If set to ``TRUE`` will enable Control Flow Integrity security checks. This is only supported by MSVC and Clang and will
+* ``Z3_ENABLE_CFI`` - BOOL. If set to ``TRUE`` will enable Control Flow Integrity security checks. This is only supported by Clang and will
     fail on other compilers. This requires Z3_LINK_TIME_OPTIMIZATION to also be enabled.
+* ``Z3_ENABLE_CFG`` - BOOL. If set to ``TRUE`` will enable Control Flow Guard security checks. This is only supported by MSVC and will
+    fail on other compilers. This does not require link time optimization. Control Flow Guard is enabled by default for MSVC builds.
+    Note: Control Flow Guard is incompatible with ``/ZI`` (Edit and Continue debug information) and ``/clr`` (Common Language Runtime compilation).
 * ``Z3_API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature.
 * ``WARNINGS_AS_ERRORS`` - STRING. If set to ``ON`` compiler warnings will be treated as errors. If set to ``OFF`` compiler warnings will not be treated as errors.
     If set to ``SERIOUS_ONLY`` a subset of compiler warnings will be treated as errors.

README.md

@@ -49,7 +49,12 @@ cd build
 nmake
 ```
 
-Z3 uses C++20. The recommended version of Visual Studio is therefore VS2019 or later. 
+Z3 uses C++20. The recommended version of Visual Studio is therefore VS2019 or later.
+
+**Security Features (MSVC)**: When building with Visual Studio/MSVC, a couple of security features are enabled by default for Z3:
+- Control Flow Guard (`/guard:cf`) - enabled by default to detect attempts to compromise your code by preventing calls to locations other than function entry points, making it more difficult for attackers to execute arbitrary code through control flow redirection
+- Address Space Layout Randomization (`/DYNAMICBASE`) - enabled by default for memory layout randomization, required by the `/GUARD:CF` linker option
+- These can be disabled using `python scripts/mk_make.py --no-guardcf` (Python build) or `cmake -DZ3_ENABLE_CFG=OFF` (CMake build) if needed
 
 ## Building Z3 using make and GCC/Clang
 

scripts/mk_util.py

@@ -645,6 +645,9 @@ def check_eol():
     IS_WINDOWS=True
     # Visual Studio already displays the files being compiled
     SHOW_CPPS=False
+    # Enable Control Flow Guard by default on Windows with MSVC
+    # Note: Python build system on Windows assumes MSVC (cl.exe) compiler
+    GUARD_CF = True
 elif os.name == 'posix':
     if os.uname()[0] == 'Darwin':
         IS_OSX=True
@@ -695,6 +698,8 @@ def display_help(exit_code):
     print("  -t, --trace                   enable tracing in release mode.")
     if IS_WINDOWS:
         print("  --guardcf                     enable Control Flow Guard runtime checks.")
+        print("                                (incompatible with /ZI, -ZI, /clr, and -clr options)")
+        print("  --no-guardcf                  disable Control Flow Guard runtime checks.")
         print("  -x, --x64                     create 64 binary when using Visual Studio.")
     else:
         print("  --x86                         force 32-bit x86 build on x64 systems.")
@@ -746,7 +751,7 @@ def parse_options():
     try:
         options, remainder = getopt.gnu_getopt(sys.argv[1:],
                                                'b:df:sxa:hmcvtnp:gj',
-                                               ['build=', 'debug', 'silent', 'x64', 'arm64=', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf',
+                                               ['build=', 'debug', 'silent', 'x64', 'arm64=', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf', 'no-guardcf',
                                                 'trace', 'dotnet', 'dotnet-key=', 'assembly-version=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js',
                                                 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'pypkgdir=', 'python', 'staticbin', 'log-sync', 'single-threaded'])
     except:
@@ -821,11 +826,42 @@ def parse_options():
             PYTHON_INSTALL_ENABLED = True
         elif opt == '--guardcf':
             GUARD_CF = True
-            ALWAYS_DYNAMIC_BASE = True # /GUARD:CF requires /DYNAMICBASE
+        elif opt == '--no-guardcf':
+            GUARD_CF = False
+            # Note: ALWAYS_DYNAMIC_BASE can remain True if set elsewhere
         else:
             print("ERROR: Invalid command line option '%s'" % opt)
             display_help(1)
 
+    # Ensure ALWAYS_DYNAMIC_BASE is True whenever GUARD_CF is enabled
+    # This is required because /GUARD:CF linker option requires /DYNAMICBASE
+    if GUARD_CF:
+        ALWAYS_DYNAMIC_BASE = True
+
+def validate_guard_cf_compatibility(final_cxxflags):
+    """Validate that Control Flow Guard is compatible with the final compiler options.
+
+    Args:
+        final_cxxflags: The complete CXXFLAGS string that will be used for compilation
+    """
+    global GUARD_CF
+
+    if not GUARD_CF or not IS_WINDOWS:
+        return
+
+    # Check the final compiler flags for incompatible options
+    zi_pattern = re.compile(r'[/-]ZI\b')
+    if zi_pattern.search(final_cxxflags):
+        raise MKException("Control Flow Guard (/guard:cf) is incompatible with Edit and Continue debug information (/ZI or -ZI). Disable Control Flow Guard with --no-guardcf.")
+
+    clr_pattern = re.compile(r'[/-]clr(?::|$|\s)')
+    if clr_pattern.search(final_cxxflags):
+        raise MKException("Control Flow Guard (/guard:cf) is incompatible with Common Language Runtime compilation (/clr or -clr). Disable Control Flow Guard with --no-guardcf when using managed code.")
+
+    # Note: /Zi or -Zi (Program Database debug info) is compatible with /guard:cf
+    if is_verbose() and GUARD_CF:
+        print("Control Flow Guard enabled and compatible with current compiler options.")
+
 
 # Return a list containing a file names included using '#include' in
 # the given C/C++ file named fname.
@@ -2503,6 +2539,8 @@ def mk_config():
     config = open(os.path.join(BUILD_DIR, 'config.mk'), 'w')
     global CXX, CC, GMP, GUARD_CF, STATIC_BIN, GIT_HASH, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC, SINGLE_THREADED, IS_ARCH_ARM64
     if IS_WINDOWS:
+        # On Windows, Python build system assumes MSVC (cl.exe) compiler
+        # GUARD_CF is only supported with MSVC, which is the default on Windows
         CXXFLAGS = '/nologo /Zi /D WIN32 /D _WINDOWS /EHsc /GS /Gd /std:c++20 -D_DISABLE_CONSTEXPR_MUTEX_CONSTRUCTOR'
         config.write(
             'CC=cl\n'
@@ -2531,6 +2569,10 @@ def mk_config():
         if GUARD_CF:
             extra_opt = ' %s /guard:cf' % extra_opt
             link_extra_opt = ' %s /GUARD:CF' % link_extra_opt
+        else:
+            # Explicitly disable Control Flow Guard when GUARD_CF is False
+            extra_opt = ' %s /guard:cf-' % extra_opt
+            link_extra_opt = ' %s /GUARD:NO' % link_extra_opt
         if STATIC_BIN:
             static_opt = '/MT'
         else:
@@ -2543,17 +2585,21 @@ def mk_config():
                 'LINK_FLAGS=/nologo %s\n'
                 'SLINK_FLAGS=/nologo /LDd\n' % static_opt)
             if VS_X64:
+                final_cxxflags = '/c %s /Zi /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 %s %s' % (CXXFLAGS, extra_opt, static_opt)
+                validate_guard_cf_compatibility(final_cxxflags)
                 config.write(
-                    'CXXFLAGS=/c %s /Zi /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 %s %s\n' % (CXXFLAGS, extra_opt, static_opt))
+                    'CXXFLAGS=%s\n' % final_cxxflags)
                 config.write(
                     'LINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
                     'SLINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
             elif VS_ARM:
                 print("ARM on VS is unsupported")
                 exit(1)
             else:
+                final_cxxflags = '/c %s /Zi /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 /arch:SSE2 %s %s' % (CXXFLAGS, extra_opt, static_opt)
+                validate_guard_cf_compatibility(final_cxxflags)
                 config.write(
-                    'CXXFLAGS=/c %s /Zi /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 /arch:SSE2 %s %s\n' % (CXXFLAGS, extra_opt, static_opt))
+                    'CXXFLAGS=%s\n' % final_cxxflags)
                 config.write(
                     'LINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
                     'SLINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
@@ -2568,17 +2614,21 @@ def mk_config():
             if TRACE:
                 extra_opt = '%s /D _TRACE ' % extra_opt
             if VS_X64:
+                final_cxxflags = '/c%s %s /Zi /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D NDEBUG /D _LIB /D UNICODE /Gm- /GF /Gy /TP %s %s' % (GL, CXXFLAGS, extra_opt, static_opt)
+                validate_guard_cf_compatibility(final_cxxflags)
                 config.write(
-                    'CXXFLAGS=/c%s %s /Zi /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D NDEBUG /D _LIB /D UNICODE /Gm- /GF /Gy /TP %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt))
+                    'CXXFLAGS=%s\n' % final_cxxflags)
                 config.write(
                     'LINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /profile /MACHINE:X64 /SUBSYSTEM:CONSOLE /STACK:8388608 %s\n'
                     'SLINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /profile /MACHINE:X64 /SUBSYSTEM:WINDOWS /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt))
             elif VS_ARM:
                 print("ARM on VS is unsupported")
                 exit(1)
             else:
+                final_cxxflags = '/c%s %s /Zi /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D NDEBUG /D _CONSOLE /D ASYNC_COMMANDS /Gm- /arch:SSE2 %s %s' % (GL, CXXFLAGS, extra_opt, static_opt)
+                validate_guard_cf_compatibility(final_cxxflags)
                 config.write(
-                    'CXXFLAGS=/c%s %s /Zi /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D NDEBUG /D _CONSOLE /D ASYNC_COMMANDS /Gm- /arch:SSE2 %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt))
+                    'CXXFLAGS=%s\n' % final_cxxflags)
                 config.write(
                     'LINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
                     'SLINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (LTCG, link_extra_opt, LTCG, maybe_disable_dynamic_base, link_extra_opt))

src/math/lp/nla_grobner.cpp

@@ -47,9 +47,22 @@ namespace nla {
         if (m_quota == 0)
             m_quota = c().params().arith_nl_gr_q();                    
 
+        bool const use_exp_delay = c().params().arith_nl_grobner_exp_delay();
+
         if (m_quota == 1) {
-            m_delay_base++;
-            m_delay = m_delay_base;
+            if (use_exp_delay) {
+                constexpr unsigned delay_cap = 1000000;
+                if (m_delay_base == 0)
+                    m_delay_base = 1;
+                else if (m_delay_base < delay_cap) {
+                    m_delay_base *= 2;
+                    if (m_delay_base > delay_cap)
+                        m_delay_base = delay_cap;
+                }
+                m_delay = m_delay_base;
+            }
+            else
+                m_delay = ++m_delay_base;
             m_quota = c().params().arith_nl_gr_q();
         }