Autoharness: &str arguments can be invalid UTF-8 under verify-std, causing spurious failures #5030

Under verify-std, the &str values that autoharness generates with --bounded-arguments (via any_str_ref) are not always valid UTF-8, so harnesses for functions taking &str can fail on inputs that no real caller could pass.

Mechanism

1. any_str_ref (added in Autoharness: support slice and string arguments (bounded) #4691) builds the string as the longest valid UTF-8 prefix of nondeterministic bytes, using core::str::from_utf8 and Utf8Error::valid_up_to.
2. In verify-rust-std, run_utf8_validation carries loop_invariants (added in Add loop contracts and harness for run_utf8_validation verify-rust-std#159). These invariants only bound the loop index; they say nothing about the bytes being valid UTF-8.
3. kani autoharness always enables loop contracts (enable_autoharness in kani-driver/src/autoharness/mod.rs), so under verify-std the validator loops are replaced by their invariants.
4. As a result, from_utf8 / valid_up_to can return imprecise results there: Ok for invalid bytes, Err for valid bytes, or a valid_up_to that falls inside a character. any_str_ref then hands an invalid &str to the function under test.

Minimal reproduction

The function below checks UTF-8 validity byte by byte (RFC 3629), without calling from_utf8 or anything in str::validations.

fn kani_repro_assert_valid_utf8(s: &str) {
    let b = s.as_bytes();
    let n = b.len();
    crate::kani::cover(n > 0 && b[0] >= 0x80, "non-ASCII first byte");
    crate::kani::cover(n >= 2, "at least two bytes");
    let mut i: usize = 0;
    while i < n {
        let x = b[i];
        // (sequence width, allowed range of the second byte)
        let (w, lo, hi): (usize, u8, u8) = if x < 0x80 {
            (1, 0x80, 0xBF)
        } else if x >= 0xC2 && x <= 0xDF {
            (2, 0x80, 0xBF)
        } else if x == 0xE0 {
            (3, 0xA0, 0xBF)
        } else if x == 0xED {
            (3, 0x80, 0x9F)
        } else if (x >= 0xE1 && x <= 0xEC) || x == 0xEE || x == 0xEF {
            (3, 0x80, 0xBF)
        } else if x == 0xF0 {
            (4, 0x90, 0xBF)
        } else if x >= 0xF1 && x <= 0xF3 {
            (4, 0x80, 0xBF)
        } else if x == 0xF4 {
            (4, 0x80, 0x8F)
        } else {
            (0, 0, 0)
        };
        assert!(w != 0, "repro: invalid lead byte");
        assert!(i + w <= n, "repro: truncated sequence");
        if w >= 2 {
            assert!(b[i + 1] >= lo && b[i + 1] <= hi, "repro: bad second byte");
        }
        let mut k: usize = 2;
        while k < w {
            assert!(b[i + k] >= 0x80 && b[i + k] <= 0xBF, "repro: bad continuation byte");
            k += 1;
        }
        i += w;
    }
}

kani autoharness -Z autoharness -Z unstable-options -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers -Z stubbing --std ./library --bounded-arguments --include-pattern kani_repro_assert_valid_utf8 --harness kani_repro

cargo kani autoharness -Z autoharness --bounded-arguments

Results

Default string bound of 4 in both cases:

1. verify-std: FAILED, 4 of 832 checks failed. All four assertions fail (invalid lead byte, truncated sequence, bad second byte, bad continuation byte). Both cover properties are satisfied.
2. Regular crate: SUCCESS, 0 of 204 checks failed. Both cover properties are satisfied, so multi-byte inputs are reached.

Counterexamples

Taken from CBMC traces (--keep-temps, then cbmc --property <id> --trace) under the same verify-std setup:

1. Bytes 57 ED ED ED (invalid: ED must be followed by 80..=9F), from the autoharness for <char as FromStr>::from_str. from_utf8 returned Ok, so the generated &str is all four bytes. Decoding later yields code point 0xDB6D, and the from_u32_unchecked precondition char_try_from_u32(i).is_ok() fails.
2. Bytes CD 8F CD CD (the valid prefix is 2 bytes), from the same harness. from_utf8 returned Err with valid_up_to() == 1, so the generated &str is the lone lead byte CD. next_code_point then calls unwrap_unchecked on None, and the requires(false) on hint::unreachable_unchecked fails.
3. The opposite direction also occurs: in a harness for the searcher models I'm adding for Autoharness: support the MultiCharEq searcher types in core::str::pattern #4811 (which build their haystack with any_str_ref), the valid sequence F2 8F BF BF (U+8FFFF) got valid_up_to() == 3.

Impact

1. Under verify-std, autoharness harnesses with &str arguments can report spurious failures, typically on the preconditions of char::from_u32_unchecked and hint::unreachable_unchecked reached while decoding.
2. Whether this can also hide real failures (for example, if some valid strings can no longer be generated) is not confirmed. I haven't checked that.
3. My guess is that CI has not hit this because the verify-rust-std workflows pass --no-assert-contracts, so these preconditions are not checked there and invalid strings go unnoticed. I haven't verified this.

Related

1. Autoharness: support slice and string arguments (bounded) #4691: introduced any_str_ref and the longest-valid-prefix approach.
2. Add loop contracts and harness for run_utf8_validation verify-rust-std#159: added the loop contracts to run_utf8_validation.
3. Verify safety of char-related Searcher methods (Challenge 20) verify-rust-std#537: notes that under -Z loop-contracts the from_utf8 result "cannot soundly filter symbolic bytes", and builds haystacks constructively instead.
4. Challenge 10: Verify memory safety of String functions with Kani verify-rust-std#702: notes that the abstracted validator can return Err for valid multi-byte UTF-8, and stubs from_utf8 in a retain harness.

Possible directions

Just ideas, happy to follow whatever you prefer:

1. Compute the longest valid UTF-8 prefix inside kani_core itself, so that it does not go through str::validations and is not affected by its loop contracts.
2. Build the string constructively from nondeterministic chars via encode_utf8, as verify-rust-std#537 does.
3. Either way, String's BoundedArbitrary implementation uses the same prefix approach and is probably affected too.

Versions

1. Kani 0.68.0, built from a local branch based on main at 9461e07. The branch does not modify any_str_ref or String's BoundedArbitrary; it only adds new models that call any_str_ref.
2. CBMC 6.11.0.
3. Rust toolchain nightly-2026-10-12.
4. verify-rust-std at bcb233071e1 (sync-2026-10-11).
5. aarch64 Linux (Ubuntu 26.04).