Prusti does not understand the question mark operator

[enjhnsn2]

When working with result and option types, it is very convenient to use the ? operator to propagate errors. Prusti does not crash when you use the ? operator, but it does not seem to understand that using a value unwrapped via ? is the same as a value unwrapped via a match. Given a function that returns an option:

#[ensures(match result {
    Some(r) => r == 3,
    None => true,  
})]
pub fn three_or_none(x: u32) -> Option<u32> {
    if x == 3 {
        Some(3)
    }
    else {
        None
    }
}

This function verifies:

// passes
pub fn test_manual_unwrap(x: u32) -> Option<u32> {
    let y = three_or_none(x);
    let y = match y {
        Some(z) => z,
        None => {return None;},
    };
    assert!(y == 3);
    Some(y)
}

whereas this function fails:

// fails
pub fn test_qm(x: u32) -> Option<u32> {
    let y = three_or_none(x)?;
    assert!(y == 3);
    Some(y)
}

while I expect these two assertions to be equisatisfiable.

Its not a huge priority, since it is not too hard to work around, however it would be very convenient if prusti had a better understanding of the ? operator. Thanks for the help.

[Aurel300]

Thanks for the suggestion! The reason this doesn't work right now is that the ? operator is desugared by the Rust compiler to a method call and by default that method has no specification and so Prusti has no way to know that internally the method does such a match. This might already be solvable using extern specs (maybe after #882). In any case, in the long term such a specification should of course be a part of the library of standard lib specifications.

[enjhnsn2]

Thanks for the fast response! I would have expected it to have been desugared to a match, but I guess I'll take a look at the underlying MIR to see how its desugared exactly and try to implement an external spec for it.

I don't need anything more from you, but if you keep this issue open, I'll post an update about whether I got it to work with the external spec if you're interested.