cprover
/builddir/build/BUILD/cbmc-cbmc-5.11/doc/architectural/compilation-and-development.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \page compilation-and-development Compilation and Development
3 
4 \author Martin Brain, Peter Schrammel, Owen Jones
5 
6 \section compilation-and-development-section-compilation Compilation
7 
8 The CBMC source code is available on
9 [its GitHub page](https://github.com/diffblue/cbmc).
10 
11 
12 \subsection compilation-and-development-subsection-makefiles Makefiles
13 
14 Instructions for compiling CBMC using makefiles are
15 available in
16 [COMPILING.md](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md#what-architecture)
17 in the root of the CBMC repository. They cover Linux, Solaris 11,
18 FreeBSD 11, MacOS X and Windows.
19 
20 
21 \subsection compilation-and-development-subsection-cmake-files CMake files
22 
23 There is also support for compiling using CMake. Instructions are
24 available in
25 [COMPILING.md](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md#working-with-cmake)
26 in the root of the CBMC repository.
27 
28 
29 \subsection compilation-and-development-subsection-personal-configuration Personal configuration
30 
31 \subsubsection compilation-and-development-subsubsection-config-inc config.inc
32 
33 Two files,
34 [config.inc](https://github.com/diffblue/cbmc/blob/develop/src/config.inc) and
35 [common](https://github.com/diffblue/cbmc/blob/develop/src/common), are
36 included in every makefile.
37 [config.inc](https://github.com/diffblue/cbmc/blob/develop/src/config.inc)
38 contains configuration options
39 relating to compilation so that they can be conveniently edited in one place.
40 [common](https://github.com/diffblue/cbmc/blob/develop/src/common)
41 contains commands that are needed in every makefile but which the
42 developer is not expected to edit. (There is also
43 [another config.inc](https://github.com/diffblue/cbmc/blob/develop/jbmc/src/config.inc)
44 which is also included in every makefile in the `jbmc` folder.)
45 
46 Note, these files are not involved in the CMake build.
47 
48 
49 \subsubsection compilation-and-development-subsubsection-macro-debug Macro DEBUG
50 
51 If the macro `DEBUG` is defined during compilation of CBMC (for example by
52 using a compiler flag) then extra debug code will be included. This includes
53 print statements and code checking that data structures are as expected.
54 
55 
56 \section compilation-and-development-section-running-tests Running tests
57 
58 \subsection compilation-and-development-subsection-regression-tests Regression tests
59 
60 The regression tests are contained in `regression/` and `jbmc/regression/`.
61 Inside these folders there is a directory for each of the modules. Each
62 of these contains multiple test directories, with names describing
63 what they test. When there are multiple tests in a test directory then
64 they should all test very similar aspects of the program's behaviour. Each
65 test directory contains input files and one or more test description files,
66 which have the ending `.desc`. The test description files specify what command
67 to run, what output is expected and so on. The test framework is a
68 Perl script,
69 [test.pl](https://github.com/diffblue/cbmc/blob/develop/regression/test.pl),
70 located in `regression/test.pl`.
71 
72 The `--help` option to `test.pl` outlines the
73 format of the test description files. Most importantly, the first word in a
74 test description file is its level, which is one of: `CORE` (should be run in
75 CI, should succeed), `THOROUGH` (takes too long to be run in CI, should
76 succeed), `FUTURE` (will succeed when a planned feature is added) or
77 `KNOWNBUG` (will succeed when a bug is fixed).
78 
79 \subsubsection compilation-and-development-subsubsection-running-regression-tests-with-make Running regression tests with make
80 
81 If you have compiled using `make` then you can run the regression tests
82 using `make test`. Run it from `regression/` to run all the regression tests,
83 or any of its subfolders to just run the tests for that module. The number
84 of tests that are run in parallel can be controlled through the environment
85 variable `TESTPL_JOBS`.
86 
87 If you have not compiled using `make` then this won't work, because the
88 makefile is expecting to find binaries like `cbmc` and `jbmc` in the source
89 folders.
90 
91 \subsubsection compilation-and-development-subsubsection-running-regression-tests-with-ctest Running regression tests with CTest
92 
93 If you have compiled using CMake then you can run the regression tests using
94 CTest. (Note: this will also run the unit tests.)
95 
96 Here are two example commands, to be run from the `build/` directory:
97 
98  ctest -V -L CORE -R cpp
99  ctest -V -L CORE -R cpp -E cbmc-cpp
100 
101 `-V` makes it print out more
102 useful output. `-L CORE` makes it only run tests that have been tagged
103 `CORE`. `-R regular_expression` can be used to limit which tests are run to
104 those which match the given regular expression, and `-E regex` excludes tests
105 to those which match the given regular expression.
106 So the first command will run all the CORE tests in `regression/cbmc/cpp` and
107 `regression/cbmc/cbmc-cpp`, and the second will run all the CORE tests in
108 `regression/cbmc/cpp` only. Another useful option is `-N`, which makes CTest
109 list which tests it will run without actually running them.
110 
111 
112 \subsubsection compilation-and-development-subsubsection-running-individual-regression-tests-directly-with-test-pl Running individual regression tests directly with test.pl
113 
114 It can be useful to run a single test folder in isolation. This can be done by
115 running `regression/test.pl` directly. The way that `test.pl` is run varies between the
116 different modules, and can be ascertained by looking at the `test` target in
117 the makefile. The simple case is when there isn't a file called `chain.sh`.
118 Then you can directly run `test.pl` on a single test folder with the
119 following command from the module directory (note that it is recommended to
120 use absolute paths as it avoids many issues, e.g. the path to the binary
121 should be relative to `<test-folder>`):
122 
123  <absolute-path-to-test.pl> -p -c <absolute-path-to-binary> <test-folder>
124 
125 `-p` makes it print a log of failed tests and `-c` tells it where to find the
126 binary to run, e.g. `cbmc`, `jbmc` or `goto-analyzer`.
127 If `<test-folder>` is not provided then all test directories are run. The
128 `--help` option lists all command line options, including `-j` for running
129 multiple tests in parallel and `-C`, `-T`, `-F` and `-K` for controlling
130 whether `CORE`, `THOROUGH`, `FUTURE` or `KNOWNBUG` tests are run.
131 
132 When there is a file called `chain.sh` then the command should look like
133 
134  <absolute-path-to-test.pl> -p -c '<absolute-path-to-chain-sh> <arg-1> ... <arg-n>' <test-folder>
135 
136 Note that the test binary and its initial command line arguments are a single
137 value for the -c option, so they must be be wrapped in quotes if they contain
138 any unescaped spaces. What to put for the
139 arguments `<arg-1>` to `<arg-n>` varies from module to module. To find
140 out, look in `chain.sh` and see what arguments it expects. You can also look in
141 the `Makefile` and see how it calls `chain.sh` in the `test` target.
142 
143 
144 \subsection compilation-and-development-subsection-unit-tests Unit tests
145 
146 The unit tests are contained in the `unit/` folder. They are written using the
147 [Catch](https://github.com/philsquared/Catch) unit test framework.
148 
149 If you have compiled with `make`, you can run the unit tests for CBMC directly
150 by going to `unit/`, running `make` to compile the unit tests and then
151 `make test` to run them. You can run the unit tests for JBMC directly by going
152 to `jbmc/unit/` and running the same commands.
153 
154 If you have compiled with CMake, you can run the unit tests for CBMC directly
155 by going to `unit/` and running
156 
157  ../<build-folder>/bin/unit
158 
159 and you can run the unit tests for JBMC directly by going to `jbmc/unit/` and
160 running
161 
162  ../../<build-folder>/bin/java-unit
163 
164 If you have compiled with CMake you can also run the unit tests through CTest,
165 with the names `unit` and `java-unit`. So, from the `build/` directory, run
166 
167  ctest -V -L CORE -R ^unit
168  ctest -V -L CORE -R java-unit
169 
170 to run the CBMC unit tests and the JBMC unit tests respectively. (The `^` is
171 needed to make it a regular expression that matches `unit` but not `java-unit`.)
172 
173 Note that some tests run which are expected to fail - see the summary at
174 the end of the run to see how many tests passed, how many failed which were
175 expected to and how many tests failed which were not expected to.
176 
177 For more information on the structure of `unit/` and how to tag tests, see
178 [the section on unit tests in `CODING_STANDARD.md` in the root of the CBMC
179 repository](https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md#unit-tests)
180 
181 
182 \subsection compilation-and-development-subsection-sat-solver Using a different SAT solver
183 
184 By default, CBMC will assume MiniSat 2 as the SAT back-end. Several other
185 solvers are supported (see also
186 [config.inc](compilation-and-development-subsubsection-config-inc) above). As a
187 more general option, which is not limited to a single SAT solver, you may use
188 the IPASIR interface. For example, to use the SAT solver RISS, proceed as
189 follows:
190 
191 1) Build RISS (in particular its IPASIR configuration):
192 
193  git clone https://github.com/conp-solutions/riss riss.git
194  cd riss.git
195  mkdir build
196  cd build
197  cmake ..
198  make riss-coprocessor-lib-static
199  cd ../..
200 
201 2) Build CBMC while enabling the IPASIR back-end:
202  make -C src IPASIR=../../riss.git/riss \
203  LIBS="../../riss.git/build/lib/libriss-coprocessor.a -lpthread"
204 
205 3) Run CBMC - note that RISS is highly configurable via the RISSCONFIG
206 environment variable:
207  export RISSCONFIG=VERBOSE:BMC1
208  ... run CBMC ...
209 
210 
211 \section compilation-and-development-section-documentation Documentation
212 
213 Apart from the (user-orientated) CBMC user manual and this document, most
214 of the rest of the documentation is inline in the code as `doxygen` and
215 some comments. A man page for CBMC, goto-cc and goto-instrument is
216 contained in the `doc/` directory and gives some options for these
217 tools. All of these could be improved and patches are very welcome. In
218 some cases the algorithms used are described in the relevant papers.
219 
220 The doxygen documentation can be [accessed online](http://cprover.diffblue.com).
221 To build it locally, run `scripts/run_doxygen.sh`. HTML output will be created
222 in `doc/html/`. The index page is `doc/html/index.html`. This script will
223 filter out expected warning messages from doxygen, so that new problems are more
224 obvious. It is important to use the correct version of doxygen, as specified
225 in `run_doxygen.sh`, so that there are no unexpected changes to the list of
226 expected warnings. In the event that any change fixes an old warning, then the
227 corresponding line(s) should be deleted from
228 `scripts/expected_doxygen_warnings.txt`. We want to avoid adding any more
229 warnings to this list of expected warnings, but that can be done to work around
230 limitations in Doxygen (where the code and documentation are completely correct).
231 
232 
233 \section compilation-and-development-section-formatting Formatting
234 
235 The <a
236 href="https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md">
237 `CODING_STANDARD.md`</a> file in the root of the CBMC repository contains
238 guidance on how to write code for the CBMC repository. This includes
239 which language features can be used and formatting rules.
240 
241 C++ code can be automatically reformatted in the correct way by running
242 `clang-format`. There are more details in
243 [CODING_STANDARD.md](https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md#using-clang-format).
244 
245 
246 \section compilation-and-development-section-linting Linting
247 
248 There is also a linting script, `scripts/cpplint.py`. There is a wrapper
249 script to run `cpplint.py` only on lines that differ from another
250 branch, e.g. to run it on lines that have been changed from `develop`:
251 
252  scripts/run_lint.sh develop
253 
254 There are also instructions for adding this as a git pre-commit hook in
255 [CODING_STANDARD.md](https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md#pre-commit-hook-to-run-cpplint-locally).