From 4b00bc636bda344ba8ae7ea28a2d5d949d4dc629 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 14 Aug 2017 23:00:59 +0100 Subject: [PATCH] revert the patch to remove no-strict-aliasing VS 2012 doesnt support C++11 unions.. --- CMakeLists.txt | 4 ++++ scripts/mk_util.py | 8 +++---- src/ast/ast.cpp | 8 +++---- src/ast/ast.h | 24 +++++++++++---------- src/util/optional.h | 51 +++++++++++++++++++++------------------------ 5 files changed, 49 insertions(+), 46 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 715679957..a3ed2a312 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -234,18 +234,22 @@ 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 24f22d8ee..d2e3d6b4c 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 -D_LINUX_' % CXXFLAGS + CXXFLAGS = '%s -fno-strict-aliasing -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 -D_FREEBSD_' % CXXFLAGS + CXXFLAGS = '%s -fno-strict-aliasing -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 -D_OPENBSD_' % CXXFLAGS + CXXFLAGS = '%s -fno-strict-aliasing -D_OPENBSD_' % CXXFLAGS OS_DEFINES = '-D_OPENBSD_' SO_EXT = '.so' SLIBFLAGS = '-shared' elif sysname[:6] == 'CYGWIN': - CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS + CXXFLAGS = '%s -D_CYGWIN -fno-strict-aliasing' % CXXFLAGS OS_DEFINES = '-D_CYGWIN' SO_EXT = '.dll' SLIBFLAGS = '-shared' diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 38d432f33..a1efed19e 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -35,7 +35,7 @@ Revision History: parameter::~parameter() { if (m_kind == PARAM_RATIONAL) { - m_rational.~rational(); + reinterpret_cast(m_rational)->~rational(); } } @@ -50,14 +50,14 @@ parameter& parameter::operator=(parameter const& other) { return *this; } if (m_kind == PARAM_RATIONAL) { - m_rational.~rational(); + reinterpret_cast(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: m_symbol = other.get_symbol(); break; - case PARAM_RATIONAL: new (&m_rational) rational(other.get_rational()); 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_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 64122a7dc..3a3f08df2 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 - 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 + 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 }; public: @@ -114,10 +114,12 @@ 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), m_symbol(s) {} - explicit parameter(rational const & r): m_kind(PARAM_RATIONAL), m_rational(r) {} + 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(double d):m_kind(PARAM_DOUBLE), m_dval(d) {} - explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(s) {} + explicit parameter(const char *s):m_kind(PARAM_SYMBOL) { + new (m_symbol) symbol(s); + } explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {} parameter(parameter const&); @@ -154,8 +156,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 m_symbol; } - rational const & get_rational() const { SASSERT(is_rational()); return m_rational; } + 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)); } 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/util/optional.h b/src/util/optional.h index 6a00cf841..22757f3bd 100644 --- a/src/util/optional.h +++ b/src/util/optional.h @@ -23,35 +23,32 @@ Revision History: template class optional { - union { - T m_obj; - char m_dummy; - }; - bool m_initialized; + char m_obj[sizeof(T)]; + char m_initialized; void construct(const T & val) { - m_initialized = true; - new (&m_obj) T(val); + m_initialized = 1; + new (reinterpret_cast(m_obj)) T(val); } void destroy() { - if (m_initialized) { - m_obj.~T(); + if (m_initialized == 1) { + reinterpret_cast(m_obj)->~T(); } - m_initialized = false; + m_initialized = 0; } public: optional(): - m_initialized(false) {} + m_initialized(0) {} explicit optional(const T & val) { construct(val); } optional(const optional & val): - m_initialized(false) { - if (val.m_initialized) { + m_initialized(0) { + if (val.m_initialized == 1) { construct(*val); } } @@ -62,13 +59,13 @@ public: static optional const & undef() { static optional u; return u; } - bool initialized() const { return m_initialized; } - operator bool() const { return m_initialized; } - bool operator!() const { return !m_initialized; } + bool initialized() const { return m_initialized == 1; } + operator bool() const { return m_initialized == 1; } + bool operator!() const { return m_initialized == 0; } T * get() const { - if (m_initialized) { - return &m_obj; + if (m_initialized == 1) { + return reinterpret_cast(m_obj); } else { return 0; @@ -76,29 +73,29 @@ public: } void set_invalid() { - if (m_initialized) { + if (m_initialized == 1) { destroy(); } } T * operator->() { - SASSERT(m_initialized); - return &m_obj; + SASSERT(m_initialized==1); + return reinterpret_cast(m_obj); } T const * operator->() const { - SASSERT(m_initialized); - return &m_obj; + SASSERT(m_initialized==1); + return reinterpret_cast(m_obj); } const T & operator*() const { - SASSERT(m_initialized); - return m_obj; + SASSERT(m_initialized==1); + return *reinterpret_cast(m_obj); } T & operator*() { - SASSERT(m_initialized); - return m_obj; + SASSERT(m_initialized==1); + return *reinterpret_cast(m_obj); } optional & operator=(const T & val) {