RFC: Global Conditions

[adpaco-aws]

Description of changes:

This RFC proposes a new section in Kani's output to summarize the status of properties that depend on other properties, referred to as "Global Conditions". Originally, I wanted this change to be part of #2299, but then I realized a small RFC might be appropriate.

Resolved issues:

N/A

Testing:

• How is this change tested? N/A

• Is this a refactor change? N/A

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]

It makes sense.

[zhassan-aws]

Link to rendered version: https://github.com/adpaco-aws/rmc/blob/update-other-rfcs/rfc/src/rfcs/0007-global-conditions.md

[zhassan-aws]

I cannot think of other "Global Conditions" that may be introduced in the future. Do you have any in mind? If not, I think for the case of fail_uncoverable, it would be obvious why verification fails when the unsatisfiable cover properties are included in the "Failed Checks" section. In which case, a new section may not be needed.

[karkhaz]

It seems to me that there are two commonalities in @adpaco-aws's examples of should_panic and fail_uncoverable:

• Their statuses are derived entirely from the status of other properties, and not directly a result from the SAT solver
• They are of the form "{panic,coverage} did not happen along any path" rather than "{overflow} happened along some path".

Would you expect these to be true for other global conditions that might be added in the future? I think the first bullet point is how you're defining hyperproperty/global condition, but I think the second bullet point is more relevant to users and might be a good reason to separate hyperproperties out from regular ones.

[adpaco-aws]

I cannot think of other "Global Conditions" that may be introduced in the future. Do you have any in mind?

Yes, the check for expectations on individual properties mentioned here could be implemented as a global condition. Another global condition that I think could be interesting for users would check that specific properties (e.g., user-defined assertions) are not unreachable. This can already be manually done by adding cover statements, but that isn't always an option (because the user may not want to add them) and users may not realize they are unreachable if they appear in deep places in the call graph.

But one of the cool things about global conditions is that we could also define them for existing properties. For example, we could have a memory safety condition that summarizes the status memory-safety checks (and hide them from RESULTS if all went well). Or do the same for unwinding assertions, as @celinval mentioned. If we did that, this section could become the main component of Kani's output.

[celinval]

I cannot think of other "Global Conditions" that may be introduced in the future. Do you have any in mind?

Yes, the check for expectations on individual properties mentioned here could be implemented as a global condition. Another global condition that I think could be interesting for users would check that specific properties (e.g., user-defined assertions) are not unreachable. This can already be manually done by adding cover statements, but that isn't always an option (because the user may not want to add them) and users may not realize they are unreachable if they appear in deep places in the call graph.

But one of the cool things about global conditions is that we could also define them for existing properties. For example, we could have a memory safety condition that summarizes the status memory-safety checks (and hide them from RESULTS if all went well). Or do the same for unwinding assertions, as @celinval mentioned. If we did that, this section could become the main component of Kani's output.

Please do replace the memory safety and arithmetic checks by global conditions! :) It would result in a much cleaner output.

One thing I'm missing in this RFC is an explanation on how the user could easily find the root cause of the failing global condition. For example, for the fail_uncovered, do we expect users to go inspect all the covers or can we print the uncovered ones the same way we print failed checks at the end?

[adpaco-aws]

They are of the form "{panic,coverage} did not happen along any path" rather than "{overflow} happened along some path".

Actually, the should_panic condition expresses "there exists at least one path with an assertion-related failure". I'm defining global conditions as in the first item because that's what I'm trying to generalize here, and I'd expect new ones to follow this rule but I can't guarantee it. But that's OK, we can always go back to this RFC and update it 😄

[adpaco-aws]

One thing I'm missing in this RFC is an explanation on how the user could easily find the root cause of the failing global condition. For example, for the fail_uncovered, do we expect users to go inspect all the covers or can we print the uncovered ones the same way we print failed checks at the end?

That's a great point, but I'm concerned about the output getting longer and less comprehensible if we include that change in this RFC. My preference here would be to keep it simple for now, but I'm happy to talk about it.

[celinval]

One thing I'm missing in this RFC is an explanation on how the user could easily find the root cause of the failing global condition. For example, for the fail_uncovered, do we expect users to go inspect all the covers or can we print the uncovered ones the same way we print failed checks at the end?

That's a great point, but I'm concerned about the output getting longer and less comprehensible if we include that change in this RFC. My preference here would be to keep it simple for now, but I'm happy to talk about it.

I agree that our output is pretty long and it needs refactoring ASAP.

However, I think that printing the uncovered statements at the end will alleviate the problem of our super verbose output. At least the information that the user really needs is readily available at the end of the report, just like failed properties.

[adpaco-aws]

However, I think that printing the uncovered statements at the end will alleviate the problem of our super verbose output. At least the information that the user really needs is readily available at the end of the report, just like failed properties.

Makes sense. I've been extending the current implementation (in #2532) to use the function that reports failed checks for standard verification jobs, but it needs improvements. For example, for a simple harness which contains an unreachable cover statement we get this information:

