diff --git a/scripts/mk_util.py b/scripts/mk_util.py index b3d843cc4..589fc1013 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -73,6 +73,7 @@ GMP=False VS_PAR=False VS_PAR_NUM=8 GPROF=False +GIT_HASH=False def git_hash(): try: @@ -372,6 +373,7 @@ def display_help(exit_code): else: print(" --parallel=num use cl option /MP with 'num' parallel processes") print(" -b , --build= subdirectory where Z3 will be built (default: build).") + print(" --githash=hash include the given hash in the binaries.") print(" -d, --debug compile Z3 in debug mode.") print(" -t, --trace enable tracing in release mode.") if IS_WINDOWS: @@ -402,12 +404,13 @@ 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, STATIC_LIB, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF + global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:dsxhmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', - 'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof']) + 'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', + 'githash=']) except: print("ERROR: Invalid command line option") display_help(1) @@ -454,6 +457,8 @@ def parse_options(): JAVA_ENABLED = True elif opt == '--gprof': GPROF = True + elif opt == '--githash': + GIT_HASH=arg else: print("ERROR: Invalid command line option '%s'" % opt) display_help(1) @@ -1291,18 +1296,23 @@ def mk_config(): 'SO_EXT=.dll\n' 'SLINK=cl\n' 'SLINK_OUT_FLAG=/Fe\n') + extra_opt = '' + if GIT_HASH: + extra_opt = '%s /D Z3GITHASH="%s"' % (extra_opt, GIT_HASH) if DEBUG_MODE: config.write( 'LINK_FLAGS=/nologo /MDd\n' 'SLINK_FLAGS=/nologo /LDd\n') if not VS_X64: config.write( - '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\n' + 'CXXFLAGS=/c /Zi /nologo /openmp /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) + 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') else: config.write( - '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-\n' + 'CXXFLAGS=/c /Zi /nologo /openmp /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) + 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') else: @@ -1310,9 +1320,8 @@ def mk_config(): config.write( 'LINK_FLAGS=/nologo /MD\n' 'SLINK_FLAGS=/nologo /LD\n') - extra_opt = '' if TRACE: - extra_opt = '/D _TRACE' + extra_opt = '%s /D _TRACE' % extra_opt if not VS_X64: config.write( 'CXXFLAGS=/nologo /c /Zi /openmp /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' % extra_opt) @@ -1351,6 +1360,8 @@ def mk_config(): SLIBEXTRAFLAGS = '%s -lgmp' % SLIBEXTRAFLAGS else: CPPFLAGS = '%s -D_MP_INTERNAL' % CPPFLAGS + if GIT_HASH: + CPPFLAGS = '%s -DZ3GITHASH="%s"' % (CPPFLAGS, GIT_HASH) CXXFLAGS = '%s -c' % CXXFLAGS HAS_OMP = test_openmp(CXX) if HAS_OMP: diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 961425101..85c1dddfc 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -101,6 +101,8 @@ def mk_build_dir(path, x64): opts.append('--java') if x64: opts.append('-x') + if GIT_HASH: + opts.append('--githash=%s' % mk_util.git_hash()) if subprocess.call(opts) != 0: raise MKException("Failed to generate build directory at '%s'" % path) diff --git a/src/shell/main.cpp b/src/shell/main.cpp index d91038b39..7c69f66ba 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -51,13 +51,18 @@ void error(const char * msg) { } void display_usage() { - std::cout << "Z3 [version " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << " - "; + std::cout << "Z3 [version " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER; + std::cout << " - "; #ifdef _AMD64_ std::cout << "64"; #else std::cout << "32"; #endif - std::cout << " bit]. (C) Copyright 2006 Microsoft Corp.\n"; + std::cout << " bit"; +#ifdef Z3GITHASH + std::cout << " - build hashcode " << Z3GITHASH; +#endif + std::cout << "]. (C) Copyright 2006-2013 Microsoft Corp.\n"; std::cout << "Usage: z3 [options] [-file:]file\n"; std::cout << "\nInput format:\n"; std::cout << " -smt use parser for SMT input format.\n";