From 00e514b579399736f60c0f3473ddfaea704a3adb Mon Sep 17 00:00:00 2001 From: Felipe Monteiro Date: Fri, 21 Aug 2026 20:26:40 +0000 Subject: [PATCH] Fix write_any_slice resolution for slice modifies stubs (#4748) When a function contract modifies a whole slice (e.g. `#[kani::modifies(x)]` with `x: &mut [u8]`) and the contract is used as a verified stub via `#[kani::stub_verified]`, the compiler crashed while collecting reachable items: Failed to resolve `into_iter` with `GenericArgs([Ref(Slice(Slice(U8)), Mut)])` The `AnyModifiesPass` rewrites the `write_any` marker into one of `write_any_slim`/`write_any_slice`/`write_any_str` depending on the pointee type. For the slice case it resolved `write_any_slice(slice: *mut [T])` using the marker's `instance_args`, which hold the *pointee* type `[T]` rather than the element type `T`. This produced `write_any_slice<[T]>` with argument `*mut [[T]]` (a doubled slice), whose `fill_with` body then failed to resolve. Resolve `write_any_slice` with the slice's element type instead. This path is only exercised in replace mode (`stub_verified`), which is why `proof_for_contract` harnesses were unaffected and the existing `modifies_fat_pointer` tests did not catch it. Resolves: https://github.com/model-checking/kani/issues/4748 --- .../src/kani_middle/transform/contracts.rs | 15 ++++++---- .../slice_replace.expected | 7 +++++ .../modifies_fat_pointer/slice_replace.rs | 29 +++++++++++++++++++ 3 files changed, 46 insertions(+), 5 deletions(-) create mode 100644 tests/expected/function-contract/modifies_fat_pointer/slice_replace.expected create mode 100644 tests/expected/function-contract/modifies_fat_pointer/slice_replace.rs diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 4669f79e8fff..f82e3523a7c2 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -18,7 +18,8 @@ use rustc_public::mir::{ }; use rustc_public::rustc_internal; use rustc_public::ty::{ - ClosureDef, FnDef, GenericArgs, MirConst, RigidTy, Ty, TyKind, TypeAndMut, UintTy, + ClosureDef, FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyKind, TypeAndMut, + UintTy, }; use rustc_span::Symbol; use std::collections::HashSet; @@ -135,11 +136,15 @@ impl AnyModifiesPass { fn_sig.skip_binder().inputs()[0].kind().builtin_deref(true) { // case on the type of the input - if let TyKind::RigidTy(RigidTy::Slice(_)) = internal_type.kind() { - //if the input is a slice, use write_any_slice + if let TyKind::RigidTy(RigidTy::Slice(elem_ty)) = internal_type.kind() { + //if the input is a slice `[T]`, use write_any_slice. Note that + //`write_any_slice(slice: *mut [T])` is generic over the *element* type + //`T`, whereas `instance_args` holds the pointee type `[T]`. Resolving with + //`instance_args` here would incorrectly produce `write_any_slice<[T]>` + //(i.e. a `*mut [[T]]`), so we resolve with the element type instead. + let elem_args = GenericArgs(vec![GenericArgKind::Type(elem_ty)]); let instance = - Instance::resolve(self.kani_write_any_slice.unwrap(), &instance_args) - .unwrap(); + Instance::resolve(self.kani_write_any_slice.unwrap(), &elem_args).unwrap(); let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); let span = bb.terminator.span; let new_func = ConstOperand { span, user_ty: None, const_: literal }; diff --git a/tests/expected/function-contract/modifies_fat_pointer/slice_replace.expected b/tests/expected/function-contract/modifies_fat_pointer/slice_replace.expected new file mode 100644 index 000000000000..7d918117e015 --- /dev/null +++ b/tests/expected/function-contract/modifies_fat_pointer/slice_replace.expected @@ -0,0 +1,7 @@ +Checking harness zero_replace... + +VERIFICATION:- SUCCESSFUL + +Checking harness zero_contract... + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies_fat_pointer/slice_replace.rs b/tests/expected/function-contract/modifies_fat_pointer/slice_replace.rs new file mode 100644 index 000000000000..5bbfbe7c74ae --- /dev/null +++ b/tests/expected/function-contract/modifies_fat_pointer/slice_replace.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts -Zstubbing + +// Test that a contract modifying a whole slice `&mut [T]` can be used as a +// verified stub. This exercises the `write_any` -> `write_any_slice` rewrite in +// the contract replacement pass, which previously produced an invalid doubled +// slice type (`*mut [[T]]`) and crashed the compiler. +// See https://github.com/model-checking/kani/issues/4748 + +#[kani::modifies(x)] +#[kani::ensures(|_| x.iter().all(|v| *v == 0))] +fn zero(x: &mut [u8]) { + x.fill(0) +} + +#[kani::proof_for_contract(zero)] +fn zero_contract() { + let mut x = [kani::any(), kani::any(), kani::any()]; + zero(&mut x); +} + +#[kani::proof] +#[kani::stub_verified(zero)] +fn zero_replace() { + let mut x = [kani::any(), kani::any(), kani::any()]; + zero(&mut x); + assert!(x.iter().all(|v| *v == 0)); +}