Adjust enum aggregation

Simplify the code by reusing some of the existing logic

cprover_bindings/src/goto_program/expr.rs

@@ -131,7 +131,7 @@ pub enum ExprValue {
     StringConstant {
         s: InternedString,
     },
-    /// Struct initializer  
+    /// Struct initializer
     /// `struct foo the_foo = >>> {field1, field2, ... } <<<`
     Struct {
         values: Vec<Expr>,
@@ -142,7 +142,7 @@ pub enum ExprValue {
     },
     /// `(typ) self`. Target type is in the outer `Expr` struct.
     Typecast(Expr),
-    /// Union initializer  
+    /// Union initializer
     /// `union foo the_foo = >>> {.field = value } <<<`
     Union {
         value: Expr,
@@ -681,7 +681,7 @@ impl Expr {
         expr!(StatementExpression { statements: ops }, typ)
     }
 
-    /// Internal helper function for Struct initalizer  
+    /// Internal helper function for Struct initalizer
     /// `struct foo the_foo = >>> {.field1 = val1, .field2 = val2, ... } <<<`
     /// ALL fields must be given, including padding
     fn struct_expr_with_explicit_padding(
@@ -698,7 +698,7 @@ impl Expr {
         expr!(Struct { values }, typ)
     }
 
-    /// Struct initializer  
+    /// Struct initializer
     /// `struct foo the_foo = >>> {.field1 = val1, .field2 = val2, ... } <<<`
     /// Note that only the NON padding fields should be explicitly given.
     /// Padding fields are automatically inserted using the type from the `SymbolTable`
@@ -719,7 +719,7 @@ impl Expr {
             "Error in struct_expr; mismatch in number of fields and components.\n\t{typ:?}\n\t{components:?}"
         );
 
-        // Check that each formal field has an value
+        // Check that each formal field has a value
         for field in non_padding_fields {
             let field_typ = field.field_typ().unwrap();
             let value = components.get(&field.name()).unwrap();
@@ -764,7 +764,7 @@ impl Expr {
         Expr::struct_expr_from_values(typ, values, symbol_table)
     }
 
-    /// Struct initializer  
+    /// Struct initializer
     /// `struct foo the_foo = >>> {field1, field2, ... } <<<`
     /// Note that only the NON padding fields should be explicitly given.
     /// Padding fields are automatically inserted using the type from the `SymbolTable`
@@ -800,7 +800,7 @@ impl Expr {
         Expr::struct_expr_with_explicit_padding(typ, fields, values)
     }
 
-    /// Struct initializer  
+    /// Struct initializer
     /// `struct foo the_foo = >>> {field1, padding2, field3, ... } <<<`
     /// Note that padding fields should be explicitly given.
     /// This would be used when the values and padding have already been combined,
@@ -859,7 +859,7 @@ impl Expr {
         self.transmute_to(t, st)
     }
 
-    /// Union initializer  
+    /// Union initializer
     /// `union foo the_foo = >>> {.field = value } <<<`
     pub fn union_expr<T: Into<InternedString>>(
         typ: Type,

kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

@@ -231,6 +231,17 @@ impl<'tcx> TypeOrVariant<'tcx> {
             }
         }
     }
+
+    #[allow(dead_code)]
+    pub fn expect_gen_variant(&self) -> VariantIdx {
+        match self {
+            TypeOrVariant::Type(t) => panic!("expect a generator but found type: {t:?}"),
+            TypeOrVariant::Variant(v) => {
+                panic!("expect a generator but found variant: {v:?}")
+            }
+            TypeOrVariant::GeneratorVariant(v) => *v,
+        }
+    }
 }
 
 impl<'tcx> GotocCtx<'tcx> {
@@ -624,6 +635,17 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    /// Given a projection, generate an lvalue that represents the given variant index.
+    pub fn codegen_variant_lvalue(
+        &mut self,
+        initial_projection: ProjectedPlace<'tcx>,
+        variant_idx: VariantIdx,
+    ) -> ProjectedPlace<'tcx> {
+        debug!(?initial_projection, ?variant_idx, "codegen_variant_lvalue");
+        let downcast = ProjectionElem::Downcast(None, variant_idx);
+        self.codegen_projection(Ok(initial_projection), downcast).unwrap()
+    }
+
     // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.ProjectionElem.html
     // ConstantIndex
     // [−]