add git shortened sha1sum to CBMC version for unique id

[mgudemann]

this adds the output of git describe --tags --always to the CBMC version string, making exact identification of a binary CBMC version possible.

[tautschnig]

I think this is a very good idea; yet I'd have a slightly different proposal lying around that I'd like to put forward for discussion. I'll post a link to a branch in a few minutes.

[mgudemann]

I am curious to see this. Obviously my approach is not mergeable right away as it does not format nicely in the CBMC help() message, but having a UID would be beneficial in any case.

[tautschnig]

I have pushed tautschnig/cbmc@6694d4e - comments much appreciated.

[tautschnig]

@mgudemann I'll move the discussion in here if that's ok? Just to have the full trail in one place. Quoting yourself in the context of my use of git rev-parse --short HEAD:

@mgudemann said in tautschnig/cbmc@6694d4e:

For the overall version, I'd prefer the git describe --tags --always output, as it is a bit more extensive; as it will only show on --version this should be ok. But I have no strong feelings about this, in any case having n/a in case of a fail or +dirty is a very good idea.

Will the above work on windows? My proposal fails on Travis as git is not installed, I presume your version would work?

Quite frankly I wasn't aware of git describe --tags --always - it's indeed very nice and allows us to move that stanza I had placed in config.inc into common as there shouldn't be a need to change that anymore. All version setting is then sorted out via git tags.

The key difference between our approaches is the use of command-line defines vs generating a file. Can the file-base approach deal with uncommitted changes?

[mgudemann]

git-describe even has a --dirty option which generates something like cbmc-5.6-847-g887c9c0-dirty for my current version (after an intentional uncommited change). If I am right, then this is tag+number of commits after last tag+short hash + (optional dirty flag)

[martin-cs]

I have no useful opinion on which to pick but I'd really like that one of them is picked. This will make my job working with customers much easier!

[mgudemann]

I think @tautschnig's solution is better, this together with git-describe and appropriate options should be enough to uniquely identify and also make local recompilation of an equivalent version possible.
We'd need to update the CI builds with git though, or at least have a fallback like n/a as in @tautschnig's approach

[tautschnig]

@mgudemann Would you mind doing the following, in an attempt to preserve the discussion: cherry-pick my commit into your branch for this pull request, possibly discard your commit, and add the suggested improvements such as using git describe --tags --always --dirty? Closing this pull request and opening a new one from my branch would be easy, but would lose the discussion.

[kroening]

A luxury variant of this would recognise that a particular version is a release, and then mark it as such.

[tautschnig]

@kroening I believe we would actually get that via the proposed git describe: As an example, git describe --tags --always 8a0088e (the 5.6 tag) yields "cbmc-5.6", without any additional git revision.

[mgudemann]

