extend generic fn note to show for generic traits too

Author: Carolyn Zech

kani-compiler/src/kani_middle/attributes.rs

@@ -688,8 +688,12 @@ impl<'tcx> KaniAttributes<'tcx> {
                 }
                 ResolveError::MissingTraitImpl { tcx: _, trait_fn_id, ty: _ } => {
                     let generics = self.tcx.generics_of(trait_fn_id);
-                    if !generics.own_params.is_empty() {
-                        err = err.with_help(
+                    let parent_generics =
+                        generics.parent.map(|parent| self.tcx.generics_of(parent));
+                    if !generics.own_params.is_empty()
+                        || parent_generics.is_some_and(|generics| !generics.own_params.is_empty())
+                    {
+                        err = err.with_note(
                             "Kani does not currently support stubs or function contracts on generic functions in traits.\n \
                             See https://github.com/model-checking/kani/issues/1997#issuecomment-3134614734 for more information.",
                         );

tests/ui/function-contracts/generic_slice_index.expected

@@ -0,0 +1,11 @@
+error: failed to resolve `<usize as SliceIndex < [i32] >>::get_unchecked`: unable to find implementation of associated function `SliceIndex::get_unchecked` for usize\
+generic_slice_index.rs\
+|\
+| #[kani::proof_for_contract(<usize as SliceIndex<[i32]>>::get_unchecked)]\
+| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
+|\
+= note: Kani does not currently support stubs or function contracts on generic functions in traits.\
+    See https://github.com/model-checking/kani/issues/1997#issuecomment-3134614734 for more information.
+
+
+error: aborting due to 1 previous error

tests/ui/function-contracts/generic_slice_index.rs

@@ -0,0 +1,37 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+//! Test function contracts on generic trait implementations based on SliceIndex,
+//! c.f. https://github.com/model-checking/kani/issues/4084
+//! This `proof_for_contract` should work,
+//! but we do not yet support stubbing/contracts on trait fns with generic arguments
+//! c.f. https://github.com/model-checking/kani/issues/1997#issuecomment-3134614734.
+//! So for now, test that we emit a nice error message.
+
+const INVALID_INDEX: usize = 10;
+
+trait SliceIndex<T: ?Sized> {
+    type Output: ?Sized;
+    unsafe fn get_unchecked(self, slice: *const T) -> *const Self::Output;
+}
+
+impl<T> SliceIndex<[T]> for usize {
+    type Output = T;
+
+    #[kani::requires(!slice.is_null())]
+    #[kani::requires(self < slice.len())]
+    unsafe fn get_unchecked(self, slice: *const [T]) -> *const Self::Output {
+        unsafe { (*slice).as_ptr().add(self) }
+    }
+}
+
+#[kani::proof_for_contract(<usize as SliceIndex<[i32]>>::get_unchecked)]
+fn test_generic_slice_contract() {
+    let data = [1i32, 2, 3, 4, 5];
+    let slice_ptr = &data as *const [i32];
+
+    unsafe {
+        // This violates the contract precondition (index >= slice length)
+        let _ptr = INVALID_INDEX.get_unchecked(slice_ptr);
+    }
+}

tests/ui/stubbing/generic_trait_fn.expected

@@ -4,7 +4,7 @@ generic_trait_fn.rs\
 | #[kani::stub(<TestStruct as TraitX>::generic_fn, <TestStruct as TraitY>::generic_fn)]\
 | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
 |\
-   = help: Kani does not currently support stubs or function contracts on generic functions in traits.\
+   = note: Kani does not currently support stubs or function contracts on generic functions in traits.\
             See https://github.com/model-checking/kani/issues/1997#issuecomment-3134614734 for more information.
 
 error: failed to resolve `<TestStruct as TraitY>::generic_fn`: unable to find implementation of associated function `TraitY::generic_fn` for TestStruct\
@@ -13,7 +13,7 @@ generic_trait_fn.rs\
 | #[kani::stub(<TestStruct as TraitX>::generic_fn, <TestStruct as TraitY>::generic_fn)]\
 | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
 |\
-   = help: Kani does not currently support stubs or function contracts on generic functions in traits.\
+   = note: Kani does not currently support stubs or function contracts on generic functions in traits.\
             See https://github.com/model-checking/kani/issues/1997#issuecomment-3134614734 for more information.
 
 error: aborting due to 2 previous errors