1.1. CBMC
CBMC is a Bounded Model Checker for C and C++ programs. For details see CBMC Home
1.1.1. CBMC in RMM
CBMC needs to be run on a C program that has a single entry point. To test all
the RMM ABI commands, for each command a testbench file is created. These files
are generated by a script offline from the RMM MRS (Machine Readable
Specification), and committed to the RMM repository under the folder
tools/cbmc/testbenches
Note
Currently only a subset of the ABI calls have a testbench implemented. Also there are errors reported by CBMC for some of the testbenches. Further testbenches and fixes are expected to be added later.
These files contain asserts that correspond to the Faliure and Success conditions defined in the RMM specification. To read on further how such a file should be defined please refer to Writing a good proof
The recommended way for installing CBMC is via the pre-built package found at the github release page. The same page contains the instructions for installing the different release packages.
An example install command for Ubuntu linux is
dpkg -i ubuntu-20.04-cbmc-5.95.1-Linux.deb
The invocation of CBMC tool is integrated in the RMM CMake system. CBMC analysis
can be run by passing specific targets (detailed later) to the build command. to
make the targets available the RMM build must be configured with
-DRMM_CONFIG=host_defcfg -DHOST_VARIANT=host_cbmc
options.
The results of a CBMC run are generated in the
${RMM_BUILD_DIR}/tools/cbmc/cbmc_${MODE}_results
directory. There are 3
files, ${TESTBENCH_FILE_NAME}.${MODE}.[cmd|error|output]
generated for each
RMM ABI under test, each one containing the CBMC command line, the CBMC
executable’s output to the standard error, and the output to the standard out
respectively. There is also a single SUMMARY.${MODE}
file is generated for
each build.
For an example build command please refer to RMM Build Examples
The CMake system by default runs CBMC on all the testbenches. This can take a
long time, and it can be convenient to run a single testcase at once. This can
be achieved using the option -DRMM_CBMC_SINGLE_TESTBENCH="testbench_name"
.
The list of possible testbench_name``s can be listed by using the option
``-DRMM_CBMC_SINGLE_TESTBENCH="help"
.
The CMake system provides different modes in which CBMC can be called, along with their respective build targets.
1.1.1.1. CBMC Assert
In this mode CBMC is configured, so that it tries to find inputs that makes an assertion in the code to fail. If there is such an input, then CBMC provides a trace that leads to that assertion failure.
To use this mode the target cbmc-assert
must be passed to the build command.
1.1.1.2. CBMC Analysis
In this mode CBMC is configured to generate assertions for certain properties in the code. The properties are selected so that for example no buffer overflows, or arithmetic overflow errors can happen in the code. For more details please refer to Automatically Generating Properties. Then CBMC is run in a configuration similar to the Assert mode, except that this time traces are not generated.
To use this mode the target cbmc-analysis
must be passed to the build
command.
1.1.1.3. CBMC Coverage
This mode checks whether all the conditions for an ABI function are covered.
The pre and post conditions for the command are expressed as boolean values in
the testbench, and a __CPROVER_cover()
macro is added for each condition
that is expressed with the pre and post conditions. CBMC is configured to try
to generate an input for each __CPROVER_cover()
call that makes the code
reach that call.
To use this mode the target cbmc-coverage
must be passed to the build
command.
Note
For all the modes the summary files are committed in the source tree as
baseline in tools/cbmc/testbenches_results/BASELINE.${MODE}
.
1.1.1.4. Build The CBMC testbench with GCC
In the RMM CMake system there is an option to build the CBMC testbench with GCC compiler. The resulting binary doesn’t have any particular value, however during the compilation GCC may flag errors that can cause CBMC work unexpectedly. For example functions that are defined in a file that is linked during the CBMC build, however not declared, due to a missing include. In this case CBMC seems to be silently ignoring the function body. This error is quite difficult to find using only CBMC output.
To use this mode the target cbmc-gcc
must be passed to the build command.
1.1.2. cbmc-viewer
cbmc-viewer is a python package that can parse the XML output of CBMC. It generates a html report that can be opened in a browser. The report contains a collapsible representation of assert traces, and clickable links to the source code locations associated with a specific trace item.
The RMM cmake build system is capable of generating the cbmc-viewer report. If
the option -DRMM_CBMC_VIEWER_OUTPUT=ON
is passed to the RMM Cmake
configuration command then the Cmake system calls cbmc-viewer and generates the
report under ${RMM_BUILD_DIR}/tools/cbmc/cbmc_${MODE}_results/report
Please note that the CMake build system currently only generates report for the
cbmc-assert
target. The cbmc-coverage
and cbmc-analysis
targets
doesn’t generate trace, so generating a report wouldn’t be useful.
cbmc-viewer
can be installed using the following command:
python3 -m pip install cbmc-viewer
For further details and installation guide on cbmc-viewer please see the cbmc-viewer github page.
1.1.3. CBMC proof debugger
CBMC proof debugger is an extension to a popular code editor that can be used to load the json summaries of a CBMC analysis that is generated by cbmc-viewer. The trace then can be explored in the built in debugger of the editor as if stepping through an actual code execution.
For further details on installing and using the extension please see CBMC proof debugger in the editor’s extensions page.