RFC for cover ctatement #1906

zhassan-aws · 2022-11-15T23:53:44Z

Description of changes:

An RFC for adding a new cover API to Kani.

A rendered version can be found here.

Resolved issues:

Resolves #1905

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

Testing:

How is this change tested?
Is this a refactor change?

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

celinval

Awesome! I have 2 questions about UX:

What will be the Description: of a cover statement?
What about the summary message?

celinval · 2022-11-16T00:03:21Z

rfc/src/rfcs/0003-cover-statement.md

+
+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:


What about UNDETERMINED?

Added a sentence to clarify.

celinval · 2022-11-16T00:04:20Z

rfc/src/rfcs/0003-cover-statement.md

+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


What about COVERED and UNREACHABLE?

That was my original plan, but rethinking about it, it makes sense to consider an unsatisfiable cover a verification failure, in which case SUCCESS and FAILURE would fit well with the current summary, i.e. the summary line would include the failure in the ** 1 of 15 failed line.

If we were to add separate results, e.g. SATISFIABLE/UNSATISFIABLE or COVERED/UNCOVERABLE, the summary would be

** 0 of 15 failed (1 unsatisfiable) VERIFICATION:- FAILED

which might be less clear.

I think SUCCESS and FAILURE are rather confusing today, so I was hoping to avoid that for covers. I'm OK with leaving as is for now though. @tedinski are you thinking about improving these statuses as part of #1690?

celinval · 2022-11-16T00:06:13Z

rfc/src/rfcs/0003-cover-statement.md

+
+## Other Considerations
+
+We need to make sure the concrete playback feature can be used with `cover` statements that were found to be coverable.


Not for this RFC, but food for thought: How could we help users debug cases where a cover statement is not coverable? I suppose this would be similar to helping users understand why a program is in fact safe (i.e., why no bad state is reachable).

celinval · 2022-11-16T00:07:19Z

rfc/src/rfcs/0003-cover-statement.md

+
+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)


Would it make sense to add a message now?

I debated this a bit. If we make the message a required part of the basic cover API, then the user may end up doing lots of kani::cover(c, "") or kani::cover(c, None), so it seems desirable to not make the message a mandatory argument. The alternatives are:

Add a separate function that takes a custom message.

Make cover a macro instead of a function, similar to the assert macro.

Thoughts?

I like the idea of adding the function and the macro. The function takes a str and the macro generates one using the user expression if no message was provided.

…le unsupported constructs

tedinski · 2022-11-16T17:49:05Z

rfc/src/rfcs/0003-cover-statement.md

+
+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 satisfies the condition
+- `FAILURE` (red): if Kani proved that the condition cannot be satisfied


IMO we need better results here. There's three cases:

Success: reachable, satisfiable

Failure: reachable, not satisfiable

Failure: unreachable

I think it's very important for debugging to distinguish these.

That's a good point! This would require that we generate a "cover current location" check for every cover property the user writes. I'll add that.

While I agree it's an important detail for debugging, I think this would complicate our verification output by adding another "status". Perhaps it would be simpler to just generate two checks for each cover statement, one for satisfiability and another one for reachability.

tedinski · 2022-11-16T17:51:00Z

rfc/src/rfcs/0003-cover-statement.md

+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


Please comment on the ability to deprecate the current expect_fail. I think we could deprecate and replace this with cover, right?

Good point. I'll add that.

camshaft · 2022-11-17T04:05:35Z

How does this all work with with linker slicing and multiple harnesses? Say for example I have the following code

fn my_function() {
    kani::cover!(true):
}

#[kani::proof]
fn proof_a() {
    // Calls my function 
    my_function();
}

#[kani::proof]
fn proof_b() {
    // Doesn't call my function - the cover isn't reachable from this proof. 
    // Should it fail?
}

For proof_b I imagine it's possible to want two different answers to if it should fail or not, depending on what you're trying to accomplish.

On the one hand, if I know proof_b will never call my_function, then I definitely don't want it to fail because they're unrelated. If it failed that would mean that I need to include every single cover statement in every single proof in the codebase.

On the other hand, what if I want to make sure that my_function is always reachable by proof_b? Let's say my_function is some critical code that must be called at some point in relation to another function. proof_b would pass and the only way I would know it's proving what I think it's proving is doing an audit of the properties output. And even if you see it at the time of writing the proof, there could be a change in the future where it's no longer reachable but the proof still passes.

zhassan-aws · 2022-11-17T06:39:27Z

Good questions @camshaft!

I would expect cover properties to be primarily used within proof harnesses since cover is only interpreted by Kani. But in the example you gave, the cover property won't fail for proof_b because slicing (more specifically CBMC's --drop-unused-functions) is applied to each harness separately, so the cover property won't be checked for proof_b.

