|
|
|
@ -10,118 +10,73 @@ 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.
|
|
|
|
|
how to run the proofs on your local clone of FreeRTOS.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Bulding and running proofs
|
|
|
|
|
Building 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.
|
|
|
|
|
Currently, only python based builds are supported for the CBMC proofs. The proofs
|
|
|
|
|
can be run on Linux and MacOS. Windows users can use [WSL](https://docs.microsoft.com/en-us/windows/wsl).
|
|
|
|
|
The below section outlines the instructions for the Python based build.
|
|
|
|
|
|
|
|
|
|
### Prerequisites
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
```
|
|
|
|
|
On Windows, you can install WSL using these simple [instructions](https://docs.microsoft.com/en-us/windows/wsl/install).
|
|
|
|
|
|
|
|
|
|
You will need Python version >= 3.7.
|
|
|
|
|
And you will need Make to build and run the proofs.
|
|
|
|
|
|
|
|
|
|
If you are running on a 64-bit machine, please install the 32-bit version of gcc
|
|
|
|
|
libraires. For example, on linux, one would run the following command to install
|
|
|
|
|
the libraries: `sudo apt-get install gcc-multilib`
|
|
|
|
|
|
|
|
|
|
Python-based build
|
|
|
|
|
------------------
|
|
|
|
|
### Installing CBMC
|
|
|
|
|
|
|
|
|
|
### Prerequisites
|
|
|
|
|
- The latest installation instructions can be found on the
|
|
|
|
|
[releases](https://github.com/diffblue/cbmc/releases) page of the CBMC repository.
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
- Please follow all the installation instructions given for your platform.
|
|
|
|
|
|
|
|
|
|
- Ensure that you can run the programs `cbmc`, `goto-cc` (or `goto-cl`
|
|
|
|
|
on Windows), and `goto-instrument` from the command line. If you cannot run these
|
|
|
|
|
commands, please refer to the above instructions to install CBMC.
|
|
|
|
|
|
|
|
|
|
### Installing CBMC
|
|
|
|
|
### Installing CBMC-viewer (to generate the report)
|
|
|
|
|
|
|
|
|
|
- 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
|
|
|
|
|
```
|
|
|
|
|
- The latest installation instructions can be found on the
|
|
|
|
|
[releases](https://github.com/awslabs/aws-viewer-for-cbmc/releases) page of the CBMC-viewer repository.
|
|
|
|
|
|
|
|
|
|
- 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.
|
|
|
|
|
- Please follow all the installation instructions given for your platform.
|
|
|
|
|
|
|
|
|
|
- Ensure that you can run the programs `cbmc-viewer`. If not, please verify
|
|
|
|
|
that all instructions above have been followed.
|
|
|
|
|
|
|
|
|
|
### Setting up the proofs
|
|
|
|
|
|
|
|
|
|
Change into the `proofs` directory. On Windows, run
|
|
|
|
|
```
|
|
|
|
|
python prepare.py
|
|
|
|
|
```
|
|
|
|
|
On macOS or Linux, run
|
|
|
|
|
Make sure that all the submodules of the FreeRTOS repository have been cloned. To
|
|
|
|
|
clone all the submodules, go to the root of the FreeRTOS repository and run this
|
|
|
|
|
command: `git submodule update --init --recursive --checkout`.
|
|
|
|
|
|
|
|
|
|
Change into the `proofs` directory and run
|
|
|
|
|
```
|
|
|
|
|
./prepare.py
|
|
|
|
|
python3 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.
|
|
|
|
|
run a proof, change into the directory for that proof and run `make`.
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
The make command will also generate a report in html and json format which makes
|
|
|
|
|
understanding the failures easier.
|
|
|
|
|
|
|
|
|
|
### Proof directory structure
|
|
|
|
|
|
|
|
|
@ -129,5 +84,6 @@ 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
|
|
|
|
|
running the proofs. The patches are used to remove static and volatile qulaifiers
|
|
|
|
|
from the source.
|
|
|
|
|
- `include` and `windows` contain header files used by the proofs.
|
|
|
|
|