Autoharness: support &Wtf8 arguments under --bounded-arguments

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`, `&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

kani-compiler/src/kani_middle/kani_functions.rs

@@ -93,6 +93,10 @@ pub enum KaniModel {
     AnyArc,
     #[strum(serialize = "AnyBoxModel")]
     AnyBox,
+    #[strum(serialize = "AnyByteStrRefModel")]
+    AnyByteStrRef,
+    #[strum(serialize = "AnyCStrRefModel")]
+    AnyCStrRef,
     #[strum(serialize = "AnyPtrModel")]
     AnyPtr,
     #[strum(serialize = "AnyRcModel")]
@@ -101,6 +105,8 @@ pub enum KaniModel {
     AnySliceRef,
     #[strum(serialize = "AnyStrRefModel")]
     AnyStrRef,
+    #[strum(serialize = "AnyWtf8RefModel")]
+    AnyWtf8Ref,
     #[strum(serialize = "AssumeSafeModel")]
     AssumeSafe,
     #[strum(serialize = "BoundedAnyModel")]

kani-compiler/src/kani_middle/mod.rs

@@ -1024,6 +1024,41 @@ 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)
+}
+
+/// 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"
+}
+
+/// 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)]
@@ -1222,6 +1257,18 @@ fn autoharness_supported_arg_ty(
                     ArgSupport::Unsupported
                 }
             }
+            // 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) || is_wtf8(tcx, def) =>
+            {
+                if inner_mutability == Mutability::Not {
+                    ArgSupport::Bounded
+                } else {
+                    ArgSupport::Unsupported
+                }
+            }
             _ => arbitrary_or_derive(ty, ty_arbitrary_cache),
         }
     } else {

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_byte_str, is_c_str, is_wtf8, scalar_niche, smart_pointer_model_instance,
 };
 use crate::kani_queries::QueryDb;
 use rustc_data_structures::fx::FxHashMap;
@@ -51,6 +51,12 @@ 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 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,
@@ -84,6 +90,9 @@ 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_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(),
@@ -1173,12 +1182,20 @@ 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) || 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,
@@ -1197,6 +1214,30 @@ fn call_kani_any_for_ty(
                     TyConst::try_from_target_usize(models.string_bound).unwrap(),
                 )]),
             ),
+            // `&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. `&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,
+                GenericArgs(vec![GenericArgKind::Const(
+                    TyConst::try_from_target_usize(models.slice_bound).unwrap(),
+                )]),
+            ),
+            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!(),
         };
 
@@ -1250,10 +1291,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,
@@ -1263,7 +1305,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(

library/kani/src/lib.rs

@@ -19,6 +19,8 @@
 // `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(wtf8_internals)]
 #![feature(ptr_metadata)]
 #![feature(f16)]
 #![feature(f128)]

library/kani_core/src/arbitrary.rs

@@ -241,6 +241,56 @@ 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<const N: usize>(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()
+        }
+
+        /// 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<const N: usize>(
+            storage: &mut [u8; N],
+        ) -> &core_path::bstr::ByteStr {
+            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<const N: usize>(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);

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)'] }

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.

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

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

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()
+}

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)'] }

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.