diff --git a/CMakeLists.txt b/CMakeLists.txt index c8ecb5295..a3bba73ba 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -411,6 +411,38 @@ endif() ################################################################################ include(${CMAKE_SOURCE_DIR}/cmake/compiler_lto.cmake) +################################################################################ +# Control flow integrity +################################################################################ +option(ENABLE_CFI "Enable control flow integrity checking" OFF) +if (ENABLE_CFI) + set(build_types_with_cfi "RELEASE" "RELWITHDEBINFO") + if (NOT LINK_TIME_OPTIMIZATION) + message(FATAL_ERROR "Cannot enable control flow integrity checking without link-time optimization." + "You should set LINK_TIME_OPTIMIZATION to ON or ENABLE_CFI to OFF.") + endif() + 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 ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") + 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() + else() + message(FATAL_ERROR "Can't enable control flow integrity for compiler \"${CMAKE_CXX_COMPILER_ID}\"." + "You should set ENABLE_CFI to OFF or use Clang or MSVC to compile.") + endif() +endif() + ################################################################################ # MSVC specific flags inherited from old build system ################################################################################ diff --git a/README-CMake.md b/README-CMake.md index 715cacad2..605c14818 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -265,6 +265,8 @@ The following useful options can be passed to CMake whilst configuring. * ``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. +* ``ENABLE_CFI`` - BOOL. If set to ``TRUE`` will enable Control Flow Integrity security checks. This is only supported by MSVC and Clang and will + fail on other compilers. This requires LINK_TIME_OPTIMIZATION to also be enabled. * ``API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature. * ``WARNINGS_AS_ERRORS`` - STRING. If set to ``TRUE`` compiler warnings will be treated as errors. If set to ``False`` 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/cmake/msvc_legacy_quirks.cmake b/cmake/msvc_legacy_quirks.cmake index 2ca20277c..36fe82bb3 100644 --- a/cmake/msvc_legacy_quirks.cmake +++ b/cmake/msvc_legacy_quirks.cmake @@ -184,7 +184,12 @@ foreach (_build_type ${_build_types_as_upper}) # 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") + if(ENABLE_CFI) + # CFI requires /DYNAMICBASE to be enabled. + string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /DYNAMICBASE") + else() + string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /DYNAMICBASE:NO") + endif() # FIXME: This is not necessary. This is MSVC's default. # Indicate that the executable is compatible with DEP diff --git a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh index 0d8e59b0f..666673328 100755 --- a/contrib/ci/scripts/test_z3_unit_tests_cmake.sh +++ b/contrib/ci/scripts/test_z3_unit_tests_cmake.sh @@ -1,6 +1,7 @@ #!/bin/bash SCRIPT_DIR="$( cd ${BASH_SOURCE[0]%/*} ; echo $PWD )" +. ${SCRIPT_DIR}/run_quiet.sh set -x set -e @@ -21,4 +22,5 @@ cd "${Z3_BUILD_DIR}" # Build and run internal tests cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}" -./test-z3 +# Run all tests that don't require arguments +run_quiet ./test-z3 /a diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 8b5f941c8..f97397108 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -429,8 +429,9 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) { if ((get_sutil().is_seq(s) || get_sutil().is_re(s)) && !get_sutil().is_string(s)) { ptr_buffer fs; fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast()))); - return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"Re"); + return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"RegEx"); } +#if 0 if (get_dtutil().is_datatype(s)) { ptr_buffer fs; unsigned sz = get_dtutil().get_datatype_num_parameter_sorts(s); @@ -439,6 +440,7 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) { } return mk_seq1(m, fs.begin(), fs.end(), f2f(), s->get_name().str().c_str()); } +#endif return format_ns::mk_string(get_manager(), s->get_name().str().c_str()); } diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 8cf3965cf..fe02f24a0 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -366,13 +366,14 @@ class smt_printer { return; } else if (s->is_sort_of(m_dt_fid, DATATYPE_SORT)) { + m_out << m_renaming.get_symbol(s->get_name()); +#if 0 datatype_util util(m_manager); unsigned num_sorts = util.get_datatype_num_parameter_sorts(s); if (num_sorts > 0) { m_out << "("; } - m_out << m_renaming.get_symbol(s->get_name()); if (num_sorts > 0) { for (unsigned i = 0; i < num_sorts; ++i) { m_out << " "; @@ -380,6 +381,7 @@ class smt_printer { } m_out << ")"; } +#endif return; } else { diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 92a80375e..5d9491da2 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1190,6 +1190,7 @@ namespace nlsat { info.m_lc = lc_eq.get(); info.m_lc_sign = sign(lc_eq); info.m_lc_add = false; + info.m_lc_add_ineq = false; info.m_lc_const = m_pm.is_const(lc_eq); SASSERT(info.m_lc != 0); scoped_literal new_lit(m_solver); diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 4bf8dab4e..08bb6bbee 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -620,8 +620,8 @@ namespace smt2 { int idx = 0; if (d == 0) { if (m_dt_name2idx.find(id, idx)) { - unsigned num_params = m_dt_name2arity.find(id); throw parser_exception("smtlib 2.6 parametric datatype sorts are not supported"); + // unsigned num_params = m_dt_name2arity.find(id); // d = pm().mk_psort_dt_decl(num_params, id); } else { diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp index 41a269820..c461b130b 100644 --- a/src/smt/smt_case_split_queue.cpp +++ b/src/smt/smt_case_split_queue.cpp @@ -51,9 +51,9 @@ namespace smt { if (!m_theory_var_priority.find(v2, p_v2)) { p_v2 = 0.0; } - // add clause activity - p_v1 += m_activity[v1]; - p_v2 += m_activity[v2]; + // add clause activity + p_v1 += m_activity[v1]; + p_v2 += m_activity[v2]; return p_v1 > p_v2; } }; @@ -82,6 +82,7 @@ namespace smt { virtual void mk_var_eh(bool_var v) { m_queue.reserve(v+1); + SASSERT(!m_queue.contains(v)); m_queue.insert(v); } @@ -130,10 +131,7 @@ namespace smt { virtual void display(std::ostream & out) { bool first = true; - bool_var_act_queue::const_iterator it = m_queue.begin(); - bool_var_act_queue::const_iterator end = m_queue.end(); - for (; it != end ; ++it) { - unsigned v = *it; + for (unsigned v : m_queue) { if (m_context.get_assignment(v) == l_undef) { if (first) { out << "remaining case-splits:\n"; @@ -143,8 +141,7 @@ namespace smt { } } if (!first) - out << "\n"; - + out << "\n"; } virtual ~act_case_split_queue() {}; @@ -166,11 +163,15 @@ namespace smt { act_case_split_queue::activity_increased_eh(v); if (m_queue.contains(v)) m_queue.decreased(v); + if (m_delayed_queue.contains(v)) + m_delayed_queue.decreased(v); } virtual void mk_var_eh(bool_var v) { m_queue.reserve(v+1); m_delayed_queue.reserve(v+1); + SASSERT(!m_delayed_queue.contains(v)); + SASSERT(!m_queue.contains(v)); if (m_context.is_searching()) m_delayed_queue.insert(v); else @@ -1099,8 +1100,6 @@ namespace smt { #endif GOAL_STOP(); - - //std::cout << "goal set, time " << m_goal_time.get_seconds() << "\n"; } void set_global_generation() diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 4e56d3004..b5789a597 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1826,6 +1826,7 @@ namespace smt { } void context::rescale_bool_var_activity() { + TRACE("case_split", tout << "rescale\n";); svector::iterator it = m_activity.begin(); svector::iterator end = m_activity.end(); for (; it != end; ++it) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 9c70f5999..6b3129d91 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1040,6 +1040,7 @@ namespace smt { if (act > ACTIVITY_LIMIT) rescale_bool_var_activity(); m_case_split_queue->activity_increased_eh(v); + TRACE("case_split", tout << "v" << v << " " << m_bvar_inc << " -> " << act << "\n";); } protected: diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 2e928af37..89e0123a8 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -4653,34 +4653,24 @@ namespace smt { } bool theory_str::get_arith_value(expr* e, rational& val) const { - if (opt_DisableIntegerTheoryIntegration) { - TRACE("str", tout << "WARNING: integer theory integration disabled" << std::endl;); - return false; - } - context& ctx = get_context(); ast_manager & m = get_manager(); - theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e); - if (!tha) { + + // safety + if (!ctx.e_internalized(e)) { + return false; + } + + // if an integer constant exists in the eqc, it should be the root + enode * en_e = ctx.get_enode(e); + enode * root_e = en_e->get_root(); + if (m_autil.is_numeral(root_e->get_owner(), val) && val.is_int()) { + TRACE("str", tout << mk_pp(e, m) << " ~= " << mk_pp(root_e->get_owner(), m) << std::endl;); + return true; + } else { + TRACE("str", tout << "root of eqc of " << mk_pp(e, m) << " is not a numeral" << std::endl;); return false; } - TRACE("str", tout << "checking eqc of " << mk_pp(e, m) << " for arithmetic value" << std::endl;); - expr_ref _val(m); - enode * en_e = ctx.get_enode(e); - enode * it = en_e; - do { - if (m_autil.is_numeral(it->get_owner(), val) && val.is_int()) { - // found an arithmetic term - TRACE("str", tout << mk_pp(it->get_owner(), m) << " is an integer ( ~= " << val << " )" - << std::endl;); - return true; - } else { - TRACE("str", tout << mk_pp(it->get_owner(), m) << " not a numeral" << std::endl;); - } - it = it->get_next(); - } while (it != en_e); - TRACE("str", tout << "no arithmetic values found in eqc" << std::endl;); - return false; } bool theory_str::lower_bound(expr* _e, rational& lo) { diff --git a/src/util/heap.h b/src/util/heap.h index e8964a4f0..cde2451db 100644 --- a/src/util/heap.h +++ b/src/util/heap.h @@ -43,6 +43,15 @@ class heap : private LT { return i >> 1; } + void display(std::ostream& out, unsigned indent, int idx) const { + if (idx < static_cast(m_values.size())) { + for (unsigned i = 0; i < indent; ++i) out << " "; + out << m_values[idx] << "\n"; + display(out, indent + 1, left(idx)); + display(out, indent + 1, right(idx)); + } + } + #ifdef Z3DEBUG // Return true if the value can be inserted in the heap. That is, the vector m_value2indices is big enough to store this value. bool is_valid_value(int v) const { @@ -59,10 +68,13 @@ class heap : private LT { } return true; } + + public: bool check_invariant() const { return check_invariant_core(1); } + #endif private: @@ -219,6 +231,7 @@ public: void insert(int val) { CASSERT("heap", check_invariant()); + CASSERT("heap", !contains(val)); SASSERT(is_valid_value(val)); int idx = static_cast(m_values.size()); m_value2indices[val] = idx; @@ -272,6 +285,11 @@ public: } } } + + void display(std::ostream& out) const { + display(out, 0, 1); + } + }; diff --git a/src/util/lp/lp_settings_instances.cpp b/src/util/lp/lp_settings_instances.cpp index e9a3888ba..ac2ed4b51 100644 --- a/src/util/lp/lp_settings_instances.cpp +++ b/src/util/lp/lp_settings_instances.cpp @@ -2,8 +2,8 @@ Copyright (c) 2017 Microsoft Corporation Author: Lev Nachmanson */ -#include "util/vector.h" #include +#include "util/vector.h" #include "util/lp/lp_settings.hpp" template bool lean::vectors_are_equal(vector const&, vector const&); template bool lean::vectors_are_equal(vector const&, vector const&); diff --git a/src/util/lp/row_eta_matrix_instances.cpp b/src/util/lp/row_eta_matrix_instances.cpp index c32023164..c172eda11 100644 --- a/src/util/lp/row_eta_matrix_instances.cpp +++ b/src/util/lp/row_eta_matrix_instances.cpp @@ -2,8 +2,8 @@ Copyright (c) 2017 Microsoft Corporation Author: Lev Nachmanson */ -#include "util/vector.h" #include +#include "util/vector.h" #include "util/lp/row_eta_matrix.hpp" #include "util/lp/lu.h" namespace lean { diff --git a/src/util/lp/static_matrix_instances.cpp b/src/util/lp/static_matrix_instances.cpp index d0e2045c0..ef4374a50 100644 --- a/src/util/lp/static_matrix_instances.cpp +++ b/src/util/lp/static_matrix_instances.cpp @@ -2,10 +2,10 @@ Copyright (c) 2017 Microsoft Corporation Author: Lev Nachmanson */ -#include "util/vector.h" #include #include #include +#include "util/vector.h" #include "util/lp/static_matrix.hpp" #include "util/lp/lp_core_solver_base.h" #include "util/lp/lp_dual_core_solver.h"