Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add proof for Result method check_unwrap_unchecked #35

Closed
wants to merge 4 commits into from
Closed

Add proof for Result method check_unwrap_unchecked #35

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e351be9
Add first proof
jaisnan Jul 10, 2024
262f391
Merge branch 'main' into add-result-contract
jaisnan Aug 16, 2024
cc2c94b
Merge branch 'main' into add-result-contract
tautschnig Aug 20, 2024
4b36a0e
Merge branch 'main' into add-result-contract
jaisnan Aug 28, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 20 additions & 0 deletions library/core/src/result.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -513,10 +513,14 @@

#![stable(feature = "rust1", since = "1.0.0")]

use safety::requires;
use crate::iter::{self, FusedIterator, TrustedLen};
use crate::ops::{self, ControlFlow, Deref, DerefMut};
use crate::{convert, fmt, hint};

#[cfg(kani)]
use crate::kani;

/// `Result` is a type that represents either success ([`Ok`]) or failure ([`Err`]).
///
/// See the [module documentation](self) for details.
Expand Down Expand Up @@ -1480,6 +1484,7 @@ impl<T, E> Result<T, E> {
#[inline]
#[track_caller]
#[stable(feature = "option_result_unwrap_unchecked", since = "1.58.0")]
#[requires(self.is_ok())]
pub unsafe fn unwrap_unchecked(self) -> T {
debug_assert!(self.is_ok());
match self {
Expand Down Expand Up @@ -1512,6 +1517,7 @@ impl<T, E> Result<T, E> {
#[inline]
#[track_caller]
#[stable(feature = "option_result_unwrap_unchecked", since = "1.58.0")]
#[requires(self.is_err())]
pub unsafe fn unwrap_err_unchecked(self) -> E {
debug_assert!(self.is_err());
match self {
Expand Down Expand Up @@ -2003,3 +2009,17 @@ impl<T, E, F: From<E>> ops::FromResidual<ops::Yeet<E>> for Result<T, F> {
impl<T, E> ops::Residual<T> for Result<convert::Infallible, E> {
type TryType = Result<T, E>;
}

#[cfg(kani)]
#[unstable(feature="kani", issue="none")]
mod verify {
use super::*;

#[kani::proof_for_contract(Result::unwrap_unchecked)]
pub fn check_unwrap_unchecked() {
let val: Result<u32, u64> = kani::any();
let ok_variant: Result<u32, u64> = Ok(0);
let copy = unsafe { ok_variant.unwrap_unchecked() };
assert_eq!(val, Result::Ok(copy));
Copy link

@carolynzech carolynzech Aug 28, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since val is a nondeterministic Result, it's not necessary equal to Result::Ok(0) (it could also be Result::Err, or Result::Ok(12), etc.).
Instead, I'd write:

pub fn check_unwrap_unchecked() {
        let val: u32= kani::any();
        let ok_variant: Result<u32, u64> = Ok(val);
        let copy = unsafe { ok_variant.unwrap_unchecked() };
        assert_eq!(val, copy);
    }

which passes verification for me locally.

(I'd also add harnesses for other types besides u32 and for unwrap_err_unchecked, but I assume you were planning on that).

}
}
Loading