Autoharness: unbounded slice, mutable slice and Vec arguments

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -925,6 +925,94 @@ impl GotocHook for LoopInvariantRegister {
     }
 }
 
+/// Lower `kani::slice_validity_assume::<T>(ptr, len)` (KaniHook::SliceValidityAssume) to a
+/// quantified assumption constraining every element's raw bits to `T`'s layout niche:
+/// `assume(forall i. i < len ==> lo <= *(uN*)ptr + i <= hi)` (wrapping ranges use `||`).
+/// A no-op for element types without a niche (every bit pattern valid).
+///
+/// This is lowered directly to pure goto expressions rather than through `kani::forall!`:
+/// the closure-based quantifier lowering cannot substitute bodies containing checked
+/// arithmetic or bounds checks (it falls back to an unconstrained predicate), whereas the
+/// expressions built here are side-effect-free by construction.
+struct SliceValidityAssume;
+impl GotocHook for SliceValidityAssume {
+    fn hook_applies(
+        &self,
+        _tcx: TyCtxt,
+        _instance: Instance,
+        _instance_name: &str,
+        _kani_tool_attr: Option<&String>,
+    ) -> bool {
+        unreachable!("{UNEXPECTED_CALL}")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        instance: Instance,
+        mut fargs: Vec<Expr>,
+        _assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 2);
+        let loc = gcx.codegen_span_stable(span);
+        let target = target.unwrap();
+        let goto_target = Stmt::goto(bb_label(target), loc);
+
+        let elem_ty = instance.args().0[0].expect_ty().to_owned();
+        let Some(niche) = crate::kani_middle::scalar_niche(gcx.tcx, elem_ty) else {
+            // Every bit pattern is valid: nothing to assume.
+            return goto_target;
+        };
+        let len = fargs.remove(1);
+        let ptr = fargs.remove(0);
+
+        // Fresh quantified variable of the same type as `len`.
+        let base_name = "kani_slice_validity_var".to_string();
+        let mut counter = 0;
+        let mut unique_name = format!("{base_name}_{counter}");
+        while gcx.symbol_table.lookup(&unique_name).is_some() {
+            counter += 1;
+            unique_name = format!("{base_name}_{counter}");
+        }
+        let qvar = {
+            let sym =
+                GotoSymbol::variable(unique_name.clone(), unique_name, len.typ().clone(), loc);
+            gcx.symbol_table.insert(sym.clone());
+            sym.to_expr()
+        };
+
+        // CBMC's quantifier handling binds byte-granularity dereferences reliably, but not
+        // wider ones (byte_extract at a symbolic index under a forall does not propagate),
+        // so the validity predicate is expressed over bytes:
+        // - 8-bit niches (bool, u8-based ranged types): direct range check on the byte;
+        // - NonZero-style niches (excluded zero, full top): OR over "some byte nonzero".
+        // Wider general ranges are not byte-decomposable this simply; the element classifier
+        // (kani_middle::slice_elem_unbounded_ok) never routes such types to this hook.
+        let byte_ty = Type::unsigned_int(8u64);
+        let byte_ptr = ptr.clone().cast_to(byte_ty.clone().to_pointer());
+        let valid = if niche.bits == 8 {
+            let elem = byte_ptr.plus(qvar.clone()).dereference();
+            let lo = Expr::int_constant(niche.start, byte_ty.clone());
+            let hi = Expr::int_constant(niche.end, byte_ty.clone());
+            if niche.start <= niche.end {
+                lo.le(elem.clone()).and(elem.le(hi))
+            } else {
+                lo.le(elem.clone()).or(elem.le(hi))
+            }
+        } else {
+            unreachable!(
+                "slice_validity_assume: element type with non-byte-decomposable niche                  should have been rejected by the classifier"
+            )
+        };
+        let domain = qvar.clone().lt(len).implies(valid);
+        let quantified = Expr::forall_expr(Type::Bool, qvar, domain);
+
+        Stmt::block(vec![gcx.codegen_assume(quantified, loc), goto_target], loc)
+    }
+}
+
 struct Forall;
 struct Exists;
 
