diff --git a/scripts/mk_util.py b/scripts/mk_util.py index a02a9b40f..36f7b5ce3 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -82,6 +82,7 @@ JAVA_ENABLED=False ML_ENABLED=False PYTHON_INSTALL_ENABLED=False STATIC_LIB=False +STATIC_BIN=False VER_MAJOR=None VER_MINOR=None VER_BUILD=None @@ -532,6 +533,9 @@ def get_version(): def build_static_lib(): return STATIC_LIB +def build_static_bin(): + return STATIC_BIN + def is_cr_lf(fname): # Check whether text files use cr/lf f = open(fname, 'r') @@ -616,6 +620,7 @@ def display_help(exit_code): print(" --ml generate OCaml bindings.") print(" --python generate Python bindings.") print(" --staticlib build Z3 static library.") + print(" --staticbin build a statically linked Z3 binary.") if not IS_WINDOWS: print(" -g, --gmp use GMP.") print(" --gprof enable gprof") @@ -646,14 +651,14 @@ def display_help(exit_code): # Parse configuration option for mk_make script def parse_options(): 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 try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', '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: print("ERROR: Invalid command line option") display_help(1) @@ -688,6 +693,8 @@ def parse_options(): DOTNET_ENABLED = True elif opt in ('--staticlib'): STATIC_LIB = True + elif opt in ('--staticbin'): + STATIC_BIN = True elif opt in ('--optimize'): SLOW_OPTIMIZE = True elif not IS_WINDOWS and opt in ('-p', '--prefix'): @@ -2189,14 +2196,19 @@ def mk_config(): extra_opt = ' -D_NO_OMP_' if 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: + static_opt = static_opt + 'd' config.write( 'AR_FLAGS=/nologo\n' - 'LINK_FLAGS=/nologo /MDd\n' - 'SLINK_FLAGS=/nologo /LDd\n') + 'LINK_FLAGS=/nologo %s\n' + '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 %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( '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') @@ -2205,7 +2217,7 @@ def mk_config(): exit(1) else: 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( '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') @@ -2214,15 +2226,14 @@ def mk_config(): LTCG=' /LTCG' if SLOW_OPTIMIZE else '' GL = ' /GL' if SLOW_OPTIMIZE else '' config.write( - 'AR_FLAGS=/nologo%s\n' - 'LINK_FLAGS=/nologo /MD\n' - 'SLINK_FLAGS=/nologo /LD\n' - % LTCG) + 'AR_FLAGS=/nologo %s\n' + 'LINK_FLAGS=/nologo %s\n' + 'SLINK_FLAGS=/nologo /LD\n' % (LTCG, static_opt)) if TRACE: 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 %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( '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)) @@ -2231,7 +2242,7 @@ def mk_config(): exit(1) else: 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( '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)) @@ -2356,7 +2367,10 @@ def mk_config(): config.write('AR_OUTFLAG=\n') config.write('EXE_EXT=\n') 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_EXTRA_FLAGS=-lpthread %s\n' % LDFLAGS) config.write('SO_EXT=%s\n' % SO_EXT)