From 9b7911b046c018746cbb23c96d58796dcb7bc712 Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Thu, 3 Mar 2022 11:50:35 -0800 Subject: [PATCH] Update readme file with latest instructions to run CBMC proofs (#801) * Update readme * Address comments * Update instructions according to comments * Remove windows based instructions * Add details for CBMC-viewer --- FreeRTOS/Test/CBMC/README.md | 120 +++++++++++------------------------ 1 file changed, 38 insertions(+), 82 deletions(-) diff --git a/FreeRTOS/Test/CBMC/README.md b/FreeRTOS/Test/CBMC/README.md index 09d5e14810..00baa4423a 100644 --- a/FreeRTOS/Test/CBMC/README.md +++ b/FreeRTOS/Test/CBMC/README.md @@ -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.