From fd12a28932e93b49ca7418299e88f28fd238786b Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 12 Jan 2024 14:56:24 -0500 Subject: [PATCH] Rethink `should_panic` and `fail_uncoverable` options as global conditions (#2967) This PR is the next step to rework/introduce the `should_panic`/`fail_uncoverable` options as global conditions. Until now, we haven't had a concrete proposal to do so other than the implementation in #2532. This PR presents one for each option in their respective RFCs. I'd like to agree on this design before starting the code review for #2532. Related to #1905 #2272 #2299 #2516 --- rfc/src/rfcs/0003-cover-statement.md | 13 +++++++++++-- rfc/src/rfcs/0005-should-panic-attr.md | 27 +++++++++++++++----------- 2 files changed, 27 insertions(+), 13 deletions(-) diff --git a/rfc/src/rfcs/0003-cover-statement.md b/rfc/src/rfcs/0003-cover-statement.md index 320bc53aebe3..6839af22f929 100644 --- a/rfc/src/rfcs/0003-cover-statement.md +++ b/rfc/src/rfcs/0003-cover-statement.md @@ -2,7 +2,7 @@ - **Feature Request Issue:** - **RFC PR:** - **Status:** Unstable -- **Version:** 0 +- **Version:** 1 ------------------- @@ -85,7 +85,16 @@ fn foo() { } ``` -We can consider adding an option that would cause verification to fail if a cover property was unsatisfiable or unreachable, e.g. `--fail-uncoverable`. +The `--fail-uncoverable` option will allow users to fail the verification if a cover property is unsatisfiable or unreachable. +This option will be integrated within the framework of [Global Conditions](https://model-checking.github.io/kani/rfc/rfcs/0007-global-conditions.html), which is used to define properties that depend on other properties. + +Using the `--fail-uncoverable` option will enable the global condition with name `fail_uncoverable`. +Following the format for global conditions, the outcome will be one of the following: + 1. `` - fail_uncoverable: FAILURE (expected all cover statements to be satisfied, but at least one was not)`` + 2. `` - fail_uncoverable: SUCCESS (all cover statements were satisfied as expected)`` + +Note that the criteria to achieve a `SUCCESS` status depends on all properties of the `"cover"` class having a `SATISFIED` status. +Otherwise, we return a `FAILURE` status. ### Inclusion in the Verification Summary diff --git a/rfc/src/rfcs/0005-should-panic-attr.md b/rfc/src/rfcs/0005-should-panic-attr.md index 1f4aafb599e6..80d9b59c40f4 100644 --- a/rfc/src/rfcs/0005-should-panic-attr.md +++ b/rfc/src/rfcs/0005-should-panic-attr.md @@ -2,8 +2,10 @@ - **Feature Request Issue:** - **RFC PR:** - **Status:** Unstable -- **Version:** 0 -- **Proof-of-concept:** +- **Version:** 1 +- **Proof-of-concept:** + * Version 0: + * Version 1: ------------------- @@ -95,20 +97,23 @@ 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. +Therefore, the representation must make clear both the expectation and the outcome. Below, we show how we'll represent this result. -#### 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). +#### Recommended Representation: As a Global Condition -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. +The `#[kani::should_panic]` attribute essentially behaves as a property that depends on other properties. +This makes it well-suited for integration within the framework of [Global Conditions](https://model-checking.github.io/kani/rfc/rfcs/0007-global-conditions.html). -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. +Using the `#[kani::should_panic]` attribute will enable the global condition with name `should_panic`. +Following the format for global conditions, the outcome will be one of the following: + 1. `` - `should_panic`: FAILURE (encountered no panics, but at least one was expected)`` if there were no failures. + 2. `` - `should_panic`: FAILURE (encountered failures other than panics, which were unexpected)`` if there were failures but not all them had `prop.property_class() == "assertion"`. + 3. `` - `should_panic`: SUCCESS (encountered one or more panics as expected)`` otherwise. + +Note that the criteria to achieve a `SUCCESS` status depends on all failed properties having the property class `"assertion"`. +If they don't, then the failed properties may contain UB, so we return a `FAILURE` status instead. ### Multiple Harnesses