Challenge 13: Safety of CStr

[celinval]

Challenge link: https://model-checking.github.io/verify-rust-std/challenges/0013-cstr.html

[Yenyun035]

Edit: After discussion, we were recommended to implement the Invariant manually using ub_checks::Invariant, as similar to this code.

---

@celinval We (Team 2) decided to work on this challenge for a week while waiting for Kani issue #3711 to unblock #59 Part 3.

For Part 1, we are writing a safety invariant for CStr. From the doc and Kani PR#3270 we found that #[derive(Invariant)] macro and #[safety_constraint(...)] attribute look useful. We are thinking about writing the safety invariant in c_str.rs like:

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

// Struct-level CStr safety invariant
#[derive(kani::Arbitrary)] // Might be useful when verifying methods that take a CStr as input
#[derive(kani::Invariant)]
#[safety_constraint(inner.len() > 0 && inner[inner.len() - 1] == 0 && !inner[..inner.len() - 1].contains(&0))]
pub struct CStr {
    // comments omitted
    inner: [c_char],
}

// Test harness
// pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError>
#[kani::proof]
#[kani::unwind(16)]  // Proof bounded by array length
fn check_from_bytes_until_nul() {
    const ARR_LEN: usize = 16;
    let mut string: [u8; ARR_LEN] = kani::any();
    // ensure that there is at least one null byte
    let idx: usize = kani::any_where(|x| *x >= 0 && *x < ARR_LEN);
    string[idx] = 0;

    let c_str = CStr::from_bytes_until_nul(&string).unwrap();
    assert!(c_str.is_safe());
}

However, the compilation of core (using the kani script) failed due to the following error:

error[E0404]: expected trait, found derive macro `core::kani::Invariant`
   --> /Users/yew005/Docs/Academic/CMU/Fall24/practicum/vrs/library/core/src/ffi/c_str.rs:109:10
    |
109 | #[derive(kani::Invariant)]
    |          ^^^^^^^^^^^^^^^ not a trait

We thought that this should be supported in Kani 0.54.0, but we were not able to compile. How could we fix it?

@rajathkotyal, @lanfeima, @MWDZ for visibility.

[rajathkotyal]

Upon some research, The compilation error could be due to the fact we are trying to include an external dep (kani::Invariant) into the source code compilation process, So even with the use of cfg["kani"] flag, the compiler tries to parse and resolve all macros and attributes. It cannot find kani::Invariant within the core crate.

There seems to be some ambiguity in the code / with my understanding. Some insight on this would help.