From 3828ddf06dc9a5ee9e2dadf87429e67ca8af194c Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 1 Aug 2024 11:59:44 -0700 Subject: [PATCH] Extract variant size from layout --- .../src/codegen_cprover_gotoc/codegen/typ.rs | 25 +++++++++++++------ 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index a6ec8c07bb07..9baa3c59f4c2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1229,7 +1229,8 @@ impl<'tcx> GotocCtx<'tcx> { } let union_name = format!("{name}-union"); let union_pretty_name = format!("{pretty_name}-union"); - let cases = + fields.push(DatatypeComponent::field( + "cases", gcx.ensure_union(&union_name, &union_pretty_name, |ctx, name| { ctx.codegen_enum_cases( name, @@ -1239,15 +1240,23 @@ impl<'tcx> GotocCtx<'tcx> { variants, initial_offset, ) - }); - let cases_size = Size::from_bytes(cases.sizeof(&gcx.symbol_table)); - fields.push(DatatypeComponent::field("cases", cases)); + }), + )); // Check if any padding is needed for alignment. This is needed for // https://github.com/model-checking/kani/issues/2857 for example. - let bytes_so_far = initial_offset + cases_size; - if let Some(padding) = - gcx.codegen_alignment_padding(bytes_so_far, &layout, fields.len()) - { + // The logic for determining the maximum variant size is taken from: + // https://github.com/rust-lang/rust/blob/e60ebb2f2c1facba87e7971798f3cbdfd309cd23/compiler/rustc_session/src/code_stats.rs#L166 + let max_variant_size = variants + .iter() + .map(|l: &LayoutS| l.size) + .max() + .unwrap(); + let max_variant_size = std::cmp::max(max_variant_size, discr_offset); + if let Some(padding) = gcx.codegen_alignment_padding( + max_variant_size, + &layout, + fields.len(), + ) { fields.push(padding); } fields