CBMC_VERSION: Use generated include files instead of command-line defines

Also fixes a number of shortcomings of the earlier approach as far as CMake is
concerned:
- Adds --dirty to the git command line (as is done for Makefiles).
- Does not require a rebuild when there are no changes to the version string.
- CBMC release number updates will be reflected and trigger a rebuild (even when
  no other changes have taken place).

Author: tautschnig

.gitignore

@@ -28,7 +28,7 @@ Release/*
 *.obj
 *.a
 *.lib
-.release_info
+version.h
 src/ansi-c/arm_builtin_headers.inc
 src/ansi-c/clang_builtin_headers.inc
 src/ansi-c/cprover_builtin_headers.inc

CMakeLists.txt

@@ -39,52 +39,47 @@ if(${enable_cbmc_tests})
     enable_testing()
 endif()
 
-file(STRINGS src/config.inc config_inc_v REGEX "CBMC_VERSION *= *[0-9\.]+")
-string(REGEX REPLACE "^CBMC_VERSION *= *" "" CBMC_RELEASE ${config_inc_v})
-message(STATUS "CBMC release ${CBMC_RELEASE}")
-
+# based on https://cmake.org/pipermail/cmake/2010-July/038015.html
 find_package(Git)
+if(GIT_FOUND)
+  file(WRITE ${CMAKE_BINARY_DIR}/version.cmake
+    "
+    file(STRINGS \${CBMC_SOURCE_DIR}/config.inc
+      config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\")
+    string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v})
+    execute_process(
+      COMMAND \"${GIT_EXECUTABLE}\" \"describe\" \"--tags\" \"--always\" \"--dirty\"
+      OUTPUT_VARIABLE GIT_INFO
+      OUTPUT_STRIP_TRAILING_WHITESPACE
+    )
+    configure_file(\${CUR}/version.h.in version.h)
+    "
+  )
+else()
+  file(WRITE ${CMAKE_BINARY_DIR}/version.cmake
+    "
+    file(STRINGS \${CBMC_SOURCE_DIR}/config.inc
+      config_inc_v REGEX \"CBMC_VERSION *= *[0-9\.]+\")
+    string(REGEX REPLACE \"^CBMC_VERSION *= *\" \"\" CBMC_RELEASE \${config_inc_v})
+    set(GIT_INFO \"n/a\")
+    configure_file(\${CUR}/version.h.in version.h)
+    "
+  )
+endif()
 
-macro(git_revision target files_var)
-  if(GIT_FOUND)
-    add_custom_command(
-      OUTPUT .release_info
-      COMMAND ${CMAKE_COMMAND} -E echo_append "#define __CBMC_VERSION " > .release_info
-      COMMAND "${GIT_EXECUTABLE}" "describe" "--tags" "--always" "--long" >> .release_info
-      COMMAND ${CMAKE_COMMAND} -E echo "#define __CBMC_VERSION_str(v) \"${CBMC_RELEASE} (\" # v \")\"" >> .release_info
-      COMMAND ${CMAKE_COMMAND} -E echo "#define __CBMC_VERSION_xstr(v) __CBMC_VERSION_str(v)" >> .release_info
-      COMMAND ${CMAKE_COMMAND} -E echo "#define CBMC_VERSION __CBMC_VERSION_xstr(__CBMC_VERSION)" >> .release_info
-      VERBATIM
-      )
-    add_custom_command(
-      TARGET ${target}
-      POST_BUILD
-      COMMAND ${CMAKE_COMMAND} -E remove -f .release_info
-      )
-  else()
-    add_custom_command(
-      OUTPUT .release_info
-      COMMAND ${CMAKE_COMMAND} -E echo "#define CBMC_VERSION \"${CBMC_RELEASE} (n/a)\"" >> .release_info
-      VERBATIM
-      )
-  endif()
-
-  if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
-     "${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang" OR
-     "${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU"
+macro(git_revision target)
+  file(WRITE ${CMAKE_CURRENT_BINARY_DIR}/version.h.in
+    "\#define CBMC_VERSION \"@CBMC_RELEASE@ (@GIT_INFO@)\"\n")
+  add_custom_target(
+    ${target}-version.h
+    COMMAND ${CMAKE_COMMAND}
+      -D CBMC_SOURCE_DIR=${CBMC_SOURCE_DIR}
+      -D CUR=${CMAKE_CURRENT_BINARY_DIR}
+      -P ${CMAKE_BINARY_DIR}/version.cmake
   )
-    set_source_files_properties(
-      ${${files_var}}
-      PROPERTIES
-        OBJECT_DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/.release_info
-        COMPILE_FLAGS "-include .release_info")
-  elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
-    set_source_files_properties(
-      ${${files_var}}
-      PROPERTIES
-        COMPILE_FLAGS "/DCBMC_VERSION=\"${CBMC_RELEASE} (n/a)\"")
-  endif()
+ add_dependencies(${target} ${target}-version.h)
 endmacro()
+include_directories(${CMAKE_CURRENT_BINARY_DIR})
 
 add_subdirectory(src)
 add_subdirectory(regression)

jbmc/src/janalyzer/CMakeLists.txt

@@ -25,5 +25,4 @@ target_link_libraries(janalyzer-lib
 add_executable(janalyzer janalyzer_main.cpp)
 target_link_libraries(janalyzer janalyzer-lib)
 
-set(cbmc_version_files janalyzer_parse_options.cpp)
-git_revision(janalyzer-lib cbmc_version_files)
+git_revision(janalyzer-lib)

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -56,6 +56,8 @@ Author: Daniel Kroening, [email protected]
 #include <goto-analyzer/taint_analysis.h>
 #include <goto-analyzer/unreachable_instructions.h>
 
+#include "version.h"
+
 janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
   : parse_options_baset(JANALYZER_OPTIONS, argc, argv),
     messaget(ui_message_handler),

jbmc/src/jbmc/CMakeLists.txt

@@ -30,5 +30,4 @@ target_link_libraries(jbmc-lib
 add_executable(jbmc jbmc_main.cpp)
 target_link_libraries(jbmc jbmc-lib)
 
-set(cbmc_version_files jbmc_parse_options.cpp)
-git_revision(jbmc-lib cbmc_version_files)
+git_revision(jbmc-lib)

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -60,6 +60,8 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/replace_java_nondet.h>
 #include <java_bytecode/simple_method_stubbing.h>
 
+#include "version.h"
+
 jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv):
   parse_options_baset(JBMC_OPTIONS, argc, argv),
   messaget(ui_message_handler),

jbmc/src/jdiff/CMakeLists.txt

@@ -27,5 +27,4 @@ target_link_libraries(jdiff-lib
 add_executable(jdiff jdiff_main.cpp)
 target_link_libraries(jdiff jdiff-lib)
 
-set(cbmc_version_files jdiff_parse_options.cpp)
-git_revision(jdiff-lib cbmc_version_files)
+git_revision(jdiff-lib)

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -60,6 +60,8 @@ Author: Peter Schrammel
 #include <goto-diff/goto_diff.h>
 #include <goto-diff/unified_diff.h>
 
+#include "version.h"
+
 jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
   : parse_options_baset(JDIFF_OPTIONS, argc, argv),
     jdiff_languagest(cmdline, ui_message_handler),

src/cbmc/CMakeLists.txt

@@ -32,5 +32,4 @@ add_if_library(cbmc-lib jsil)
 add_executable(cbmc cbmc_main.cpp)
 target_link_libraries(cbmc cbmc-lib)
 
-set(cbmc_version_files cbmc_parse_options.cpp cbmc_solvers.cpp)
-git_revision(cbmc-lib cbmc_version_files)
+git_revision(cbmc-lib)

src/cbmc/Makefile

@@ -56,15 +56,15 @@ INCLUDES= -I ..
 
 LIBS =
 
-CBMC_VERSION_FILES = cbmc_solvers$(OBJEXT)
-
 include ../config.inc
 include ../common
 
 CLEANFILES = cbmc$(EXEEXT)
 
 all: cbmc$(EXEEXT)
 
+cbmc_solvers$(OBJEXT): $(GIT_INFO_FILE)
+
 ifneq ($(wildcard ../bv_refinement/Makefile),)
   OBJ += ../bv_refinement/bv_refinement$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_BV_REFINEMENT

src/cbmc/cbmc_parse_options.cpp

@@ -64,6 +64,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "xml_interface.h"
 
+#include "version.h"
+
 cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv):
   parse_options_baset(CBMC_OPTIONS, argc, argv),
   xml_interfacet(cmdline),

src/cbmc/cbmc_solvers.cpp

@@ -28,6 +28,7 @@ Author: Daniel Kroening, [email protected]
 #include "bv_cbmc.h"
 #include "cbmc_dimacs.h"
 #include "counterexample_beautification.h"
+#include "version.h"
 
 /// Uses the options to pick an SMT 2.0 solver
 /// \return An smt2_dect::solvert giving the solver to use.

src/clobber/CMakeLists.txt

@@ -30,5 +30,4 @@ add_if_library(clobber-lib bv_refinement)
 add_executable(clobber clobber_main.cpp)
 target_link_libraries(clobber clobber-lib)
 
-set(cbmc_version_files clobber_parse_options.cpp)
-git_revision(clobber-lib cbmc_version_files)
+git_revision(clobber-lib)

src/clobber/clobber_parse_options.cpp

@@ -34,6 +34,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <langapi/mode.h>
 
+#include "version.h"
 
 clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv):
   parse_options_baset(CLOBBER_OPTIONS, argc, argv),

src/common

@@ -229,23 +229,18 @@ OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC)))
 
 # get version from git
 GIT_INFO = $(shell git describe --tags --always --dirty || echo "n/a")
-GIT_INFO_FILE = .release_info
+RELEASE_INFO = \#define CBMC_VERSION "$(CBMC_VERSION) ($(GIT_INFO))"
+GIT_INFO_FILE = version.h
 
-CBMC_VERSION_FILES += $(filter %_parse_options$(OBJEXT), $(OBJ))
+$(GIT_INFO_FILE):
+	echo '$(RELEASE_INFO)' > $@
 
-ifeq ($(BUILD_ENV_),MSVC)
-$(CBMC_VERSION_FILES): CP_CXXFLAGS += /DCBMC_VERSION='"""$(CBMC_VERSION) ($(GIT_INFO))"""'
-else
-$(CBMC_VERSION_FILES): CP_CXXFLAGS += -DCBMC_VERSION="\"$(CBMC_VERSION) ($(GIT_INFO))\""
-endif
+$(filter %_parse_options$(OBJEXT), $(OBJ)): $(GIT_INFO_FILE)
 
+# mark the actually generated file as a phony target to enforce a rebuild - but
+# only of the version information has changed!
 KNOWN_RELEASE_INFO = $(shell cat $(GIT_INFO_FILE) 2>/dev/null)
-ifneq ($(GIT_INFO), $(KNOWN_RELEASE_INFO))
-$(CBMC_VERSION_FILES): $(GIT_INFO_FILE)
-
-$(GIT_INFO_FILE):
-	echo $(GIT_INFO) > $@
-
+ifneq ($(RELEASE_INFO), $(KNOWN_RELEASE_INFO))
 .PHONY: $(GIT_INFO_FILE)
 endif
 

src/goto-analyzer/CMakeLists.txt

@@ -27,5 +27,4 @@ add_if_library(goto-analyzer-lib jsil)
 add_executable(goto-analyzer goto_analyzer_main.cpp)
 target_link_libraries(goto-analyzer goto-analyzer-lib)
 
-set(cbmc_version_files goto_analyzer_parse_options.cpp)
-git_revision(goto-analyzer-lib cbmc_version_files)
+git_revision(goto-analyzer-lib)

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -61,6 +61,7 @@ Author: Daniel Kroening, [email protected]
 #include "static_show_domain.h"
 #include "static_simplifier.h"
 #include "static_verifier.h"
+#include "version.h"
 
 goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(
   int argc,

src/goto-cc/CMakeLists.txt

@@ -35,5 +35,4 @@ else()
       goto-cc $<TARGET_FILE_DIR:goto-cc>/goto-gcc)
 endif()
 
-set(cbmc_version_files as_mode.cpp compile.cpp gcc_mode.cpp goto_cc_mode.cpp)
-git_revision(goto-cc-lib cbmc_version_files)
+git_revision(goto-cc-lib)

src/goto-cc/Makefile

@@ -38,11 +38,6 @@ LIBS =
 
 CLEANFILES = goto-cc$(EXEEXT) goto-cl$(EXEEXT)
 
-CBMC_VERSION_FILES = as_mode$(OBJEXT) \
-                     compile$(OBJEXT) \
-                     gcc_mode$(OBJEXT) \
-                     goto_cc_mode$(OBJEXT)
-
 include ../config.inc
 include ../common
 
@@ -51,6 +46,8 @@ all: goto-cl$(EXEEXT)
 endif
 all: goto-cc$(EXEEXT)
 
+as_mode$(OBJEXT) compile$(OBJEXT) gcc_mode$(OBJEXT) goto_cc_mode$(OBJEXT): $(GIT_INFO_FILE)
+
 ifneq ($(wildcard ../jsil/Makefile),)
   OBJ += ../jsil/jsil$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_JSIL

src/goto-cc/as_mode.cpp

@@ -30,6 +30,7 @@ Author: Michael Tautschnig
 #include <util/cout_message.h>
 
 #include "compile.h"
+#include "version.h"
 
 static std::string assembler_name(
   const cmdlinet &cmdline,

src/goto-cc/compile.cpp

@@ -63,6 +63,8 @@ Date: June 2006
 #define pclose _pclose
 #endif
 
+#include "version.h"
+
 /// reads and source and object files, compiles and links them into goto program
 /// objects.
 /// \return true on error, false otherwise

src/goto-cc/gcc_mode.cpp

@@ -48,6 +48,7 @@ Author: CM Wintersteiger, 2006
 
 #include "hybrid_binary.h"
 #include "linker_script_merge.h"
+#include "version.h"
 
 static std::string compiler_name(
   const cmdlinet &cmdline,

src/goto-cc/goto_cc_mode.cpp

@@ -24,6 +24,8 @@ Author: CM Wintersteiger, 2006
 
 #include <util/parse_options.h>
 
+#include "version.h"
+
 /// constructor
 goto_cc_modet::goto_cc_modet(
   goto_cc_cmdlinet &_cmdline,

src/goto-diff/CMakeLists.txt

@@ -29,5 +29,4 @@ add_if_library(goto-diff-lib jsil)
 add_executable(goto-diff goto_diff_main.cpp)
 target_link_libraries(goto-diff goto-diff-lib)
 
-set(cbmc_version_files goto_diff_parse_options.cpp)
-git_revision(goto-diff-lib cbmc_version_files)
+git_revision(goto-diff-lib)

src/goto-diff/goto_diff_parse_options.cpp

@@ -59,6 +59,7 @@ Author: Peter Schrammel
 #include "syntactic_diff.h"
 #include "unified_diff.h"
 #include "change_impact.h"
+#include "version.h"
 
 goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv):
   parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv),

src/goto-instrument/CMakeLists.txt

@@ -33,5 +33,4 @@ add_if_library(goto-instrument-lib glpk)
 add_executable(goto-instrument goto_instrument_main.cpp)
 target_link_libraries(goto-instrument goto-instrument-lib)
 
-set(cbmc_version_files "goto_instrument_parse_options.cpp")
-git_revision(goto-instrument-lib cbmc_version_files)
+git_revision(goto-instrument-lib)

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -98,6 +98,7 @@ Author: Daniel Kroening, [email protected]
 #include "undefined_functions.h"
 #include "remove_function.h"
 #include "splice_call.h"
+#include "version.h"
 
 /// invoke main modules
 int goto_instrument_parse_optionst::doit()

src/memory-models/CMakeLists.txt

@@ -12,5 +12,4 @@ generic_includes(mmcc)
 
 target_link_libraries(mmcc util)
 
-set(cbmc_version_files mmcc_parse_options.cpp)
-git_revision(mmcc cbmc_version_files)
+git_revision(mmcc)

src/memory-models/mmcc_parse_options.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "mm_parser.h"
 #include "mm2cpp.h"
+#include "version.h"
 
 mmcc_parse_optionst::mmcc_parse_optionst(int argc, const char **argv):
   parse_options_baset(MMCC_OPTIONS, argc, argv)