From cf5a088adfc88a10b7daa3bd2821b7a961a225f7 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 3 Mar 2023 22:29:20 +0000 Subject: [PATCH 01/11] Draft for RFC of `should_fail` attribute --- rfc/src/rfcs/0005-should-fail-attr.md | 174 ++++++++++++++++++++++++++ 1 file changed, 174 insertions(+) create mode 100644 rfc/src/rfcs/0005-should-fail-attr.md diff --git a/rfc/src/rfcs/0005-should-fail-attr.md b/rfc/src/rfcs/0005-should-fail-attr.md new file mode 100644 index 000000000000..51448893c0b7 --- /dev/null +++ b/rfc/src/rfcs/0005-should-fail-attr.md @@ -0,0 +1,174 @@ +- **Feature Name:** *Fill me with pretty name and a unique ident. E.g: New Feature (`new_feature`)* +- **Feature Request Issue:** +- **RFC PR:** *Link to original PR* +- **Status:** Under Review +- **Version:** 0 +- **Proof-of-concept:** *Optional field. If you have implemented a proof of concept, add a link here* + +## Summary + +Users may want to express that a verification harness should fail. +This RFC proposes a new harness attribute `#[kani::should_fail]` that informs Kani about this expectation. + +## User Impact + +Users may want to express that a verification harness should fail for multiple reasons. +In general, users writing such harnesses want to demonstrate that their verification results in a failure. +Let's refer to this concept as *negative verification*, inspired by the term [negative testing](https://en.wikipedia.org/wiki/Negative_testing). +We may consider the following reasons for users to write negative verification harnesses: + * To improve the coverage achieved with verification. + * To demonstrate that invalid input ends up produing errors. + +In fact, the closest example of this are some of our tests. +Currently, we use test annotations specific to `compiletest` to indicate that a failure is expected. +The proposed annotation would provide a way in Kani to express that a verification harness should fail, +allowing users to write verification harness that are expected to fail. + + +--- +Why are we doing this? How will this benefit the final user? + + - If this is an API change, how will that impact current users? + - For deprecation or breaking changes, how will the transition look like? + - If this RFC is related to change in the architecture without major user impact, think about the long term +impact for user. I.e.: what future work will this enable. + +## User Experience + +The scope of this functionality is limited to the overall verification result. +The [rationale section](#rationale-and-alternatives) discusses the granularity of failures, and how this attribute could be extended. + +### Single Harness + +Let's take one of the simplest examples from our regression: + +```rust +#[kani::proof] +fn simple_add_overflows() { + let a: u32 = kani::any(); + let b: u32 = kani::any(); + a + b; +} +``` + +Currently, this example produces a `VERIFICATION:- FAILED` result.[^footnote-compiletest] + +```rust +#[kani::proof] +#[kani::should_fail] +fn simple_add_overflows() { + let a: u32 = kani::any(); + let b: u32 = kani::any(); + a + b; +} +``` + +Since we added `#[kani::should_fail]`, running this example would produce a successful verification code. + +Now, we've considered two ways to represent this result in the verification output. +Note that it's important that we provide the user with this feedback: + 1. **(Expectation)** Kani was expecting the harness to fail. + 2. **(Transparency)**: The actual verification result that Kani produced after the analysis. +This will avoid a potential scenario where the user doesn't know for sure if the attribute has had an effect when running the verification harness. + +As mentioned, we've considered two ways to represent this result. + +#### Representation #1 (Recommended): No changes to overall result + +```rust +VERIFICATION:- FAILED (should have FAILED) +``` + +#### Representation #2: Changes to overall result + +```rust +VERIFICATION:- SUCCESSFUL (should have FAILED and it FAILED) +``` + +### Multiple Harnesses + +When there are multiple harness, we'll implement the single-harness changes in addition to these ones. +Currently, a "Summary" section appears after reporting the results for each harness: +``` +Verification failed for - harness3 +Verification failed for - harness2 +Verification failed for - harness1 +Complete - 0 successfully verified harnesses, 3 failures, 3 total. +``` + +Harnesses marked with `#[kani::should_fail]` won't show unless the expected result was different from the actual result. +The summary will consider harness that match the expectation as "successfully verified harnesses". + +Therefore, if we added `#[kani::should_fail]` to all harnesses in the previous example, we'd see this output: +``` +Complete - 3 successfully verified harnesses, 0 failures, 3 total. +``` + +### Availability + +This feature will only be available as an attribute. +That means this feature won't be available as a CLI option (i.e., `--should-fail`). +There are good reasons to avoid the CLI option: + - It'd make the design and implementation unnecessarily complex. + - It'd only be useful when combined with `--harness` to filter negative harnesses. + - We could have trouble extending its functionality (see [Future possibilities](#future-possibilities) for more details). + +### Pedagogy + +The `#[kani::should_fail]` attribute will become on the most basic attributes in Kani. +As such, it'll be mentioned in the tutorial and added to the dedicated section planned in [#2208](https://github.com/model-checking/kani/issues/2208). + +## Detailed Design + +At a high level, we expect modifications in the following components: + - `kani-compiler`: Changes required to (1) process the new attribute, and (2) extend `HarnessMetadata` with a `should_fail: bool` field. + - `kani-driver`: Changes required to (1) edit information about harnesses printed by `kani-driver`, (2) edit verification output when post-processing CBMC verification results, and (3) return the appropriate exit status after post-processing CBMC verification results. + +We don't expect these changes to require new dependencies. +Besides, we don't expect these changes to be updated unless we decide to extend the attribute with further fields (see [Future possibilities](#future-possibilities) for more details). + +## Rationale and alternatives + +This proposal would enable users to exercise negative verification with a relatively +Moreover, we could use it in our own regression and remove special-cased code to handle this case in `compiletest`. +This is a relatively cheap feature to implement if we compare it take into account the expressivenes it provides. + +### Alternative #1: Name + +Our first choice is made in the name of the attribute. +It should be noted that Rust has a similarly named attribute for unit tests: [the `#[should_panic]` attribute](https://doc.rust-lang.org/rust-by-example/testing/unit_testing.html#testing-panics). +At first, one may think that `#[kani::should_fail]` and `#[should_panic]` have the same semantics. +However, if we keep thinking about this, we'll realize that: + 1. A panic in Rust should always result in a failure in Kani, but + 2. A failure in Kani doesn't always result in a panic in Rust. + +Our running example shows an instance of (2): an overflow error doesn't result in a panic in Rust. +So it's better to avoid `panic` in the name. + +We have also considered two alternatives for the expectation: `should` and `expect`. +To be honest, we've avoided `expect` altogether for two reasons: + - We may consider a more granular approach to indicate expectations regarding individual checks and cover statements in the future. The tentative name for the attribute is `#[kani::expect]`. + - We heavily use this word for testing in Kani. + +### Alternative #2: Granularity + + + +- What are the pros and cons of this design? +- What is the impact of not doing this? +- What other designs have you considered? Why didn't you choose them? + +## Open questions + +- Is there any part of the design that you expect to resolve through the RFC process? +- What kind of user feedback do you expect to gather before stabilization? How will this impact your design? + +## Future possibilities + +What are natural extensions and possible improvements that you predict for this feature that is out of the +scope of this RFC? Feel free to brainstorm here. + + * More granular checks. + * Attribute auto-generation from `kani::proof` + +[footnote-compiletest]: `compiletest` knows that the test should fail because it parses the `// kani-verify-fail` comment at the top. From ce7a995c3401dca6a7c376c9d6eb964b24f8efcf Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 6 Mar 2023 22:26:45 +0000 Subject: [PATCH 02/11] Add more content and add to `SUMMARY.md` --- rfc/src/SUMMARY.md | 1 + rfc/src/rfcs/0005-should-fail-attr.md | 107 ++++++++++++++++---------- 2 files changed, 66 insertions(+), 42 deletions(-) diff --git a/rfc/src/SUMMARY.md b/rfc/src/SUMMARY.md index ade6c44df5df..51cef60366ce 100644 --- a/rfc/src/SUMMARY.md +++ b/rfc/src/SUMMARY.md @@ -9,3 +9,4 @@ - [0001-mir-linker](rfcs/0001-mir-linker.md) - [0002-function-stubbing](rfcs/0002-function-stubbing.md) - [0003-cover-statement](rfcs/0003-cover-statement.md) +- [0005-should-fail-attr](rfcs/0005-should-fail-attr.md) diff --git a/rfc/src/rfcs/0005-should-fail-attr.md b/rfc/src/rfcs/0005-should-fail-attr.md index 51448893c0b7..cd07d85a9e31 100644 --- a/rfc/src/rfcs/0005-should-fail-attr.md +++ b/rfc/src/rfcs/0005-should-fail-attr.md @@ -1,4 +1,4 @@ -- **Feature Name:** *Fill me with pretty name and a unique ident. E.g: New Feature (`new_feature`)* +- **Feature Name:** The `kani::should_fail` attribute (`should-fail-attr`)* - **Feature Request Issue:** - **RFC PR:** *Link to original PR* - **Status:** Under Review @@ -12,26 +12,22 @@ This RFC proposes a new harness attribute `#[kani::should_fail]` that informs Ka ## User Impact -Users may want to express that a verification harness should fail for multiple reasons. -In general, users writing such harnesses want to demonstrate that their verification results in a failure. +Users may want to express that a verification harness should fail. +In general, users writing such harnesses want to demonstrate that verification results include at least a failure. Let's refer to this concept as *negative verification*, inspired by the term [negative testing](https://en.wikipedia.org/wiki/Negative_testing). -We may consider the following reasons for users to write negative verification harnesses: - * To improve the coverage achieved with verification. - * To demonstrate that invalid input ends up produing errors. - -In fact, the closest example of this are some of our tests. -Currently, we use test annotations specific to `compiletest` to indicate that a failure is expected. -The proposed annotation would provide a way in Kani to express that a verification harness should fail, -allowing users to write verification harness that are expected to fail. +Negative verification harnesses could be useful to show that invalid inputs result in verification failures, +or increase the overall verification coverage. +In fact, some of the tests in the Kani regression are written as negative harnesses. +Currently, we [use comments](https://model-checking.github.io/kani/regression-testing.html#testing-stages) specific to `compiletest` to indicate that a verification failure is expected. +The proposed attribute would provide a way in Kani to express that a verification harness should fail, +allowing users to write negative verification harnesses. ---- -Why are we doing this? How will this benefit the final user? - - - If this is an API change, how will that impact current users? - - For deprecation or breaking changes, how will the transition look like? - - If this RFC is related to change in the architecture without major user impact, think about the long term -impact for user. I.e.: what future work will this enable. +We also acknowledge that, in other cases, users may want to express more granular expectations for their harnesses. +For example, a user may want to specify that a given check results in a failure. +An ergonomic mechanism for informing Kani about such expectations is likely to require other improvements in Kani (a comprehensive classification for checks reported by Kani, a language to describe expectations for checks and cover statements, and general output improvements). +We consider that the mechanism we just mentioned and the one discussed in this proposal solve different problems, so they don't need to be discussed together. +This is further discussed in the [rationale and alternatives](#rationale-and-alternatives) and [future possibilities](#future-possibilities) sections. ## User Experience @@ -40,7 +36,7 @@ The [rationale section](#rationale-and-alternatives) discusses the granularity o ### Single Harness -Let's take one of the simplest examples from our regression: +Let's take an example from the Kani regression: ```rust #[kani::proof] @@ -52,6 +48,7 @@ fn simple_add_overflows() { ``` Currently, this example produces a `VERIFICATION:- FAILED` result.[^footnote-compiletest] +In addition, it will return a non-successful code. ```rust #[kani::proof] @@ -63,12 +60,12 @@ fn simple_add_overflows() { } ``` -Since we added `#[kani::should_fail]`, running this example would produce a successful verification code. +Since we added `#[kani::should_fail]`, running this example would produce a successful code. Now, we've considered two ways to represent this result in the verification output. Note that it's important that we provide the user with this feedback: 1. **(Expectation)** Kani was expecting the harness to fail. - 2. **(Transparency)**: The actual verification result that Kani produced after the analysis. + 2. **(Outcome)**: The actual verification result that Kani produced after the analysis. This will avoid a potential scenario where the user doesn't know for sure if the attribute has had an effect when running the verification harness. As mentioned, we've considered two ways to represent this result. @@ -76,18 +73,20 @@ As mentioned, we've considered two ways to represent this result. #### Representation #1 (Recommended): No changes to overall result ```rust -VERIFICATION:- FAILED (should have FAILED) +VERIFICATION:- FAILED (expected FAILED) ``` +We recommend this representation so the user receives clear information about both the outcome and the expectation. + #### Representation #2: Changes to overall result ```rust -VERIFICATION:- SUCCESSFUL (should have FAILED and it FAILED) +VERIFICATION:- SUCCESSFUL (expected FAILED and it FAILED) ``` ### Multiple Harnesses -When there are multiple harness, we'll implement the single-harness changes in addition to these ones. +When there are multiple harnesses, we'll implement the single-harness changes in addition to the following ones. Currently, a "Summary" section appears after reporting the results for each harness: ``` Verification failed for - harness3 @@ -97,9 +96,10 @@ Complete - 0 successfully verified harnesses, 3 failures, 3 total. ``` Harnesses marked with `#[kani::should_fail]` won't show unless the expected result was different from the actual result. -The summary will consider harness that match the expectation as "successfully verified harnesses". +The summary will consider harnesses that match their expectation as "successfully verified harnesses". Therefore, if we added `#[kani::should_fail]` to all harnesses in the previous example, we'd see this output: + ``` Complete - 3 successfully verified harnesses, 0 failures, 3 total. ``` @@ -115,7 +115,7 @@ There are good reasons to avoid the CLI option: ### Pedagogy -The `#[kani::should_fail]` attribute will become on the most basic attributes in Kani. +The `#[kani::should_fail]` attribute will become one of the most basic attributes in Kani. As such, it'll be mentioned in the tutorial and added to the dedicated section planned in [#2208](https://github.com/model-checking/kani/issues/2208). ## Detailed Design @@ -129,9 +129,10 @@ Besides, we don't expect these changes to be updated unless we decide to extend ## Rationale and alternatives -This proposal would enable users to exercise negative verification with a relatively -Moreover, we could use it in our own regression and remove special-cased code to handle this case in `compiletest`. -This is a relatively cheap feature to implement if we compare it take into account the expressivenes it provides. +This proposal would enable users to exercise negative verification with a relatively simple mechanism. +Moreover, it could be used in the Kani regression and remove the special-cased code to handle negative harnesses in `compiletest`. + +Not adding such a mechanism could impact Kani's usability by limiting the harnesses that users can write. ### Alternative #1: Name @@ -146,29 +147,51 @@ Our running example shows an instance of (2): an overflow error doesn't result i So it's better to avoid `panic` in the name. We have also considered two alternatives for the expectation: `should` and `expect`. -To be honest, we've avoided `expect` altogether for two reasons: - - We may consider a more granular approach to indicate expectations regarding individual checks and cover statements in the future. The tentative name for the attribute is `#[kani::expect]`. - - We heavily use this word for testing in Kani. +To be honest, we avoid `expect` altogether for two reasons: + - We may consider a more granular approach to indicate expectations regarding individual checks and cover statements in the future. One possible name for the attribute is `#[kani::expect]`. + - We heavily use this word for testing in Kani: there is an `expected` mode, which works with `*.expected` files. Other modes also use such files. ### Alternative #2: Granularity +As mentioned earlier, users may want to express more granular expectations for their harnesses. +For example, a user may want to specify that a given check results in a failure. +Again, there is a relation between this and the [the `#[should_panic]` attribute](https://doc.rust-lang.org/rust-by-example/testing/unit_testing.html#testing-panics) for Rust tests. +More specifically, the `#[should_panic]` attribute may receive an argument `expected` which allows users to specify the expected panic string: -- What are the pros and cons of this design? -- What is the impact of not doing this? -- What other designs have you considered? Why didn't you choose them? +```rust + #[test] + #[should_panic(expected = "Divide result is zero")] + fn test_specific_panic() { + divide_non_zero_result(1, 10); + } +``` + +In principle, it wouldn't be a problem to extend this proposal to include the `expected` argument. +The implementation could compare the `expected` string against property descriptions. + +However, there could be some problems later with this approach: + * What if users want to specify multiple `expected` strings? + * What if users don't want to only check for failures? + * In the previous case, would they expect the overall verification to fail or not? + +We don't know if these will be requirements in the future. +If they were, then we'd need to come up with language to state expectations about properties (checks or cover statements). +A good option to consider here is adding the single-string `expected` argument (as in `#[should_panic]`) and see how it's used. +It could be the cause of a breaking change in the future, but it would provide us with useful data in the meatime. ## Open questions -- Is there any part of the design that you expect to resolve through the RFC process? -- What kind of user feedback do you expect to gather before stabilization? How will this impact your design? +The main question I'd like to get resolved are: + * Do we want to extend `#[kani::should_fail]` with an `expected` field? -## Future possibilities +Once the feature is available, it'd be good to gather user feedback to answer these questions: + 1. Do we need a mechanism to express more granular expectations or it's (1) enough? + 2. If we need the mechanism in (2), do we really want to collapse them into one feature? -What are natural extensions and possible improvements that you predict for this feature that is out of the -scope of this RFC? Feel free to brainstorm here. +## Future possibilities - * More granular checks. - * Attribute auto-generation from `kani::proof` + * The attribute could be an argument to `kani::proof` (`#[kani::proof(should_fail)]` reads very well). + * Other extensions have been discussed earlier. [footnote-compiletest]: `compiletest` knows that the test should fail because it parses the `// kani-verify-fail` comment at the top. From 8736d28ee88bd43a8c413a75cc303dcb3080bf9f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 10 Mar 2023 22:57:27 +0000 Subject: [PATCH 03/11] Address PR comments --- rfc/src/rfcs/0005-should-fail-attr.md | 175 +++++++++++++++----------- 1 file changed, 103 insertions(+), 72 deletions(-) diff --git a/rfc/src/rfcs/0005-should-fail-attr.md b/rfc/src/rfcs/0005-should-fail-attr.md index cd07d85a9e31..c5b381b5814b 100644 --- a/rfc/src/rfcs/0005-should-fail-attr.md +++ b/rfc/src/rfcs/0005-should-fail-attr.md @@ -1,32 +1,33 @@ -- **Feature Name:** The `kani::should_fail` attribute (`should-fail-attr`)* +- **Feature Name:** The `kani::should_panic` attribute (`should-panic-attr`)* - **Feature Request Issue:** -- **RFC PR:** *Link to original PR* +- **RFC PR:** - **Status:** Under Review - **Version:** 0 - **Proof-of-concept:** *Optional field. If you have implemented a proof of concept, add a link here* ## Summary -Users may want to express that a verification harness should fail. -This RFC proposes a new harness attribute `#[kani::should_fail]` that informs Kani about this expectation. +Users may want to express that a verification harness should panic. +This RFC proposes a new harness attribute `#[kani::should_panic]` that informs Kani about this expectation. ## User Impact -Users may want to express that a verification harness should fail. -In general, users writing such harnesses want to demonstrate that verification results include at least a failure. -Let's refer to this concept as *negative verification*, inspired by the term [negative testing](https://en.wikipedia.org/wiki/Negative_testing). -Negative verification harnesses could be useful to show that invalid inputs result in verification failures, -or increase the overall verification coverage. +Users may want to express that a verification harness should panic. +In general, a user adding such a harness wants to demonstrate that the verification fails because a panic is reachable from the harness. -In fact, some of the tests in the Kani regression are written as negative harnesses. -Currently, we [use comments](https://model-checking.github.io/kani/regression-testing.html#testing-stages) specific to `compiletest` to indicate that a verification failure is expected. -The proposed attribute would provide a way in Kani to express that a verification harness should fail, -allowing users to write negative verification harnesses. +Let's refer to this concept as *negative verification*, +so the relation with [negative testing](https://en.wikipedia.org/wiki/Negative_testing) becomes clearer. +Negative testing can be exercised in Rust unit tests using [the `#[should_panic]` attribute](https://doc.rust-lang.org/rust-by-example/testing/unit_testing.html#testing-panics). +If the `#[should_panic]` attribute is added to a test, `cargo test` will check that the execution of the test results in a panic. +This capability doesn't exist in Kani at the moment, but it would be useful for the same reasons +(e.g., to show that invalid inputs result in verification failures, or increase the overall verification coverage). + +We propose an attribute that allows users to exercise negative verification in Kani. We also acknowledge that, in other cases, users may want to express more granular expectations for their harnesses. -For example, a user may want to specify that a given check results in a failure. +For example, a user may want to specify that a given check is unreachable from the harness. An ergonomic mechanism for informing Kani about such expectations is likely to require other improvements in Kani (a comprehensive classification for checks reported by Kani, a language to describe expectations for checks and cover statements, and general output improvements). -We consider that the mechanism we just mentioned and the one discussed in this proposal solve different problems, so they don't need to be discussed together. +Moving forward, we consider that such a mechanism and this proposal solve different problems, so they don't need to be discussed together. This is further discussed in the [rationale and alternatives](#rationale-and-alternatives) and [future possibilities](#future-possibilities) sections. ## User Experience @@ -36,37 +37,60 @@ The [rationale section](#rationale-and-alternatives) discusses the granularity o ### Single Harness -Let's take an example from the Kani regression: +Let's look at this code: ```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; + } +} + #[kani::proof] -fn simple_add_overflows() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - a + b; +fn cannot_init_device_twice() { + let mut device = Device::new(); + device.init(); + device.init(); } ``` -Currently, this example produces a `VERIFICATION:- FAILED` result.[^footnote-compiletest] +This is what a negative harness may look like. +The user wants to verify that calling `device.init()` more than once should result in a panic. + +> **NOTE**: We could convert this into a Rust unit test and add the `#[should_panic]` attribute to it. +> However, there are two good reasons to have a verification-specific attribute that does the same: +> 1. To ensure that other unexpected behaviors don't occur (e.g., overflows). +> 2. Because `#[should_panic]` cannot be used if the harness contains calls to Kani's API. + +Currently, this example produces a `VERIFICATION:- FAILED` result. In addition, it will return a non-successful code. ```rust #[kani::proof] -#[kani::should_fail] -fn simple_add_overflows() { - let a: u32 = kani::any(); - let b: u32 = kani::any(); - a + b; +#[kani::should_panic] +fn cannot_init_device_twice() { + let mut device = Device::new(); + device.init(); + device.init(); } ``` -Since we added `#[kani::should_fail]`, running this example would produce a successful code. +Since we added `#[kani::should_panic]`, running this example would produce a successful code. Now, we've considered two ways to represent this result in the verification output. Note that it's important that we provide the user with this feedback: - 1. **(Expectation)** Kani was expecting the harness to fail. - 2. **(Outcome)**: The actual verification result that Kani produced after the analysis. -This will avoid a potential scenario where the user doesn't know for sure if the attribute has had an effect when running the verification harness. + 1. **(Expectation)** Was Kani expecting the harness to pass or fail? + 2. **(Outcome)**: What's the actual result that Kani produced after the analysis? +This will avoid a potential scenario where the user doesn't know for sure if the attribute has had an effect when verifying the harness. As mentioned, we've considered two ways to represent this result. @@ -76,7 +100,7 @@ As mentioned, we've considered two ways to represent this result. VERIFICATION:- FAILED (expected FAILED) ``` -We recommend this representation so the user receives clear information about both the outcome and the expectation. +We recommend this representation so the user receives clear information about both the outcome and the expectation.[^footnote-representation] #### Representation #2: Changes to overall result @@ -87,7 +111,7 @@ VERIFICATION:- SUCCESSFUL (expected FAILED and it FAILED) ### Multiple Harnesses When there are multiple harnesses, we'll implement the single-harness changes in addition to the following ones. -Currently, a "Summary" section appears after reporting the results for each harness: +Currently, a "Summary" section appears[^footnote-summary] after reporting the results for each harness: ``` Verification failed for - harness3 Verification failed for - harness2 @@ -95,10 +119,10 @@ Verification failed for - harness1 Complete - 0 successfully verified harnesses, 3 failures, 3 total. ``` -Harnesses marked with `#[kani::should_fail]` won't show unless the expected result was different from the actual result. +Harnesses marked with `#[kani::should_panic]` won't show unless the expected result was different from the actual result. The summary will consider harnesses that match their expectation as "successfully verified harnesses". -Therefore, if we added `#[kani::should_fail]` to all harnesses in the previous example, we'd see this output: +Therefore, if we added `#[kani::should_panic]` to all harnesses in the previous example, we'd see this output: ``` Complete - 3 successfully verified harnesses, 0 failures, 3 total. @@ -107,7 +131,7 @@ Complete - 3 successfully verified harnesses, 0 failures, 3 total. ### Availability This feature will only be available as an attribute. -That means this feature won't be available as a CLI option (i.e., `--should-fail`). +That means this feature won't be available as a CLI option (i.e., `--should-panic`). There are good reasons to avoid the CLI option: - It'd make the design and implementation unnecessarily complex. - It'd only be useful when combined with `--harness` to filter negative harnesses. @@ -115,13 +139,18 @@ There are good reasons to avoid the CLI option: ### Pedagogy -The `#[kani::should_fail]` attribute will become one of the most basic attributes in Kani. +The `#[kani::should_panic]` attribute will become one of the most basic attributes in Kani. As such, it'll be mentioned in the tutorial and added to the dedicated section planned in [#2208](https://github.com/model-checking/kani/issues/2208). +In general, we'll also advise against negative verification when a harness can be written both as a regular (positive) harness and a negative one. +The feature, as it's presented in this proposal, won't allow checking that the panic failure is due to the panic we expected. +So there could be cases where the panic changes, but it goes unnoticed while running Kani. +Because of that, it'll preferred that users write positive harnesses instead. + ## Detailed Design At a high level, we expect modifications in the following components: - - `kani-compiler`: Changes required to (1) process the new attribute, and (2) extend `HarnessMetadata` with a `should_fail: bool` field. + - `kani-compiler`: Changes required to (1) process the new attribute, and (2) extend `HarnessMetadata` with a `should_panic: bool` field. - `kani-driver`: Changes required to (1) edit information about harnesses printed by `kani-driver`, (2) edit verification output when post-processing CBMC verification results, and (3) return the appropriate exit status after post-processing CBMC verification results. We don't expect these changes to require new dependencies. @@ -130,34 +159,26 @@ Besides, we don't expect these changes to be updated unless we decide to extend ## Rationale and alternatives This proposal would enable users to exercise negative verification with a relatively simple mechanism. -Moreover, it could be used in the Kani regression and remove the special-cased code to handle negative harnesses in `compiletest`. - Not adding such a mechanism could impact Kani's usability by limiting the harnesses that users can write. -### Alternative #1: Name +### Alternative #1: Generic failures -Our first choice is made in the name of the attribute. -It should be noted that Rust has a similarly named attribute for unit tests: [the `#[should_panic]` attribute](https://doc.rust-lang.org/rust-by-example/testing/unit_testing.html#testing-panics). -At first, one may think that `#[kani::should_fail]` and `#[should_panic]` have the same semantics. -However, if we keep thinking about this, we'll realize that: - 1. A panic in Rust should always result in a failure in Kani, but - 2. A failure in Kani doesn't always result in a panic in Rust. +This proposal **doesn't consider generic failures but only panics**. +In principle, it's not clear that a mechanism for generic failures would be useful. +Such a mechanism would allow users to expect UB in their harness, but there isn't a clear motivation for doing that. -Our running example shows an instance of (2): an overflow error doesn't result in a panic in Rust. -So it's better to avoid `panic` in the name. +### Alternative #2: Name -We have also considered two alternatives for the expectation: `should` and `expect`. -To be honest, we avoid `expect` altogether for two reasons: +We have considered two alternatives for the "expectation" part of the attribute's name: `should` and `expect`. +We avoid `expect` altogether for two reasons: + - We may consider adding the `expected` argument to `#[kani::should_panic]`. - We may consider a more granular approach to indicate expectations regarding individual checks and cover statements in the future. One possible name for the attribute is `#[kani::expect]`. - We heavily use this word for testing in Kani: there is an `expected` mode, which works with `*.expected` files. Other modes also use such files. -### Alternative #2: Granularity +### Alternative #3: The `expected` argument -As mentioned earlier, users may want to express more granular expectations for their harnesses. -For example, a user may want to specify that a given check results in a failure. - -Again, there is a relation between this and the [the `#[should_panic]` attribute](https://doc.rust-lang.org/rust-by-example/testing/unit_testing.html#testing-panics) for Rust tests. -More specifically, the `#[should_panic]` attribute may receive an argument `expected` which allows users to specify the expected panic string: +We could consider an `expected` argument, similar to [the `#[should_panic]` attribute](https://doc.rust-lang.org/rust-by-example/testing/unit_testing.html#testing-panics). +To be clear, the `#[should_panic]` attribute may receive an argument `expected` which allows users to specify the expected panic string: ```rust #[test] @@ -167,31 +188,41 @@ More specifically, the `#[should_panic]` attribute may receive an argument `expe } ``` -In principle, it wouldn't be a problem to extend this proposal to include the `expected` argument. -The implementation could compare the `expected` string against property descriptions. +In principle, we anticipate that we'll extend this proposal to include the `expected` argument at some point. +The implementation could compare the `expected` string against the panic string. + +At present, the only technical limitation is that panic strings printed in Kani aren't formatted. +One option is to use substrings to compare. +However, the long-term solution is to use concrete playback to *replay* the panic and match against the expected panic string. +By doing this, we would achieve feature parity with Rust's `#[should_panic]`. -However, there could be some problems later with this approach: - * What if users want to specify multiple `expected` strings? - * What if users don't want to only check for failures? +### Alternative #4: Granularity + +As mentioned earlier, users may want to express more granular expectations for their harnesses. + +There could be problems with this proposal if we attempt to do both: + * What if users don't want to only check for failures (e.g., reachability)? * In the previous case, would they expect the overall verification to fail or not? + * How do we want these expectations to be declared? -We don't know if these will be requirements in the future. -If they were, then we'd need to come up with language to state expectations about properties (checks or cover statements). -A good option to consider here is adding the single-string `expected` argument (as in `#[should_panic]`) and see how it's used. -It could be the cause of a breaking change in the future, but it would provide us with useful data in the meatime. +We don't have sufficient data about the use-case considered in this alternative. +This proposal can also contribute to collect this data: once users can expect panics, they may want to expect other things. ## Open questions -The main question I'd like to get resolved are: - * Do we want to extend `#[kani::should_fail]` with an `expected` field? +The main questions I'd like to get resolved are: + - What is the best representation to use for this feature? + - Do we want to extend `#[kani::should_panic]` with an `expected` field? Once the feature is available, it'd be good to gather user feedback to answer these questions: - 1. Do we need a mechanism to express more granular expectations or it's (1) enough? - 2. If we need the mechanism in (2), do we really want to collapse them into one feature? + - Do we need a mechanism to express more granular expectations? + - If we need the mechanism in (2), do we really want to collapse them into one feature? ## Future possibilities - * The attribute could be an argument to `kani::proof` (`#[kani::proof(should_fail)]` reads very well). - * Other extensions have been discussed earlier. + - The attribute could be an argument to `kani::proof` (`#[kani::proof(should_panic)]` reads very well). + - Add an `expected` argument to `#[kani::should_panic]`, and *replay* the harness with concrete playback to get the actual panic string. + +[^footnote-representation]: Double negation may not be the best representation, but it's at least accurate with respect to the original result. -[footnote-compiletest]: `compiletest` knows that the test should fail because it parses the `// kani-verify-fail` comment at the top. +[^footnote-summary]: This summary is printed in both the default and terse outputs. From 1a774ce3ddd2f7bc4d73bb1989922455165fb1e9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 10 Mar 2023 23:12:40 +0000 Subject: [PATCH 04/11] Comments about multiple panics --- rfc/src/rfcs/0005-should-fail-attr.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/rfc/src/rfcs/0005-should-fail-attr.md b/rfc/src/rfcs/0005-should-fail-attr.md index c5b381b5814b..c4b18fbf4c9b 100644 --- a/rfc/src/rfcs/0005-should-fail-attr.md +++ b/rfc/src/rfcs/0005-should-fail-attr.md @@ -156,6 +156,11 @@ At a high level, we expect modifications in the following components: We don't expect these changes to require new dependencies. Besides, we don't expect these changes to be updated unless we decide to extend the attribute with further fields (see [Future possibilities](#future-possibilities) for more details). +There is one design aspect that needs discussion: What should happen if multiple panics are triggered? +It seems that this scenario is less likely, but it's certainly possible and we may want to prevent it. +The initial proposal is for `#[kani::should_panic]` to check that only one panic occurs in the harness +This would also simplify [adding an `expected` argument](#alternative-3-the-expected-argument) later. + ## Rationale and alternatives This proposal would enable users to exercise negative verification with a relatively simple mechanism. @@ -213,6 +218,7 @@ This proposal can also contribute to collect this data: once users can expect pa The main questions I'd like to get resolved are: - What is the best representation to use for this feature? - Do we want to extend `#[kani::should_panic]` with an `expected` field? + - Do we want to allow multiple panics with `#[kani::should_panic]`. Once the feature is available, it'd be good to gather user feedback to answer these questions: - Do we need a mechanism to express more granular expectations? From 0fe6f3ab63d42c31d89ff39973a6254459429f4f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 10 Mar 2023 23:22:02 +0000 Subject: [PATCH 05/11] Correct `SUMMARY.md` and emphasis --- rfc/src/SUMMARY.md | 2 +- rfc/src/rfcs/0005-should-fail-attr.md | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/rfc/src/SUMMARY.md b/rfc/src/SUMMARY.md index 51cef60366ce..78e5a845ef04 100644 --- a/rfc/src/SUMMARY.md +++ b/rfc/src/SUMMARY.md @@ -9,4 +9,4 @@ - [0001-mir-linker](rfcs/0001-mir-linker.md) - [0002-function-stubbing](rfcs/0002-function-stubbing.md) - [0003-cover-statement](rfcs/0003-cover-statement.md) -- [0005-should-fail-attr](rfcs/0005-should-fail-attr.md) +- [0005-should-panic-attr](rfcs/0005-should-panic-attr.md) diff --git a/rfc/src/rfcs/0005-should-fail-attr.md b/rfc/src/rfcs/0005-should-fail-attr.md index c4b18fbf4c9b..791b9660b6f7 100644 --- a/rfc/src/rfcs/0005-should-fail-attr.md +++ b/rfc/src/rfcs/0005-should-fail-attr.md @@ -3,7 +3,7 @@ - **RFC PR:** - **Status:** Under Review - **Version:** 0 -- **Proof-of-concept:** *Optional field. If you have implemented a proof of concept, add a link here* +- **Proof-of-concept:** N/A ## Summary @@ -32,7 +32,7 @@ This is further discussed in the [rationale and alternatives](#rationale-and-alt ## User Experience -The scope of this functionality is limited to the overall verification result. +The scope of this functionality is **limited to the overall verification result**. The [rationale section](#rationale-and-alternatives) discusses the granularity of failures, and how this attribute could be extended. ### Single Harness @@ -69,7 +69,7 @@ The user wants to verify that calling `device.init()` more than once should resu > **NOTE**: We could convert this into a Rust unit test and add the `#[should_panic]` attribute to it. > However, there are two good reasons to have a verification-specific attribute that does the same: > 1. To ensure that other unexpected behaviors don't occur (e.g., overflows). -> 2. Because `#[should_panic]` cannot be used if the harness contains calls to Kani's API. +> 2. Because `#[should_panic]` cannot be used if the test harness contains calls to Kani's API. Currently, this example produces a `VERIFICATION:- FAILED` result. In addition, it will return a non-successful code. @@ -130,7 +130,7 @@ Complete - 3 successfully verified harnesses, 0 failures, 3 total. ### Availability -This feature will only be available as an attribute. +This feature **will only be available as an attribute**. That means this feature won't be available as a CLI option (i.e., `--should-panic`). There are good reasons to avoid the CLI option: - It'd make the design and implementation unnecessarily complex. @@ -142,7 +142,7 @@ There are good reasons to avoid the CLI option: The `#[kani::should_panic]` attribute will become one of the most basic attributes in Kani. As such, it'll be mentioned in the tutorial and added to the dedicated section planned in [#2208](https://github.com/model-checking/kani/issues/2208). -In general, we'll also advise against negative verification when a harness can be written both as a regular (positive) harness and a negative one. +In general, **we'll also advise against negative verification** when a harness can be written both as a regular (positive) harness and a negative one. The feature, as it's presented in this proposal, won't allow checking that the panic failure is due to the panic we expected. So there could be cases where the panic changes, but it goes unnoticed while running Kani. Because of that, it'll preferred that users write positive harnesses instead. @@ -156,7 +156,7 @@ At a high level, we expect modifications in the following components: We don't expect these changes to require new dependencies. Besides, we don't expect these changes to be updated unless we decide to extend the attribute with further fields (see [Future possibilities](#future-possibilities) for more details). -There is one design aspect that needs discussion: What should happen if multiple panics are triggered? +There is one design aspect that needs discussion: **What should happen if multiple panics are triggered?** It seems that this scenario is less likely, but it's certainly possible and we may want to prevent it. The initial proposal is for `#[kani::should_panic]` to check that only one panic occurs in the harness This would also simplify [adding an `expected` argument](#alternative-3-the-expected-argument) later. From 698067b1fbd8f585bb5a58c69d212167d69467c0 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 20 Mar 2023 20:59:19 +0000 Subject: [PATCH 06/11] Add example for multiple panics --- rfc/src/rfcs/0005-should-fail-attr.md | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/rfc/src/rfcs/0005-should-fail-attr.md b/rfc/src/rfcs/0005-should-fail-attr.md index 791b9660b6f7..740a76386709 100644 --- a/rfc/src/rfcs/0005-should-fail-attr.md +++ b/rfc/src/rfcs/0005-should-fail-attr.md @@ -157,9 +157,25 @@ We don't expect these changes to require new dependencies. Besides, we don't expect these changes to be updated unless we decide to extend the attribute with further fields (see [Future possibilities](#future-possibilities) for more details). There is one design aspect that needs discussion: **What should happen if multiple panics are triggered?** -It seems that this scenario is less likely, but it's certainly possible and we may want to prevent it. -The initial proposal is for `#[kani::should_panic]` to check that only one panic occurs in the harness -This would also simplify [adding an `expected` argument](#alternative-3-the-expected-argument) later. +In other words, in the example +```rust +#[kani::proof] +#[kani::should_panic] +fn branch_panics() { + let b: bool = kani::any(); + + do_something(); + + if b { + call_panic_1(); // leads to a panic-related failure + } else { + call_panic_2(); // leads to a different panic-related failure + } +} +``` +should `#[kani::should_panic]` return a succesful verification code? + +While this scenario is less likely, we may want to return a failed verification in this case. ## Rationale and alternatives From 05d6f032f8757a77b1d072a222362ce5f9bdf5e0 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 21 Mar 2023 19:03:02 +0000 Subject: [PATCH 07/11] Update representations and recommend #2 --- rfc/src/rfcs/0005-should-fail-attr.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/rfc/src/rfcs/0005-should-fail-attr.md b/rfc/src/rfcs/0005-should-fail-attr.md index 740a76386709..daf311ab2137 100644 --- a/rfc/src/rfcs/0005-should-fail-attr.md +++ b/rfc/src/rfcs/0005-should-fail-attr.md @@ -88,24 +88,24 @@ Since we added `#[kani::should_panic]`, running this example would produce a suc Now, we've considered two ways to represent this result in the verification output. Note that it's important that we provide the user with this feedback: - 1. **(Expectation)** Was Kani expecting the harness to pass or fail? + 1. **(Expectation)** Was Kani expecting the harness to panic? 2. **(Outcome)**: What's the actual result that Kani produced after the analysis? This will avoid a potential scenario where the user doesn't know for sure if the attribute has had an effect when verifying the harness. As mentioned, we've considered two ways to represent this result. -#### Representation #1 (Recommended): No changes to overall result +#### Representation #1: No changes to overall result ```rust -VERIFICATION:- FAILED (expected FAILED) +VERIFICATION:- FAILED (expected one panic at least) ``` We recommend this representation so the user receives clear information about both the outcome and the expectation.[^footnote-representation] -#### Representation #2: Changes to overall result +#### Representation #2 (Recommended): Changes to overall result ```rust -VERIFICATION:- SUCCESSFUL (expected FAILED and it FAILED) +VERIFICATION:- SUCCESSFUL (expected and verified one panic at least) ``` ### Multiple Harnesses From 84d1b4f4897dc178bb504efdf5cbe1c7bcc6b390 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 21 Mar 2023 20:06:34 +0000 Subject: [PATCH 08/11] Move multi-panic to UX, answer questions, new alternative --- rfc/src/rfcs/0005-should-fail-attr.md | 65 ++++++++++++++++----------- 1 file changed, 39 insertions(+), 26 deletions(-) diff --git a/rfc/src/rfcs/0005-should-fail-attr.md b/rfc/src/rfcs/0005-should-fail-attr.md index daf311ab2137..b8155d197d6c 100644 --- a/rfc/src/rfcs/0005-should-fail-attr.md +++ b/rfc/src/rfcs/0005-should-fail-attr.md @@ -128,6 +128,32 @@ Therefore, if we added `#[kani::should_panic]` to all harnesses in the previous Complete - 3 successfully verified harnesses, 0 failures, 3 total. ``` +### Multiple panics + +In a verification context, an execution can branch into multiple executions that depend on a condition. +This may result in a situation where different panics are reachable, as in this example: + +```rust +#[kani::proof] +#[kani::should_panic] +fn branch_panics() { + let b: bool = kani::any(); + + do_something(); + + if b { + call_panic_1(); // leads to a panic-related failure + } else { + call_panic_2(); // leads to a different panic-related failure + } +} +``` + +Note that we could safeguard against these situations by checking that only one panic-related failure is reachable. +However, users have expressed that a *coarse* version (i.e., checking that at least one panic can be reached) is preferred. +Users also anticipate that `#[kani::should_panic]` will be used to exercise [smoke testing](https://en.wikipedia.org/wiki/Smoke_testing_(software)) in many cases. +Additionally, restricting `#[kani::should_panic]` to the verification of single panic-related failures could be confusing for users and reduce its overall usefulness. + ### Availability This feature **will only be available as an attribute**. @@ -156,27 +182,6 @@ At a high level, we expect modifications in the following components: We don't expect these changes to require new dependencies. Besides, we don't expect these changes to be updated unless we decide to extend the attribute with further fields (see [Future possibilities](#future-possibilities) for more details). -There is one design aspect that needs discussion: **What should happen if multiple panics are triggered?** -In other words, in the example -```rust -#[kani::proof] -#[kani::should_panic] -fn branch_panics() { - let b: bool = kani::any(); - - do_something(); - - if b { - call_panic_1(); // leads to a panic-related failure - } else { - call_panic_2(); // leads to a different panic-related failure - } -} -``` -should `#[kani::should_panic]` return a succesful verification code? - -While this scenario is less likely, we may want to return a failed verification in this case. - ## Rationale and alternatives This proposal would enable users to exercise negative verification with a relatively simple mechanism. @@ -229,17 +234,25 @@ There could be problems with this proposal if we attempt to do both: We don't have sufficient data about the use-case considered in this alternative. This proposal can also contribute to collect this data: once users can expect panics, they may want to expect other things. -## Open questions +### Alternative #5: Kani API -The main questions I'd like to get resolved are: - - What is the best representation to use for this feature? - - Do we want to extend `#[kani::should_panic]` with an `expected` field? - - Do we want to allow multiple panics with `#[kani::should_panic]`. +This functionality could be part of the Kani API instead of being an attribute. +For example, some contributors proposed a function that takes a predicate closure to filter executions and check that they result in a panic. + +However, such a function couldn't be used in external code, limiting its usability to the user's code. + +## Open questions Once the feature is available, it'd be good to gather user feedback to answer these questions: - Do we need a mechanism to express more granular expectations? - If we need the mechanism in (2), do we really want to collapse them into one feature? +### Resolved questions + + - *What is the best representation to use for this feature?* Representation #2 seems to be preferred, according to feedback we received during a discussion. + - *Do we want to extend `#[kani::should_panic]` with an `expected` field?* Yes, but not in this version. + - *Do we want to allow multiple panic-related failures with `#[kani::should_panic]`?* Yes (this is now discussed in [User Experience](#user-experience)). + ## Future possibilities - The attribute could be an argument to `kani::proof` (`#[kani::proof(should_panic)]` reads very well). From 5af36bb35cc17eeb574813278b2a2203f314ad7c Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 21 Mar 2023 21:42:05 +0000 Subject: [PATCH 09/11] Add third reason --- rfc/src/rfcs/0005-should-fail-attr.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/rfc/src/rfcs/0005-should-fail-attr.md b/rfc/src/rfcs/0005-should-fail-attr.md index b8155d197d6c..1f6086797592 100644 --- a/rfc/src/rfcs/0005-should-fail-attr.md +++ b/rfc/src/rfcs/0005-should-fail-attr.md @@ -67,9 +67,10 @@ This is what a negative harness may look like. The user wants to verify that calling `device.init()` more than once should result in a panic. > **NOTE**: We could convert this into a Rust unit test and add the `#[should_panic]` attribute to it. -> However, there are two good reasons to have a verification-specific attribute that does the same: +> However, there are a few good reasons to have a verification-specific attribute that does the same: > 1. To ensure that other unexpected behaviors don't occur (e.g., overflows). > 2. Because `#[should_panic]` cannot be used if the test harness contains calls to Kani's API. +> 3. To ensure that a panic still occurs after stubbing out code which is expected to panic. Currently, this example produces a `VERIFICATION:- FAILED` result. In addition, it will return a non-successful code. From 2848cb2e2e54d80cfabd90a1dab19ad6c5b551e1 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 21 Mar 2023 22:32:02 +0000 Subject: [PATCH 10/11] Add note on representation --- rfc/src/rfcs/0005-should-fail-attr.md | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/rfc/src/rfcs/0005-should-fail-attr.md b/rfc/src/rfcs/0005-should-fail-attr.md index 1f6086797592..bb9a9826157c 100644 --- a/rfc/src/rfcs/0005-should-fail-attr.md +++ b/rfc/src/rfcs/0005-should-fail-attr.md @@ -98,10 +98,12 @@ As mentioned, we've considered two ways to represent this result. #### Representation #1: No changes to overall result ```rust -VERIFICATION:- FAILED (expected one panic at least) +VERIFICATION:- FAILED (expected and verified one panic at least) ``` -We recommend this representation so the user receives clear information about both the outcome and the expectation.[^footnote-representation] +In this representation, both expectation and the outcome are clear[^footnote-representation], but the result doesn't change. +This could be confusing. + #### Representation #2 (Recommended): Changes to overall result @@ -109,6 +111,9 @@ We recommend this representation so the user receives clear information about bo VERIFICATION:- SUCCESSFUL (expected and verified one panic at least) ``` +In this representation, both expectation and the outcome are clear, and the verification result changes. +We recommend this representation. + ### Multiple Harnesses When there are multiple harnesses, we'll implement the single-harness changes in addition to the following ones. From dd6c972d18d64b631150fe0d5edba014a0f1c270 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 23 Mar 2023 19:12:47 +0000 Subject: [PATCH 11/11] Link to PoC, extend representation --- rfc/src/rfcs/0005-should-fail-attr.md | 30 +++++++++++---------------- 1 file changed, 12 insertions(+), 18 deletions(-) diff --git a/rfc/src/rfcs/0005-should-fail-attr.md b/rfc/src/rfcs/0005-should-fail-attr.md index bb9a9826157c..a5dcff085d2d 100644 --- a/rfc/src/rfcs/0005-should-fail-attr.md +++ b/rfc/src/rfcs/0005-should-fail-attr.md @@ -3,7 +3,7 @@ - **RFC PR:** - **Status:** Under Review - **Version:** 0 -- **Proof-of-concept:** N/A +- **Proof-of-concept:** ## Summary @@ -93,26 +93,20 @@ Note that it's important that we provide the user with this feedback: 2. **(Outcome)**: What's the actual result that Kani produced after the analysis? This will avoid a potential scenario where the user doesn't know for sure if the attribute has had an effect when verifying the harness. -As mentioned, we've considered two ways to represent this result. +Below, we show how we'll represent this result. -#### Representation #1: No changes to overall result - -```rust -VERIFICATION:- FAILED (expected and verified one panic at least) -``` - -In this representation, both expectation and the outcome are clear[^footnote-representation], but the result doesn't change. -This could be confusing. +#### Recommended Representation: Changes to overall result +The representation must make clear both the expectation and the outcome. +Moreover, the overall result must change according to the verification results (i.e., the failures that were found). -#### Representation #2 (Recommended): Changes to overall result - -```rust -VERIFICATION:- SUCCESSFUL (expected and verified one panic at least) -``` +Using the `#[kani::should_panic]` attribute will return one of the following results: + 1. `VERIFICATION:- FAILED (encountered no panics, but at least one was expected)` if there were no failures. + 2. `VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)` if there were failures but not all them had `prop.property_class() == "assertion"`. + 3. `VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)` otherwise. -In this representation, both expectation and the outcome are clear, and the verification result changes. -We recommend this representation. +Note that the criteria to achieve a `SUCCESSFUL` result depends on all failures having the property class `"assertion"`. +If they don't, then the failed properties may contain UB, so we return a `FAILED` result instead. ### Multiple Harnesses @@ -255,7 +249,7 @@ Once the feature is available, it'd be good to gather user feedback to answer th ### Resolved questions - - *What is the best representation to use for this feature?* Representation #2 seems to be preferred, according to feedback we received during a discussion. + - *What is the best representation to use for this feature?* A representation that changes the overall result seems to be preferred, according to feedback we received during a discussion. - *Do we want to extend `#[kani::should_panic]` with an `expected` field?* Yes, but not in this version. - *Do we want to allow multiple panic-related failures with `#[kani::should_panic]`?* Yes (this is now discussed in [User Experience](#user-experience)).