From 5790115e40fa54aa937e1d021a40eacfaff801fe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 13 Feb 2013 08:39:26 -0800
Subject: [PATCH] Include git hash in the binary

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 scripts/mk_util.py     | 23 +++++++++++++++++------
 scripts/mk_win_dist.py |  2 ++
 src/shell/main.cpp     |  9 +++++++--
 3 files changed, 26 insertions(+), 8 deletions(-)

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 <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("  -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";