Skip to content

[RFC] Build system support in CBMC version 6 #7835

Closed
@thomasspriggs

Description

@thomasspriggs

We are currently in the planning stages of deciding what major changes should be made for the major CBMC release version 6. The overall issue for release version 6 changes is here - #7743 I am raising this issue to express some of the points in favour and against build systems changes and to collect further feedback.

We currently have two parallel build systems - a set of handwritten makefiles and a cmake based build system. There is a significant maintenance burden from keeping both build systems working. This applies to both individuals working within Diffblue and to new contributors. There is a fairly regular pattern of forgetting one build system or the other when authoring PRs. Not to mention the number of effectively duplicate CI jobs which are required in order to check both builds.

In my opinion there are a number of tangible benefits to solely using a cmake based build system rather than using handwritten makefiles -

  • IDE support - The CMakeLists.txt files define properties of the project such as "which are the source files?" and "what are the dependencies?" whereas the makefiles define "what are the build commands which need to be executed in order to build?". For IDEs this distinction turns out to be important. It facilitates an IDE to open up the project as a project, rather than just a collection of files in a directory hierarchy.
  • Packaging support - We use cpack to produce the installation packages which are posted on the release pages. This includes both the windows installer and the .deb packages for Ubuntu. cpack is based on top of cmake. So without cmake an entirely different packaging system would have to have been written.
  • Modularisation - The build currently relies on a single global include directory shared by all modules. This means any header file in any module can be included from any file in any other module. This is mitigated somewhat by the module_dependences.txt files. However it is still really easy to accidentally introduce cyclic module dependencies or problems with transitive dependencies. With cmake we could more easily define separate include directories for these modules along with the module dependencies. This enables sane logic to do with if module A depends on module B, then it can include the header files of module B and we need to link the object files of module B along with the link dependencies of module B.
  • Build system generation - cmake actually generates build files for other build systems. This doesn't just mean that downstream consumers of cbmc could generate makefiles for compatibility reasons but it also opens up the use of other build systems. These include variations of make such as nmake, ninja for potentially faster builds and Visual Studio project files for VS compatibility. Recent versions of Visual Studio ship with cmake; so cmake itself is not an additional dependency to manually install when working with this platform.
  • Out of tree builds - The cmake build system is setup to build cbmc in a separate build directory. The makefiles build within the src hierarchy alongside the source files themselves. This cleaning a separate source directory is far more straight forward, as we don't need to maintain clean targets in the build system in order for cleaning to work correctly.

Drawbacks of removing the makefiles -

  • Established users of the make build system would need to learn the equivalent commands to build using cmake instead of just make.
  • Downstream projects which are using cbmc's Makefiles would need to be updated for compatibility with newer versions of cbmc. Potentially by using cmake to generate Makefiles and then depending on the generated files.

This potential change was also discussed as comments on this PR - #5558
I think the conclusions of the previous discussions were that there would need to be a migration guide and that it was the kind of change which is better to undertake as part of a major release alongside other potentially breaking changes. There was also some consideration of support for building cbmc with alternate SAT solvers. At the time the PR was raised building with some of the alternate SAT solvers was only supported for the make build. My understanding is that building with these alternates is now well supported in the cmake build.

Metadata

Metadata

Assignees

No one assigned

    Labels

    BuildRFCRequest for commentVersion 6Pull requests and issues requiring a major version bump

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions