[RFC] Version 6

[TGWDB]

This issue is to coordinate a major version bump in CBMC. This can include discussion of things to add/change that may be breaking to backwards compatibility, and other related details.

Note that this RFC will be updated routinely ton reflect the discussion, details listed below are not finalised yet!

Major Changes

1. Make CBMC's default behaviour "sound". This includes turning on/off appropriate checks and other details so that an out of the box run of CBMC should be as close to correct as possible. Related issues include: RFC: How to handle unsound flags #6480 Unsound command line options should be documented and warnings given when used. #6397 reachability-slice changes verification from FAILED to SUCCESSFUL  #6394 Soundness bug with unconstrained pointers #2617 Goto programs with missing function bodies should not be considered well-formed #1949
2. Fix inconsistencies between binaries, e.g. cbmc and goto-instrument. Related issues: Behavior of infinite loops with goto-instrument --unwind N --unwinding-assertions differs from cbmc --unwind N --unwinding-assertions #6433 Difference in behavior of cbmc --unwind N and goto-instrument --unwind N #6432
3. Update to C++17 and replace backported STL functions with standard library versions.
4. Report more fine grained verification results. Related issues: RFC: How to handle unsound flags #6480

Minor Changes

1. Remove deprecated functions
2. Array types to contain an index type: introduce index_type and element_type for arrays and vectors #6552

Related Tagged Issues/PRs

Related issues and PRs

[martin-cs]

1. What is the time-frame for version 6? There are some changes I would really like to make but which rather depends on when V6 will be.
2. The convention used to be that a major version number change was when the on-disk format changed in a significant way. Is this still the case?

[TGWDB]

1. What is the time-frame for version 6? There are some changes I would really like to make but which rather depends on when V6 will be.

We'd be aiming for August, likely finalise in the second half.

2. The convention used to be that a major version number change was when the on-disk format changed in a significant way. Is this still the case?

You mean the goto binary disk representation? If so I don't think there is anything in the list at the top that requires a change (although some related representations of memory might do this?). However, since some of the proposed changes that would alter CBMC's default behaviour significantly we considered this worthy of a major version change. Happy to discuss/clarify if I've misunderstood here.

[rod-chapman]

Please look at #7732 too - this is a soundness issue.

[thomasspriggs]

This RFC is currently missing any outline of a process for the major release process. I am going to outline a release process here, for visibility and to give an opportunity for discussion -

1. Copy the develop branch to develop-v5 on this repository, with git hub protections in place as for the original develop branch. This branch is for the release of any required back ported updates/fixes. Hopefully once we have started the process there will be no need to back port fixes, but this protected branch will exist for that contingency. The expectation is that by default all further enhancements to cbmc will be made to the develop branch as per the normal process outside of a major release.
2. Bump version of develop to cbmc-6.0.0-preview the suffix indicates that more non-backwards compatible changes are yet to be merged. See - CBMC version 6 release process changes #7987 the idea is that it may take longer than our typical release cycle to get all major version related changes merged. Therefore any releases done during this period will be pre-releases. The PR for this change is to also disable pushing pre-releases to docker / homebrew.
3. Marshall in all issues and PRs agreed upon for the major release. See previous discussions in this RFC and all issues / PRs marked with the version 6 label - Version 6 Pull requests and issues requiring a major version bump My team is planning to undertake work involving rebasing and managing dependencies to get everything in. The PRs will go through the usual PR process. It is expected that some / or all of them will need rebasing effort due either to the time since the work was started or the merging of other version 6 PRs.
4. Remove -preview from release suffix. The PR for this change is to also re-enable pushing pre-releases to docker / homebrew. This final step will mark the major release as complete and ready for use.

I have deliberately kept discussions of which PRs should go in, in what order out of the above list in an attempt to focus an overall process. My team has begun work on producing rebased/updated branches for the less controversial / most ready to merge changes, in an effort to keep the process more streamlined. We need to co-ordinate to avoid duplicated effort on this front.

[TGWDB]

Project board for Version 6 now available here: https://github.com/orgs/diffblue/projects/11/views/1