Merge branch 'master' of https://github.com/z3prover/z3

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
 ################################################################################

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.

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")
+    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

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

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<format> 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<format> 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());
 }
 

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 {

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);

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 {

src/smt/smt_case_split_queue.cpp

@@ -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();
+            for (unsigned v : m_queue) {
-            bool_var_act_queue::const_iterator end = m_queue.end();
-            for (; it != end ; ++it) {
-                unsigned v = *it;
                 if (m_context.get_assignment(v) == l_undef) {
                     if (first) {
                         out << "remaining case-splits:\n";
@@ -144,7 +142,6 @@ namespace smt {
             }
             if (!first)
                 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()

src/smt/smt_context.cpp

@@ -1826,6 +1826,7 @@ namespace smt {
     }
     
     void context::rescale_bool_var_activity() {
+        TRACE("case_split", tout << "rescale\n";);
         svector<double>::iterator it  = m_activity.begin();
         svector<double>::iterator end = m_activity.end();
         for (; it != end; ++it)

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:

src/smt/theory_str.cpp

@@ -4653,35 +4653,25 @@ namespace smt {
     }
 
     bool theory_str::get_arith_value(expr* e, rational& val) const {
-        if (opt_DisableIntegerTheoryIntegration) {
+        context& ctx = get_context();
-            TRACE("str", tout << "WARNING: integer theory integration disabled" << std::endl;);
+        ast_manager & m = get_manager();
+
+	// safety
+	if (!ctx.e_internalized(e)) {
 	  return false;
 	}
 	
-        context& ctx = get_context();
+        // if an integer constant exists in the eqc, it should be the root
-        ast_manager & m = get_manager();
-        theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
-        if (!tha) {
-            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;
+        enode * root_e = en_e->get_root();
-        do {
+        if (m_autil.is_numeral(root_e->get_owner(), val) && val.is_int()) {
-            if (m_autil.is_numeral(it->get_owner(), val) && val.is_int()) {
+            TRACE("str", tout << mk_pp(e, m) << " ~= " << mk_pp(root_e->get_owner(), m) << std::endl;);
-                // 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;);
+            TRACE("str", tout << "root of eqc of " << mk_pp(e, m) << " is 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) {
         if (opt_DisableIntegerTheoryIntegration) {

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<int>(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<int>(m_values.size());
         m_value2indices[val] = idx;
@@ -273,6 +286,11 @@ public:
         }
     }
 
+    void display(std::ostream& out) const {
+        display(out, 0, 1);
+    }
+
+  
 };
 
 #endif /* HEAP_H_ */

src/util/lp/lp_settings_instances.cpp

@@ -2,8 +2,8 @@
   Copyright (c) 2017 Microsoft Corporation
   Author: Lev Nachmanson
 */
-#include "util/vector.h"
 #include <memory>
+#include "util/vector.h"
 #include "util/lp/lp_settings.hpp"
 template bool lean::vectors_are_equal<double>(vector<double> const&, vector<double> const&);
 template bool lean::vectors_are_equal<lean::mpq>(vector<lean::mpq > const&, vector<lean::mpq> const&);

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 <memory>
+#include "util/vector.h"
 #include "util/lp/row_eta_matrix.hpp"
 #include "util/lp/lu.h"
 namespace lean {

src/util/lp/static_matrix_instances.cpp

@@ -2,10 +2,10 @@
   Copyright (c) 2017 Microsoft Corporation
   Author: Lev Nachmanson
 */
-#include "util/vector.h"
 #include <memory>
 #include <set>
 #include <utility>
+#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"