Skip to content

Update compilation and development docs #2789

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Aug 31, 2018
Merged

Update compilation and development docs #2789

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2e9bcb4
Update compilation and development docs
Aug 21, 2018
95eae59
CMake support is no longer experimental
Aug 23, 2018
f88a065
Address most review comments
Aug 23, 2018
3f9d01f
Address more review comments
Aug 29, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions COMPILING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -202,9 +202,9 @@ helpful for GUI-based tasks, e.g., the class viewer, debugging, etc., and can
be used for building with MSBuild. Note that you still need to run flex/bison
using "make generated_files" before opening the project.

# WORKING WITH CMAKE (EXPERIMENTAL)
# WORKING WITH CMAKE

There is an experimental build based on CMake instead of hand-written
There is also a build based on CMake instead of hand-written
makefiles. It should work on a wider variety of systems than the standard
makefile build, and can integrate better with IDEs and static-analysis tools.
On Windows, the CMake build does not depend on Cygwin or MinGW, and doesn't
Expand Down
172 changes: 118 additions & 54 deletions doc/architectural/compilation-and-development.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,45 +1,113 @@
\ingroup module_hidden
\page compilation-and-development Compilation and Development

\author Martin Brain, Peter Schrammel
\author Martin Brain, Peter Schrammel, Owen Jones
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've seen @peterschrammel comment on this elsewhere: are authors being recorded or removed?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the conclusion was to record the authors - there were a few arguments for it (more difficult to git praise these pages, recognition of doc contributors).


## Makefiles ##
\section compilation-and-development-section-compilation Compilation

