From cecc910278c22579360b3940c3ddb5f6dc366701 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 15 Nov 2022 15:48:48 -0800 Subject: [PATCH 1/6] RFC for cover ctatement --- rfc/src/SUMMARY.md | 2 +- rfc/src/rfcs/0003-cover-statement.md | 76 ++++++++++++++++++++++++++++ 2 files changed, 77 insertions(+), 1 deletion(-) create mode 100644 rfc/src/rfcs/0003-cover-statement.md diff --git a/rfc/src/SUMMARY.md b/rfc/src/SUMMARY.md index c98698d2ce6a..ade6c44df5df 100644 --- a/rfc/src/SUMMARY.md +++ b/rfc/src/SUMMARY.md @@ -8,4 +8,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) diff --git a/rfc/src/rfcs/0003-cover-statement.md b/rfc/src/rfcs/0003-cover-statement.md new file mode 100644 index 000000000000..7a0d5ab9c5cd --- /dev/null +++ b/rfc/src/rfcs/0003-cover-statement.md @@ -0,0 +1,76 @@ +- **Feature Name:** Cover statement `cover_statement` +- **Feature Request Issue:** +- **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 + +A new Kani API that allows users to check that a certain condition can occur at a specific location in the code. + +## User Impact + +Users typically want to gain confidence that a proof checks what it is supposed to check, i.e. that properties are not passing vacuously due to an over-constrained environment. + +A new Kani function, `cover` will be created with the following signature: +```rust +fn cover(cond: bool) +``` +This function can be used for checking that a certain condition _can_ occur at a specific location in the code, to verify, for example, that assumptions are not ruling out those conditions, e.g.: +```rust +let mut v: Vec = Vec::new(); +let len: usize = kani::any(); +kani::assume(len < 5); +for _i in 0..len { + v.push(kani::any()); +} +// make sure we can get a vector of length 5 +kani::cover(v.len() == 5); +``` +This is typically used to ensure that verified checks are not passing _vacuously_, e.g. due to overconstrained pre-conditions. + +The special case of verifying that a certain line of code is reachable can be achieved using `kani::cover(true)`, e.g. +```rust +match x { + val_1 => ..., + val_2 => ..., + ... + val_i => kani::cover(true), // verify that `x` can be `val_i` +} +``` + +## User Experience + +The `cover` function instructs Kani to find _at least one_ possible execution that satisfies the specified condition at that line of code. If there is no such execution, verification *fails*. + +Each cover statements will be reported as a check whose description is "condition is satisfiable" and whose status is: +- `SUCCESS` (green): if Kani found an execution that would cover the condition +- `FAILURE` (red): if Kani proved that the condition cannot be satisfied + +## Detailed Design + +The implementation will touch the following components: +- Kani library: The `cover` function will be added there +- `kani-compiler`: The `cover` function will be handled via a hook and codegen as an assertion (`cover(cond)` will be codegen as `assert(!cond)`) +- `kani-driver`: The CBMC output parser will extract cover properties through their property class, and their result will be flipped. + +## Rationale and alternatives + +- What is the impact of not doing this? +The current workaround to accomplish the same effect of verifying that a condition can be covered is to use `assert!(!cond)`. +However, if the condition can indeed be covered, verification would fail due to the failure of the assertion. + +## Open questions + +## Other Considerations + +We need to make sure the concrete playback feature can be used with `cover` statements that were found to be coverable. + +## Future possibilities + +Users may want to specify a custom message for the cover property, in which case, we may consider adding a separate function that takes a static `str`, e.g. +```rust +fn cover_msg(cond: bool, msg: &'static str) +``` +or a `cover` macro (similar to Rust's `assert` macro). From bb26594b6099c9bbd7907663db8111ef85b90fcc Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 15 Nov 2022 18:11:02 -0800 Subject: [PATCH 2/6] AClarify the interaction with failed unwinding assertions and reachable unsupported constructs --- rfc/src/rfcs/0003-cover-statement.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/rfc/src/rfcs/0003-cover-statement.md b/rfc/src/rfcs/0003-cover-statement.md index 7a0d5ab9c5cd..c598cd57c855 100644 --- a/rfc/src/rfcs/0003-cover-statement.md +++ b/rfc/src/rfcs/0003-cover-statement.md @@ -45,9 +45,19 @@ match x { The `cover` function instructs Kani to find _at least one_ possible execution that satisfies the specified condition at that line of code. If there is no such execution, verification *fails*. Each cover statements will be reported as a check whose description is "condition is satisfiable" and whose status is: -- `SUCCESS` (green): if Kani found an execution that would cover the condition +- `SUCCESS` (green): if Kani found an execution that satisfies the condition - `FAILURE` (red): if Kani proved that the condition cannot be satisfied +For example: +``` +Check 2: main.cover.2 + - Status: SUCCESS + - Description: "condition is satisfiable" + - Location: foo.rs:9:5 in function main +``` + +If one or more unwinding assertions fail or an unsupported construct is found to be reachable, and Kani proved that the condition cannot be satisfied, the result will be reported as `UNDETERMINED` instead of `FAILURE`. + ## Detailed Design The implementation will touch the following components: From 21bbc24bc960678c745771df0bb4d61e5bead454 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Wed, 16 Nov 2022 16:33:47 -0800 Subject: [PATCH 3/6] Address PR comments --- rfc/src/rfcs/0003-cover-statement.md | 59 ++++++++++++++++++---------- 1 file changed, 39 insertions(+), 20 deletions(-) diff --git a/rfc/src/rfcs/0003-cover-statement.md b/rfc/src/rfcs/0003-cover-statement.md index c598cd57c855..23b398ba6093 100644 --- a/rfc/src/rfcs/0003-cover-statement.md +++ b/rfc/src/rfcs/0003-cover-statement.md @@ -13,11 +13,8 @@ A new Kani API that allows users to check that a certain condition can occur at Users typically want to gain confidence that a proof checks what it is supposed to check, i.e. that properties are not passing vacuously due to an over-constrained environment. -A new Kani function, `cover` will be created with the following signature: -```rust -fn cover(cond: bool) -``` -This function can be used for checking that a certain condition _can_ occur at a specific location in the code, to verify, for example, that assumptions are not ruling out those conditions, e.g.: +A new Kani macro, `cover` will be created that can be used for checking that a certain condition _can_ occur at a specific location in the code. +The purpose of the macro is to verify, for example, that assumptions are not ruling out those conditions, e.g.: ```rust let mut v: Vec = Vec::new(); let len: usize = kani::any(); @@ -26,33 +23,43 @@ for _i in 0..len { v.push(kani::any()); } // make sure we can get a vector of length 5 -kani::cover(v.len() == 5); +kani::cover!(v.len() == 5); ``` This is typically used to ensure that verified checks are not passing _vacuously_, e.g. due to overconstrained pre-conditions. -The special case of verifying that a certain line of code is reachable can be achieved using `kani::cover(true)`, e.g. +The special case of verifying that a certain line of code is reachable can be achieved using `kani::cover!(true)`, e.g. ```rust match x { val_1 => ..., val_2 => ..., ... - val_i => kani::cover(true), // verify that `x` can be `val_i` + val_i => kani::cover!(true), // verify that `x` can take the value `val_i` } ``` +Similar to Rust's `assert` macro, a custom message can be specified, e.g. +```rust +kani::cover!(x > y, "x can be greater than y"); +``` + ## User Experience -The `cover` function instructs Kani to find _at least one_ possible execution that satisfies the specified condition at that line of code. If there is no such execution, verification *fails*. +The `cover` macro instructs Kani to find _at least one_ possible execution that satisfies the specified condition at that line of code. If no such execution is possible, verification *fails*. -Each cover statements will be reported as a check whose description is "condition is satisfiable" and whose status is: +Each cover statements will be reported as a check whose description is `condition "cond" is satisfiable` and whose status is: - `SUCCESS` (green): if Kani found an execution that satisfies the condition - `FAILURE` (red): if Kani proved that the condition cannot be satisfied +- `FAILURE (UNREACHABLE)` (red): if Kani proved that the cover statement itself cannot be reached -For example: +For example, for the following `cover` statement: +```rust +kani::cover!(a == 0); +``` +The result can be: ``` Check 2: main.cover.2 - Status: SUCCESS - - Description: "condition is satisfiable" + - Description: "condition "a == 0" is satisfiable" - Location: foo.rs:9:5 in function main ``` @@ -61,26 +68,38 @@ If one or more unwinding assertions fail or an unsupported construct is found to ## Detailed Design The implementation will touch the following components: -- Kani library: The `cover` function will be added there -- `kani-compiler`: The `cover` function will be handled via a hook and codegen as an assertion (`cover(cond)` will be codegen as `assert(!cond)`) -- `kani-driver`: The CBMC output parser will extract cover properties through their property class, and their result will be flipped. +- Kani library: The `cover` macro will be added there along with a `cover` function with a `rustc_diagnostic_item` +- `kani-compiler`: The `cover` function will be handled via a hook and codegen as two assertions (`cover(cond)` will be codegen as `__CPROVER_assert(false); __CPROVER_assert(!cond)`). +The purpose of the `__CPROVER_assert(false)` is to determine whether the `cover` statement is reachable. +If it is, the second `__CPROVER_assert(!cond)` indicates whether the condition is satisfiable or not. +- `kani-driver`: The CBMC output parser will extract cover properties through their property class, and their result will be set based on the result of the two assertions: + - The first (reachability) assertion is proven: report as `FAILURE (UNREACHABLE)` + - The first assertion fails, and the second one is proven: report as `FAILURE` to indicate that the condition is unsatisfiable + - The first assertion fails, and the second one fails: report as `SUCCESS` to indicate that the condition is satisfiable ## Rationale and alternatives +- What are the pros and cons of this design? +CBMC has its own [cover API (`__CPROVER_cover`)](https://diffblue.github.io/cbmc//cprover__builtin__headers_8h.html#a44f072b21e93cb0f72adcccc9005f307), for which `SUCCESS` is reported if an execution is found, and `FAILURE` is reported otherwise. +However, using this API currently requires running CBMC in a separate ["cover" mode](https://github.com/diffblue/cbmc/issues/6613). +Having to run CBMC in that mode would complicate the Kani driver as it will have to perform two CBMC runs, and then combine their results into a single report. +Thus, the advantage of the proposed design is that it keeps the Kani driver simple. +In addition, the proposed solution does not depend on a feature in the backend, and thus will continue to work if we were to integrate a different backend. + - What is the impact of not doing this? The current workaround to accomplish the same effect of verifying that a condition can be covered is to use `assert!(!cond)`. However, if the condition can indeed be covered, verification would fail due to the failure of the assertion. ## Open questions +Should we allow format arguments in the macro, e.g. `kani::cover!(x > y, "{} can be greater than {}", x, y)`? +Users may expect this to be supported since the macro looks similar to the `assert` macro, but Kani doesn't include the formatted string in the message description, since it's not available at compile time. + ## Other Considerations We need to make sure the concrete playback feature can be used with `cover` statements that were found to be coverable. ## Future possibilities -Users may want to specify a custom message for the cover property, in which case, we may consider adding a separate function that takes a static `str`, e.g. -```rust -fn cover_msg(cond: bool, msg: &'static str) -``` -or a `cover` macro (similar to Rust's `assert` macro). +The new cover API subsumes the current `kani::expect_fail` function. +Once it's implemented, we should be able to get rid of `expect_fail`, and all the related code in `compiletest` that handles the `EXPECTED FAILURE` message in a special manner. From 9b242e59516f618381c56ef1153c0def348eb883 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 2 Dec 2022 13:03:15 -0800 Subject: [PATCH 4/6] Make unsatisfiable cover properties not cause verification to fail --- rfc/src/rfcs/0003-cover-statement.md | 54 +++++++++++++++++++++++----- 1 file changed, 45 insertions(+), 9 deletions(-) diff --git a/rfc/src/rfcs/0003-cover-statement.md b/rfc/src/rfcs/0003-cover-statement.md index 23b398ba6093..5bebe4bdc90a 100644 --- a/rfc/src/rfcs/0003-cover-statement.md +++ b/rfc/src/rfcs/0003-cover-statement.md @@ -44,26 +44,62 @@ kani::cover!(x > y, "x can be greater than y"); ## User Experience -The `cover` macro instructs Kani to find _at least one_ possible execution that satisfies the specified condition at that line of code. If no such execution is possible, verification *fails*. +The `cover` macro instructs Kani to find _at least one_ possible execution that satisfies the specified condition at that line of code. If no such execution is possible, the check is reported as *unsatisfiable*. -Each cover statements will be reported as a check whose description is `condition "cond" is satisfiable` and whose status is: -- `SUCCESS` (green): if Kani found an execution that satisfies the condition -- `FAILURE` (red): if Kani proved that the condition cannot be satisfied -- `FAILURE (UNREACHABLE)` (red): if Kani proved that the cover statement itself cannot be reached +Each cover statements will be reported as a check whose description is `cover condition "cond"` and whose status is: +- `SATISFIED` (green): if Kani found an execution that satisfies the condition +- `UNSATISFIABLE` (yellow): if Kani proved that the condition cannot be satisfied +- `UNREACHABLE` (yellow): if Kani proved that the cover statement itself cannot be reached For example, for the following `cover` statement: ```rust kani::cover!(a == 0); ``` -The result can be: +An example result is: ``` Check 2: main.cover.2 - - Status: SUCCESS - - Description: "condition "a == 0" is satisfiable" + - Status: SATISFIED + - Description: "cover condition "a == 0"" - Location: foo.rs:9:5 in function main ``` -If one or more unwinding assertions fail or an unsupported construct is found to be reachable, and Kani proved that the condition cannot be satisfied, the result will be reported as `UNDETERMINED` instead of `FAILURE`. +### Impact on Overall Verification Status + +By default, unsatisfiable and unreachable `cover` checks will not impact verification success or failure. +This is to avoid getting verification failure for harnesses for which a `cover` check is not relevant. +For example, on the following program, verification should not fail for `another_harness_that_doesnt_call_foo` because the `cover` statement in `foo` is unreachable from it. +```rust +[kani::proof] +fn a_harness_that_calls_foo() { + foo(); +} + +#[kani::proof] +fn another_harness_that_doesnt_call_foo() { + // ... +} + +fn foo() { + kani::cover!( /* some condition */); +} +``` + +We can consider adding an option that would cause verification to fail if a cover property was unsatisfiable or unreachable, e.g. `--fail-uncoverable`. + +### Inclusion in the Verification Summary + +Cover checks will be reported separately in the verification summary, e.g. +``` +SUMMARY: + ** 1 of 206 failed (2 unreachable) + Failed Checks: assertion failed: x[0] == x[1] + + ** 30 of 35 cover statements satisfied (1 unreachable) <--- NEW + ``` +In this example, 5 of the 35 cover statements were found to be unsatisfiable, and one of those 5 is additionally unreachable. +### Interaction with Other Checks + +If one or more unwinding assertions fail or an unsupported construct is found to be reachable (which indicate an incomplete path exploration), and Kani found the condition to be unsatisfiable or unreachable, the result will be reported as `UNDETERMINED`. ## Detailed Design From 90cd8a9cb35a77530a5484fa8e3a54afb75a7ff2 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 9 Dec 2022 09:38:11 -0800 Subject: [PATCH 5/6] Address PR comments. - Allow `cover!()` without arguments - Move discussion on adding an option to fail verification to open questions --- rfc/src/rfcs/0003-cover-statement.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/rfc/src/rfcs/0003-cover-statement.md b/rfc/src/rfcs/0003-cover-statement.md index 5bebe4bdc90a..4686e4119ea7 100644 --- a/rfc/src/rfcs/0003-cover-statement.md +++ b/rfc/src/rfcs/0003-cover-statement.md @@ -27,13 +27,13 @@ kani::cover!(v.len() == 5); ``` This is typically used to ensure that verified checks are not passing _vacuously_, e.g. due to overconstrained pre-conditions. -The special case of verifying that a certain line of code is reachable can be achieved using `kani::cover!(true)`, e.g. +The special case of verifying that a certain line of code is reachable can be achieved using `kani::cover!()` (which is equivalent to `cover!(true)`), e.g. ```rust match x { val_1 => ..., val_2 => ..., ... - val_i => kani::cover!(true), // verify that `x` can take the value `val_i` + val_i => kani::cover!(), // verify that `x` can take the value `val_i` } ``` From 33b9f58745cf223f16cdd881e7d793e8c9915495 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Sat, 10 Dec 2022 14:26:29 -0800 Subject: [PATCH 6/6] Address PR comments --- rfc/src/rfcs/0003-cover-statement.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/rfc/src/rfcs/0003-cover-statement.md b/rfc/src/rfcs/0003-cover-statement.md index 4686e4119ea7..bbb7a8904e6e 100644 --- a/rfc/src/rfcs/0003-cover-statement.md +++ b/rfc/src/rfcs/0003-cover-statement.md @@ -46,10 +46,10 @@ kani::cover!(x > y, "x can be greater than y"); The `cover` macro instructs Kani to find _at least one_ possible execution that satisfies the specified condition at that line of code. If no such execution is possible, the check is reported as *unsatisfiable*. -Each cover statements will be reported as a check whose description is `cover condition "cond"` and whose status is: -- `SATISFIED` (green): if Kani found an execution that satisfies the condition -- `UNSATISFIABLE` (yellow): if Kani proved that the condition cannot be satisfied -- `UNREACHABLE` (yellow): if Kani proved that the cover statement itself cannot be reached +Each cover statement will be reported as a check whose description is `cover condition: cond` and whose status is: +- `SATISFIED` (green): if Kani found an execution that satisfies the condition. +- `UNSATISFIABLE` (yellow): if Kani proved that the condition cannot be satisfied. +- `UNREACHABLE` (yellow): if Kani proved that the cover statement itself cannot be reached. For example, for the following `cover` statement: ```rust @@ -59,7 +59,7 @@ An example result is: ``` Check 2: main.cover.2 - Status: SATISFIED - - Description: "cover condition "a == 0"" + - Description: "cover condition: a == 0" - Location: foo.rs:9:5 in function main ```