Fix compiler crash on slice-modifies verified stubs (#4748)

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<T>(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 };

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

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