charon_driver/translate/
translate_types.rs

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

charon_driver/translate/
translate_types.rs
