charon_lib/transform/add_missing_info/
compute_layout_guarantees.rs

1//! Compute layout facts guaranteed by the language.
2use itertools::Itertools;
3
4use crate::ast::*;
5use crate::options::TranslateOptions;
6use crate::transform::{TransformCtx, ctx::TransformPass};
7
8pub struct Transform;
9
10impl TransformPass for Transform {
11    fn should_run(&self, options: &TranslateOptions) -> bool {
12        !options.no_compute_layout_guarantees
13    }
14
15    fn transform_ctx(&self, ctx: &mut TransformCtx) {
16        let target = ctx
17            .translated
18            .target_information
19            .keys()
20            .exactly_one()
21            .expect("layout guarantees expect exactly one target")
22            .clone();
23
24        ctx.for_each_type_decl(|ctx, decl| {
25            let Some(layout) = decl.layout.get_mut(&target) else {
26                return;
27            };
28
29            // Normalize Inhabited predicates
30            layout.inhabited = layout.inhabited.clone().normalize(&ctx.translated, None);
31            for layout in layout.variant_layouts.iter_mut().flatten() {
32                layout.inhabited = layout.inhabited.clone().normalize(&ctx.translated, None);
33            }
34
35            let field_tys: Vec<_> = match &decl.kind {
36                TypeDeclKind::Struct(fields) | TypeDeclKind::Union(fields)
37                    if layout.inhabited.always_true() =>
38                {
39                    fields.iter().map(|field| field.ty.clone()).collect()
40                }
41                TypeDeclKind::Enum(variants) => variants
42                    .iter_enumerated()
43                    .filter(|(id, _)| {
44                        layout.variant_layouts[*id]
45                            .as_ref()
46                            .is_some_and(|vl| vl.inhabited.always_true())
47                    })
48                    .flat_map(|(_, variant)| variant.fields.iter())
49                    .map(|field| field.ty.clone())
50                    .collect(),
51                _ => return,
52            };
53
54            // `repr(packed)` caps the effective alignment of each field.
55            let pack = match &layout.repr.align_modif {
56                Some(AlignmentModifier::Pack(pack)) => Some(u128::from(*pack)),
57                _ => None,
58            };
59            let field_aligns = field_tys.iter().cloned().map(|ty| {
60                let align = SizeExprKind::Constant(ConstantExpr::new(
61                    ConstantExprKind::AlignOf(ty),
62                    Ty::mk_usize(),
63                ))
64                .into_expr();
65                if let Some(pack) = pack {
66                    SizeExprKind::Min(vec![align, SizeExprKind::from_usize(pack).into_expr()])
67                        .into_expr()
68                } else {
69                    align
70                }
71            });
72            let align = SizeExprKind::Max(field_aligns.collect()).into_expr();
73            let align = align.normalize(None, None, false);
74
75            let field_sizes = field_tys.into_iter().map(|ty| {
76                SizeExprKind::Constant(ConstantExpr::new(
77                    ConstantExprKind::SizeOf(ty),
78                    Ty::mk_usize(),
79                ))
80                .into_expr()
81            });
82            let size = SizeExprKind::AlignTo {
83                base: SizeExprKind::Max(field_sizes.collect()).into_expr(),
84                target_align: align.clone(),
85            }
86            .into_expr();
87            let size = size.normalize(None, None, false);
88
89            layout.align.guarantee = Some(SizeExprKind::AtLeast(align).into_expr());
90            layout.size.guarantee = Some(SizeExprKind::AtLeast(size).into_expr());
91        });
92    }
93}
charon_lib/transform/add_missing_info/compute_layout_guarantees.rs

charon_lib/transform/add_missing_info/
compute_layout_guarantees.rs
