charon_driver/translate/
translate_types.rs

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

charon_driver/translate/
translate_types.rs