RESULTS:
Check 1: harness_uncoverable.cover.1
         - Status: UNREACHABLE
         - Description: "cover location"
         - Location: tests/ui/fail-uncoverable/uncoverable/test.rs:13:9 in function harness_uncoverable

GLOBAL CONDITIONS:
 - fail_uncoverable: FAILURE (encountered one or more cover statements which were not satisfied)
Failed Checks: cover location

SUMMARY:
 ** 0 of 0 failed

 ** 0 of 1 cover properties satisfied (1 unreachable)


VERIFICATION:- FAILED (one or more global conditions failed)
Verification Time: 0.02321334s

Note that it only says "Failed Checks: cover location", but it doesn't attach a location despite showing it for the property because the trace doesn't refer to this location, causing us to return earlier. We should make some changes here, also because the "Failed Checks: " gets printed for each item (the results below are for tests/ui/should-panic-attribute/unexpected-failures/test.rs) which is causing the output to be cluttered and a little confusing:

SUMMARY:
 ** 3 of 18 failed
Failed Checks: panicked on the `1` arm!
 File: "/home/ubuntu/kani/tests/ui/should-panic-attribute/unexpected-failures/test.rs", line 18, in check
Failed Checks: panicked on the `0` arm!
 File: "/home/ubuntu/kani/tests/ui/should-panic-attribute/unexpected-failures/test.rs", line 17, in check
Failed Checks: shift distance too large

In any case, I agree with your point - I'll change the RFC with a new proposal to report these failed checks.

[celinval]

Since this is an RFC, please wait for a second approval before merging.

[karkhaz]

Awesome. Thanks for working on this!!

[jaisnan]

Thanks :) !

[remi-delmas-3000]

would "dependent conditions" be a better name than "global conditions" ?

[remi-delmas-3000]

So are global conditions solely defined as conjunctions of assert/cover statement or are there other ways of defining them ?

[adpaco-aws]

Not sure about the name.

Global conditions do not need to depend on assert/cover statements, and there should be other ways to define them. For example, one possibility we've discussed in the past is to have a memory-safety condition based on the result of all memory safety checks we currently produce.

[remi-delmas-3000]

What are the problems being addressed ?

[adpaco-aws]

I'm not sure if you're asking about the problems being addressed in Kani (to enable global conditions) or the problems being addressed with the feature requested in #2299 .

If it's the former, then the problem is that Kani isn't flexible enough. Until the #[kani::should_panic] attribute was introduced, there was only one way to get a successful verification: making all checks pass (i.e., getting a SUCCESS status in each of the individual checks/properties). But users may want to verify other things, or define additional conditions for verification like we're doing here.

If it's the latter, then the problem is vacuity. We check the status for cover properties, but their status doesn't impact verification in any way. Some users want to additionally ensure that the predicates in cover are always satisfied - the option requested in #2299 is for them.

[remi-delmas-3000]

Is it possible to list the basic conditions that failed to explain why a global condition failed ?

[adpaco-aws]

Yes, it should be possible.

[remi-delmas-3000]

is "hyperproperties" meant as in "a property that relates two or more executions of the same program?"

[remi-delmas-3000]

Are global conditions only enabled using special flags or can the user also define his own groups of dependent conditions ?

[adpaco-aws]

Please note that those are two separate questions:

1. Are global conditions only enabled using special flags?: No. Some may be enabled using special flags. Others may be enabled using attributes. Others may use a combination. We don't put constrains on this at the moment.
2. Can the user also define his own groups of dependent conditions?: No, the RFC doesn't contemplate this option at the moment. That would require a language to define conditions.

[remi-delmas-3000]

the documentation of should_panic does not really give a precise meaning to the check, i.e. it does not say if at least one execution must trigger a panic or if all executions must trigger a panic. How can it be modelled in terms of dependent conditions and statuses ?

[adpaco-aws]

I don't think we do that for any of the checks we currently produce. Regardless, I think it's well defined in here, and if you think otherwise I'm happy to do any editions you consider appropriate.

[remi-delmas-3000]

What is a regular check ? kani::assert ? kani::cover ?

[adpaco-aws]

Check is the simpler term we use to refer to properties. Running Kani on any will output something like this:

RESULTS:
Check 1: example.assertion.1
         - Status: <status>
         - Description: <description>
         - Location: <location>
[...]

So this refers to those checks/properties.

[remi-delmas-3000]

is it possible to give a more explicit and rigorous definition of global conditions ?

e.g. "a global condition is specified by a set of assert or cover statements and an aggregation function that computes a status for the global conditions from the statuses of the basic conditions."

[adpaco-aws]

Maybe? But it's definitely not that.

I'm actually thinking about growing the scope of global conditions to consider things other than other properties. For example, a timeout feature could be implemented a global condition. However, the current definition of global condition does not consider resources like memory or time, only verification properties.

[remi-delmas-3000]

so the status of a global condition could differ when the switch --fail-uncoverable is activated vs not activated ?

[adpaco-aws]

No. The status computed for the condition itself won't differ. But activating the switch will simply cause the status of the global condition to affect the overall verification result.