FreeRTOS/FreeRTOS-Plus/Test/CBMC

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, an open-source static analysis tool (GitHub repository). 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:

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:

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.

• The canonical compilation and installation instructions are in the 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.
  • Download and install the "git for Windows" package, which also provides the patch command, from here.
  • Download the flex and bison for Windows package from this sourceforge site. "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.