Skip to content

Commit a2101d3

Browse files
zhassan-awszhassan-aws
committed
[Boogie Backend] Add instructions on how to use the Boogie backend to the README (#2958)
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 2e57044 commit a2101d3

File tree

1 file changed

+220
-32
lines changed

1 file changed

+220
-32
lines changed

‎README.md‎

Lines changed: 220 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -1,54 +1,242 @@
11
![](./kani-logo.png)
2-
[![Kani regression](https://github.com/model-checking/kani/actions/workflows/kani.yml/badge.svg)](https://github.com/model-checking/kani/actions/workflows/kani.yml)
3-
[![Nightly: CBMC Latest](https://github.com/model-checking/kani/actions/workflows/cbmc-latest.yml/badge.svg)](https://github.com/model-checking/kani/actions/workflows/cbmc-latest.yml)
42

5-
The Kani Rust Verifier is a bit-precise model checker for Rust.
3+
**This is a feature branch of Kani that contains an experimental Boogie-based backend. If you are looking for the main version of Kani, visit https://github.com/model-checking/kani instead.**
64

7-
Kani is particularly useful for verifying unsafe code blocks in Rust, where the "[unsafe superpowers](https://doc.rust-lang.org/stable/book/ch19-01-unsafe-rust.html#unsafe-superpowers)" are unchecked by the compiler.
8-
___
9-
Kani verifies:
10-
* Memory safety (e.g., null pointer dereferences)
11-
* User-specified assertions (i.e., `assert!(...)`)
12-
* The absence of panics (e.g., `unwrap()` on `None` values)
13-
* The absence of some types of unexpected behavior (e.g., arithmetic overflows)
5+
The main version of Kani translates [MIR](https://blog.rust-lang.org/2016/04/19/MIR.html) to Goto and uses CBMC as the verification engine.
146

15-
## Installation
7+
This branch implements a translation of MIR to [Boogie](https://github.com/boogie-org/boogie) that can be verified using the Boogie Verifier.
8+
It currently supports a very small subset of Rust.
169

17-
To install the latest version of Kani ([Rust 1.58+; Linux or Mac](https://model-checking.github.io/kani/install-guide.html)), run:
10+
The Boogie backend is not included in Kani's [releases](https://github.com/model-checking/kani/releases), so in order to use it, you need to clone this branch and build from source.
11+
Refer to the [Installing from source code](https://model-checking.github.io/kani/build-from-source.html) section of the documentation for instructions on how to build Kani from source.
1812

13+
## Prerequisites
14+
15+
You need to have the Boogie Verifier installed.
16+
Refer to https://github.com/boogie-org/boogie#installation for the installation instructions.
17+
18+
## Instructions for Using the Boogie Backend
19+
20+
To invoke the Boogie backend, pass the unstable `-Zboogie` option to the Kani command, e.g.
21+
```
22+
kani test.rs -Zboogie
23+
```
24+
or
25+
```
26+
cargo kani -Zboogie
27+
```
28+
Kani will print the name of the generated Boogie file, e.g.
29+
```
30+
Writing Boogie file to /home/ubuntu/test1_main.symtab.bpl
31+
```
32+
You need to manually invoke the Boogie verifier on the generated Boogie file to verify it:
1933
```bash
20-
cargo install --locked kani-verifier
21-
cargo kani setup
34+
$ boogie test1_main.symtab.bpl
35+
36+
Boogie program verifier finished with 1 verified, 0 errors
2237
```
2338

24-
See [the installation guide](https://model-checking.github.io/kani/install-guide.html) for more details.
39+
### Example
2540

26-
## How to use Kani
41+
Consider the following function (whose source file can be found [here](https://github.com/model-checking/kani/blob/features/boogie/tests/script-based-boogie/unbounded_array_copy/test.rs)) which creates an array of integers, `src`, and copies it into another array of integers, `dst`:
42+
```rust
43+
#[kani::proof]
44+
fn copy() {
45+
let src = kani::array::any_array::<i32>();
46+
let mut dst = kani::array::any_array::<i32>();
47+
let src_len: usize = src.len();
48+
let dst_len: usize = dst.len();
2749

28-
Similar to testing, you write a harness, but with Kani you can check all possible values using `kani::any()`:
50+
// copy as many elements as possible of `src` to `dst`
51+
let mut i: usize = 0;
52+
// Loop invariant: forall j: usize :: j < i => dst[j] == src[j])
53+
while i < src_len && i < dst_len {
54+
dst[i] = src[i];
55+
i = i + 1;
56+
}
2957

30-
```rust
31-
use my_crate::{function_under_test, meets_specification, precondition};
58+
// check that the data was copied
59+
i = 0;
60+
while i < src_len && i < dst_len {
61+
kani::assert(dst[i] == src[i], "element doesn't have the correct value");
62+
i = i + 1;
63+
}
64+
}
65+
```
66+
The arrays are created using `kani::array::any_array`, which creates an array with non-deterministic content and length.
3267

33-
#[kani::proof]
34-
fn check_my_property() {
35-
// Create a nondeterministic input
36-
let input = kani::any();
68+
Running Kani with `-Zboogie` produces the following Boogie file:
69+
<details>
70+
<summary>Click to expand Boogie file contents</summary>
3771

38-
// Constrain it according to the function's precondition
39-
kani::assume(precondition(input));
72+
```boogie
73+
// Datatypes:
74+
datatype $Array<T> { $Array(data: [bv64]T, len: bv64) }
4075
41-
// Call the function under verification
42-
let output = function_under_test(input);
76+
// Functions:
77+
function {:bvbuiltin "bvult"} $BvUnsignedLessThan<T>(lhs: T, rhs: T) returns (bool);
4378
44-
// Check that it meets the specification
45-
assert!(meets_specification(input, output));
79+
function {:bvbuiltin "bvslt"} $BvSignedLessThan<T>(lhs: T, rhs: T) returns (bool);
80+
81+
function {:bvbuiltin "bvugt"} $BvUnsignedGreaterThan<T>(lhs: T, rhs: T) returns (bool);
82+
83+
function {:bvbuiltin "bvsgt"} $BvSignedGreaterThan<T>(lhs: T, rhs: T) returns (bool);
84+
85+
function {:bvbuiltin "bvadd"} $BvAdd<T>(lhs: T, rhs: T) returns (T);
86+
87+
function {:bvbuiltin "bvor"} $BvOr<T>(lhs: T, rhs: T) returns (T);
88+
89+
function {:bvbuiltin "bvand"} $BvAnd<T>(lhs: T, rhs: T) returns (T);
90+
91+
function {:bvbuiltin "bvshl"} $BvShl<T>(lhs: T, rhs: T) returns (T);
92+
93+
function {:bvbuiltin "bvlshr"} $BvShr<T>(lhs: T, rhs: T) returns (T);
94+
95+
// Procedures:
96+
procedure _RNvCs7Oe89NXlEjS_4test4copy()
97+
{
98+
var src: $Array bv32;
99+
var dst: $Array bv32;
100+
var src_len: bv64;
101+
var _4: $Array bv32;
102+
var dst_len: bv64;
103+
var _6: $Array bv32;
104+
var i: bv64;
105+
var _8: bool;
106+
var _9: bv64;
107+
var _10: bool;
108+
var _11: bv64;
109+
var _12: bv32;
110+
var _13: bv32;
111+
var _14: $Array bv32;
112+
var _15: bv64;
113+
var _18: bv64;
114+
var _19: bv64;
115+
var _20: bv64;
116+
var _21: bool;
117+
var _22: bv64;
118+
var _23: bool;
119+
var _24: bv64;
120+
var _26: bool;
121+
var _27: bv32;
122+
var _28: bv32;
123+
var _29: $Array bv32;
124+
var _30: bv64;
125+
var _31: bv32;
126+
var _32: bv32;
127+
var _33: $Array bv32;
128+
var _34: bv64;
129+
var _35: bv64;
130+
var _36: bv64;
131+
bb0:
132+
havoc src;
133+
goto bb1;
134+
bb1:
135+
havoc dst;
136+
goto bb2;
137+
bb2:
138+
src_len := src->len;
139+
bb3:
140+
dst_len := dst->len;
141+
bb4:
142+
i := 0bv64;
143+
goto bb5;
144+
bb5:
145+
_9 := i;
146+
_8 := $BvUnsignedLessThan(_9, src_len);
147+
if ((_8 == false)) {
148+
goto bb11;
149+
} else {
150+
goto bb6;
151+
}
152+
bb6:
153+
_11 := i;
154+
_10 := $BvUnsignedLessThan(_11, dst_len);
155+
if ((_10 == false)) {
156+
goto bb11;
157+
} else {
158+
goto bb7;
159+
}
160+
bb11:
161+
i := 0bv64;
162+
goto bb12;
163+
bb12:
164+
_22 := i;
165+
_21 := $BvUnsignedLessThan(_22, src_len);
166+
if ((_21 == false)) {
167+
goto bb19;
168+
} else {
169+
goto bb13;
170+
}
171+
bb13:
172+
_24 := i;
173+
_23 := $BvUnsignedLessThan(_24, dst_len);
174+
if ((_23 == false)) {
175+
goto bb19;
176+
} else {
177+
goto bb14;
178+
}
179+
bb19:
180+
return;
181+
bb14:
182+
_30 := i;
183+
_28 := dst->data[(_30)];
184+
bb15:
185+
_27 := _28;
186+
_34 := i;
187+
_32 := src->data[(_34)];
188+
bb16:
189+
_31 := _32;
190+
_26 := (_27 == _31);
191+
assert _26;
192+
bb17:
193+
_35 := i;
194+
_36 := $BvAdd(_35, 1bv64);
195+
bb18:
196+
i := _36;
197+
goto bb12;
198+
bb7:
199+
_15 := i;
200+
_13 := src->data[(_15)];
201+
bb8:
202+
_12 := _13;
203+
_18 := i;
204+
bb9:
205+
dst->data[(_18)] := _12;
206+
_19 := i;
207+
_20 := $BvAdd(_19, 1bv64);
208+
bb10:
209+
i := _20;
210+
goto bb5;
46211
}
47212
```
213+
</details>
48214

49-
Kani will then try to prove that all valid inputs produce acceptable outputs, without panicking or executing unexpected behavior.
50-
Otherwise Kani will generate a trace that points to the failure.
51-
We recommend following [the tutorial](https://model-checking.github.io/kani/kani-tutorial.html) to learn more about how to use Kani.
215+
If we invoke the Boogie Verifier on the generated file, it fails to prove the assertion:
216+
```bash
217+
$ boogie test__RNvCs7Oe89NXlEjS_4test4copy.symtab.bpl
218+
test__RNvCs7Oe89NXlEjS_4test4copy.symtab.bpl(119,3): Error: this assertion could not be proved
219+
Execution trace:
220+
test__RNvCs7Oe89NXlEjS_4test4copy.symtab.bpl(59,3): bb0
221+
test__RNvCs7Oe89NXlEjS_4test4copy.symtab.bpl(72,3): bb5
222+
test__RNvCs7Oe89NXlEjS_4test4copy.symtab.bpl(76,5): anon8_Then
223+
test__RNvCs7Oe89NXlEjS_4test4copy.symtab.bpl(91,3): bb12
224+
test__RNvCs7Oe89NXlEjS_4test4copy.symtab.bpl(97,5): anon10_Else
225+
test__RNvCs7Oe89NXlEjS_4test4copy.symtab.bpl(105,5): anon11_Else
226+
227+
Boogie program verifier finished with 0 verified, 1 error
228+
```
229+
This is due to the presence of a loop, which requires specifying a loop invariant.
230+
If we add the following assertion after the `bb5:` line (which is the loop head):
231+
```
232+
assert (forall j: bv64 :: $BvUnsignedLessThan(j, i) ==> dst->data[j] == src->data[j]);
233+
```
234+
verification succeeds:
235+
```bash
236+
$ boogie test__RNvCs7Oe89NXlEjS_4test4copy.symtab.bpl
237+
238+
Boogie program verifier finished with 1 verified, 0 errors
239+
```
52240

53241
## GitHub Action
54242

0 commit comments

Comments
 (0)