1.. SPDX-License-Identifier: BSD-3-Clause
2.. SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
3
4****
5CBMC
6****
7
8CBMC is a Bounded Model Checker for C and C++ programs. For details see
9`CBMC Home`_
10
11CBMC in RMM
12===========
13
14CBMC needs to be run on a C program that has a single entry point. To test all
15the RMM ABI commands, for each command a testbench file is created. These files
16are generated by a script offline from the RMM MRS (Machine Readable
17Specification), and committed to the RMM repository under the folder
18``tools/cbmc/testbenches``
19
20.. note::
21
22    Currently only a subset of the ABI calls have a testbench implemented. Also
23    there are errors reported by CBMC for some of the testbenches. Further
24    testbenches and fixes are expected to be added later.
25
26These files contain asserts that correspond to
27the Faliure and Success conditions defined in the RMM specification. To read on
28further how such a file should be defined please refer to
29`Writing a good proof`_
30
31The recommended way for installing CBMC is via the pre-built package found at
32the `github release page`_. The same page contains the instructions for
33installing the different release packages.
34
35An example install command for Ubuntu linux is
36
37.. code-block:: bash
38
39    dpkg -i ubuntu-20.04-cbmc-5.95.1-Linux.deb
40
41The invocation of CBMC tool is integrated in the RMM CMake system. CBMC analysis
42can be run by passing specific targets (detailed later) to the build command. to
43make the targets available the RMM build must be configured with
44``-DRMM_CONFIG=host_defcfg -DHOST_VARIANT=host_cbmc`` options.
45
46The results of a CBMC run are generated in the
47``${RMM_BUILD_DIR}/tools/cbmc/cbmc_${MODE}_results`` directory. There are 3
48files, ``${TESTBENCH_FILE_NAME}.${MODE}.[cmd|error|output]`` generated for each
49RMM ABI under test, each one containing the CBMC command line, the CBMC
50executable's output to the standard error, and the output to the standard out
51respectively. There is also a single ``SUMMARY.${MODE}`` file is generated for
52each build.
53
54For an example build command please refer to :ref:`RMM Build Examples`
55
56The CMake system by default runs CBMC on all the testbenches. This can take a
57long time, and it can be convenient to run a single testcase at once. This can
58be achieved using the option ``-DRMM_CBMC_SINGLE_TESTBENCH="testbench_name"``.
59The list of possible ``testbench_name``s can be listed by using the option
60``-DRMM_CBMC_SINGLE_TESTBENCH="help"``.
61
62The CMake system provides different modes in which CBMC can be called, along
63with their respective build targets.
64
65CBMC Assert
66-----------
67
68In this mode CBMC is configured, so that it tries to find inputs that makes an
69assertion in the code to fail. If there is such an input, then CBMC provides a
70trace that leads to that assertion failure.
71
72To use this mode the target ``cbmc-assert`` must be passed to the build command.
73
74CBMC Analysis
75-------------
76
77In this mode CBMC is configured to generate assertions for certain properties in
78the code. The properties are selected so that for example no buffer overflows,
79or arithmetic overflow errors can happen in the code. For more details please
80refer to `Automatically Generating Properties`_.
81Then CBMC is run in a configuration similar to the Assert mode, except that this
82time traces are not generated.
83
84To use this mode the target ``cbmc-analysis`` must be passed to the build
85command.
86
87CBMC Coverage
88-------------
89
90This mode checks whether all the conditions for an ABI function are covered.
91The pre and post conditions for the command are expressed as boolean values in
92the testbench, and a ``__CPROVER_cover()`` macro is added for each condition
93that is expressed with the pre and post conditions. CBMC is configured to try
94to generate an input for each ``__CPROVER_cover()`` call that makes the code
95reach that call.
96
97To use this mode the target ``cbmc-coverage`` must be passed to the build
98command.
99
100.. note::
101
102    For all the modes the summary files are committed in the source tree as
103    baseline in ``tools/cbmc/testbenches_results/BASELINE.${MODE}``.
104
105Build The CBMC testbench with GCC
106---------------------------------
107
108In the RMM CMake system there is an option to build the CBMC testbench with GCC
109compiler. The resulting binary doesn't have any particular value, however during
110the compilation GCC may flag errors that can cause CBMC work unexpectedly. For
111example functions that are defined in a file that is linked during the CBMC
112build, however not declared, due to a missing include. In this case CBMC seems
113to be silently ignoring the function body. This error is quite difficult to find
114using only CBMC output.
115
116To use this mode the target ``cbmc-gcc`` must be passed to the build command.
117
118cbmc-viewer
119===========
120
121cbmc-viewer is a python package that can parse the XML output of CBMC. It
122generates a html report that can be opened in a browser. The report contains a
123collapsible representation of assert traces, and clickable links to the source
124code locations associated with a specific trace item.
125
126The RMM cmake build system is capable of generating the cbmc-viewer report. If
127the option ``-DRMM_CBMC_VIEWER_OUTPUT=ON`` is passed to the RMM Cmake
128configuration command then the Cmake system calls cbmc-viewer and generates the
129report under ``${RMM_BUILD_DIR}/tools/cbmc/cbmc_${MODE}_results/report``
130
131Please note that the CMake build system currently only generates report for the
132``cbmc-assert`` target. The ``cbmc-coverage`` and ``cbmc-analysis`` targets
133doesn't generate trace, so generating a report wouldn't be useful.
134
135``cbmc-viewer`` can be installed using the following command:
136
137.. code-block:: bash
138
139    python3 -m pip install cbmc-viewer
140
141For further details and installation guide on cbmc-viewer please see the
142`cbmc-viewer github page`_.
143
144CBMC proof debugger
145===================
146
147CBMC proof debugger is an extension to a popular code editor that can be used to
148load the json summaries of a CBMC analysis that is generated by cbmc-viewer.
149The trace then can be explored in the built in debugger of the editor as if
150stepping through an actual code execution.
151
152For further details on installing and using the extension please see
153`CBMC proof debugger in the editor's extensions page`_.
154
155-----
156
157.. _CBMC Home: https://www.cprover.org/cbmc/
158.. _Writing a good proof: https://model-checking.github.io/cbmc-training/management/Write-a-good-proof.html
159.. _github release page: https://github.com/diffblue/cbmc/releases
160.. _Automatically Generating Properties: https://www.cprover.org/cprover-manual/properties/
161.. _cbmc-viewer github page: https://github.com/model-checking/cbmc-viewer
162.. _CBMC proof debugger in the editor's extensions page: https://marketplace.visualstudio.com/items?itemName=model-checking.cbmc-proof-debugger
163