CBMC Proof Infrastructure
This directory contains automated proofs of the memory safety of various parts of the amazon: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.
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.
Follow the CBMC installation instructions below.
Suppose that the amazon-freertos source tree is located at
~/src/amazon-freertos and you wish to build the proofs into
~/build/amazon-freertos. The following three commands build and run
cmake -S~/src/amazon-freertos -B~/build/amazon-freertos -DCOMPILER=cbmc -DBOARD=windows -DVENDOR=pc cmake --build ~/build/amazon-freertos --target all-proofs cd ~/build/amazon-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/amazon-freertos \ ~/build/amazon-freertos \ --build-target cbmc \ --build-generator Ninja \ --build-options \ -DCOMPILER=cbmc \ -DBOARD=windows \ -DVENDOR=pc \ --test-command ctest -j4 -L cbmc --output-on-failure
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.
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
patchcommand, 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
goto-clon Windows), and
goto-instrumentfrom the command line. If you build CBMC with CMake, the programs will have been installed under the
build/bin/Debugdirectory under the top-level
cbmcdirectory; you should add that directory to your
$PATH. If you built CBMC using Make, then those programs will have been installed in the
Setting up the proofs
Change into the
proofs directory. On Windows, run
On macOS or Linux, run
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
Running the proofs
Each of the leaf directories under
proofs is a proof of the memory
safety of a single entry point in a:FR. 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
make on Linux or macOS. The proofs may take some time to
run; they eventually write their output to
cbmc.txt, which should have
VERIFICATION SUCCESSFUL at the end.
Proof directory structure
This directory contains the following subdirectories:
proofscontains the proofs run against each pull request
patchescontains a set of patches that get applied to the codebase prior to running the proofs
windowscontain header files used by the proofs.