Give KLEE release version information in the output of klee and kleaver

when they are given the --version command line option.

Unfortunately to make the build type and git revision available we
need to check this for every build which means KLEE's support library
will be rebuilt for every build which will slow down incremental builds.

This addresses issue #231

10 files changed, 102 insertions, 57 deletions

diff --git a/Makefile.config.in b/Makefile.config.in
index 098b68fb..5b9f929c 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -1,8 +1,8 @@
 # -*- Makefile -*-
 
 # Set the name of the project here
-PROJECT_NAME := klee
-PROJ_VERSION := 0.01
+PROJECT_NAME := @PACKAGE_NAME@
+PROJ_VERSION := @PACKAGE_VERSION@
 
 # Set this variable to the top of the LLVM source tree.
 LLVM_SRC_ROOT = @LLVM_SRC@
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 747f6544..ae497b48 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -1,7 +1,7 @@
 dnl **************************************************************************
 dnl * Initialize
 dnl **************************************************************************
-AC_INIT([[KLEE]],[[0.01]],[daniel@minormatter.com])
+AC_INIT([[KLEE]],[[0.2.0]],[[klee-dev@imperial.ac.uk]],[[klee-]],[[https://klee.github.io]])
 
 dnl Identify where LLVM source tree is (this is patched by
 dnl AutoRegen.sh)
diff --git a/configure b/configure
index e4f8ffb6..9e524f41 100755
--- a/configure
+++ b/configure
@@ -1,8 +1,8 @@
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
-# Generated by GNU Autoconf 2.69 for KLEE 0.01.
+# Generated by GNU Autoconf 2.69 for KLEE 0.2.0.
 #
-# Report bugs to <daniel@minormatter.com>.
+# Report bugs to <klee-dev@imperial.ac.uk>.
 #
 #
 # Copyright (C) 1992-1996, 1998-2012 Free Software Foundation, Inc.
@@ -267,10 +267,10 @@ fi
     $as_echo "$0: be upgraded to zsh 4.3.4 or later."
   else
     $as_echo "$0: Please tell bug-autoconf@gnu.org and
-$0: daniel@minormatter.com about your system, including any
-$0: error possibly output before this message. Then install
-$0: a modern shell, or manually run the script under such a
-$0: shell if you do have one."
+$0: [klee-dev@imperial.ac.uk] about your system, including
+$0: any error possibly output before this message. Then
+$0: install a modern shell, or manually run the script
+$0: under such a shell if you do have one."
   fi
   exit 1
 fi
@@ -579,11 +579,11 @@ MAKEFLAGS=
 
 # Identity of this package.
 PACKAGE_NAME='KLEE'
-PACKAGE_TARNAME='-klee-'
-PACKAGE_VERSION='0.01'
-PACKAGE_STRING='KLEE 0.01'
-PACKAGE_BUGREPORT='daniel@minormatter.com'
-PACKAGE_URL=''
+PACKAGE_TARNAME='klee-'
+PACKAGE_VERSION='0.2.0'
+PACKAGE_STRING='KLEE 0.2.0'
+PACKAGE_BUGREPORT='klee-dev@imperial.ac.uk'
+PACKAGE_URL='https://klee.github.io'
 
 ac_unique_file=""Makefile.config.in""
 # Factoring default headers for most tests.
@@ -1285,7 +1285,7 @@ if test "$ac_init_help" = "long"; then
   # Omit some internal or obsolete options to make the list less imposing.
   # This message is too long to be a string in the A/UX 3.1 sh.
   cat <<_ACEOF
-\`configure' configures KLEE 0.01 to adapt to many kinds of systems.
+\`configure' configures KLEE 0.2.0 to adapt to many kinds of systems.
 
 Usage: $0 [OPTION]... [VAR=VALUE]...
 
@@ -1333,7 +1333,7 @@ Fine tuning of the installation directories:
   --infodir=DIR           info documentation [DATAROOTDIR/info]
   --localedir=DIR         locale-dependent data [DATAROOTDIR/locale]
   --mandir=DIR            man documentation [DATAROOTDIR/man]
-  --docdir=DIR            documentation root [DATAROOTDIR/doc/-klee-]
+  --docdir=DIR            documentation root [DATAROOTDIR/doc/klee-]
   --htmldir=DIR           html documentation [DOCDIR]
   --dvidir=DIR            dvi documentation [DOCDIR]
   --pdfdir=DIR            pdf documentation [DOCDIR]
@@ -1351,7 +1351,7 @@ fi
 
 if test -n "$ac_init_help"; then
   case $ac_init_help in
-     short | recursive ) echo "Configuration of KLEE 0.01:";;
+     short | recursive ) echo "Configuration of KLEE 0.2.0:";;
    esac
   cat <<\_ACEOF
 
@@ -1399,7 +1399,8 @@ Some influential environment variables:
 Use these variables to override the choices made by `configure' or to help
 it to find libraries and programs with nonstandard names/locations.
 
-Report bugs to <daniel@minormatter.com>.
+Report bugs to <klee-dev@imperial.ac.uk>.
+KLEE home page: <https://klee.github.io>.
 _ACEOF
 ac_status=$?
 fi
@@ -1462,7 +1463,7 @@ fi
 test -n "$ac_init_help" && exit $ac_status
 if $ac_init_version; then
   cat <<\_ACEOF
-KLEE configure 0.01
+KLEE configure 0.2.0
 generated by GNU Autoconf 2.69
 
 Copyright (C) 2012 Free Software Foundation, Inc.
@@ -1705,9 +1706,9 @@ $as_echo "$as_me: WARNING: $2: see the Autoconf documentation" >&2;}
 $as_echo "$as_me: WARNING: $2:     section \"Present But Cannot Be Compiled\"" >&2;}
     { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: $2: proceeding with the compiler's result" >&5
 $as_echo "$as_me: WARNING: $2: proceeding with the compiler's result" >&2;}
-( $as_echo "## ------------------------------------- ##
-## Report this to daniel@minormatter.com ##
-## ------------------------------------- ##"
+( $as_echo "## -------------------------------------- ##
+## Report this to klee-dev@imperial.ac.uk ##
+## -------------------------------------- ##"
      ) | sed "s/^/$as_me: WARNING:     /" >&2
     ;;
 esac
@@ -1952,9 +1953,9 @@ $as_echo "$as_me: WARNING: $2: see the Autoconf documentation" >&2;}
 $as_echo "$as_me: WARNING: $2:     section \"Present But Cannot Be Compiled\"" >&2;}
     { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: $2: proceeding with the compiler's result" >&5
 $as_echo "$as_me: WARNING: $2: proceeding with the compiler's result" >&2;}
