From 24626ac44367402e154c05f1cbd901a47fa348d0 Mon Sep 17 00:00:00 2001 From: Srivatsan Samraj <321934658+srivatsansamraj@users.noreply.github.com> Date: Thu, 17 Sep 2026 18:55:29 -0700 Subject: [PATCH 1/4] Autoharness: support `&CStr` arguments under --bounded-arguments `&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. --- .../src/reference/experimental/autoharness.md | 8 ++-- .../src/kani_middle/kani_functions.rs | 2 + kani-compiler/src/kani_middle/mod.rs | 18 +++++++++ .../src/kani_middle/transform/automatic.rs | 22 ++++++++--- library/kani_core/src/arbitrary.rs | 18 +++++++++ .../cargo_autoharness_c_str/Cargo.toml | 10 +++++ .../cargo_autoharness_c_str/c-str.expected | 16 ++++++++ .../cargo_autoharness_c_str/c-str.sh | 15 ++++++++ .../cargo_autoharness_c_str/config.yml | 5 +++ .../cargo_autoharness_c_str/src/lib.rs | 38 +++++++++++++++++++ 10 files changed, 144 insertions(+), 8 deletions(-) create mode 100644 tests/script-based-pre/cargo_autoharness_c_str/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoharness_c_str/c-str.expected create mode 100755 tests/script-based-pre/cargo_autoharness_c_str/c-str.sh create mode 100644 tests/script-based-pre/cargo_autoharness_c_str/config.yml create mode 100644 tests/script-based-pre/cargo_autoharness_c_str/src/lib.rs diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index 9cf4070c199..3e25fa198f2 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -250,9 +250,11 @@ that use bounded values are marked **"(bounded)"** in the summary table, and a n table repeats the caveat. With `--bounded-arguments`, for a function with `&[T]`/`&mut [T]` arguments (where `T` -implements or can derive `Arbitrary`) or `&str` arguments, the generated harness produces a -slice of nondeterministic length, backed by nondeterministic storage that lives for the entire -harness: by default **up to 16 elements** for slices and **up to 4 bytes** for strings. Strings cover all +implements or can derive `Arbitrary`), `&str` arguments, or `&CStr` arguments, the generated +harness produces a slice of nondeterministic length, backed by nondeterministic storage that +lives for the entire harness: by default **up to 16 elements** for slices, **up to 4 bytes** for +strings, and **up to 15 bytes** plus the terminating NUL for C strings (which follow the slice +bound, less one for the NUL). Strings cover all valid UTF-8 contents up to the bound (the generated string is the longest valid-UTF-8 prefix of nondeterministic bytes, the same approach as `String`'s `BoundedArbitrary` implementation); the smaller bound reflects the cost of reasoning about UTF-8 for symbolic execution. The bounds are diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 20d4fe00902..2439e63119f 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -93,6 +93,8 @@ pub enum KaniModel { AnyArc, #[strum(serialize = "AnyBoxModel")] AnyBox, + #[strum(serialize = "AnyCStrRefModel")] + AnyCStrRef, #[strum(serialize = "AnyPtrModel")] AnyPtr, #[strum(serialize = "AnyRcModel")] diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index f3376274697..44a2b9a1eb6 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -1024,6 +1024,15 @@ fn implements_bounded_arbitrary(tcx: TyCtxt, ty: Ty, kani_bounded_any_def: FnDef false } +/// Whether `def` is `core::ffi::CStr`. +/// +/// Both the eligibility check (`autoharness_supported_arg_ty`) and the harness generation +/// (`call_kani_any_for_ty`) use this, so that they cannot disagree on a `&CStr` argument. +pub fn is_c_str(tcx: TyCtxt, def: AdtDef) -> bool { + Some(rustc_internal::internal(tcx, def.def_id())) + == tcx.get_diagnostic_item(rustc_span::sym::cstr_type) +} + /// The formatting traits whose implementations automatic harnesses can verify via dedicated /// models (c.f. `KaniModel::CheckDebugFmt`/`CheckDisplayFmt`). #[derive(Copy, Clone, Debug, Eq, PartialEq)] @@ -1222,6 +1231,15 @@ fn autoharness_supported_arg_ty( ArgSupport::Unsupported } } + // A `&CStr` is the bytes of nondeterministic storage up to its first NUL, c.f. + // `any_c_str_ref`. Immutable only, as for `&str`. + TyKind::RigidTy(RigidTy::Adt(def, _)) if is_c_str(tcx, def) => { + if inner_mutability == Mutability::Not { + ArgSupport::Bounded + } else { + ArgSupport::Unsupported + } + } _ => arbitrary_or_derive(ty, ty_arbitrary_cache), } } else { diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 65c3a8bf87c..d547f90c1dc 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -18,7 +18,7 @@ use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_middle::{ CtorReturn, FmtTrait, SmartPointerModels, adt_has_private_field_check, can_derive_arbitrary, find_arbitrary_constructor, fmt_impl_self_ty, implements_arbitrary, implements_invariant, - scalar_niche, smart_pointer_model_instance, + is_c_str, scalar_niche, smart_pointer_model_instance, }; use crate::kani_queries::QueryDb; use rustc_data_structures::fx::FxHashMap; @@ -51,6 +51,8 @@ struct AnyModels { kani_any_slice_ref: FnDef, /// The FnDef of KaniModel::AnyStrRef kani_any_str_ref: FnDef, + /// The FnDef of KaniModel::AnyCStrRef + kani_any_c_str_ref: FnDef, /// The FnDef of KaniHook::Assume (used for layout-niche assumptions and constructor /// success). kani_assume: FnDef, @@ -84,6 +86,7 @@ impl AnyModels { kani_any_ptr: *kani_fns.get(&KaniModel::AnyPtr.into()).unwrap(), kani_any_slice_ref: *kani_fns.get(&KaniModel::AnySliceRef.into()).unwrap(), kani_any_str_ref: *kani_fns.get(&KaniModel::AnyStrRef.into()).unwrap(), + kani_any_c_str_ref: *kani_fns.get(&KaniModel::AnyCStrRef.into()).unwrap(), kani_assume: *kani_fns.get(&KaniHook::Assume.into()).unwrap(), kani_assert: *kani_fns.get(&KaniHook::Assert.into()).unwrap(), kani_assume_safe: *kani_fns.get(&KaniModel::AssumeSafe.into()).unwrap(), @@ -1173,10 +1176,11 @@ fn call_kani_any_for_ty( return lcl; } if let TyKind::RigidTy(RigidTy::Ref(region, inner_ty, inner_mutability)) = ty.kind() - && matches!( - inner_ty.kind(), - TyKind::RigidTy(RigidTy::Slice(..)) | TyKind::RigidTy(RigidTy::Str) - ) + && match inner_ty.kind() { + TyKind::RigidTy(RigidTy::Slice(..)) | TyKind::RigidTy(RigidTy::Str) => true, + TyKind::RigidTy(RigidTy::Adt(def, _)) => is_c_str(tcx, def), + _ => false, + } { let is_str = matches!(inner_ty.kind(), TyKind::RigidTy(RigidTy::Str)); let (elem_ty, model, model_args) = match inner_ty.kind() { @@ -1197,6 +1201,14 @@ fn call_kani_any_for_ty( TyConst::try_from_target_usize(models.string_bound).unwrap(), )]), ), + // `&CStr`: bytes up to the first NUL of the storage, sized by the slice bound. + TyKind::RigidTy(RigidTy::Adt(..)) => ( + Ty::unsigned_ty(UintTy::U8), + models.kani_any_c_str_ref, + GenericArgs(vec![GenericArgKind::Const( + TyConst::try_from_target_usize(models.slice_bound).unwrap(), + )]), + ), _ => unreachable!(), }; diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index 1ed78a5e702..c02b8d23f16 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/library/kani_core/src/arbitrary.rs @@ -241,6 +241,24 @@ macro_rules! generate_arbitrary { unsafe { core_path::str::from_utf8_unchecked(&storage[..valid_len]) } } + /// Generate a C string referring to the bytes of `storage` up to its first NUL, where + /// `storage` is a nondeterministic byte array (at most `N` bytes, `N` at least 1) whose + /// last byte is set to NUL so that one always exists. As with `any_str_ref`, the result + /// is a deterministic function of the nondeterministic bytes: every C string of length + /// `k < N` arises from storage whose first NUL is at index `k`. + /// + /// This model is used by the compiler to generate nondeterministic `&CStr` arguments for + /// automatic harnesses (`kani autoharness`). Note that any verification result obtained + /// with a bounded value like this one is valid only up to the bound. + #[kanitool::fn_marker = "AnyCStrRefModel"] + #[inline(never)] + #[doc(hidden)] + pub fn any_c_str_ref(storage: &mut [u8; N]) -> &core_path::ffi::CStr { + storage[N - 1] = 0; + // `storage` ends in NUL, so one is always found. + core_path::ffi::CStr::from_bytes_until_nul(storage).unwrap() + } + arbitrary_tuple!(A); arbitrary_tuple!(A, B); arbitrary_tuple!(A, B, C); diff --git a/tests/script-based-pre/cargo_autoharness_c_str/Cargo.toml b/tests/script-based-pre/cargo_autoharness_c_str/Cargo.toml new file mode 100644 index 00000000000..e01cf4097ba --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_c_str/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_c_str" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoharness_c_str/c-str.expected b/tests/script-based-pre/cargo_autoharness_c_str/c-str.expected new file mode 100644 index 00000000000..07c364e3b77 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_c_str/c-str.expected @@ -0,0 +1,16 @@ +[without --bounded-arguments] +| cargo_autoharness_c_str | c_str_cover | Requires --bounded-arguments for argument(s) s: &std::ffi::CStr | +[with --bounded-arguments] +| cargo_autoharness_c_str | nested | Missing Arbitrary implementation for argument(s) s: &&std::ffi::CStr | +Failed Checks: index out of bounds: the length is less than or equal to the given index +Status: SATISFIED\ +Description: "empty C string" +Status: SATISFIED\ +Description: "maximum-length C string" +Status: SATISFIED\ +Description: "C string "ab"" +| cargo_autoharness_c_str | c_str_cover | #[kani::proof] (bounded) | Success | +| cargo_autoharness_c_str | len | #[kani::proof] (bounded) | Success | +| cargo_autoharness_c_str | no_interior_nul | #[kani::proof] (bounded) | Success | +| cargo_autoharness_c_str | first | #[kani::proof] (bounded) | Failure | +Complete - 3 successfully verified functions, 1 failures, 4 total. diff --git a/tests/script-based-pre/cargo_autoharness_c_str/c-str.sh b/tests/script-based-pre/cargo_autoharness_c_str/c-str.sh new file mode 100755 index 00000000000..abe44932bef --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_c_str/c-str.sh @@ -0,0 +1,15 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eu + +echo "[without --bounded-arguments]" +# Capture the command status explicitly: piping straight into `grep` would mask a +# failure of `cargo kani ... --list` (the pipeline would report grep's status). +list_output=$(cargo kani autoharness -Z autoharness --list 2>&1) +echo "$list_output" | grep -m1 'Requires --bounded-arguments' + +echo "[with --bounded-arguments]" +# This run reports a failure (`first`), so it exits non-zero (see config.yml). +cargo kani autoharness -Z autoharness -Z unstable-options --output-format=regular --bounded-arguments --harness-timeout 5m diff --git a/tests/script-based-pre/cargo_autoharness_c_str/config.yml b/tests/script-based-pre/cargo_autoharness_c_str/config.yml new file mode 100644 index 00000000000..4416db02ff2 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_c_str/config.yml @@ -0,0 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: c-str.sh +expected: c-str.expected +exit_code: 1 diff --git a/tests/script-based-pre/cargo_autoharness_c_str/src/lib.rs b/tests/script-based-pre/cargo_autoharness_c_str/src/lib.rs new file mode 100644 index 00000000000..d1e0c9e8509 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_c_str/src/lib.rs @@ -0,0 +1,38 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that the autoharness subcommand supports `&CStr` arguments. The generated harness +// produces a C string of nondeterministic length, bounded by AUTOHARNESS_SLICE_BOUND (16) less +// the terminating NUL, backed by nondeterministic harness-local storage whose last byte is NUL, +// c.f. the `AnyCStrRef` model. The "TEST NOTE" comments explain the expected result per function. + +use std::ffi::CStr; + +// TEST NOTE: should PASS: the length of a C string of at most 15 bytes fits any usize. +pub fn len(s: &CStr) -> usize { + s.to_bytes().len() +} + +// TEST NOTE: should FAIL: the C string may be empty, so the index may be out of bounds. +pub fn first(s: &CStr) -> u8 { + s.to_bytes()[0] +} + +// TEST NOTE: should PASS: the generated value is a valid C string, so no interior NUL. +pub fn no_interior_nul(s: &CStr) { + assert!(!s.to_bytes().contains(&0)); +} + +// TEST NOTE: should PASS, and the cover checks must be SATISFIED: the empty C string, the +// longest C string, and a specific content are all generated. +pub fn c_str_cover(s: &CStr) { + kani::cover!(s.is_empty(), "empty C string"); + kani::cover!(s.to_bytes().len() == 15, "maximum-length C string"); + kani::cover!(s.to_bytes() == b"ab", "C string \"ab\""); +} + +// TEST NOTE: is skipped: a C string behind a further reference is not supported, as for +// slices, since the backing storage would not outlive the value. +pub fn nested(s: &&CStr) -> usize { + s.to_bytes().len() +} From 00a4c2ab4f4642d6c75070376d9fffcbaae6b5cd Mon Sep 17 00:00:00 2001 From: Srivatsan Samraj <321934658+srivatsansamraj@users.noreply.github.com> Date: Fri, 18 Sep 2026 19:09:00 -0700 Subject: [PATCH 2/4] Autoharness: type the model call's destination by what the model returns 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. --- kani-compiler/src/kani_middle/transform/automatic.rs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index d547f90c1dc..1c3d2a6fc07 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -1262,10 +1262,11 @@ fn call_kani_any_for_ty( InsertPosition::Before, ); let model_inst = Instance::resolve(model, &model_args).unwrap(); - // For `&str`, the model already returns the shared-reference type (there is no - // `&mut str` in practice); for slices it returns `&mut [T]`. + // The slice model returns `&mut [T]`, to serve both mutabilities; the string models + // return the shared reference, since a mutable one is not supported. + let is_slice = matches!(inner_ty.kind(), TyKind::RigidTy(RigidTy::Slice(..))); let model_ret_ty = - if is_str { ty } else { Ty::new_ref(region.clone(), inner_ty, Mutability::Mut) }; + if is_slice { Ty::new_ref(region.clone(), inner_ty, Mutability::Mut) } else { ty }; let slice_lcl = body.new_local(model_ret_ty, source.span(body.blocks()), mutability); body.insert_call( &model_inst, @@ -1275,7 +1276,7 @@ fn call_kani_any_for_ty( Place::from(slice_lcl), ); - if inner_mutability == Mutability::Not && !is_str { + if inner_mutability == Mutability::Not && is_slice { // Reborrow the `&mut [T]` the model returned as `&[T]`. let shared_lcl = body.new_local(ty, source.span(body.blocks()), mutability); body.assign_to( From 9612d4457d8f66fb823d6adb50c7b833b07ac771 Mon Sep 17 00:00:00 2001 From: Srivatsan Samraj <321934658+srivatsansamraj@users.noreply.github.com> Date: Thu, 17 Sep 2026 21:56:56 -0700 Subject: [PATCH 3/4] Autoharness: support `&ByteStr` arguments under --bounded-arguments `&[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. --- .../src/reference/experimental/autoharness.md | 8 ++--- .../src/kani_middle/kani_functions.rs | 2 ++ kani-compiler/src/kani_middle/mod.rs | 22 ++++++++++-- .../src/kani_middle/transform/automatic.rs | 19 +++++++--- library/kani/src/lib.rs | 1 + library/kani_core/src/arbitrary.rs | 16 +++++++++ .../cargo_autoharness_byte_str/Cargo.toml | 10 ++++++ .../byte-str.expected | 15 ++++++++ .../cargo_autoharness_byte_str/byte-str.sh | 15 ++++++++ .../cargo_autoharness_byte_str/config.yml | 5 +++ .../cargo_autoharness_byte_str/src/lib.rs | 35 +++++++++++++++++++ 11 files changed, 137 insertions(+), 11 deletions(-) create mode 100644 tests/script-based-pre/cargo_autoharness_byte_str/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoharness_byte_str/byte-str.expected create mode 100755 tests/script-based-pre/cargo_autoharness_byte_str/byte-str.sh create mode 100644 tests/script-based-pre/cargo_autoharness_byte_str/config.yml create mode 100644 tests/script-based-pre/cargo_autoharness_byte_str/src/lib.rs diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index 3e25fa198f2..b798d4f3c12 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -250,11 +250,11 @@ that use bounded values are marked **"(bounded)"** in the summary table, and a n table repeats the caveat. With `--bounded-arguments`, for a function with `&[T]`/`&mut [T]` arguments (where `T` -implements or can derive `Arbitrary`), `&str` arguments, or `&CStr` arguments, the generated +implements or can derive `Arbitrary`), `&str`, `&CStr` or `&ByteStr` arguments, the generated harness produces a slice of nondeterministic length, backed by nondeterministic storage that -lives for the entire harness: by default **up to 16 elements** for slices, **up to 4 bytes** for -strings, and **up to 15 bytes** plus the terminating NUL for C strings (which follow the slice -bound, less one for the NUL). Strings cover all +lives for the entire harness: by default **up to 16 elements** for slices and byte strings, +**up to 4 bytes** for strings, and **up to 15 bytes** plus the terminating NUL for C strings +(which follow the slice bound, less one for the NUL). Strings cover all valid UTF-8 contents up to the bound (the generated string is the longest valid-UTF-8 prefix of nondeterministic bytes, the same approach as `String`'s `BoundedArbitrary` implementation); the smaller bound reflects the cost of reasoning about UTF-8 for symbolic execution. The bounds are diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 2439e63119f..5b291d9e899 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -93,6 +93,8 @@ pub enum KaniModel { AnyArc, #[strum(serialize = "AnyBoxModel")] AnyBox, + #[strum(serialize = "AnyByteStrRefModel")] + AnyByteStrRef, #[strum(serialize = "AnyCStrRefModel")] AnyCStrRef, #[strum(serialize = "AnyPtrModel")] diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 44a2b9a1eb6..bdf12c18c32 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -1033,6 +1033,19 @@ pub fn is_c_str(tcx: TyCtxt, def: AdtDef) -> bool { == tcx.get_diagnostic_item(rustc_span::sym::cstr_type) } +/// Whether `def` is `core::bstr::ByteStr`, which has no diagnostic item. +/// +/// Shared by the eligibility check and the harness generation, as `is_c_str` is. +pub fn is_byte_str(tcx: TyCtxt, def: AdtDef) -> bool { + let def_id = rustc_internal::internal(tcx, def.def_id()); + tcx.crate_name(def_id.krate) == rustc_span::sym::core + && tcx + .opt_parent(def_id) + .and_then(|module| tcx.opt_item_name(module)) + .is_some_and(|name| name.as_str() == "bstr") + && tcx.item_name(def_id).as_str() == "ByteStr" +} + /// The formatting traits whose implementations automatic harnesses can verify via dedicated /// models (c.f. `KaniModel::CheckDebugFmt`/`CheckDisplayFmt`). #[derive(Copy, Clone, Debug, Eq, PartialEq)] @@ -1231,9 +1244,12 @@ fn autoharness_supported_arg_ty( ArgSupport::Unsupported } } - // A `&CStr` is the bytes of nondeterministic storage up to its first NUL, c.f. - // `any_c_str_ref`. Immutable only, as for `&str`. - TyKind::RigidTy(RigidTy::Adt(def, _)) if is_c_str(tcx, def) => { + // A `&CStr` is the bytes of nondeterministic storage up to its first NUL and a + // `&ByteStr` a prefix of it, c.f. `any_c_str_ref` and `any_byte_str_ref`. Immutable + // only, as for `&str`. + TyKind::RigidTy(RigidTy::Adt(def, _)) + if is_c_str(tcx, def) || is_byte_str(tcx, def) => + { if inner_mutability == Mutability::Not { ArgSupport::Bounded } else { diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 1c3d2a6fc07..2a321f36edd 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -18,7 +18,7 @@ use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_middle::{ CtorReturn, FmtTrait, SmartPointerModels, adt_has_private_field_check, can_derive_arbitrary, find_arbitrary_constructor, fmt_impl_self_ty, implements_arbitrary, implements_invariant, - is_c_str, scalar_niche, smart_pointer_model_instance, + is_byte_str, is_c_str, scalar_niche, smart_pointer_model_instance, }; use crate::kani_queries::QueryDb; use rustc_data_structures::fx::FxHashMap; @@ -53,6 +53,8 @@ struct AnyModels { kani_any_str_ref: FnDef, /// The FnDef of KaniModel::AnyCStrRef kani_any_c_str_ref: FnDef, + /// The FnDef of KaniModel::AnyByteStrRef + kani_any_byte_str_ref: FnDef, /// The FnDef of KaniHook::Assume (used for layout-niche assumptions and constructor /// success). kani_assume: FnDef, @@ -87,6 +89,7 @@ impl AnyModels { kani_any_slice_ref: *kani_fns.get(&KaniModel::AnySliceRef.into()).unwrap(), kani_any_str_ref: *kani_fns.get(&KaniModel::AnyStrRef.into()).unwrap(), kani_any_c_str_ref: *kani_fns.get(&KaniModel::AnyCStrRef.into()).unwrap(), + kani_any_byte_str_ref: *kani_fns.get(&KaniModel::AnyByteStrRef.into()).unwrap(), kani_assume: *kani_fns.get(&KaniHook::Assume.into()).unwrap(), kani_assert: *kani_fns.get(&KaniHook::Assert.into()).unwrap(), kani_assume_safe: *kani_fns.get(&KaniModel::AssumeSafe.into()).unwrap(), @@ -1178,7 +1181,7 @@ fn call_kani_any_for_ty( if let TyKind::RigidTy(RigidTy::Ref(region, inner_ty, inner_mutability)) = ty.kind() && match inner_ty.kind() { TyKind::RigidTy(RigidTy::Slice(..)) | TyKind::RigidTy(RigidTy::Str) => true, - TyKind::RigidTy(RigidTy::Adt(def, _)) => is_c_str(tcx, def), + TyKind::RigidTy(RigidTy::Adt(def, _)) => is_c_str(tcx, def) || is_byte_str(tcx, def), _ => false, } { @@ -1201,14 +1204,22 @@ fn call_kani_any_for_ty( TyConst::try_from_target_usize(models.string_bound).unwrap(), )]), ), - // `&CStr`: bytes up to the first NUL of the storage, sized by the slice bound. - TyKind::RigidTy(RigidTy::Adt(..)) => ( + // `&CStr` is the bytes of the storage up to the first NUL and `&ByteStr` a prefix of + // it; both are sized by the slice bound. + TyKind::RigidTy(RigidTy::Adt(def, _)) if is_c_str(tcx, def) => ( Ty::unsigned_ty(UintTy::U8), models.kani_any_c_str_ref, GenericArgs(vec![GenericArgKind::Const( TyConst::try_from_target_usize(models.slice_bound).unwrap(), )]), ), + TyKind::RigidTy(RigidTy::Adt(..)) => ( + Ty::unsigned_ty(UintTy::U8), + models.kani_any_byte_str_ref, + GenericArgs(vec![GenericArgKind::Const( + TyConst::try_from_target_usize(models.slice_bound).unwrap(), + )]), + ), _ => unreachable!(), }; diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 74c53363d39..fde96712454 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -19,6 +19,7 @@ // `core::mem::{size_of,align_of}_val_raw` are only reached by the `concrete_playback` paths of // the `kani_core` memory models this crate expands. #![cfg_attr(feature = "concrete_playback", feature(layout_for_ptr))] +#![feature(bstr)] #![feature(ptr_metadata)] #![feature(f16)] #![feature(f128)] diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index c02b8d23f16..926a94cf38c 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/library/kani_core/src/arbitrary.rs @@ -259,6 +259,22 @@ macro_rules! generate_arbitrary { core_path::ffi::CStr::from_bytes_until_nul(storage).unwrap() } + /// Generate a byte string referring to a prefix of `storage` of nondeterministic length + /// (at most `N`), as `any_slice_ref` does for `&[u8]`: a `ByteStr` is a `[u8]` with no + /// further invariant. + /// + /// This model is used by the compiler to generate nondeterministic `&ByteStr` arguments + /// for automatic harnesses (`kani autoharness`). Note that any verification result + /// obtained with a bounded value like this one is valid only up to the bound. + #[kanitool::fn_marker = "AnyByteStrRefModel"] + #[inline(never)] + #[doc(hidden)] + pub fn any_byte_str_ref( + storage: &mut [u8; N], + ) -> &core_path::bstr::ByteStr { + core_path::bstr::ByteStr::new(any_slice_ref(storage)) + } + arbitrary_tuple!(A); arbitrary_tuple!(A, B); arbitrary_tuple!(A, B, C); diff --git a/tests/script-based-pre/cargo_autoharness_byte_str/Cargo.toml b/tests/script-based-pre/cargo_autoharness_byte_str/Cargo.toml new file mode 100644 index 00000000000..29f2be0aa3d --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_byte_str/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_byte_str" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoharness_byte_str/byte-str.expected b/tests/script-based-pre/cargo_autoharness_byte_str/byte-str.expected new file mode 100644 index 00000000000..09cda7c5ddf --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_byte_str/byte-str.expected @@ -0,0 +1,15 @@ +[without --bounded-arguments] +| cargo_autoharness_byte_str | byte_str_cover | Requires --bounded-arguments for argument(s) s: &std::bstr::ByteStr | +[with --bounded-arguments] +| cargo_autoharness_byte_str | nested | Missing Arbitrary implementation for argument(s) s: &&std::bstr::ByteStr | +Failed Checks: index out of bounds: the length is less than or equal to the given index +Status: SATISFIED\ +Description: "empty byte string" +Status: SATISFIED\ +Description: "maximum-length byte string" +Status: SATISFIED\ +Description: "byte string "ab"" +| cargo_autoharness_byte_str | byte_str_cover | #[kani::proof] (bounded) | Success | +| cargo_autoharness_byte_str | len | #[kani::proof] (bounded) | Success | +| cargo_autoharness_byte_str | first | #[kani::proof] (bounded) | Failure | +Complete - 2 successfully verified functions, 1 failures, 3 total. diff --git a/tests/script-based-pre/cargo_autoharness_byte_str/byte-str.sh b/tests/script-based-pre/cargo_autoharness_byte_str/byte-str.sh new file mode 100755 index 00000000000..abe44932bef --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_byte_str/byte-str.sh @@ -0,0 +1,15 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eu + +echo "[without --bounded-arguments]" +# Capture the command status explicitly: piping straight into `grep` would mask a +# failure of `cargo kani ... --list` (the pipeline would report grep's status). +list_output=$(cargo kani autoharness -Z autoharness --list 2>&1) +echo "$list_output" | grep -m1 'Requires --bounded-arguments' + +echo "[with --bounded-arguments]" +# This run reports a failure (`first`), so it exits non-zero (see config.yml). +cargo kani autoharness -Z autoharness -Z unstable-options --output-format=regular --bounded-arguments --harness-timeout 5m diff --git a/tests/script-based-pre/cargo_autoharness_byte_str/config.yml b/tests/script-based-pre/cargo_autoharness_byte_str/config.yml new file mode 100644 index 00000000000..67830f7fc1b --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_byte_str/config.yml @@ -0,0 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: byte-str.sh +expected: byte-str.expected +exit_code: 1 diff --git a/tests/script-based-pre/cargo_autoharness_byte_str/src/lib.rs b/tests/script-based-pre/cargo_autoharness_byte_str/src/lib.rs new file mode 100644 index 00000000000..7cb1c9aa879 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_byte_str/src/lib.rs @@ -0,0 +1,35 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that the autoharness subcommand supports `&ByteStr` arguments. The generated harness +// produces a byte string of nondeterministic length, bounded by AUTOHARNESS_SLICE_BOUND (16), +// backed by nondeterministic harness-local storage, c.f. the `AnyByteStrRef` model. The +// "TEST NOTE" comments explain the expected result per function. + +#![feature(bstr)] + +use std::bstr::ByteStr; + +// TEST NOTE: should PASS: the length of a byte string of at most 16 bytes fits any usize. +pub fn len(s: &ByteStr) -> usize { + s.len() +} + +// TEST NOTE: should FAIL: the byte string may be empty, so the index may be out of bounds. +pub fn first(s: &ByteStr) -> u8 { + s[0] +} + +// TEST NOTE: should PASS, and the cover checks must be SATISFIED: the empty byte string, the +// longest byte string, and a specific content are all generated. +pub fn byte_str_cover(s: &ByteStr) { + kani::cover!(s.is_empty(), "empty byte string"); + kani::cover!(s.len() == 16, "maximum-length byte string"); + kani::cover!(&*s == b"ab", "byte string \"ab\""); +} + +// TEST NOTE: is skipped: a byte string behind a further reference is not supported, as for +// slices, since the backing storage would not outlive the value. +pub fn nested(s: &&ByteStr) -> usize { + s.len() +} From f3c66ce2e7a3da95a0a4cabfdc122babec21449e Mon Sep 17 00:00:00 2001 From: Srivatsan Samraj <321934658+srivatsansamraj@users.noreply.github.com> Date: Thu, 17 Sep 2026 23:23:24 -0700 Subject: [PATCH 4/4] Autoharness: support `&Wtf8` arguments under --bounded-arguments `&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. --- .../src/reference/experimental/autoharness.md | 10 +++--- .../src/kani_middle/kani_functions.rs | 2 ++ kani-compiler/src/kani_middle/mod.rs | 21 ++++++++--- .../src/kani_middle/transform/automatic.rs | 28 ++++++++++++--- library/kani/src/lib.rs | 1 + library/kani_core/src/arbitrary.rs | 16 +++++++++ .../cargo_autoharness_wtf8/Cargo.toml | 10 ++++++ .../cargo_autoharness_wtf8/config.yml | 5 +++ .../cargo_autoharness_wtf8/src/lib.rs | 36 +++++++++++++++++++ .../cargo_autoharness_wtf8/wtf8.expected | 15 ++++++++ .../cargo_autoharness_wtf8/wtf8.sh | 15 ++++++++ 11 files changed, 145 insertions(+), 14 deletions(-) create mode 100644 tests/script-based-pre/cargo_autoharness_wtf8/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoharness_wtf8/config.yml create mode 100644 tests/script-based-pre/cargo_autoharness_wtf8/src/lib.rs create mode 100644 tests/script-based-pre/cargo_autoharness_wtf8/wtf8.expected create mode 100755 tests/script-based-pre/cargo_autoharness_wtf8/wtf8.sh diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index b798d4f3c12..f395b477a96 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -250,11 +250,11 @@ that use bounded values are marked **"(bounded)"** in the summary table, and a n table repeats the caveat. With `--bounded-arguments`, for a function with `&[T]`/`&mut [T]` arguments (where `T` -implements or can derive `Arbitrary`), `&str`, `&CStr` or `&ByteStr` arguments, the generated -harness produces a slice of nondeterministic length, backed by nondeterministic storage that -lives for the entire harness: by default **up to 16 elements** for slices and byte strings, -**up to 4 bytes** for strings, and **up to 15 bytes** plus the terminating NUL for C strings -(which follow the slice bound, less one for the NUL). Strings cover all +implements or can derive `Arbitrary`), `&str`, `&CStr`, `&ByteStr` or `&Wtf8` arguments, the +generated harness produces a slice of nondeterministic length, backed by nondeterministic storage +that lives for the entire harness: by default **up to 16 elements** for slices and byte strings, +**up to 4 bytes** for strings and WTF-8 strings, and **up to 15 bytes** plus the terminating NUL +for C strings (which follow the slice bound, less one for the NUL). Strings cover all valid UTF-8 contents up to the bound (the generated string is the longest valid-UTF-8 prefix of nondeterministic bytes, the same approach as `String`'s `BoundedArbitrary` implementation); the smaller bound reflects the cost of reasoning about UTF-8 for symbolic execution. The bounds are diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 5b291d9e899..d47cf6824f8 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -105,6 +105,8 @@ pub enum KaniModel { AnySliceRef, #[strum(serialize = "AnyStrRefModel")] AnyStrRef, + #[strum(serialize = "AnyWtf8RefModel")] + AnyWtf8Ref, #[strum(serialize = "AssumeSafeModel")] AssumeSafe, #[strum(serialize = "BoundedAnyModel")] diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index bdf12c18c32..8351b8b5fd3 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -1046,6 +1046,19 @@ pub fn is_byte_str(tcx: TyCtxt, def: AdtDef) -> bool { && tcx.item_name(def_id).as_str() == "ByteStr" } +/// Whether `def` is `core::wtf8::Wtf8`, which has no diagnostic item. +/// +/// Shared by the eligibility check and the harness generation, as `is_c_str` is. +pub fn is_wtf8(tcx: TyCtxt, def: AdtDef) -> bool { + let def_id = rustc_internal::internal(tcx, def.def_id()); + tcx.crate_name(def_id.krate) == rustc_span::sym::core + && tcx + .opt_parent(def_id) + .and_then(|module| tcx.opt_item_name(module)) + .is_some_and(|name| name.as_str() == "wtf8") + && tcx.item_name(def_id).as_str() == "Wtf8" +} + /// The formatting traits whose implementations automatic harnesses can verify via dedicated /// models (c.f. `KaniModel::CheckDebugFmt`/`CheckDisplayFmt`). #[derive(Copy, Clone, Debug, Eq, PartialEq)] @@ -1244,11 +1257,11 @@ fn autoharness_supported_arg_ty( ArgSupport::Unsupported } } - // A `&CStr` is the bytes of nondeterministic storage up to its first NUL and a - // `&ByteStr` a prefix of it, c.f. `any_c_str_ref` and `any_byte_str_ref`. Immutable - // only, as for `&str`. + // A `&CStr` is the bytes of nondeterministic storage up to its first NUL, a + // `&ByteStr` a prefix of it and a `&Wtf8` a `&str` over it, c.f. `any_c_str_ref`, + // `any_byte_str_ref` and `any_wtf8_ref`. Immutable only, as for `&str`. TyKind::RigidTy(RigidTy::Adt(def, _)) - if is_c_str(tcx, def) || is_byte_str(tcx, def) => + if is_c_str(tcx, def) || is_byte_str(tcx, def) || is_wtf8(tcx, def) => { if inner_mutability == Mutability::Not { ArgSupport::Bounded diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 2a321f36edd..1332e37df06 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -18,7 +18,7 @@ use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_middle::{ CtorReturn, FmtTrait, SmartPointerModels, adt_has_private_field_check, can_derive_arbitrary, find_arbitrary_constructor, fmt_impl_self_ty, implements_arbitrary, implements_invariant, - is_byte_str, is_c_str, scalar_niche, smart_pointer_model_instance, + is_byte_str, is_c_str, is_wtf8, scalar_niche, smart_pointer_model_instance, }; use crate::kani_queries::QueryDb; use rustc_data_structures::fx::FxHashMap; @@ -55,6 +55,8 @@ struct AnyModels { kani_any_c_str_ref: FnDef, /// The FnDef of KaniModel::AnyByteStrRef kani_any_byte_str_ref: FnDef, + /// The FnDef of KaniModel::AnyWtf8Ref + kani_any_wtf8_ref: FnDef, /// The FnDef of KaniHook::Assume (used for layout-niche assumptions and constructor /// success). kani_assume: FnDef, @@ -90,6 +92,7 @@ impl AnyModels { kani_any_str_ref: *kani_fns.get(&KaniModel::AnyStrRef.into()).unwrap(), kani_any_c_str_ref: *kani_fns.get(&KaniModel::AnyCStrRef.into()).unwrap(), kani_any_byte_str_ref: *kani_fns.get(&KaniModel::AnyByteStrRef.into()).unwrap(), + kani_any_wtf8_ref: *kani_fns.get(&KaniModel::AnyWtf8Ref.into()).unwrap(), kani_assume: *kani_fns.get(&KaniHook::Assume.into()).unwrap(), kani_assert: *kani_fns.get(&KaniHook::Assert.into()).unwrap(), kani_assume_safe: *kani_fns.get(&KaniModel::AssumeSafe.into()).unwrap(), @@ -1181,11 +1184,18 @@ fn call_kani_any_for_ty( if let TyKind::RigidTy(RigidTy::Ref(region, inner_ty, inner_mutability)) = ty.kind() && match inner_ty.kind() { TyKind::RigidTy(RigidTy::Slice(..)) | TyKind::RigidTy(RigidTy::Str) => true, - TyKind::RigidTy(RigidTy::Adt(def, _)) => is_c_str(tcx, def) || is_byte_str(tcx, def), + TyKind::RigidTy(RigidTy::Adt(def, _)) => { + is_c_str(tcx, def) || is_byte_str(tcx, def) || is_wtf8(tcx, def) + } _ => false, } { - let is_str = matches!(inner_ty.kind(), TyKind::RigidTy(RigidTy::Str)); + // A `&Wtf8` is generated as a `&str` and handled as one below. + let is_str = match inner_ty.kind() { + TyKind::RigidTy(RigidTy::Str) => true, + TyKind::RigidTy(RigidTy::Adt(def, _)) => is_wtf8(tcx, def), + _ => false, + }; let (elem_ty, model, model_args) = match inner_ty.kind() { TyKind::RigidTy(RigidTy::Slice(elem_ty)) => ( elem_ty, @@ -1205,7 +1215,8 @@ fn call_kani_any_for_ty( )]), ), // `&CStr` is the bytes of the storage up to the first NUL and `&ByteStr` a prefix of - // it; both are sized by the slice bound. + // it; both are sized by the slice bound. `&Wtf8` is a `&str` over the storage and is + // sized by the string bound. TyKind::RigidTy(RigidTy::Adt(def, _)) if is_c_str(tcx, def) => ( Ty::unsigned_ty(UintTy::U8), models.kani_any_c_str_ref, @@ -1213,13 +1224,20 @@ fn call_kani_any_for_ty( TyConst::try_from_target_usize(models.slice_bound).unwrap(), )]), ), - TyKind::RigidTy(RigidTy::Adt(..)) => ( + TyKind::RigidTy(RigidTy::Adt(def, _)) if is_byte_str(tcx, def) => ( Ty::unsigned_ty(UintTy::U8), models.kani_any_byte_str_ref, GenericArgs(vec![GenericArgKind::Const( TyConst::try_from_target_usize(models.slice_bound).unwrap(), )]), ), + TyKind::RigidTy(RigidTy::Adt(..)) => ( + Ty::unsigned_ty(UintTy::U8), + models.kani_any_wtf8_ref, + GenericArgs(vec![GenericArgKind::Const( + TyConst::try_from_target_usize(models.string_bound).unwrap(), + )]), + ), _ => unreachable!(), }; diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index fde96712454..3926affd5fd 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -20,6 +20,7 @@ // the `kani_core` memory models this crate expands. #![cfg_attr(feature = "concrete_playback", feature(layout_for_ptr))] #![feature(bstr)] +#![feature(wtf8_internals)] #![feature(ptr_metadata)] #![feature(f16)] #![feature(f128)] diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index 926a94cf38c..65aaa7995f9 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/library/kani_core/src/arbitrary.rs @@ -275,6 +275,22 @@ macro_rules! generate_arbitrary { core_path::bstr::ByteStr::new(any_slice_ref(storage)) } + /// Generate a WTF-8 string referring to a prefix of `storage` of nondeterministic length + /// (at most `N`), through `any_str_ref`: WTF-8 is a superset of UTF-8, so every `&str` + /// converts with `Wtf8::from_str`. Strings holding surrogate code points, which only + /// WTF-8 admits, are not generated. + /// + /// This model is used by the compiler to generate nondeterministic `&Wtf8` arguments for + /// automatic harnesses (`kani autoharness`). Note that any verification result obtained + /// with a bounded value like this one is valid only up to the bound. + #[kanitool::fn_marker = "AnyWtf8RefModel"] + #[inline(never)] + #[doc(hidden)] + // `std` does not re-export `core::wtf8`, so the type is named through `core` in both arms. + pub fn any_wtf8_ref(storage: &mut [u8; N]) -> &core::wtf8::Wtf8 { + core::wtf8::Wtf8::from_str(any_str_ref(storage)) + } + arbitrary_tuple!(A); arbitrary_tuple!(A, B); arbitrary_tuple!(A, B, C); diff --git a/tests/script-based-pre/cargo_autoharness_wtf8/Cargo.toml b/tests/script-based-pre/cargo_autoharness_wtf8/Cargo.toml new file mode 100644 index 00000000000..e402d35c9da --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_wtf8/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_wtf8" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoharness_wtf8/config.yml b/tests/script-based-pre/cargo_autoharness_wtf8/config.yml new file mode 100644 index 00000000000..e2ed2bcc4c4 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_wtf8/config.yml @@ -0,0 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: wtf8.sh +expected: wtf8.expected +exit_code: 1 diff --git a/tests/script-based-pre/cargo_autoharness_wtf8/src/lib.rs b/tests/script-based-pre/cargo_autoharness_wtf8/src/lib.rs new file mode 100644 index 00000000000..f3eee01b104 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_wtf8/src/lib.rs @@ -0,0 +1,36 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that the autoharness subcommand supports `&Wtf8` arguments. The generated harness +// produces a WTF-8 string of nondeterministic length, bounded by AUTOHARNESS_STRING_BOUND (4), +// backed by nondeterministic harness-local storage, c.f. the `AnyWtf8Ref` model. The +// "TEST NOTE" comments explain the expected result per function. + +#![feature(wtf8_internals)] +#![allow(internal_features)] + +use core::wtf8::Wtf8; + +// TEST NOTE: should PASS: the length of a string of at most 4 bytes fits any usize. +pub fn len(s: &Wtf8) -> usize { + s.len() +} + +// TEST NOTE: should FAIL: the string may be empty, so the index may be out of bounds. +pub fn first(s: &Wtf8) -> u8 { + s.as_bytes()[0] +} + +// TEST NOTE: should PASS, and the cover checks must be SATISFIED: the empty string, the longest +// string, and a specific content are all generated. +pub fn wtf8_cover(s: &Wtf8) { + kani::cover!(s.is_empty(), "empty string"); + kani::cover!(s.len() == 4, "maximum-length string"); + kani::cover!(s.as_bytes() == b"ab", "string \"ab\""); +} + +// TEST NOTE: is skipped: a string behind a further reference is not supported, as for slices, +// since the backing storage would not outlive the value. +pub fn nested(s: &&Wtf8) -> usize { + s.len() +} diff --git a/tests/script-based-pre/cargo_autoharness_wtf8/wtf8.expected b/tests/script-based-pre/cargo_autoharness_wtf8/wtf8.expected new file mode 100644 index 00000000000..d112f8e616f --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_wtf8/wtf8.expected @@ -0,0 +1,15 @@ +[without --bounded-arguments] +| cargo_autoharness_wtf8 | first | Requires --bounded-arguments for argument(s) s: &core::wtf8::Wtf8 | +[with --bounded-arguments] +| cargo_autoharness_wtf8 | nested | Missing Arbitrary implementation for argument(s) s: &&core::wtf8::Wtf8 | +Failed Checks: index out of bounds: the length is less than or equal to the given index +Status: SATISFIED\ +Description: "empty string" +Status: SATISFIED\ +Description: "maximum-length string" +Status: SATISFIED\ +Description: "string "ab"" +| cargo_autoharness_wtf8 | len | #[kani::proof] (bounded) | Success | +| cargo_autoharness_wtf8 | first | #[kani::proof] (bounded) | Failure | +| cargo_autoharness_wtf8 | wtf8_cover | #[kani::proof] (bounded) | Success | +Complete - 2 successfully verified functions, 1 failures, 3 total. diff --git a/tests/script-based-pre/cargo_autoharness_wtf8/wtf8.sh b/tests/script-based-pre/cargo_autoharness_wtf8/wtf8.sh new file mode 100755 index 00000000000..abe44932bef --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_wtf8/wtf8.sh @@ -0,0 +1,15 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eu + +echo "[without --bounded-arguments]" +# Capture the command status explicitly: piping straight into `grep` would mask a +# failure of `cargo kani ... --list` (the pipeline would report grep's status). +list_output=$(cargo kani autoharness -Z autoharness --list 2>&1) +echo "$list_output" | grep -m1 'Requires --bounded-arguments' + +echo "[with --bounded-arguments]" +# This run reports a failure (`first`), so it exits non-zero (see config.yml). +cargo kani autoharness -Z autoharness -Z unstable-options --output-format=regular --bounded-arguments --harness-timeout 5m