mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

Added support for clang++ on OSX

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-12 04:56:48 +00:00
parent 99b7f7509d
commit e0fcbc101c
10 changed files with 68 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

11
README
View file

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

12
configure.ac
View file

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

4
scripts/config-debug.mk.in
View file

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

4
scripts/config-release.mk.in
View file

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

2
scripts/config-vs-debug-x64.mk
View file

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

2
scripts/config-vs-debug.mk
View file

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

2
scripts/config-vs-release.mk
View file

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

43
scripts/mk_util.py
View file

@ -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):

6
src/test/polynomial.cpp
View file

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

2
src/util/object_allocator.h
View file

@ -140,7 +140,7 @@ class object_allocator : public ResetProc {
free_list.pop_back();
return r;
}
return m_regions[idx]->allocate<construct>();
return m_regions[idx]->template allocate<construct>();
}
void recycle_core(unsigned idx, T * ptr) {