From 51a947b73d9d597029c30c62fe8d59d013a48f3c Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sun, 9 Dec 2018 16:16:20 +0700 Subject: [PATCH] Change how 64 bit builds are detected. Instead of doing this at configure time, we look at the actual compile time status. This also avoids hardcoding checks based on what CPU architecture is present, which doesn't work when Z3 is being built on non-x86_64 platforms. --- CMakeLists.txt | 3 --- scripts/mk_util.py | 5 ++--- scripts/update_api.py | 2 +- src/api/java/CMakeLists.txt | 3 +-- src/sat/sat_clause.cpp | 4 ++-- src/shell/main.cpp | 4 ++-- src/smt/watch_list.cpp | 6 +++--- src/util/hwf.cpp | 4 ++-- src/util/machine.h | 2 +- src/util/mpn.h | 2 +- src/util/mpz.cpp | 2 +- src/util/symbol.h | 2 +- 12 files changed, 17 insertions(+), 22 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 34d2c689d..9877af89e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -205,9 +205,6 @@ message(STATUS "PYTHON_EXECUTABLE: ${PYTHON_EXECUTABLE}") include(${CMAKE_SOURCE_DIR}/cmake/target_arch_detect.cmake) detect_target_architecture(TARGET_ARCHITECTURE) message(STATUS "Detected target architecture: ${TARGET_ARCHITECTURE}") -if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") - list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_AMD64_") -endif() ################################################################################ diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 83ae3d455..b3e75af32 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2635,7 +2635,7 @@ def mk_config(): 'SLINK_FLAGS=/nologo /LDd\n' % static_opt) if VS_X64: config.write( - 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- %s %s\n' % (extra_opt, static_opt)) + 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- %s %s\n' % (extra_opt, static_opt)) config.write( 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n' 'SLINK_EXTRA_FLAGS=/link /DEBUG /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)) @@ -2660,7 +2660,7 @@ def mk_config(): extra_opt = '%s /D _TRACE ' % extra_opt if VS_X64: config.write( - 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP %s %s\n' % (GL, extra_opt, static_opt)) + 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _UNICODE /D UNICODE /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP %s %s\n' % (GL, extra_opt, static_opt)) config.write( 'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 %s\n' 'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt)) @@ -2782,7 +2782,6 @@ def mk_config(): if is64(): if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'): CXXFLAGS = '%s -fPIC' % CXXFLAGS - CPPFLAGS = '%s -D_AMD64_' % CPPFLAGS if sysname == 'Linux': CPPFLAGS = '%s -D_USE_THREAD_LOCAL' % CPPFLAGS elif not LINUX_X64: diff --git a/scripts/update_api.py b/scripts/update_api.py index 13f1aaf9c..161c783e8 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -584,7 +584,7 @@ def mk_java(java_dir, package_name): java_wrapper.write('extern "C" {\n') java_wrapper.write('#endif\n\n') java_wrapper.write('#ifdef __GNUC__\n#if __GNUC__ >= 4\n#define DLL_VIS __attribute__ ((visibility ("default")))\n#else\n#define DLL_VIS\n#endif\n#else\n#define DLL_VIS\n#endif\n\n') - java_wrapper.write('#if defined(_M_X64) || defined(_AMD64_)\n\n') + java_wrapper.write('#if defined(__LP64__) || defined(_WIN64)\n\n') java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW) \\\n') java_wrapper.write(' T * NEW = (OLD == 0) ? 0 : (T*) jenv->GetLongArrayElements(OLD, NULL);\n') java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW) \\\n') diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 302b3d5bd..c2d73ffb1 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -39,8 +39,7 @@ add_library(z3java SHARED ${Z3_JAVA_NATIVE_CPP}) target_link_libraries(z3java PRIVATE libz3) # FIXME: # Not sure if using all the flags used by the Z3 components is really necessary -# here. At the bare minimum setting _AMD64_ depending on the target is -# necessary but seeing as the Python build system uses all the flags used for building +# here. The Python build system uses all the flags used for building # Z3's components to build ``Native.cpp`` lets do the same for now. target_compile_options(z3java PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) target_compile_definitions(z3java PRIVATE ${Z3_COMPONENT_CXX_DEFINES}) diff --git a/src/sat/sat_clause.cpp b/src/sat/sat_clause.cpp index 3cbd3015b..31a4bba72 100644 --- a/src/sat/sat_clause.cpp +++ b/src/sat/sat_clause.cpp @@ -111,7 +111,7 @@ namespace sat { clause_offset clause::get_new_offset() const { unsigned o1 = m_lits[0].index(); -#if defined(_AMD64_) || defined(_M_IA64) +#if defined(__LP64__) || defined(_WIN64) if (sizeof(clause_offset) == 8) { unsigned o2 = m_lits[1].index(); return (clause_offset)o1 + (((clause_offset)o2) << 32); @@ -122,7 +122,7 @@ namespace sat { void clause::set_new_offset(clause_offset offset) { m_lits[0] = to_literal(static_cast(offset)); -#if defined(_AMD64_) || defined(_M_IA64) +#if defined(__LP64__) || defined(_WIN64) if (sizeof(offset) == 8) { m_lits[1] = to_literal(static_cast(offset >> 32)); } diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 3b97d4462..b036628b1 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -60,7 +60,7 @@ void error(const char * msg) { void display_usage() { std::cout << "Z3 [version " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER; std::cout << " - "; -#ifdef _AMD64_ +#if defined(__LP64__) || defined(_WIN64) std::cout << "64"; #else std::cout << "32"; @@ -161,7 +161,7 @@ void parse_cmd_line_args(int argc, char ** argv) { if (strcmp(opt_name, "version") == 0) { std::cout << "Z3 version " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER; std::cout << " - "; -#ifdef _AMD64_ +#if defined(__LP64__) || defined(_WIN64) std::cout << "64"; #else std::cout << "32"; diff --git a/src/smt/watch_list.cpp b/src/smt/watch_list.cpp index 778e93021..f95e1c571 100644 --- a/src/smt/watch_list.cpp +++ b/src/smt/watch_list.cpp @@ -21,7 +21,7 @@ Revision History: namespace smt { #define DEFAULT_WATCH_LIST_SIZE (sizeof(clause *) * 4) -#ifdef _AMD64_ +#if defined(__LP64__) || defined(_WIN64) // make sure data is aligned in 64 bit machines #define HEADER_SIZE (4 * sizeof(unsigned)) #else @@ -38,7 +38,7 @@ namespace smt { if (m_data == nullptr) { unsigned size = DEFAULT_WATCH_LIST_SIZE + HEADER_SIZE; unsigned * mem = reinterpret_cast(alloc_svect(char, size)); -#ifdef _AMD64_ +#if defined(__LP64__) || defined(_WIN64) ++mem; // make sure data is aligned in 64 bit machines #endif *mem = 0; @@ -61,7 +61,7 @@ namespace smt { unsigned new_capacity = (((curr_capacity * 3 + sizeof(clause *)) >> 1)+3)&~3U; unsigned * mem = reinterpret_cast(alloc_svect(char, new_capacity + HEADER_SIZE)); unsigned curr_end_cls = end_cls_core(); -#ifdef _AMD64_ +#if defined(__LP64__) || defined(_WIN64) ++mem; // make sure data is aligned in 64 bit machines #endif *mem = curr_end_cls; diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index e6393adbd..4a7a0b7e4 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -61,7 +61,7 @@ hwf_manager::hwf_manager() : m_mpz_manager(m_mpq_manager) { #ifdef _WINDOWS -#if defined(_AMD64_) || defined(_M_IA64) +#if defined(_WIN64) // Precision control is not supported on x64. // See: http://msdn.microsoft.com/en-us/library/e9b52ceh(VS.110).aspx // CMW: I think this is okay though, the compiler will chose the right instructions @@ -557,7 +557,7 @@ void hwf_manager::mk_ninf(hwf & o) { } #ifdef _WINDOWS -#if defined(_AMD64_) || defined(_M_IA64) +#if defined(_WIN64) #ifdef USE_INTRINSICS #define SETRM(RM) _MM_SET_ROUNDING_MODE(RM) #else diff --git a/src/util/machine.h b/src/util/machine.h index 70baee41e..1ccff6330 100644 --- a/src/util/machine.h +++ b/src/util/machine.h @@ -20,7 +20,7 @@ Revision History: #ifndef MACHINE_H_ #define MACHINE_H_ -#ifdef _AMD64_ +#if defined(__LP64__) || defined(_WIN64) #define PTR_ALIGNMENT 3 #else #define PTR_ALIGNMENT 2 diff --git a/src/util/mpn.h b/src/util/mpn.h index ea20fc42b..bae972b0c 100644 --- a/src/util/mpn.h +++ b/src/util/mpn.h @@ -61,7 +61,7 @@ public: char * to_string(mpn_digit const * a, size_t lng, char * buf, size_t lbuf) const; private: - #ifdef _AMD64_ + #if defined(__LP64__) || defined(_WIN64) class mpn_sbuffer : public sbuffer { public: mpn_sbuffer() : sbuffer() {} diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index af95e1a2a..0d3a6040d 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -56,7 +56,7 @@ Revision History: #define _trailing_zeros32(X) _tzcnt_u32(X) #endif -#if defined(_AMD64_) +#if defined(__LP64__) || defined(_WIN64) #if defined(__GNUC__) #define _trailing_zeros64(X) __builtin_ctzll(X) #else diff --git a/src/util/symbol.h b/src/util/symbol.h index 40844cf3b..90a4eeb38 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -56,7 +56,7 @@ public: explicit symbol(char const * d); explicit symbol(unsigned idx): m_data(BOXTAGINT(char const *, idx, 1)) { -#ifndef _AMD64_ +#if !defined(__LP64__) && !defined(_WIN64) SASSERT(idx < (SIZE_MAX >> PTR_ALIGNMENT)); #endif }