@tautschnig I took your commit and adapted to current master
Windows uses different escaping, so the Makefiles now contain two definitions for CBMC_VERSION, using -DCBMC_VERSION=\"..\" and /DCBMC_VERSION='"""..."""''.

[kroening]

The benefit of the earlier variant was that the build system would notice that a new version got checked out, and then re-build the files that include version.h.

Right now, that will only work when a manual 'make clean' is issued.

[tautschnig]

@kroening Isn't that only an issue when placing a tag? Any code changes would obviously trigger a rebuild and therefore the binaries would have the most up-to-date version information. If the only change is the version (but no files have been touched), then the only case where that can occur is when a tag has been placed. This seems to be a quarterly activity (at most), hence it might be acceptable to do touch */*parse_options.cpp (make clean isn't required).

[kroening]

Yes, code changes would trigger a rebuild, but not necessarily to the file that prints the version number; i.e., you would get a binary that has a hash in that is inconsistent with the code that was compiled.

[tautschnig]

Ah, of course, apologies for missing that. There should actually be a setup such that a file is re-built whenever the version string changes. I'll think about a suitable make rule.

[mgudemann]

how about

git_new_version: ../.git/HEAD ../.git/index
	touch git_new_version; touch */*parse_options.cpp

and adding git_new_version to the relevant build goals ?

[tautschnig]

@mgudemann My concern here is that it wouldn't update on a dirty code base!?

[forejtv]

@martin-cs @mgudemann @kroening For identifying a version used by DiffBlue customers we use versioning from https://github.com/diffblue/platform/tree/develop/docker (private repo). The customers won't directly run cbmc from command line, so whatever approach is implemented here, they will not see it.

[tautschnig]

Here's how to make the version string update (not sure tabs paste well):

--- a/.gitignore
+++ b/.gitignore
@@ -20,6 +20,7 @@ src/goto-analyzer/taint_driver_scripts/.idea/*
 *.obj
 *.a
 *.lib
+.release_info
 src/ansi-c/arm_builtin_headers.inc
 src/ansi-c/clang_builtin_headers.inc
 src/ansi-c/cprover_library.inc
diff --git a/src/common b/src/common
index 20c4fad..fa290cb 100644
--- a/src/common
+++ b/src/common
@@ -182,12 +182,22 @@ OBJ += $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC)))
 %.obj:%.c
        $(CC) $(CP_CFLAGS) /nologo /c /EHsc $< /Fo$@

+KNOWN_RELEASE_INFO = $(shell cat .release_info 2>/dev/null)
+ifneq ($(RELEASE_INFO), $(KNOWN_RELEASE_INFO))
+$(filter %_parse_options$(OBJEXT), $(OBJ)): .release_info
+
+.release_info:
+       echo $(RELEASE_INFO) > $@
+
+.PHONY: .release_info
+endif
+
 clean:
        $(RM) $(patsubst %.cpp, %$(OBJEXT), $(filter %.cpp, $(SRC))) \
                $(patsubst %.cpp, %.d, $(filter %.cpp, $(SRC))) \
                $(patsubst %.cc, %$(OBJEXT), $(filter %.cc, $(SRC))) \
                $(patsubst %.cc, %.d, $(filter %.cc, $(SRC))) \
-               $(CLEANFILES)
+               $(CLEANFILES) .release_info

 .PHONY: first_target clean all
 .PHONY: sources generated_files

[mgudemann]

@tautschnig you could attach the patch, as zip if it doesn't work directly

[tautschnig]

I'm sorry, I should have done that before:
0001-Build-.release_info-files-containing-the-version-str.patch.zip

[martin-cs]

@forejtv There are two important use cases for this. One is me looking at logs to work out what is going wrong and being able to remotely replicate what is happening on customer sites -- they may not see it but I will. Second is for https://github.com/diffblue/test-gen/issues/187 . Both of these are causing pain in supporting customers so please could we remove the do not merge?

@tautschnig @mgudemann Can't this be done with simple keyword substitution in one file, like subversion would? Apparently https://git-scm.com/book/en/v2/Customizing-Git-Git-Attributes#Keyword-Expansion gives a recipe for this.

[tautschnig]

@forejtv I actually don't know why this is marked do-not-merge?

@martin-cs Thanks for the pointer to keyword substitution! Yet I'm not sure there's a genuine problem with the proposed solution? Note that keyword substitution won't cover the local-changes-in-repository problem, which the proposed patch does address.

[tautschnig]

I'll refrain from approving a PR that contains changes by myself ;-)

For regression tests, actually the keyword expansion might come into play: we could have a test that checks that the specific git commit id is included in the --version output.

[mgudemann]

@tautschnig one thing I saw is this

* *   CBMC 5.7 (cbmc-5.7-243-gf7be1c4) - Copyright (C) 2001-2016 (64-bit version)   * *
* *              Daniel Kroening, Edmund Clarke             * *
* * Carnegie Mellon University, Computer Science Department * *
* *                 [email protected]                   * *
* *        Protected in part by U.S. patent 7,225,417       * *

maybe better have something like

* *   CBMC 5.7 - Copyright (C) 2001-2016 (64-bit version)   * *
* *                  (cbmc-5.7-243-gf7be1c4)                * *
* *              Daniel Kroening, Edmund Clarke             * *
* * Carnegie Mellon University, Computer Science Department * *
* *                 [email protected]                   * *
* *        Protected in part by U.S. patent 7,225,417       * *

[tautschnig]

Indeed; how about

* *       CBMC - Copyright (C) 2001-2016 (64-bit version)   * *
* *              (version cbmc-5.7-243-gf7be1c4)            * *
* *              Daniel Kroening, Edmund Clarke             * *
* * Carnegie Mellon University, Computer Science Department * *
* *                 [email protected]                   * *
* *        Protected in part by U.S. patent 7,225,417       * *

to make the implementation via CBMC_VERSION simpler?

[mgudemann]

@tautschnig we have this now

* *   CBMC 5.7 - Copyright (C) 2001-2016 (64-bit version)   * *
* *                  (cbmc-5.7-244-g4df4a36)                * * 
* *              Daniel Kroening, Edmund Clarke             * *
* * Carnegie Mellon University, Computer Science Department * *
* *                 [email protected]                   * *
* *        Protected in part by U.S. patent 7,225,417       * *

[mgudemann]

@forejtv I think this is becoming mergeable

[forejtv]

I am not able to figure out how I should test this. When I check the branch out and compile, I don't see a git sha anywhere when I run cbmc, cbmc -help or cbmc --version, I am always just getting "5.7".

What should I be running to see the sha?

[tautschnig]

@forejtv That's rather surprising. I've just done this:

$ git remote add mgudemann https://github.com/mgudemann/cbmc
$ git fetch mgudemann
$ git checkout -t -b git_version_output mgudemann/git_version_output
$ make minisat2-download
$ make -j3
$ cbmc/cbmc --version
(cbmc-5.7-244-g4df4a36b8)

(And you should also see CBMC_VERSION being defined on the compiler command lines.)

[forejtv]

Why is this different from https://github.com/diffblue/cbmc/pull/668/files#diff-d9c95ec27fc25a0481354de531adad56R34?

[forejtv]

When I delete the .git directory before compiling, as a result I get

CBMC version (n/a) 64-bit x86_64 linux

Is that expected? We're still keeping version info in https://github.com/diffblue/cbmc/pull/668/files/4df4a36b894fdf1f5fcfe4ad196505f2d334e36e#diff-b4a2f4e2f20572b496e8590dcf1dec51R33, so maybe that one should be used, with some suffix indicating that the version cannot be determined?

[forejtv]

@tautschnig It worked for me on the next compilation attempt, I must have had a bad day.

[tautschnig]

Ok, good to know it worked. Your concerns are of course valid and need a solution.

[kroening]

The key problem I see is that this requires a 'make clean' to make sure that all files that use the define get recompiled. Is there an intend to add dependencies on .release_info?

The key benefit of using an include is that the dependency system takes care of incremental builds. Thus, I'd suggest:

1. The make files write the git hash into some header file IF it has changed.
2. The .cpp files include that header file to get the version string.

[tautschnig]

The dependencies are addressed via changes to common - and it would be possible to use the .release_info files for grabbing the version string.

[tautschnig]

@mgudemann Any chance to push this further?

[tautschnig]

@mgudemann Is there any chance you might be able to progress this PR? Do let me know if you'd like to hand off this PR to someone else. I'm repeatedly running into the issue that people have results with some version of CBMC and we then cannot figure out what exact source version that had been compiled from.

[martin-cs]

+1 would love to see this functionality merged.

[chrisr-diffblue]

+1 would love to see this too.

[tautschnig]

I'm happy to create a new PR to drive this myself, but I don't want to do what could be seen as a hostile takeover as @mgudemann hasn't commented on this.

[mgudemann]

@tautschnig I am happy with you taking this over. For TG we have a cmake solution, we should keep that in mind when adding that to CBMC / JBMC.

[tautschnig]

Taking over work on this in #2373.