mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

Include git hash in the binary

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-02-13 08:39:26 -08:00
parent fa0bd4f789
commit 5790115e40
3 changed files with 26 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
scripts/mk_util.py
View file

@ -73,6 +73,7 @@ GMP=False
VS_PAR=False VS_PAR=False
VS_PAR_NUM=8 VS_PAR_NUM=8
GPROF=False GPROF=False
GIT_HASH=False
def git_hash(): def git_hash():
try: try:
@ -372,6 +373,7 @@ def display_help(exit_code):
else: else:
print(" --parallel=num use cl option /MP with 'num' parallel processes") print(" --parallel=num use cl option /MP with 'num' parallel processes")
print(" -b <sudir>, --build=<subdir> subdirectory where Z3 will be built (default: build).") print(" -b <sudir>, --build=<subdir> 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(" -d, --debug compile Z3 in debug mode.")
print(" -t, --trace enable tracing in release mode.") print(" -t, --trace enable tracing in release mode.")
if IS_WINDOWS: if IS_WINDOWS:
@ -402,12 +404,13 @@ 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, STATIC_LIB, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
try: try:
options, remainder = getopt.gnu_getopt(sys.argv[1:], options, remainder = getopt.gnu_getopt(sys.argv[1:],
'b:dsxhmcvtnp:gj', 'b:dsxhmcvtnp:gj',
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', ['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: except:
print("ERROR: Invalid command line option") print("ERROR: Invalid command line option")
display_help(1) display_help(1)
@ -454,6 +457,8 @@ def parse_options():
JAVA_ENABLED = True JAVA_ENABLED = True
elif opt == '--gprof': elif opt == '--gprof':
GPROF = True GPROF = True
elif opt == '--githash':
GIT_HASH=arg
else: else:
print("ERROR: Invalid command line option '%s'" % opt) print("ERROR: Invalid command line option '%s'" % opt)
display_help(1) display_help(1)
@ -1291,18 +1296,23 @@ def mk_config():
'SO_EXT=.dll\n' 'SO_EXT=.dll\n'
'SLINK=cl\n' 'SLINK=cl\n'
'SLINK_OUT_FLAG=/Fe\n') 'SLINK_OUT_FLAG=/Fe\n')
extra_opt = ''
if GIT_HASH:
extra_opt = '%s /D Z3GITHASH="%s"' % (extra_opt, GIT_HASH)
if DEBUG_MODE: if DEBUG_MODE:
config.write( config.write(
'LINK_FLAGS=/nologo /MDd\n' 'LINK_FLAGS=/nologo /MDd\n'
'SLINK_FLAGS=/nologo /LDd\n') 'SLINK_FLAGS=/nologo /LDd\n')
if not VS_X64: if not VS_X64:
config.write( 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' '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')
else: else:
config.write( 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' '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')
else: else:
@ -1310,9 +1320,8 @@ def mk_config():
config.write( config.write(
'LINK_FLAGS=/nologo /MD\n' 'LINK_FLAGS=/nologo /MD\n'
'SLINK_FLAGS=/nologo /LD\n') 'SLINK_FLAGS=/nologo /LD\n')
extra_opt = ''
if TRACE: if TRACE:
extra_opt = '/D _TRACE' extra_opt = '%s /D _TRACE' % extra_opt
if not VS_X64: if not VS_X64:
config.write( 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) '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 SLIBEXTRAFLAGS = '%s -lgmp' % SLIBEXTRAFLAGS
else: else:
CPPFLAGS = '%s -D_MP_INTERNAL' % CPPFLAGS CPPFLAGS = '%s -D_MP_INTERNAL' % CPPFLAGS
if GIT_HASH:
CPPFLAGS = '%s -DZ3GITHASH="%s"' % (CPPFLAGS, GIT_HASH)
CXXFLAGS = '%s -c' % CXXFLAGS CXXFLAGS = '%s -c' % CXXFLAGS
HAS_OMP = test_openmp(CXX) HAS_OMP = test_openmp(CXX)
if HAS_OMP: if HAS_OMP:

2
scripts/mk_win_dist.py
View file

@ -101,6 +101,8 @@ def mk_build_dir(path, x64):
opts.append('--java') opts.append('--java')
if x64: if x64:
opts.append('-x') opts.append('-x')
if GIT_HASH:
opts.append('--githash=%s' % mk_util.git_hash())
if subprocess.call(opts) != 0: if subprocess.call(opts) != 0:
raise MKException("Failed to generate build directory at '%s'" % path) raise MKException("Failed to generate build directory at '%s'" % path)

9
src/shell/main.cpp
View file

@ -51,13 +51,18 @@ void error(const char * msg) {
} }
void display_usage() { 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_ #ifdef _AMD64_
std::cout << "64"; std::cout << "64";
#else #else
std::cout << "32"; std::cout << "32";
#endif #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 << "Usage: z3 [options] [-file:]file\n";
std::cout << "\nInput format:\n"; std::cout << "\nInput format:\n";
std::cout << " -smt use parser for SMT input format.\n"; std::cout << " -smt use parser for SMT input format.\n";