begriffs open source - cmsis-freertos/blob - Test/VeriFast/README.md

   1 # FreeRTOS VeriFast proofs
   2
   3 This directory contains unbounded proofs of the FreeRTOS kernel queue and list
   4 data structures. Unbounded proofs mean that these results hold independent of
   5 the length of the queue or list.
   6
   7 Informally, the queue proofs demonstrate that the queue implementation is
   8 memory safe (does not access invalid memory), thread safe (properly
   9 synchronizes accesses) and functionally correct (behaves like a queue) under
  10 any arbitrary number of tasks or ISRs. The list proofs demonstrate that the
  11 list implementation is memory safe and functionally correct.
  12
  13 These properties are proven with the
  14 [VeriFast](https://github.com/verifast/verifast) verifier. See the proof
  15 [signoff](docs/signoff.md) document for more on the proof properties,
  16 assumptions, and simplifications.
  17
  18 ## Proof directory structure
  19
  20 We split proofs by data structure into separate proof directories. Each file
  21 within a proof directory is a proof of one or more related API functions. A
  22 proof is the source code of the FreeRTOS implementation with VeriFast
  23 annotations (denoted by special comments `/*@ ... @*/`). A set of common
  24 predicates, functions and lemmas used by all proofs is maintained in the
  25 `include/proof` directory.
  26
  27   - `queue`: proofs for the FreeRTOS queue data structure
  28   - `list`: proofs for the FreeRTOS list data structure
  29
  30 The following figure gives the callgraph of the queue proofs. Green=Proven
  31 functions, Blue=Functions modeled by lock invariants (underlying implementation
  32 assumed to provide these atomicity guarantees), Grey=Assumed stubs.
  33
  34 ![Queue proof callgraph](docs/callgraph.png?raw=true "Queue proofs")
  35
  36 ## Prerequisites
  37
  38 Proof checking needs VeriFast and proof regression further needs make and perl.
  39
  40 We recommend installing VeriFast from the nightly builds on the [VeriFast
  41 GitHub page](https://github.com/verifast/verifast). After unpacking the build
  42 tarball, the `verifast` and `vfide` binaries will be in the directory
  43 `verifast-COMMIT/bin/` where `COMMIT` is the Git commit of the VeriFast build.
  44
  45 Note that for CI we use [VeriFast 19.12](https://github.com/verifast/verifast/releases).
  46
  47 ## Proof checking a single proof in the VeriFast IDE
  48
  49 To load a proof in the `vfide` VeriFast IDE:
  50
  51 ```
  52 $ /path/to/vfide -I include queue/xQueueGenericSend.c
  53 ```
  54
  55 Then click `Verify` and `Verify Program` (or press F5). Note that the following
  56 proofs require arithmetic overflow checking to be turned off (click `Verify`
  57 and uncheck `Check arithmetic overflow`).
  58
  59   - `queue/prvCopyDataToQueue.c`
  60   - `queue/xQueueGenericSendFromISR.c`
  61   - `queue/xQueueReceiveFromISR.c`
  62
  63 A successful proof results in the top banner turning green with a statement
  64 similar to: `0 errors found (335 statements verified)`.
  65
  66 ## Proof checking a single proof at the command-line
  67
  68 The following is an example of checking a proof using the `verifast`
  69 command-line tool. Turn off arithmetic overflow checking where necessary with
  70 the flag `-disable_overflow_check`.
  71
  72 ```
  73 $ /path/to/verifast -I include -c queue/xQueueGenericSend.c
  74 ```
  75
  76 A successful proof results in output similar to:
  77
  78 ```
  79 queue/xQueueGenericSend.c
  80 0 errors found (335 statements verified)
  81 ```
  82
  83 ## Running proof regression
  84
  85 The following will check all proofs in the repo along with a statement coverage
  86 regression.
  87
  88 ```
  89 $ VERIFAST=/path/to/verifast make
  90 ```
  91
  92 If you have made changes to the proofs so the statement coverage no longer
  93 matches then you can temporarily turn off coverage checking:
  94
  95 ```
  96 $ VERIFAST=/path/to/verifast NO_COVERAGE=1 make
  97 ```
  98
  99 ## Annotation burden
 100
 101 VeriFast can emit statistics about the number of source code lines and
 102 annotations. These range from .3-2x annotations per line of source code for the
 103 queue proofs and up to 7x for the list proofs.
 104
 105 ```
 106 $ VERIFAST=/path/to/verifast ./scripts/annotation_overhead.sh
 107 ```
 108
 109 ## Reading a VeriFast proof
 110
 111 VeriFast is a modular deductive verifier using separation logic. A quick
 112 introduction is given by [Jacobs and Piessens][1]. In particular, Section 1
 113 Introduction, gives a high-level overview of the proof technique, which uses
 114 forward symbolic execution over a symbolic heap.
 115
 116 Learning how to use VeriFast will help you read and understand the proofs. The
 117 VeriFast [tutorial][2] is a good guide. You will need to understand:
 118
 119   - Sec 4. Functions and Contracts
 120   - Sec 5. Patterns
 121   - Sec 6. Predicates
 122   - Sec 7. Recursive Predicates
 123   - Sec 8. Loops
 124   - Sec 9. Inductive Datatypes
 125   - Sec 10. Inductive Datatypes
 126   - Sec 11. Lemmas
 127
 128 [1]: https://people.cs.kuleuven.be/~bart.jacobs/verifast/verifast.pdf
 129 [2]: https://people.cs.kuleuven.be/~bart.jacobs/verifast/tutorial.pdf
 130
 131 ## Contributors
 132
 133 We acknowledge and thank the following contributors:
 134
 135   - Bart Jacobs, KU Leuven, https://people.cs.kuleuven.be/~bart.jacobs/
 136   - Aalok Thakkar, University of Pennsylvania, https://aalok-thakkar.github.io/