Skip to content

Commit bf603f0

Browse files
adpaco-awsadpaco-aws
authored
RFC: Global Conditions (rust-lang#2516)
1 parent fda2b42 commit bf603f0

File tree

1 file changed

+111
-0
lines changed

1 file changed

+111
-0
lines changed

‎rfc/src/rfcs/0007-global-conditions.md

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
- **Feature Name:** Global Conditions (`global-conditions`)
2+
- **Feature Request Issue:** <https://github.com/model-checking/kani/issues/2525>
3+
- **RFC PR:** <https://github.com/model-checking/kani/pull/2516>
4+
- **Status:** *Unstable*
5+
- **Version:** 0
6+
- **Proof-of-concept:** <https://github.com/model-checking/kani/pull/2532>
7+
8+
-------------------
9+
10+
## Summary
11+
12+
A new section in Kani's output to summarize the status of properties that depend on other properties. We use the term *global conditions* to refer to such properties.
13+
14+
## User Impact
15+
16+
The addition of new options that affect the overall verification result depending on certain property attributes demands some consideration.
17+
In particular, the addition of a new option to fail verification if there are uncoverable (i.e., unsatisfiable or unreachable) `cover` properties (requested in [#2299](https://github.com/model-checking/kani/issues/2299)) is posing new challenges to our current architecture and UI.
18+
19+
This concept isn't made explicit in Kani, but exists in some ways.
20+
For example, the `kani::should_panic` attribute is a global condition because it can be described in terms of other properties (checks).
21+
The request in [#2299](https://github.com/model-checking/kani/issues/2299) is essentially another global conditions, and we may expect more to be requested in the future.
22+
23+
In this RFC, we propose a new section in Kani's output focused on reporting global conditions.
24+
The goal is for users to receive useful information about hyperproperties without it becoming overwhelming.
25+
This will help users to understand better options that are enabled through global conditions and ease the addition of such options to Kani.
26+
27+
## User Experience
28+
29+
**The output will refer to properties that depend on other properties as "global conditions"**, which is a simpler term.
30+
The options to enable different global conditions will depend on a case-by-case basis[^enable-options].
31+
32+
The main UI change in this proposal is a new `GLOBAL CONDITIONS` section that **won't be printed if no global conditions have been enabled**.
33+
This section will only appear in Kani's default output after the `RESULTS` section (used for individual checks) and have the format:
34+
35+
```
36+
GLOBAL CONDITIONS:
37+
- `<name>`: <status> (<reason>)
38+
- `<name>`: <status> (<reason>)
39+
[...]
40+
```
41+
42+
where:
43+
- `<name>` is the name given to the global condition.
44+
- `<status>` is the status determined for the global condition.
45+
- `<reason>` is an explanation that depends on the status of the global condition.
46+
47+
For example, let's assume we implement the option requested in [#2299](https://github.com/model-checking/kani/issues/2299).
48+
A concrete example of this output would be:
49+
50+
```
51+
GLOBAL CONDITIONS:
52+
- `fail_uncoverable`: SUCCESS (all cover statements were satisfied as expected)
53+
```
54+
55+
A `FAILED` status in any enabled global condition will cause verification to fail.
56+
In that case, the overall verification result will point out that one or more global conditions failed, as in:
57+
58+
```
59+
VERIFICATION:- FAILURE (one or more global conditions failed)
60+
```
61+
62+
This last UI change will also be implemented for the terse output.
63+
Finally, checks that cause an enabled global condition to fail will be reported using the same interface we use for failed checks[^failed-checks].
64+
65+
**Global conditions which aren't enabled won't appear in the `GLOBAL CONDITIONS` section**.
66+
Their status will be computed regardless[^status-computation], and we may consider showing this status when the `--verbose` option is passed.
67+
68+
The documentation of global conditions will depend on how they're enabled, which depends on a case-by-case basis.
69+
However, we may consider adding a new subsection `Global conditions` to the `Reference` section that collects all of them so it's easier for users to consult all of them in one place.
70+
71+
## Detailed Design
72+
73+
The only component to be modified is `kani-driver` since that's where verification results are built and determined.
74+
But we should consider moving this logic into another crate.
75+
76+
We don't need new dependencies.
77+
The corner cases will depend on the specific global conditions to be implemented.
78+
79+
## Rationale and alternatives
80+
81+
As mentioned earlier, we're proposing this change to help users understand global conditions and how they're determined.
82+
In many cases, global conditions empower users to write harnesses which weren't possible to write before.
83+
As an example, the `#[kani::should_panic]` attribute allowed users to write harnesses expecting panic-related failures.
84+
85+
Also, we don't really know if more global conditions will be requested in the future.
86+
We may consider discarding this proposal and waiting for the next feature that can be implemented as a global condition to be requested.
87+
88+
### Alternative: Global conditions as regular checks
89+
90+
One option we've considered in the past is to enable global conditions as a regular checks.
91+
While it's technically doable, it doesn't feel appropriate for global conditions to reported through regular checks since generally a higher degree of visibility may be appreciated.
92+
93+
## Open questions
94+
95+
No open questions.
96+
97+
## Future possibilities
98+
99+
A redesign of Kani's output is likely to change the style/architecture to report global conditions.
100+
101+
[^status-computation]: The results for global conditions would be computed during postprocessing based on the results of other checks.
102+
Global conditions' checks aren't part of the SAT, therefore this computation won't impact verification time.
103+
104+
[^failed-checks]: We do not discuss the specific interface to report the failed checks because it needs improvements (for both global conditions and standard verification).
105+
In particular, the description field is the only information printed for properties (such as `cover` statements) without trace locations.
106+
There are additional improvements we should consider: printing the actual status (for global conditions, this won't always be `FAILED`), avoid the repetition of `Failed Checks: `, etc.
107+
[This comment](https://github.com/model-checking/kani/pull/2516#issuecomment-1597524184) discusses problems with the current interface on some examples.
108+
109+
[^enable-options]: In other words, global conditions won't force a specific mechanism to be enabled.
110+
For example, if the `#[kani::should_panic]` attribute is converted into a global condition, it will continue to be enabled through the attribute itself.
111+
Other global conditions may be enabled through CLI flags only (e.g., `--fail-uncoverable`), or a combination of options in general.

0 commit comments

Comments
 (0)