build(tools/cbmc): integrate cbmc-viewer
Add option to the build system to call cbmc-viewer. The following
changes were necessary:
- Add option to make call of cbmc-viewer optional
- Update CBMC Application note with cbmc-viewer
- Separate CBMC run to 2 steps: compiling to GOTO program, and call
CBMC on the resulting goto program. This is necessary becasue
cbmc-viewer operates on the GOTO program.
- Rewrite extraction of summary, as XML output (required by CBMC) files
doesn't contain summary
Change-Id: Ieb2623d3b03845dcb4ab74baead81d3c0fc6dee8
Signed-off-by: Mate Toth-Pal <mate.toth-pal@arm.com>
diff --git a/docs/getting_started/build-options.rst b/docs/getting_started/build-options.rst
index 6dab78d..de0e8cc 100644
--- a/docs/getting_started/build-options.rst
+++ b/docs/getting_started/build-options.rst
@@ -281,6 +281,7 @@
HOST_MEM_SIZE , ,0x40000000 ,"Host memory size that will be used as physical granules"
RMM_COVERAGE ,ON | OFF ,OFF ,"Enable coverage analysis"
RMM_HTML_COV_REPORT ,ON | OFF ,ON ,"Enable HTML output report for coverage analysis"
+ RMM_CBMC_VIEWER_OUTPUT ,ON | OFF ,OFF ,"Generate report of CBMC results using the tool cbmc-viewer"
.. _llvm_build:
diff --git a/docs/resources/application-notes/cbmc.rst b/docs/resources/application-notes/cbmc.rst
index 01378f6..0564ef3 100644
--- a/docs/resources/application-notes/cbmc.rst
+++ b/docs/resources/application-notes/cbmc.rst
@@ -57,7 +57,7 @@
with their respective build targets.
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
@@ -66,7 +66,7 @@
To use this mode the target ``cbmc-assert`` must be passed to the build command.
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,
@@ -79,7 +79,7 @@
command.
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
@@ -96,10 +96,48 @@
For all the modes the summary files are committed in the source tree as
baseline in ``tools/cbmc/testbenches_results/BASELINE.${MODE}``.
+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:
+
+.. code-block:: bash
+
+ python3 -m pip install cbmc-viewer
+
+For further details and installation guide on cbmc-viewer please see the
+`cbmc-viewer github page`_.
+
+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`_.
+
-----
.. _CBMC Home: https://www.cprover.org/cbmc/
.. _Writing a good proof: https://model-checking.github.io/cbmc-training/management/Write-a-good-proof.html
.. _github release page: https://github.com/diffblue/cbmc/releases
.. _Automatically Generating Properties: https://www.cprover.org/cprover-manual/properties/
-
+.. _cbmc-viewer github page: https://github.com/model-checking/cbmc-viewer
+.. _CBMC proof debugger in the editor's extensions page: https://marketplace.visualstudio.com/items?itemName=model-checking.cbmc-proof-debugger