charon_driver/translate/
translate_types.rs

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

charon_driver/translate/
translate_types.rs
