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

charon_driver/translate/
translate_types.rs
