charon_lib/ast/items/
layout_guarantees.rs

1//! Guarantees about the layout of types, as given by the Rust Reference.
2use crate::ast::*;
3use derive_generic_visitor::*;
4use macros::{EnumAsGetters, EnumIsA, VariantName};
5use serde_state::{DeserializeState, SerializeState};
6
7/// Guaranteed facts about a layout size.
8#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
9pub enum SizeGuarantee {
10    Equals(ExactSizeExpr),
11    AtLeast(ExactSizeExpr),
12}
13
14/// Guaranteed facts about a field offset.
15#[derive(
16    Debug,
17    Clone,
18    EnumIsA,
19    EnumAsGetters,
20    VariantName,
21    SerializeState,
22    DeserializeState,
23    Drive,
24    DriveMut,
25    DriveTwo,
26)]
27pub enum OffsetGuarantee {
28    /// Guaranteed to be at offset zero. This applies for `repr(transparent)` and in some `repr(C)` cases.
29    AtOffsetZero,
30    /// Guaranteed only to be aligned to the given expression.
31    GuaranteedAlignment(ExactSizeExpr),
32    /// This offset is computed by the layout algorithm for C: take the previous field offset, add
33    /// the previous field size, and align to the current field alignment.
34    ReprCField {
35        /// If this is `None`, then the field is directly after the enum tag.
36        predecessor: Option<FieldId>,
37    },
38}
39
40/// Layout information given by the metadata of an unsized type.
41#[derive(
42    Debug,
43    Clone,
44    PartialEq,
45    Eq,
46    PartialOrd,
47    Ord,
48    Hash,
49    EnumIsA,
50    EnumAsGetters,
51    VariantName,
52    SerializeState,
53    DeserializeState,
54    Drive,
55    DriveMut,
56    DriveTwo,
57)]
58#[cfg_attr(feature = "charon_on_charon", charon::variant_prefix("LayoutValue"))]
59pub enum MetadataValue {
60    /// For a DST with `dyn Trait` metadata, this refers to the size found in the metadata.
61    DynSize,
62    /// For a DST with `dyn Trait` metadata, this refers to the alignment found in the metadata.
63    DynAlign,
64    /// For a DST with slice metadata, this refers to the length found in the metadata.
65    SliceLength,
66}
67
68/// An expression that represents a size in bytes.
69#[derive(
70    Debug,
71    Clone,
72    PartialEq,
73    Eq,
74    PartialOrd,
75    Ord,
76    Hash,
77    SerializeState,
78    DeserializeState,
79    Drive,
80    DriveMut,
81    DriveTwo,
82)]
83#[serde_state(state_implements = DedupSerializerState)]
84pub struct ExactSizeExpr(pub HashConsed<ExactSizeExprKind>);
85
86#[derive(
87    Debug,
88    Clone,
89    PartialEq,
90    Eq,
91    PartialOrd,
92    Ord,
93    Hash,
94    EnumIsA,
95    EnumAsGetters,
96    VariantName,
97    SerializeState,
98    DeserializeState,
99    Drive,
100    DriveMut,
101    DriveTwo,
102)]
103#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("ExactSizeExpr"))]
104pub enum ExactSizeExprKind {
105    /// An arbitrary constant of type `usize`.
106    Constant(ConstantExpr),
107    /// Layout information stored in the pointer metadata to this object.
108    FromMetadata(MetadataValue),
109    Max(Vec<ExactSizeExpr>),
110    Min(Vec<ExactSizeExpr>),
111    Plus(ExactSizeExpr, ExactSizeExpr),
112    Scale(ExactSizeExpr, ConstantExpr),
113    /// The next multiple of `target_align` from `base`.
114    AlignTo {
115        base: ExactSizeExpr,
116        target_align: ExactSizeExpr,
117    },
118    /// A size expression that depens on whether the given type is inhabited.
119    IfInhabited {
120        ty: Ty,
121        then_size: ExactSizeExpr,
122        else_size: ExactSizeExpr,
123    },
124}
125
126impl ExactSizeExpr {
127    pub fn new(kind: ExactSizeExprKind) -> Self {
128        Self(HashConsed::new(kind))
129    }
130
131    pub fn kind(&self) -> &ExactSizeExprKind {
132        self.0.inner()
133    }
134
135    pub fn with_kind_mut<R>(&mut self, f: impl FnOnce(&mut ExactSizeExprKind) -> R) -> R {
136        self.0.with_inner_mut(f)
137    }
138
139    /// Recursively evaluate the parts of this expression that are known in `krate`.
140    pub fn normalize(mut self, krate: &TranslatedCrate, target: &TargetTriple) -> Self {
141        #[derive(Visitor)]
142        struct NormalizeSizeExpr<'a> {
143            krate: &'a TranslatedCrate,
144            target: &'a TargetTriple,
145        }
146
147        /// Take out the concrete values from the vec and fold them with the provided function.
148        fn fold_concrete_values(
149            values: &mut Vec<ExactSizeExpr>,
150            f: impl Fn(u128, u128) -> u128,
151        ) -> Option<u128> {
152            values
153                .extract_if(.., |val| val.as_usize().is_some())
154                .map(|val| val.as_usize().unwrap())
155                .reduce(f)
156        }
157
158        impl VisitAstMut for NormalizeSizeExpr<'_> {
159            fn exit_exact_size_expr_kind(&mut self, expr: &mut ExactSizeExprKind) {
160                *expr = match expr {
161                    ExactSizeExprKind::Constant(constant) => {
162                        debug_assert!(constant.ty().is_usize());
163                        let exact_guarantee = |size: &SizeExpr| match &size.guarantee {
164                            Some(SizeGuarantee::Equals(value)) => Some(value.clone()),
165                            Some(SizeGuarantee::AtLeast(_)) | None => None,
166                        };
167                        let mut guaranteed = match constant.kind() {
168                            ConstantExprKind::SizeOf(ty) => match ty.kind() {
169                                TyKind::Never => ExactSizeExpr::from_usize(0),
170                                TyKind::Scalar(scalar_ty) => {
171                                    if let Some(target) =
172                                        self.krate.target_information.get(self.target)
173                                    {
174                                        ExactSizeExpr::from_usize(
175                                            scalar_ty.target_size(target.target_pointer_size)
176                                                as u128,
177                                        )
178                                    } else {
179                                        return;
180                                    }
181                                }
182                                _ => {
183                                    if let Some(ty_ref) = ty.as_adt()
184                                        && let Some(decl) = self.krate.type_decls.get(ty_ref.id)
185                                        && let Some(layout) = decl.layout.get(self.target)
186                                        && let Some(value) = exact_guarantee(&layout.size)
187                                    {
188                                        value.substitute(&ty_ref.generics)
189                                    } else {
190                                        return;
191                                    }
192                                }
193                            },
194                            ConstantExprKind::AlignOf(ty) => match ty.kind() {
195                                TyKind::Never => ExactSizeExpr::from_usize(1),
196                                TyKind::Scalar(scalar_ty) => {
197                                    if let Some(target) =
198                                        self.krate.target_information.get(self.target)
199                                        && let Some(value) =
200                                            target.primitive_alignments.get(scalar_ty)
201                                    {
202                                        ExactSizeExpr::from_usize(u128::from(*value))
203                                    } else {
204                                        return;
205                                    }
206                                }
207                                _ => {
208                                    if let Some(ty_ref) = ty.as_adt()
209                                        && let Some(decl) = self.krate.type_decls.get(ty_ref.id)
210                                        && let Some(layout) = decl.layout.get(self.target)
211                                        && let Some(value) = exact_guarantee(&layout.align)
212                                    {
213                                        value.substitute(&ty_ref.generics)
214                                    } else {
215                                        return;
216                                    }
217                                }
218                            },
219                            _ => return,
220                        };
221                        self.visit(&mut guaranteed);
222                        guaranteed.kind().clone()
223                    }
224                    ExactSizeExprKind::FromMetadata(_) => return,
225                    ExactSizeExprKind::Max(values) => {
226                        // Flatten nested operations.
227                        for val in std::mem::take(values) {
228                            match val.kind() {
229                                ExactSizeExprKind::Max(nested) => {
230                                    values.extend(nested.iter().cloned())
231                                }
232                                _ => values.push(val),
233                            }
234                        }
235                        // Get the max of the concrete values.
236                        if let Some(value) = fold_concrete_values(values, std::cmp::max)
237                            && value != 0
238                        {
239                            // Zero is the identity of `Max` so we don't push in that case.
240                            values.push(ExactSizeExpr::from_usize(value));
241                        }
242                        if values.len() == 1 {
243                            values.pop().unwrap().kind().clone()
244                        } else if values.is_empty() {
245                            ExactSizeExprKind::zero()
246                        } else {
247                            return;
248                        }
249                    }
250                    ExactSizeExprKind::Min(values) => {
251                        // Flatten nested operations.
252                        for val in std::mem::take(values) {
253                            match val.kind() {
254                                ExactSizeExprKind::Min(nested) => {
255                                    values.extend(nested.iter().cloned())
256                                }
257                                _ => values.push(val),
258                            }
259                        }
260                        // Get the min of the concrete values.
261                        if let Some(value) = fold_concrete_values(values, std::cmp::min) {
262                            // Zero is absorbing for `Min`.
263                            if value == 0 {
264                                values.clear();
265                            }
266                            values.push(ExactSizeExpr::from_usize(value));
267                        }
268                        if values.len() == 1 {
269                            values.pop().unwrap().kind().clone()
270                        } else {
271                            return;
272                        }
273                    }
274                    ExactSizeExprKind::Plus(left, right) => {
275                        match (left.as_usize(), right.as_usize()) {
276                            (Some(left), Some(right)) => {
277                                ExactSizeExprKind::from_usize(left.strict_add(right))
278                            }
279                            (Some(0), None) => right.kind().clone(),
280                            (None, Some(0)) => left.kind().clone(),
281                            _ => return,
282                        }
283                    }
284                    ExactSizeExprKind::Scale(base, multiplier) => {
285                        match (base.as_usize(), multiplier.as_usize_literal()) {
286                            (_, Some(0)) | (Some(0), _) => ExactSizeExprKind::zero(),
287                            (_, Some(1)) => base.kind().clone(),
288                            (Some(base), Some(multiplier)) => {
289                                ExactSizeExprKind::from_usize(base.strict_mul(multiplier))
290                            }
291                            _ => return,
292                        }
293                    }
294                    ExactSizeExprKind::AlignTo { base, target_align } => {
295                        match (base.as_usize(), target_align.as_usize()) {
296                            (_, Some(1)) => base.kind().clone(),
297                            (Some(0), Some(align)) if align != 0 => base.kind().clone(),
298                            (Some(base), Some(align)) if align != 0 => {
299                                let remainder = base % align;
300                                ExactSizeExprKind::from_usize(if remainder == 0 {
301                                    base
302                                } else {
303                                    base.strict_add(align - remainder)
304                                })
305                            }
306                            _ => return,
307                        }
308                    }
309                    ExactSizeExprKind::IfInhabited { .. } => {
310                        // FIXME: evaluate type inhabitedness
311                        return;
312                    }
313                };
314            }
315        }
316
317        NormalizeSizeExpr { krate, target }.visit(&mut self);
318        self
319    }
320
321    fn as_usize(&self) -> Option<u128> {
322        if let ExactSizeExprKind::Constant(constant) = self.kind() {
323            constant.as_usize_literal()
324        } else {
325            None
326        }
327    }
328
329    fn from_usize(value: u128) -> Self {
330        ExactSizeExprKind::from_usize(value).into_expr()
331    }
332}
333
334impl ExactSizeExprKind {
335    pub fn zero() -> Self {
336        Self::from_usize(0)
337    }
338
339    pub fn from_usize(value: u128) -> Self {
340        Self::Constant(ConstantExpr::mk_usize(value))
341    }
342
343    pub fn into_expr(self) -> ExactSizeExpr {
344        ExactSizeExpr::new(self)
345    }
346}
347
348impl From<ExactSizeExprKind> for ExactSizeExpr {
349    fn from(kind: ExactSizeExprKind) -> Self {
350        kind.into_expr()
351    }
352}
353
354impl std::ops::Deref for ExactSizeExpr {
355    type Target = ExactSizeExprKind;
356
357    fn deref(&self) -> &Self::Target {
358        self.kind()
359    }
360}
361
362#[cfg(test)]
363mod tests {
364    use super::*;
365
366    fn test_krate() -> (TranslatedCrate, TargetTriple) {
367        let mut krate = TranslatedCrate::default();
368        let target = "test-target".to_owned();
369        krate.target_information.insert(
370            target.clone(),
371            TargetInfo {
372                target_pointer_size: 8,
373                is_little_endian: true,
374                c_enum_smallest_repr_ty: IntTy::I32,
375                primitive_alignments: SeqHashMap::new(),
376            },
377        );
378        (krate, target)
379    }
380
381    #[test]
382    fn normalize_arithmetic() {
383        let (krate, target) = test_krate();
384        let expr = ExactSizeExprKind::AlignTo {
385            base: ExactSizeExprKind::Plus(
386                ExactSizeExpr::from_usize(2),
387                ExactSizeExprKind::Scale(ExactSizeExpr::from_usize(3), ConstantExpr::mk_usize(4))
388                    .into_expr(),
389            )
390            .into_expr(),
391            target_align: ExactSizeExpr::from_usize(8),
392        }
393        .into_expr()
394        .normalize(&krate, &target);
395
396        assert_eq!(expr.as_usize(), Some(16));
397    }
398
399    #[test]
400    fn normalize_extrema_partially() {
401        let (krate, target) = test_krate();
402        let expr = ExactSizeExprKind::Max(vec![
403            ExactSizeExpr::from_usize(2),
404            ExactSizeExprKind::Max(vec![
405                ExactSizeExpr::from_usize(5),
406                ExactSizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr(),
407            ])
408            .into_expr(),
409            ExactSizeExpr::from_usize(3),
410        ])
411        .into_expr()
412        .normalize(&krate, &target);
413
414        let ExactSizeExprKind::Max(contenders) = expr.kind() else {
415            panic!("expected a partially normalized maximum")
416        };
417        assert_eq!(contenders.len(), 2);
418        assert_eq!(contenders[1].as_usize(), Some(5));
419        assert!(matches!(
420            contenders[0].kind(),
421            ExactSizeExprKind::FromMetadata(MetadataValue::DynSize)
422        ));
423
424        let empty = ExactSizeExprKind::Max(Vec::new())
425            .into_expr()
426            .normalize(&krate, &target);
427        assert_eq!(empty.as_usize(), Some(0));
428    }
429
430    #[test]
431    fn normalize_extrema_identities() {
432        let (krate, target) = test_krate();
433        let max = ExactSizeExprKind::Max(vec![
434            ExactSizeExpr::from_usize(0),
435            ExactSizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr(),
436        ])
437        .into_expr()
438        .normalize(&krate, &target);
439        let min = ExactSizeExprKind::Min(vec![
440            ExactSizeExpr::from_usize(7),
441            ExactSizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr(),
442            ExactSizeExpr::from_usize(0),
443        ])
444        .into_expr()
445        .normalize(&krate, &target);
446
447        assert!(matches!(
448            max.kind(),
449            ExactSizeExprKind::FromMetadata(MetadataValue::DynSize)
450        ));
451        assert_eq!(min.as_usize(), Some(0));
452    }
453
454    #[test]
455    fn normalize_if_inhabited() {
456        let (krate, target) = test_krate();
457        let expr = ExactSizeExprKind::IfInhabited {
458            ty: TyKind::Never.into_ty(),
459            then_size: ExactSizeExpr::from_usize(10),
460            else_size: ExactSizeExprKind::Plus(
461                ExactSizeExpr::from_usize(2),
462                ExactSizeExpr::from_usize(3),
463            )
464            .into_expr(),
465        }
466        .into_expr()
467        .normalize(&krate, &target);
468
469        let ExactSizeExprKind::IfInhabited {
470            then_size,
471            else_size,
472            ..
473        } = expr.kind()
474        else {
475            panic!("inhabitedness is not normalized yet")
476        };
477        assert_eq!(then_size.as_usize(), Some(10));
478        assert_eq!(else_size.as_usize(), Some(5));
479    }
480
481    #[test]
482    fn normalize_for_the_selected_target() {
483        let mut krate = TranslatedCrate::default();
484        let scalar_ty = ScalarTy::Integer(IntegerTy::Unsigned(UIntTy::U64));
485        for (triple, pointer_size, alignment) in [("a", 4, 4), ("b", 8, 8)] {
486            let mut primitive_alignments = SeqHashMap::new();
487            primitive_alignments.insert(scalar_ty, alignment);
488            krate.target_information.insert(
489                triple.to_owned(),
490                TargetInfo {
491                    target_pointer_size: pointer_size,
492                    is_little_endian: true,
493                    c_enum_smallest_repr_ty: IntTy::I32,
494                    primitive_alignments,
495                },
496            );
497        }
498        let target_a = "a".to_owned();
499        let target_b = "b".to_owned();
500
501        let size = ExactSizeExprKind::Constant(ConstantExpr::new(
502            ConstantExprKind::SizeOf(TyKind::Scalar(scalar_ty).into_ty()),
503            Ty::mk_usize(),
504        ))
505        .into_expr()
506        .normalize(&krate, &target_a);
507        let align = ExactSizeExprKind::Constant(ConstantExpr::new(
508            ConstantExprKind::AlignOf(TyKind::Scalar(scalar_ty).into_ty()),
509            Ty::mk_usize(),
510        ))
511        .into_expr()
512        .normalize(&krate, &target_a);
513        let pointer_size = ExactSizeExprKind::Constant(ConstantExpr::new(
514            ConstantExprKind::SizeOf(Ty::mk_usize()),
515            Ty::mk_usize(),
516        ))
517        .into_expr();
518        let pointer_size_a = pointer_size.clone().normalize(&krate, &target_a);
519        let pointer_size_b = pointer_size.normalize(&krate, &target_b);
520
521        assert_eq!(size.as_usize(), Some(8));
522        assert_eq!(align.as_usize(), Some(4));
523        assert_eq!(pointer_size_a.as_usize(), Some(4));
524        assert_eq!(pointer_size_b.as_usize(), Some(8));
525    }
526
527    #[test]
528    fn normalize_uses_guarantees_not_chosen_values() {
529        let (mut krate, target) = test_krate();
530        let id = TypeDeclId::ZERO;
531        let mut generics = GenericParams::empty();
532        generics
533            .types
534            .push_with(|id| TypeParam::new(id, "T".to_owned(), Variance::Invariant));
535        let generic_ty = generics.identity_args().types[TypeVarId::ZERO].clone();
536        let mut layouts = SeqHashMap::new();
537        layouts.insert(
538            target.clone(),
539            Layout {
540                size: SizeExpr {
541                    guarantee: None,
542                    chosen: Some(99),
543                },
544                align: SizeExpr::new(1),
545                discriminator: None,
546                uninhabited: false,
547                variant_layouts: Default::default(),
548                repr: Default::default(),
549            },
550        );
551        krate.type_decls.insert(
552            id,
553            TypeDecl {
554                def_id: id,
555                item_meta: ItemMeta::dummy_public(
556                    Span::default(),
557                    Name::from_path(&["T"]),
558                    true,
559                    ItemOpacity::Transparent,
560                ),
561                generics,
562                src: TypeSource::Normal,
563                kind: TypeDeclKind::Opaque,
564                layout: layouts,
565                ptr_metadata: PtrMetadata::None,
566            },
567        );
568        let ty = TyKind::Adt(TypeDeclRef::new(
569            id,
570            GenericArgs::new_types(
571                [TyKind::Scalar(ScalarTy::Integer(IntegerTy::Unsigned(UIntTy::U16))).into_ty()]
572                    .into_iter()
573                    .collect(),
574            ),
575            None,
576        ))
577        .into_ty();
578        let size_of = || {
579            ExactSizeExprKind::Constant(ConstantExpr::new(
580                ConstantExprKind::SizeOf(ty.clone()),
581                Ty::mk_usize(),
582            ))
583            .into_expr()
584        };
585
586        let without_guarantee = size_of().normalize(&krate, &target);
587        assert!(matches!(
588            without_guarantee.kind(),
589            ExactSizeExprKind::Constant(constant)
590                if matches!(constant.kind(), ConstantExprKind::SizeOf(_))
591        ));
592
593        let size = &mut krate.type_decls.get_mut(id).unwrap().layout[&target].size;
594        size.guarantee = Some(SizeGuarantee::Equals(
595            ExactSizeExprKind::Plus(
596                ExactSizeExprKind::Constant(ConstantExpr::new(
597                    ConstantExprKind::SizeOf(generic_ty),
598                    Ty::mk_usize(),
599                ))
600                .into_expr(),
601                ExactSizeExpr::from_usize(5),
602            )
603            .into_expr(),
604        ));
605        let with_guarantee = size_of().normalize(&krate, &target);
606        assert_eq!(with_guarantee.as_usize(), Some(7));
607    }
608}
charon_lib/ast/items/layout_guarantees.rs

charon_lib/ast/items/
layout_guarantees.rs
