diff --git a/BUILD.bazel b/BUILD.bazel index 7fde74caa..f4d69a747 100644 --- a/BUILD.bazel +++ b/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.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"], diff --git a/CMakeLists.txt b/CMakeLists.txt index 603e86ee1..6d66f8dc4 100644 --- a/CMakeLists.txt +++ b/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() diff --git a/README-CMake.md b/README-CMake.md index 93cf00e7b..c8fa0faae 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -365,6 +365,35 @@ build type when invoking ``cmake`` by passing ``-DCMAKE_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. diff --git a/README.md b/README.md index b99c9e6b5..21585aef6 100644 --- a/README.md +++ b/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 diff --git a/scripts/mk_util.py b/scripts/mk_util.py index c1070e62a..005c90ecb 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -645,6 +645,9 @@ if os.name == 'nt': 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,8 +2585,10 @@ 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)) @@ -2552,8 +2596,10 @@ def mk_config(): 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,8 +2614,10 @@ 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)) @@ -2577,8 +2625,10 @@ def mk_config(): 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)) diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 89396b41f..f0db19649 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/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(); } diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index ff1ae6a07..2d3b89928 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -44,6 +44,7 @@ namespace nlsat { bool m_full_dimensional; bool m_minimize_cores; bool m_factor; + bool m_add_all_coeffs; bool m_signed_project; bool m_cell_sample; @@ -154,6 +155,7 @@ namespace nlsat { m_simplify_cores = false; m_full_dimensional = false; m_minimize_cores = false; + m_add_all_coeffs = true; m_signed_project = false; } @@ -622,6 +624,8 @@ namespace nlsat { //"An improved projection operation for cylindrical algebraic decomposition of three-dimensional space", by McCallum, Scott bool is_square_free(polynomial_ref_vector &ps, var x) { + if (m_add_all_coeffs) + return false; polynomial_ref p(m_pm); polynomial_ref lc_poly(m_pm); polynomial_ref disc_poly(m_pm); @@ -2135,6 +2139,10 @@ namespace nlsat { m_imp->m_factor = f; } + void explain::set_add_all_coeffs(bool f) { + m_imp->m_add_all_coeffs = f; + } + void explain::set_signed_project(bool f) { m_imp->m_signed_project = f; } @@ -2185,4 +2193,3 @@ void pp_lit(nlsat::explain::imp & ex, nlsat::literal l) { std::cout << std::endl; } #endif - diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h index 6e1cf091b..2c3adfcb2 100644 --- a/src/nlsat/nlsat_explain.h +++ b/src/nlsat/nlsat_explain.h @@ -44,6 +44,7 @@ namespace nlsat { void set_full_dimensional(bool f); void set_minimize_cores(bool f); void set_factor(bool f); + void set_add_all_coeffs(bool f); void set_signed_project(bool f); /** @@ -109,4 +110,3 @@ namespace nlsat { }; }; - diff --git a/src/nlsat/nlsat_params.pyg b/src/nlsat/nlsat_params.pyg index 6a0f50cd3..b035f4189 100644 --- a/src/nlsat/nlsat_params.pyg +++ b/src/nlsat/nlsat_params.pyg @@ -19,5 +19,6 @@ def_module_params('nlsat', ('inline_vars', BOOL, False, "inline variables that can be isolated from equations (not supported in incremental mode)"), ('seed', UINT, 0, "random seed."), ('factor', BOOL, True, "factor polynomials produced during conflict resolution."), + ('add_all_coeffs', BOOL, False, "add all polynomial coefficients during projection."), ('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only") )) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 5bc0d214f..bad981011 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -306,6 +306,7 @@ namespace nlsat { m_explain.set_simplify_cores(m_simplify_cores); m_explain.set_minimize_cores(min_cores); m_explain.set_factor(p.factor()); + m_explain.set_add_all_coeffs(p.add_all_coeffs()); m_am.updt_params(p.p); } diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 487772c81..451a07964 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -80,6 +80,7 @@ def_module_params(module_name='smt', ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'), ('arith.nl.grobner_propagate_quotients', BOOL, True, 'detect conflicts x*y + z = 0 where x doesn\'t divide z'), ('arith.nl.grobner_gcd_test', BOOL, True, 'detect gcd conflicts for polynomial powers x^k - y = 0'), + ('arith.nl.grobner_exp_delay', BOOL, True, 'use exponential delay between grobner basis attempts'), ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'), ('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.nl.grobner_expand_terms', BOOL, True, 'expand terms before computing grobner basis'), @@ -138,4 +139,3 @@ def_module_params(module_name='smt', ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy'), ('qsat_use_qel', BOOL, True, 'Use QEL for lite quantifier elimination and model-based projection in QSAT') )) - diff --git a/src/params/theory_arith_params.cpp b/src/params/theory_arith_params.cpp index 27a8949b0..39e520287 100644 --- a/src/params/theory_arith_params.cpp +++ b/src/params/theory_arith_params.cpp @@ -22,6 +22,11 @@ Revision History: void theory_arith_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); + m_nl_arith_delay = p.arith_nl_delay(); + m_nl_arith_expensive_patching = p.arith_nl_expensive_patching(); + m_nl_arith_horner = p.arith_nl_horner(); + m_nl_arith_horner_frequency = p.arith_nl_horner_frequency(); + m_nl_arith_tangents = p.arith_nl_tangents(); m_arith_random_initial_value = p.arith_random_initial_value(); m_arith_random_seed = p.random_seed(); m_arith_mode = static_cast(p.arith_solver()); @@ -102,4 +107,9 @@ void theory_arith_params::display(std::ostream & out) const { DISPLAY_PARAM(m_arith_validate); DISPLAY_PARAM(m_arith_dump_lemmas); DISPLAY_PARAM(m_arith_epsilon); + DISPLAY_PARAM(m_nl_arith_delay); + DISPLAY_PARAM(m_nl_arith_expensive_patching); + DISPLAY_PARAM(m_nl_arith_horner); + DISPLAY_PARAM(m_nl_arith_horner_frequency); + DISPLAY_PARAM(m_nl_arith_tangents); } diff --git a/src/params/theory_arith_params.h b/src/params/theory_arith_params.h index 8329ae1fd..9b2b60b95 100644 --- a/src/params/theory_arith_params.h +++ b/src/params/theory_arith_params.h @@ -112,6 +112,11 @@ struct theory_arith_params { bool m_nl_arith_propagate_linear_monomials = true; bool m_nl_arith_optimize_bounds = true; bool m_nl_arith_cross_nested = true; + unsigned m_nl_arith_delay = 10; + bool m_nl_arith_expensive_patching = false; + bool m_nl_arith_horner = true; + unsigned m_nl_arith_horner_frequency = 4; + bool m_nl_arith_tangents = true; theory_arith_params(params_ref const & p = params_ref()) { updt_params(p); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 7d68dc808..198c099a0 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -137,6 +137,7 @@ namespace smt { scoped_ptr m_fmls; svector m_lit_scores[2]; + vector m_recorded_clauses; // ----------------------------------- @@ -1301,6 +1302,8 @@ namespace smt { void add_scores(unsigned n, literal const *lits); + void record_clause(unsigned n, literal const * lits); + // ----------------------------------- // diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 7f0fe1e9e..be884fd18 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -965,17 +965,24 @@ namespace smt { return v; } + // following the pattern of solver::persist_clause in src/sat/smt/user_solver.cpp + void context::record_clause(unsigned num_lits, literal const *lits) { + literal_vector clause; + clause.append(num_lits, lits); + m_recorded_clauses.push_back(clause); + } + void context::add_scores(unsigned n, literal const *lits) { for (unsigned i = 0; i < n; ++i) { auto lit = lits[i]; - unsigned v = lit.var(); // unique key per literal - m_lit_scores[lit.sign()][v] += 1.0 / n; + unsigned v = lit.var(); // uniq0 / n; } } void context::undo_mk_bool_var() { - SASSERT(!m_b_internalized_stack.empty()); + SASSERT(!m_b_internalized_stack.empty(ue key per literal + m_lit_scores[lit.sign()][v] += 1.)); m_stats.m_num_del_bool_var++; expr * n = m_b_internalized_stack.back(); unsigned n_id = n->get_id(); @@ -1433,6 +1440,7 @@ namespace smt { case CLS_LEARNED: dump_lemma(num_lits, lits); add_scores(num_lits, lits); + record_clause(num_lits, lits); break; default: break; diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index b711394d9..4f4ce1db2 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -64,6 +64,122 @@ namespace smt { namespace smt { + lbool parallel::param_generator::run_prefix_step() { + IF_VERBOSE(1, verbose_stream() << " Param generator running prefix step\n"); + ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts; + lbool r = l_undef; + try { + r = ctx->check(); + } catch (z3_error &err) { + b.set_exception(err.error_code()); + } catch (z3_exception &ex) { + b.set_exception(ex.what()); + } catch (...) { + b.set_exception("unknown exception"); + } + return r; + } + + unsigned parallel::param_generator::replay_proof_prefixes(vector candidate_param_states, unsigned max_conflicts_epsilon=200) { + unsigned conflict_budget = m_max_prefix_conflicts + max_conflicts_epsilon; + unsigned best_param_state_idx; + double best_score; + + for (unsigned i = 0; i < m_param_probe_contexts.size(); ++i) { + IF_VERBOSE(1, verbose_stream() << " PARAM TUNER: replaying proof prefix in param probe context " << i << "\n"); + context *probe_ctx = m_param_probe_contexts[i]; + probe_ctx->get_fparams().m_max_conflicts = conflict_budget; + double score = 0.0; + + // apply the ith param state to probe_ctx + smt_params params = candidate_param_states[i]; + params_ref p; + params.updt_params(p); + probe_ctx->updt_params(p); + + for (auto const& clause : probe_ctx->m_recorded_clauses) { + expr_ref_vector negated_lits(probe_ctx->m); + for (literal lit : clause) { + expr* e = probe_ctx->bool_var2expr(lit.var()); + if (!e) continue; // skip if var not yet mapped + if (!lit.sign()) + e = probe_ctx->m.mk_not(e); // since bool_var2expr discards sign + negated_lits.push_back(e); + } + + // Replay the negated clause + lbool r = probe_ctx->check(negated_lits.size(), negated_lits.data()); + + ::statistics st; + probe_ctx->collect_statistics(st); + unsigned conflicts = 0, decisions = 0, rlimit = 0; + + // I can't figure out how to access the statistics fields, I only see an update method + // st.get_uint("conflicts", conflicts); + // st.get_uint("decisions", decisions); + // st.get_uint("rlimit count", rlimit); + score += conflicts + decisions + rlimit; + } + + if (i == 0 || score < best_score) { + best_score = score; + best_param_state_idx = i; + } + } + + return best_param_state_idx; + } + + void parallel::param_generator::protocol_iteration() { + IF_VERBOSE(1, verbose_stream() << " PARAM TUNER running protocol iteration\n"); + ctx->get_fparams().m_max_conflicts = m_max_prefix_conflicts; + + // copy current param state to all param probe contexts, before running the next prefix step + // this ensures that each param probe context replays the prefix from the same configuration + for (unsigned i = 0; i < m_param_probe_contexts.size(); ++i) { + context::copy(*ctx, *m_param_probe_contexts[i], true); + } + + lbool r = run_prefix_step(); + + switch (r) { + case l_undef: { + smt_params best_param_state = m_param_state; + vector candidate_param_states; + + candidate_param_states.push_back(best_param_state); // first candidate param state is current best + while (candidate_param_states.size() <= N) { + candidate_param_states.push_back(mutate_param_state()); + } + + unsigned best_param_state_idx = replay_proof_prefixes(candidate_param_states); + + if (best_param_state_idx != 0) { + m_param_state = candidate_param_states[best_param_state_idx]; + b.set_param_state(m_param_state); + IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found better param state at index " << best_param_state_idx << "\n"); + } else { + IF_VERBOSE(1, verbose_stream() << " PARAM TUNER retained current param state\n"); + } + } + case l_true: { + IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found formula sat\n"); + model_ref mdl; + ctx->get_model(mdl); + b.set_sat(m_l2g, *mdl); + return; + } + case l_false: { + expr_ref_vector const &unsat_core = ctx->unsat_core(); + IF_VERBOSE(2, verbose_stream() << " unsat core:\n"; + for (auto c : unsat_core) verbose_stream() << mk_bounded_pp(c, m, 3) << "\n"); + IF_VERBOSE(1, verbose_stream() << " PARAM TUNER determined formula unsat\n"); + b.set_unsat(m_l2g, unsat_core); + return; + } + } + } + void parallel::worker::run() { search_tree::node *node = nullptr; expr_ref_vector cube(m); @@ -77,6 +193,13 @@ namespace smt { check_cube_start: LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n"); + + // apply current best param state from batch manager + smt_params params = b.get_best_param_state(); + params_ref p; + params.updt_params(p); + ctx->updt_params(p); + lbool r = check_cube(cube); if (!m.inc()) { @@ -143,6 +266,21 @@ namespace smt { m_num_initial_atoms = ctx->get_num_bool_vars(); } + parallel::param_generator::param_generator(parallel& p) + : p(p), b(p.m_batch_manager), m_param_state(p.ctx.get_fparams()), m_p(p.ctx.get_params()), m_l2g(m, p.ctx.m) { + ctx = alloc(context, m, m_param_state, m_p); + context::copy(p.ctx, *ctx, true); + + for (unsigned i = 0; i < N; ++i) { + m_param_probe_contexts.push_back(alloc(context, m, m_param_state, m_p)); + } + + // don't share initial units + ctx->pop_to_base_lvl(); + init_param_state(); + IF_VERBOSE(1, verbose_stream() << "Initialized parameter generator\n"); + } + void parallel::worker::share_units() { // Collect new units learned locally by this worker and send to batch manager ctx->pop_to_base_lvl(); @@ -294,6 +432,11 @@ namespace smt { } } + smt_params parallel::batch_manager::get_best_param_state() { + std::scoped_lock lock(mux); + return m_param_state; + } + void parallel::worker::collect_shared_clauses() { expr_ref_vector new_clauses = b.return_shared_clauses(m_g2l, m_shared_clause_limit, id); // iterate over new clauses and assert them in the local context @@ -489,15 +632,19 @@ namespace smt { SASSERT(num_threads > 1); for (unsigned i = 0; i < num_threads; ++i) m_workers.push_back(alloc(worker, i, *this, asms)); - + for (auto w : m_workers) sl.push_child(&(w->limit())); + + sl.push_child(&(m_param_generator.limit())); // Launch threads - vector threads(num_threads); - for (unsigned i = 0; i < num_threads; ++i) { + vector threads(num_threads + 1); // +1 for parameter generator + for (unsigned i = 0; i < num_threads - 1; ++i) { threads[i] = std::thread([&, i]() { m_workers[i]->run(); }); } + // the final thread runs the parameter generator + threads[num_threads - 1] = std::thread([&]() { m_param_generator.protocol_iteration(); }); // Wait for all threads to finish for (auto &th : threads) diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index f3fa7371b..f0a438a47 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -20,12 +20,30 @@ Revision History: #include "smt/smt_context.h" #include "util/search_tree.h" +// #include "util/util.h" #include #include namespace smt { + inline bool operator==(const smt_params& a, const smt_params& b) { + return a.m_nl_arith_branching == b.m_nl_arith_branching && + a.m_nl_arith_cross_nested == b.m_nl_arith_cross_nested && + a.m_nl_arith_delay == b.m_nl_arith_delay && + a.m_nl_arith_expensive_patching == b.m_nl_arith_expensive_patching && + a.m_nl_arith_gb == b.m_nl_arith_gb && + a.m_nl_arith_horner == b.m_nl_arith_horner && + a.m_nl_arith_horner_frequency == b.m_nl_arith_horner_frequency && + a.m_nl_arith_optimize_bounds == b.m_nl_arith_optimize_bounds && + a.m_nl_arith_propagate_linear_monomials == b.m_nl_arith_propagate_linear_monomials && + a.m_nl_arith_tangents == b.m_nl_arith_tangents; + } + + inline bool operator!=(const smt_params& a, const smt_params& b) { + return !(a == b); + } + struct cube_config { using literal = expr_ref; static bool literal_is_null(expr_ref const& l) { return l == nullptr; } @@ -62,6 +80,7 @@ namespace smt { std::mutex mux; state m_state = state::is_running; stats m_stats; + smt_params m_param_state; using node = search_tree::node; search_tree::tree m_search_tree; @@ -77,8 +96,6 @@ namespace smt { w->cancel(); } - void init_parameters_state(); - public: batch_manager(ast_manager& m, parallel& p) : m(m), p(p), m_search_tree(expr_ref(m)) { } @@ -88,8 +105,10 @@ namespace smt { void set_sat(ast_translation& l2g, model& m); void set_exception(std::string const& msg); void set_exception(unsigned error_code); + void set_param_state(smt_params const& p) { m_param_state = p; } void collect_statistics(::statistics& st) const; - + + smt_params get_best_param_state(); bool get_cube(ast_translation& g2l, unsigned id, expr_ref_vector& cube, node*& n); void backtrack(ast_translation& l2g, expr_ref_vector const& core, node* n); void split(ast_translation& l2g, unsigned id, node* n, expr* atom); @@ -107,11 +126,75 @@ namespace smt { // 3. pick winner configuration if any are better than current. // 4. update current configuration with the winner - class parameter_generator_thread { - unsigned N; // number of prefix permutation testers - scoped_ptr prefix_solver; - scoped_ptr_vector testers; // N testers + class param_generator { + parallel& p; + batch_manager& b; + ast_manager m; + scoped_ptr ctx; + ast_translation m_l2g; + + unsigned N = 4; // number of prefix permutations to test (including current) + unsigned m_max_prefix_conflicts = 1000; + + scoped_ptr m_prefix_solver; + scoped_ptr_vector m_param_probe_contexts; + smt_params m_param_state; + params_ref m_p; + + private: + void init_param_state() { + m_param_state.m_nl_arith_branching = true; + m_param_state.m_nl_arith_cross_nested = true; + m_param_state.m_nl_arith_delay = 10; + m_param_state.m_nl_arith_expensive_patching = false; + m_param_state.m_nl_arith_gb = true; + m_param_state.m_nl_arith_horner = true; + m_param_state.m_nl_arith_horner_frequency = 4; + m_param_state.m_nl_arith_optimize_bounds = true; + m_param_state.m_nl_arith_propagate_linear_monomials = true; + m_param_state.m_nl_arith_tangents = true; + m_param_state.updt_params(m_p); + ctx->updt_params(m_p); + }; + + smt_params mutate_param_state() { + smt_params p = m_param_state; + random_gen m_rand; + + auto flip_bool = [&](bool &x) { + if ((m_rand() % 2) == 0) + x = !x; + }; + + auto mutate_uint = [&](unsigned &x, unsigned lo, unsigned hi) { + if ((m_rand() % 2) == 0) + x = lo + (m_rand() % (hi - lo + 1)); + }; + + flip_bool(p.m_nl_arith_branching); + flip_bool(p.m_nl_arith_cross_nested); + mutate_uint(p.m_nl_arith_delay, 5, 20); + flip_bool(p.m_nl_arith_expensive_patching); + flip_bool(p.m_nl_arith_gb); + flip_bool(p.m_nl_arith_horner); + mutate_uint(p.m_nl_arith_horner_frequency, 2, 6); + flip_bool(p.m_nl_arith_optimize_bounds); + flip_bool(p.m_nl_arith_propagate_linear_monomials); + flip_bool(p.m_nl_arith_tangents); + + return p; + } + + public: + param_generator(parallel& p); + lbool run_prefix_step(); + void protocol_iteration(); + unsigned replay_proof_prefixes(vector candidate_param_states, unsigned max_conflicts_epsilon); + + reslimit& limit() { + return m.limit(); + } }; class worker { @@ -173,6 +256,7 @@ namespace smt { batch_manager m_batch_manager; scoped_ptr_vector m_workers; + param_generator m_param_generator; public: parallel(context& ctx) : @@ -180,7 +264,8 @@ namespace smt { num_threads(std::min( (unsigned)std::thread::hardware_concurrency(), ctx.get_fparams().m_threads)), - m_batch_manager(ctx.m, *this) {} + m_batch_manager(ctx.m, *this), + m_param_generator(*this) {} lbool operator()(expr_ref_vector const& asms); };