EBMC: include git commit in version

To distinguish in-between release builds from releases, include the git
commit in the version output, using the same style as CBMC.

Author: kroening

src/Makefile

@@ -24,7 +24,7 @@ endif
 hw-cbmc.dir: trans-word-level.dir trans-netlist.dir verilog.dir \
          vhdl.dir smvlang.dir cprover.dir temporal-logic.dir
 
-vlindex.dir: cprover.dir verilog.dir
+vlindex.dir: ebmc.dir cprover.dir verilog.dir
 
 # building cbmc proper
 .PHONY: cprover.dir

src/config.inc

@@ -0,0 +1 @@
+EBMC_VERSION = 5.7

src/ebmc/Makefile

@@ -16,6 +16,7 @@ SRC = \
       ebmc_parse_options.cpp \
       ebmc_properties.cpp \
       ebmc_solver_factory.cpp \
+      ebmc_version.cpp \
       instrument_past.cpp \
       k_induction.cpp \
       liveness_to_safety.cpp \
@@ -69,12 +70,27 @@ endif
 include ../config.inc
 include ../common
 
+# get version from git
+GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a")
+RELEASE_INFO = const char *EBMC_VERSION="$(EBMC_VERSION) ($(GIT_INFO))";
+GIT_INFO_FILE = ebmc_version.cpp
+
+$(GIT_INFO_FILE):
+	echo '$(RELEASE_INFO)' > $@
+
+# mark the actually generated file as a phony target to enforce a rebuild - but
+# only if the version information has changed!
+KNOWN_RELEASE_INFO = $(shell cat $(GIT_INFO_FILE) 2>/dev/null)
+ifneq ($(RELEASE_INFO), $(KNOWN_RELEASE_INFO))
+.PHONY: $(GIT_INFO_FILE)
+endif
+
 ifneq ($(wildcard ../vhdl/Makefile),)
   OBJ += ../vhdl/vhdl$(LIBEXT)
   CXXFLAGS += -DHAVE_VHDL
 endif
 
-CLEANFILES = ebmc$(EXEEXT)
+CLEANFILES = $(GIT_INFO_FILE) ebmc$(EXEEXT)
 
 all: ebmc$(EXEEXT)
 

src/ebmc/ebmc_parse_options.cpp

@@ -344,13 +344,13 @@ Function: ebmc_parse_optionst::help
 
 void ebmc_parse_optionst::help()
 {
-  std::cout <<
-    "\n"
-    "* *      EBMC - Copyright (C) 2001-2017 Daniel Kroening     * *\n"
-    "* *                     Version " EBMC_VERSION "                         * *\n"
-    "* *     University of Oxford, Computer Science Department   * *\n"
-    "* *                  kroening@kroening.com                  * *\n"
-    "\n";
+  std::cout
+    << '\n'
+    << banner_string("EBMC", EBMC_VERSION) << '\n'
+    << "* *      EBMC - Copyright (C) 2001-2017 Daniel Kroening     * *\n"
+       "* *     University of Oxford, Computer Science Department   * *\n"
+       "* *                  kroening@kroening.com                  * *\n"
+       "\n";
 
   std::cout << help_formatter(
     // clang-format off

src/ebmc/ebmc_parse_options.h

@@ -55,7 +55,7 @@ class ebmc_parse_optionst:public parse_options_baset
         argc,
         argv,
         std::string("EBMC ") + EBMC_VERSION),
-      ui_message_handler(cmdline, "EBMC " EBMC_VERSION)
+      ui_message_handler(cmdline, std::string("EBMC ") + EBMC_VERSION)
   {
   }
 

src/ebmc/ebmc_solver_factory.cpp

@@ -92,7 +92,7 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline)
         auto dec = std::make_unique<smt2_convt>(
           ns,
           "ebmc",
-          "Generated by EBMC " EBMC_VERSION,
+          std::string("Generated by EBMC ") + EBMC_VERSION,
           "QF_AUFBV",
           smt2_solver.value(),
           *outfile_ptr);
@@ -118,7 +118,7 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline)
           return ebmc_solvert{std::make_unique<smt2_convt>(
             ns,
             "ebmc",
-            "Generated by EBMC " EBMC_VERSION,
+            std::string("Generated by EBMC ") + EBMC_VERSION,
             "QF_AUFBV",
             smt2_solver.value(),
             std::cout)};
@@ -128,7 +128,7 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline)
           return ebmc_solvert{std::make_unique<smt2_dect>(
             ns,
             "ebmc",
-            "Generated by EBMC " EBMC_VERSION,
+            std::string("Generated by EBMC ") + EBMC_VERSION,
             "QF_AUFBV",
             smt2_solver.value(),
             message_handler)};

src/ebmc/ebmc_version.h

@@ -1 +1 @@
-#define EBMC_VERSION "5.7"
+extern const char *EBMC_VERSION;

src/vlindex/Makefile

@@ -8,6 +8,7 @@ SRC = \
 OBJ+= $(CPROVER_DIR)/util/util$(LIBEXT) \
       $(CPROVER_DIR)/langapi/langapi$(LIBEXT) \
       $(CPROVER_DIR)/big-int/big-int$(LIBEXT) \
+      ../ebmc/ebmc_version$(OBJEXT) \
       ../verilog/verilog$(LIBEXT)
 
 include ../config.inc

src/vlindex/vlindex_parse_options.cpp

@@ -79,9 +79,8 @@ void vlindex_parse_optionst::help()
 {
   std::cout
     << "\n"
-       "* *             VLINDEX - Copyright (C) 2024                * *\n"
-       "* *                     Version " EBMC_VERSION
-       "                         * *\n"
+    << banner_string("VLINDEX", EBMC_VERSION) << '\n'
+    << "* *                  Copyright (C) 2024                     * *\n"
        "* *                    dkr@amazon.com                       * *\n"
        "\n";
 

src/vlindex/vlindex_parse_options.h

@@ -35,7 +35,7 @@ class vlindex_parse_optionst : public parse_options_baset
         argc,
         argv,
         std::string("EBMC ") + EBMC_VERSION),
-      ui_message_handler(cmdline, "EBMC " EBMC_VERSION)
+      ui_message_handler(cmdline, std::string("EBMC ") + EBMC_VERSION)
   {
   }