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

improving clang++ support

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-13 21:26:28 -08:00
parent 3e8d3db290
commit ad3aa96726
7 changed files with 33 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

2
README
View file

@ -40,7 +40,7 @@ Remark: clang does not support OpenMP yet.
autoconf autoconf
./configure CXX=clang++ ./configure CXX=clang++
python scripts/mk_make.py --noomp python scripts/mk_make.py
cd build cd build
make make

47
configure.ac
View file

@ -83,7 +83,7 @@ fi
################### ###################
# Sets CXX # Sets CXX
AC_LANG([C++]) AC_LANG([C++])
AC_PROG_CXX(g++ false) AC_PROG_CXX(g++ clang++ false)
AC_PROG_CC AC_PROG_CC
if test $CXX = "false"; then if test $CXX = "false"; then
AC_MSG_ERROR([C++ compiler was not found]) AC_MSG_ERROR([C++ compiler was not found])
@ -99,8 +99,21 @@ AC_PROG_GREP
# Sets SED # Sets SED
AC_PROG_SED AC_PROG_SED
# Sets OPENMP_CFLAGS AS_IF([test "$CXX" = "g++"], [
m4_ifdef([AC_OPENMP], [AC_OPENMP]) # Enable OpenMP
CXXFLAGS+=" -fopenmp"
LDFLAGS+=" -fopenmp"
SLIBEXTRAFLAGS+=" -fopenmp"
# Use -mfpmath=sse
CXXFLAGS+=" -mfpmath=sse"
],
[test "$CXX" = "clang++"], [
# OpenMP is not supported in clang++
CXXFLAGS+=" -D _NO_OMP_"
],
[
AC_MSG_ERROR([Unsupported compiler: $CXX])
])
AR=ar AR=ar
AC_SUBST(AR) AC_SUBST(AR)
@ -115,30 +128,25 @@ host_os=`uname -s`
AS_IF([test "$host_os" = "Darwin"], [ AS_IF([test "$host_os" = "Darwin"], [
PLATFORM=osx PLATFORM=osx
SO_EXT=.dylib SO_EXT=.dylib
LDFLAGS= SLIBFLAGS+="-dynamiclib"
SLIBFLAGS="-dynamiclib"
SLIBEXTRAFLAGS=""
COMP_VERSIONS="-compatibility_version \$(Z3_VERSION) -current_version \$(Z3_VERSION)" COMP_VERSIONS="-compatibility_version \$(Z3_VERSION) -current_version \$(Z3_VERSION)"
STATIC_FLAGS= STATIC_FLAGS=
], [test "$host_os" = "Linux"], [ ], [test "$host_os" = "Linux"], [
PLATFORM=linux PLATFORM=linux
SO_EXT=.so SO_EXT=.so
LDFLAGS=-lrt SLIBFLAGS+="-shared"
SLIBFLAGS="-shared"
SLIBEXTRAFLAGS=
COMP_VERSIONS= COMP_VERSIONS=
STATIC_FLAGS=-static STATIC_FLAGS=-static
CXXFLAGS+=" -fno-strict-aliasing" CXXFLAGS+=" -fno-strict-aliasing"
if test "$CXX" = "clang++"; then if test "$CXX" = "clang++"; then
# More flags for clang++ for Linux
CXXFLAGS+=" -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value" CXXFLAGS+=" -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value"
SLIBEXTRAFLAGS+=" -lrt"
fi fi
SLIBEXTRAFLAGS+=" -lrt"
], [test "${host_os:0:6}" = "CYGWIN"], [ ], [test "${host_os:0:6}" = "CYGWIN"], [
PLATFORM=win PLATFORM=win
SO_EXT=.dll SO_EXT=.dll
LDFLAGS= SLIBFLAGS+="-shared"
SLIBFLAGS="-shared"
SLIBEXTRAFLAGS=
COMP_VERSIONS= COMP_VERSIONS=
CXXFLAGS+=" -D_CYGWIN -fno-strict-aliasing" CXXFLAGS+=" -D_CYGWIN -fno-strict-aliasing"
], ],
@ -146,11 +154,6 @@ AS_IF([test "$host_os" = "Darwin"], [
AC_MSG_ERROR([Unknown host platform: $host_os]) 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(SLIBFLAGS)
AC_SUBST(LDFLAGS) AC_SUBST(LDFLAGS)
AC_SUBST(SLIBEXTRAFLAGS) AC_SUBST(SLIBEXTRAFLAGS)
@ -189,22 +192,18 @@ AC_OUTPUT(scripts/config-debug.mk scripts/config-release.mk)
# #
################### ###################
MKMAKE_OPT=
if test "$CXX" = "clang++"; then
MKMAKE_OPT="--noomp"
fi
# Python is available, give user the option to generate the make files wherever they want # Python is available, give user the option to generate the make files wherever they want
cat <<EOF cat <<EOF
Z3 was configured with success. Z3 was configured with success.
Host platform: $PLATFORM Host platform: $PLATFORM
Compiler: $CXX
Arithmetic: $ARITH Arithmetic: $ARITH
Python: $PYTHON Python: $PYTHON
Prefix: $prefix Prefix: $prefix
64-bit: $IS_X64 64-bit: $IS_X64
To build and install Z3, execute: To build and install Z3, execute:
python scripts/mk_make.py $MKMAKE_OPT python scripts/mk_make.py
cd build cd build
make make
sudo make install sudo make install

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

@ -1,6 +1,6 @@
CC=cl CC=cl
CXX=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 /Gd /analyze- CXXFLAGS=/c /Zi /nologo /openmp /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 CXX_OUT_FLAG=/Fo
OBJ_EXT=.obj OBJ_EXT=.obj
LIB_EXT=.lib LIB_EXT=.lib

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

@ -1,6 +1,6 @@
CC=cl CC=cl
CXX=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 /Gd /analyze- /arch:SSE2 CXXFLAGS=/c /Zi /nologo /openmp /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 CXX_OUT_FLAG=/Fo
OBJ_EXT=.obj OBJ_EXT=.obj
LIB_EXT=.lib LIB_EXT=.lib

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

@ -1,6 +1,6 @@
CC=cl CC=cl
CXX=cl CXX=cl
CXXFLAGS=/c /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP
CXX_OUT_FLAG=/Fo CXX_OUT_FLAG=/Fo
OBJ_EXT=.obj OBJ_EXT=.obj
LIB_EXT=.lib LIB_EXT=.lib

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

@ -1,6 +1,6 @@
CC=cl CC=cl
CXX=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 /Gd /analyze- /arch:SSE2 CXXFLAGS=/nologo /c /Zi /openmp /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 CXX_OUT_FLAG=/Fo
OBJ_EXT=.obj OBJ_EXT=.obj
LIB_EXT=.lib LIB_EXT=.lib

35
scripts/mk_util.py
View file

@ -40,7 +40,6 @@ Z3PY_SRC_DIR=None
VS_PROJ = False VS_PROJ = False
TRACE = False TRACE = False
DOTNET_ENABLED=False DOTNET_ENABLED=False
OMP = True
VER_MAJOR=None VER_MAJOR=None
VER_MINOR=None VER_MINOR=None
@ -121,12 +120,11 @@ def display_help():
print " -v, --vsproj generate Visual Studio Project Files." print " -v, --vsproj generate Visual Studio Project Files."
print " -t, --trace enable tracing in release mode." print " -t, --trace enable tracing in release mode."
print " -n, --nodotnet do not generate Microsoft.Z3.dll make rules." print " -n, --nodotnet do not generate Microsoft.Z3.dll make rules."
print " --noomp disable support for openmp."
exit(0) exit(0)
# Parse configuration option for mk_make script # Parse configuration option for mk_make script
def parse_options(): def parse_options():
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, DOTNET_ENABLED, OMP global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, DOTNET_ENABLED
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:dsxhmcvtn', ['build=', options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:dsxhmcvtn', ['build=',
'debug', 'debug',
'silent', 'silent',
@ -136,8 +134,7 @@ def parse_options():
'showcpp', 'showcpp',
'vsproj', 'vsproj',
'trace', 'trace',
'nodotnet', 'nodotnet'
'noomp'
]) ])
for opt, arg in options: for opt, arg in options:
if opt in ('-b', '--build'): if opt in ('-b', '--build'):
@ -164,8 +161,6 @@ def parse_options():
TRACE = True TRACE = True
elif opt in ('-n', '--nodotnet'): elif opt in ('-n', '--nodotnet'):
DOTNET_ENABLED = False DOTNET_ENABLED = False
elif opt in ('--noomp'):
OMP = False
else: else:
raise MKException("Invalid command line option '%s'" % opt) raise MKException("Invalid command line option '%s'" % opt)
@ -347,17 +342,6 @@ class Component:
extra_opt = '/D _TRACE' extra_opt = '/D _TRACE'
else: else:
extra_opt = '-D _TRACE' extra_opt = '-D _TRACE'
if not OMP:
if IS_WINDOWS:
extra_opt = '%s /D _NO_OMP_' % extra_opt
else:
extra_opt = '%s -D _NO_OMP_' % extra_opt
else:
if IS_WINDOWS:
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)) out.write('\t@$(CXX) $(CXXFLAGS) %s $(%s) $(CXX_OUT_FLAG)%s %s\n' % (extra_opt, include_defs, objfile, srcfile))
def mk_makefile(self, out): def mk_makefile(self, out):
@ -492,10 +476,7 @@ class ExeComponent(Component):
for dep in deps: for dep in deps:
c_dep = get_component(dep) c_dep = get_component(dep)
out.write(' %s/%s$(LIB_EXT)' % (c_dep.build_dir, c_dep.name)) out.write(' %s/%s$(LIB_EXT)' % (c_dep.build_dir, c_dep.name))
extra_flags = '' out.write(' $(LINK_EXTRA_FLAGS)\n')
if OMP and not IS_WINDOWS:
extra_flags = '-fopenmp'
out.write(' $(LINK_EXTRA_FLAGS) %s\n' % extra_flags)
out.write('%s: %s\n\n' % (self.name, exefile)) out.write('%s: %s\n\n' % (self.name, exefile))
def require_install_tactics(self): def require_install_tactics(self):
@ -571,10 +552,7 @@ class DLLComponent(Component):
if not dep in self.reexports: if not dep in self.reexports:
c_dep = get_component(dep) c_dep = get_component(dep)
out.write(' %s/%s$(LIB_EXT)' % (c_dep.build_dir, c_dep.name)) out.write(' %s/%s$(LIB_EXT)' % (c_dep.build_dir, c_dep.name))
extra_flags= '' out.write(' $(SLINK_EXTRA_FLAGS)')
if OMP and not IS_WINDOWS:
extra_flags = '-fopenmp'
out.write(' $(SLINK_EXTRA_FLAGS) %s' % extra_flags)
if IS_WINDOWS: if IS_WINDOWS:
out.write(' /DEF:%s/%s.def' % (self.to_src_dir, self.name)) out.write(' /DEF:%s/%s.def' % (self.to_src_dir, self.name))
out.write('\n') out.write('\n')
@ -701,10 +679,7 @@ class CppExampleComponent(ExampleComponent):
out.write('%s.lib' % dll_name) out.write('%s.lib' % dll_name)
else: else:
out.write(dll) out.write(dll)
extra_flags = '' out.write(' $(LINK_EXTRA_FLAGS)\n')
if OMP and not IS_WINDOWS:
extra_flags = '-fopenmp'
out.write(' $(LINK_EXTRA_FLAGS) %s\n' % extra_flags)
out.write('_ex_%s: %s\n\n' % (self.name, exefile)) out.write('_ex_%s: %s\n\n' % (self.name, exefile))
class CExampleComponent(CppExampleComponent): class CExampleComponent(CppExampleComponent):