From 301cd6aaab722aab88051215b6acea450120aaa7 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Fri, 20 Jun 2025 11:31:12 -0700
Subject: [PATCH] Handle enums with zero or one variants

---
 library/kani_macros/src/derive_bounded.rs     | 43 ++++++++++++++-----
 .../enum_one_variant.expected                 |  7 +++
 .../enum_one_variant.rs                       | 23 ++++++++++
 3 files changed, 62 insertions(+), 11 deletions(-)
 create mode 100644 tests/expected/derive-bounded-arbitrary/enum_one_variant.expected
 create mode 100644 tests/expected/derive-bounded-arbitrary/enum_one_variant.rs

diff --git a/library/kani_macros/src/derive_bounded.rs b/library/kani_macros/src/derive_bounded.rs
index 38e6472eff38..301021d02b95 100644
--- a/library/kani_macros/src/derive_bounded.rs
+++ b/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),* ,
+            }
         }
     }
 }
diff --git a/tests/expected/derive-bounded-arbitrary/enum_one_variant.expected b/tests/expected/derive-bounded-arbitrary/enum_one_variant.expected
new file mode 100644
index 000000000000..a3ca79efaa07
--- /dev/null
+++ b/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.
diff --git a/tests/expected/derive-bounded-arbitrary/enum_one_variant.rs b/tests/expected/derive-bounded-arbitrary/enum_one_variant.rs
new file mode 100644
index 000000000000..6d8f41bcc24e
--- /dev/null
+++ b/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);
+}