First off, read the \ref cbmc-user-manual "CBMC User Manual". It describes
how to get, build and use CBMC. This document covers the
internals of the system and how to get started on development.
The CBMC source code is available on
[its GitHub page](https://github.com/diffblue/cbmc).

## CMake files ##

To be documented.
\subsection compilation-and-development-subsection-makefiles Makefiles

## Personal configuration: config.inc, macro DEBUG ##
Instructions for compiling CBMC using makefiles are
available in
[COMPILING.md](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md#what-architecture)
in the root of the CBMC repository. They cover Linux, Solaris 11,
FreeBSD 11, MacOS X and Windows.

To be documented.

## Running tests ##
\subsection compilation-and-development-subsection-cmake-files CMake files

### Regression tests ###
There is also support for compiling using CMake. Instructions are
available in
[COMPILING.md](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md#working-with-cmake-experimental)
in the root of the CBMC repository.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One note here is that cmake currently always compiles CBMC and JBMC, whereas with Makefiles you can compile CBMC without JBMC.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Surely with CMake targets you can just compile CBMC?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I asked @smowton and he agreed that you can compile just CBMC using CMake targets, so unless I hear otherwise I won't add anything about this.


The regression tests are contained in the `regression/` folder.
They are grouped into directories for each of the tools/modules.
Each of these contains multiple directories, each of which contains
input files and one or more `.desc` files that describe what command
to run, what output is expected and so on. There is a Perl script,
`test.pl` that is used to invoke the tests as:

\subsection compilation-and-development-subsection-personal-configuration Personal configuration

\subsubsection compilation-and-development-subsubsection-config-inc config.inc

Two files,
[config.inc](https://github.com/diffblue/cbmc/blob/develop/src/config.inc) and
[common](https://github.com/diffblue/cbmc/blob/develop/src/common), are
included in every makefile.
[config.inc](https://github.com/diffblue/cbmc/blob/develop/src/config.inc)
contains configuration options
relating to compilation so that they can be conveniently edited in one place.
[common](https://github.com/diffblue/cbmc/blob/develop/src/common)
contains commands that are needed in every makefile but which the
developer is not expected to edit. (There is also
[another config.inc](https://github.com/diffblue/cbmc/blob/develop/jbmc/src/config.inc)
which is also included in every makefile in the `jbmc` folder.)


\subsubsection compilation-and-development-subsubsection-macro-debug Macro DEBUG

If the macro `DEBUG` is defined during compilation of CBMC (for example by
using a compiler flag) then extra debug code will be included. This includes
print statements and code checking that data structures are as expected.


\section compilation-and-development-section-running-tests Running tests

\subsection compilation-and-development-subsection-regression-tests Regression tests

The regression tests are contained in `regression/` and `jbmc/regression/`.
Inside these folders there is a directory for each of the tools/modules. Each
of these contains multiple test directories, with names describing
what they test. When there are multiple tests in a test directory then
they should be testing very similar aspects of the program's behaviour. Each
test directory contains input files and one or more test description files,
which have the ending `.desc`. The test description files describe what command
to run, what output is expected and so on. The test framework is a
Perl script,
[test.pl](https://github.com/diffblue/cbmc/blob/develop/regression/test.pl).
To run all the tests in a directory corresponding to a tool or module:

../test.pl -c PATH_TO_CBMC
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nobody does that by hand. You usually run it through make.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Be careful when using the term "nobody" :-) - legitimate uses include running selected tests. But arguably the text could recommend the use of make test.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Everyone I know runs test.pl directly, though as @tautschnig says it's normally for running a single test. I will add instructions for make test.


The `–help` option gives instructions for use and the
format of the description files.
The `--help` option to `test.pl` gives instructions for use and outlines the
format of the test description files. Most importantly, the first word in a
test description file is its level, which is one of: `CORE` (should be run in
CI, should succeed), `THOROUGH` (takes too long to be run in CI, should
succeed), `FUTURE` (will succeed when a planned feature is added) or
`KNOWNBUG` (will succeed when a bug is fixed).

If you have compiled CBMC using CMake then another way to run the same tests
is through `CTest`. From the build directory, the command `ctest -V -L CORE`
will run all of the tests that are labelled CORE in the desc files and unit
tests. `-V` makes it print out more
useful output and `-L CORE` makes it only run tests that have been tagged
`CORE`. `-R regular_expression` can be used to limit which tests are run, and
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Might be worth mentioning this can't be used to for example run a specific .desc file, only one of the top level folders.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there actually a way to run individual tests in CMake? Not knowing how to work with the tests is one of the reasons I've largely refrained from adopting CMake.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe that what we add to CTest is one command per module/tool folder, so CTest doesn't know how to run just one folder within one of those.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 provide an example

ctest -L CORE -V -R goto-analyzer will run all the CORE tests in regression/goto-analyzer

`-N` makes it lists which tests it will run without actually running them.


\subsection compilation-and-development-subsection-unit-tests Unit tests

The unit tests are contained in the `unit/` folder. They are written using the
[Catch](https://github.com/philsquared/Catch) unit test framework.

To run the unit tests for CBMC, go to `unit/` and run

To be documented further.
../<build-folder>/bin/unit

### Unit tests ###
To run the unit tests for JBMC, go to `jbmc/unit/` and run

To be documented.
../../<build-folder>/bin/java-unit

## Documentation ##
Note that some tests run which are expected to fail - see the summary at
the end of the run to see how many tests passed, how many failed which were
expected to and how many tests failed which were not expected to.

For more information on the structure of `unit/` and how to tag tests, see
[the section on unit tests in `Compiling.md` in the root of the CBMC
repository](https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md#unit-tests)


\section compilation-and-development-section-documentation Documentation

Apart from the (user-orientated) CBMC user manual and this document, most
of the rest of the documentation is inline in the code as `doxygen` and
Expand All @@ -48,35 +116,31 @@ contained in the `doc/` directory and gives some options for these
tools. All of these could be improved and patches are very welcome. In
some cases the algorithms used are described in the relevant papers.

## Accessing doxygen documentation ##

The doxygen documentation can be [accessed online](http://cprover.diffblue.com).
To build it locally, run `doxygen` in `/src`. HTML output will be created in
`/doc/html`. The index page is `/doc/html/index.html`.

## Coding standards ##

See <a
href="https://github.com/diffblue/cbmc/blob/master/CODING_STANDARD.md">
`CODING_STANDARD.md`</a> file in the root of the CBMC repository.

CPROVER is written in a fairly minimalist subset of C++; templates and
meta-programming are avoided except where necessary.
External library dependencies are avoided (only STL and a SAT solver
are required). Boost is not used. The `util` directory contains many
utilities that are not (yet) in the standard library.

Patches should be formatted so that code is indented with two space
characters, not tab and wrapped to 80 columns. Headers for doxygen
should be given (and preferably filled!) and the author will be the
person who first created the file. Add doxygen comments to
undocumented functions as you touch them. Coding standards
and doxygen comments are enforced by CI before a patch can be
merged by running `clang-format` and `cpplint`.

Identifiers should be lower case with underscores to separate words.
Types (classes, structures and typedefs) names must end with a `t`.
Types that model types (i.e. C types in the program that is being
interpreted) are named with `_typet`. For example `ui_message_handlert`
rather than `UI_message_handlert` or `UIMessageHandler` and
`union_typet`.
To build it locally, run `doxygen` in `src/`. HTML output will be created in
`doc/html/`. The index page is `doc/html/index.html`.


\section compilation-and-development-section-formatting Formatting

The <a
href="https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md">
`CODING_STANDARD.md`</a> file in the root of the CBMC repository contains
guidance on how to write code for the CBMC repository. This includes
which language features can be used and formatting rules.

C++ code can be automatically reformatted in the correct way by running
`clang-format`. There are more details in
[CODING_STANDARD.md](https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md#using-clang-format).


\section compilation-and-development-section-linting Linting

There is also a linting script, `scripts/cpplint.py`. There is a wrapper
script to run `cpplint.py` only on lines that differ from another
branch, e.g. to run it on lines that have been changed from `develop`:

scripts/run_lint.sh develop

There are also instructions for adding this as a git pre-commit hook in
[CODING_STANDARD.md](https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md#pre-commit-hook-to-run-cpplint-locally).