RFC for Rust UB checks #3092
RFC for Rust UB checks #3092
Conversation
rfc/src/rfcs/0010-rust-ub-checks.md
Outdated
|
|
||
| A counter example that triggers UB may require extra tooling for debugging, e.g.: MIRI or valgrind. | ||
| We propose that tests added by concrete playback in those cases should include a comment stating such limitation. | ||
| Other possibilities are discussed in [0010-rust-ub-checks.md#open-questions]. |
There was a problem hiding this comment.
Thanks, @celinval ! I'm all down for a more consistent and intuitive experience like the one proposed in this RFC.
However, I'd have liked to see some content regarding categorization of UB checks. At the same time, I acknowledge that this subject deserves its own RFC, so I'd be satisfied if this RFC included a forward declaration about a future categorization effort that tries to be as exhaustive as possible (think of it as a more detailed version of this reference section).
In the previous PR model-checking#3085, we did not support checks for `write_bytes` which is added in this PR. I am waiting for model-checking#3092 to add expected tests.
Conflicts:
- rfc/src/SUMMARY.md
- Changed the example. - Improved text. - Removed restriction on unstable opt-out.
celinval
force-pushed
the
issue-2998-ub-rfc
branch
from
4f6c75f to
96f50da
Compare
|
|
||
| ## User Experience | ||
|
|
||
| A UB check should behave consistently independent on how and where it is implemented. |
There was a problem hiding this comment.
| A UB check should behave consistently independent on how and where it is implemented. | |
| A UB check should behave consistently independent of how and where it is implemented. |
| For simplicity, we propose that all undefined behavior checks are modelled as assert-assume pairs. | ||
| We propose that the status of all passing assertions that may be affected by this check to be displayed as | ||
| `UNDETERMINED` if one or more UB checks fail. | ||
| For simplicity, Kani currently over-approximate this set by marking all passing assertions as `UNDETERMINED`. |
There was a problem hiding this comment.
| For simplicity, Kani currently over-approximate this set by marking all passing assertions as `UNDETERMINED`. | |
| For simplicity, Kani currently over-approximates this set by marking all passing assertions as `UNDETERMINED`. |
| assignment to its tracker that violates the assertion. | ||
| Picking an assignment that fails can be seen as choosing the worst possible action, known as demonic nondeterminism. | ||
|
|
||
| See [Open questions section](0010-rust-ub-checks.md#open-questions) for alternatives to be considered. |
There was a problem hiding this comment.
| See [Open questions section](0010-rust-ub-checks.md#open-questions) for alternatives to be considered. | |
| See the [Open questions section](0014-rust-ub-checks.md#open-questions) for alternatives to be considered. |
|
|
||
| A counter example that triggers UB may require extra tooling for debugging, e.g.: MIRI or valgrind. | ||
| We propose that tests added by concrete playback in those cases should include a comment stating such limitation. | ||
| Other possibilities are discussed in [0010-rust-ub-checks.md#open-questions]. |
There was a problem hiding this comment.
| Other possibilities are discussed in [0010-rust-ub-checks.md#open-questions]. | |
| Other possibilities are discussed in [0014-rust-ub-checks.md#open-questions]. |
| For option 2, Kani may fail verification even if the code does not have UB. | ||
| In those cases, Kani check must be explicit about this failure being an over-approximation. | ||
| For that, we propose that the check message is clear about this limitation, and potentially its status | ||
| (see [0010-rust-ub-checks.md#open-questions]). |
There was a problem hiding this comment.
| (see [0010-rust-ub-checks.md#open-questions]). | |
| (see [0014-rust-ub-checks.md#open-questions]). |
|
|
||
| ```rust | ||
| #[kani::proof] | ||
| #[kani::ignore(CHECK_NAMES)] |
There was a problem hiding this comment.
"ignore" is a bit too general. Maybe use ignore_ub?
|
|
||
| ## Rationale and alternatives | ||
|
|
||
| Kani already has undefined behavior checks, some are implemented on the CBMC side, such as access out bounds, and |
There was a problem hiding this comment.
| Kani already has undefined behavior checks, some are implemented on the CBMC side, such as access out bounds, and | |
| Kani already has undefined behavior checks, some are implemented on the CBMC side, such as out-of-bounds access, and |
| ``` | ||
|
|
||
| We would like to keep taking advantage of existing instrumentation to maximize the UB check coverage. | ||
| The mechanism used to build the check, however, shouldn't influence in the user experience. |
There was a problem hiding this comment.
| The mechanism used to build the check, however, shouldn't influence in the user experience. | |
| The mechanism used to build the check, however, shouldn't influence the user experience. |
There was a problem hiding this comment.
This section does a great job of explaining the current division of UB checks and how those manifest in different experiences for users, but I'm missing a call to action--what are you proposing we do about it? Should we add a model of get_unchecked to Kani so that we can catch this error ourselves and provide a better error message? Or not, because then we're not relying on existing instrumentation? We don't need to land on a precise answer now (I know the implementation section is empty), but can we give some options at least?
Also, I'm a bit confused about the scope of this RFC. The User Experience section made me think that we were just talking about whether a passing check should pass or be undetermined based on a failing UB check before it. Now it seems like we're also considering the UX of the UB checks themselves. I would recommend adding a sentence or two about consistent messaging for failing UB checks to the User Experience section if you intend for that to be part of the "consistent framework" you're proposing.
| - Another possibility would be to add a `unreachable!()` statement at the end of the test case with a message | ||
| explaining why the statement should be unreachable. | ||
| - Should we deprecate the `--no-default-checks` and all `--[CHECK-NAME]-checks` checks. | ||
| - Should we add an attribute that allows us to opt-out some UB checks for a function or some code block? |
There was a problem hiding this comment.
| - Should we add an attribute that allows us to opt-out some UB checks for a function or some code block? | |
| - Should we add an attribute that allows us to opt-out of some UB checks for a function or some code block? |
|
Please take a look at the modifications suggested in the previous round of review as well. |
There was a problem hiding this comment.
Thanks! High-level comment: I think the RFC would benefit from a longer summary that outlines the key elements of what defines a "consistent framework." Bullet points are fine--something like:
- Consistent standards for the status of assertions downstream of a failing UB check
- Consistent error message style for failing UB checks, regardless of whether the UB was detected in Kani, CBMC, or the Rust standard library
- Consistent mechanisms by which a user can opt in or out of a given UB check
Laying this out in the beginning would give the reader a better idea of what they can expect from reading the rest of the RFC.
| The detection of an undefined behavior should impact the status of any assertion that may be reachable from the | ||
| detected undefined behavior. | ||
|
|
||
| For simplicity, we propose that all undefined behavior checks are modelled as assert-assume pairs. |
There was a problem hiding this comment.
Does this comment affect the validity of this approach at all?
(More generally, the PR description mentions that those two CBMC issues will affect the RFC. Since those issues are now closed/merged, could you update the PR description to instead explain how they affect the approach outlined here, if at all?)
There was a problem hiding this comment.
Ok, after finishing the RFC, I believe the demonic nondeterminism mention later addresses the soundness concerns from the linked comment.
| We propose that the status of all passing assertions that may be affected by this check to be displayed as | ||
| `UNDETERMINED` if one or more UB checks fail. | ||
| For simplicity, Kani currently over-approximate this set by marking all passing assertions as `UNDETERMINED`. |
There was a problem hiding this comment.
| We propose that the status of all passing assertions that may be affected by this check to be displayed as | |
| `UNDETERMINED` if one or more UB checks fail. | |
| For simplicity, Kani currently over-approximate this set by marking all passing assertions as `UNDETERMINED`. | |
| Currently, if a UB check fails, Kani overapproximates and marks all passing assertions as `UNDETERMINED`. | |
| We propose refining this overapproximation to only mark a passing assertion as `UNDETERMINED` if it is reachable from the failing UB check. | |
There was a problem hiding this comment.
I suppose after looking at this comment, maybe "reachable" isn't the right word here--you said "downstream," and I take the difference to be that "downstream" just means "after" whereas "reachable" is "after, and also reachable." So perhaps this section can say that we propose an assertion be undetermined if it's "downstream" of the failing UB check, and then later, as an example of future pruning, you could give the example of only reachable passing assertions being undetermined.
There was a problem hiding this comment.
My overall motivation here is to try to be specific about what exactly we're proposing--we can always come back and update the RFC if we implement something different.
There was a problem hiding this comment.
I actually don't want to be super specific at this point. Maybe let me change the proposal to say that we shall mark all passing assertions as UNDETERMINED, and mentioned that refining the set of assertions marked as UNDETERMINED is out of scope of this RFC.
| We propose that the status of all passing assertions that may be affected by this check to be displayed as | ||
| `UNDETERMINED` if one or more UB checks fail. | ||
| For simplicity, Kani currently over-approximate this set by marking all passing assertions as `UNDETERMINED`. | ||
| Future pruning of this set can be done with further analysis, but it should not affect soundness. |
There was a problem hiding this comment.
Can you give examples of other pruning that we could do / it would make sense for us to do?
| This may create spurious counter examples for cases where the failing UB check is implemented using "demonic" | ||
| non-determinism.[^demonic] |
| ### Concrete playback of UB checks | ||
|
|
||
| A counter example that triggers UB may require extra tooling for debugging, e.g.: MIRI or valgrind. | ||
| We propose that tests added by concrete playback in those cases should include a comment stating such limitation. |
There was a problem hiding this comment.
| We propose that tests added by concrete playback in those cases should include a comment stating such limitation. | |
| We propose that tests added by concrete playback in those cases should include a comment stating this limitation. |
|
|
||
| ```rust | ||
| #[kani::proof] | ||
| #[kani::ignore(CHECK_NAMES)] |
| Failing due to an assumption check inside `get_unchecked` function. | ||
|
|
||
| ```plaintext | ||
| Failed Checks: assumption failed | ||
| ``` |
There was a problem hiding this comment.
| Failing due to an assumption check inside `get_unchecked` function. | |
| ```plaintext | |
| Failed Checks: assumption failed | |
| ``` | |
| Failing due to an [assumption check](https://github.com/rust-lang/rust/blob/a1d7676d6a8c6ff13f9165e98cc25eeec66cb592/library/core/src/slice/index.rs#L255) inside the `get_unchecked` function. | |
| ```plaintext | |
| Failed Checks: assumption failed | |
| File: "library/core/src/slice/index.rs", line 255, in <usize as std::slice::SliceIndex<[i32]>>::get_unchecked |
There was a problem hiding this comment.
(Just to make it a bit clearer that this is an assumption in the standard library itself, not some Kani model of get_unchecked).
| ``` | ||
|
|
||
| We would like to keep taking advantage of existing instrumentation to maximize the UB check coverage. | ||
| The mechanism used to build the check, however, shouldn't influence in the user experience. |
There was a problem hiding this comment.
This section does a great job of explaining the current division of UB checks and how those manifest in different experiences for users, but I'm missing a call to action--what are you proposing we do about it? Should we add a model of get_unchecked to Kani so that we can catch this error ourselves and provide a better error message? Or not, because then we're not relying on existing instrumentation? We don't need to land on a precise answer now (I know the implementation section is empty), but can we give some options at least?
Also, I'm a bit confused about the scope of this RFC. The User Experience section made me think that we were just talking about whether a passing check should pass or be undetermined based on a failing UB check before it. Now it seems like we're also considering the UX of the UB checks themselves. I would recommend adding a sentence or two about consistent messaging for failing UB checks to the User Experience section if you intend for that to be part of the "consistent framework" you're proposing.
|
@zhassan-aws @carolynzech thank you for the latest round of review. I gave this PR a second thought, and I decided to close it. Unfortunately, I don't think I have enough time to address the open questions, and maybe the UX we want can be driven by the std verification effort. It will give us opportunity to incorporate more user feedback and ensure we have a robust solution. |
Create a new RFC for standardizing Kani's UB checks.
I left the "Software Design" section empty for now so we can first focus on the user experience.
Note that this RFC might need some adjustment depending on the outcome of diffblue/cbmc#8242 and diffblue/cbmc#8226.
Related to #3089
Rendered version: https://celinval.github.io/kani-dev/rfc/rfcs/0010-rust-ub-checks.html
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.