diff options
Diffstat (limited to 'FreeRTOS/Test/VeriFast/README.md')
| -rw-r--r-- | FreeRTOS/Test/VeriFast/README.md | 122 |
1 files changed, 122 insertions, 0 deletions
diff --git a/FreeRTOS/Test/VeriFast/README.md b/FreeRTOS/Test/VeriFast/README.md new file mode 100644 index 000000000..f0deecdfc --- /dev/null +++ b/FreeRTOS/Test/VeriFast/README.md @@ -0,0 +1,122 @@ +# FreeRTOS VeriFast proofs + +This directory contains automated functional correctness proofs of the FreeRTOS +kernel queue data structure. These properties are proven with the +[VeriFast](https://github.com/verifast/verifast) verifier. + +## Proof directory structure + +We split proofs by data structure into separate proof directories. Each file +within a proof directory is a proof of one or more related API functions. A +proof is the source code of the FreeRTOS implementation with VeriFast +annotations (denoted by special comments `/*@ ... @*/`). A set of common +predicates, functions and lemmas used by all proofs is maintained in the +`include/proof` directory. + + - `queue`: proofs for the FreeRTOS queue data structure + +The following figure gives the callgraph of the queue proofs. Green=Proven +functions, Blue=Functions modeled by lock invariants (underlying implementation +assumed to provide these atomicity guarantees), Grey=Assumed stubs. + + + +## Prerequisites + +Proof checking needs VeriFast and proof regression further needs make and perl. + +We recommend installing VeriFast from the nightly builds on the [VeriFast +GitHub page](https://github.com/verifast/verifast). After unpacking the build +tarball, the `verifast` and `vfide` binaries will be in the directory +`verifast-COMMIT/bin/` where `COMMIT` is the Git commit of the VeriFast build. + +Note that for CI we use [VeriFast 19.12](https://github.com/verifast/verifast/releases). + +## Proof checking a single proof in the VeriFast IDE + +To load a proof in the `vfide` VeriFast IDE: + +``` +$ /path/to/vfide -I include queue/xQueueGenericSend.c +``` + +Then click `Verify` and `Verify Program` (or press F5). Note that the following +proofs require arithmetic overflow checking to be turned off (click `Verify` +and uncheck `Check arithmetic overflow`). + + - `queue/prvCopyDataToQueue.c` + - `queue/xQueueGenericSendFromISR.c` + - `queue/xQueueReceiveFromISR.c` + +A successful proof results in the top banner turning green with a statement +similar to: `0 errors found (328 statements verified)`. + +## Proof checking a single proof at the command-line + +The following is an example of checking a proof using the `verifast` +command-line tool. Turn off arithmetic overflow checking where necessary with +the flag `-disable_overflow_check`. + +``` +$ /path/to/verifast -I include -c queue/xQueueGenericSend.c +``` + +A successful proof results in output similar to: + +``` +queue/xQueueGenericSend.c +0 errors found (328 statements verified) +``` + +## Running proof regression + +The following will check all proofs in the repo along with a statement coverage +regression. + +``` +$ VERIFAST=/path/to/verifast make +``` + +If you have made changes to the proofs so the statement coverage no longer +matches then you can temporarily turn off coverage checking: + +``` +$ VERIFAST=/path/to/verifast NO_COVERAGE=1 make +``` + +## Annotation burden + +VeriFast can emit statistics about the number of source code lines and +annotations. These range from .3-2x annotations per line of source code. + +``` +$ VERIFAST=/path/to/verifast ./scripts/annotation_overhead.sh +``` + +## Reading a VeriFast proof + +VeriFast is a modular deductive verifier using separation logic. A quick +introduction is given by [Jacobs and +Piessens](https://people.cs.kuleuven.be/~bart.jacobs/verifast/verifast.pdf). +In particular, Section 1 Introduction, gives a high-level overview of the proof +technique, which uses forward symbolic execution over a symbolic heap. + +Learning how to use VeriFast will help you read and understand the proofs. +The VeriFast +[tutorial](https://people.cs.kuleuven.be/~bart.jacobs/verifast/tutorial.pdf) is +a good guide. You will need to understand: + + - Sec 4. Functions and Contracts + - Sec 5. Patterns + - Sec 6. Predicates + - Sec 7. Recursive Predicates + - Sec 8. Loops + - Sec 9. Inductive Datatypes + - Sec 10. Inductive Datatypes + - Sec 11. Lemmas + +## Contributors + +We acknowledge and thank the following contributors, listed alphabetically: + + - Bart Jacobs, KU Leuven, https://people.cs.kuleuven.be/~bart.jacobs/ |