From b431d77f74df41beadb51f305331ae476b44be79 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 6 Apr 2023 15:26:05 +0000 Subject: [PATCH 1/4] Docs: Add an "Attributes" section --- docs/src/SUMMARY.md | 1 + docs/src/reference/attributes.md | 232 +++++++++++++++++++++++++++++++ 2 files changed, 233 insertions(+) create mode 100644 docs/src/reference/attributes.md diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 545c7ea4a270..940bf643b6e6 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -15,6 +15,7 @@ - [Debugging verification failures](./debugging-verification-failures.md) - [Reference](./reference.md) + - [Attributes](./reference/attributes.md) - [Stubbing](./reference/stubbing.md) - [Application](./application.md) diff --git a/docs/src/reference/attributes.md b/docs/src/reference/attributes.md new file mode 100644 index 000000000000..d6f31694db9a --- /dev/null +++ b/docs/src/reference/attributes.md @@ -0,0 +1,232 @@ +# Attributes + +In Kani, attributes are used to mark functions as harnesses and control their execution. +This section explains the attributes available in Kani and how they affect the verification process. + +At present, the available Kani attributes are the following: + - [`#[kani::proof]`](#kaniproof) + - [`#[kani::should_panic]`](#kanishould_panic) + - [`#[kani::unwind()]`](#kaniunwindnumber) + - [`#[kani::solver()]`](#kanisolversolver) + - [`#[kani::stub(, )]`](#kanistuboriginal-replacement) + +## `#[kani::proof]` + +**The `#[kani::proof]` attribute specifies that a [function](https://doc.rust-lang.org/reference/items/functions.html) is a proof harness.** + +Proof harnesses are similar to test harnesses, especially property-based test harnesses, +and they may use functions from the Kani API (e.g., `kani::any()`). +A proof harness is the smallest verification unit in Kani. + +When Kani is run, either through `kani` or `cargo kani`, it'll first collect all proof harnesses +(i.e., functions with the attribute `#[kani::proof]`) and then attempt to verify them. + +### Example + +If we run Kani on this example: + +```rust +#[kani::proof] +fn my_harness() { + assert!(1 + 1 == 2); +} +``` + +We should see the sentence `Checking harness my_harness...` (assuming `my_harness` is the only harness in our code). +This will be followed by multiple messages that come from CBMC (the verification engine used by Kani) and the [verification results](../verification-results.md). + +Using any other Kani attributes without `#[kani::proof]` will result in compilation errors. + +### Limitations + +The `#[kani::proof]` attribute can only be added to functions without parameters which are not `const`, `async` nor generic functions. + +## `#[kani::should_panic]` + +**The `#[kani::should_panic]` attribute specifies that a proof harness is expected to panic.** + +This attribute allows users to exercise *negative verification*. +It's analogous to how [`#[should_panic]`](https://doc.rust-lang.org/rust-by-example/testing/unit_testing.html#testing-panics) allows users to exercise [negative testing](https://en.wikipedia.org/wiki/Negative_testing) for Rust unit tests. + +This attribute **only affects the overall verification result**. +In particular, using the `#[kani::should_panic]` attribute will return one of the following results: + - `VERIFICATION:- FAILED (encountered no panics, but at least one was expected)` if there were no failed checks. + - `VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)` if there were failed checks but not all them were related to panics. + - `VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)` otherwise. + +At the moment, to determine if a check is related to a panic, we check if its class is `assertion`. +The class is the second member in the property name, the triple that's printed after `Check X: `: `..`. +For example, the class in `Check 1: my_harness.assertion.1` is `assertion`, so this check is considered to be related to a panic. + +> **NOTE**: The `#[kani::should_panic]` is only recommended for writing +> harnesses which complement existing harnesses that don't use the same +> attribute. In order words, it's only recommended to write *negative harnesses* +> after having written *positive* harnesses that successfully verify interesting +> properties about the function under verification. + +### Limitations + +The `#[kani::should_panic]` attribute verifies that are one or more failed checks related to panics. +At the moment, it's not possible to pin it down to specific panics. +Therefore, **it's possible that the panics detected with `#[kani::should_panic]` aren't the ones that were originally expected** after a change in the code under verification. + +### Example + +Let's assume we're using the `Device` from this example: + +```rust +struct Device { + is_init: bool, +} + +impl Device { + fn new() -> Self { + Device { is_init: false } + } + + fn init(&mut self) { + assert!(!self.is_init); + self.is_init = true; + } +} +``` + +We may want to verify that calling `device.init()` more than once should result in a panic. +We can do so with the following harness: + +```rust +#[kani::proof] +fn cannot_init_device_twice() { + let mut device = Device::new(); + device.init(); + device.init(); +} +``` + +Running Kani on it will produce the result `VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)` + +## `#[kani::unwind()]` + +**The `#[kani::unwind()]` attribute specifies that all loops must be unwound up to `` times.** + +By default, Kani attempts to unwind all loops automatically. +However, this unwinding process doesn't always terminate. +The `#[kani::unwind()]` attribute will: + 1. Disable automatic unwinding. + 2. Unwind all loops up to `` times. + +After the unwinding stage, Kani will attempt to verify the harness. +If the `#[kani::unwind()]` attribute was specified, there's a chance that one or more loops weren't unwound enough times. +In that case, there will be at least one failed unwinding assertion (there's one unwinding assertion for each loop), causing verification to fail. + +Check the [*Loops, unwinding and bounds* section](../tutorial-loop-unwinding.md) for more information about stubbing. + +### Example + +Let's assume we've written this code which contains a loop: + +```rust +fn my_sum(vec: &Vec) -> u32 { + let mut counter = 0; + for elem in vec { + counter += elem; + } + counter +} + +#[kani::proof] +fn my_harness() { + let vec = vec![1, 2, 3]; + let sum = my_sum(&vec); + assert!(sum == 6); +} +``` + +Running this example on Kani will produce a successful verification result. +In this case, Kani automatically finds the required unwinding value (i.e., the number of times it needs to unwind all loops). +This means that the `#[kani::unwind()]` attribute isn't needed, as we'll see soon. +In general, the required unwinding value is equal to the maximum number of iterations for all loops, plus one. +The required unwinding value in this example is 4: the 3 iterations in the `for elem in vec` loop, plus 1. + +Let's see what happens if we force a lower unwinding value with `#[kani::unwind(3)]`: + +```rust +#[kani::proof] +#[kani::unwind(3)] +fn my_harness() { + let vec = vec![1, 2, 3]; + let sum = my_sum(&vec); + assert!(sum == 6); +} +``` + +As we mentioned, trying to verify this harness causes an unwinding failure: + +``` +SUMMARY: + ** 1 of 187 failed (186 undetermined) +Failed Checks: unwinding assertion loop 0 + File: "/home/ubuntu/devices/src/main.rs", line 32, in my_sum + +VERIFICATION:- FAILED +[Kani] info: Verification output shows one or more unwinding failures. +[Kani] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`. +``` + +Kani cannot verify the harness because there is at least an unwinding failure. +But, if we use `#[kani::unwind(4)]`, which is the right unwinding value we computed earlier: + +```rust +#[kani::proof] +#[kani::unwind(4)] +fn my_harness() { + let vec = vec![1, 2, 3]; + let sum = my_sum(&vec); + assert!(sum == 6); +} +``` + +We'll get a successful result again: + +``` +SUMMARY: + ** 0 of 186 failed + +VERIFICATION:- SUCCESSFUL +``` + +## `#[kani::solver()]` + +**Changes the solver to be used by Kani.** + +This may change the verification time required to verify a harness. + +At present, `` can be one of: + - `minisat` (default): [MiniSat](http://minisat.se/), a minimalistic open-source SAT solver. + - `cadical`: [CaDiCaL](https://github.com/arminbiere/cadical), an extensible open-source SAT solver. + - `kissat`: [kissat](https://github.com/arminbiere/kissat), an optimized variant of CaDiCaL. + - `bin=""`: A custom solver, whose binary is to be found in the path `""`. + +### Example + +Kani will use the CaDiCaL solver in the following example: + +```rust +#[kani::proof] +#[kani::solver(cadical)] +fn check() { + let mut a = [2, 3, 1]; + a.sort(); + assert_eq!(a[0], 1); + assert_eq!(a[1], 2); + assert_eq!(a[2], 3); +} +``` + +Changing the solver may result in different verification times depending on the harness. + +## `#[kani::stub(, )]` + +**Replaces the function/method with name with the function/method with name during compilation** + +Check the [*Stubbing* section](../reference/stubbing.md) for more information about stubbing. From cff93fd7cd65f26b1cb6edbd22c1ddd06a56053c Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Mon, 10 Apr 2023 10:52:33 -0400 Subject: [PATCH 2/4] Apply suggestions from Zyad Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- docs/src/reference/attributes.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/docs/src/reference/attributes.md b/docs/src/reference/attributes.md index d6f31694db9a..b758804adf68 100644 --- a/docs/src/reference/attributes.md +++ b/docs/src/reference/attributes.md @@ -32,10 +32,10 @@ fn my_harness() { } ``` -We should see the sentence `Checking harness my_harness...` (assuming `my_harness` is the only harness in our code). +We should see a line in the output that says `Checking harness my_harness...` (assuming `my_harness` is the only harness in our code). This will be followed by multiple messages that come from CBMC (the verification engine used by Kani) and the [verification results](../verification-results.md). -Using any other Kani attributes without `#[kani::proof]` will result in compilation errors. +Using any other Kani attribute without `#[kani::proof]` will result in compilation errors. ### Limitations @@ -66,7 +66,7 @@ For example, the class in `Check 1: my_harness.assertion.1` is `assertion`, so t ### Limitations -The `#[kani::should_panic]` attribute verifies that are one or more failed checks related to panics. +The `#[kani::should_panic]` attribute verifies that there are one or more failed checks related to panics. At the moment, it's not possible to pin it down to specific panics. Therefore, **it's possible that the panics detected with `#[kani::should_panic]` aren't the ones that were originally expected** after a change in the code under verification. @@ -119,7 +119,7 @@ After the unwinding stage, Kani will attempt to verify the harness. If the `#[kani::unwind()]` attribute was specified, there's a chance that one or more loops weren't unwound enough times. In that case, there will be at least one failed unwinding assertion (there's one unwinding assertion for each loop), causing verification to fail. -Check the [*Loops, unwinding and bounds* section](../tutorial-loop-unwinding.md) for more information about stubbing. +Check the [*Loops, unwinding and bounds* section](../tutorial-loop-unwinding.md) for more information about unwinding. ### Example @@ -173,7 +173,7 @@ VERIFICATION:- FAILED [Kani] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`. ``` -Kani cannot verify the harness because there is at least an unwinding failure. +Kani cannot verify the harness because there is at least one unwinding assertion failure. But, if we use `#[kani::unwind(4)]`, which is the right unwinding value we computed earlier: ```rust @@ -197,7 +197,7 @@ VERIFICATION:- SUCCESSFUL ## `#[kani::solver()]` -**Changes the solver to be used by Kani.** +**Changes the solver to be used by Kani's verification engine (CBMC).** This may change the verification time required to verify a harness. @@ -205,7 +205,7 @@ At present, `` can be one of: - `minisat` (default): [MiniSat](http://minisat.se/), a minimalistic open-source SAT solver. - `cadical`: [CaDiCaL](https://github.com/arminbiere/cadical), an extensible open-source SAT solver. - `kissat`: [kissat](https://github.com/arminbiere/kissat), an optimized variant of CaDiCaL. - - `bin=""`: A custom solver, whose binary is to be found in the path `""`. + - `bin=""`: A custom solver binary, `""`, that must be in path. ### Example From e56e6dffefae552a4ed9ccd579c9c60ca9d790ee Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 10 Apr 2023 15:04:00 +0000 Subject: [PATCH 3/4] Address other comments from Zyad --- docs/src/reference/attributes.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/docs/src/reference/attributes.md b/docs/src/reference/attributes.md index b758804adf68..bb7823eb8116 100644 --- a/docs/src/reference/attributes.md +++ b/docs/src/reference/attributes.md @@ -39,7 +39,7 @@ Using any other Kani attribute without `#[kani::proof]` will result in compilati ### Limitations -The `#[kani::proof]` attribute can only be added to functions without parameters which are not `const`, `async` nor generic functions. +The `#[kani::proof]` attribute can only be added to functions without parameters. ## `#[kani::should_panic]` @@ -96,6 +96,7 @@ We can do so with the following harness: ```rust #[kani::proof] +#[kani::should_panic] fn cannot_init_device_twice() { let mut device = Device::new(); device.init(); @@ -127,11 +128,11 @@ Let's assume we've written this code which contains a loop: ```rust fn my_sum(vec: &Vec) -> u32 { - let mut counter = 0; + let mut sum = 0; for elem in vec { - counter += elem; + sum += elem; } - counter + sum } #[kani::proof] @@ -202,9 +203,9 @@ VERIFICATION:- SUCCESSFUL This may change the verification time required to verify a harness. At present, `` can be one of: - - `minisat` (default): [MiniSat](http://minisat.se/), a minimalistic open-source SAT solver. - - `cadical`: [CaDiCaL](https://github.com/arminbiere/cadical), an extensible open-source SAT solver. - - `kissat`: [kissat](https://github.com/arminbiere/kissat), an optimized variant of CaDiCaL. + - `minisat` (default): [MiniSat](http://minisat.se/). + - `cadical`: [CaDiCaL](https://github.com/arminbiere/cadical). + - `kissat`: [kissat](https://github.com/arminbiere/kissat). - `bin=""`: A custom solver binary, `""`, that must be in path. ### Example From ab85c397f22d522312cf2e67ebd0750b48c5cab6 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 10 Apr 2023 15:11:35 +0000 Subject: [PATCH 4/4] Link from the tutorial --- docs/src/tutorial-first-steps.md | 2 +- docs/src/tutorial-loop-unwinding.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/src/tutorial-first-steps.md b/docs/src/tutorial-first-steps.md index 42520b33d2a2..c6d5cbf306c1 100644 --- a/docs/src/tutorial-first-steps.md +++ b/docs/src/tutorial-first-steps.md @@ -29,7 +29,7 @@ test tests::doesnt_crash ... ok There's only 1 in 4 billion inputs that fail, so it's vanishingly unlikely the property test will find it, even with a million samples. -Let's write a Kani _proof harness_ for `estimate_size`. +Let's write a Kani [_proof harness_](reference/attributes.md#kaniproof) for `estimate_size`. This is a lot like a test harness, but now we can use `kani::any()` to represent all possible `u32` values: ```rust diff --git a/docs/src/tutorial-loop-unwinding.md b/docs/src/tutorial-loop-unwinding.md index ef4f59773943..81bfbdf68cfb 100644 --- a/docs/src/tutorial-loop-unwinding.md +++ b/docs/src/tutorial-loop-unwinding.md @@ -13,7 +13,7 @@ We can try to find this bug with a proof harness like this: {{#include tutorial/loops-unwinding/src/lib.rs:kani}} ``` -But we've just used a new feature (`#[kani::unwind(1)]`) that requires some explanation. +But we've just used a [new attribute](reference/attributes.md#kaniunwindnumber) (`#[kani::unwind(1)]`) that requires some explanation. When we run `cargo kani` on this code as we have written it, we see an odd verification failure: ```