@@ -1365,6 +1453,7 @@ pub fn fn_hooks() -> GotocHooks {
     let kani_lib_hooks = [
         (KaniHook::Assert, Rc::new(Assert) as Rc<dyn GotocHook>),
         (KaniHook::Assume, Rc::new(Assume)),
+        (KaniHook::SliceValidityAssume, Rc::new(SliceValidityAssume)),
         (KaniHook::Exists, Rc::new(Exists)),
         (KaniHook::Forall, Rc::new(Forall)),
         (KaniHook::Panic, Rc::new(Panic)),

kani-compiler/src/kani_middle/codegen_units.rs

@@ -113,6 +113,19 @@ impl CodegenUnits {
                     *kani_fns.get(&KaniModel::Any.into()).unwrap(),
                     *kani_fns.get(&KaniModel::BoundedAny.into()).unwrap(),
                     SmartPointerModels::from_kani_functions(kani_fns),
+                    // Require *all three* unbounded models: eligibility admits `&[T]`, `&mut [T]`
+                    // and `Vec<T>`, but generation resolves each model independently, so gating on
+                    // only one could report a `&mut [T]`/`Vec<T>` arg as unbounded-verified while
+                    // generation silently fell back to a bounded (or unsupported) path. They are
+                    // defined together (all present with `alloc`, all absent in `no_core`), so this
+                    // is all-or-nothing in practice; the conjunction just makes that explicit.
+                    [
+                        KaniModel::AnySliceRefUnbounded,
+                        KaniModel::AnySliceMutUnbounded,
+                        KaniModel::AnyVecUnbounded,
+                    ]
+                    .iter()
+                    .all(|m| kani_fns.contains_key(&(*m).into())),
                 );
                 AUTOHARNESS_MD
                     .set(AutoHarnessMetadata {
@@ -685,6 +698,7 @@ fn automatic_harness_partition(
     kani_any_def: FnDef,
     kani_bounded_any_def: FnDef,
     smart_pointer_models: SmartPointerModels,
+    unbounded_slice_available: bool,
 ) -> (Vec<(Instance, AutoHarnessCaveats)>, BTreeMap<String, AutoHarnessSkipReason>) {
     let crate_fn_defs = rustc_public::local_crate().fn_defs().into_iter().collect::<FxHashSet<_>>();
     // Filter out CrateItems that are functions, but not functions defined in the crate itself, i.e., rustc-inserted functions
@@ -766,6 +780,26 @@ fn automatic_harness_partition(
         let mut problematic_args = vec![];
         let mut bounded_args = vec![];
         for (idx, arg) in body.arg_locals().iter().enumerate() {
+            // Unbounded generation: slices (&[T], &mut [T]) and Vec<T> of primitive
+            // integer/float elements are generated as fresh allocations of nondeterministic
+            // size (results hold for *all* lengths -- unbounded, so no bound caveat), when the
+            // optional alloc-requiring models are present. This takes precedence over the
+            // bounded slice/string support classified by `autoharness_supported_arg_ty`.
+            if unbounded_slice_available {
+                let slice_ok = match arg.ty.kind() {
+                    TyKind::RigidTy(RigidTy::Ref(_, inner, _)) => match inner.kind() {
+                        TyKind::RigidTy(RigidTy::Slice(elem)) => {
+                            crate::kani_middle::slice_elem_unbounded_ok(tcx, elem)
+                        }
+                        _ => false,
+                    },
+                    _ => crate::kani_middle::vec_elem_ty(arg.ty)
+                        .is_some_and(|elem| crate::kani_middle::slice_elem_unbounded_ok(tcx, elem)),
+                };
+                if slice_ok {
+                    continue;
+                }
+            }
             // Note: we deliberately do not insert the verdict into `ty_arbitrary_cache` here.
             // The cache stores whether a type implements (or can derive) Arbitrary, which is the
             // wrong semantics for types that are supported in argument position only (raw

kani-compiler/src/kani_middle/kani_functions.rs

@@ -65,6 +65,12 @@ pub enum KaniModel {
     AlignOfDynObject,
     #[strum(serialize = "AlignOfValRawModel")]
     AlignOfVal,
+    #[strum(serialize = "AnySliceMutUnboundedModel")]
+    AnySliceMutUnbounded,
+    #[strum(serialize = "AnySliceRefUnboundedModel")]
+    AnySliceRefUnbounded,
+    #[strum(serialize = "AnyVecUnboundedModel")]
+    AnyVecUnbounded,
     #[strum(serialize = "AnyModel")]
     Any,
     #[strum(serialize = "AnyArcModel")]
@@ -157,6 +163,8 @@ pub enum KaniHook {
     AnyRaw,
     #[strum(serialize = "AssertHook")]
     Assert,
+    #[strum(serialize = "SliceValidityAssumeHook")]
+    SliceValidityAssume,
     #[strum(serialize = "AssumeHook")]
     Assume,
     #[strum(serialize = "CheckHook")]
@@ -191,11 +199,19 @@ pub enum KaniHook {
 }
 
 impl KaniModel {
-    /// Whether this model may legitimately be absent. The smart-pointer models require `alloc`
-    /// and are only defined in the `kani` library, not in `core::kani` (the `no_core` flow used
-    /// by `kani verify-std`). Code retrieving optional models must handle their absence.
+    /// Whether this model may legitimately be absent. These models require `alloc` and are
+    /// only defined in the `kani` library, not in `core::kani` (the `no_core` flow used by
+    /// `kani verify-std`). Code retrieving optional models must handle their absence.
     pub fn is_optional(&self) -> bool {
-        matches!(self, KaniModel::AnyArc | KaniModel::AnyBox | KaniModel::AnyRc)
+        matches!(
+            self,
+            KaniModel::AnyArc
+                | KaniModel::AnyBox
+                | KaniModel::AnyRc
+                | KaniModel::AnySliceMutUnbounded
+                | KaniModel::AnySliceRefUnbounded
+                | KaniModel::AnyVecUnbounded
+        )
     }
 }
 

kani-compiler/src/kani_middle/mod.rs

@@ -630,6 +630,61 @@ fn to_fn_def(tcx: TyCtxt, def_id: rustc_span::def_id::DefId) -> Option<FnDef> {
     }
 }
 
+/// If `ty` is `Vec<T>` with the default allocator, return `T`.
+pub fn vec_elem_ty(ty: Ty) -> Option<Ty> {
+    let TyKind::RigidTy(RigidTy::Adt(def, ref args)) = ty.kind() else { return None };
+    let name = def.name();
+    if name != "std::vec::Vec" && name != "alloc::vec::Vec" {
+        return None;
+    }
+    // Vec<T, A = Global>: only the default allocator is supported (the model allocates via
+    // the global allocator). The allocator parameter is defaulted, so a crate naming a
+    // custom allocator produces a second type argument != Global.
+    let mut ty_args = args.0.iter().filter_map(|a| match a {
+        GenericArgKind::Type(t) => Some(*t),
+        _ => None,
+    });
+    let elem = ty_args.next()?;
+    // Only the default `Global` allocator is supported. Match the allocator type exactly rather
+    // than by substring, so a custom allocator whose name merely contains "Global" (e.g.
+    // `MyGlobalAlloc`) is not misclassified as the default.
+    if let Some(alloc_ty) = ty_args.next() {
+        let is_global = matches!(
+            alloc_ty.kind(),
+            TyKind::RigidTy(RigidTy::Adt(def, _))
+                if matches!(def.name().as_str(), "std::alloc::Global" | "alloc::alloc::Global")
+        );
+        if !is_global {
+            return None;
+        }
+    }
+    Some(elem)
+}
+
+/// Whether `&[T]` arguments with this element type qualify for *unbounded* generation
+/// (`KaniModel::AnySliceRefUnbounded`): raw nondeterministic memory must be a sound AND
+/// complete model of the element's values *without any validity assumption*, i.e. every bit
+/// pattern must be a valid element. This holds exactly for the primitive integer and float
+/// types.
+///
+/// Types with validity constraints (bool, char, NonZero, ranged newtypes) are excluded even
+/// though the `SliceValidityAssume` hook can express byte-width niche constraints: CBMC's
+/// default (SAT) backend only instantiates quantifiers with *constant* bounds, and silently
+/// degrades symbolic-bound quantifiers to unconstrained free variables
+/// (`boolbvt::finish_eager_conversion_quantifiers` -> `conversion_failed`), which would make
+/// the validity assumption vacuous. SMT backends (e.g. `--solver z3`) handle the quantified
+/// assumption, including multi-byte elements; routing niched element types here can be
+/// revisited when CBMC's SAT backend learns symbolic-bound instantiation or Kani selects
+/// backends per harness.
+pub fn slice_elem_unbounded_ok(_tcx: TyCtxt, ty: Ty) -> bool {
+    matches!(
+        ty.kind(),
+        TyKind::RigidTy(RigidTy::Int(_))
+            | TyKind::RigidTy(RigidTy::Uint(_))
+            | TyKind::RigidTy(RigidTy::Float(_))
+    )
+}
+
 /// The niche constraint of a scalar-ABI type: the width of the scalar in bits, and the
 /// (possibly wrapping) inclusive range of valid bit patterns.
 /// Returns None for non-scalar ABIs, pointer/float scalars, and scalars whose valid range

kani-compiler/src/kani_middle/transform/automatic.rs

@@ -9,7 +9,7 @@
 use crate::args::ReachabilityType;
 use crate::kani_middle::attributes::KaniAttributes;
 use crate::kani_middle::codegen_units::CodegenUnit;
-use crate::kani_middle::kani_functions::{KaniHook, KaniIntrinsic, KaniModel};
+use crate::kani_middle::kani_functions::{KaniFunction, KaniHook, KaniIntrinsic, KaniModel};
 use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction};
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_middle::{
@@ -60,6 +60,8 @@ struct AnyModels {
     kani_bounded_any: FnDef,
     /// The (optional) smart-pointer generation models (`Box`/`Rc`/`Arc`).
     smart_pointer_models: SmartPointerModels,
+    /// The (optional, alloc-requiring) unbounded slice/`Vec` generation models.
+    unbounded_models: UnboundedModels,
 }
 
 impl AnyModels {
@@ -75,6 +77,7 @@ impl AnyModels {
             kani_assume_safe: *kani_fns.get(&KaniModel::AssumeSafe.into()).unwrap(),
             kani_bounded_any: *kani_fns.get(&KaniModel::BoundedAny.into()).unwrap(),
             smart_pointer_models: SmartPointerModels::from_kani_functions(kani_fns),
+            unbounded_models: UnboundedModels::from_kani_functions(kani_fns),
         }
     }
 }
@@ -753,6 +756,55 @@ fn assume_scalar_niche(
     );
 }
 
+/// The (optional, alloc-requiring) unbounded generation models, resolved per argument type.
+#[derive(Debug, Clone, Copy, Default)]
+pub struct UnboundedModels {
+    slice_ref: Option<FnDef>,
+    slice_mut: Option<FnDef>,
+    vec: Option<FnDef>,
+}
+
+impl UnboundedModels {
+    pub fn from_kani_functions(kani_fns: &std::collections::HashMap<KaniFunction, FnDef>) -> Self {
+        UnboundedModels {
+            slice_ref: kani_fns.get(&KaniModel::AnySliceRefUnbounded.into()).copied(),
+            slice_mut: kani_fns.get(&KaniModel::AnySliceMutUnbounded.into()).copied(),
+            vec: kani_fns.get(&KaniModel::AnyVecUnbounded.into()).copied(),
+        }
+    }
+
+    /// The model instance generating `ty` unbounded, if `ty` qualifies.
+    fn instance_for(&self, tcx: TyCtxt, ty: Ty) -> Option<Instance> {
+        let (def, elem) = match ty.kind() {
+            TyKind::RigidTy(RigidTy::Ref(_, inner, mutability)) => match inner.kind() {
+                TyKind::RigidTy(RigidTy::Slice(elem))
+                    if crate::kani_middle::slice_elem_unbounded_ok(tcx, elem) =>
+                {
+                    let def =
+                        if mutability == Mutability::Not { self.slice_ref } else { self.slice_mut };
+                    (def?, elem)
+                }
+                _ => return None,
+            },
+            _ => {
+                let elem = crate::kani_middle::vec_elem_ty(ty)?;
+                if !crate::kani_middle::slice_elem_unbounded_ok(tcx, elem) {
+                    return None;
+                }
+                (self.vec?, elem)
+            }
+        };
+        let instance =
+            Instance::resolve(def, &GenericArgs(vec![GenericArgKind::Type(elem)])).ok()?;
+        // Only use the model if its return type matches `ty` exactly (mirrors
+        // `smart_pointer_model_instance`): guards against generating an ill-typed value if the
+        // model's signature ever skews from the argument type (e.g. a `Vec<T, A>` with a
+        // non-`Global` allocator that slipped past `vec_elem_ty`).
+        let ret_ty = instance.ty().kind().fn_sig()?.skip_binder().output();
+        (ret_ty == ty).then_some(instance)
+    }
+}
+
 fn call_kani_any_for_ty(
     tcx: TyCtxt,
     models: AnyModels,
@@ -762,6 +814,14 @@ fn call_kani_any_for_ty(
     source: &mut SourceInstruction,
     invariant_cache: &mut FxHashMap<Ty, bool>,
 ) -> Local {
+    // Unbounded generation for slices (&[T]/&mut [T]) and Vec<T> of primitive
+    // integer/float elements: fresh allocations of nondeterministic size, so results hold
+    // for all lengths (mirrors the eligibility decision in automatic_harness_partition).
+    if let Some(model_inst) = models.unbounded_models.instance_for(tcx, ty) {
+        let lcl = body.new_local(ty, source.span(body.blocks()), mutability);
+        body.insert_call(&model_inst, source, InsertPosition::Before, vec![], Place::from(lcl));
+        return lcl;
+    }
     if let TyKind::RigidTy(RigidTy::Ref(region, inner_ty, inner_mutability)) = ty.kind()
         && matches!(
             inner_ty.kind(),

library/kani/build.rs

@@ -4,4 +4,8 @@
 fn main() {
     // Make sure `kani_sysroot` is a recognized config
     println!("cargo::rustc-check-cfg=cfg(kani_sysroot)");
+    // `kani` is set by the Kani compiler when verifying user code; recognize it here so that
+    // verification-only hook bodies can gate on `cfg(not(kani))` without tripping the
+    // `unexpected_cfgs` lint during the library's own build.
+    println!("cargo::rustc-check-cfg=cfg(kani)");
 }