charon_driver/translate/
translate_types.rs

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

charon_driver/translate/
translate_types.rs
