CStr Safety invariant & Harnesses for from_bytes_until_nul

[Yenyun035]

Resolves / Towards #150

Changes

• Added a CStr Safety Invariant
• Added a harness for from_bytes_until_nul, the harness covers:
  • The input slice contains a single null byte at the end;
  • The input slice contains no null bytes;
  • The input slice contains intermediate null bytes

Discussion

• Safety invariant implementation
• Input array generation

Verification Result

./scripts/run-kani.sh --kani-args --harness ffi::c_str::verify

// array size 16
Checking harness ffi::c_str::verify::check_from_bytes_until_nul...

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

VERIFICATION:- SUCCESSFUL
Verification Time: 7.3023376s

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

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Yenyun035]

@celinval @zhassan-aws

Questions
While we explicitly write three different checks, we're wondering if a positive harness (e.g. Check 1) and a negative harness would be sufficient. By negative, we mean that we can have a check to call from_bytes_until_nul on an array without a null byte. The difference between the two harnesses is that we need the kani::should_panic for the negative case. Here is an example of the said two harnesses:

    // Positive check
    #[kani::proof]
    #[kani::unwind(32)]
    fn check_from_bytes_until_nul() {
        const ARR_LEN: usize = 32;
        let mut string: [u8; ARR_LEN] = kani::any();
        // ensure that there is at least one null byte
        let idx: usize = kani::any_where(|x: &usize| *x >= 0 && *x < ARR_LEN);
        string[idx] = 0;

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

    // Negative check
    #[kani::proof]
    #[kani::unwind(5)]
    #[kani::should_panic]
    fn check_from_bytes_until_nul_panic() {
        const ARR_LEN: usize = 4;
        // let mut string: [u8; ARR_LEN] = [64, 65, 66];
        // The array does not contain any null bytes. Calling
        // from_bytes_until_nul will return an error.
        let mut string: [u8; ARR_LEN] = kani::any_where(|x: &[u8; ARR_LEN]| !x.contains(&0));

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

Verification result:

// panic case
SUMMARY:
 ** 1 of 134 failed (18 unreachable)
Failed Checks: This is a placeholder message; Kani doesn't support message formatted at runtime
 File: "/Users/yew005/Docs/Academic/CMU/Fall24/practicum/vrs/library/core/src/result.rs", line 1698, in result::unwrap_failed

VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
Verification Time: 0.6366273s

// regular case
SUMMARY:
 ** 0 of 142 failed (5 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 5.0670085s

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

[celinval]

Hi @Yenyun035, that's a great question. I think in the case of from_bytes_until_nul, you could potentially have one harness only. If you don't invoke unwrap in the result, the harness shouldn't panic, independent on whether it has a nul character or not.

Thus, it should be enough to create an arbitrary slice of [u8], and provide it to the function. You could then match on the result, and if it is Ok(cstr), you check that the cstr is safe.

[Yenyun035]

@celinval Thank you very much for your advice! I modified the harness and the PR description accordingly, and now it should be good to go.

[celinval]

Thanks!

[Yenyun035]

@celinval Thank you for your comments. I resolved the conversations. Please let me know if anything else to be modified :)

[Yenyun035]

@zhassan-aws Thank you for your comments. I just fixed them.