Autoharness: support &Wtf8 arguments under --bounded-arguments - #4809
Open
srivatsansamraj wants to merge 4 commits into
Open
srivatsansamraj wants to merge 4 commits into
srivatsansamraj wants to merge 4 commits into
Conversation
`&str` arguments are generated by `any_str_ref`, which returns the longest valid-UTF-8 prefix of nondeterministic harness-local storage. `&CStr` had no such model and was skipped for a missing Arbitrary implementation: 67 functions on a whole-library `verify-std` run, 23 of them in `core`. Add `any_c_str_ref` with the same discipline. The last byte of the storage is set to NUL and `from_bytes_until_nul` returns the bytes before the first one, so the result is a deterministic function of the nondeterministic bytes and satisfies `CStr`'s invariant by construction: no `assume` is involved, and every C string of length `k` below the bound arises from storage whose first NUL is at index `k`. The slice bound applies, less one byte for the NUL. Eligibility and harness generation both identify `CStr` through `is_c_str`, so they cannot disagree. `&mut CStr` stays unsupported, as `&mut str` does. The test follows `cargo_autoharness_slices`: the argument is reported as requiring the flag without it, and with it a bounds-checked read fails on the empty string, the no-interior-NUL invariant holds, and covers show the empty, the longest and a specific C string are all generated.
github-actions
Bot
added
Z-EndToEndBenchCI
The local receiving the `any_c_str_ref` call was typed `&mut CStr`, the shape the slice model returns, while the model returns `&CStr`; the value was then reborrowed as shared. Codegen tolerated the mismatch, but the MIR was ill-typed. Only the slice model returns `&mut [T]`, to serve both mutabilities; the string models return the shared reference. The destination now follows that, and the reborrow applies to slices only.
`&[T]` and `&str` arguments are generated from nondeterministic harness-local storage by `any_slice_ref` and `any_str_ref`, and `&CStr` by `any_c_str_ref`. `&ByteStr` had no model and was skipped for a missing Arbitrary implementation: 104 functions on a whole-library `verify-std` run, 88 of them in `core`. A `ByteStr` is a `[u8]` with no further invariant, so `any_byte_str_ref` is `ByteStr::new` over `any_slice_ref`, with the slice bound. Eligibility and harness generation identify the type through `is_byte_str`, matched by name inside `core::bstr` since the type has no diagnostic item. `&mut ByteStr` stays unsupported, as `&mut str` does. The `kani` crate gains `#![feature(bstr)]`; inside `core` the module is already present. The test follows `cargo_autoharness_slices`: reported as requiring the flag without it; with it, an unchecked index fails on the empty value, and covers show the empty, the 16-byte and a specific byte string are all generated.
`&str` arguments are generated from nondeterministic harness-local storage by `any_str_ref`, `&CStr` by `any_c_str_ref` and `&ByteStr` by `any_byte_str_ref`. `&Wtf8` had no model and was skipped for a missing Arbitrary implementation: 32 functions in `core` on a whole-library `verify-std` run. WTF-8 is a superset of UTF-8, so `any_wtf8_ref` is `Wtf8::from_str` over `any_str_ref`, with the string bound. Strings holding surrogate code points are not generated, since `core` has no WTF-8 validator to build them soundly. Eligibility and harness generation identify the type through `is_wtf8`, matched by name inside `core::wtf8` since the type has no diagnostic item. `&mut Wtf8` stays unsupported, as `&mut str` does. The `kani` crate gains `#![feature(wtf8_internals)]`; `std` does not re-export the module, so the model names the type through `core`. The test follows `cargo_autoharness_byte_str`: reported as requiring the flag without it; with it, an unchecked index fails on the empty value, and covers show the empty, the 4-byte and a specific string are all generated.
srivatsansamraj
force-pushed
the
wtf8-bounded-ref
branch
from
September 19, 2026 02:13
ae45a19 to
f3c66ce
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
&strarguments are generated from nondeterministic harness-local storage byany_str_ref; #4804 adds&CStrand #4806&ByteStr.&Wtf8had no model and was skipped for a missing Arbitrary implementation: 32 functions incoreon a whole-libraryverify-stdrun.WTF-8 is a superset of UTF-8, so
any_wtf8_refisWtf8::from_stroverany_str_ref, with the string bound. Strings holding surrogate code points are not generated, sincecorehas no WTF-8 validator to build them soundly. Eligibility and harness generation identify the type throughis_wtf8, matched by name insidecore::wtf8since the type has no diagnostic item.&mut Wtf8stays unsupported, as&mut strdoes. Thekanicrate gains#![feature(wtf8_internals)];stddoes not re-export the module, so the model names the type throughcore.The test follows
cargo_autoharness_byte_str: reported as requiring the flag without it; with it, an unchecked index fails on the empty value, and covers show the empty, the 4-byte and a specific string are all generated.This branch includes #4804 and #4806; only the last commit is new here.
Resolves #4808
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.