Handle enums with zero or one variants (model-checking#4171)

Handle enums with zero or one variants when deriving `BoundedArbitrary`.

Resolves model-checking#4170

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: zhassan-aws

library/kani_macros/src/derive_bounded.rs

@@ -92,19 +92,40 @@ fn generate_type_constructor(type_name: TokenStream, fields: &syn::Fields) -> To
 /// Generates a `match` case to construct each variant of the given type. Uses a
 /// symbolic `usize` to decide which variant to construct.
 fn enum_constructor(ident: &syn::Ident, data_enum: &syn::DataEnum) -> TokenStream {
-    let variant_constructors = data_enum.variants.iter().map(|variant| {
+    if data_enum.variants.is_empty() {
+        let msg = format!(
+            "Cannot create symbolic enum `{ident}`. Enums with zero-variants cannot be instantiated"
+        );
+        quote! {
+            panic!(#msg)
+        }
+    } else if data_enum.variants.len() == 1 {
+        let variant = data_enum.variants.first().unwrap();
         let variant_name = &variant.ident;
-        generate_type_constructor(quote!(#ident::#variant_name), &variant.fields)
-    });
-    let n_variants = data_enum.variants.len();
-    let cases = variant_constructors.enumerate().map(|(idx, var_constr)| {
-        if idx < n_variants - 1 { quote!(#idx => #var_constr) } else { quote!(_ => #var_constr) }
-    });
+        let variant_constructor =
+            generate_type_constructor(quote!(#ident::#variant_name), &variant.fields);
+        quote! {
+            #variant_constructor
+        }
+    } else {
+        let variant_constructors = data_enum.variants.iter().map(|variant| {
+            let variant_name = &variant.ident;
+            generate_type_constructor(quote!(#ident::#variant_name), &variant.fields)
+        });
+        let n_variants = data_enum.variants.len();
+        let cases = variant_constructors.enumerate().map(|(idx, var_constr)| {
+            if idx < n_variants - 1 {
+                quote!(#idx => #var_constr)
+            } else {
+                quote!(_ => #var_constr)
+            }
+        });
 
-    let kani_path = kani_path();
-    quote! {
-        match #kani_path::any() {
-            #(#cases),* ,
+        let kani_path = kani_path();
+        quote! {
+            match #kani_path::any() {
+                #(#cases),* ,
+            }
         }
     }
 }

tests/expected/derive-bounded-arbitrary/enum_one_variant.expected

@@ -0,0 +1,7 @@
+Checking harness check_enum...
+
+ ** 5 of 5 cover properties satisfied
+
+VERIFICATION:- SUCCESSFUL
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

tests/expected/derive-bounded-arbitrary/enum_one_variant.rs

@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that derive BoundedArbitrary macro works on enums with a single variant
+//! See https://github.com/model-checking/kani/issues/4170
+
+#[allow(unused)]
+#[derive(kani::BoundedArbitrary)]
+enum Foo {
+    A(#[bounded] String),
+}
+
+#[kani::proof]
+#[kani::unwind(6)]
+fn check_enum() {
+    let any_enum: Foo = kani::bounded_any::<_, 4>();
+    let Foo::A(s) = any_enum;
+    kani::cover!(s.len() == 0);
+    kani::cover!(s.len() == 1);
+    kani::cover!(s.len() == 2);
+    kani::cover!(s.len() == 3);
+    kani::cover!(s.len() == 4);
+}