Spurious failure due to pointer operation returning non-deterministic value for dangling pointer

[celinval]

I tried this code:

#![feature(iter_advance_by)]

use std::iter::DoubleEndedIterator;

fn addr() -> usize {
    let addr = kani::any_where::<usize, _>(|val| *val == 9223372036854775809);
    // ***** Uncomment the line below to make the harness pass. ******
    // let addr =  9223372036854775809;
    assert_eq!(addr, 9223372036854775809);
    addr
}

fn any_slice(orig_slice: &[u8]) -> &[u8] {
    let ptr = addr() as *const u8;
    unsafe { core::slice::from_raw_parts(ptr, 0) }
}

mod verify_u8 {
    use super::*;
    const MAX_LEN: usize = 1;

    #[kanitool::proof]
    fn check_nth_back() {
        let array = [0u8; 0];
        let slice = any_slice(&array);
        assert!(slice.is_empty());
        let mut iter = slice.iter();
        let _ = iter.advance_by(kani::any());
    }
}

using the following command line invocation:

kani iter.rs

with Kani version: 0.56.0 (verify-rust-std branch)

I expected to see this happen: The verification result should be the same as the one where we assign addr directly.

Instead, this happened: Assigning the address using any_where makes the harness fail, while it succeeds when using the concrete value.

[celinval]

@tautschnig do you think you can take a look at this one to see if the inconsistency is coming from Kani or CBMC? Thanks!

[tautschnig]

This appears to be a bug in CBMC as disabling simplification makes the property fail even when let addr = 9223372036854775809; is in effect.

[tautschnig]

Turns out that CBMC may be doing something questionable, but the true problem remains with the input: 9223372036854775809 is not a pointer to an allocated object, which I believe violates the safety preconditions of sub_ptr. CBMC's back-end treats subtraction of pointers outside object bounds as producing an unconstrained value.

Kani will happily report this problem on this example with --enable-unstable --extra-pointer-checks, irrespective of whether you use assumptions or the direct assignment.

So I'd rather claim the problem is in the lack of (default) checks enabled by Kani?!

[remi-delmas-3000]

@tautschnig do you think we should instantiate pointer validity checks for each occurrence of pointer-integer conversions during the GOTO codegen from Kani ?

let ptr = addr() as *const u8;
/* assert(__CPROVER_r_ok(ptr, 0)) */

[tautschnig]

To me, that seems like a good idea. Though I don’t know how easy that is, e.g., with transmute to a union that includes a pointer-typed member.

[celinval]

@tautschnig do you think we should instantiate pointer validity checks for each occurrence of pointer-integer conversions during the GOTO codegen from Kani ?

let ptr = addr() as *const u8;
/* assert(__CPROVER_r_ok(ptr, 0)) */

Wait, wouldn't that cause spurious counter examples with slices and vectors? This issue is showing up because the standard library encodes length of a ZST iterator by casting the length as a pointer.

[tautschnig]

Wait, wouldn't that cause spurious counter examples with slices and vectors? This issue is showing up because the standard library encodes length of a ZST iterator by casting the length as a pointer.

Is that defined behaviour in Rust? Given all the talk that some integer (Boolean?) types must not have values outside a certain range I am wondering whether pointers do have a similar constraint to them?

[tautschnig]

Should be addressed by diffblue/cbmc#8497.

[celinval]

Wait, wouldn't that cause spurious counter examples with slices and vectors? This issue is showing up because the standard library encodes length of a ZST iterator by casting the length as a pointer.

Is that defined behaviour in Rust? Given all the talk that some integer (Boolean?) types must not have values outside a certain range I am wondering whether pointers do have a similar constraint to them?

Yes. That's a well defined behavior. Raw pointers don't have any validity requirements.

[tautschnig]

diffblue/cbmc#8497 has been merged and I have confirmed that we now get consistent results. We should close this issue with the next CBMC release (and Kani using that newer version).

[celinval]

And which behavior is that? Will the verification succeed?

[tautschnig]

And which behavior is that? Will the verification succeed?

My apologies for not having clarified that: yes, verification now consistently succeeds. (Which should be the correct result given all pointer handling is well-defined for Rust.)

[celinval]

I've built CBMC from scratch and I was able to verify that it fixes all the harnesses that are currently commented out in model-checking/verify-rust-std#148. Thanks!

Looking forward for the next CBMC release.

[celinval]

Note that there is also a harness commented out in model-checking/verify-rust-std#122 that needs to be updated once we fix this issue.