From e0fcbc101cc7b52d2b42e8046b4c5e08ea164358 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 12 Nov 2012 04:56:48 +0000 Subject: [PATCH] Added support for clang++ on OSX Signed-off-by: Leonardo de Moura --- README | 11 +++++++++ configure.ac | 12 +++++++--- scripts/config-debug.mk.in | 4 ++-- scripts/config-release.mk.in | 4 ++-- scripts/config-vs-debug-x64.mk | 2 +- scripts/config-vs-debug.mk | 2 +- scripts/config-vs-release.mk | 2 +- scripts/mk_util.py | 43 +++++++++++++++++++++++++++------- src/test/polynomial.cpp | 6 +++++ src/util/object_allocator.h | 2 +- 10 files changed, 68 insertions(+), 20 deletions(-) diff --git a/README b/README index a752c1acd..4c4718ca3 100644 --- a/README +++ b/README @@ -35,3 +35,14 @@ To uninstall Z3, use sudo make uninstall +3) Building Z3 using clang++ on OSX +Remark: clang does not support OpenMP yet. + + autoconf + ./configure CXX=clang++ + python scripts/mk_make.py --noomp + cd build + make + + + diff --git a/configure.ac b/configure.ac index e111a31ce..d92af8f64 100644 --- a/configure.ac +++ b/configure.ac @@ -116,7 +116,7 @@ AS_IF([test "$host_os" = "Darwin"], [ PLATFORM=osx SO_EXT=.dylib LDFLAGS= - SLIBFLAGS="-dynamiclib -fopenmp" + SLIBFLAGS="-dynamiclib" SLIBEXTRAFLAGS="" COMP_VERSIONS="-compatibility_version \$(Z3_VERSION) -current_version \$(Z3_VERSION)" STATIC_FLAGS= @@ -124,7 +124,7 @@ AS_IF([test "$host_os" = "Darwin"], [ PLATFORM=linux SO_EXT=.so LDFLAGS=-lrt - SLIBFLAGS="-shared -fopenmp" + SLIBFLAGS="-shared" SLIBEXTRAFLAGS= COMP_VERSIONS= STATIC_FLAGS=-static @@ -133,7 +133,7 @@ AS_IF([test "$host_os" = "Darwin"], [ PLATFORM=win SO_EXT=.dll LDFLAGS= - SLIBFLAGS="-shared -fopenmp" + SLIBFLAGS="-shared" SLIBEXTRAFLAGS= COMP_VERSIONS= CXXFLAGS+=" -D_CYGWIN -fno-strict-aliasing" @@ -141,6 +141,12 @@ AS_IF([test "$host_os" = "Darwin"], [ [ AC_MSG_ERROR([Unknown host platform: $host_os]) ]) + +# Only add -mfpmath=sse if g++ +if test "$CXX" = "g++"; then + CXXFLAGS+=" -mfpmath=sse" +fi + AC_SUBST(SLIBFLAGS) AC_SUBST(LDFLAGS) AC_SUBST(SLIBEXTRAFLAGS) diff --git a/scripts/config-debug.mk.in b/scripts/config-debug.mk.in index 187130607..d15ab82df 100644 --- a/scripts/config-debug.mk.in +++ b/scripts/config-debug.mk.in @@ -1,7 +1,7 @@ CC=@CC@ PREFIX=@prefix@ CXX=@CXX@ -CXXFLAGS=@CPPFLAGS@ @CXXFLAGS@ -DZ3DEBUG -D_TRACE -c -g -Wall -fopenmp -msse -msse2 -mfpmath=sse +CXXFLAGS=@CPPFLAGS@ @CXXFLAGS@ -DZ3DEBUG -D_TRACE -c -g -Wall -msse -msse2 CXX_OUT_FLAG=-o OBJ_EXT=.o LIB_EXT=.a @@ -12,7 +12,7 @@ EXE_EXT= LINK=@CXX@ LINK_FLAGS= LINK_OUT_FLAG=-o -LINK_EXTRA_FLAGS=-lpthread -fopenmp @LDFLAGS@ +LINK_EXTRA_FLAGS=-lpthread @LDFLAGS@ SO_EXT=@SO_EXT@ SLINK=@CXX@ SLINK_FLAGS=@SLIBFLAGS@ diff --git a/scripts/config-release.mk.in b/scripts/config-release.mk.in index 2f0a34a15..5936c6135 100644 --- a/scripts/config-release.mk.in +++ b/scripts/config-release.mk.in @@ -1,7 +1,7 @@ CC=@CC@ PREFIX=@prefix@ CXX=@CXX@ -CXXFLAGS=@CPPFLAGS@ @CXXFLAGS@ -c -O3 -fomit-frame-pointer -fopenmp -msse -msse2 -mfpmath=sse +CXXFLAGS=@CPPFLAGS@ @CXXFLAGS@ -c -O3 -fomit-frame-pointer -msse -msse2 CXX_OUT_FLAG=-o OBJ_EXT=.o LIB_EXT=.a @@ -12,7 +12,7 @@ EXE_EXT= LINK=@CXX@ LINK_FLAGS= LINK_OUT_FLAG=-o -LINK_EXTRA_FLAGS=-lpthread -fopenmp @LDFLAGS@ +LINK_EXTRA_FLAGS=-lpthread @LDFLAGS@ SO_EXT=@SO_EXT@ SLINK=@CXX@ SLINK_FLAGS=@SLIBFLAGS@ diff --git a/scripts/config-vs-debug-x64.mk b/scripts/config-vs-debug-x64.mk index 5810d8fe4..d5654292a 100644 --- a/scripts/config-vs-debug-x64.mk +++ b/scripts/config-vs-debug-x64.mk @@ -1,6 +1,6 @@ CC=cl CXX=cl -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 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /openmp /Gd /analyze- +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 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- CXX_OUT_FLAG=/Fo OBJ_EXT=.obj LIB_EXT=.lib diff --git a/scripts/config-vs-debug.mk b/scripts/config-vs-debug.mk index bef47d337..8733e2ffb 100644 --- a/scripts/config-vs-debug.mk +++ b/scripts/config-vs-debug.mk @@ -1,6 +1,6 @@ CC=cl CXX=cl -CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /openmp /Gd /analyze- /arch:SSE2 +CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 CXX_OUT_FLAG=/Fo OBJ_EXT=.obj LIB_EXT=.lib diff --git a/scripts/config-vs-release.mk b/scripts/config-vs-release.mk index d2c44f704..0257d87dc 100644 --- a/scripts/config-vs-release.mk +++ b/scripts/config-vs-release.mk @@ -1,6 +1,6 @@ CC=cl CXX=cl -CXXFLAGS=/nologo /c /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /openmp /Gd /analyze- /arch:SSE2 +CXXFLAGS=/nologo /c /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 CXX_OUT_FLAG=/Fo OBJ_EXT=.obj LIB_EXT=.lib diff --git a/scripts/mk_util.py b/scripts/mk_util.py index ae8cf32bb..0bee78e79 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -40,6 +40,7 @@ Z3PY_SRC_DIR=None VS_PROJ = False TRACE = False DOTNET_ENABLED=False +OMP = True VER_MAJOR=None VER_MINOR=None @@ -120,11 +121,12 @@ def display_help(): print " -v, --vsproj generate Visual Studio Project Files." print " -t, --trace enable tracing in release mode." print " -n, --nodotnet do not generate Microsoft.Z3.dll make rules." + print " --noomp disable support for openmp." exit(0) # Parse configuration option for mk_make script def parse_options(): - global VERBOSE, DEBUG_MODE, IS_WINDOW, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, DOTNET_ENABLED + global VERBOSE, DEBUG_MODE, IS_WINDOW, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, DOTNET_ENABLED, OMP options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:dsxhmcvtn', ['build=', 'debug', 'silent', @@ -134,7 +136,8 @@ def parse_options(): 'showcpp', 'vsproj', 'trace', - 'nodotnet' + 'nodotnet', + 'noomp' ]) for opt, arg in options: if opt in ('-b', '--build'): @@ -161,6 +164,8 @@ def parse_options(): TRACE = True elif opt in ('-n', '--nodotnet'): DOTNET_ENABLED = False + elif opt in ('--noomp'): + OMP = False else: raise MKException("Invalid command line option '%s'" % opt) @@ -336,13 +341,24 @@ class Component: if SHOW_CPPS: out.write('\t@echo %s/%s\n' % (self.src_dir, cppfile)) # TRACE is enabled in debug mode by default - trace_opt = '' + extra_opt = '' if TRACE and not DEBUG_MODE: if IS_WINDOW: - trace_opt = '/D _TRACE' + extra_opt = '/D _TRACE' else: - trace_opt = '-D _TRACE' - out.write('\t@$(CXX) $(CXXFLAGS) %s $(%s) $(CXX_OUT_FLAG)%s %s\n' % (trace_opt, include_defs, objfile, srcfile)) + extra_opt = '-D _TRACE' + if not OMP: + if IS_WINDOW: + extra_opt = '%s /D _NO_OMP_' % extra_opt + else: + extra_opt = '%s -D _NO_OMP_' % extra_opt + else: + if IS_WINDOW: + extra_opt = '%s /openmp' % extra_opt + else: + extra_opt = '%s -fopenmp' % extra_opt + + out.write('\t@$(CXX) $(CXXFLAGS) %s $(%s) $(CXX_OUT_FLAG)%s %s\n' % (extra_opt, include_defs, objfile, srcfile)) def mk_makefile(self, out): include_defs = mk_fresh_name('includes') @@ -476,7 +492,10 @@ class ExeComponent(Component): for dep in deps: c_dep = get_component(dep) out.write(' %s/%s$(LIB_EXT)' % (c_dep.build_dir, c_dep.name)) - out.write(' $(LINK_EXTRA_FLAGS)\n') + extra_flags = '' + if OMP and not WINDOWS: + extra_flags = '-fopenmp' + out.write(' $(LINK_EXTRA_FLAGS) %s\n' % extra_flags) out.write('%s: %s\n\n' % (self.name, exefile)) def require_install_tactics(self): @@ -552,7 +571,10 @@ class DLLComponent(Component): if not dep in self.reexports: c_dep = get_component(dep) out.write(' %s/%s$(LIB_EXT)' % (c_dep.build_dir, c_dep.name)) - out.write(' $(SLINK_EXTRA_FLAGS)') + extra_flags= '' + if OMP and not WINDOWS: + extra_flags = '-fopenmp' + out.write(' $(SLINK_EXTRA_FLAGS) %s' % extra_flags) if IS_WINDOW: out.write(' /DEF:%s/%s.def' % (self.to_src_dir, self.name)) out.write('\n') @@ -679,7 +701,10 @@ class CppExampleComponent(ExampleComponent): out.write('%s.lib' % dll_name) else: out.write(dll) - out.write(' $(LINK_EXTRA_FLAGS)\n') + extra_flags = '' + if OMP and not WINDOWS: + extra_flags = '-fopenmp' + out.write(' $(LINK_EXTRA_FLAGS) %s\n' % extra_flags) out.write('_ex_%s: %s\n\n' % (self.name, exefile)) class CExampleComponent(CppExampleComponent): diff --git a/src/test/polynomial.cpp b/src/test/polynomial.cpp index beb53c0fc..b51d14645 100644 --- a/src/test/polynomial.cpp +++ b/src/test/polynomial.cpp @@ -16,6 +16,7 @@ Author: Notes: --*/ +#if !defined(__clang__) #include"polynomial.h" #include"polynomial_factorization.h" #include"polynomial_var2value.h" @@ -1851,3 +1852,8 @@ void tst_polynomial() { tst1(); tst4(); } +#else +void tst_polynomial() { + // it takes forever to compiler these regressions using clang++ +} +#endif diff --git a/src/util/object_allocator.h b/src/util/object_allocator.h index 96e705da7..db8a149c1 100644 --- a/src/util/object_allocator.h +++ b/src/util/object_allocator.h @@ -140,7 +140,7 @@ class object_allocator : public ResetProc { free_list.pop_back(); return r; } - return m_regions[idx]->allocate(); + return m_regions[idx]->template allocate(); } void recycle_core(unsigned idx, T * ptr) {