blob: f0deecdfc4c8a20854f5aa19d0c0d91b9cf8a82f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
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/
|