-( $as_echo "## ------------------------------------- ##
-## Report this to daniel@minormatter.com ##
-## ------------------------------------- ##"
+( $as_echo "## -------------------------------------- ##
+## Report this to klee-dev@imperial.ac.uk ##
+## -------------------------------------- ##"
      ) | sed "s/^/$as_me: WARNING:     /" >&2
     ;;
 esac
@@ -2043,7 +2044,7 @@ cat >config.log <<_ACEOF
 This file contains any messages produced by compilers while
 running configure, to aid debugging if configure makes a mistake.
 
-It was created by KLEE $as_me 0.01, which was
+It was created by KLEE $as_me 0.2.0, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   $ $0 $@
@@ -5618,7 +5619,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1
 # report actual input values of CONFIG_FILES etc. instead of their
 # values after options handling.
 ac_log="
-This file was extended by KLEE $as_me 0.01, which was
+This file was extended by KLEE $as_me 0.2.0, which was
 generated by GNU Autoconf 2.69.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES
@@ -5678,13 +5679,14 @@ $config_headers
 Configuration commands:
 $config_commands
 
-Report bugs to <daniel@minormatter.com>."
+Report bugs to <klee-dev@imperial.ac.uk>.
+KLEE home page: <https://klee.github.io>."
 
 _ACEOF
 cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
 ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`"
 ac_cs_version="\\
-KLEE config.status 0.01
+KLEE config.status 0.2.0
 configured by $0, generated by GNU Autoconf 2.69,
   with options \\"\$ac_cs_config\\"
 
diff --git a/include/klee/Internal/Support/PrintVersion.h b/include/klee/Internal/Support/PrintVersion.h
new file mode 100644
index 00000000..2c375ad2
--- /dev/null
+++ b/include/klee/Internal/Support/PrintVersion.h
@@ -0,0 +1,17 @@
+//===-- Version.h -----------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_PRINT_VERSION_H
+#define KLEE_PRINT_VERSION_H
+
+namespace klee {
+  void printVersion();
+}
+
+#endif
diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
index 5f9f8dc6..ecc9912e 100644
--- a/lib/Core/ExternalDispatcher.cpp
+++ b/lib/Core/ExternalDispatcher.cpp
@@ -10,13 +10,6 @@
 #include "ExternalDispatcher.h"
 #include "klee/Config/Version.h"
 
-// Ugh.
-#undef PACKAGE_BUGREPORT
-#undef PACKAGE_NAME
-#undef PACKAGE_STRING
-#undef PACKAGE_TARNAME
-#undef PACKAGE_VERSION
-
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
 #include "llvm/IR/Module.h"
 #include "llvm/IR/Constants.h"
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 0e564fe5..cf8a1654 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -27,13 +27,6 @@
 #include "UserSearcher.h"
 #include "../Solver/SolverStats.h"
 
-// FIXME: Ugh, this is gross. But otherwise our config.h conflicts with LLVMs.
-#undef PACKAGE_BUGREPORT
-#undef PACKAGE_NAME
-#undef PACKAGE_STRING
-#undef PACKAGE_TARNAME
-#undef PACKAGE_VERSION
-
 #if LLVM_VERSION_CODE > LLVM_VERSION(3, 2)
 #include "llvm/IR/BasicBlock.h"
 #include "llvm/IR/Function.h"
diff --git a/lib/Support/Makefile b/lib/Support/Makefile
index 67272908..ff28b06e 100644
--- a/lib/Support/Makefile
+++ b/lib/Support/Makefile
@@ -14,4 +14,23 @@ DONT_BUILD_RELINKED=1
 BUILD_ARCHIVE=1
 NO_INSTALL=1
 
+# FIXME: This is nasty. We don't want to rebuild this library everytime
+# but this was the only way I could find to make the build work.
+#
+# Note this rule has to go here so it is run first.
+CompileTimeInfoFile:=../../include/klee/Config/CompileTimeInfo.h
+all-local:: $(CompileTimeInfoFile)
+
 include $(LEVEL)/Makefile.common
+
+
+GIT_PRESENT:=$(shell [ -d "$(PROJ_SRC_ROOT)/.git" ] && echo 1 || echo 0)
+
+.PHONY: $(CompileTimeInfoFile)
+$(CompileTimeInfoFile):
+	$(Verb) echo "Regenerating $(CompileTimeInfoFile)"
+	$(Verb) echo '#define KLEE_BUILD_MODE "$(BuildMode)"' > $(CompileTimeInfoFile)
+ifeq ($(GIT_PRESENT),1)
+	$(Verb) echo '#define KLEE_BUILD_REVISION "'$(shell cd $(PROJ_SRC_ROOT); git rev-parse HEAD)'"' >> \
+	$(CompileTimeInfoFile)
+endif
diff --git a/lib/Support/PrintVersion.cpp b/lib/Support/PrintVersion.cpp
new file mode 100644
index 00000000..d62269ba
--- /dev/null
+++ b/lib/Support/PrintVersion.cpp
@@ -0,0 +1,31 @@
+//===-- PrintVersion.cpp --------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/Internal/Support/PrintVersion.h"
+#include "klee/Config/config.h"
+#include "llvm/Support/raw_ostream.h"
+#include "llvm/Support/CommandLine.h"
+
+#include "klee/Config/CompileTimeInfo.h"
+
+void klee::printVersion()
+{
+  llvm::outs() << PACKAGE_STRING " (" PACKAGE_URL ")\n";
+  llvm::outs() << "  Built " __DATE__ " (" __TIME__ ")\n";
+  llvm::outs() << "  Build mode: " << KLEE_BUILD_MODE "\n";
+  llvm::outs() << "  Build revision: ";
+#ifdef KLEE_BUILD_REVISION
+  llvm::outs() << KLEE_BUILD_REVISION "\n";
+#else
+  llvm::outs() << "unknown\n";
+#endif
+  // Show LLVM version information
+  llvm::outs() << "\n";
+  llvm::cl::PrintVersionMessage();
+}
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index fafe955f..af337abe 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -12,8 +12,8 @@
 #include "klee/Common.h"
 #include "klee/util/ExprPPrinter.h"
 #include "klee/util/ExprVisitor.h"
-
 #include "klee/util/ExprSMTLIBPrinter.h"
+#include "klee/Internal/Support/PrintVersion.h"
 
 #include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/CommandLine.h"
@@ -24,12 +24,6 @@
 #include <sys/stat.h>
 #include <unistd.h>
 
-// FIXME: Ugh, this is gross. But otherwise our config.h conflicts with LLVMs.
-#undef PACKAGE_BUGREPORT
-#undef PACKAGE_NAME
-#undef PACKAGE_STRING
-#undef PACKAGE_TARNAME
-#undef PACKAGE_VERSION
 
 #include "llvm/Support/Signals.h"
 
@@ -451,6 +445,7 @@ int main(int argc, char **argv) {
   bool success = true;
 
   llvm::sys::PrintStackTraceOnErrorSignal();
+  llvm::cl::SetVersionPrinter(klee::printVersion);
   llvm::cl::ParseCommandLineOptions(argc, argv);
 
   std::string ErrorStr;
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 2cb9537b..97192183 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -13,13 +13,7 @@
 #include "klee/Internal/Support/Debug.h"
 #include "klee/Internal/Support/ModuleUtil.h"
 #include "klee/Internal/System/Time.h"
-
-// FIXME: Ugh, this is gross. But otherwise our config.h conflicts with LLVMs.
-#undef PACKAGE_BUGREPORT
-#undef PACKAGE_NAME
-#undef PACKAGE_STRING
-#undef PACKAGE_TARNAME
-#undef PACKAGE_VERSION
+#include "klee/Internal/Support/PrintVersion.h"
 
 #if LLVM_VERSION_CODE > LLVM_VERSION(3, 2)
 #include "llvm/IR/Constants.h"
@@ -630,6 +624,7 @@ static std::string strip(std::string &in) {
 }
 
 static void parseArguments(int argc, char **argv) {
+  cl::SetVersionPrinter(klee::printVersion);
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 2)
   // This version always reads response files
   cl::ParseCommandLineOptions(argc, argv, " klee\n");