From caff2c71bc8bd1ac59f3f27d431e42590286acb8 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 3 Jan 2024 22:29:05 +0000 Subject: [PATCH 1/3] Recommend to represent `should_panic` as global condition --- rfc/src/rfcs/0005-should-panic-attr.md | 27 +++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) 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 From 29af80d5fff2da46e8bf0e2a6fa5bd872dfae5d4 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 3 Jan 2024 22:45:54 +0000 Subject: [PATCH 2/3] Recommend to represent `--fail-uncoverable` as a global condition --- rfc/src/rfcs/0003-cover-statement.md | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/rfc/src/rfcs/0003-cover-statement.md b/rfc/src/rfcs/0003-cover-statement.md index 320bc53aebe3..092f8d8d18b3 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 (encountered one or more cover statements which were not satisfied)`` + 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 From 709253b2b875db636ba6d197c63ac16dd174b9c1 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 12 Jan 2024 13:22:16 -0500 Subject: [PATCH 3/3] Update one of the outcomes for `fail_uncoverable` --- rfc/src/rfcs/0003-cover-statement.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rfc/src/rfcs/0003-cover-statement.md b/rfc/src/rfcs/0003-cover-statement.md index 092f8d8d18b3..6839af22f929 100644 --- a/rfc/src/rfcs/0003-cover-statement.md +++ b/rfc/src/rfcs/0003-cover-statement.md @@ -90,7 +90,7 @@ This option will be integrated within the framework of [Global Conditions](https 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 (encountered one or more cover statements which were not satisfied)`` + 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.