Handle generic defaults in BoundedArbitrary derives

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()
     }

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

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