diff options
Diffstat (limited to 'FreeRTOS/Test/CBMC/README.md')
| -rw-r--r-- | FreeRTOS/Test/CBMC/README.md | 133 |
1 files changed, 133 insertions, 0 deletions
diff --git a/FreeRTOS/Test/CBMC/README.md b/FreeRTOS/Test/CBMC/README.md new file mode 100644 index 000000000..09d5e1481 --- /dev/null +++ b/FreeRTOS/Test/CBMC/README.md @@ -0,0 +1,133 @@ +CBMC Proof Infrastructure +========================= + +This directory contains automated proofs of the memory safety of various parts +of the FreeRTOS codebase. A continuous integration system validates every +pull request posted to the repository against these proofs, and developers can +also run the proofs on their local machines. + +The proofs are checked using the +[C Bounded Model Checker](http://www.cprover.org/cbmc/), an open-source static +analysis tool +([GitHub repository](https://github.com/diffblue/cbmc)). This README describes +how to run the proofs on your local clone of a:FR. + + +Bulding and running proofs +-------------------------- + +For historical reasons, some of the proofs are built and run using CMake +and CTest. Others use a custom python-based build system. New proofs +should use CMake. This README describes how to build and run both kinds +of proof. + + +CMake-based build +----------------- + +Follow the CBMC installation instructions below. + +Suppose that the freertos source tree is located at +`~/src/freertos` and you wish to build the proofs into +`~/build/freertos`. The following three commands build and run +the proofs: + +```sh +cmake -S~/src/freertos -B~/build/freertos -DCOMPILER=cbmc +-DBOARD=windows -DVENDOR=pc +cmake --build ~/build/freertos --target all-proofs +cd ~/build/freertos && ctest -L cbmc +``` + +Alternatively, this single command does the same thing, assuming you +have the Ninja build tool installed: + +```sh +ctest --build-and-test \ + ~/src/freertos \ + ~/build/freertos \ + --build-target cbmc \ + --build-generator Ninja \ + --build-options \ + -DCOMPILER=cbmc \ + -DBOARD=windows \ + -DVENDOR=pc \ + --test-command ctest -j4 -L cbmc --output-on-failure +``` + + + +Python-based build +------------------ + +### Prerequisites + +You will need Python 3. On Windows, you will need Visual Studio 2015 or later +(in particular, you will need the Developer Command Prompt and NMake). On macOS +and Linux, you will need Make. + + +### Installing CBMC + +- Clone the [CBMC repository](https://github.com/diffblue/cbmc). + +- The canonical compilation and installation instructions are in the + [COMPILING.md](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md) + file in the CBMC repository; we reproduce the most important steps for + Windows users here, but refer to that document if in doubt. + - Download and install CMake from the [CMake website](https://cmake.org/download). + - Download and install the "git for Windows" package, which also + provides the `patch` command, from [here](https://git-scm.com/download/win). + - Download the flex and bison for Windows package from + [this sourceforge site](https://sourceforge.net/projects/winflexbison). + "Install" it by dropping the contents of the entire unzipped + package into the top-level CBMC source directory. + - Change into the top-level CBMC source directory and run + ``` + cmake -H. -Bbuild -DCMAKE_BUILD_TYPE=Release -DWITH_JBMC=OFF + cmake --build build + ``` + +- Ensure that you can run the programs `cbmc`, `goto-cc` (or `goto-cl` + on Windows), and `goto-instrument` from the command line. If you build + CBMC with CMake, the programs will have been installed under the + `build/bin/Debug` directory under the top-level `cbmc` directory; you + should add that directory to your `$PATH`. If you built CBMC using + Make, then those programs will have been installed in the `src/cbmc`, + `src/goto-cc`, and `src/goto-instrument` directories respectively. + + +### Setting up the proofs + +Change into the `proofs` directory. On Windows, run +``` +python prepare.py +``` +On macOS or Linux, run +``` +./prepare.py +``` +If you are on a Windows machine but want to generate Linux Makefiles (or vice +versa), you can pass the `--system linux` or `--system windows` options to those +programs. + + +### Running the proofs + +Each of the leaf directories under `proofs` is a proof of the memory +safety of a single entry point in FreeRTOS. The scripts that you ran in the +previous step will have left a Makefile in each of those directories. To +run a proof, change into the directory for that proof and run `nmake` on +Windows or `make` on Linux or macOS. The proofs may take some time to +run; they eventually write their output to `cbmc.txt`, which should have +the text `VERIFICATION SUCCESSFUL` at the end. + + +### Proof directory structure + +This directory contains the following subdirectories: + +- `proofs` contains the proofs run against each pull request +- `patches` contains a set of patches that get applied to the codebase prior to + running the proofs +- `include` and `windows` contain header files used by the proofs. |