Fix codegen_rvalue_aggregate for tuples (rust-lang#2371)

celinval · Apr 13, 2023 · a85f77c · a85f77c
1 parent 4f710d4
commit a85f77c
Showing 1 changed file with 13 additions and 11 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -304,17 +304,19 @@ impl<'tcx> GotocCtx<'tcx> {
                     )
                 }
             }
-            AggregateKind::Tuple => Expr::struct_expr_from_values(
-                self.codegen_ty(res_ty),
-                operands
-                    .iter()
-                    .filter_map(|o| {
-                        let oty = self.operand_ty(o);
-                        if oty.is_unit() { None } else { Some(self.codegen_operand(o)) }
-                    })
-                    .collect(),
-                &self.symbol_table,
-            ),
+            AggregateKind::Tuple => {
+                let typ = self.codegen_ty(res_ty);
+                let layout = self.layout_of(res_ty);
+                Expr::struct_expr_from_values(
+                    typ,
+                    layout
+                        .fields
+                        .index_by_increasing_offset()
+                        .map(|idx| self.codegen_operand(&operands[idx]))
+                        .collect(),
+                    &self.symbol_table,
+                )
+            }
             AggregateKind::Adt(_, _, _, _, _) => unimplemented!(),
             AggregateKind::Closure(_, _) => unimplemented!(),
             AggregateKind::Generator(_, _, _) => unimplemented!(),