xref: /FreeRTOS-Plus-TCP-v4.0.0/test/cbmc/README.md (revision dfe2e90ad7488c5ecfea69e095105e590f2ab006) 
1CBMC Proof Infrastructure
2=========================
3
4This directory contains automated proofs of the memory safety of various parts
5of the FreeRTOS codebase. A continuous integration system validates every
6pull request posted to the repository against these proofs, and developers can
7also run the proofs on their local machines.
8
9The proofs are checked using the
10[C Bounded Model Checker](http://www.cprover.org/cbmc/), an open-source static
11analysis tool
12([GitHub repository](https://github.com/diffblue/cbmc)). This README describes
13how to run the proofs on your local clone of a:FR.
14
15
16Bulding and running proofs
17--------------------------
18
19For historical reasons, some of the proofs are built and run using CMake
20and CTest. Others use a custom python-based build system. New proofs
21should use CMake. This README describes how to build and run both kinds
22of proof.
23
24
25CMake-based build
26-----------------
27
28Follow the CBMC installation instructions below.
29
30Suppose that the freertos source tree is located at
31`~/src/freertos` and you wish to build the proofs into
32`~/build/freertos`. The following three commands build and run
33the proofs:
34
35```sh
36cmake -S~/src/freertos -B~/build/freertos -DCOMPILER=cbmc
37-DBOARD=windows -DVENDOR=pc
38cmake --build ~/build/freertos --target all-proofs
39cd ~/build/freertos && ctest -L cbmc
40```
41
42Alternatively, this single command does the same thing, assuming you
43have the Ninja build tool installed:
44
45```sh
46ctest --build-and-test                \
47    ~/src/freertos             \
48    ~/build/freertos           \
49    --build-target cbmc               \
50    --build-generator Ninja           \
51    --build-options                   \
52      -DCOMPILER=cbmc                 \
53      -DBOARD=windows                 \
54      -DVENDOR=pc                     \
55    --test-command ctest -j4 -L cbmc --output-on-failure
56```
57
58
59
60Python-based build
61------------------
62
63### Prerequisites
64
65You will need Python 3. On Windows, you will need Visual Studio 2015 or later
66(in particular, you will need the Developer Command Prompt and NMake). On macOS
67and Linux, you will need Make.
68
69
70### Installing CBMC
71
72- Clone the [CBMC repository](https://github.com/diffblue/cbmc).
73
74- The canonical compilation and installation instructions are in the
75  [COMPILING.md](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md)
76  file in the CBMC repository; we reproduce the most important steps for
77  Windows users here, but refer to that document if in doubt.
78  - Download and install CMake from the [CMake website](https://cmake.org/download).
79  - Download and install the "git for Windows" package, which also
80    provides the `patch` command, from [here](https://git-scm.com/download/win).
81  - Download the flex and bison for Windows package from
82    [this sourceforge site](https://sourceforge.net/projects/winflexbison).
83    "Install" it by dropping the contents of the entire unzipped
84    package into the top-level CBMC source directory.
85  - Change into the top-level CBMC source directory and run
86    ```
87    cmake -H. -Bbuild -DCMAKE_BUILD_TYPE=Release -DWITH_JBMC=OFF
88    cmake --build build
89    ```
90
91- Ensure that you can run the programs `cbmc`, `goto-cc` (or `goto-cl`
92  on Windows), and `goto-instrument` from the command line. If you build
93  CBMC with CMake, the programs will have been installed under the
94  `build/bin/Debug` directory under the top-level `cbmc` directory; you
95  should add that directory to your `$PATH`. If you built CBMC using
96  Make, then those programs will have been installed in the `src/cbmc`,
97  `src/goto-cc`, and `src/goto-instrument` directories respectively.
98
99
100### Setting up the proofs
101
102Change into the `proofs` directory. On Windows, run
103```
104python prepare.py
105```
106On macOS or Linux, run
107```
108./prepare.py
109```
110If you are on a Windows machine but want to generate Linux Makefiles (or vice
111versa), you can pass the `--system linux` or `--system windows` options to those
112programs.
113
114
115### Running the proofs
116
117Each of the leaf directories under `proofs` is a proof of the memory
118safety of a single entry point in FreeRTOS. The scripts that you ran in the
119previous step will have left a Makefile in each of those directories. To
120run a proof, change into the directory for that proof and run `nmake` on
121Windows or `make` on Linux or macOS. The proofs may take some time to
122run; they eventually write their output to `cbmc.txt`, which should have
123the text `VERIFICATION SUCCESSFUL` at the end.
124
125
126### Proof directory structure
127
128This directory contains the following subdirectories:
129
130- `proofs` contains the proofs run against each pull request
131- `patches` contains a set of patches that get applied to the codebase prior to
132  running the proofs
133- `include` and `windows` contain header files used by the proofs.
134