added harnesses for c_str: is_empty

[lanfeima]

Update:

I noticed that PR #194 leverages arbitrary_cstr (introduced in #189) to simplify the harness CStr::is_empty. Please also check that PR for additional context.

Towards: Issue #150

Parent branch: main

---

Changes

• added harnesses. for CStr:: is_empty

This version of C

To revalidate the verification results, run ./scripts/run-kani.sh --kani-args --harness ffi::c_str::verify::check_is_empty

Example output:

Checking harness ffi::c_str::verify::check_is_empty...

VERIFICATION RESULT:
 ** 0 of 216 failed (5 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 1121.6111s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.

[Yenyun035]

Duplicate with #194. Will resolve later.

[lanfeima]

I see that PR #194 takes an efficient approach by leveraging arbitrary_cstr. The main difference is that PR #195 explores handling invalid cases during the construction phase (e.g., how is_empty behaves under invalid input), which takes a long time and might not be necessary given that is_empty can only be invoked on valid CStr instances. I now realize that focusing on valid inputs may be more aligned with the project goals.

Would it make sense to address invalid cases elsewhere, or should we focus solely on valid instances here? Feedback from reviewers would be helpful. I’d be happy to close this PR or contribute to refining #194 if needed. Thank you!

[celinval]

Can we merge the ideas by optimizing the arbitrary_str by adding byte 0 to the end of the slice?

[Yenyun035]

Can we merge the ideas by optimizing the arbitrary_str by adding byte 0 to the end of the slice?

@celinval If I understand correctly, do you mean that we ensure the input slice is null-terminated before passing it to arbitrary_cstr? This sounds equivalent to the idea that we assume the input slice is null-terminated within arbitrary_cstr, e.g.

fn arbitrary_cstr(slice: &[u8]) -> &CStr {
    // At a minimum, the slice contains a null byte to form a valid CStr.
    kani::assume(slice.len() > 0 && slice[slice.len() - 1] == 0);
    let result = CStr::from_bytes_until_nul(&slice);
    // Given the assumption, from_bytes_until_nul should never fail
    kani::assume(result.is_ok()); // maybe change to assert!(result.is_ok());
    let c_str = result.unwrap();
    assert!(c_str.is_safe());
    c_str
}

I updated PR#194 accordingly.

[Yenyun035]

PR #194 was merged. This PR can be closed. @lanfeima

[tautschnig]

Closing per #195 (comment).