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/// The predecessor of a field in a struct or enum variant.
8#[derive(Debug, Copy, Clone, PartialEq)]
9#[derive(SerializeState, DeserializeState)]
10#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Predecessor"))]
11pub enum FieldPredecessor {
12    Field(FieldId),
13    Tag,
14}
15
16/// Guaranteed facts about a field offset.
17#[derive(Debug, Clone)]
18#[derive(EnumIsA, EnumAsGetters, VariantName)]
19#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
20pub enum OffsetGuarantee {
21    /// Guaranteed to be exactly at the given offset.
22    AtOffset(SizeExpr),
23    /// Guaranteed only to be aligned to the given expression.
24    GuaranteedAlignment(SizeExpr),
25    /// This offset is computed by the layout algorithm for C: take the previous field offset, add
26    /// the previous field size, and align to the current field alignment (as capped by `packed`).
27    ReprCField(FieldPredecessor),
28}
29
30/// Layout information given by the metadata of an unsized type.
31#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
32#[derive(EnumIsA, EnumAsGetters, VariantName)]
33#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
34#[cfg_attr(feature = "charon_on_charon", charon::variant_prefix("LayoutValue"))]
35pub enum MetadataValue {
36    /// For a DST with `dyn Trait` metadata, this refers to the size found in the metadata.
37    DynSize,
38    /// For a DST with `dyn Trait` metadata, this refers to the alignment found in the metadata.
39    DynAlign,
40    /// For a DST with slice metadata, this refers to the length found in the metadata.
41    SliceLength,
42}
43
44/// An expression that represents a size in bytes.
45#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
46#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
47#[serde_state(state_implements = DedupSerializerState)]
48pub struct SizeExpr(pub HashConsed<WithCachedTypeInfo<SizeExprKind>>);
49
50#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
51#[derive(EnumIsA, EnumAsGetters, VariantName)]
52#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
53#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("SizeExpr"))]
54pub enum SizeExprKind {
55    /// An arbitrary constant of type `usize`.
56    Constant(ConstantExpr),
57    /// Layout information stored in the pointer metadata to this object.
58    FromMetadata(MetadataValue),
59    Max(Vec<SizeExpr>),
60    Min(Vec<SizeExpr>),
61    Plus(SizeExpr, SizeExpr),
62    /// Multiply by a constant.
63    Scale(SizeExpr, ConstantExpr),
64    /// The size is at least the value of this expression.
65    AtLeast(SizeExpr),
66    /// The next multiple of `target_align` from `base`.
67    AlignTo {
68        base: SizeExpr,
69        target_align: SizeExpr,
70    },
71    /// A size expression that depens on whether the given type is inhabited.
72    IfInhabited {
73        ty: Ty,
74        then_size: SizeExpr,
75        else_size: SizeExpr,
76    },
77}
78
79impl SizeExpr {
80    pub fn new(kind: SizeExprKind) -> Self {
81        Self(HashConsed::new(WithCachedTypeInfo::new(kind)))
82    }
83
84    pub fn kind(&self) -> &SizeExprKind {
85        self.0.inner()
86    }
87
88    pub fn with_kind_mut<R>(&mut self, f: impl FnOnce(&mut SizeExprKind) -> R) -> R {
89        self.0.with_inner_mut(|kind| kind.with_value_mut(f))
90    }
91
92    pub fn from_usize(value: u128) -> Self {
93        SizeExprKind::from_usize(value).into_expr()
94    }
95
96    /// The symbolic constant `size_of::<ty>()`.
97    pub fn size_of(ty: &Ty) -> Self {
98        Self::constant(ConstantExprKind::SizeOf(ty.clone()))
99    }
100
101    /// The symbolic constant `align_of::<ty>()`.
102    pub fn align_of(ty: &Ty) -> Self {
103        Self::constant(ConstantExprKind::AlignOf(ty.clone()))
104    }
105
106    /// The symbolic constant `offset_of!(ty, variant.field)`.
107    pub fn offset_of(ty: TypeDeclRef, variant: Option<VariantId>, field: FieldId) -> Self {
108        Self::constant(ConstantExprKind::OffsetOf(ty, variant, field))
109    }
110
111    fn constant(kind: ConstantExprKind) -> Self {
112        SizeExprKind::Constant(ConstantExpr::new(kind, Ty::mk_usize())).into_expr()
113    }
114
115    /// The maximum of the given values; or `default` if the list is empty.
116    pub fn max_or(mut values: Vec<SizeExpr>, default: SizeExpr) -> SizeExpr {
117        match values.len() {
118            0 => default,
119            1 => values.pop().unwrap(),
120            _ => SizeExprKind::Max(values).into_expr(),
121        }
122    }
123
124    /// The maximum of the given values; defaults to 1 if the list is empty.
125    pub fn max_align(values: Vec<SizeExpr>) -> SizeExpr {
126        Self::max_or(values, SizeExpr::from_usize(1))
127    }
128
129    /// The maximum of the given values; defaults to 0 if the list is empty.
130    pub fn max_size(values: Vec<SizeExpr>) -> SizeExpr {
131        Self::max_or(values, SizeExpr::from_usize(0))
132    }
133
134    pub fn align_to(base: SizeExpr, target_align: SizeExpr) -> SizeExpr {
135        SizeExprKind::AlignTo { base, target_align }.into_expr()
136    }
137
138    pub fn at_least(value: SizeExpr) -> SizeExpr {
139        SizeExprKind::AtLeast(value).into_expr()
140    }
141
142    pub fn if_inhabited(ty: &Ty, then_size: SizeExpr, else_size: SizeExpr) -> SizeExpr {
143        SizeExprKind::IfInhabited {
144            ty: ty.clone(),
145            then_size,
146            else_size,
147        }
148        .into_expr()
149    }
150
151    /// Recursively evaluate the parts of this expression that are known in `krate`.
152    /// If `allow_precision_loss` is false, `SizeOf` and `AlignOf` are only replaced with a
153    /// [`SizeExprKind::Constant`].
154    pub fn normalize(
155        mut self,
156        krate: Option<&TranslatedCrate>,
157        for_target: Option<&TargetTriple>,
158        allow_precision_loss: bool,
159    ) -> Self {
160        #[derive(Visitor)]
161        struct NormalizeSizeExpr<'a> {
162            krate: Option<&'a TranslatedCrate>,
163            for_target: Option<&'a TargetTriple>,
164            allow_precision_loss: bool,
165        }
166
167        /// Take out the concrete values from the vec and fold them with the provided function.
168        fn fold_concrete_values(
169            values: &mut Vec<SizeExpr>,
170            f: impl Fn(u128, u128) -> u128,
171        ) -> Option<u128> {
172            values
173                .extract_if(.., |val| val.as_usize().is_some())
174                .map(|val| val.as_usize().unwrap())
175                .reduce(f)
176        }
177
178        fn peel_at_least(value: &SizeExpr) -> (SizeExpr, bool) {
179            if let SizeExprKind::AtLeast(inner) = value.kind() {
180                (inner.clone(), true)
181            } else {
182                (value.clone(), false)
183            }
184        }
185
186        fn rewrap_at_least(kind: SizeExprKind, at_least: bool) -> SizeExprKind {
187            if at_least {
188                SizeExprKind::AtLeast(kind.into_expr())
189            } else {
190                kind
191            }
192        }
193
194        fn as_usize_bound(value: &SizeExpr) -> Option<(u128, bool)> {
195            match value.kind() {
196                SizeExprKind::Constant(constant) => {
197                    constant.as_usize_literal().map(|value| (value, true))
198                }
199                SizeExprKind::AtLeast(inner) => inner.as_usize().map(|value| (value, false)),
200                _ => None,
201            }
202        }
203
204        fn is_aligned_to(value: &SizeExpr, align: u128) -> bool {
205            if align == 0 {
206                return false;
207            }
208            match value.kind() {
209                SizeExprKind::Constant(constant) => constant
210                    .as_usize_literal()
211                    .is_some_and(|value| value % align == 0),
212                SizeExprKind::Scale(_, multiplier) => multiplier
213                    .as_usize_literal()
214                    .is_some_and(|multiplier| multiplier % align == 0),
215                SizeExprKind::AlignTo { target_align, .. } => target_align
216                    .as_usize()
217                    .is_some_and(|target_align| target_align % align == 0),
218                _ => false,
219            }
220        }
221
222        impl VisitAstMut for NormalizeSizeExpr<'_> {
223            fn visit_with_cached_type_info<T: AstVisitable>(
224                &mut self,
225                value: &mut WithCachedTypeInfo<T>,
226            ) -> ControlFlow<Self::Break> {
227                if value.type_info().is_normalized() {
228                    Continue(())
229                } else {
230                    self.visit_inner(value)
231                }
232            }
233
234            fn exit_size_expr_kind(&mut self, expr: &mut SizeExprKind) {
235                *expr = match expr {
236                    SizeExprKind::Constant(constant) => {
237                        debug_assert!(constant.ty().is_usize());
238                        let mut guaranteed = match constant.kind() {
239                            ConstantExprKind::SizeOf(ty) => match ty.kind() {
240                                TyKind::Never => SizeExpr::from_usize(0),
241                                TyKind::DynTrait(..) => {
242                                    SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr()
243                                }
244                                TyKind::Scalar(scalar_ty) => {
245                                    if let Some(krate) = self.krate
246                                        && let Some(target) = self.for_target
247                                        && let Some(target) = krate.target_information.get(target)
248                                    {
249                                        SizeExpr::from_usize(
250                                            scalar_ty.target_size(target.target_pointer_size)
251                                                as u128,
252                                        )
253                                    } else {
254                                        return;
255                                    }
256                                }
257                                _ => {
258                                    if let Some(krate) = self.krate
259                                        && let Some(ty_ref) = ty.as_adt()
260                                        && let Some(decl) = krate.type_decls.get(ty_ref.id)
261                                        && let Some(target) = self.for_target
262                                        && let Some(layout) = decl.layout.get(target)
263                                        && let Some(value) = layout.size.guarantee.clone()
264                                    {
265                                        value.substitute(&ty_ref.generics)
266                                    } else {
267                                        return;
268                                    }
269                                }
270                            },
271                            ConstantExprKind::AlignOf(ty) => match ty.kind() {
272                                TyKind::Never => SizeExpr::from_usize(1),
273                                TyKind::DynTrait(..) => {
274                                    SizeExprKind::FromMetadata(MetadataValue::DynAlign).into_expr()
275                                }
276                                TyKind::Scalar(scalar_ty) => {
277                                    if let Some(krate) = self.krate
278                                        && let Some(target) = self.for_target
279                                        && let Some(target) = krate.target_information.get(target)
280                                        && let Some(value) =
281                                            target.primitive_alignments.get(scalar_ty)
282                                    {
283                                        SizeExpr::from_usize(u128::from(*value))
284                                    } else {
285                                        return;
286                                    }
287                                }
288                                _ => {
289                                    if let Some(krate) = self.krate
290                                        && let Some(ty_ref) = ty.as_adt()
291                                        && let Some(decl) = krate.type_decls.get(ty_ref.id)
292                                        && let Some(target) = self.for_target
293                                        && let Some(layout) = decl.layout.get(target)
294                                        && let Some(value) = layout.align.guarantee.clone()
295                                    {
296                                        value.substitute(&ty_ref.generics)
297                                    } else {
298                                        return;
299                                    }
300                                }
301                            },
302                            _ => return,
303                        };
304                        self.visit(&mut guaranteed);
305                        if !self.allow_precision_loss
306                            && !matches!(
307                                guaranteed.kind(),
308                                SizeExprKind::Constant(_) | SizeExprKind::FromMetadata(_)
309                            )
310                        {
311                            return;
312                        }
313                        guaranteed.kind().clone()
314                    }
315                    SizeExprKind::Max(values) => {
316                        let mut at_least = false;
317                        // Flatten nested operations.
318                        for val in std::mem::take(values) {
319                            let (val, val_at_least) = peel_at_least(&val);
320                            at_least |= val_at_least;
321                            match val.kind() {
322                                SizeExprKind::Max(nested) => values.extend(nested.iter().cloned()),
323                                _ => values.push(val),
324                            }
325                        }
326                        // Get the max of the concrete values.
327                        if let Some(value) = fold_concrete_values(values, std::cmp::max)
328                            && value != 0
329                        {
330                            // Zero is the identity of `Max` so we don't push in that case.
331                            values.push(SizeExpr::from_usize(value));
332                        }
333                        let kind = if values.len() == 1 {
334                            values.pop().unwrap().kind().clone()
335                        } else if values.is_empty() {
336                            SizeExprKind::zero()
337                        } else if at_least {
338                            SizeExprKind::Max(std::mem::take(values))
339                        } else {
340                            return;
341                        };
342                        rewrap_at_least(kind, at_least)
343                    }
344                    SizeExprKind::Min(values) => {
345                        // Flatten nested operations.
346                        for val in std::mem::take(values) {
347                            match val.kind() {
348                                SizeExprKind::Min(nested) => values.extend(nested.iter().cloned()),
349                                _ => values.push(val),
350                            }
351                        }
352                        // Get the min of the concrete values. If the smallest value is an exact
353                        // value, it makes the whole `min` exact. Otherwise, we only get an
354                        // `AtLeast` lower bound.
355                        if let Some((value, exact)) = values
356                            .extract_if(.., |value| as_usize_bound(value).is_some())
357                            .map(|value| as_usize_bound(&value).unwrap())
358                            .reduce(|(left, left_exact), (right, right_exact)| {
359                                match left.cmp(&right) {
360                                    std::cmp::Ordering::Less => (left, left_exact),
361                                    std::cmp::Ordering::Greater => (right, right_exact),
362                                    std::cmp::Ordering::Equal => (left, left_exact || right_exact),
363                                }
364                            })
365                        {
366                            // Zero is absorbing for `Min`.
367                            if value == 0 {
368                                values.clear();
369                            }
370                            let value = SizeExprKind::from_usize(value);
371                            values.push(rewrap_at_least(value, !exact).into_expr());
372                        }
373                        if values.len() == 1 {
374                            values.pop().unwrap().kind().clone()
375                        } else {
376                            return;
377                        }
378                    }
379                    SizeExprKind::Plus(left, right) => {
380                        // Flatten nested sums.
381                        fn flatten_addition(
382                            value: &SizeExpr,
383                            values: &mut Vec<SizeExpr>,
384                            at_least: &mut bool,
385                        ) {
386                            match value.kind() {
387                                SizeExprKind::Plus(left, right) => {
388                                    flatten_addition(left, values, at_least);
389                                    flatten_addition(right, values, at_least);
390                                }
391                                SizeExprKind::AtLeast(inner) => {
392                                    *at_least = true;
393                                    flatten_addition(inner, values, at_least);
394                                }
395                                _ => values.push(value.clone()),
396                            }
397                        }
398                        let mut values = Vec::new();
399                        let mut at_least = false;
400                        flatten_addition(left, &mut values, &mut at_least);
401                        flatten_addition(right, &mut values, &mut at_least);
402
403                        // Sum all the constants and leave the sum at the start.
404                        if let Some(constant) = fold_concrete_values(&mut values, u128::strict_add)
405                            && constant != 0
406                        {
407                            values.insert(0, SizeExpr::from_usize(constant));
408                        }
409                        let kind = if values.len() == 1 {
410                            values.pop().unwrap().kind().clone()
411                        } else if values.is_empty() {
412                            SizeExprKind::zero()
413                        } else {
414                            values
415                                .into_iter()
416                                .reduce(|left, right| SizeExprKind::Plus(left, right).into_expr())
417                                .unwrap()
418                                .kind()
419                                .clone()
420                        };
421                        rewrap_at_least(kind, at_least)
422                    }
423                    SizeExprKind::Scale(base, multiplier) => {
424                        match (base.as_usize(), multiplier.as_usize_literal()) {
425                            (_, Some(0)) | (Some(0), _) => SizeExprKind::zero(),
426                            (_, Some(1)) => base.kind().clone(),
427                            (Some(base), Some(multiplier)) => {
428                                SizeExprKind::from_usize(base.strict_mul(multiplier))
429                            }
430                            _ if let (base, true) = peel_at_least(base) => {
431                                let mut kind = SizeExprKind::Scale(base, multiplier.clone());
432                                self.visit(&mut kind);
433                                rewrap_at_least(kind, true)
434                            }
435                            _ => return,
436                        }
437                    }
438                    SizeExprKind::AlignTo { base, target_align } => {
439                        match (base.as_usize(), target_align.as_usize()) {
440                            (_, Some(1)) => base.kind().clone(),
441                            (Some(base), Some(align)) if align != 0 => {
442                                let remainder = base % align;
443                                SizeExprKind::from_usize(if remainder == 0 {
444                                    base
445                                } else {
446                                    base.strict_add(align - remainder)
447                                })
448                            }
449                            (_, Some(align)) if is_aligned_to(base, align) => base.kind().clone(),
450                            (_, Some(align))
451                                if let SizeExprKind::Plus(left, right) = base.kind()
452                                    && is_aligned_to(left, align) =>
453                            {
454                                // If `left` is a multiple of `align`, then
455                                // `align_to(left + right, align) = left + align_to(right, align)`.
456                                let right = SizeExprKind::AlignTo {
457                                    base: right.clone(),
458                                    target_align: target_align.clone(),
459                                }
460                                .into_expr();
461                                let mut new = SizeExprKind::Plus(left.clone(), right);
462                                self.visit(&mut new);
463                                new
464                            }
465                            _ if let (base, base_at_least) = peel_at_least(base)
466                                && let (target_align, align_at_least) =
467                                    peel_at_least(target_align)
468                                && (base_at_least || align_at_least) =>
469                            {
470                                let mut kind = SizeExprKind::AlignTo { base, target_align };
471                                self.visit(&mut kind);
472                                rewrap_at_least(kind, true)
473                            }
474                            _ => return,
475                        }
476                    }
477                    SizeExprKind::IfInhabited {
478                        ty,
479                        then_size,
480                        else_size,
481                    } => {
482                        if then_size == else_size {
483                            then_size.kind().clone()
484                        } else if let Some(krate) = self.krate
485                            && let Some(inhabited) = ty
486                                .inhabited_predicate(krate, self.for_target)
487                                .normalize(krate, self.for_target)
488                                .as_bool()
489                        {
490                            if inhabited { then_size } else { else_size }.kind().clone()
491                        } else {
492                            return;
493                        }
494                    }
495                    SizeExprKind::AtLeast(inner) => {
496                        if inner.kind().is_at_least() {
497                            inner.kind().clone()
498                        } else {
499                            return;
500                        }
501                    }
502                    SizeExprKind::FromMetadata(_) => return,
503                };
504            }
505        }
506
507        NormalizeSizeExpr {
508            krate,
509            for_target,
510            allow_precision_loss,
511        }
512        .visit(&mut self);
513        self
514    }
515
516    fn as_usize(&self) -> Option<u128> {
517        if let SizeExprKind::Constant(constant) = self.kind() {
518            constant.as_usize_literal()
519        } else {
520            None
521        }
522    }
523}
524
525impl SizeExprKind {
526    pub fn zero() -> Self {
527        Self::from_usize(0)
528    }
529
530    pub fn from_usize(value: u128) -> Self {
531        Self::Constant(ConstantExpr::mk_usize(value))
532    }
533
534    pub fn into_expr(self) -> SizeExpr {
535        SizeExpr::new(self)
536    }
537}
538
539impl From<SizeExprKind> for SizeExpr {
540    fn from(kind: SizeExprKind) -> Self {
541        kind.into_expr()
542    }
543}
544
545impl std::ops::Deref for SizeExpr {
546    type Target = WithCachedTypeInfo<SizeExprKind>;
547    fn deref(&self) -> &Self::Target {
548        &self.0
549    }
550}
551
552#[cfg(test)]
553mod tests {
554    use super::*;
555
556    fn test_krate() -> (TranslatedCrate, TargetTriple) {
557        let mut krate = TranslatedCrate::default();
558        let target = "test-target".to_owned();
559        krate.target_information.insert(
560            target.clone(),
561            TargetInfo {
562                target_pointer_size: 8,
563                is_little_endian: true,
564                c_enum_smallest_repr_ty: IntTy::I32,
565                primitive_alignments: SeqHashMap::new(),
566            },
567        );
568        (krate, target)
569    }
570
571    #[test]
572    fn normalize_arithmetic() {
573        let (krate, target) = test_krate();
574        let expr = SizeExprKind::AlignTo {
575            base: SizeExprKind::Plus(
576                SizeExpr::from_usize(2),
577                SizeExprKind::Scale(SizeExpr::from_usize(3), ConstantExpr::mk_usize(4)).into_expr(),
578            )
579            .into_expr(),
580            target_align: SizeExpr::from_usize(8),
581        }
582        .into_expr()
583        .normalize(Some(&krate), Some(&target), false);
584
585        assert_eq!(expr.as_usize(), Some(16));
586    }
587
588    #[test]
589    fn normalize_additions() {
590        let (krate, target) = test_krate();
591        let dyn_size = SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr();
592        let dyn_align = SizeExprKind::FromMetadata(MetadataValue::DynAlign).into_expr();
593        let expr = SizeExprKind::Plus(
594            dyn_size.clone(),
595            SizeExprKind::Plus(
596                SizeExpr::from_usize(2),
597                SizeExprKind::Plus(dyn_align.clone(), SizeExpr::from_usize(3)).into_expr(),
598            )
599            .into_expr(),
600        )
601        .into_expr()
602        .normalize(Some(&krate), Some(&target), false);
603
604        assert_eq!(
605            expr,
606            SizeExprKind::Plus(
607                SizeExprKind::Plus(SizeExpr::from_usize(5), dyn_size).into_expr(),
608                dyn_align,
609            )
610            .into_expr()
611        );
612    }
613
614    #[test]
615    fn normalize_align_to_with_aligned_prefix() {
616        let (krate, target) = test_krate();
617        let dyn_size = SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr();
618        let dyn_align = SizeExprKind::FromMetadata(MetadataValue::DynAlign).into_expr();
619        let target_align = SizeExpr::from_usize(4);
620
621        let with_constant = SizeExprKind::AlignTo {
622            base: SizeExprKind::Plus(SizeExpr::from_usize(8), dyn_size.clone()).into_expr(),
623            target_align: target_align.clone(),
624        }
625        .into_expr()
626        .normalize(Some(&krate), Some(&target), false);
627        assert_eq!(
628            with_constant,
629            SizeExprKind::Plus(
630                SizeExpr::from_usize(8),
631                SizeExprKind::AlignTo {
632                    base: dyn_size.clone(),
633                    target_align: target_align.clone(),
634                }
635                .into_expr(),
636            )
637            .into_expr()
638        );
639
640        let scaled = SizeExprKind::Scale(dyn_size, ConstantExpr::mk_usize(8)).into_expr();
641        let aligned_scale = SizeExprKind::AlignTo {
642            base: scaled.clone(),
643            target_align: target_align.clone(),
644        }
645        .into_expr()
646        .normalize(Some(&krate), Some(&target), false);
647        assert_eq!(aligned_scale, scaled);
648
649        let inner_align_to = SizeExprKind::AlignTo {
650            base: dyn_align.clone(),
651            target_align: SizeExpr::from_usize(8),
652        }
653        .into_expr();
654        let nested_align_to = SizeExprKind::AlignTo {
655            base: inner_align_to.clone(),
656            target_align: target_align.clone(),
657        }
658        .into_expr()
659        .normalize(Some(&krate), Some(&target), false);
660        assert_eq!(nested_align_to, inner_align_to);
661
662        let insufficient_inner_align = SizeExprKind::AlignTo {
663            base: SizeExprKind::AlignTo {
664                base: dyn_align.clone(),
665                target_align: SizeExpr::from_usize(4),
666            }
667            .into_expr(),
668            target_align: SizeExpr::from_usize(8),
669        }
670        .into_expr();
671        assert_eq!(
672            insufficient_inner_align
673                .clone()
674                .normalize(Some(&krate), Some(&target), false),
675            insufficient_inner_align
676        );
677
678        let with_scale = SizeExprKind::AlignTo {
679            base: SizeExprKind::Plus(scaled.clone(), dyn_align.clone()).into_expr(),
680            target_align: target_align.clone(),
681        }
682        .into_expr()
683        .normalize(Some(&krate), Some(&target), false);
684        assert_eq!(
685            with_scale,
686            SizeExprKind::Plus(
687                scaled,
688                SizeExprKind::AlignTo {
689                    base: dyn_align,
690                    target_align,
691                }
692                .into_expr(),
693            )
694            .into_expr()
695        );
696
697        let unaligned_scale = SizeExprKind::AlignTo {
698            base: SizeExprKind::Plus(
699                SizeExprKind::Scale(
700                    SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr(),
701                    ConstantExpr::mk_usize(6),
702                )
703                .into_expr(),
704                SizeExprKind::FromMetadata(MetadataValue::DynAlign).into_expr(),
705            )
706            .into_expr(),
707            target_align: SizeExpr::from_usize(4),
708        }
709        .into_expr();
710        assert_eq!(
711            unaligned_scale
712                .clone()
713                .normalize(Some(&krate), Some(&target), false),
714            unaligned_scale
715        );
716    }
717
718    #[test]
719    fn normalize_extrema_partially() {
720        let (krate, target) = test_krate();
721        let expr = SizeExprKind::Max(vec![
722            SizeExpr::from_usize(2),
723            SizeExprKind::Max(vec![
724                SizeExpr::from_usize(5),
725                SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr(),
726            ])
727            .into_expr(),
728            SizeExpr::from_usize(3),
729        ])
730        .into_expr()
731        .normalize(Some(&krate), Some(&target), false);
732
733        let SizeExprKind::Max(contenders) = expr.kind() else {
734            panic!("expected a partially normalized maximum")
735        };
736        assert_eq!(contenders.len(), 2);
737        assert_eq!(contenders[1].as_usize(), Some(5));
738        assert!(matches!(
739            contenders[0].kind(),
740            SizeExprKind::FromMetadata(MetadataValue::DynSize)
741        ));
742
743        let empty =
744            SizeExprKind::Max(Vec::new())
745                .into_expr()
746                .normalize(Some(&krate), Some(&target), false);
747        assert_eq!(empty.as_usize(), Some(0));
748    }
749
750    #[test]
751    fn normalize_extrema_identities() {
752        let (krate, target) = test_krate();
753        let max = SizeExprKind::Max(vec![
754            SizeExpr::from_usize(0),
755            SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr(),
756        ])
757        .into_expr()
758        .normalize(Some(&krate), Some(&target), false);
759        let min = SizeExprKind::Min(vec![
760            SizeExpr::from_usize(7),
761            SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr(),
762            SizeExpr::from_usize(0),
763        ])
764        .into_expr()
765        .normalize(Some(&krate), Some(&target), false);
766
767        assert!(matches!(
768            max.kind(),
769            SizeExprKind::FromMetadata(MetadataValue::DynSize)
770        ));
771        assert_eq!(min.as_usize(), Some(0));
772    }
773
774    #[test]
775    fn normalize_lower_bounds() {
776        let normalize = |kind: SizeExprKind| kind.into_expr().normalize(None, None, false);
777        let at_least = |value| SizeExprKind::AtLeast(SizeExpr::from_usize(value)).into_expr();
778        let dyn_size = SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr();
779
780        assert_eq!(
781            normalize(SizeExprKind::Max(vec![at_least(2), dyn_size.clone()])),
782            SizeExprKind::AtLeast(
783                SizeExprKind::Max(vec![dyn_size.clone(), SizeExpr::from_usize(2)]).into_expr()
784            )
785            .into_expr()
786        );
787        assert_eq!(
788            normalize(SizeExprKind::Plus(at_least(2), SizeExpr::from_usize(3))),
789            at_least(5)
790        );
791        assert_eq!(
792            normalize(SizeExprKind::Scale(at_least(2), ConstantExpr::mk_usize(3))),
793            at_least(6)
794        );
795        assert_eq!(
796            normalize(SizeExprKind::AlignTo {
797                base: at_least(5),
798                target_align: SizeExpr::from_usize(4),
799            }),
800            at_least(8)
801        );
802        assert_eq!(
803            normalize(SizeExprKind::Min(vec![
804                at_least(5),
805                SizeExpr::from_usize(3)
806            ])),
807            SizeExpr::from_usize(3)
808        );
809        assert_eq!(
810            normalize(SizeExprKind::Min(vec![
811                at_least(3),
812                SizeExpr::from_usize(5)
813            ])),
814            at_least(3)
815        );
816    }
817
818    #[test]
819    fn normalize_if_inhabited() {
820        let (krate, target) = test_krate();
821        let expr = SizeExprKind::IfInhabited {
822            ty: TyKind::Never.into_ty(),
823            then_size: SizeExpr::from_usize(10),
824            else_size: SizeExprKind::Plus(SizeExpr::from_usize(2), SizeExpr::from_usize(3))
825                .into_expr(),
826        }
827        .into_expr()
828        .normalize(Some(&krate), Some(&target), false);
829
830        assert_eq!(expr.as_usize(), Some(5));
831    }
832
833    #[test]
834    fn normalize_for_the_selected_target() {
835        let mut krate = TranslatedCrate::default();
836        let scalar_ty = ScalarTy::Integer(IntegerTy::Unsigned(UIntTy::U64));
837        for (triple, pointer_size, alignment) in [("a", 4, 4), ("b", 8, 8)] {
838            let mut primitive_alignments = SeqHashMap::new();
839            primitive_alignments.insert(scalar_ty, alignment);
840            krate.target_information.insert(
841                triple.to_owned(),
842                TargetInfo {
843                    target_pointer_size: pointer_size,
844                    is_little_endian: true,
845                    c_enum_smallest_repr_ty: IntTy::I32,
846                    primitive_alignments,
847                },
848            );
849        }
850        let target_a = "a".to_owned();
851        let target_b = "b".to_owned();
852
853        let size = SizeExprKind::Constant(ConstantExpr::new(
854            ConstantExprKind::SizeOf(TyKind::Scalar(scalar_ty).into_ty()),
855            Ty::mk_usize(),
856        ))
857        .into_expr()
858        .normalize(Some(&krate), Some(&target_a), false);
859        let align = SizeExprKind::Constant(ConstantExpr::new(
860            ConstantExprKind::AlignOf(TyKind::Scalar(scalar_ty).into_ty()),
861            Ty::mk_usize(),
862        ))
863        .into_expr()
864        .normalize(Some(&krate), Some(&target_a), false);
865        let pointer_size = SizeExprKind::Constant(ConstantExpr::new(
866            ConstantExprKind::SizeOf(Ty::mk_usize()),
867            Ty::mk_usize(),
868        ))
869        .into_expr();
870        let pointer_size_a = pointer_size
871            .clone()
872            .normalize(Some(&krate), Some(&target_a), false);
873        let pointer_size_b = pointer_size.normalize(Some(&krate), Some(&target_b), false);
874
875        assert_eq!(size.as_usize(), Some(8));
876        assert_eq!(align.as_usize(), Some(4));
877        assert_eq!(pointer_size_a.as_usize(), Some(4));
878        assert_eq!(pointer_size_b.as_usize(), Some(8));
879    }
880
881    #[test]
882    fn normalize_without_a_crate_or_target() {
883        let size_of_usize = SizeExprKind::Constant(ConstantExpr::new(
884            ConstantExprKind::SizeOf(Ty::mk_usize()),
885            Ty::mk_usize(),
886        ))
887        .into_expr();
888        let align_of_u16 = SizeExprKind::Constant(ConstantExpr::new(
889            ConstantExprKind::AlignOf(
890                TyKind::Scalar(ScalarTy::Integer(IntegerTy::Unsigned(UIntTy::U16))).into_ty(),
891            ),
892            Ty::mk_usize(),
893        ))
894        .into_expr();
895
896        assert_eq!(
897            size_of_usize.clone().normalize(None, None, false),
898            size_of_usize
899        );
900        assert_eq!(
901            align_of_u16.clone().normalize(None, None, false),
902            align_of_u16
903        );
904
905        let target_independent = SizeExprKind::Plus(
906            SizeExprKind::Constant(ConstantExpr::new(
907                ConstantExprKind::SizeOf(TyKind::Never.into_ty()),
908                Ty::mk_usize(),
909            ))
910            .into_expr(),
911            SizeExpr::from_usize(4),
912        )
913        .into_expr()
914        .normalize(None, None, false);
915        assert_eq!(target_independent.as_usize(), Some(4));
916    }
917
918    #[test]
919    fn normalize_uses_guarantees_not_chosen_values() {
920        let (mut krate, target) = test_krate();
921        let id = TypeDeclId::ZERO;
922        let mut generics = GenericParams::empty();
923        generics
924            .types
925            .push_with(|id| TypeParam::new(id, "T".to_owned(), Variance::Invariant));
926        let generic_ty = generics.identity_args().types[TypeVarId::ZERO].clone();
927        let mut layouts = SeqHashMap::new();
928        layouts.insert(
929            target.clone(),
930            Layout {
931                size: Size {
932                    chosen: Some(SizeExpr::from_usize(99)),
933                    guarantee: None,
934                },
935                align: Size::new(1),
936                discriminator: None,
937                inhabited: InhabitedPredicate::mk_true(),
938                variant_layouts: Default::default(),
939                repr: Default::default(),
940            },
941        );
942        krate.type_decls.insert(
943            id,
944            TypeDecl {
945                def_id: id,
946                item_meta: ItemMeta::dummy_public(
947                    Span::default(),
948                    Name::from_path(&["T"]),
949                    true,
950                    ItemOpacity::Transparent,
951                ),
952                generics,
953                src: TypeSource::Normal,
954                kind: TypeDeclKind::Opaque,
955                layout: layouts,
956                ptr_metadata: PtrMetadata::None,
957                marker_traits: None,
958            },
959        );
960        let ty = TyKind::Adt(TypeDeclRef::new(
961            id,
962            GenericArgs::new_types(
963                [TyKind::Scalar(ScalarTy::Integer(IntegerTy::Unsigned(UIntTy::U16))).into_ty()]
964                    .into_iter()
965                    .collect(),
966            ),
967            None,
968        ))
969        .into_ty();
970        let size_of = || {
971            SizeExprKind::Constant(ConstantExpr::new(
972                ConstantExprKind::SizeOf(ty.clone()),
973                Ty::mk_usize(),
974            ))
975            .into_expr()
976        };
977        let align_of = || {
978            SizeExprKind::Constant(ConstantExpr::new(
979                ConstantExprKind::AlignOf(ty.clone()),
980                Ty::mk_usize(),
981            ))
982            .into_expr()
983        };
984
985        let without_guarantee = size_of().normalize(Some(&krate), Some(&target), false);
986        assert!(matches!(
987            without_guarantee.kind(),
988            SizeExprKind::Constant(constant)
989                if matches!(constant.kind(), ConstantExprKind::SizeOf(_))
990        ));
991
992        {
993            let layout = &mut krate.type_decls.get_mut(id).unwrap().layout[&target];
994            layout.size.guarantee =
995                Some(SizeExprKind::AtLeast(SizeExpr::from_usize(2)).into_expr());
996            layout.align.guarantee =
997                Some(SizeExprKind::AtLeast(SizeExpr::from_usize(1)).into_expr());
998        }
999
1000        let size_without_precision_loss = size_of().normalize(Some(&krate), Some(&target), false);
1001        assert!(matches!(
1002            size_without_precision_loss.kind(),
1003            SizeExprKind::Constant(constant)
1004                if matches!(constant.kind(), ConstantExprKind::SizeOf(_))
1005        ));
1006        let align_without_precision_loss = align_of().normalize(Some(&krate), Some(&target), false);
1007        assert!(matches!(
1008            align_without_precision_loss.kind(),
1009            SizeExprKind::Constant(constant)
1010                if matches!(constant.kind(), ConstantExprKind::AlignOf(_))
1011        ));
1012
1013        let size_with_precision_loss = size_of().normalize(Some(&krate), Some(&target), true);
1014        assert!(matches!(
1015            size_with_precision_loss.kind(),
1016            SizeExprKind::AtLeast(value) if value.as_usize() == Some(2)
1017        ));
1018        let align_with_precision_loss = align_of().normalize(Some(&krate), Some(&target), true);
1019        assert!(matches!(
1020            align_with_precision_loss.kind(),
1021            SizeExprKind::AtLeast(value) if value.as_usize() == Some(1)
1022        ));
1023
1024        let size = &mut krate.type_decls.get_mut(id).unwrap().layout[&target].size;
1025        size.guarantee = Some(
1026            SizeExprKind::Plus(
1027                SizeExprKind::Constant(ConstantExpr::new(
1028                    ConstantExprKind::SizeOf(generic_ty),
1029                    Ty::mk_usize(),
1030                ))
1031                .into_expr(),
1032                SizeExpr::from_usize(5),
1033            )
1034            .into_expr(),
1035        );
1036        let with_guarantee = size_of().normalize(Some(&krate), Some(&target), false);
1037        assert_eq!(with_guarantee.as_usize(), Some(7));
1038    }
1039}
charon_lib/ast/items/layout_guarantees.rs

charon_lib/ast/items/
layout_guarantees.rs
