From adee68bece708304114344206e6f6cf8a4bd8372 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Thu, 29 May 2025 16:45:32 -0700
Subject: [PATCH] Handle generic defaults in BoundedArbitrary derives

---
 library/kani_macros/src/derive_bounded.rs     | 17 +++++++------
 .../generic_default.expected                  |  5 ++++
 .../generic_default.rs                        | 24 +++++++++++++++++++
 3 files changed, 39 insertions(+), 7 deletions(-)
 create mode 100644 tests/expected/derive-bounded-arbitrary/generic_default.expected
 create mode 100644 tests/expected/derive-bounded-arbitrary/generic_default.rs

diff --git a/library/kani_macros/src/derive_bounded.rs b/library/kani_macros/src/derive_bounded.rs
index b95624594453..38e6472eff38 100644
--- a/library/kani_macros/src/derive_bounded.rs
+++ b/library/kani_macros/src/derive_bounded.rs
@@ -53,13 +53,14 @@ pub(crate) fn expand_derive_bounded_arbitrary(
     };
 
     // add `T: Arbitrary` bounds for generics
-    let (generics, clauses) = quote_generics(&parsed.generics);
+    let clauses = quote_generics(&parsed.generics);
+    let (impl_generics, ty_generics, _) = parsed.generics.split_for_impl();
     let name = &parsed.ident;
 
     // generate the implementation
     let kani_path = kani_path();
     quote! {
-        impl #generics #kani_path::BoundedArbitrary for #name #generics
+        impl #impl_generics #kani_path::BoundedArbitrary for #name #ty_generics
             #clauses
         {
             fn bounded_any<const N: usize>() -> Self {
@@ -127,12 +128,14 @@ fn union_constructor(ident: &syn::Ident, _data_union: &syn::DataUnion) -> TokenS
 ///     ...
 /// }
 /// ```
-fn quote_generics(generics: &syn::Generics) -> (TokenStream, TokenStream) {
+fn quote_generics(generics: &syn::Generics) -> TokenStream {
     let kani_path = kani_path();
-    let params = generics.type_params().map(|param| quote!(#param)).collect::<Vec<_>>();
-    let where_clauses = generics.type_params().map(|param| quote!(#param : #kani_path::Arbitrary));
-    if !params.is_empty() {
-        (quote!(<#(#params),*>), quote!(where #(#where_clauses),*))
+    let where_clauses = generics.type_params().map(|param| {
+        let ident = &param.ident;
+        quote!(#ident : #kani_path::Arbitrary)
+    });
+    if generics.type_params().count() > 0 {
+        quote!(where #(#where_clauses),*)
     } else {
         Default::default()
     }
diff --git a/tests/expected/derive-bounded-arbitrary/generic_default.expected b/tests/expected/derive-bounded-arbitrary/generic_default.expected
new file mode 100644
index 000000000000..a0f48be25480
--- /dev/null
+++ b/tests/expected/derive-bounded-arbitrary/generic_default.expected
@@ -0,0 +1,5 @@
+Checking harness check_my_vec...
+
+ ** 2 of 2 cover properties satisfied
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/derive-bounded-arbitrary/generic_default.rs b/tests/expected/derive-bounded-arbitrary/generic_default.rs
new file mode 100644
index 000000000000..25c9e1da6723
--- /dev/null
+++ b/tests/expected/derive-bounded-arbitrary/generic_default.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that derive BoundedArbitrary macro works on structs with a generic default
+//! which had an issue in the past:
+//! https://github.com/model-checking/kani/issues/4116
+
+extern crate kani;
+use kani::BoundedArbitrary;
+
+#[derive(BoundedArbitrary)]
+#[allow(unused)]
+struct MyVector<T = i32> {
+    #[bounded]
+    vector: Vec<T>,
+}
+
+#[kani::proof]
+#[kani::unwind(6)]
+fn check_my_vec() {
+    let my_vec: MyVector<u8> = kani::bounded_any::<_, 1>();
+    kani::cover!(my_vec.vector.len() == 0);
+    kani::cover!(my_vec.vector.len() == 1);
+}