mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-09 07:33:24 +00:00
Code Activity

Added --staticbin option.

Browse source 
Relates to #456
This commit is contained in:
Christoph M. Wintersteiger 2016-03-04 18:32:45 +00:00
parent cf5910e041
commit 40c5152075
1 changed files with 27 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

40
scripts/mk_util.py
View file

@ -82,6 +82,7 @@ JAVA_ENABLED=False
ML_ENABLED=False ML_ENABLED=False
PYTHON_INSTALL_ENABLED=False PYTHON_INSTALL_ENABLED=False
STATIC_LIB=False STATIC_LIB=False
STATIC_BIN=False
VER_MAJOR=None VER_MAJOR=None
VER_MINOR=None VER_MINOR=None
VER_BUILD=None VER_BUILD=None
@ -532,6 +533,9 @@ def get_version():
def build_static_lib(): def build_static_lib():
return STATIC_LIB return STATIC_LIB
def build_static_bin():
return STATIC_BIN
def is_cr_lf(fname): def is_cr_lf(fname):
# Check whether text files use cr/lf # Check whether text files use cr/lf
f = open(fname, 'r') f = open(fname, 'r')
@ -616,6 +620,7 @@ def display_help(exit_code):
print(" --ml generate OCaml bindings.") print(" --ml generate OCaml bindings.")
print(" --python generate Python bindings.") print(" --python generate Python bindings.")
print(" --staticlib build Z3 static library.") print(" --staticlib build Z3 static library.")
print(" --staticbin build a statically linked Z3 binary.")
if not IS_WINDOWS: if not IS_WINDOWS:
print(" -g, --gmp use GMP.") print(" -g, --gmp use GMP.")
print(" --gprof enable gprof") print(" --gprof enable gprof")
@ -646,14 +651,14 @@ def display_help(exit_code):
# 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, VS_PAR, VS_PAR_NUM global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, PYTHON_INSTALL_ENABLED global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, PYTHON_INSTALL_ENABLED
global LINUX_X64, SLOW_OPTIMIZE, USE_OMP global LINUX_X64, SLOW_OPTIMIZE, USE_OMP
try: try:
options, remainder = getopt.gnu_getopt(sys.argv[1:], options, remainder = getopt.gnu_getopt(sys.argv[1:],
'b:df:sxhmcvtnp:gj', 'b:df:sxhmcvtnp:gj',
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
'trace', 'dotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof', 'trace', 'dotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python']) 'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin'])
except: except:
print("ERROR: Invalid command line option") print("ERROR: Invalid command line option")
display_help(1) display_help(1)
@ -688,6 +693,8 @@ def parse_options():
DOTNET_ENABLED = True DOTNET_ENABLED = True
elif opt in ('--staticlib'): elif opt in ('--staticlib'):
STATIC_LIB = True STATIC_LIB = True
elif opt in ('--staticbin'):
STATIC_BIN = True
elif opt in ('--optimize'): elif opt in ('--optimize'):
SLOW_OPTIMIZE = True SLOW_OPTIMIZE = True
elif not IS_WINDOWS and opt in ('-p', '--prefix'): elif not IS_WINDOWS and opt in ('-p', '--prefix'):
@ -2189,14 +2196,19 @@ def mk_config():
extra_opt = ' -D_NO_OMP_' extra_opt = ' -D_NO_OMP_'
if GIT_HASH: if GIT_HASH:
extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH)
if STATIC_BIN:
static_opt = '/MT'
else:
static_opt = '/MD'
if DEBUG_MODE: if DEBUG_MODE:
static_opt = static_opt + 'd'
config.write( config.write(
'AR_FLAGS=/nologo\n' 'AR_FLAGS=/nologo\n'
'LINK_FLAGS=/nologo /MDd\n' 'LINK_FLAGS=/nologo %s\n'
'SLINK_FLAGS=/nologo /LDd\n') 'SLINK_FLAGS=/nologo /LDd\n' % static_opt)
if VS_X64: if VS_X64:
config.write( config.write(
'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt) 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt)
config.write( config.write(
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
@ -2205,7 +2217,7 @@ def mk_config():
exit(1) exit(1)
else: else:
config.write( config.write(
'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt) 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt)
config.write( config.write(
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
@ -2214,15 +2226,14 @@ def mk_config():
LTCG=' /LTCG' if SLOW_OPTIMIZE else '' LTCG=' /LTCG' if SLOW_OPTIMIZE else ''
GL = ' /GL' if SLOW_OPTIMIZE else '' GL = ' /GL' if SLOW_OPTIMIZE else ''
config.write( config.write(
'AR_FLAGS=/nologo%s\n' 'AR_FLAGS=/nologo %s\n'
'LINK_FLAGS=/nologo /MD\n' 'LINK_FLAGS=/nologo %s\n'
'SLINK_FLAGS=/nologo /LD\n' 'SLINK_FLAGS=/nologo /LD\n' % (LTCG, static_opt))
% LTCG)
if TRACE: if TRACE:
extra_opt = '%s /D _TRACE ' % extra_opt extra_opt = '%s /D _TRACE ' % extra_opt
if VS_X64: if VS_X64:
config.write( config.write(
'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % (GL, extra_opt)) 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % (GL, extra_opt))
config.write( config.write(
'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n' 'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n'
'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n' % (LTCG, LTCG)) 'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n' % (LTCG, LTCG))
@ -2231,7 +2242,7 @@ def mk_config():
exit(1) exit(1)
else: else:
config.write( config.write(
'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % (GL, extra_opt)) 'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % (GL, extra_opt))
config.write( config.write(
'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n' % (LTCG, LTCG)) 'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n' % (LTCG, LTCG))
@ -2356,7 +2367,10 @@ def mk_config():
config.write('AR_OUTFLAG=\n') config.write('AR_OUTFLAG=\n')
config.write('EXE_EXT=\n') config.write('EXE_EXT=\n')
config.write('LINK=%s\n' % CXX) config.write('LINK=%s\n' % CXX)
config.write('LINK_FLAGS=\n') if STATIC_BIN:
config.write('LINK_FLAGS=-static\n')
else:
config.write('LINK_FLAGS=\n')
config.write('LINK_OUT_FLAG=-o \n') config.write('LINK_OUT_FLAG=-o \n')
config.write('LINK_EXTRA_FLAGS=-lpthread %s\n' % LDFLAGS) config.write('LINK_EXTRA_FLAGS=-lpthread %s\n' % LDFLAGS)
config.write('SO_EXT=%s\n' % SO_EXT) config.write('SO_EXT=%s\n' % SO_EXT)