You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When we run Kani on this, we run into an unfortunate result: non-termination.
17
-
This non-termination is caused by CBMC trying to unwind the loop an unlimited number of times.
16
+
But we've just used a new feature (`#[kani::unwind(1)]`) that requires some explanation.
17
+
When we run `cargo kani` on this code as we have written it, we see an odd verification failure:
18
+
19
+
```
20
+
SUMMARY:
21
+
** 1 of 67 failed (66 undetermined)
22
+
Failed Checks: unwinding assertion loop 0
23
+
24
+
VERIFICATION:- FAILED
25
+
```
26
+
27
+
If we try removing this "unwind" annotation and re-running Kani, the result is worse: non-termination.
28
+
Kani simply doesn't produce a result.
18
29
19
30
> **NOTE**: Presently, [due to a bug](https://github.com/model-checking/kani/issues/493), this is especially bad: we don't see any output at all.
20
31
> Kani is supposed to emit some log lines that might give some clue that an infinite loop is occurring.
21
-
> If Kani doesn't terminate, it's almost always the problem that this section covers.
32
+
> If Kani doesn't terminate, it's most frequently the problem that this section covers.
33
+
> The workaround is to use the technique we're demoing here: use `#[kani::unwind(1)]` to force termination of the loops, and work upwards from there.
34
+
35
+
The problem we're struggling with is the technique Kani uses to verify code.
36
+
We're not able to handle code with "unbounded" loops, and what "bounded" means can be quite subtle.
37
+
It has to have a constant number of iterations that's _"obviously constant"_ enough for the verifier to actually figure this out.
38
+
In practice, very few loops are like this.
22
39
23
-
To verify programs like this, we need to do two things:
40
+
To verify programs like this with Kani as it exists today, we need to do two things:
24
41
25
42
1. Set an upper bound on the size of the problem.
26
-
We've actually already done part of this: our proof harness seems to be trying to set an upper limit of 10.
27
-
2. Tell Kani about this limit if it's not able to figure it out on its own.
43
+
We've actually already done part of this: our proof harness above seems to be trying to set an upper `LIMIT` of 10.
44
+
2. Tell Kani about this limit if (or when) it's not able to figure it out on its own.
45
+
This is the purpose of the `kani::unwind` annotation.
28
46
29
47
Bounding proofs like this means we may no longer be proving as much as we originally hoped.
30
-
Who's to say, if we prove everything works up to size 10, that there isn't a novel bug lurking, expressible only with problems of size 11+?
48
+
Who's to say, if we prove everything works up to size 10, that there isn't a novel bug lurking, reachable only with problems of size 11+?
49
+
Perhaps!
31
50
But, let's get back to the issue at hand.
32
51
33
-
We can "make progress" in our work by giving Kani a global bound on the problem size using the `--default-unwind <bound>` flag.
34
-
This flag puts a fixed upper bound on loop unwinding.
35
-
Kani will automatically generate verification conditions that help us understand if that bound isn't enough.
36
-
Let's start with a small unwinding value:
37
-
38
-
```
39
-
# kani src/lib.rs --default-unwind 1
40
-
Check 69: .unwind.0
41
-
- Status: FAILURE
42
-
- Description: "unwinding assertion loop 0"
43
-
[...]
44
-
VERIFICATION:- FAILED
45
-
```
52
+
By putting `#[kani::unwind(1)]` on the proof harness, we've placed an upper bound of 1 loop iteration.
53
+
The "unwinding assertion" failure that Kani reports is because this bound is not high enough.
54
+
The code tries to execute more than 1 loop iteration.
55
+
(And, because the unwinding isn't high enough, many of the other properties Kani is verifying become "undetermined": we don't really know if they're true or false, because we can't get far enough.)
46
56
47
-
This output is showing us two things:
57
+
**Exercise**: Try increasing the bound. Where might you start? How high do you need to go to get rid of the "unwinding assertion" failure?
48
58
49
-
1. Kani tells us we haven't unwound enough. This is the failure of the "unwinding assertion."
50
-
2. We aren't seeing other failures if we only unwind the loop once.
51
-
The execution can't progress far enough to reveal the bug we're interested in (which actually only happens in the last iteration of the loop).
59
+
<details>
60
+
<summary>Click to see explanation for the exercise</summary>
52
61
53
-
Doing an initial `--default-unwind 1` is generally enough to force termination, but often too little for verification.
62
+
Since the proof harness is trying to limit the array to size 10, an initial unwind value of 10 seems like the obvious place to start.
63
+
But that's not large enough for Kani.
54
64
55
-
We were clearly aiming at a size limit of 10 in our proof harness, so let's try a few things:
65
+
At size 11, we still see the "unwinding assertion" failure, but now we can see the actual failures we're trying to find, too.
66
+
Finally at size 12, the "unwinding assertion" goes away, just leaving the other failures.
67
+
We'll explain why we see this behavior in a moment.
We now return to the question: why is 12 the unwinding bound?
87
+
Well, the first answer is: it isn't!
88
+
Reduce it to 11 and observe that the proof now still works!
89
+
90
+
Kani needs the unwinding bound to be "one more than" the number of loop iterations.
91
+
We previously had an off-by-one error that tried to do 11 iterations on an array of size 10.
92
+
So... the unwinding bound needed to be 12, then.
93
+
Fixing that error to do the correct 10 iterations means we can now successfully reduce that unwind bound to 11 again.
94
+
95
+
> **NOTE**: Presently, there are some situations where "number of iterations of a loop" can be less obvious than it seems.
96
+
> This can be easily triggered with use of `break` or `continue` within loops.
97
+
> Often this manifests itself as needing "two more" or "three more" iterations in the unwind bound than seems like it would actually run.
98
+
> In those situations, we might still need a bound like `kani::unwind(13)`, despite looking like a loop bounded to 10 iterations.
99
+
100
+
The approach we've taken here is a general method for getting a bounded proof to go through:
79
101
80
-
Kani is now sure we've unwound the loop enough to verify our proof harness, and now we're seeing just the bound checking failures from the off-by-one error.
102
+
1. Put an actual upper bound on the problem itself.
103
+
Here that's accomplished via `LIMIT` in our proof harness.
104
+
We don't create a slice any bigger than that, and that's what we loop over.
105
+
2. Start at a reasonable guess for a `kani::unwind` bound, and increase until the unwinding assertion failure goes away.
106
+
3. Or, if that starts to take too long to verify, decrease your problem's bound, to accommodate the verifier's performance.
81
107
82
108
## Unwinding value specification
83
109
84
-
Kani allows three options to specify the unwind value for a particular harness:
110
+
The best approach to supplying Kani with unwind bounds is using the annotation `kani::unwind`, as we show above.
111
+
112
+
You might want to supply one via command line when experimenting, however.
113
+
In that case you can either use `--default-unwind x` to set an unwind bound for every proof harness that **does not** have an explicit bound.
114
+
115
+
Or you can _override_ a harness's bound, but only when running a specific harness:
85
116
86
-
1. The unwind annotation `#[kani::unwind(<num>)]`. This sets the unwind value for the harness with the annotation. Example -
87
-
```rust
88
-
#[kani::proof]
89
-
#[kani::unwind(3)]
90
-
fnproof_harness() {
91
-
[...]
92
-
}
93
-
```
94
-
2.`--default-unwind` flag. This sets the global or default unwind value for the entire file/crate on which kani or cargo-kani is called. Example -
95
-
```
96
-
kani file.rs --default-unwind 3
97
117
```
98
-
3.`--unwind` flag. This overrides any annotation and forces the harness to use the specified value. This needs to be used alongside `--harness` and sets the unwind value for the harness specified. Example -
Finally, you might be interested in defaulting the unwind bound to 1, to force termination (and force supplying a bound) on all your proof harnesses.
122
+
You can do this by putting this into your `Cargo.toml` file:
123
+
124
+
```toml
125
+
[workspace.metadata.kani.flags]
126
+
default-unwind = 1
101
127
```
102
128
103
-
### Exercises -
129
+
## Bounded proof
130
+
131
+
Before we finish, it's worth revisiting the implications of what we've done here.
132
+
Kani frequently needs to do "bounded proof", which contrasts with unbounded or full verification.
133
+
134
+
We've written a proof harness that shows `initialize_prefix` has no errors on input slices of size 10, but no higher.
135
+
The particular size we choose is usually determined by balancing the level of assurance we want, versus runtime of Kani.
136
+
It's often not worth running proofs for large numbers of iterations, unless either very high assurance is necessary, or there's reason to suspect larger problems will contain novel failure modes.
137
+
138
+
**Exercise**: Try increasing the problem size (both the unwind and the `LIMIT` constant). When does it start to take more than a few seconds?
139
+
140
+
<details>
141
+
<summary>Click to see explanation for the exercise</summary>
142
+
143
+
On your friendly neighborhood author's machine, a `LIMIT` of 100 takes about 3.8 seconds end-to-end.
144
+
This is a relatively simple bit of code, though, and it's not uncommon for some proofs to scale poorly even to 5 iterations.
145
+
146
+
</details>
147
+
148
+
One consequence of this, however, is that Kani often scales poorly to "big string problems" like parsing.
149
+
Often a parser will need to consume inputs larger than 10-20 characters to exhibit strange behaviors.
150
+
151
+
## Summary
152
+
153
+
In this section:
104
154
105
-
1. Exercise: Fix the off-by-one bounds error and get Kani to verify successfully.
106
-
2. Exercise: After fixing the error, `--default-unwind 11` works. Why?
155
+
1. We saw Kani fail to terminate.
156
+
2. We saw how `#[kani::unwind(1)]` can help force Kani to terminate (with a verification failure).
157
+
3. We saw "unwinding assertions" verify that we've set the unwinding limit high enough.
158
+
4. We saw how to put a practical bound on problem size in our proof harness.
159
+
5. We saw how to pick an unwinding size large enough to successfully verify that bounded proof.
0 commit comments