Skip to content

Commit e137210

Browse files
btjbtj
committed
Add a VeriFast tool chapter to the book
1 parent 685cb48 commit e137210

File tree

3 files changed

+187
-0
lines changed

3 files changed

+187
-0
lines changed

‎doc/src/SUMMARY.md

+1
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@
88

99
- [Verification Tools](./tools.md)
1010
- [Kani](./tools/kani.md)
11+
- [VeriFast](./tools/verifast.md)
1112

1213

1314
---

‎doc/src/tools.md

+1
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ please see the [Tool Application](general-rules.md#tool-applications) section.
1212
| Tool | CI Status |
1313
|---------------------|-------|
1414
| Kani Rust Verifier | [![Kani](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml) |
15+
| VeriFast for Rust | [![VeriFast](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml) |
1516

1617

1718

‎doc/src/tools/verifast.md

+185
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,185 @@
1+
# VeriFast for Rust
2+
3+
[VeriFast](https://github.com/verifast/verifast) is a tool for verifying the
4+
absence of [undefined
5+
behavior](https://doc.rust-lang.org/reference/behavior-considered-undefined.html)
6+
in single-threaded or multithreaded Rust programs that use `unsafe` blocks, and
7+
for verifying
8+
[soundness](https://doc.rust-lang.org/nomicon/working-with-unsafe.html) of Rust
9+
crates/modules that use `unsafe` blocks. VeriFast performs *modular
10+
verification*: it verifies one function at a time; during the verification of
11+
one function, if that function calls another function, VeriFast uses the
12+
callee's *specification*, not its implementation, to reason about the call.
13+
VeriFast verifies each function against its specification: it verifies that, if
14+
started in a state that satisfies the precondition, the function does not have
15+
undefined behavior and any state in which it returns satisfies the
16+
postcondition.
17+
18+
Besides requiring that the user annotate each function with a precondition and
19+
a postcondition, VeriFast also requires that the user annotate each loop with a
20+
loop invariant. This enables its modular symbolic execution algorithm to
21+
perform only a single symbolic execution of the loop's body to cover all
22+
possible real executions of the loop. Furthermore, the use of function
23+
specifications means a single symbolic execution of a function covers all
24+
possible real executions, even if the function is recursive. In summary, these
25+
annotations enable VeriFast to perform unbounded verification (i.e. of
26+
arbitrarily long, including infinitely long, executions) in finite time.
27+
28+
VeriFast function specifications and loop invariants are expressed in a form of
29+
[*separation logic*](https://en.wikipedia.org/wiki/Separation_logic), and it
30+
performs symbolic execution using a separation logic-based representation of
31+
memory. Separation logic addresses the problem of *aliasing*, which is that in
32+
programs involving pointers or references, different expressions can denote the
33+
same variable. By enabling assertions to express exclusive *ownership* of
34+
memory regions, separation logic enables concise specifications, proper
35+
information hiding, and efficient verification for pointer-manipulating
36+
programs.
37+
38+
## Verifying `unsafe` functions
39+
40+
Consider, for example, the function `Node::reverse` below that reverses the
41+
given linked list in-place and returns a pointer to the first node (which
42+
was the originally the last node).
43+
44+
```rust
45+
struct Node {
46+
next: *mut Node,
47+
}
48+
49+
/*@
50+
51+
pred Nodes(n: *mut Node; nodes: list<*mut Node>) =
52+
if n == 0 {
53+
nodes == nil
54+
} else {
55+
(*n).next |-> ?next &*& Nodes(next, ?nodes0) &*& nodes == cons(n, nodes0)
56+
};
57+
58+
@*/
59+
60+
impl Node {
61+
62+
unsafe fn reverse(mut n: *mut Node) -> *mut Node
63+
//@ req Nodes(n, ?nodes);
64+
//@ ens Nodes(result, reverse(nodes));
65+
//@ on_unwind_ens false;
66+
{
67+
let mut m = std::ptr::null_mut();
68+
loop {
69+
//@ inv Nodes(n, ?n_nodes) &*& Nodes(m, ?m_nodes) &*& reverse(nodes) == append(reverse(n_nodes), m_nodes);
70+
//@ open Nodes(n, _);
71+
if n.is_null() {
72+
return m;
73+
}
74+
let k = (*n).next;
75+
//@ append_assoc(reverse(tail(n_nodes)), [n], m_nodes);
76+
(*n).next = m;
77+
m = n;
78+
n = k;
79+
}
80+
}
81+
82+
}
83+
```
84+
85+
VeriFast interprets comments of the form `/*@ ... @*/` or `//@ ...` as VeriFast annotations. This example illustrates four types of annotations:
86+
- Three *specification clause annotations* specify the function's precondition, postcondition, and unwind postcondition, respectively. The function never unwinds, so its
87+
unwind postcondition is `false`.
88+
- The precondition and postcondition are specified in terms of the separation logic predicate `Nodes`, defined in a *ghost declaration annotation*. This predicate
89+
recursively defines the memory footprint of the linked list starting at a given node `n` and associates it with a mathematical list `nodes` of node locations.
90+
The separating conjunction `&*&` implies that the first node of the linked list is *separate* from the remainder of the linked list. It follows that mutating the first node does not affect
91+
the remainder of the linked list. The *variable pattern* `?next` binds logical variable `next` to the value of field `(*n).next`; its scope extends to the end of the assertion.
92+
If a logical variable is introduced in a precondition, its scope includes the postcondition.
93+
- At the start of the loop body, a *block annotation* specifies the loop invariant, expressing that `n` and `m` point to disjoint linked lists and expressing the relationship between their contents and that of the original linked list.
94+
- *Ghost command annotations* provide hints needed for the symbolic execution algorithm to succeed. `open Nodes(n, _)` unfolds the `Nodes` predicate application whose first argument equals `n`. `append_assoc` invokes a library *lemma* expressing the associativity of the `append` operation on mathematical lists.
95+
96+
The generic mathematical datatype `list` is defined in file [`list.rsspec`](https://github.com/verifast/verifast/blob/master/bin/rust/list.rsspec), part of VeriFast's *prelude*, as follows:
97+
```
98+
inductive list<t> = nil | cons(t, list<t>);
99+
```
100+
A list of `t` values is either empty, denoted by *constructor* `nil`, or nonempty, with first element (or *head*) `v` and remainder (or *tail*) `vs`, denoted by `cons(v, vs)`.
101+
102+
Mathematical functions `append` and `reverse` are defined in the same file as follows:
103+
```
104+
fix append<t>(xs: list<t>, ys: list<t>) -> list<t> {
105+
match xs {
106+
nil => ys,
107+
cons(x, xs0) => cons(x, append(xs0, ys))
108+
}
109+
}
110+
111+
fix reverse<t>(xs: list<t>) -> list<t> {
112+
match xs {
113+
nil => nil,
114+
cons(x, xs0) => append(reverse(xs0), cons(x, nil))
115+
}
116+
}
117+
```
118+
Lemma `append_assoc` is declared (but not proven) in the same file. Here is a proof:
119+
```
120+
lem append_assoc<t>(xs: list<t>, ys: list<t>, zs: list<t>)
121+
req true;
122+
ens append(append(xs, ys), zs) == append(xs, append(ys, zs));
123+
{
124+
match xs {
125+
nil => {}
126+
cons(x, xs0) => {
127+
append_assoc(xs0, ys, zs);
128+
}
129+
}
130+
}
131+
```
132+
A lemma is like a regular Rust function, except that it is declared inside an annotation. VeriFast checks that it has no side effects and that it terminates.
133+
134+
## Verifying safe abstractions
135+
136+
Consider the following broken implementation of [`std::mem::replace`](https://doc.rust-lang.org/std/mem/fn.replace.html):
137+
```rust
138+
fn replace<T>(dest: &mut T, src: T) -> T {
139+
unsafe {
140+
let result = (dest as *mut T).read();
141+
(dest as *mut T).write(src);
142+
(dest as *mut T).read() // should be `result`
143+
}
144+
}
145+
```
146+
The Rust compiler accepts it just fine, but VeriFast complains that it cannot prove that when this function returns, the ownership of the value pointed to by `dest` is *separate* from the ownership of the return value. If we replace the final line by `result`, VeriFast accepts the code.
147+
148+
For a function not marked as `unsafe`, VeriFast generates a specification expressing that the function is *semantically well-typed* per [RustBelt](https://research.ralfj.de/thesis.html)'s definition of what Rust's types mean in separation logic. If no specification clause annotations are provided for the function, VeriFast verifies the function against the generated specification; otherwise, VeriFast first verifies that the provided specification implies the generated one, and then verifies the function against the provided specification.
149+
150+
The generated specification for `replace` is as follows:
151+
```rust
152+
fn replace<T>(dest: &mut T, src: T) -> T
153+
//@ req thread_token(?_t) &*& *dest |-> ?dest0 &*& <T>.own(_t, dest0) &*& <T>.own(_t, src);
154+
//@ ens thread_token(_t) &*& *dest |-> ?dest1 &*& <T>.own(_t, dest1) &*& <T>.own(_t, result);
155+
```
156+
The thread token serves as a proof that the function is running in thread `_t`, which is the thread that owns the incoming T values. (This matters in case T is not [Send](https://doc.rust-lang.org/nomicon/send-and-sync.html).) `<T>.own(t, v)` expresses ownership of the T value `v` by thread `t`.
157+
158+
For more information on how to verify safe abstractions in VeriFast, see the relevant [chapter](https://verifast.github.io/verifast/rust-reference/non-unsafe-funcs.html) in the VeriFast for Rust Reference and the [examples](https://github.com/verifast/verifast/tree/master/tests/rust/safe_abstraction) (in `tests/rust/safe_abstraction` in the VeriFast binary distributions). (See [`testsuite.mysh`](https://github.com/verifast/verifast/blob/master/tests/rust/testsuite.mysh) to learn the command line to use to verify a particular example.)
159+
160+
## Running VeriFast
161+
162+
To run VeriFast, download a binary distribution for your platform, either the
163+
[nightly build](https://github.com/verifast/verifast/releases/tag/nightly) or
164+
the [latest named
165+
release](https://github.com/verifast/verifast/releases/latest). Extract the
166+
archive to any folder on your computer. (On Macs, first [remove the quarantine
167+
bit](https://github.com/verifast/verifast?tab=readme-ov-file#binaries).) Then,
168+
either use the VeriFast IDE at `bin/vfide`, the command-line tool at
169+
`bin/verifast`, or the [VSCode
170+
extension](https://marketplace.visualstudio.com/items?itemName=VeriFast.verifast).
171+
In the IDE, open a file and press F5 to verify it. VeriFast will then either
172+
report "0 errors found" or show a debugger-like GUI that allows you to step
173+
through the failed symbolic execution path and inspect the symbolic state at
174+
each step. If verification succeeds, choose Show execution tree to see the tree
175+
of symbolic execution paths traversed for each function that was verified.
176+
177+
In the IDE, the Verify menu allows you to postpone dealing with certain
178+
complexities of the verification task. Specifically, you can tell VeriFast to
179+
ignore unwind paths, ignore arithmetic overflow, and treat shared reference
180+
creation like raw pointer creation (which ignores the complexities of Rust's
181+
[pointer aliasing
182+
rules](https://marketplace.visualstudio.com/items?itemName=VeriFast.verifast)).
183+
(Many of the other options are only relevant when verifying C programs and have
184+
no effect when verifying Rust programs.) All of these options can also be
185+
specified on the command line.

0 commit comments

Comments
 (0)