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                arch: from_rustc::Arch::Other("test".into()),
563                vendor: "unknown".to_owned(),
564                os: from_rustc::Os::Unknown,
565                env: from_rustc::Env::Unspecified,
566                cfg_abi: from_rustc::CfgAbi::Unspecified,
567                target_pointer_size: 8,
568                is_little_endian: true,
569                c_enum_smallest_repr_ty: IntTy::I32,
570                primitive_alignments: SeqHashMap::new(),
571            },
572        );
573        (krate, target)
574    }
575
576    #[test]
577    fn normalize_arithmetic() {
578        let (krate, target) = test_krate();
579        let expr = SizeExprKind::AlignTo {
580            base: SizeExprKind::Plus(
581                SizeExpr::from_usize(2),
582                SizeExprKind::Scale(SizeExpr::from_usize(3), ConstantExpr::mk_usize(4)).into_expr(),
583            )
584            .into_expr(),
585            target_align: SizeExpr::from_usize(8),
586        }
587        .into_expr()
588        .normalize(Some(&krate), Some(&target), false);
589
590        assert_eq!(expr.as_usize(), Some(16));
591    }
592
593    #[test]
594    fn normalize_additions() {
595        let (krate, target) = test_krate();
596        let dyn_size = SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr();
597        let dyn_align = SizeExprKind::FromMetadata(MetadataValue::DynAlign).into_expr();
598        let expr = SizeExprKind::Plus(
599            dyn_size.clone(),
600            SizeExprKind::Plus(
601                SizeExpr::from_usize(2),
602                SizeExprKind::Plus(dyn_align.clone(), SizeExpr::from_usize(3)).into_expr(),
603            )
604            .into_expr(),
605        )
606        .into_expr()
607        .normalize(Some(&krate), Some(&target), false);
608
609        assert_eq!(
610            expr,
611            SizeExprKind::Plus(
612                SizeExprKind::Plus(SizeExpr::from_usize(5), dyn_size).into_expr(),
613                dyn_align,
614            )
615            .into_expr()
616        );
617    }
618
619    #[test]
620    fn normalize_align_to_with_aligned_prefix() {
621        let (krate, target) = test_krate();
622        let dyn_size = SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr();
623        let dyn_align = SizeExprKind::FromMetadata(MetadataValue::DynAlign).into_expr();
624        let target_align = SizeExpr::from_usize(4);
625
626        let with_constant = SizeExprKind::AlignTo {
627            base: SizeExprKind::Plus(SizeExpr::from_usize(8), dyn_size.clone()).into_expr(),
628            target_align: target_align.clone(),
629        }
630        .into_expr()
631        .normalize(Some(&krate), Some(&target), false);
632        assert_eq!(
633            with_constant,
634            SizeExprKind::Plus(
635                SizeExpr::from_usize(8),
636                SizeExprKind::AlignTo {
637                    base: dyn_size.clone(),
638                    target_align: target_align.clone(),
639                }
640                .into_expr(),
641            )
642            .into_expr()
643        );
644
645        let scaled = SizeExprKind::Scale(dyn_size, ConstantExpr::mk_usize(8)).into_expr();
646        let aligned_scale = SizeExprKind::AlignTo {
647            base: scaled.clone(),
648            target_align: target_align.clone(),
649        }
650        .into_expr()
651        .normalize(Some(&krate), Some(&target), false);
652        assert_eq!(aligned_scale, scaled);
653
654        let inner_align_to = SizeExprKind::AlignTo {
655            base: dyn_align.clone(),
656            target_align: SizeExpr::from_usize(8),
657        }
658        .into_expr();
659        let nested_align_to = SizeExprKind::AlignTo {
660            base: inner_align_to.clone(),
661            target_align: target_align.clone(),
662        }
663        .into_expr()
664        .normalize(Some(&krate), Some(&target), false);
665        assert_eq!(nested_align_to, inner_align_to);
666
667        let insufficient_inner_align = SizeExprKind::AlignTo {
668            base: SizeExprKind::AlignTo {
669                base: dyn_align.clone(),
670                target_align: SizeExpr::from_usize(4),
671            }
672            .into_expr(),
673            target_align: SizeExpr::from_usize(8),
674        }
675        .into_expr();
676        assert_eq!(
677            insufficient_inner_align
678                .clone()
679                .normalize(Some(&krate), Some(&target), false),
680            insufficient_inner_align
681        );
682
683        let with_scale = SizeExprKind::AlignTo {
684            base: SizeExprKind::Plus(scaled.clone(), dyn_align.clone()).into_expr(),
685            target_align: target_align.clone(),
686        }
687        .into_expr()
688        .normalize(Some(&krate), Some(&target), false);
689        assert_eq!(
690            with_scale,
691            SizeExprKind::Plus(
692                scaled,
693                SizeExprKind::AlignTo {
694                    base: dyn_align,
695                    target_align,
696                }
697                .into_expr(),
698            )
699            .into_expr()
700        );
701
702        let unaligned_scale = SizeExprKind::AlignTo {
703            base: SizeExprKind::Plus(
704                SizeExprKind::Scale(
705                    SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr(),
706                    ConstantExpr::mk_usize(6),
707                )
708                .into_expr(),
709                SizeExprKind::FromMetadata(MetadataValue::DynAlign).into_expr(),
710            )
711            .into_expr(),
712            target_align: SizeExpr::from_usize(4),
713        }
714        .into_expr();
715        assert_eq!(
716            unaligned_scale
717                .clone()
718                .normalize(Some(&krate), Some(&target), false),
719            unaligned_scale
720        );
721    }
722
723    #[test]
724    fn normalize_extrema_partially() {
725        let (krate, target) = test_krate();
726        let expr = SizeExprKind::Max(vec![
727            SizeExpr::from_usize(2),
728            SizeExprKind::Max(vec![
729                SizeExpr::from_usize(5),
730                SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr(),
731            ])
732            .into_expr(),
733            SizeExpr::from_usize(3),
734        ])
735        .into_expr()
736        .normalize(Some(&krate), Some(&target), false);
737
738        let SizeExprKind::Max(contenders) = expr.kind() else {
739            panic!("expected a partially normalized maximum")
740        };
741        assert_eq!(contenders.len(), 2);
742        assert_eq!(contenders[1].as_usize(), Some(5));
743        assert!(matches!(
744            contenders[0].kind(),
745            SizeExprKind::FromMetadata(MetadataValue::DynSize)
746        ));
747
748        let empty =
749            SizeExprKind::Max(Vec::new())
750                .into_expr()
751                .normalize(Some(&krate), Some(&target), false);
752        assert_eq!(empty.as_usize(), Some(0));
753    }
754
755    #[test]
756    fn normalize_extrema_identities() {
757        let (krate, target) = test_krate();
758        let max = SizeExprKind::Max(vec![
759            SizeExpr::from_usize(0),
760            SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr(),
761        ])
762        .into_expr()
763        .normalize(Some(&krate), Some(&target), false);
764        let min = SizeExprKind::Min(vec![
765            SizeExpr::from_usize(7),
766            SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr(),
767            SizeExpr::from_usize(0),
768        ])
769        .into_expr()
770        .normalize(Some(&krate), Some(&target), false);
771
772        assert!(matches!(
773            max.kind(),
774            SizeExprKind::FromMetadata(MetadataValue::DynSize)
775        ));
776        assert_eq!(min.as_usize(), Some(0));
777    }
778
779    #[test]
780    fn normalize_lower_bounds() {
781        let normalize = |kind: SizeExprKind| kind.into_expr().normalize(None, None, false);
782        let at_least = |value| SizeExprKind::AtLeast(SizeExpr::from_usize(value)).into_expr();
783        let dyn_size = SizeExprKind::FromMetadata(MetadataValue::DynSize).into_expr();
784
785        assert_eq!(
786            normalize(SizeExprKind::Max(vec![at_least(2), dyn_size.clone()])),
787            SizeExprKind::AtLeast(
788                SizeExprKind::Max(vec![dyn_size.clone(), SizeExpr::from_usize(2)]).into_expr()
789            )
790            .into_expr()
791        );
792        assert_eq!(
793            normalize(SizeExprKind::Plus(at_least(2), SizeExpr::from_usize(3))),
794            at_least(5)
795        );
796        assert_eq!(
797            normalize(SizeExprKind::Scale(at_least(2), ConstantExpr::mk_usize(3))),
798            at_least(6)
799        );
800        assert_eq!(
801            normalize(SizeExprKind::AlignTo {
802                base: at_least(5),
803                target_align: SizeExpr::from_usize(4),
804            }),
805            at_least(8)
806        );
807        assert_eq!(
808            normalize(SizeExprKind::Min(vec![
809                at_least(5),
810                SizeExpr::from_usize(3)
811            ])),
812            SizeExpr::from_usize(3)
813        );
814        assert_eq!(
815            normalize(SizeExprKind::Min(vec![
816                at_least(3),
817                SizeExpr::from_usize(5)
818            ])),
819            at_least(3)
820        );
821    }
822
823    #[test]
824    fn normalize_if_inhabited() {
825        let (krate, target) = test_krate();
826        let expr = SizeExprKind::IfInhabited {
827            ty: TyKind::Never.into_ty(),
828            then_size: SizeExpr::from_usize(10),
829            else_size: SizeExprKind::Plus(SizeExpr::from_usize(2), SizeExpr::from_usize(3))
830                .into_expr(),
831        }
832        .into_expr()
833        .normalize(Some(&krate), Some(&target), false);
834
835        assert_eq!(expr.as_usize(), Some(5));
836    }
837
838    #[test]
839    fn normalize_for_the_selected_target() {
840        let mut krate = TranslatedCrate::default();
841        let scalar_ty = ScalarTy::Integer(IntegerTy::Unsigned(UIntTy::U64));
842        for (triple, pointer_size, alignment) in [("a", 4, 4), ("b", 8, 8)] {
843            let mut primitive_alignments = SeqHashMap::new();
844            primitive_alignments.insert(scalar_ty, alignment);
845            krate.target_information.insert(
846                triple.to_owned(),
847                TargetInfo {
848                    arch: from_rustc::Arch::Other("test".into()),
849                    vendor: "unknown".to_owned(),
850                    os: from_rustc::Os::Unknown,
851                    env: from_rustc::Env::Unspecified,
852                    cfg_abi: from_rustc::CfgAbi::Unspecified,
853                    target_pointer_size: pointer_size,
854                    is_little_endian: true,
855                    c_enum_smallest_repr_ty: IntTy::I32,
856                    primitive_alignments,
857                },
858            );
859        }
860        let target_a = "a".to_owned();
861        let target_b = "b".to_owned();
862
863        let size = SizeExprKind::Constant(ConstantExpr::new(
864            ConstantExprKind::SizeOf(TyKind::Scalar(scalar_ty).into_ty()),
865            Ty::mk_usize(),
866        ))
867        .into_expr()
868        .normalize(Some(&krate), Some(&target_a), false);
869        let align = SizeExprKind::Constant(ConstantExpr::new(
870            ConstantExprKind::AlignOf(TyKind::Scalar(scalar_ty).into_ty()),
871            Ty::mk_usize(),
872        ))
873        .into_expr()
874        .normalize(Some(&krate), Some(&target_a), false);
875        let pointer_size = SizeExprKind::Constant(ConstantExpr::new(
876            ConstantExprKind::SizeOf(Ty::mk_usize()),
877            Ty::mk_usize(),
878        ))
879        .into_expr();
880        let pointer_size_a = pointer_size
881            .clone()
882            .normalize(Some(&krate), Some(&target_a), false);
883        let pointer_size_b = pointer_size.normalize(Some(&krate), Some(&target_b), false);
884
885        assert_eq!(size.as_usize(), Some(8));
886        assert_eq!(align.as_usize(), Some(4));
887        assert_eq!(pointer_size_a.as_usize(), Some(4));
888        assert_eq!(pointer_size_b.as_usize(), Some(8));
889    }
890
891    #[test]
892    fn normalize_without_a_crate_or_target() {
893        let size_of_usize = SizeExprKind::Constant(ConstantExpr::new(
894            ConstantExprKind::SizeOf(Ty::mk_usize()),
895            Ty::mk_usize(),
896        ))
897        .into_expr();
898        let align_of_u16 = SizeExprKind::Constant(ConstantExpr::new(
899            ConstantExprKind::AlignOf(
900                TyKind::Scalar(ScalarTy::Integer(IntegerTy::Unsigned(UIntTy::U16))).into_ty(),
901            ),
902            Ty::mk_usize(),
903        ))
904        .into_expr();
905
906        assert_eq!(
907            size_of_usize.clone().normalize(None, None, false),
908            size_of_usize
909        );
910        assert_eq!(
911            align_of_u16.clone().normalize(None, None, false),
912            align_of_u16
913        );
914
915        let target_independent = SizeExprKind::Plus(
916            SizeExprKind::Constant(ConstantExpr::new(
917                ConstantExprKind::SizeOf(TyKind::Never.into_ty()),
918                Ty::mk_usize(),
919            ))
920            .into_expr(),
921            SizeExpr::from_usize(4),
922        )
923        .into_expr()
924        .normalize(None, None, false);
925        assert_eq!(target_independent.as_usize(), Some(4));
926    }
927
928    #[test]
929    fn normalize_uses_guarantees_not_chosen_values() {
930        let (mut krate, target) = test_krate();
931        let id = TypeDeclId::ZERO;
932        let mut generics = GenericParams::empty();
933        generics
934            .types
935            .push_with(|id| TypeParam::new(id, "T".to_owned(), Variance::Invariant));
936        let generic_ty = generics.identity_args().types[TypeVarId::ZERO].clone();
937        let mut layouts = SeqHashMap::new();
938        layouts.insert(
939            target.clone(),
940            Layout {
941                size: Size {
942                    chosen: Some(SizeExpr::from_usize(99)),
943                    guarantee: None,
944                },
945                align: Size::new(1),
946                discriminator: None,
947                inhabited: InhabitedPredicate::mk_true(),
948                variant_layouts: Default::default(),
949                repr: Default::default(),
950            },
951        );
952        krate.type_decls.insert(
953            id,
954            TypeDecl {
955                def_id: id,
956                item_meta: ItemMeta::dummy_public(
957                    Span::default(),
958                    Name::from_path(&["T"]),
959                    true,
960                    ItemOpacity::Transparent,
961                ),
962                generics,
963                src: TypeSource::Normal,
964                kind: TypeDeclKind::Opaque,
965                layout: layouts,
966                ptr_metadata: PtrMetadata::None,
967                marker_traits: None,
968            },
969        );
970        let ty = TyKind::Adt(TypeDeclRef::new(
971            id,
972            GenericArgs::new_types(
973                [TyKind::Scalar(ScalarTy::Integer(IntegerTy::Unsigned(UIntTy::U16))).into_ty()]
974                    .into_iter()
975                    .collect(),
976            ),
977            None,
978        ))
979        .into_ty();
980        let size_of = || {
981            SizeExprKind::Constant(ConstantExpr::new(
982                ConstantExprKind::SizeOf(ty.clone()),
983                Ty::mk_usize(),
984            ))
985            .into_expr()
986        };
987        let align_of = || {
988            SizeExprKind::Constant(ConstantExpr::new(
989                ConstantExprKind::AlignOf(ty.clone()),
990                Ty::mk_usize(),
991            ))
992            .into_expr()
993        };
994
995        let without_guarantee = size_of().normalize(Some(&krate), Some(&target), false);
996        assert!(matches!(
997            without_guarantee.kind(),
998            SizeExprKind::Constant(constant)
999                if matches!(constant.kind(), ConstantExprKind::SizeOf(_))
1000        ));
1001
1002        {
1003            let layout = &mut krate.type_decls.get_mut(id).unwrap().layout[&target];
1004            layout.size.guarantee =
1005                Some(SizeExprKind::AtLeast(SizeExpr::from_usize(2)).into_expr());
1006            layout.align.guarantee =
1007                Some(SizeExprKind::AtLeast(SizeExpr::from_usize(1)).into_expr());
1008        }
1009
1010        let size_without_precision_loss = size_of().normalize(Some(&krate), Some(&target), false);
1011        assert!(matches!(
1012            size_without_precision_loss.kind(),
1013            SizeExprKind::Constant(constant)
1014                if matches!(constant.kind(), ConstantExprKind::SizeOf(_))
1015        ));
1016        let align_without_precision_loss = align_of().normalize(Some(&krate), Some(&target), false);
1017        assert!(matches!(
1018            align_without_precision_loss.kind(),
1019            SizeExprKind::Constant(constant)
1020                if matches!(constant.kind(), ConstantExprKind::AlignOf(_))
1021        ));
1022
1023        let size_with_precision_loss = size_of().normalize(Some(&krate), Some(&target), true);
1024        assert!(matches!(
1025            size_with_precision_loss.kind(),
1026            SizeExprKind::AtLeast(value) if value.as_usize() == Some(2)
1027        ));
1028        let align_with_precision_loss = align_of().normalize(Some(&krate), Some(&target), true);
1029        assert!(matches!(
1030            align_with_precision_loss.kind(),
1031            SizeExprKind::AtLeast(value) if value.as_usize() == Some(1)
1032        ));
1033
1034        let size = &mut krate.type_decls.get_mut(id).unwrap().layout[&target].size;
1035        size.guarantee = Some(
1036            SizeExprKind::Plus(
1037                SizeExprKind::Constant(ConstantExpr::new(
1038                    ConstantExprKind::SizeOf(generic_ty),
1039                    Ty::mk_usize(),
1040                ))
1041                .into_expr(),
1042                SizeExpr::from_usize(5),
1043            )
1044            .into_expr(),
1045        );
1046        let with_guarantee = size_of().normalize(Some(&krate), Some(&target), false);
1047        assert_eq!(with_guarantee.as_usize(), Some(7));
1048    }
1049}
charon_lib/ast/items/layout_guarantees.rs

charon_lib/ast/items/
layout_guarantees.rs
