From 96f50da432aebb5641f84307f1899ce1773548dd Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 28 Jun 2024 16:07:33 -0700 Subject: [PATCH] Address some of the feedback - Changed the example. - Improved text. - Removed restriction on unstable opt-out. --- rfc/src/SUMMARY.md | 2 +- rfc/src/rfcs/0011-rust-ub-checks.md | 40 +++++++++++++++++++---------- 2 files changed, 27 insertions(+), 15 deletions(-) diff --git a/rfc/src/SUMMARY.md b/rfc/src/SUMMARY.md index b3acd8794988..33cc132baf1e 100644 --- a/rfc/src/SUMMARY.md +++ b/rfc/src/SUMMARY.md @@ -16,4 +16,4 @@ - [0008-line-coverage](rfcs/0008-line-coverage.md) - [0009-function-contracts](rfcs/0009-function-contracts.md) - [0010-quantifiers](rfcs/0010-quantifiers.md) -- [0011-rust-ub-checks](rfcs/0011-rust-ub-checks) +- [0011-rust-ub-checks](rfcs/0011-rust-ub-checks.md) diff --git a/rfc/src/rfcs/0011-rust-ub-checks.md b/rfc/src/rfcs/0011-rust-ub-checks.md index 9519c93e8914..b2fbc3089dd9 100644 --- a/rfc/src/rfcs/0011-rust-ub-checks.md +++ b/rfc/src/rfcs/0011-rust-ub-checks.md @@ -1,7 +1,7 @@ - **Feature Name:** Rust UB Checks (`rust-ub-checks`) - **Feature Request Issue:** [#3089](https://github.com/model-checking/kani/issues/3089) -- **RFC PR:** [#XXXX](https://github.com/model-checking/kani/pull/3091) -- **Status:** Under Review +- **RFC PR:** [#3091](https://github.com/model-checking/kani/pull/3091) +- **Status:** Unstable - **Version:** 0 - **Proof-of-concept:** @@ -24,11 +24,21 @@ detected undefined behavior. 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. [^all-passing] +`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. -All failing assertions should have their status preserved, unless the UB check is implemented using "demonic" -non-determinism, such as CBMC's deallocated check. -See [0010-rust-ub-checks.md#open-questions] for alternatives to be considered. +All failing assertions will have their status preserved. +This may create spurious counter examples for cases where the failing UB check is implemented using "demonic" +non-determinism.[^demonic] + +[^demonic]: Some UB checks implementation use one tracker with non-deterministic assignment to track the +status of different objects. +This implementation relies on the fact that an assertion will fail if there is at least one possible +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. ### Concrete playback of UB checks @@ -47,11 +57,12 @@ invalid write: #[kani::proof] fn buggy_code() { let mut value: bool = false; + let ptr: *mut bool = &mut value as *mut _; + let mut_ref = &mut value; unsafe { - let ptr: *mut u8 = &mut value as *mut _ as *mut u8; - *ptr = 8; // This assignment does not cause UB... + *ptr = true; // This assignment is safe if `mut_ref` is never used! } - assert!(value); // ...but this read triggers UB! ⚠️ + assert!(!*mut_ref); // This triggers UB ⚠️! } ``` @@ -69,7 +80,7 @@ In those cases, Kani check must be explicit about this failure being an over-app 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]). -### Opt-out a class of UB checks +### Opt-out of a class of UB checks Undefined behavior checks that have been stabilized should be added by default by Kani. However, Kani should provide a fine-grained control for users to choose which checks to disable. @@ -91,8 +102,8 @@ fn harness() {} Where `CHECK_NAMES` is a list of check category names in snake case, such as `memory_safety`, `valid_values`. -For checks that are unstable, Kani should support both opt-out mechanisms. -These checks shall be included by default if their respective unstable flag are passed, i.e., `-Z[CHECK-NAME]` +For checks that are unstable, they should only be included if their respective unstable flag are passed, i.e., +`-Z [CHECK-NAME]`. ## Software Design @@ -167,9 +178,10 @@ I.e.: It may impact the status of a previously passing harness if a new check fa - 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? + - I think we should at least consider adding that option for `kani` library code. + - We've been adding more logic that is used by UB checks, and we may want to skip some checks for them. ## Out of scope / Future Improvements - **List enabled checks:** Kani could include a command that list all the categories of undefined behaviors supported. - -[^all-passing]: For simplicity, we currently over-approximate this by marking all passing assertions as UNDETERMINED. \ No newline at end of file