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

charon_driver/translate/
translate_types.rs