But if a function is not "obviously" unused, e.g.:

fn my_function() {
    kani::cover!(true):
}

fn foo(x: bool) {
    if x {
        my_function();
    }
}

#[kani::proof]
fn proof_a() {
    my_function(true);
}

#[kani::proof]
fn proof_b() {
    my_function(false);
}

The cover property will fail for proof_b.

aaronbembenek-aws · 2022-11-17T14:23:53Z

Good questions @camshaft!

I would expect cover properties to be primarily used within proof harnesses since cover is only interpreted by Kani. But in the example you gave, the cover property won't fail for proof_b because slicing (more specifically CBMC's --drop-unused-functions) is applied to each harness separately, so the cover property won't be checked for proof_b.

But if a function is not "obviously" unused, e.g.:
fn my_function() {
    kani::cover!(true):
}

fn foo(x: bool) {
    if x {
        my_function();
    }
}

#[kani::proof]
fn proof_a() {
    my_function(true);
}

#[kani::proof]
fn proof_b() {
    my_function(false);
}
The cover property will fail for proof_b.

Hm, this is sort of tricky. For example, what if CBMC changed the way it does program slicing? That could change whether a proof harness passes or fails, right? If so, that behavior strikes me as surprising.

Maybe we could restrict kani::cover to be only in harnesses. Or alternatively we could add another argument to kani::cover identifying the harnesses it is applicable to, and make sure that CBMC considers the relevant code to be reachable when handling those harnesses.

camshaft · 2022-11-17T17:30:50Z

Yes this is a bit tricky. These cover! statements should ideally be properties of a particular proof, not the general code base. And I think that's OK as long as we document this aspect.

As a side note, this got me thinking about how to reason about coverage of a program in relation to its inputs. I wrote up a quick sketch of what it could look like: https://gist.github.com/camshaft/9cc5e93c1bfdf96ec7dddfd1264a8b5d

celinval · 2022-11-17T18:33:57Z

I don't know if we should limit cover statements to only be used inside a harness although I do agree that the current behavior would be rather cryptic. Ideally, we should report all properties that were dropped by CBMC as unreachable, and that should be the case for assertions and cover statements.

This discussion made me wonder if we should really fail the verification because a cover statement.

adpaco-aws · 2022-11-18T21:41:26Z

rfc/src/rfcs/0003-cover-statement.md

+
+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 macro, `cover` will be created that can be used for checking that a certain condition _can_ occur at a specific location in the code.


Something that isn't clear to me after reading this section is how cover is different from assert. If my understanding is correct, assert checks a condition, while cover checks a condition AND ensures that the statement itself is reachable.

If we agree on that, then the "can" in this sentence should be "will" instead.

I think conceptually they are similar. assert says this condition must hold for all executions. cover says this condition must hold for at least one execution.

adpaco-aws · 2022-11-18T21:45:30Z

rfc/src/rfcs/0003-cover-statement.md

+
+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 satisfies the condition
+- `FAILURE` (red): if Kani proved that the condition cannot be satisfied


While I agree it's an important detail for debugging, I think this would complicate our verification output by adding another "status". Perhaps it would be simpler to just generate two checks for each cover statement, one for satisfiability and another one for reachability.

zhassan-aws · 2022-11-18T21:48:33Z

Good discussion. How about we make an unsatisfiable cover property non-failing by default, but add an option, e.g. --fail-uncoverable that makes it a failure?

zhassan-aws · 2022-12-02T21:05:39Z

Good discussion. How about we make an unsatisfiable cover property non-failing by default, but add an option, e.g. --fail-uncoverable that makes it a failure?

Updated RFC to reflect this discussion.

celinval · 2022-12-09T06:28:48Z

rfc/src/rfcs/0003-cover-statement.md

+```
+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.


Since this is a macro, could we just allow users to do kani::cover!()?

Good idea! I'll update the RFC.

celinval · 2022-12-09T06:32:32Z

rfc/src/rfcs/0003-cover-statement.md

+
+### Impact on Overall Verification Status
+
+By default, unsatisfiable and unreachable `cover` checks will not impact verification success or failure.


Impact overall verification results

What I meant is that they won't cause an otherwise successful verification run to fail (i.e. if all normal checks are passing). Should I clarify the sentence a bit, or did you mean something else?

I think it's OK

celinval · 2022-12-09T06:33:35Z

rfc/src/rfcs/0003-cover-statement.md

+}
+```
+
+We can consider adding an option that would cause verification to fail if a cover property was unsatisfiable or unreachable, e.g. `--fail-uncoverable`.


