charon_driver/translate/
translate_types.rs

1use itertools::Itertools;
2use rustc_middle::ty;
3use rustc_span::sym;
4
5use super::translate_ctx::*;
6use crate::hax;
7use crate::hax::{HasOwner, HasParamEnv, Visibility};
8use charon_lib::ast::*;
9use charon_lib::ids::IndexVec;
10
11impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
12    /// Translate an erased region. If we're inside a body, this will return a fresh body region
13    /// instead.
14    pub(crate) fn translate_erased_region(&mut self) -> Region {
15        if let Some(v) = &mut self.lifetime_freshener {
16            Region::Body(v.push(()))
17        } else {
18            Region::Erased
19        }
20    }
21
22    /// Erase a region binder by supplying erased lifetimes (or fresh body lifetimes) for all its
23    /// arguments.
24    pub(crate) fn erase_region_binder<T: TyVisitable>(&mut self, b: RegionBinder<T>) -> T {
25        let regions = b
26            .regions
27            .map_ref_indexed(|_, _| self.translate_erased_region());
28        b.apply(regions)
29    }
30
31    // Translate a region
32    pub(crate) fn translate_region(
33        &mut self,
34        span: Span,
35        region: &hax::Region,
36    ) -> Result<Region, Error> {
37        use crate::hax::RegionKind::*;
38        match &region.kind {
39            ReErased => Ok(self.translate_erased_region()),
40            ReStatic => Ok(Region::Static),
41            ReBound(hax::BoundVarIndexKind::Bound(id), br) => {
42                Ok(match self.lookup_bound_region(span, *id, br.var) {
43                    Ok(var) => Region::Var(var),
44                    Err(_) => Region::Erased,
45                })
46            }
47            ReEarlyParam(region) => Ok(match self.lookup_early_region(span, region) {
48                Ok(var) => Region::Var(var),
49                Err(_) => Region::Erased,
50            }),
51            ReVar(..) | RePlaceholder(..) => {
52                // Shouldn't exist outside of type inference.
53                raise_error!(
54                    self,
55                    span,
56                    "Should not exist outside of type inference: {region:?}"
57                )
58            }
59            ReBound(..) | ReLateParam(..) | ReError(..) => {
60                raise_error!(self, span, "Unexpected region kind: {region:?}")
61            }
62        }
63    }
64
65    pub(crate) fn translate_hax_int_ty(int_ty: &hax::IntTy) -> IntTy {
66        match int_ty {
67            hax::IntTy::Isize => IntTy::Isize,
68            hax::IntTy::I8 => IntTy::I8,
69            hax::IntTy::I16 => IntTy::I16,
70            hax::IntTy::I32 => IntTy::I32,
71            hax::IntTy::I64 => IntTy::I64,
72            hax::IntTy::I128 => IntTy::I128,
73        }
74    }
75
76    pub(crate) fn translate_hax_uint_ty(uint_ty: &hax::UintTy) -> UIntTy {
77        use crate::hax::UintTy;
78        match uint_ty {
79            UintTy::Usize => UIntTy::Usize,
80            UintTy::U8 => UIntTy::U8,
81            UintTy::U16 => UIntTy::U16,
82            UintTy::U32 => UIntTy::U32,
83            UintTy::U64 => UIntTy::U64,
84            UintTy::U128 => UIntTy::U128,
85        }
86    }
87
88    /// Translate a Ty.
89    ///
90    /// Typically used in this module to translate the fields of a structure/
91    /// enumeration definition, or later to translate the type of a variable.
92    ///
93    /// Note that we take as parameter a function to translate regions, because
94    /// regions can be translated in several manners (non-erased region or erased
95    /// regions), in which case the return type is different.
96    #[tracing::instrument(skip(self, span))]
97    pub(crate) fn translate_ty(&mut self, span: Span, hax_ty: &hax::Ty) -> Result<Ty, Error> {
98        let mut ty = if let Some(ty) = self
99            .innermost_binder()
100            .type_trans_cache
101            .get(hax_ty)
102            .cloned()
103        {
104            ty
105        } else {
106            let ty = self
107                .translate_ty_inner(span, hax_ty)
108                .unwrap_or_else(|e| TyKind::Error(e.msg).into_ty());
109            self.innermost_binder_mut()
110                .type_trans_cache
111                .insert(hax_ty.clone(), ty.clone());
112            ty
113        };
114        if let Some(v) = &mut self.lifetime_freshener {
115            // We might be reusing a value from cache: we must refresh the erased & body regions.
116            ty = ty.replace_erased_regions(|| Region::Body(v.push(())));
117        }
118        Ok(ty)
119    }
120
121    fn translate_ty_inner(&mut self, span: Span, ty: &hax::Ty) -> Result<Ty, Error> {
122        trace!("{:?}", ty);
123        let kind = match ty.kind() {
124            hax::TyKind::Bool => TyKind::Literal(LiteralTy::Bool),
125            hax::TyKind::Char => TyKind::Literal(LiteralTy::Char),
126            hax::TyKind::Int(int_ty) => {
127                TyKind::Literal(LiteralTy::Int(Self::translate_hax_int_ty(int_ty)))
128            }
129            hax::TyKind::Uint(uint_ty) => {
130                TyKind::Literal(LiteralTy::UInt(Self::translate_hax_uint_ty(uint_ty)))
131            }
132            hax::TyKind::Float(float_ty) => {
133                use crate::hax::FloatTy;
134                TyKind::Literal(LiteralTy::Float(match float_ty {
135                    FloatTy::F16 => types::FloatTy::F16,
136                    FloatTy::F32 => types::FloatTy::F32,
137                    FloatTy::F64 => types::FloatTy::F64,
138                    FloatTy::F128 => types::FloatTy::F128,
139                }))
140            }
141            hax::TyKind::Never => TyKind::Never,
142
143            hax::TyKind::Alias(alias) => match &alias.kind {
144                hax::AliasKind::Projection {
145                    impl_expr,
146                    assoc_item,
147                } => {
148                    let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
149                    let name = self.t_ctx.translate_trait_item_name(&assoc_item.def_id)?;
150                    TyKind::TraitType(trait_ref, name)
151                }
152                hax::AliasKind::Opaque { hidden_ty, .. } => {
153                    return self.translate_ty(span, hidden_ty);
154                }
155                _ => {
156                    raise_error!(self, span, "Unsupported alias type: {:?}", alias.kind)
157                }
158            },
159
160            hax::TyKind::Adt(item) => {
161                let tref = self.translate_type_decl_ref(span, item)?;
162                TyKind::Adt(tref)
163            }
164            hax::TyKind::Str => {
165                let tref = TypeDeclRef::new(TypeId::Builtin(BuiltinTy::Str), GenericArgs::empty());
166                TyKind::Adt(tref)
167            }
168            hax::TyKind::Array(item_ref) => {
169                let mut args = self.translate_generic_args(span, &item_ref.generic_args, &[])?;
170                assert!(args.types.len() == 1 && args.const_generics.len() == 1);
171                TyKind::Array(
172                    args.types.pop().unwrap(),
173                    Box::new(args.const_generics.pop().unwrap()),
174                )
175            }
176            hax::TyKind::Slice(item_ref) => {
177                let mut args = self.translate_generic_args(span, &item_ref.generic_args, &[])?;
178                assert!(args.types.len() == 1);
179                TyKind::Slice(args.types.pop().unwrap())
180            }
181            hax::TyKind::Tuple(item_ref) => {
182                let args = self.translate_generic_args(span, &item_ref.generic_args, &[])?;
183                let tref = TypeDeclRef::new(TypeId::Tuple, args);
184                TyKind::Adt(tref)
185            }
186            hax::TyKind::Ref(region, ty, mutability) => {
187                trace!("Ref");
188
189                let region = self.translate_region(span, region)?;
190                let ty = self.translate_ty(span, ty)?;
191                let kind = if mutability.is_mut() {
192                    RefKind::Mut
193                } else {
194                    RefKind::Shared
195                };
196                TyKind::Ref(region, ty, kind)
197            }
198            hax::TyKind::RawPtr(ty, mutbl) => {
199                trace!("RawPtr: {:?}", (ty, mutbl));
200                let ty = self.translate_ty(span, ty)?;
201                let kind = if mutbl.is_mut() {
202                    RefKind::Mut
203                } else {
204                    RefKind::Shared
205                };
206                TyKind::RawPtr(ty, kind)
207            }
208
209            hax::TyKind::Param(param) => {
210                // A type parameter, for example `T` in `fn f<T>(x : T) {}`.
211                // Note that this type parameter may actually have been
212                // instantiated (in our environment, we may map it to another
213                // type): we just have to look it up.
214                // Note that if we are using this function to translate a field
215                // type in a type definition, it should actually map to a type
216                // parameter.
217                match self.lookup_type_var(span, param) {
218                    Ok(var) => TyKind::TypeVar(var),
219                    Err(err) => TyKind::Error(err.msg),
220                }
221            }
222
223            hax::TyKind::Foreign(item) => {
224                let tref = self.translate_type_decl_ref(span, item)?;
225                TyKind::Adt(tref)
226            }
227
228            hax::TyKind::Arrow(sig) => {
229                trace!("Arrow");
230                trace!("bound vars: {:?}", sig.bound_vars);
231                let sig = self.translate_poly_fun_sig(span, sig)?;
232                TyKind::FnPtr(sig)
233            }
234            hax::TyKind::FnDef { item, .. } => {
235                let fnref = self.translate_bound_fn_ptr(span, item, TransItemSourceKind::Fun)?;
236                TyKind::FnDef(fnref)
237            }
238            hax::TyKind::Closure(args) => {
239                let tref = self.translate_closure_type_ref(span, args)?;
240                TyKind::Adt(tref)
241            }
242
243            hax::TyKind::Dynamic(dyn_binder, region) => {
244                // self.check_no_monomorphize(span)?;
245                // Translate the region outside the binder.
246                let region = self.translate_region(span, region)?;
247
248                let binder = self.translate_dyn_binder(span, dyn_binder, |ctx, ty, ()| {
249                    let region = region.move_under_binder();
250                    ctx.innermost_binder_mut()
251                        .params
252                        .types_outlive
253                        .push(RegionBinder::empty(OutlivesPred(ty.clone(), region)));
254                    Ok(ty)
255                })?;
256
257                if let hax::ClauseKind::Trait(trait_predicate) = dyn_binder.predicates.predicates[0]
258                    .clause
259                    .kind
260                    .hax_skip_binder_ref()
261                {
262                    // TODO(dyn): for now, we consider traits with associated types to not be dyn
263                    // compatible because we don't know how to handle them; for these we skip
264                    // translating the vtable.
265                    if self.trait_is_dyn_compatible(&trait_predicate.trait_ref.def_id)? {
266                        // Ensure the vtable type is translated. The first predicate is the one that
267                        // can have methods, i.e. a vtable.
268                        if self.monomorphize() {
269                            let item_src = TransItemSource::monomorphic_trait(
270                                &trait_predicate.trait_ref.def_id,
271                                TransItemSourceKind::VTable,
272                            );
273                            let _: TypeDeclId = self.register_and_enqueue(span, item_src);
274                        } else {
275                            let _: TypeDeclId = self.register_item(
276                                span,
277                                &trait_predicate.trait_ref,
278                                TransItemSourceKind::VTable,
279                            );
280                        }
281                    }
282                }
283                TyKind::DynTrait(DynPredicate { binder })
284            }
285
286            hax::TyKind::Infer(_) => {
287                raise_error!(self, span, "Unsupported type: infer type")
288            }
289            hax::TyKind::Coroutine(..) => {
290                raise_error!(self, span, "Coroutine types are not supported yet")
291            }
292            hax::TyKind::Bound(_, _) => {
293                raise_error!(self, span, "Unexpected type kind: bound")
294            }
295            hax::TyKind::Placeholder(_) => {
296                raise_error!(self, span, "Unsupported type: placeholder")
297            }
298
299            hax::TyKind::Error => {
300                raise_error!(self, span, "Type checking error")
301            }
302            hax::TyKind::Todo(s) => {
303                raise_error!(self, span, "Unsupported type: {:?}", s)
304            }
305        };
306        Ok(kind.into_ty())
307    }
308
309    pub(crate) fn translate_rustc_ty(
310        &mut self,
311        span: Span,
312        ty: &ty::Ty<'tcx>,
313    ) -> Result<Ty, Error> {
314        let ty = self.t_ctx.catch_sinto(&self.hax_state, span, ty)?;
315        self.translate_ty(span, &ty)
316    }
317
318    pub fn translate_poly_fun_sig(
319        &mut self,
320        span: Span,
321        sig: &hax::Binder<hax::TyFnSig>,
322    ) -> Result<RegionBinder<FunSig>, Error> {
323        self.translate_region_binder(span, sig, |ctx, sig| ctx.translate_fun_sig(span, sig))
324    }
325    pub fn translate_fun_sig(&mut self, span: Span, sig: &hax::TyFnSig) -> Result<FunSig, Error> {
326        let inputs = sig
327            .inputs
328            .iter()
329            .map(|x| self.translate_ty(span, x))
330            .try_collect()?;
331        let output = self.translate_ty(span, &sig.output)?;
332        Ok(FunSig {
333            is_unsafe: sig.safety == hax::Safety::Unsafe,
334            inputs,
335            output,
336        })
337    }
338
339    /// Translate generic args. Don't call directly; use `translate_xxx_ref` as much as possible.
340    pub fn translate_generic_args(
341        &mut self,
342        span: Span,
343        substs: &[hax::GenericArg],
344        trait_refs: &[hax::ImplExpr],
345    ) -> Result<GenericArgs, Error> {
346        use crate::hax::GenericArg::*;
347        trace!("{:?}", substs);
348
349        let mut regions = IndexVec::new();
350        let mut types = IndexVec::new();
351        let mut const_generics = IndexVec::new();
352        for param in substs {
353            match param {
354                Type(param_ty) => {
355                    types.push(self.translate_ty(span, param_ty)?);
356                }
357                Lifetime(region) => {
358                    regions.push(self.translate_region(span, region)?);
359                }
360                Const(c) => {
361                    const_generics.push(self.translate_constant_expr(span, c)?);
362                }
363            }
364        }
365        let trait_refs = self.translate_trait_impl_exprs(span, trait_refs)?;
366
367        Ok(GenericArgs {
368            regions,
369            types,
370            const_generics,
371            trait_refs,
372        })
373    }
374
375    /// Checks whether the given id corresponds to a built-in type.
376    pub(crate) fn recognize_builtin_type(
377        &mut self,
378        item: &hax::ItemRef,
379    ) -> Result<Option<BuiltinTy>, Error> {
380        let def = self.hax_def(item)?;
381        let ty = if def.lang_item == Some(sym::owned_box) && self.t_ctx.options.treat_box_as_builtin
382        {
383            Some(BuiltinTy::Box)
384        } else {
385            None
386        };
387        Ok(ty)
388    }
389
390    /// Translate a Dynamically Sized Type metadata kind.
391    ///
392    /// Returns `None` if the type is generic, or if it is not a DST.
393    pub fn translate_ptr_metadata(
394        &mut self,
395        span: Span,
396        item: &hax::ItemRef,
397    ) -> Result<PtrMetadata, Error> {
398        // prepare the call to the method
399        use rustc_middle::ty;
400        let tcx = self.t_ctx.tcx;
401        let rdefid = item.def_id.real_rust_def_id();
402        let hax_state = &self.hax_state;
403        let ty_env = hax_state.typing_env();
404        let ty = tcx
405            .type_of(rdefid)
406            .instantiate(tcx, item.rustc_args(hax_state));
407
408        // Get the tail type, which determines the metadata of `ty`.
409        let tail_ty = tcx.struct_tail_raw(
410            ty,
411            &rustc_middle::traits::ObligationCause::dummy(),
412            |ty| tcx.try_normalize_erasing_regions(ty_env, ty).unwrap_or(ty),
413            || {},
414        );
415        let hax_ty: hax::Ty = self.t_ctx.catch_sinto(hax_state, span, &tail_ty)?;
416
417        // If we're hiding `Sized`, let's consider everything to be sized.
418        let everything_is_sized = self.t_ctx.options.hide_marker_traits;
419        let ret = match tail_ty.kind() {
420            _ if everything_is_sized || tail_ty.is_sized(tcx, ty_env) => PtrMetadata::None,
421            ty::Str | ty::Slice(..) => PtrMetadata::Length,
422            ty::Dynamic(..) => match hax_ty.kind() {
423                hax::TyKind::Dynamic(dyn_binder, _) => {
424                    let vtable = self.translate_region_binder(
425                        span,
426                        &dyn_binder.predicates.predicates[0].clause.kind,
427                        |ctx, kind: &hax::ClauseKind| {
428                            let hax::ClauseKind::Trait(trait_predicate) = kind else {
429                                unreachable!()
430                            };
431                            ctx.translate_vtable_struct_ref(span, &trait_predicate.trait_ref)
432                        },
433                    )?;
434                    let vtable = self.erase_region_binder(vtable);
435                    PtrMetadata::VTable(vtable)
436                }
437                _ => unreachable!("Unexpected hax type {hax_ty:?} for dynamic type: {ty:?}"),
438            },
439            ty::Param(..) => PtrMetadata::InheritFrom(self.translate_ty(span, &hax_ty)?),
440            ty::Placeholder(..) | ty::Infer(..) | ty::Bound(..) => {
441                panic!(
442                    "We should never encounter a placeholder, infer, or bound type from ptr_metadata translation. Got: {tail_ty:?}"
443                )
444            }
445            _ => PtrMetadata::None,
446        };
447
448        Ok(ret)
449    }
450
451    /// Translate a type layout.
452    ///
453    /// Translates the layout as queried from rustc into
454    /// the more restricted [`Layout`].
455    #[tracing::instrument(skip(self))]
456    pub fn translate_layout(&self, item: &hax::ItemRef) -> Option<Layout> {
457        use rustc_abi as r_abi;
458
459        fn translate_variant_layout(
460            variant_layout: &r_abi::LayoutData<r_abi::FieldIdx, r_abi::VariantIdx>,
461            tag: Option<ScalarValue>,
462        ) -> VariantLayout {
463            let field_offsets = match &variant_layout.fields {
464                r_abi::FieldsShape::Arbitrary { offsets, .. } => {
465                    offsets.iter().map(|o| o.bytes()).collect()
466                }
467                r_abi::FieldsShape::Primitive | r_abi::FieldsShape::Union(_) => IndexVec::default(),
468                r_abi::FieldsShape::Array { .. } => panic!("Unexpected layout shape"),
469            };
470            VariantLayout {
471                field_offsets,
472                uninhabited: variant_layout.is_uninhabited(),
473                tag,
474            }
475        }
476
477        fn translate_primitive_int(int_ty: r_abi::Integer, signed: bool) -> IntegerTy {
478            if signed {
479                IntegerTy::Signed(match int_ty {
480                    r_abi::Integer::I8 => IntTy::I8,
481                    r_abi::Integer::I16 => IntTy::I16,
482                    r_abi::Integer::I32 => IntTy::I32,
483                    r_abi::Integer::I64 => IntTy::I64,
484                    r_abi::Integer::I128 => IntTy::I128,
485                })
486            } else {
487                IntegerTy::Unsigned(match int_ty {
488                    r_abi::Integer::I8 => UIntTy::U8,
489                    r_abi::Integer::I16 => UIntTy::U16,
490                    r_abi::Integer::I32 => UIntTy::U32,
491                    r_abi::Integer::I64 => UIntTy::U64,
492                    r_abi::Integer::I128 => UIntTy::U128,
493                })
494            }
495        }
496
497        let tcx = self.t_ctx.tcx;
498        let rdefid = item.def_id.real_rust_def_id();
499        let hax_state = self.hax_state_with_id();
500        assert_eq!(hax_state.owner(), item.def_id);
501        let ty_env = hax_state.typing_env();
502        let ty = tcx
503            .type_of(rdefid)
504            .instantiate(tcx, item.rustc_args(hax_state));
505        let pseudo_input = ty_env.as_query_input(ty);
506
507        // If layout computation returns an error, we return `None`.
508        let layout = tcx.layout_of(pseudo_input).ok()?.layout;
509        let (size, align) = if layout.is_sized() {
510            (
511                Some(layout.size().bytes()),
512                Some(layout.align().abi.bytes()),
513            )
514        } else {
515            (None, None)
516        };
517
518        // Get the layout of the discriminant when there is one (even if it is encoded in a niche).
519        let discriminant_layout = match layout.variants() {
520            r_abi::Variants::Multiple {
521                tag,
522                tag_encoding,
523                tag_field,
524                ..
525            } => {
526                // The tag_field is the index into the `offsets` vector.
527                let r_abi::FieldsShape::Arbitrary { offsets, .. } = layout.fields() else {
528                    unreachable!()
529                };
530
531                let tag_ty = match tag.primitive() {
532                    r_abi::Primitive::Int(int_ty, signed) => {
533                        translate_primitive_int(int_ty, signed)
534                    }
535                    // Try to handle pointer as integers of the same size.
536                    r_abi::Primitive::Pointer(_) => IntegerTy::Signed(IntTy::Isize),
537                    r_abi::Primitive::Float(_) => {
538                        unreachable!()
539                    }
540                };
541
542                let encoding = match tag_encoding {
543                    r_abi::TagEncoding::Direct => TagEncoding::Direct,
544                    r_abi::TagEncoding::Niche {
545                        untagged_variant, ..
546                    } => TagEncoding::Niche {
547                        untagged_variant: VariantId::from_usize(r_abi::VariantIdx::as_usize(
548                            *untagged_variant,
549                        )),
550                    },
551                };
552                offsets.get(*tag_field).map(|s| DiscriminantLayout {
553                    offset: r_abi::Size::bytes(*s),
554                    tag_ty,
555                    encoding,
556                })
557            }
558            r_abi::Variants::Single { .. } | r_abi::Variants::Empty => None,
559        };
560
561        let mut variant_layouts: IndexVec<VariantId, VariantLayout> = IndexVec::new();
562
563        match layout.variants() {
564            r_abi::Variants::Multiple { variants, .. } => {
565                let tag_ty = discriminant_layout
566                    .as_ref()
567                    .expect("No discriminant layout for enum?")
568                    .tag_ty;
569                let ptr_size = self.translated.the_target_information().target_pointer_size;
570                let tag_size = r_abi::Size::from_bytes(tag_ty.target_size(ptr_size));
571
572                for (id, variant_layout) in variants.iter_enumerated() {
573                    let tag = if variant_layout.is_uninhabited() {
574                        None
575                    } else {
576                        tcx.tag_for_variant(ty_env.as_query_input((ty, id)))
577                            .map(|s| match tag_ty {
578                                IntegerTy::Signed(int_ty) => {
579                                    ScalarValue::from_int(ptr_size, int_ty, s.to_int(tag_size))
580                                        .unwrap()
581                                }
582                                IntegerTy::Unsigned(uint_ty) => {
583                                    ScalarValue::from_uint(ptr_size, uint_ty, s.to_uint(tag_size))
584                                        .unwrap()
585                                }
586                            })
587                    };
588                    variant_layouts.push(translate_variant_layout(variant_layout, tag));
589                }
590            }
591            r_abi::Variants::Single { index } => {
592                if let r_abi::FieldsShape::Arbitrary { .. } = layout.fields() {
593                    let n_variants = match ty.kind() {
594                        _ if let Some(range) = ty.variant_range(tcx) => range.end.index(),
595                        _ => 1,
596                    };
597                    // All the variants not initialized below are uninhabited.
598                    variant_layouts = (0..n_variants)
599                        .map(|_| VariantLayout {
600                            field_offsets: IndexVec::default(),
601                            uninhabited: true,
602                            tag: None,
603                        })
604                        .collect();
605                    variant_layouts[index.index()] = translate_variant_layout(&layout, None);
606                }
607            }
608            r_abi::Variants::Empty => {}
609        }
610
611        Some(Layout {
612            size,
613            align,
614            discriminant_layout,
615            uninhabited: layout.is_uninhabited(),
616            variant_layouts,
617        })
618    }
619
620    /// Generate a naive layout for this type.
621    pub fn generate_naive_layout(&self, span: Span, ty: &TypeDeclKind) -> Result<Layout, Error> {
622        match ty {
623            TypeDeclKind::Struct(fields) => {
624                let mut size = 0;
625                let mut align = 0;
626                let ptr_size = self.translated.the_target_information().target_pointer_size;
627                let field_offsets = fields.map_ref(|field| {
628                    let offset = size;
629                    let size_of_ty = match field.ty.kind() {
630                        TyKind::Literal(literal_ty) => literal_ty.target_size(ptr_size) as u64,
631                        // This is a lie, the pointers could be fat...
632                        TyKind::Ref(..) | TyKind::RawPtr(..) | TyKind::FnPtr(..) => ptr_size,
633                        _ => panic!("Unsupported type for `generate_naive_layout`: {ty:?}"),
634                    };
635                    size += size_of_ty;
636                    // For these types, align == size is good enough.
637                    align = std::cmp::max(align, size);
638                    offset
639                });
640
641                Ok(Layout {
642                    size: Some(size),
643                    align: Some(align),
644                    discriminant_layout: None,
645                    uninhabited: false,
646                    variant_layouts: IndexVec::from([VariantLayout {
647                        field_offsets,
648                        tag: None,
649                        uninhabited: false,
650                    }]),
651                })
652            }
653            _ => raise_error!(
654                self,
655                span,
656                "`generate_naive_layout` only supports structs at the moment"
657            ),
658        }
659    }
660
661    /// Translate the body of a type declaration.
662    ///
663    /// Note that the type may be external, in which case we translate the body
664    /// only if it is public (i.e., it is a public enumeration, or it is a
665    /// struct with only public fields).
666    pub(crate) fn translate_adt_def(
667        &mut self,
668        trans_id: TypeDeclId,
669        def_span: Span,
670        item_meta: &ItemMeta,
671        def: &hax::FullDef,
672    ) -> Result<TypeDeclKind, Error> {
673        use crate::hax::AdtKind;
674        let hax::FullDefKind::Adt {
675            adt_kind, variants, ..
676        } = def.kind()
677        else {
678            unreachable!()
679        };
680
681        if item_meta.opacity.is_opaque() {
682            return Ok(TypeDeclKind::Opaque);
683        }
684
685        trace!("{}", trans_id);
686
687        // In case the type is external, check if we should consider the type as
688        // transparent (i.e., extract its body). If it is an enumeration, then yes
689        // (because the variants of public enumerations are public, together with their
690        // fields). If it is a structure, we check if all the fields are public.
691        let contents_are_public = match adt_kind {
692            AdtKind::Enum => true,
693            AdtKind::Struct | AdtKind::Union => {
694                // Check the unique variant
695                error_assert!(self, def_span, variants.len() == 1);
696                variants[hax::VariantIdx::from(0usize)]
697                    .fields
698                    .iter()
699                    .all(|f| matches!(f.vis, Visibility::Public))
700            }
701            // The rest are fake adt kinds that won't reach here.
702            _ => unreachable!(),
703        };
704
705        if item_meta
706            .opacity
707            .with_content_visibility(contents_are_public)
708            .is_opaque()
709        {
710            return Ok(TypeDeclKind::Opaque);
711        }
712
713        // The type is transparent: explore the variants
714        let mut translated_variants: IndexVec<VariantId, Variant> = Default::default();
715        for (i, var_def) in variants.iter().enumerate() {
716            trace!("variant {i}: {var_def:?}");
717
718            let mut fields: IndexVec<FieldId, Field> = Default::default();
719            /* This is for sanity: check that either all the fields have names, or
720             * none of them has */
721            let mut have_names: Option<bool> = None;
722            for (j, field_def) in var_def.fields.iter().enumerate() {
723                trace!("variant {i}: field {j}: {field_def:?}");
724                let field_span = self.t_ctx.translate_span(&field_def.span);
725                // Translate the field type
726                let ty = self.translate_ty(field_span, &field_def.ty)?;
727                let field_full_def =
728                    self.hax_def(&def.this().with_def_id(self.hax_state(), &field_def.did))?;
729                let field_attrs = self.t_ctx.translate_attr_info(&field_full_def);
730
731                // Retrieve the field name.
732                let field_name = field_def.name.map(|s| s.to_string());
733                // Sanity check
734                match &have_names {
735                    None => {
736                        have_names = match &field_name {
737                            None => Some(false),
738                            Some(_) => Some(true),
739                        }
740                    }
741                    Some(b) => {
742                        error_assert!(self, field_span, *b == field_name.is_some());
743                    }
744                };
745
746                // Store the field
747                let field = Field {
748                    span: field_span,
749                    attr_info: field_attrs,
750                    name: field_name,
751                    ty,
752                };
753                fields.push(field);
754            }
755
756            let discriminant = self.translate_discriminant(def_span, &var_def.discr_val)?;
757            let variant_span = self.t_ctx.translate_span(&var_def.span);
758            let variant_name = var_def.name.to_string();
759            let variant_full_def =
760                self.hax_def(&def.this().with_def_id(self.hax_state(), &var_def.def_id))?;
761            let variant_attrs = self.t_ctx.translate_attr_info(&variant_full_def);
762
763            let mut variant = Variant {
764                span: variant_span,
765                attr_info: variant_attrs,
766                name: variant_name,
767                fields,
768                discriminant,
769            };
770            // Propagate a `#[charon::variants_prefix(..)]` or `#[charon::variants_suffix(..)]` attribute to the variants.
771            if variant.attr_info.rename.is_none() {
772                let prefix = item_meta
773                    .attr_info
774                    .attributes
775                    .iter()
776                    .filter_map(|a| a.as_variants_prefix())
777                    .next()
778                    .map(|attr| attr.as_str());
779                let suffix = item_meta
780                    .attr_info
781                    .attributes
782                    .iter()
783                    .filter_map(|a| a.as_variants_suffix())
784                    .next()
785                    .map(|attr| attr.as_str());
786                if prefix.is_some() || suffix.is_some() {
787                    let prefix = prefix.unwrap_or_default();
788                    let suffix = suffix.unwrap_or_default();
789                    let name = &variant.name;
790                    variant.attr_info.rename = Some(format!("{prefix}{name}{suffix}"));
791                }
792            }
793            translated_variants.push(variant);
794        }
795
796        // Register the type
797        let type_def_kind: TypeDeclKind = match adt_kind {
798            AdtKind::Struct => TypeDeclKind::Struct(translated_variants[0].fields.clone()),
799            AdtKind::Enum => TypeDeclKind::Enum(translated_variants),
800            AdtKind::Union => TypeDeclKind::Union(translated_variants[0].fields.clone()),
801            // The rest are fake adt kinds that won't reach here.
802            _ => unreachable!(),
803        };
804
805        Ok(type_def_kind)
806    }
807
808    fn translate_discriminant(
809        &mut self,
810        def_span: Span,
811        discr: &hax::DiscriminantValue,
812    ) -> Result<Literal, Error> {
813        let ty = self.translate_ty(def_span, &discr.ty)?;
814        let lit_ty = ty.kind().as_literal().unwrap();
815        match Literal::from_bits(lit_ty, discr.val) {
816            Some(lit) => Ok(lit),
817            None => raise_error!(self, def_span, "unexpected discriminant type: {ty:?}",),
818        }
819    }
820
821    pub fn translate_repr_options(&mut self, hax_repr_options: &hax::ReprOptions) -> ReprOptions {
822        let repr_algo = if hax_repr_options.flags.is_c {
823            ReprAlgorithm::C
824        } else {
825            ReprAlgorithm::Rust
826        };
827
828        let align_mod = if let Some(align) = &hax_repr_options.align {
829            Some(AlignmentModifier::Align(align.bytes))
830        } else if let Some(pack) = &hax_repr_options.pack {
831            Some(AlignmentModifier::Pack(pack.bytes))
832        } else {
833            None
834        };
835
836        ReprOptions {
837            transparent: hax_repr_options.flags.is_transparent,
838            explicit_discr_type: hax_repr_options.int_specified,
839            repr_algo,
840            align_modif: align_mod,
841        }
842    }
843}
charon_driver/translate/translate_types.rs

charon_driver/translate/
translate_types.rs
