diff --git a/.travis.yml b/.travis.yml index 50d63e593..3764f8dac 100644 --- a/.travis.yml +++ b/.travis.yml @@ -60,15 +60,17 @@ env: - LINUX_BASE=ubuntu_14.04 C_COMPILER=/usr/bin/gcc-4.8 CXX_COMPILER=/usr/bin/g++-4.8 TARGET_ARCH=x86_64 Z3_BUILD_TYPE=Debug # macOS (a.k.a OSX) support -matrix: - include: - # For now just test a single configuration. macOS builds on TravisCI are - # very slow so we should keep the number of configurations we test on this - # OS to a minimum. - - os: osx - osx_image: xcode8.3 - # Note: Apple Clang does not support OpenMP - env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 +# FIXME: macOS support is temporarily disabled due to @wintersteiger 's concerns. +# See https://github.com/Z3Prover/z3/pull/1207#issuecomment-322200998 +# matrix: +# include: +# # For now just test a single configuration. macOS builds on TravisCI are +# # very slow so we should keep the number of configurations we test on this +# # OS to a minimum. +# - os: osx +# osx_image: xcode8.3 +# # Note: Apple Clang does not support OpenMP +# env: Z3_BUILD_TYPE=RelWithDebInfo USE_OPENMP=0 script: # Use `travis_wait` when doing LTO builds because this configuration will # have long link times during which it will not show any output which diff --git a/CMakeLists.txt b/CMakeLists.txt index a3ed2a312..715679957 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -234,22 +234,18 @@ if ("${CMAKE_SYSTEM_NAME}" STREQUAL "Linux") if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL") endif() - z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin") # Does OSX really not need any special flags? message(STATUS "Platform: Darwin") elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD") message(STATUS "Platform: FreeBSD") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_") - z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "OpenBSD") message(STATUS "Platform: OpenBSD") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_") - z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) elseif (CYGWIN) message(STATUS "Platform: Cygwin") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_CYGWIN") - z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) elseif (WIN32) message(STATUS "Platform: Windows") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS") diff --git a/scripts/mk_util.py b/scripts/mk_util.py index d2e3d6b4c..24f22d8ee 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2443,26 +2443,26 @@ def mk_config(): SO_EXT = '.dylib' SLIBFLAGS = '-dynamiclib' elif sysname == 'Linux': - CXXFLAGS = '%s -fno-strict-aliasing -D_LINUX_' % CXXFLAGS + CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS OS_DEFINES = '-D_LINUX_' SO_EXT = '.so' LDFLAGS = '%s -lrt' % LDFLAGS SLIBFLAGS = '-shared' SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS elif sysname == 'FreeBSD': - CXXFLAGS = '%s -fno-strict-aliasing -D_FREEBSD_' % CXXFLAGS + CXXFLAGS = '%s -D_FREEBSD_' % CXXFLAGS OS_DEFINES = '-D_FREEBSD_' SO_EXT = '.so' LDFLAGS = '%s -lrt' % LDFLAGS SLIBFLAGS = '-shared' SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS elif sysname == 'OpenBSD': - CXXFLAGS = '%s -fno-strict-aliasing -D_OPENBSD_' % CXXFLAGS + CXXFLAGS = '%s -D_OPENBSD_' % CXXFLAGS OS_DEFINES = '-D_OPENBSD_' SO_EXT = '.so' SLIBFLAGS = '-shared' elif sysname[:6] == 'CYGWIN': - CXXFLAGS = '%s -D_CYGWIN -fno-strict-aliasing' % CXXFLAGS + CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS OS_DEFINES = '-D_CYGWIN' SO_EXT = '.dll' SLIBFLAGS = '-shared' diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index a1efed19e..43748bd42 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -35,7 +35,7 @@ Revision History: parameter::~parameter() { if (m_kind == PARAM_RATIONAL) { - reinterpret_cast(m_rational)->~rational(); + m_rational.~rational(); } } @@ -50,14 +50,14 @@ parameter& parameter::operator=(parameter const& other) { return *this; } if (m_kind == PARAM_RATIONAL) { - reinterpret_cast(m_rational)->~rational(); + m_rational.~rational(); } m_kind = other.m_kind; switch(other.m_kind) { case PARAM_INT: m_int = other.get_int(); break; case PARAM_AST: m_ast = other.get_ast(); break; - case PARAM_SYMBOL: new (m_symbol) symbol(other.get_symbol()); break; - case PARAM_RATIONAL: new (m_rational) rational(other.get_rational()); break; + case PARAM_SYMBOL: m_symbol = other.get_symbol(); break; + case PARAM_RATIONAL: m_rational = other.get_rational(); break; case PARAM_DOUBLE: m_dval = other.m_dval; break; case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break; default: diff --git a/src/ast/ast.h b/src/ast/ast.h index 3a3f08df2..64122a7dc 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -100,12 +100,12 @@ private: // It is not possible to use tag pointers, since symbols are already tagged. union { - int m_int; // for PARAM_INT - ast* m_ast; // for PARAM_AST - char m_symbol[sizeof(symbol)]; // for PARAM_SYMBOL - char m_rational[sizeof(rational)]; // for PARAM_RATIONAL - double m_dval; // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin) - unsigned m_ext_id; // for PARAM_EXTERNAL + int m_int; // for PARAM_INT + ast* m_ast; // for PARAM_AST + symbol m_symbol; // for PARAM_SYMBOL + rational m_rational; // for PARAM_RATIONAL + double m_dval; // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin) + unsigned m_ext_id; // for PARAM_EXTERNAL }; public: @@ -114,12 +114,10 @@ public: explicit parameter(int val): m_kind(PARAM_INT), m_int(val) {} explicit parameter(unsigned val): m_kind(PARAM_INT), m_int(val) {} explicit parameter(ast * p): m_kind(PARAM_AST), m_ast(p) {} - explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL) { new (m_symbol) symbol(s); } - explicit parameter(rational const & r): m_kind(PARAM_RATIONAL) { new (m_rational) rational(r); } + explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s) {} + explicit parameter(rational const & r): m_kind(PARAM_RATIONAL), m_rational(r) {} explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {} - explicit parameter(const char *s):m_kind(PARAM_SYMBOL) { - new (m_symbol) symbol(s); - } + explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(s) {} explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {} parameter(parameter const&); @@ -156,8 +154,8 @@ public: int get_int() const { SASSERT(is_int()); return m_int; } ast * get_ast() const { SASSERT(is_ast()); return m_ast; } - symbol const & get_symbol() const { SASSERT(is_symbol()); return *(reinterpret_cast(m_symbol)); } - rational const & get_rational() const { SASSERT(is_rational()); return *(reinterpret_cast(m_rational)); } + symbol const & get_symbol() const { SASSERT(is_symbol()); return m_symbol; } + rational const & get_rational() const { SASSERT(is_rational()); return m_rational; } double get_double() const { SASSERT(is_double()); return m_dval; } unsigned get_ext_id() const { SASSERT(is_external()); return m_ext_id; } diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index d24ae4f49..c40927179 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -307,9 +307,8 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m; - imp * d = alloc(imp, m, m_params); - std::swap(d, m_imp); - dealloc(d); + m_imp->~imp(); + m_imp = new (m_imp) imp(m, m_params); } }; diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp index 91f1d9020..79526a101 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -171,9 +171,8 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m; - imp * d = alloc(imp, m, m_params); - std::swap(d, m_imp); - dealloc(d); + m_imp->~imp(); + m_imp = new (m_imp) imp(m, m_params); } }; diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index a4b9825cc..476c21232 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -502,9 +502,8 @@ void reduce_args_tactic::operator()(goal_ref const & g, } void reduce_args_tactic::cleanup() { - ast_manager & m = m_imp->m(); - imp * d = alloc(imp, m); - std::swap(d, m_imp); - dealloc(d); + ast_manager & m = m_imp->m(); + m_imp->~imp(); + m_imp = new (m_imp) imp(m); } diff --git a/src/util/debug.h b/src/util/debug.h index adc9fc6b7..e0ceb9a64 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -90,14 +90,7 @@ bool is_debug_enabled(const char * tag); exit(-1); \ } -#define MAKE_NAME2(LINE) zofty_ ## LINE -#define MAKE_NAME(LINE) MAKE_NAME2(LINE) -#define DBG_UNIQUE_NAME MAKE_NAME(__LINE__) -#ifdef __GNUC__ -#define COMPILE_TIME_ASSERT(expr) extern __attribute__((unused)) char DBG_UNIQUE_NAME[expr] -#else -#define COMPILE_TIME_ASSERT(expr) extern char DBG_UNIQUE_NAME[expr] -#endif +#define COMPILE_TIME_ASSERT(expr) static_assert(expr, "") void finalize_debug(); /* diff --git a/src/util/optional.h b/src/util/optional.h index 22757f3bd..6a00cf841 100644 --- a/src/util/optional.h +++ b/src/util/optional.h @@ -23,32 +23,35 @@ Revision History: template class optional { - char m_obj[sizeof(T)]; - char m_initialized; + union { + T m_obj; + char m_dummy; + }; + bool m_initialized; void construct(const T & val) { - m_initialized = 1; - new (reinterpret_cast(m_obj)) T(val); + m_initialized = true; + new (&m_obj) T(val); } void destroy() { - if (m_initialized == 1) { - reinterpret_cast(m_obj)->~T(); + if (m_initialized) { + m_obj.~T(); } - m_initialized = 0; + m_initialized = false; } public: optional(): - m_initialized(0) {} + m_initialized(false) {} explicit optional(const T & val) { construct(val); } optional(const optional & val): - m_initialized(0) { - if (val.m_initialized == 1) { + m_initialized(false) { + if (val.m_initialized) { construct(*val); } } @@ -59,13 +62,13 @@ public: static optional const & undef() { static optional u; return u; } - bool initialized() const { return m_initialized == 1; } - operator bool() const { return m_initialized == 1; } - bool operator!() const { return m_initialized == 0; } + bool initialized() const { return m_initialized; } + operator bool() const { return m_initialized; } + bool operator!() const { return !m_initialized; } T * get() const { - if (m_initialized == 1) { - return reinterpret_cast(m_obj); + if (m_initialized) { + return &m_obj; } else { return 0; @@ -73,29 +76,29 @@ public: } void set_invalid() { - if (m_initialized == 1) { + if (m_initialized) { destroy(); } } T * operator->() { - SASSERT(m_initialized==1); - return reinterpret_cast(m_obj); + SASSERT(m_initialized); + return &m_obj; } T const * operator->() const { - SASSERT(m_initialized==1); - return reinterpret_cast(m_obj); + SASSERT(m_initialized); + return &m_obj; } const T & operator*() const { - SASSERT(m_initialized==1); - return *reinterpret_cast(m_obj); + SASSERT(m_initialized); + return m_obj; } T & operator*() { - SASSERT(m_initialized==1); - return *reinterpret_cast(m_obj); + SASSERT(m_initialized); + return m_obj; } optional & operator=(const T & val) {