Is this part of the RFC or open questions?

I'll move it to the open questions.

- Allow `cover!()` without arguments - Move discussion on adding an option to fail verification to open questions

celinval

I'm OK with the initial proposal. I think we can tune it as we try it out. Please don't forget to get a second approval.

Thanks!

adpaco-aws

My main concern with the current proposal is the fact that unsatisfiable/unreachable cover statements don't affect overall verification results, leading to surprises later. An alternative is to switch the proposal so the option becomes --allow-uncoverable instead (think of it as a sign-off from the user).

However, there's no way to know if that's what we want at the moment, let's get an initial version out and see where it goes from here.

adpaco-aws · 2022-12-09T19:31:49Z

rfc/src/rfcs/0003-cover-statement.md

+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


Just a few suggestions in this paragraph:

"statements" (1st occurrence) -> "statement"

Dots at the end of each sentence.

Maybe use cover condition `<cond>` ?

Fixed the first two.

For the third, I changed it to:

cover condition: cond

to mimic the assert message:

assertion failed: 1 + 1 == 3

I hope this is OK.

adpaco-aws · 2022-12-09T19:33:30Z

rfc/src/rfcs/0003-cover-statement.md

+Check 2: main.cover.2
+         - Status: SATISFIED
+         - Description: "cover condition "a == 0""
+         - Location: foo.rs:9:5 in function main


Point 3 in my previous comment (use cover condition `<cond>` ) also applies here, because otherwise you end up with "" at the end.

zhassan-aws requested a review from a team as a code owner November 15, 2022 23:53

RFC for cover ctatement

cecc910

zhassan-aws force-pushed the rfc-cover branch from 122800f to cecc910 Compare November 15, 2022 23:54

celinval reviewed Nov 16, 2022

View reviewed changes

AClarify the interaction with failed unwinding assertions and reachab…

bb26594

…le unsupported constructs

tedinski reviewed Nov 16, 2022

View reviewed changes

zhassan-aws added 2 commits November 16, 2022 12:24

Merge branch 'main' into rfc-cover

c05722e

Address PR comments

21bbc24

adpaco-aws reviewed Nov 18, 2022

View reviewed changes

zhassan-aws added the T-RFC Label RFC PRs and Issues label Nov 19, 2022

zhassan-aws added 2 commits December 2, 2022 12:11

Merge branch 'main' into rfc-cover

a38f2ab

Make unsatisfiable cover properties not cause verification to fail

9b242e5

celinval reviewed Dec 9, 2022

View reviewed changes

zhassan-aws added 2 commits December 9, 2022 09:37

Merge branch 'main' into rfc-cover

e6c4ccb

Address PR comments.

90cd8a9

- Allow `cover!()` without arguments - Move discussion on adding an option to fail verification to open questions

celinval approved these changes Dec 9, 2022

View reviewed changes

adpaco-aws approved these changes Dec 9, 2022

View reviewed changes

zhassan-aws added 2 commits December 10, 2022 14:26

Address PR comments

33b9f58

Merge branch 'main' into rfc-cover

660e9b1

zhassan-aws merged commit 94b4e84 into model-checking:main Dec 10, 2022

zhassan-aws deleted the rfc-cover branch December 10, 2022 23:37

zhassan-aws mentioned this pull request Dec 16, 2022

Introduce a kani macro for checking coverage #2011

Merged

4 tasks

zhassan-aws mentioned this pull request Jan 4, 2023

Add documentation for cover properties #2057

Merged

4 tasks

carolynzech mentioned this pull request Aug 7, 2024

cover_or_fail! macro #3424

Closed


		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:


		## Other Considerations

		We need to make sure the concrete playback feature can be used with `cover` statements that were found to be coverable.


		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 macro, `cover` will be created that can be used for checking that a certain condition _can_ occur at a specific location in the code.


		### Impact on Overall Verification Status

		By default, unsatisfiable and unreachable `cover` checks will not impact verification success or failure.

RFC for cover ctatement #1906

RFC for cover ctatement #1906

Conversation

zhassan-aws commented Nov 15, 2022 • edited Loading

Description of changes:

Resolved issues:

Related RFC:

Call-outs:

Testing:

Checklist

celinval left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

camshaft commented Nov 17, 2022

zhassan-aws commented Nov 17, 2022

aaronbembenek-aws commented Nov 17, 2022

camshaft commented Nov 17, 2022

celinval commented Nov 17, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zhassan-aws commented Nov 18, 2022

zhassan-aws commented Dec 2, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval left a comment

Choose a reason for hiding this comment

adpaco-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

zhassan-aws commented Nov 15, 2022 •

edited

Loading